> ./run-satallax 600 s4/SYM/SYM001+1 -------------------====================== ;------------------------------------------------------------------------------ ("thf" "mu_type" "type" (":" "mu" "$tType")) ("thf" "meq_ind_type" "type" (":" "meq_ind" (">" "mu" (">" "mu" (">" "$i" "$o"))))) ("thf" "meq_ind" "definition" ("=" "meq_ind" ("^" ((":" "X" "mu") (":" "Y" "mu") (":" "W" "$i")) ("=" "X" "Y")))) ("thf" "meq_prop_type" "type" (":" "meq_prop" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "meq_prop" "definition" ("=" "meq_prop" ("^" ((":" "X" (">" "$i" "$o")) (":" "Y" (">" "$i" "$o")) (":" "W" "$i")) ("=" ("@" "X" "W") ("@" "Y" "W"))))) ("thf" "mnot_type" "type" (":" "mnot" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("thf" "mnot" "definition" ("=" "mnot" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "W" "$i")) ("~" ("@" "Phi" "W"))))) ("thf" "mor_type" "type" (":" "mor" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mor" "definition" ("=" "mor" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o")) (":" "W" "$i")) ("|" ("@" "Phi" "W") ("@" "Psi" "W"))))) ("thf" "mbox_type" "type" (":" "mbox" (">" (">" "$i" (">" "$i" "$o")) (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mbox" "definition" ("=" "mbox" ("^" ((":" "R" (">" "$i" (">" "$i" "$o"))) (":" "Phi" (">" "$i" "$o")) (":" "W" "$i")) ("!" ((":" "V" "$i")) ("|" ("~" ("@" ("@" "R" "W") "V")) ("@" "Phi" "V")))))) ("thf" "mforall_ind_type" "type" (":" "mforall_ind" (">" (">" "mu" (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mforall_ind" "definition" ("=" "mforall_ind" ("^" ((":" "Phi" (">" "mu" (">" "$i" "$o"))) (":" "W" "$i")) ("!" ((":" "X" "mu")) ("@" ("@" "Phi" "X") "W"))))) ("thf" "mforall_prop_type" "type" (":" "mforall_prop" (">" (">" (">" "$i" "$o") (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mforall_prop" "definition" ("=" "mforall_prop" ("^" ((":" "Phi" (">" (">" "$i" "$o") (">" "$i" "$o"))) (":" "W" "$i")) ("!" ((":" "P" (">" "$i" "$o"))) ("@" ("@" "Phi" "P") "W"))))) ("thf" "mtrue_type" "type" (":" "mtrue" (">" "$i" "$o"))) ("thf" "mtrue" "definition" ("=" "mtrue" ("^" ((":" "W" "$i")) "$true"))) ("thf" "mfalse_type" "type" (":" "mfalse" (">" "$i" "$o"))) ("thf" "mfalse" "definition" ("=" "mfalse" ("@" "mnot" "mtrue"))) ("thf" "mand_type" "type" (":" "mand" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mand" "definition" ("=" "mand" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" "mnot" ("@" ("@" "mor" ("@" "mnot" "Phi")) ("@" "mnot" "Psi")))))) ("thf" "mimplies_type" "type" (":" "mimplies" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mimplies" "definition" ("=" "mimplies" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" ("@" "mor" ("@" "mnot" "Phi")) "Psi")))) ("thf" "mimplied_type" "type" (":" "mimplied" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mimplied" "definition" ("=" "mimplied" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" ("@" "mor" ("@" "mnot" "Psi")) "Phi")))) ("thf" "mequiv_type" "type" (":" "mequiv" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mequiv" "definition" ("=" "mequiv" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" ("@" "mand" ("@" ("@" "mimplies" "Phi") "Psi")) ("@" ("@" "mimplies" "Psi") "Phi"))))) ("thf" "mxor_type" "type" (":" "mxor" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mxor" "definition" ("=" "mxor" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" "mnot" ("@" ("@" "mequiv" "Phi") "Psi"))))) ("thf" "mdia_type" "type" (":" "mdia" (">" (">" "$i" (">" "$i" "$o")) (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mdia" "definition" ("=" "mdia" ("^" ((":" "R" (">" "$i" (">" "$i" "$o"))) (":" "Phi" (">" "$i" "$o"))) ("@" "mnot" ("@" ("@" "mbox" "R") ("@" "mnot" "Phi")))))) ("thf" "mexists_ind_type" "type" (":" "mexists_ind" (">" (">" "mu" (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mexists_ind" "definition" ("=" "mexists_ind" ("^" ((":" "Phi" (">" "mu" (">" "$i" "$o")))) ("@" "mnot" ("@" "mforall_ind" ("^" ((":" "X" "mu")) ("@" "mnot" ("@" "Phi" "X")))))))) ("thf" "mexists_prop_type" "type" (":" "mexists_prop" (">" (">" (">" "$i" "$o") (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mexists_prop" "definition" ("=" "mexists_prop" ("^" ((":" "Phi" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("@" "mnot" ("@" "mforall_prop" ("^" ((":" "P" (">" "$i" "$o"))) ("@" "mnot" ("@" "Phi" "P")))))))) ("thf" "mreflexive_type" "type" (":" "mreflexive" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mreflexive" "definition" ("=" "mreflexive" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i")) ("@" ("@" "R" "S") "S"))))) ("thf" "msymmetric_type" "type" (":" "msymmetric" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "msymmetric" "definition" ("=" "msymmetric" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i")) ("=>" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "T") "S")))))) ("thf" "mserial_type" "type" (":" "mserial" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mserial" "definition" ("=" "mserial" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i")) ("?" ((":" "T" "$i")) ("@" ("@" "R" "S") "T")))))) ("thf" "mtransitive_type" "type" (":" "mtransitive" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mtransitive" "definition" ("=" "mtransitive" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "T") "U")) ("@" ("@" "R" "S") "U")))))) ("thf" "meuclidean_type" "type" (":" "meuclidean" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "meuclidean" "definition" ("=" "meuclidean" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("@" ("@" "R" "T") "U")))))) ("thf" "mpartially_functional_type" "type" (":" "mpartially_functional" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mpartially_functional" "definition" ("=" "mpartially_functional" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("=" "T" "U")))))) ("thf" "mfunctional_type" "type" (":" "mfunctional" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mfunctional" "definition" ("=" "mfunctional" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i")) ("?" ((":" "T" "$i")) ("&" ("@" ("@" "R" "S") "T") ("!" ((":" "U" "$i")) ("=>" ("@" ("@" "R" "S") "U") ("=" "T" "U"))))))))) ("thf" "mweakly_dense_type" "type" (":" "mweakly_dense" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mweakly_dense" "definition" ("=" "mweakly_dense" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("@" ("@" "R" "S") "T") ("?" ((":" "U" "$i")) ("&" ("@" ("@" "R" "S") "U") ("@" ("@" "R" "U") "T")))))))) ("thf" "mweakly_connected_type" "type" (":" "mweakly_connected" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mweakly_connected" "definition" ("=" "mweakly_connected" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("|" ("@" ("@" "R" "T") "U") ("|" ("=" "T" "U") ("@" ("@" "R" "U") "T")))))))) ("thf" "mweakly_directed_type" "type" (":" "mweakly_directed" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mweakly_directed" "definition" ("=" "mweakly_directed" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("?" ((":" "V" "$i")) ("&" ("@" ("@" "R" "T") "V") ("@" ("@" "R" "U") "V")))))))) ("thf" "mvalid_type" "type" (":" "mvalid" (">" (">" "$i" "$o") "$o"))) ("thf" "mvalid" "definition" ("=" "mvalid" ("^" ((":" "Phi" (">" "$i" "$o"))) ("!" ((":" "W" "$i")) ("@" "Phi" "W"))))) ("thf" "msatisfiable_type" "type" (":" "msatisfiable" (">" (">" "$i" "$o") "$o"))) ("thf" "msatisfiable" "definition" ("=" "msatisfiable" ("^" ((":" "Phi" (">" "$i" "$o"))) ("?" ((":" "W" "$i")) ("@" "Phi" "W"))))) ("thf" "mcountersatisfiable_type" "type" (":" "mcountersatisfiable" (">" (">" "$i" "$o") "$o"))) ("thf" "mcountersatisfiable" "definition" ("=" "mcountersatisfiable" ("^" ((":" "Phi" (">" "$i" "$o"))) ("?" ((":" "W" "$i")) ("~" ("@" "Phi" "W")))))) ("thf" "minvalid_type" "type" (":" "minvalid" (">" (">" "$i" "$o") "$o"))) ("thf" "minvalid" "definition" ("=" "minvalid" ("^" ((":" "Phi" (">" "$i" "$o"))) ("!" ((":" "W" "$i")) ("~" ("@" "Phi" "W")))))) ("thf" "rel_s4_type" "type" (":" "rel_s4" (">" "$i" (">" "$i" "$o")))) ("thf" "mbox_s4_type" "type" (":" "mbox_s4" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("thf" "mbox_s4" "definition" ("=" "mbox_s4" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "W" "$i")) ("!" ((":" "V" "$i")) ("|" ("~" ("@" ("@" "rel_s4" "W") "V")) ("@" "Phi" "V")))))) ("thf" "mdia_s4_type" "type" (":" "mdia_s4" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("thf" "mdia_s4" "definition" ("=" "mdia_s4" ("^" ((":" "Phi" (">" "$i" "$o"))) ("@" "mnot" ("@" "mbox_s4" ("@" "mnot" "Phi")))))) ("thf" "a1" "axiom" ("@" "mreflexive" "rel_s4")) ("thf" "a2" "axiom" ("@" "mtransitive" "rel_s4")) ("thf" "f_type" "type" (":" "f" (">" "mu" (">" "$i" "$o")))) ; This is the conjecture ("thf" "prove" "conjecture" ("@" "mvalid" ("@" ("@" "mimplies" ("@" "mforall_ind" ("^" ((":" "X" "mu")) ("@" "mbox_s4" ("@" "f" "X"))))) ("@" "mbox_s4" ("@" "mforall_ind" ("^" ((":" "X" "mu")) ("@" "f" "X"))))))) ;------------------------------------------------------------------------------ -------------------====================== % SZS status Theorem % SZS output start Proof Clauses: 1 0 2 0 -3 0 3 -4 0 4 5 0 4 -6 0 6 -7 0 7 8 0 7 -9 0 9 -10 0 -5 10 -8 0 8 -8 -11 -12 0 11 0 12 0 -2 13 0 -1 14 0 -2 13 0 -1 14 0 -5 15 0 -13 -8 8 -14 0 -13 -14 14 -14 0 8 -14 -11 -16 0 -13 17 0 -2 13 0 -1 14 0 -13 18 0 -2 19 0 -1 20 0 -15 10 -8 0 -15 -14 21 0 -15 -8 10 0 -15 22 0 -15 23 0 -1 14 0 14 -14 -11 -11 0 14 -8 -11 -16 0 -17 14 -14 -14 0 -17 8 -8 -14 0 -17 -14 14 -14 0 -17 -8 8 -14 0 -17 24 0 -17 25 0 -18 14 -26 -8 0 -18 8 -20 -8 0 -18 27 0 -18 28 0 -19 -14 26 -26 0 -19 -8 20 -26 0 -19 29 0 -19 30 0 -19 -20 20 -20 0 -18 -20 8 -8 0 -13 -20 8 -8 0 14 -20 -16 -16 0 8 -20 -16 -12 0 10 -21 -31 -16 0 10 -10 -31 -12 0 -22 -8 10 0 -23 -14 21 0 31 0 -24 32 8 0 -32 -14 -8 0 -25 33 14 0 -33 -14 -14 0 26 -20 -12 -16 0 26 -14 -16 -11 0 26 -8 -16 -16 0 -1 20 0 20 -20 -12 -12 0 20 -14 -16 -16 0 20 -8 -16 -12 0 -27 34 8 0 -34 -8 -20 0 -28 35 14 0 -35 -8 -26 0 -19 -26 26 -20 0 -18 -26 14 -8 0 -13 -26 14 -8 0 20 -26 -12 -16 0 26 -26 -12 -11 0 14 -26 -16 -11 0 8 -26 -16 -16 0 -29 20 -20 -20 0 -29 26 -26 -20 0 -29 -26 26 -20 0 -29 -20 20 -20 0 -29 36 0 -29 37 0 -30 20 -8 -26 0 -30 26 -14 -26 0 -30 -14 26 -26 0 -30 -8 20 -26 0 -30 38 0 -30 39 0 -36 40 20 0 -40 -20 -20 0 -37 41 26 0 -41 -20 -26 0 -38 42 20 0 -42 -26 -8 0 -39 43 26 0 -43 -26 -14 0 Atoms: Atom 1: (! (\x0:$i.(rel_s4 x0 x0))) Atom 2: (! (\x0:$i.(! (\x1:$i.(! (\x2:$i.(((~ (rel_s4 x0 x1)) | (~ (rel_s4 x1 x2))) | (rel_s4 x0 x2)))))))) Atom 3: (! (\x0:$i.((~ (! (\x1:mu.(! (\x2:$i.((~ (rel_s4 x0 x2)) | (f x1 x2))))))) | (! (\x1:$i.((~ (rel_s4 x0 x1)) | (! (\x2:mu.(f x2 x1))))))))) Atom 4: ((~ (! (\x0:mu.(! (\x1:$i.((~ (rel_s4 __1 x1)) | (f x0 x1))))))) | (! (\x0:$i.((~ (rel_s4 __1 x0)) | (! (\x1:mu.(f x1 x0))))))) Atom 5: (! (\x0:mu.(! (\x1:$i.((~ (rel_s4 __1 x1)) | (f x0 x1)))))) Atom 6: (! (\x0:$i.((~ (rel_s4 __1 x0)) | (! (\x1:mu.(f x1 x0)))))) Atom 7: ((~ (rel_s4 __1 __2)) | (! (\x0:mu.(f x0 __2)))) Atom 8: (rel_s4 __1 __2) Atom 9: (! (\x0:mu.(f x0 __2))) Atom 10: (f __3 __2) Atom 11: (__1 = __1) Atom 12: (__2 = __2) Atom 13: (! (\x0:$i.(! (\x1:$i.(((~ (rel_s4 __1 x0)) | (~ (rel_s4 x0 x1))) | (rel_s4 __1 x1)))))) Atom 14: (rel_s4 __1 __1) Atom 15: (! (\x0:$i.((~ (rel_s4 __1 x0)) | (f __3 x0)))) Atom 16: (__1 = __2) Atom 17: (! (\x0:$i.(((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 x0))) | (rel_s4 __1 x0)))) Atom 18: (! (\x0:$i.(((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 x0))) | (rel_s4 __1 x0)))) Atom 19: (! (\x0:$i.(! (\x1:$i.(((~ (rel_s4 __2 x0)) | (~ (rel_s4 x0 x1))) | (rel_s4 __2 x1)))))) Atom 20: (rel_s4 __2 __2) Atom 21: (f __3 __1) Atom 22: ((~ (rel_s4 __1 __2)) | (f __3 __2)) Atom 23: ((~ (rel_s4 __1 __1)) | (f __3 __1)) Atom 24: (((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __2))) | (rel_s4 __1 __2)) Atom 25: (((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __1))) | (rel_s4 __1 __1)) Atom 26: (rel_s4 __2 __1) Atom 27: (((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __2))) | (rel_s4 __1 __2)) Atom 28: (((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __1))) | (rel_s4 __1 __1)) Atom 29: (! (\x0:$i.(((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 x0))) | (rel_s4 __2 x0)))) Atom 30: (! (\x0:$i.(((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 x0))) | (rel_s4 __2 x0)))) Atom 31: (__3 = __3) Atom 32: ((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __2))) Atom 33: ((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __1))) Atom 34: ((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __2))) Atom 35: ((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __1))) Atom 36: (((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __2))) | (rel_s4 __2 __2)) Atom 37: (((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __1))) | (rel_s4 __2 __1)) Atom 38: (((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __2))) | (rel_s4 __2 __2)) Atom 39: (((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __1))) | (rel_s4 __2 __1)) Atom 40: ((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __2))) Atom 41: ((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __1))) Atom 42: ((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __2))) Atom 43: ((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __1))) % SZS output end Proof > ./run-satallax 600 s4/SYM/SYM015+1 -------------------====================== ;------------------------------------------------------------------------------ ("thf" "mu_type" "type" (":" "mu" "$tType")) ("thf" "meq_ind_type" "type" (":" "meq_ind" (">" "mu" (">" "mu" (">" "$i" "$o"))))) ("thf" "meq_ind" "definition" ("=" "meq_ind" ("^" ((":" "X" "mu") (":" "Y" "mu") (":" "W" "$i")) ("=" "X" "Y")))) ("thf" "meq_prop_type" "type" (":" "meq_prop" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "meq_prop" "definition" ("=" "meq_prop" ("^" ((":" "X" (">" "$i" "$o")) (":" "Y" (">" "$i" "$o")) (":" "W" "$i")) ("=" ("@" "X" "W") ("@" "Y" "W"))))) ("thf" "mnot_type" "type" (":" "mnot" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("thf" "mnot" "definition" ("=" "mnot" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "W" "$i")) ("~" ("@" "Phi" "W"))))) ("thf" "mor_type" "type" (":" "mor" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mor" "definition" ("=" "mor" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o")) (":" "W" "$i")) ("|" ("@" "Phi" "W") ("@" "Psi" "W"))))) ("thf" "mbox_type" "type" (":" "mbox" (">" (">" "$i" (">" "$i" "$o")) (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mbox" "definition" ("=" "mbox" ("^" ((":" "R" (">" "$i" (">" "$i" "$o"))) (":" "Phi" (">" "$i" "$o")) (":" "W" "$i")) ("!" ((":" "V" "$i")) ("|" ("~" ("@" ("@" "R" "W") "V")) ("@" "Phi" "V")))))) ("thf" "mforall_ind_type" "type" (":" "mforall_ind" (">" (">" "mu" (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mforall_ind" "definition" ("=" "mforall_ind" ("^" ((":" "Phi" (">" "mu" (">" "$i" "$o"))) (":" "W" "$i")) ("!" ((":" "X" "mu")) ("@" ("@" "Phi" "X") "W"))))) ("thf" "mforall_prop_type" "type" (":" "mforall_prop" (">" (">" (">" "$i" "$o") (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mforall_prop" "definition" ("=" "mforall_prop" ("^" ((":" "Phi" (">" (">" "$i" "$o") (">" "$i" "$o"))) (":" "W" "$i")) ("!" ((":" "P" (">" "$i" "$o"))) ("@" ("@" "Phi" "P") "W"))))) ("thf" "mtrue_type" "type" (":" "mtrue" (">" "$i" "$o"))) ("thf" "mtrue" "definition" ("=" "mtrue" ("^" ((":" "W" "$i")) "$true"))) ("thf" "mfalse_type" "type" (":" "mfalse" (">" "$i" "$o"))) ("thf" "mfalse" "definition" ("=" "mfalse" ("@" "mnot" "mtrue"))) ("thf" "mand_type" "type" (":" "mand" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mand" "definition" ("=" "mand" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" "mnot" ("@" ("@" "mor" ("@" "mnot" "Phi")) ("@" "mnot" "Psi")))))) ("thf" "mimplies_type" "type" (":" "mimplies" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mimplies" "definition" ("=" "mimplies" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" ("@" "mor" ("@" "mnot" "Phi")) "Psi")))) ("thf" "mimplied_type" "type" (":" "mimplied" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mimplied" "definition" ("=" "mimplied" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" ("@" "mor" ("@" "mnot" "Psi")) "Phi")))) ("thf" "mequiv_type" "type" (":" "mequiv" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mequiv" "definition" ("=" "mequiv" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" ("@" "mand" ("@" ("@" "mimplies" "Phi") "Psi")) ("@" ("@" "mimplies" "Psi") "Phi"))))) ("thf" "mxor_type" "type" (":" "mxor" (">" (">" "$i" "$o") (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mxor" "definition" ("=" "mxor" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "Psi" (">" "$i" "$o"))) ("@" "mnot" ("@" ("@" "mequiv" "Phi") "Psi"))))) ("thf" "mdia_type" "type" (":" "mdia" (">" (">" "$i" (">" "$i" "$o")) (">" (">" "$i" "$o") (">" "$i" "$o"))))) ("thf" "mdia" "definition" ("=" "mdia" ("^" ((":" "R" (">" "$i" (">" "$i" "$o"))) (":" "Phi" (">" "$i" "$o"))) ("@" "mnot" ("@" ("@" "mbox" "R") ("@" "mnot" "Phi")))))) ("thf" "mexists_ind_type" "type" (":" "mexists_ind" (">" (">" "mu" (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mexists_ind" "definition" ("=" "mexists_ind" ("^" ((":" "Phi" (">" "mu" (">" "$i" "$o")))) ("@" "mnot" ("@" "mforall_ind" ("^" ((":" "X" "mu")) ("@" "mnot" ("@" "Phi" "X")))))))) ("thf" "mexists_prop_type" "type" (":" "mexists_prop" (">" (">" (">" "$i" "$o") (">" "$i" "$o")) (">" "$i" "$o")))) ("thf" "mexists_prop" "definition" ("=" "mexists_prop" ("^" ((":" "Phi" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("@" "mnot" ("@" "mforall_prop" ("^" ((":" "P" (">" "$i" "$o"))) ("@" "mnot" ("@" "Phi" "P")))))))) ("thf" "mreflexive_type" "type" (":" "mreflexive" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mreflexive" "definition" ("=" "mreflexive" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i")) ("@" ("@" "R" "S") "S"))))) ("thf" "msymmetric_type" "type" (":" "msymmetric" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "msymmetric" "definition" ("=" "msymmetric" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i")) ("=>" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "T") "S")))))) ("thf" "mserial_type" "type" (":" "mserial" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mserial" "definition" ("=" "mserial" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i")) ("?" ((":" "T" "$i")) ("@" ("@" "R" "S") "T")))))) ("thf" "mtransitive_type" "type" (":" "mtransitive" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mtransitive" "definition" ("=" "mtransitive" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "T") "U")) ("@" ("@" "R" "S") "U")))))) ("thf" "meuclidean_type" "type" (":" "meuclidean" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "meuclidean" "definition" ("=" "meuclidean" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("@" ("@" "R" "T") "U")))))) ("thf" "mpartially_functional_type" "type" (":" "mpartially_functional" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mpartially_functional" "definition" ("=" "mpartially_functional" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("=" "T" "U")))))) ("thf" "mfunctional_type" "type" (":" "mfunctional" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mfunctional" "definition" ("=" "mfunctional" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i")) ("?" ((":" "T" "$i")) ("&" ("@" ("@" "R" "S") "T") ("!" ((":" "U" "$i")) ("=>" ("@" ("@" "R" "S") "U") ("=" "T" "U"))))))))) ("thf" "mweakly_dense_type" "type" (":" "mweakly_dense" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mweakly_dense" "definition" ("=" "mweakly_dense" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("@" ("@" "R" "S") "T") ("?" ((":" "U" "$i")) ("&" ("@" ("@" "R" "S") "U") ("@" ("@" "R" "U") "T")))))))) ("thf" "mweakly_connected_type" "type" (":" "mweakly_connected" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mweakly_connected" "definition" ("=" "mweakly_connected" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("|" ("@" ("@" "R" "T") "U") ("|" ("=" "T" "U") ("@" ("@" "R" "U") "T")))))))) ("thf" "mweakly_directed_type" "type" (":" "mweakly_directed" (">" (">" "$i" (">" "$i" "$o")) "$o"))) ("thf" "mweakly_directed" "definition" ("=" "mweakly_directed" ("^" ((":" "R" (">" "$i" (">" "$i" "$o")))) ("!" ((":" "S" "$i") (":" "T" "$i") (":" "U" "$i")) ("=>" ("&" ("@" ("@" "R" "S") "T") ("@" ("@" "R" "S") "U")) ("?" ((":" "V" "$i")) ("&" ("@" ("@" "R" "T") "V") ("@" ("@" "R" "U") "V")))))))) ("thf" "mvalid_type" "type" (":" "mvalid" (">" (">" "$i" "$o") "$o"))) ("thf" "mvalid" "definition" ("=" "mvalid" ("^" ((":" "Phi" (">" "$i" "$o"))) ("!" ((":" "W" "$i")) ("@" "Phi" "W"))))) ("thf" "msatisfiable_type" "type" (":" "msatisfiable" (">" (">" "$i" "$o") "$o"))) ("thf" "msatisfiable" "definition" ("=" "msatisfiable" ("^" ((":" "Phi" (">" "$i" "$o"))) ("?" ((":" "W" "$i")) ("@" "Phi" "W"))))) ("thf" "mcountersatisfiable_type" "type" (":" "mcountersatisfiable" (">" (">" "$i" "$o") "$o"))) ("thf" "mcountersatisfiable" "definition" ("=" "mcountersatisfiable" ("^" ((":" "Phi" (">" "$i" "$o"))) ("?" ((":" "W" "$i")) ("~" ("@" "Phi" "W")))))) ("thf" "minvalid_type" "type" (":" "minvalid" (">" (">" "$i" "$o") "$o"))) ("thf" "minvalid" "definition" ("=" "minvalid" ("^" ((":" "Phi" (">" "$i" "$o"))) ("!" ((":" "W" "$i")) ("~" ("@" "Phi" "W")))))) ("thf" "rel_s4_type" "type" (":" "rel_s4" (">" "$i" (">" "$i" "$o")))) ("thf" "mbox_s4_type" "type" (":" "mbox_s4" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("thf" "mbox_s4" "definition" ("=" "mbox_s4" ("^" ((":" "Phi" (">" "$i" "$o")) (":" "W" "$i")) ("!" ((":" "V" "$i")) ("|" ("~" ("@" ("@" "rel_s4" "W") "V")) ("@" "Phi" "V")))))) ("thf" "mdia_s4_type" "type" (":" "mdia_s4" (">" (">" "$i" "$o") (">" "$i" "$o")))) ("thf" "mdia_s4" "definition" ("=" "mdia_s4" ("^" ((":" "Phi" (">" "$i" "$o"))) ("@" "mnot" ("@" "mbox_s4" ("@" "mnot" "Phi")))))) ("thf" "a1" "axiom" ("@" "mreflexive" "rel_s4")) ("thf" "a2" "axiom" ("@" "mtransitive" "rel_s4")) ("thf" "f_type" "type" (":" "f" (">" "mu" (">" "$i" "$o")))) ("thf" "a_type" "type" (":" "a" "mu")) ("thf" "x_type" "type" (":" "x" "mu")) ; This is the conjecture ("thf" "prove" "conjecture" ("@" "mvalid" ("@" ("@" "mimplies" ("@" "mforall_ind" ("^" ((":" "X" "mu")) ("@" ("@" "mor" ("@" "mbox_s4" ("@" "f" "x"))) ("@" "mbox_s4" ("@" "mnot" ("@" "f" "x"))))))) ("@" "mbox_s4" ("@" ("@" "mequiv" ("@" "mbox_s4" ("@" "f" "a"))) ("@" "f" "a")))))) ;------------------------------------------------------------------------------ -------------------====================== % SZS status CounterSatisfiable % SZS output start FiniteModel Clauses: 1 0 2 0 -3 0 3 -4 0 4 5 0 4 -6 0 6 -7 0 7 8 0 7 9 0 -9 -10 -11 0 11 12 0 11 -13 0 13 -14 0 10 13 0 10 -12 0 12 -12 -15 -16 0 -13 12 -17 0 14 18 0 14 -19 0 -13 19 -18 0 19 -12 -15 -20 0 -13 -18 19 0 15 0 16 0 -13 21 0 -2 22 0 -1 17 0 -13 14 0 -2 23 0 -1 24 0 -1 17 0 17 -18 -16 -20 0 17 -8 -25 -16 0 18 -18 -16 -26 0 18 -8 -25 -20 0 19 -19 -15 -26 0 12 -19 -15 -20 0 -13 27 0 -2 28 0 -1 29 0 26 0 -21 -17 12 0 -22 -18 18 -17 0 -22 -8 17 -30 0 -22 31 0 -22 32 0 -22 33 0 -22 -17 17 -17 0 -13 -17 12 0 18 -17 -16 -20 0 17 -17 -16 -16 0 -14 -18 19 0 -23 -17 34 -34 0 -23 -18 24 -34 0 -23 -8 34 -35 0 -23 36 0 -23 37 0 -23 38 0 -23 -24 24 -24 0 -22 -24 18 -18 0 18 -24 -20 -26 0 17 -24 -20 -20 0 -27 -30 39 0 19 -39 -15 -40 0 12 -39 -15 -25 0 30 -24 -20 -40 0 30 -17 -16 -25 0 30 -18 -16 -40 0 30 -8 -25 -25 0 -28 -24 41 -41 0 -28 -17 8 -8 0 -28 -18 41 -8 0 -28 -8 8 -29 0 -28 42 0 -28 43 0 -28 44 0 -28 -29 29 -29 0 -23 -29 35 -35 0 -22 -29 30 -30 0 30 -29 -25 -45 0 18 -29 -25 -40 0 17 -29 -25 -25 0 -31 30 -29 -30 0 -31 18 -41 -30 0 -31 17 -8 -30 0 -31 -29 30 -30 0 -31 -8 17 -30 0 -31 46 0 -31 47 0 -31 48 0 -32 30 -35 -18 0 -32 18 -24 -18 0 -32 17 -34 -18 0 -32 -24 18 -18 0 -32 49 0 -32 50 0 -32 51 0 -33 30 -30 -17 0 -33 18 -18 -17 0 -33 17 -17 -17 0 -33 -17 17 -17 0 -33 -18 18 -17 0 -33 52 0 -33 53 0 -33 54 0 -32 -34 17 -18 0 -28 -34 8 -41 0 -23 -34 34 -24 0 -22 -34 17 -18 0 30 -34 -20 -25 0 18 -34 -20 -20 0 17 -34 -20 -16 0 34 -34 -26 -16 0 34 -29 -40 -25 0 34 -24 -26 -20 0 34 -17 -20 -16 0 34 -18 -20 -20 0 34 -8 -40 -16 0 35 -34 -26 -25 0 35 -29 -40 -45 0 35 -24 -26 -40 0 35 -17 -20 -25 0 35 -18 -20 -40 0 35 -8 -40 -25 0 -36 35 -29 -35 0 -36 34 -8 -35 0 -36 -29 35 -35 0 -36 -8 34 -35 0 -36 55 0 -36 56 0 -36 57 0 -37 35 -35 -24 0 -37 34 -34 -24 0 -37 -34 34 -24 0 -37 -24 24 -24 0 -37 58 0 -37 59 0 -37 60 0 -38 35 -30 -34 0 -38 34 -17 -34 0 -38 -17 34 -34 0 -38 -18 24 -34 0 -38 61 0 -38 62 0 -38 63 0 -38 24 -18 -34 0 -37 24 -24 -24 0 -36 24 -41 -35 0 -1 24 0 24 -34 -26 -20 0 24 -29 -40 -40 0 24 -24 -26 -26 0 24 -17 -20 -20 0 24 -18 -20 -26 0 24 -8 -40 -20 0 45 0 -36 -41 24 -35 0 -31 -41 18 -30 0 -28 -41 41 -29 0 -23 -41 24 -35 0 -22 -41 18 -30 0 24 -41 -40 -26 0 35 -41 -40 -40 0 34 -41 -40 -20 0 30 -41 -25 -40 0 18 -41 -25 -26 0 17 -41 -25 -20 0 41 -41 -45 -26 0 41 -34 -40 -20 0 41 -29 -45 -40 0 41 -24 -40 -26 0 41 -17 -25 -20 0 41 -18 -25 -26 0 41 -8 -45 -20 0 8 -41 -45 -20 0 8 -34 -40 -16 0 8 -29 -45 -25 0 8 -24 -40 -20 0 8 -17 -25 -16 0 8 -18 -25 -20 0 8 -8 -45 -16 0 -1 29 0 29 -41 -45 -40 0 29 -34 -40 -25 0 29 -29 -45 -45 0 29 -24 -40 -40 0 29 -17 -25 -25 0 29 -18 -25 -40 0 29 -8 -45 -25 0 -42 29 -29 -29 0 -42 8 -8 -29 0 -42 41 -41 -29 0 -42 -41 41 -29 0 -42 -29 29 -29 0 -42 -8 8 -29 0 -42 64 0 -42 65 0 -42 66 0 -43 29 -35 -41 0 -43 8 -34 -41 0 -43 41 -24 -41 0 -43 -34 8 -41 0 -43 -24 41 -41 0 -43 67 0 -43 68 0 -43 69 0 -44 29 -30 -8 0 -44 8 -17 -8 0 -44 41 -18 -8 0 -44 -17 8 -8 0 -44 -18 41 -8 0 -44 70 0 -44 71 0 -44 72 0 -43 -35 29 -41 0 -37 -35 35 -24 0 -32 -35 30 -18 0 -28 -35 29 -41 0 -23 -35 35 -24 0 -22 -35 30 -18 0 29 -35 -40 -45 0 8 -35 -40 -25 0 41 -35 -40 -40 0 24 -35 -26 -40 0 35 -35 -26 -45 0 34 -35 -26 -25 0 30 -35 -20 -45 0 18 -35 -20 -40 0 17 -35 -20 -25 0 -44 -30 29 -8 0 -38 -30 35 -34 0 -33 -30 30 -17 0 -28 -30 29 -8 0 -23 -30 35 -34 0 -22 -30 30 -17 0 -13 -30 39 0 29 -30 -25 -45 0 8 -30 -25 -25 0 41 -30 -25 -40 0 24 -30 -20 -40 0 35 -30 -20 -45 0 34 -30 -20 -25 0 30 -30 -16 -45 0 18 -30 -16 -40 0 17 -30 -16 -25 0 -46 73 30 0 -73 -30 -29 0 -47 74 18 0 -74 -30 -41 0 -48 75 17 0 -75 -30 -8 0 -49 76 30 0 -76 -18 -35 0 -50 77 18 0 -77 -18 -24 0 -51 78 17 0 -78 -18 -34 0 -52 79 30 0 -79 -17 -30 0 -53 80 18 0 -80 -17 -18 0 -54 81 17 0 -81 -17 -17 0 -55 82 35 0 -82 -35 -29 0 -56 83 24 0 -83 -35 -41 0 -57 84 34 0 -84 -35 -8 0 -58 85 35 0 -85 -24 -35 0 -59 86 24 0 -86 -24 -24 0 -60 87 34 0 -87 -24 -34 0 -61 88 35 0 -88 -34 -30 0 -62 89 24 0 -89 -34 -18 0 -63 90 34 0 -90 -34 -17 0 -64 91 29 0 -91 -29 -29 0 -65 92 41 0 -92 -29 -41 0 -66 93 8 0 -93 -29 -8 0 -67 94 29 0 -94 -41 -35 0 -68 95 41 0 -95 -41 -24 0 -69 96 8 0 -96 -41 -34 0 -70 97 29 0 -97 -8 -30 0 -71 98 41 0 -98 -8 -18 0 -72 99 8 0 -99 -8 -17 0 -5 100 0 -100 101 102 0 -102 -41 -103 0 -102 -29 -104 0 -102 -8 -105 0 -102 106 0 -102 107 0 -102 108 0 -101 -41 103 0 -101 -29 104 0 -101 -8 105 0 -101 109 0 -101 110 0 -101 111 0 -101 103 -41 0 103 -39 -112 -40 0 103 -19 -112 -26 0 103 -12 -112 -20 0 -101 104 -29 0 104 -39 -112 -45 0 104 -19 -112 -40 0 104 -12 -112 -25 0 -101 105 -8 0 105 -39 -112 -25 0 105 -19 -112 -20 0 105 -12 -112 -16 0 -106 -29 -104 0 -107 -41 -103 0 -108 -8 -105 0 -102 -103 -41 0 105 -103 -113 -20 0 104 -103 -113 -40 0 103 -103 -113 -26 0 19 -103 -112 -26 0 12 -103 -112 -20 0 -102 -104 -29 0 105 -104 -113 -25 0 104 -104 -113 -45 0 103 -104 -113 -40 0 19 -104 -112 -40 0 12 -104 -112 -25 0 -102 -105 -8 0 105 -105 -113 -16 0 104 -105 -113 -25 0 103 -105 -113 -20 0 19 -105 -112 -20 0 12 -105 -112 -16 0 -109 -29 104 0 -110 -41 103 0 -111 -8 105 0 -5 100 0 -5 100 0 113 0 Atoms: Atom 1: (! (\x0:$i.(rel_s4 x0 x0))) Atom 2: (! (\x0:$i.(! (\x1:$i.(! (\x2:$i.(((~ (rel_s4 x0 x1)) | (~ (rel_s4 x1 x2))) | (rel_s4 x0 x2)))))))) Atom 3: (! (\x0:$i.((~ (! (\x1:mu.((! (\x2:$i.((~ (rel_s4 x0 x2)) | (f x x2)))) | (! (\x2:$i.((~ (rel_s4 x0 x2)) | (~ (f x x2))))))))) | (! (\x1:$i.((~ (rel_s4 x0 x1)) | (~ ((~ ((~ (! (\x2:$i.((~ (rel_s4 x1 x2)) | (f a x2))))) | (f a x1))) | (~ ((~ (f a x1)) | (! (\x2:$i.((~ (rel_s4 x1 x2)) | (f a x2)))))))))))))) Atom 4: ((~ (! (\x0:mu.((! (\x1:$i.((~ (rel_s4 __1 x1)) | (f x x1)))) | (! (\x1:$i.((~ (rel_s4 __1 x1)) | (~ (f x x1))))))))) | (! (\x0:$i.((~ (rel_s4 __1 x0)) | (~ ((~ ((~ (! (\x1:$i.((~ (rel_s4 x0 x1)) | (f a x1))))) | (f a x0))) | (~ ((~ (f a x0)) | (! (\x1:$i.((~ (rel_s4 x0 x1)) | (f a x1)))))))))))) Atom 5: (! (\x0:mu.((! (\x1:$i.((~ (rel_s4 __1 x1)) | (f x x1)))) | (! (\x1:$i.((~ (rel_s4 __1 x1)) | (~ (f x x1)))))))) Atom 6: (! (\x0:$i.((~ (rel_s4 __1 x0)) | (~ ((~ ((~ (! (\x1:$i.((~ (rel_s4 x0 x1)) | (f a x1))))) | (f a x0))) | (~ ((~ (f a x0)) | (! (\x1:$i.((~ (rel_s4 x0 x1)) | (f a x1))))))))))) Atom 7: ((~ (rel_s4 __1 __2)) | (~ ((~ ((~ (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0))))) | (f a __2))) | (~ ((~ (f a __2)) | (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0))))))))) Atom 8: (rel_s4 __1 __2) Atom 9: ((~ ((~ (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0))))) | (f a __2))) | (~ ((~ (f a __2)) | (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0))))))) Atom 10: ((~ (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0))))) | (f a __2)) Atom 11: ((~ (f a __2)) | (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0))))) Atom 12: (f a __2) Atom 13: (! (\x0:$i.((~ (rel_s4 __2 x0)) | (f a x0)))) Atom 14: ((~ (rel_s4 __2 __3)) | (f a __3)) Atom 15: (a = a) Atom 16: (__2 = __2) Atom 17: (rel_s4 __2 __2) Atom 18: (rel_s4 __2 __3) Atom 19: (f a __3) Atom 20: (__2 = __3) Atom 21: ((~ (rel_s4 __2 __2)) | (f a __2)) Atom 22: (! (\x0:$i.(! (\x1:$i.(((~ (rel_s4 __2 x0)) | (~ (rel_s4 x0 x1))) | (rel_s4 __2 x1)))))) Atom 23: (! (\x0:$i.(! (\x1:$i.(((~ (rel_s4 __3 x0)) | (~ (rel_s4 x0 x1))) | (rel_s4 __3 x1)))))) Atom 24: (rel_s4 __3 __3) Atom 25: (__1 = __2) Atom 26: (__3 = __3) Atom 27: ((~ (rel_s4 __2 __1)) | (f a __1)) Atom 28: (! (\x0:$i.(! (\x1:$i.(((~ (rel_s4 __1 x0)) | (~ (rel_s4 x0 x1))) | (rel_s4 __1 x1)))))) Atom 29: (rel_s4 __1 __1) Atom 30: (rel_s4 __2 __1) Atom 31: (! (\x0:$i.(((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 x0))) | (rel_s4 __2 x0)))) Atom 32: (! (\x0:$i.(((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 x0))) | (rel_s4 __2 x0)))) Atom 33: (! (\x0:$i.(((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 x0))) | (rel_s4 __2 x0)))) Atom 34: (rel_s4 __3 __2) Atom 35: (rel_s4 __3 __1) Atom 36: (! (\x0:$i.(((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 x0))) | (rel_s4 __3 x0)))) Atom 37: (! (\x0:$i.(((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 x0))) | (rel_s4 __3 x0)))) Atom 38: (! (\x0:$i.(((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 x0))) | (rel_s4 __3 x0)))) Atom 39: (f a __1) Atom 40: (__1 = __3) Atom 41: (rel_s4 __1 __3) Atom 42: (! (\x0:$i.(((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 x0))) | (rel_s4 __1 x0)))) Atom 43: (! (\x0:$i.(((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 x0))) | (rel_s4 __1 x0)))) Atom 44: (! (\x0:$i.(((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 x0))) | (rel_s4 __1 x0)))) Atom 45: (__1 = __1) Atom 46: (((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __1))) | (rel_s4 __2 __1)) Atom 47: (((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __3))) | (rel_s4 __2 __3)) Atom 48: (((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __2))) | (rel_s4 __2 __2)) Atom 49: (((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 __1))) | (rel_s4 __2 __1)) Atom 50: (((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 __3))) | (rel_s4 __2 __3)) Atom 51: (((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 __2))) | (rel_s4 __2 __2)) Atom 52: (((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __1))) | (rel_s4 __2 __1)) Atom 53: (((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __3))) | (rel_s4 __2 __3)) Atom 54: (((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __2))) | (rel_s4 __2 __2)) Atom 55: (((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 __1))) | (rel_s4 __3 __1)) Atom 56: (((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 __3))) | (rel_s4 __3 __3)) Atom 57: (((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 __2))) | (rel_s4 __3 __2)) Atom 58: (((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 __1))) | (rel_s4 __3 __1)) Atom 59: (((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 __3))) | (rel_s4 __3 __3)) Atom 60: (((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 __2))) | (rel_s4 __3 __2)) Atom 61: (((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 __1))) | (rel_s4 __3 __1)) Atom 62: (((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 __3))) | (rel_s4 __3 __3)) Atom 63: (((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 __2))) | (rel_s4 __3 __2)) Atom 64: (((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __1))) | (rel_s4 __1 __1)) Atom 65: (((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __3))) | (rel_s4 __1 __3)) Atom 66: (((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __2))) | (rel_s4 __1 __2)) Atom 67: (((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 __1))) | (rel_s4 __1 __1)) Atom 68: (((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 __3))) | (rel_s4 __1 __3)) Atom 69: (((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 __2))) | (rel_s4 __1 __2)) Atom 70: (((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __1))) | (rel_s4 __1 __1)) Atom 71: (((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __3))) | (rel_s4 __1 __3)) Atom 72: (((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __2))) | (rel_s4 __1 __2)) Atom 73: ((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __1))) Atom 74: ((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __3))) Atom 75: ((~ (rel_s4 __2 __1)) | (~ (rel_s4 __1 __2))) Atom 76: ((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 __1))) Atom 77: ((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 __3))) Atom 78: ((~ (rel_s4 __2 __3)) | (~ (rel_s4 __3 __2))) Atom 79: ((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __1))) Atom 80: ((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __3))) Atom 81: ((~ (rel_s4 __2 __2)) | (~ (rel_s4 __2 __2))) Atom 82: ((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 __1))) Atom 83: ((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 __3))) Atom 84: ((~ (rel_s4 __3 __1)) | (~ (rel_s4 __1 __2))) Atom 85: ((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 __1))) Atom 86: ((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 __3))) Atom 87: ((~ (rel_s4 __3 __3)) | (~ (rel_s4 __3 __2))) Atom 88: ((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 __1))) Atom 89: ((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 __3))) Atom 90: ((~ (rel_s4 __3 __2)) | (~ (rel_s4 __2 __2))) Atom 91: ((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __1))) Atom 92: ((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __3))) Atom 93: ((~ (rel_s4 __1 __1)) | (~ (rel_s4 __1 __2))) Atom 94: ((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 __1))) Atom 95: ((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 __3))) Atom 96: ((~ (rel_s4 __1 __3)) | (~ (rel_s4 __3 __2))) Atom 97: ((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __1))) Atom 98: ((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __3))) Atom 99: ((~ (rel_s4 __1 __2)) | (~ (rel_s4 __2 __2))) Atom 100: ((! (\x0:$i.((~ (rel_s4 __1 x0)) | (f x x0)))) | (! (\x0:$i.((~ (rel_s4 __1 x0)) | (~ (f x x0)))))) Atom 101: (! (\x0:$i.((~ (rel_s4 __1 x0)) | (f x x0)))) Atom 102: (! (\x0:$i.((~ (rel_s4 __1 x0)) | (~ (f x x0))))) Atom 103: (f x __3) Atom 104: (f x __1) Atom 105: (f x __2) Atom 106: ((~ (rel_s4 __1 __1)) | (~ (f x __1))) Atom 107: ((~ (rel_s4 __1 __3)) | (~ (f x __3))) Atom 108: ((~ (rel_s4 __1 __2)) | (~ (f x __2))) Atom 109: ((~ (rel_s4 __1 __1)) | (f x __1)) Atom 110: ((~ (rel_s4 __1 __3)) | (f x __3)) Atom 111: ((~ (rel_s4 __1 __2)) | (f x __2)) Atom 112: (a = x) Atom 113: (x = x) % SZS output end FiniteModel