% SZS start RequiredInformation % Congratulations - you have become a registered power user of SystemOnTPTP, at IP address 89.186.28.63. % Please consider donating to the TPTP project - see www.tptp.org for details. % When you donate this message will disappear. % If you do not donate a random delay might be added to your processing time. % SZS end RequiredInformation % START OF SYSTEM OUTPUT % SZS status Satisfiable ============================== Mace4 ================================= Mace4 (64) version 2009-11A, November 2009. Process 25569 was started by tptp on quoll.cs.miami.edu, Wed May 18 05:16:17 2016 The command was "/home/tptp/Systems/Mace4---1109a/mace4 -t 60 -f /tmp/Mace4_input_25548_quoll.cs.miami.edu". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file /tmp/Mace4_input_25548_quoll.cs.miami.edu op(500,infix,"==>"). set(prolog_style_variables). set(print_models_tabular). % set(print_models_tabular) -> clear(print_models). formulas(sos). (all X exists T (nontime(X) -> present(X,T))) # label(axiom1) # label(axiom). (all X all T (phtxt(X,T) -> (all T1 (present(X,T1) -> phtxt(X,T1))))) # label(axiom2) # label(axiom). (all X all T (txt(X,T) -> (all T1 (present(X,T1) -> txt(X,T1))))) # label(axiom3) # label(axiom). (all X all Y all T (pt(X,Y,T) <-> ppt(X,Y,T) | X = Y & present(X,T) & present(Y,T))) # label(definition4) # label(axiom). (all X all Y all T (overlap(X,Y,T) <-> (exists Z (pt(Z,X,T) & pt(Z,Y,T))))) # label(definition5) # label(axiom). (all X all Y all Z all T (sumpt(X,Y,Z,T) <-> pt(Y,X,T) & pt(Z,X,T) & (all V (pt(V,X,T) -> overlap(V,Y,T) | overlap(V,Z,T))))) # label(definition6) # label(axiom). (all X all Y all T (ppt(X,Y,T) -> present(X,T) & present(Y,T))) # label(axiom7) # label(axiom). (all X all T -ppt(X,X,T)) # label(axiom8) # label(axiom). (all X all Y all T all Z (ppt(X,Y,T) & ppt(Y,Z,T) -> ppt(X,Z,T))) # label(axiom9) # label(axiom). (all X all Y all T (ppt(X,Y,T) -> (exists Z (ppt(Z,Y,T) & -overlap(X,Z,T))))) # label(axiom10) # label(axiom). (all X all T all Y (present(X,T) & present(Y,T) -> (exists Z sumpt(Z,X,Y,T)))) # label(axiom11) # label(axiom). (all S all T (reg(S) & time(T) -> occ(S,S,T))) # label(axiom12) # label(axiom). (all S all R all T (occ(S,R,T) -> present(S,T) & present(R,T))) # label(axiom13) # label(axiom). (all R1 all R2 all T (ppt(R1,R2,T) & reg(R2) & time(T) -> occ(R1,R1,T))) # label(axiom14) # label(axiom). (all X all Y all T all R1 (ppt(X,Y,T) & occ(Y,R1,T) -> (exists R2 (ppt(R2,R1,T) & occ(X,R2,T))))) # label(axiom15) # label(axiom). (all X all T (phtxt(X,T) -> (exists T1 (time(T1) & -present(X,T1))))) # label(axiom16) # label(axiom). (all X all Y all T (phppt(X,Y,T) <-> ppt(X,Y,T) & phtxt(X,T) & phtxt(Y,T))) # label(definition17) # label(axiom). (all X all Y all T (phpt(X,Y,T) <-> pt(X,Y,T) & phtxt(X,T) & phtxt(Y,T))) # label(definition18) # label(axiom). (all X all Y all T (phoverlap(X,Y,T) <-> (exists Z (phpt(Z,X,T) & phpt(Z,Y,T))))) # label(definition19) # label(axiom). (all X all Y all Z all T (phsumpt(X,Y,Z,T) <-> phpt(Y,X,T) & phpt(Z,X,T) & (all V (phpt(V,X,T) -> phoverlap(V,Y,T) | phoverlap(V,Z,T))))) # label(definition20) # label(axiom). (all X all T (compphtxt(X,T) <-> phtxt(X,T) & -(exists Y phppt(X,Y,T)))) # label(definition21) # label(axiom). (all X all Y all T (phppt(X,Y,T) -> -(exists T1 phppt(Y,X,T1)))) # label(axiom22) # label(axiom). (all X all T all Y (phtxt(X,T) & phtxt(Y,T) -> (-phpt(X,Y,T) -> (exists Z (phpt(Z,X,T) & -phoverlap(Z,Y,T)))))) # label(axiom23) # label(axiom). (all X all T (phtxt(X,T) -> (exists Z (-phtxt(Z,T) & pt(Z,X,T))))) # label(axiom24) # label(axiom). (all X all Y all T (phppt(X,Y,T) -> (exists Z (phppt(X,Z,T) & -(exists V (phppt(X,V,T) & phppt(V,Z,T))))))) # label(axiom25) # label(axiom). (all X all Y all T (phppt(X,Y,T) -> (exists Z (phppt(Z,Y,T) & -(exists V (phppt(Z,V,T) & phppt(V,Y,T))))))) # label(axiom26) # label(axiom). (all X all T all Y (phtxt(X,T) -> ((all Y phpt(Y,X,T)) -> (exists Z (phpt(Z,Y,T) & (all V -phppt(V,Z,T))))))) # label(axiom27) # label(axiom). (all X all T (phtxt(X,T) -> (exists R occ(X,R,T)))) # label(axiom28) # label(axiom). (all X all R all T all Y (occ(X,R,T) & occ(Y,R,T) -> (phtxt(X,T) & phtxt(Y,T) -> X = Y))) # label(axiom29) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> phtxt(X,T) & phtxt(Y,T))) # label(axiom30) # label(axiom). (all X all T -phtxtprec(X,X,T)) # label(axiom31) # label(axiom). (all X all Y all T all Z (phtxtprec(X,Y,T) & phtxtprec(Y,Z,T) -> phtxtprec(X,Z,T))) # label(axiom32) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> (exists Z (phtxtprec(X,Z,T) & -(exists V (phtxtprec(X,V,T) & phtxtprec(V,Z,T))))))) # label(axiom33) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> (exists Z (phtxtprec(Z,Y,T) & -(exists V (phtxtprec(Z,V,T) & phtxtprec(V,Y,T))))))) # label(axiom34) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> -(exists T1 (phpt(X,Y,T1) | phpt(Y,X,T1))))) # label(axiom35) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> (all Z (phpt(Z,X,T) -> phtxtprec(Z,Y,T))))) # label(axiom36) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> (all Z (phpt(Z,Y,T) -> phtxtprec(X,Z,T))))) # label(axiom37) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> (exists Z (compphtxt(Z,T) & phpt(X,Z,T) & phpt(Y,Z,T))))) # label(axiom38a) # label(axiom). (all X all Y all T all Z2 (phtxtprec(X,Y,T) -> (all Z1 all Z1 (compphtxt(Z1,T) & phpt(X,Z1,T) & phpt(Y,Z1,T) & compphtxt(Z2,T) & phpt(X,Z2,T) & phpt(Y,Z2,T) -> Z1 = Z2)))) # label(axiom38b) # label(axiom). (all X all T (phtxt(X,T) -> (exists Y (phpt(Y,X,T) & (all Z (phpt(Z,X,T) -> -phtxtprec(Z,Y,T))))))) # label(axiom39) # label(axiom). (all X all T (phtxt(X,T) -> (exists Y (phpt(Y,X,T) & (all Z (phpt(Z,X,T) -> -phtxtprec(Y,Z,T))))))) # label(axiom40) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) & -(exists Z (phtxtprec(X,Z,T) & phtxtprec(Z,Y,T))) -> (exists Z phsumpt(Z,X,Y,T)))) # label(axiom41) # label(axiom). (all X all Y all T all R1 all R2 (phtxtprec(X,Y,T) -> (occ(X,R1,T) & occ(Y,R2,T) -> -overlap(R1,R2,T)))) # label(axiom42) # label(axiom). (all X all Y all T (phrep(X,Y,T) -> phtxt(X,T))) # label(axiom45) # label(axiom). (all X all T all X ((exists Y phrep(X,Y,T)) -> (all T1 (present(X,T1) -> (exists Y phrep(X,Y,T1)))))) # label(axiom46) # label(axiom). (all X all T all Y all T1 (phtxtequiv(X,T,Y,T1) -> phtxt(X,T) & phtxt(Y,T1))) # label(axiom47) # label(axiom). (all X all T all Y all T1 (phtxtequiv(X,T,Y,T1) -> present(X,T) & present(Y,T1))) # label(axiom48) # label(axiom). (all X all T (phtxt(X,T) -> phtxtequiv(X,T,X,T))) # label(axiom49) # label(axiom). (all X all T all Y all T1 (phtxtequiv(X,T,Y,T1) -> phtxtequiv(Y,T1,X,T))) # label(axiom50) # label(axiom). (all X all T1 all Y all T2 all Z all T3 (phtxtequiv(X,T1,Y,T2) & phtxtequiv(Y,T2,Z,T3) -> phtxtequiv(X,T1,Z,T3))) # label(axiom51) # label(axiom). (all X all Y all T (ppt(X,Y,T) -> -phtxtequiv(X,T,Y,T))) # label(axiom52) # label(axiom). (all X1 all T all X2 all Y1 (phtxtequiv(X1,T,X2,T) & phppt(Y1,X1,T) -> (exists Y2 (phtxtequiv(Y1,T,Y2,T) & ppt(Y2,X2,T))))) # label(axiom53) # label(axiom). (all X1 all T all X2 all Y1 (phtxtequiv(X1,T,X2,T) & phppt(X1,Y1,T) -> (exists Y2 (phtxtequiv(Y1,T,Y2,T) & ppt(X2,Y2,T))))) # label(axiom54) # label(axiom). (all X1 all T1 all X2 all T2 all Y (phtxtequiv(X1,T1,X2,T2) -> (phrep(X1,Y,T1) <-> phrep(X2,Y,T2)))) # label(axiom55) # label(axiom). (all X all Y (txtdep(X,Y) -> (exists T txt(X,T)) & (exists T phtxt(Y,T)))) # label(axiom56) # label(axiom). (all X all T (phtxt(X,T) -> (exists Y (txt(Y,T) & txtdep(Y,X))))) # label(axiom57a) # label(axiom). (all X all T (phtxt(X,T) -> (all Y1 all Y2 (txt(Y1,T) & txtdep(Y1,X) & txt(Y2,T) & txtdep(Y2,X) -> Y1 = Y2)))) # label(axiom57b) # label(axiom). (all X all T (txt(X,T) -> (exists Y (phtxt(Y,T) & txtdep(X,Y))))) # label(axiom58) # label(axiom). (all X all Y1 all Y2 (txtdep(X,Y1) & txtdep(X,Y2) -> (all T1 all T2 (present(Y1,T1) & present(Y2,T2) -> phtxtequiv(Y1,T1,Y2,T2))))) # label(axiom59) # label(axiom). (all X all Y (txtdep(X,Y) -> (all T (present(X,T) -> (exists Z exists T1 phtxtequiv(Z,T,Y,T1)))))) # label(axiom60) # label(axiom). (all X all Y (txtdep(X,Y) -> (all T (present(Y,T) -> present(X,T))))) # label(axiom61) # label(axiom). (all Y1 all T1 all Y2 all T2 (phtxtequiv(Y1,T1,Y2,T2) -> (all Z (txtdep(Z,Y1) <-> txtdep(Z,Y2))))) # label(axiom62) # label(axiom). (all X1 all Y1 all X2 all Y2 all T (txtdep(X1,Y1) & txtdep(X2,Y2) -> (ppt(X1,X2,T) <-> ppt(Y1,Y2,T)))) # label(axiom63) # label(axiom). (all X1 all Y1 all X2 all Y2 all T (txtdep(X1,Y1) & txtdep(X2,Y2) -> (phtxtprec(X1,X2,T) <-> phtxtprec(Y1,Y2,T)))) # label(axiom64) # label(axiom). (all X all T all Z (txt(X,T) & ppt(Z,X,T) -> txt(Z,T))) # label(axiom65) # label(axiom). (all T -(exists X (phtxt(X,T) & txt(X,T)))) # label(axiom66) # label(axiom). (all X all Y all T (txtppt(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & ppt(X1,Y1,T))))) # label(axiom68) # label(axiom). (all X all Y all T (txtpt(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & pt(X1,Y1,T))))) # label(axiomLXX) # label(axiom). (all X all Y all T (txtoverlap(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & phoverlap(X1,Y1,T))))) # label(axiomLXXI) # label(axiom). (all X all Y all T (txtprec(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & phtxtprec(X1,Y1,T))))) # label(axiomLXXII) # label(axiom). (all X all Y all T (txtrep(X,Y,T) <-> (exists X1 (txtdep(X,X1) & phrep(X1,Y,T))))) # label(axiomLXXIII) # label(axiom). (all X all Y all Z all T (txtsumpt(X,Y,Z,T) <-> (exists X1 exists Y1 exists Z1 (txtdep(X,X1) & txtdep(Y,Y1) & txtdep(Z,Z1) & phsumpt(X1,Y1,Z1,T))))) # label(axiomLXXIV) # label(axiom). (all X all T (comptxt(X,T) <-> (exists X1 (txtdep(X,X1) & compphtxt(X1,T))))) # label(axiomLXXV) # label(axiom). (all X all T (phtxt(X,T) -> obj(X) & time(T))) # label(axiomC) # label(axiom). (all X all T (txt(X,T) -> obj(X) & time(T))) # label(axiomCI) # label(axiom). (all X all Y (txtdep(X,Y) -> obj(X) & obj(Y))) # label(axiomCII) # label(axiom). (all X all T (present(X,T) -> nontime(X) & time(T))) # label(axiomCIII) # label(axiom). (all S all R all T (occ(S,R,T) -> nontime(S) & reg(R) & time(T))) # label(axiomCIV) # label(axiom). (all X all Y all T (ppt(X,Y,T) -> nontime(X) & nontime(Y) & time(T))) # label(axiomCV) # label(axiom). (all X all Y all T (phtxtprec(X,Y,T) -> obj(X) & obj(Y) & time(T))) # label(axiomCVI) # label(axiom). (all X all T1 all Y all T2 (phtxtequiv(X,T1,Y,T2) -> obj(X) & obj(Y) & time(T1) & time(T2))) # label(axiomCVII) # label(axiom). (all X all Y all T (phrep(X,Y,T) -> obj(X) & obj(Y) & time(T))) # label(axiomCVIII) # label(axiom). (all X (obj(X) | reg(X) -> nontime(X))) # label(axiomCIX) # label(axiom). (all T (time(T) -> -nontime(T))) # label(axiomCX) # label(axiom). (all X (obj(X) -> -reg(X))) # label(axiomCXI) # label(axiom). end_of_list. % From the command line: assign(max_seconds, 60). ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all X exists T (nontime(X) -> present(X,T))) # label(axiom1) # label(axiom) # label(non_clause). [assumption]. 2 (all X all T (phtxt(X,T) -> (all T1 (present(X,T1) -> phtxt(X,T1))))) # label(axiom2) # label(axiom) # label(non_clause). [assumption]. 3 (all X all T (txt(X,T) -> (all T1 (present(X,T1) -> txt(X,T1))))) # label(axiom3) # label(axiom) # label(non_clause). [assumption]. 4 (all X all Y all T (pt(X,Y,T) <-> ppt(X,Y,T) | X = Y & present(X,T) & present(Y,T))) # label(definition4) # label(axiom) # label(non_clause). [assumption]. 5 (all X all Y all T (overlap(X,Y,T) <-> (exists Z (pt(Z,X,T) & pt(Z,Y,T))))) # label(definition5) # label(axiom) # label(non_clause). [assumption]. 6 (all X all Y all Z all T (sumpt(X,Y,Z,T) <-> pt(Y,X,T) & pt(Z,X,T) & (all V (pt(V,X,T) -> overlap(V,Y,T) | overlap(V,Z,T))))) # label(definition6) # label(axiom) # label(non_clause). [assumption]. 7 (all X all Y all T (ppt(X,Y,T) -> present(X,T) & present(Y,T))) # label(axiom7) # label(axiom) # label(non_clause). [assumption]. 8 (all X all T -ppt(X,X,T)) # label(axiom8) # label(axiom) # label(non_clause). [assumption]. 9 (all X all Y all T all Z (ppt(X,Y,T) & ppt(Y,Z,T) -> ppt(X,Z,T))) # label(axiom9) # label(axiom) # label(non_clause). [assumption]. 10 (all X all Y all T (ppt(X,Y,T) -> (exists Z (ppt(Z,Y,T) & -overlap(X,Z,T))))) # label(axiom10) # label(axiom) # label(non_clause). [assumption]. 11 (all X all T all Y (present(X,T) & present(Y,T) -> (exists Z sumpt(Z,X,Y,T)))) # label(axiom11) # label(axiom) # label(non_clause). [assumption]. 12 (all S all T (reg(S) & time(T) -> occ(S,S,T))) # label(axiom12) # label(axiom) # label(non_clause). [assumption]. 13 (all S all R all T (occ(S,R,T) -> present(S,T) & present(R,T))) # label(axiom13) # label(axiom) # label(non_clause). [assumption]. 14 (all R1 all R2 all T (ppt(R1,R2,T) & reg(R2) & time(T) -> occ(R1,R1,T))) # label(axiom14) # label(axiom) # label(non_clause). [assumption]. 15 (all X all Y all T all R1 (ppt(X,Y,T) & occ(Y,R1,T) -> (exists R2 (ppt(R2,R1,T) & occ(X,R2,T))))) # label(axiom15) # label(axiom) # label(non_clause). [assumption]. 16 (all X all T (phtxt(X,T) -> (exists T1 (time(T1) & -present(X,T1))))) # label(axiom16) # label(axiom) # label(non_clause). [assumption]. 17 (all X all Y all T (phppt(X,Y,T) <-> ppt(X,Y,T) & phtxt(X,T) & phtxt(Y,T))) # label(definition17) # label(axiom) # label(non_clause). [assumption]. 18 (all X all Y all T (phpt(X,Y,T) <-> pt(X,Y,T) & phtxt(X,T) & phtxt(Y,T))) # label(definition18) # label(axiom) # label(non_clause). [assumption]. 19 (all X all Y all T (phoverlap(X,Y,T) <-> (exists Z (phpt(Z,X,T) & phpt(Z,Y,T))))) # label(definition19) # label(axiom) # label(non_clause). [assumption]. 20 (all X all Y all Z all T (phsumpt(X,Y,Z,T) <-> phpt(Y,X,T) & phpt(Z,X,T) & (all V (phpt(V,X,T) -> phoverlap(V,Y,T) | phoverlap(V,Z,T))))) # label(definition20) # label(axiom) # label(non_clause). [assumption]. 21 (all X all T (compphtxt(X,T) <-> phtxt(X,T) & -(exists Y phppt(X,Y,T)))) # label(definition21) # label(axiom) # label(non_clause). [assumption]. 22 (all X all Y all T (phppt(X,Y,T) -> -(exists T1 phppt(Y,X,T1)))) # label(axiom22) # label(axiom) # label(non_clause). [assumption]. 23 (all X all T all Y (phtxt(X,T) & phtxt(Y,T) -> (-phpt(X,Y,T) -> (exists Z (phpt(Z,X,T) & -phoverlap(Z,Y,T)))))) # label(axiom23) # label(axiom) # label(non_clause). [assumption]. 24 (all X all T (phtxt(X,T) -> (exists Z (-phtxt(Z,T) & pt(Z,X,T))))) # label(axiom24) # label(axiom) # label(non_clause). [assumption]. 25 (all X all Y all T (phppt(X,Y,T) -> (exists Z (phppt(X,Z,T) & -(exists V (phppt(X,V,T) & phppt(V,Z,T))))))) # label(axiom25) # label(axiom) # label(non_clause). [assumption]. 26 (all X all Y all T (phppt(X,Y,T) -> (exists Z (phppt(Z,Y,T) & -(exists V (phppt(Z,V,T) & phppt(V,Y,T))))))) # label(axiom26) # label(axiom) # label(non_clause). [assumption]. 27 (all X all T all Y (phtxt(X,T) -> ((all Y phpt(Y,X,T)) -> (exists Z (phpt(Z,Y,T) & (all V -phppt(V,Z,T))))))) # label(axiom27) # label(axiom) # label(non_clause). [assumption]. 28 (all X all T (phtxt(X,T) -> (exists R occ(X,R,T)))) # label(axiom28) # label(axiom) # label(non_clause). [assumption]. 29 (all X all R all T all Y (occ(X,R,T) & occ(Y,R,T) -> (phtxt(X,T) & phtxt(Y,T) -> X = Y))) # label(axiom29) # label(axiom) # label(non_clause). [assumption]. 30 (all X all Y all T (phtxtprec(X,Y,T) -> phtxt(X,T) & phtxt(Y,T))) # label(axiom30) # label(axiom) # label(non_clause). [assumption]. 31 (all X all T -phtxtprec(X,X,T)) # label(axiom31) # label(axiom) # label(non_clause). [assumption]. 32 (all X all Y all T all Z (phtxtprec(X,Y,T) & phtxtprec(Y,Z,T) -> phtxtprec(X,Z,T))) # label(axiom32) # label(axiom) # label(non_clause). [assumption]. 33 (all X all Y all T (phtxtprec(X,Y,T) -> (exists Z (phtxtprec(X,Z,T) & -(exists V (phtxtprec(X,V,T) & phtxtprec(V,Z,T))))))) # label(axiom33) # label(axiom) # label(non_clause). [assumption]. 34 (all X all Y all T (phtxtprec(X,Y,T) -> (exists Z (phtxtprec(Z,Y,T) & -(exists V (phtxtprec(Z,V,T) & phtxtprec(V,Y,T))))))) # label(axiom34) # label(axiom) # label(non_clause). [assumption]. 35 (all X all Y all T (phtxtprec(X,Y,T) -> -(exists T1 (phpt(X,Y,T1) | phpt(Y,X,T1))))) # label(axiom35) # label(axiom) # label(non_clause). [assumption]. 36 (all X all Y all T (phtxtprec(X,Y,T) -> (all Z (phpt(Z,X,T) -> phtxtprec(Z,Y,T))))) # label(axiom36) # label(axiom) # label(non_clause). [assumption]. 37 (all X all Y all T (phtxtprec(X,Y,T) -> (all Z (phpt(Z,Y,T) -> phtxtprec(X,Z,T))))) # label(axiom37) # label(axiom) # label(non_clause). [assumption]. 38 (all X all Y all T (phtxtprec(X,Y,T) -> (exists Z (compphtxt(Z,T) & phpt(X,Z,T) & phpt(Y,Z,T))))) # label(axiom38a) # label(axiom) # label(non_clause). [assumption]. 39 (all X all Y all T all Z2 (phtxtprec(X,Y,T) -> (all Z1 all Z1 (compphtxt(Z1,T) & phpt(X,Z1,T) & phpt(Y,Z1,T) & compphtxt(Z2,T) & phpt(X,Z2,T) & phpt(Y,Z2,T) -> Z1 = Z2)))) # label(axiom38b) # label(axiom) # label(non_clause). [assumption]. 40 (all X all T (phtxt(X,T) -> (exists Y (phpt(Y,X,T) & (all Z (phpt(Z,X,T) -> -phtxtprec(Z,Y,T))))))) # label(axiom39) # label(axiom) # label(non_clause). [assumption]. 41 (all X all T (phtxt(X,T) -> (exists Y (phpt(Y,X,T) & (all Z (phpt(Z,X,T) -> -phtxtprec(Y,Z,T))))))) # label(axiom40) # label(axiom) # label(non_clause). [assumption]. 42 (all X all Y all T (phtxtprec(X,Y,T) & -(exists Z (phtxtprec(X,Z,T) & phtxtprec(Z,Y,T))) -> (exists Z phsumpt(Z,X,Y,T)))) # label(axiom41) # label(axiom) # label(non_clause). [assumption]. 43 (all X all Y all T all R1 all R2 (phtxtprec(X,Y,T) -> (occ(X,R1,T) & occ(Y,R2,T) -> -overlap(R1,R2,T)))) # label(axiom42) # label(axiom) # label(non_clause). [assumption]. 44 (all X all Y all T (phrep(X,Y,T) -> phtxt(X,T))) # label(axiom45) # label(axiom) # label(non_clause). [assumption]. 45 (all X all T all X ((exists Y phrep(X,Y,T)) -> (all T1 (present(X,T1) -> (exists Y phrep(X,Y,T1)))))) # label(axiom46) # label(axiom) # label(non_clause). [assumption]. 46 (all X all T all Y all T1 (phtxtequiv(X,T,Y,T1) -> phtxt(X,T) & phtxt(Y,T1))) # label(axiom47) # label(axiom) # label(non_clause). [assumption]. 47 (all X all T all Y all T1 (phtxtequiv(X,T,Y,T1) -> present(X,T) & present(Y,T1))) # label(axiom48) # label(axiom) # label(non_clause). [assumption]. 48 (all X all T (phtxt(X,T) -> phtxtequiv(X,T,X,T))) # label(axiom49) # label(axiom) # label(non_clause). [assumption]. 49 (all X all T all Y all T1 (phtxtequiv(X,T,Y,T1) -> phtxtequiv(Y,T1,X,T))) # label(axiom50) # label(axiom) # label(non_clause). [assumption]. 50 (all X all T1 all Y all T2 all Z all T3 (phtxtequiv(X,T1,Y,T2) & phtxtequiv(Y,T2,Z,T3) -> phtxtequiv(X,T1,Z,T3))) # label(axiom51) # label(axiom) # label(non_clause). [assumption]. 51 (all X all Y all T (ppt(X,Y,T) -> -phtxtequiv(X,T,Y,T))) # label(axiom52) # label(axiom) # label(non_clause). [assumption]. 52 (all X1 all T all X2 all Y1 (phtxtequiv(X1,T,X2,T) & phppt(Y1,X1,T) -> (exists Y2 (phtxtequiv(Y1,T,Y2,T) & ppt(Y2,X2,T))))) # label(axiom53) # label(axiom) # label(non_clause). [assumption]. 53 (all X1 all T all X2 all Y1 (phtxtequiv(X1,T,X2,T) & phppt(X1,Y1,T) -> (exists Y2 (phtxtequiv(Y1,T,Y2,T) & ppt(X2,Y2,T))))) # label(axiom54) # label(axiom) # label(non_clause). [assumption]. 54 (all X1 all T1 all X2 all T2 all Y (phtxtequiv(X1,T1,X2,T2) -> (phrep(X1,Y,T1) <-> phrep(X2,Y,T2)))) # label(axiom55) # label(axiom) # label(non_clause). [assumption]. 55 (all X all Y (txtdep(X,Y) -> (exists T txt(X,T)) & (exists T phtxt(Y,T)))) # label(axiom56) # label(axiom) # label(non_clause). [assumption]. 56 (all X all T (phtxt(X,T) -> (exists Y (txt(Y,T) & txtdep(Y,X))))) # label(axiom57a) # label(axiom) # label(non_clause). [assumption]. 57 (all X all T (phtxt(X,T) -> (all Y1 all Y2 (txt(Y1,T) & txtdep(Y1,X) & txt(Y2,T) & txtdep(Y2,X) -> Y1 = Y2)))) # label(axiom57b) # label(axiom) # label(non_clause). [assumption]. 58 (all X all T (txt(X,T) -> (exists Y (phtxt(Y,T) & txtdep(X,Y))))) # label(axiom58) # label(axiom) # label(non_clause). [assumption]. 59 (all X all Y1 all Y2 (txtdep(X,Y1) & txtdep(X,Y2) -> (all T1 all T2 (present(Y1,T1) & present(Y2,T2) -> phtxtequiv(Y1,T1,Y2,T2))))) # label(axiom59) # label(axiom) # label(non_clause). [assumption]. 60 (all X all Y (txtdep(X,Y) -> (all T (present(X,T) -> (exists Z exists T1 phtxtequiv(Z,T,Y,T1)))))) # label(axiom60) # label(axiom) # label(non_clause). [assumption]. 61 (all X all Y (txtdep(X,Y) -> (all T (present(Y,T) -> present(X,T))))) # label(axiom61) # label(axiom) # label(non_clause). [assumption]. 62 (all Y1 all T1 all Y2 all T2 (phtxtequiv(Y1,T1,Y2,T2) -> (all Z (txtdep(Z,Y1) <-> txtdep(Z,Y2))))) # label(axiom62) # label(axiom) # label(non_clause). [assumption]. 63 (all X1 all Y1 all X2 all Y2 all T (txtdep(X1,Y1) & txtdep(X2,Y2) -> (ppt(X1,X2,T) <-> ppt(Y1,Y2,T)))) # label(axiom63) # label(axiom) # label(non_clause). [assumption]. 64 (all X1 all Y1 all X2 all Y2 all T (txtdep(X1,Y1) & txtdep(X2,Y2) -> (phtxtprec(X1,X2,T) <-> phtxtprec(Y1,Y2,T)))) # label(axiom64) # label(axiom) # label(non_clause). [assumption]. 65 (all X all T all Z (txt(X,T) & ppt(Z,X,T) -> txt(Z,T))) # label(axiom65) # label(axiom) # label(non_clause). [assumption]. 66 (all T -(exists X (phtxt(X,T) & txt(X,T)))) # label(axiom66) # label(axiom) # label(non_clause). [assumption]. 67 (all X all Y all T (txtppt(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & ppt(X1,Y1,T))))) # label(axiom68) # label(axiom) # label(non_clause). [assumption]. 68 (all X all Y all T (txtpt(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & pt(X1,Y1,T))))) # label(axiomLXX) # label(axiom) # label(non_clause). [assumption]. 69 (all X all Y all T (txtoverlap(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & phoverlap(X1,Y1,T))))) # label(axiomLXXI) # label(axiom) # label(non_clause). [assumption]. 70 (all X all Y all T (txtprec(X,Y,T) <-> (exists X1 exists Y1 (txtdep(X,X1) & txtdep(Y,Y1) & phtxtprec(X1,Y1,T))))) # label(axiomLXXII) # label(axiom) # label(non_clause). [assumption]. 71 (all X all Y all T (txtrep(X,Y,T) <-> (exists X1 (txtdep(X,X1) & phrep(X1,Y,T))))) # label(axiomLXXIII) # label(axiom) # label(non_clause). [assumption]. 72 (all X all Y all Z all T (txtsumpt(X,Y,Z,T) <-> (exists X1 exists Y1 exists Z1 (txtdep(X,X1) & txtdep(Y,Y1) & txtdep(Z,Z1) & phsumpt(X1,Y1,Z1,T))))) # label(axiomLXXIV) # label(axiom) # label(non_clause). [assumption]. 73 (all X all T (comptxt(X,T) <-> (exists X1 (txtdep(X,X1) & compphtxt(X1,T))))) # label(axiomLXXV) # label(axiom) # label(non_clause). [assumption]. 74 (all X all T (phtxt(X,T) -> obj(X) & time(T))) # label(axiomC) # label(axiom) # label(non_clause). [assumption]. 75 (all X all T (txt(X,T) -> obj(X) & time(T))) # label(axiomCI) # label(axiom) # label(non_clause). [assumption]. 76 (all X all Y (txtdep(X,Y) -> obj(X) & obj(Y))) # label(axiomCII) # label(axiom) # label(non_clause). [assumption]. 77 (all X all T (present(X,T) -> nontime(X) & time(T))) # label(axiomCIII) # label(axiom) # label(non_clause). [assumption]. 78 (all S all R all T (occ(S,R,T) -> nontime(S) & reg(R) & time(T))) # label(axiomCIV) # label(axiom) # label(non_clause). [assumption]. 79 (all X all Y all T (ppt(X,Y,T) -> nontime(X) & nontime(Y) & time(T))) # label(axiomCV) # label(axiom) # label(non_clause). [assumption]. 80 (all X all Y all T (phtxtprec(X,Y,T) -> obj(X) & obj(Y) & time(T))) # label(axiomCVI) # label(axiom) # label(non_clause). [assumption]. 81 (all X all T1 all Y all T2 (phtxtequiv(X,T1,Y,T2) -> obj(X) & obj(Y) & time(T1) & time(T2))) # label(axiomCVII) # label(axiom) # label(non_clause). [assumption]. 82 (all X all Y all T (phrep(X,Y,T) -> obj(X) & obj(Y) & time(T))) # label(axiomCVIII) # label(axiom) # label(non_clause). [assumption]. 83 (all X (obj(X) | reg(X) -> nontime(X))) # label(axiomCIX) # label(axiom) # label(non_clause). [assumption]. 84 (all T (time(T) -> -nontime(T))) # label(axiomCX) # label(axiom) # label(non_clause). [assumption]. 85 (all X (obj(X) -> -reg(X))) # label(axiomCXI) # label(axiom) # label(non_clause). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -nontime(A) | present(A,f1(A)) # label(axiom1) # label(axiom). -phtxt(A,B) | -present(A,C) | phtxt(A,C) # label(axiom2) # label(axiom). -txt(A,B) | -present(A,C) | txt(A,C) # label(axiom3) # label(axiom). -pt(A,B,C) | ppt(A,B,C) | B = A # label(definition4) # label(axiom). -pt(A,B,C) | ppt(A,B,C) | present(A,C) # label(definition4) # label(axiom). -pt(A,B,C) | ppt(A,B,C) | present(B,C) # label(definition4) # label(axiom). pt(A,B,C) | -ppt(A,B,C) # label(definition4) # label(axiom). pt(A,B,C) | B != A | -present(A,C) | -present(B,C) # label(definition4) # label(axiom). -overlap(A,B,C) | pt(f2(A,B,C),A,C) # label(definition5) # label(axiom). -overlap(A,B,C) | pt(f2(A,B,C),B,C) # label(definition5) # label(axiom). overlap(A,B,C) | -pt(D,A,C) | -pt(D,B,C) # label(definition5) # label(axiom). -sumpt(A,B,C,D) | pt(B,A,D) # label(definition6) # label(axiom). -sumpt(A,B,C,D) | pt(C,A,D) # label(definition6) # label(axiom). -sumpt(A,B,C,D) | -pt(E,A,D) | overlap(E,B,D) | overlap(E,C,D) # label(definition6) # label(axiom). sumpt(A,B,C,D) | -pt(B,A,D) | -pt(C,A,D) | pt(f3(A,B,C,D),A,D) # label(definition6) # label(axiom). sumpt(A,B,C,D) | -pt(B,A,D) | -pt(C,A,D) | -overlap(f3(A,B,C,D),B,D) # label(definition6) # label(axiom). sumpt(A,B,C,D) | -pt(B,A,D) | -pt(C,A,D) | -overlap(f3(A,B,C,D),C,D) # label(definition6) # label(axiom). -ppt(A,B,C) | present(A,C) # label(axiom7) # label(axiom). -ppt(A,B,C) | present(B,C) # label(axiom7) # label(axiom). -ppt(A,A,B) # label(axiom8) # label(axiom). -ppt(A,B,C) | -ppt(B,D,C) | ppt(A,D,C) # label(axiom9) # label(axiom). -ppt(A,B,C) | ppt(f4(A,B,C),B,C) # label(axiom10) # label(axiom). -ppt(A,B,C) | -overlap(A,f4(A,B,C),C) # label(axiom10) # label(axiom). -present(A,B) | -present(C,B) | sumpt(f5(A,B,C),A,C,B) # label(axiom11) # label(axiom). -reg(A) | -time(B) | occ(A,A,B) # label(axiom12) # label(axiom). -occ(A,B,C) | present(A,C) # label(axiom13) # label(axiom). -occ(A,B,C) | present(B,C) # label(axiom13) # label(axiom). -ppt(A,B,C) | -reg(B) | -time(C) | occ(A,A,C) # label(axiom14) # label(axiom). -ppt(A,B,C) | -occ(B,D,C) | ppt(f6(A,B,C,D),D,C) # label(axiom15) # label(axiom). -ppt(A,B,C) | -occ(B,D,C) | occ(A,f6(A,B,C,D),C) # label(axiom15) # label(axiom). -phtxt(A,B) | time(f7(A,B)) # label(axiom16) # label(axiom). -phtxt(A,B) | -present(A,f7(A,B)) # label(axiom16) # label(axiom). -phppt(A,B,C) | ppt(A,B,C) # label(definition17) # label(axiom). -phppt(A,B,C) | phtxt(A,C) # label(definition17) # label(axiom). -phppt(A,B,C) | phtxt(B,C) # label(definition17) # label(axiom). phppt(A,B,C) | -ppt(A,B,C) | -phtxt(A,C) | -phtxt(B,C) # label(definition17) # label(axiom). -phpt(A,B,C) | pt(A,B,C) # label(definition18) # label(axiom). -phpt(A,B,C) | phtxt(A,C) # label(definition18) # label(axiom). -phpt(A,B,C) | phtxt(B,C) # label(definition18) # label(axiom). phpt(A,B,C) | -pt(A,B,C) | -phtxt(A,C) | -phtxt(B,C) # label(definition18) # label(axiom). -phoverlap(A,B,C) | phpt(f8(A,B,C),A,C) # label(definition19) # label(axiom). -phoverlap(A,B,C) | phpt(f8(A,B,C),B,C) # label(definition19) # label(axiom). phoverlap(A,B,C) | -phpt(D,A,C) | -phpt(D,B,C) # label(definition19) # label(axiom). -phsumpt(A,B,C,D) | phpt(B,A,D) # label(definition20) # label(axiom). -phsumpt(A,B,C,D) | phpt(C,A,D) # label(definition20) # label(axiom). -phsumpt(A,B,C,D) | -phpt(E,A,D) | phoverlap(E,B,D) | phoverlap(E,C,D) # label(definition20) # label(axiom). phsumpt(A,B,C,D) | -phpt(B,A,D) | -phpt(C,A,D) | phpt(f9(A,B,C,D),A,D) # label(definition20) # label(axiom). phsumpt(A,B,C,D) | -phpt(B,A,D) | -phpt(C,A,D) | -phoverlap(f9(A,B,C,D),B,D) # label(definition20) # label(axiom). phsumpt(A,B,C,D) | -phpt(B,A,D) | -phpt(C,A,D) | -phoverlap(f9(A,B,C,D),C,D) # label(definition20) # label(axiom). -compphtxt(A,B) | phtxt(A,B) # label(definition21) # label(axiom). -compphtxt(A,B) | -phppt(A,C,B) # label(definition21) # label(axiom). compphtxt(A,B) | -phtxt(A,B) | phppt(A,f10(A,B),B) # label(definition21) # label(axiom). -phppt(A,B,C) | -phppt(B,A,D) # label(axiom22) # label(axiom). -phtxt(A,B) | -phtxt(C,B) | phpt(A,C,B) | phpt(f11(A,B,C),A,B) # label(axiom23) # label(axiom). -phtxt(A,B) | -phtxt(C,B) | phpt(A,C,B) | -phoverlap(f11(A,B,C),C,B) # label(axiom23) # label(axiom). -phtxt(A,B) | -phtxt(f12(A,B),B) # label(axiom24) # label(axiom). -phtxt(A,B) | pt(f12(A,B),A,B) # label(axiom24) # label(axiom). -phppt(A,B,C) | phppt(A,f13(A,B,C),C) # label(axiom25) # label(axiom). -phppt(A,B,C) | -phppt(A,D,C) | -phppt(D,f13(A,B,C),C) # label(axiom25) # label(axiom). -phppt(A,B,C) | phppt(f14(A,B,C),B,C) # label(axiom26) # label(axiom). -phppt(A,B,C) | -phppt(f14(A,B,C),D,C) | -phppt(D,B,C) # label(axiom26) # label(axiom). -phtxt(A,B) | -phpt(f15(A,B,C),A,B) | phpt(f16(A,B,C),C,B) # label(axiom27) # label(axiom). -phtxt(A,B) | -phpt(f15(A,B,C),A,B) | -phppt(D,f16(A,B,C),B) # label(axiom27) # label(axiom). -phtxt(A,B) | occ(A,f17(A,B),B) # label(axiom28) # label(axiom). -occ(A,B,C) | -occ(D,B,C) | -phtxt(A,C) | -phtxt(D,C) | D = A # label(axiom29) # label(axiom). -phtxtprec(A,B,C) | phtxt(A,C) # label(axiom30) # label(axiom). -phtxtprec(A,B,C) | phtxt(B,C) # label(axiom30) # label(axiom). -phtxtprec(A,A,B) # label(axiom31) # label(axiom). -phtxtprec(A,B,C) | -phtxtprec(B,D,C) | phtxtprec(A,D,C) # label(axiom32) # label(axiom). -phtxtprec(A,B,C) | phtxtprec(A,f18(A,B,C),C) # label(axiom33) # label(axiom). -phtxtprec(A,B,C) | -phtxtprec(A,D,C) | -phtxtprec(D,f18(A,B,C),C) # label(axiom33) # label(axiom). -phtxtprec(A,B,C) | phtxtprec(f19(A,B,C),B,C) # label(axiom34) # label(axiom). -phtxtprec(A,B,C) | -phtxtprec(f19(A,B,C),D,C) | -phtxtprec(D,B,C) # label(axiom34) # label(axiom). -phtxtprec(A,B,C) | -phpt(A,B,D) # label(axiom35) # label(axiom). -phtxtprec(A,B,C) | -phpt(B,A,D) # label(axiom35) # label(axiom). -phtxtprec(A,B,C) | -phpt(D,A,C) | phtxtprec(D,B,C) # label(axiom36) # label(axiom). -phtxtprec(A,B,C) | -phpt(D,B,C) | phtxtprec(A,D,C) # label(axiom37) # label(axiom). -phtxtprec(A,B,C) | compphtxt(f20(A,B,C),C) # label(axiom38a) # label(axiom). -phtxtprec(A,B,C) | phpt(A,f20(A,B,C),C) # label(axiom38a) # label(axiom). -phtxtprec(A,B,C) | phpt(B,f20(A,B,C),C) # label(axiom38a) # label(axiom). -phtxtprec(A,B,C) | -compphtxt(D,C) | -phpt(A,D,C) | -phpt(B,D,C) | -compphtxt(E,C) | -phpt(A,E,C) | -phpt(B,E,C) | D = E # label(axiom38b) # label(axiom). -phtxt(A,B) | phpt(f21(A,B),A,B) # label(axiom39) # label(axiom). -phtxt(A,B) | -phpt(C,A,B) | -phtxtprec(C,f21(A,B),B) # label(axiom39) # label(axiom). -phtxt(A,B) | phpt(f22(A,B),A,B) # label(axiom40) # label(axiom). -phtxt(A,B) | -phpt(C,A,B) | -phtxtprec(f22(A,B),C,B) # label(axiom40) # label(axiom). -phtxtprec(A,B,C) | phtxtprec(A,f23(A,B,C),C) | phsumpt(f24(A,B,C),A,B,C) # label(axiom41) # label(axiom). -phtxtprec(A,B,C) | phtxtprec(f23(A,B,C),B,C) | phsumpt(f24(A,B,C),A,B,C) # label(axiom41) # label(axiom). -phtxtprec(A,B,C) | -occ(A,D,C) | -occ(B,E,C) | -overlap(D,E,C) # label(axiom42) # label(axiom). -phrep(A,B,C) | phtxt(A,C) # label(axiom45) # label(axiom). -phrep(A,B,C) | -present(A,D) | phrep(A,f25(E,C,A,D),D) # label(axiom46) # label(axiom). -phtxtequiv(A,B,C,D) | phtxt(A,B) # label(axiom47) # label(axiom). -phtxtequiv(A,B,C,D) | phtxt(C,D) # label(axiom47) # label(axiom). -phtxtequiv(A,B,C,D) | present(A,B) # label(axiom48) # label(axiom). -phtxtequiv(A,B,C,D) | present(C,D) # label(axiom48) # label(axiom). -phtxt(A,B) | phtxtequiv(A,B,A,B) # label(axiom49) # label(axiom). -phtxtequiv(A,B,C,D) | phtxtequiv(C,D,A,B) # label(axiom50) # label(axiom). -phtxtequiv(A,B,C,D) | -phtxtequiv(C,D,E,F) | phtxtequiv(A,B,E,F) # label(axiom51) # label(axiom). -ppt(A,B,C) | -phtxtequiv(A,C,B,C) # label(axiom52) # label(axiom). -phtxtequiv(A,B,C,B) | -phppt(D,A,B) | phtxtequiv(D,B,f26(A,B,C,D),B) # label(axiom53) # label(axiom). -phtxtequiv(A,B,C,B) | -phppt(D,A,B) | ppt(f26(A,B,C,D),C,B) # label(axiom53) # label(axiom). -phtxtequiv(A,B,C,B) | -phppt(A,D,B) | phtxtequiv(D,B,f27(A,B,C,D),B) # label(axiom54) # label(axiom). -phtxtequiv(A,B,C,B) | -phppt(A,D,B) | ppt(C,f27(A,B,C,D),B) # label(axiom54) # label(axiom). -phtxtequiv(A,B,C,D) | -phrep(A,E,B) | phrep(C,E,D) # label(axiom55) # label(axiom). -phtxtequiv(A,B,C,D) | phrep(A,E,B) | -phrep(C,E,D) # label(axiom55) # label(axiom). -txtdep(A,B) | txt(A,f28(A,B)) # label(axiom56) # label(axiom). -txtdep(A,B) | phtxt(B,f29(A,B)) # label(axiom56) # label(axiom). -phtxt(A,B) | txt(f30(A,B),B) # label(axiom57a) # label(axiom). -phtxt(A,B) | txtdep(f30(A,B),A) # label(axiom57a) # label(axiom). -phtxt(A,B) | -txt(C,B) | -txtdep(C,A) | -txt(D,B) | -txtdep(D,A) | D = C # label(axiom57b) # label(axiom). -txt(A,B) | phtxt(f31(A,B),B) # label(axiom58) # label(axiom). -txt(A,B) | txtdep(A,f31(A,B)) # label(axiom58) # label(axiom). -txtdep(A,B) | -txtdep(A,C) | -present(B,D) | -present(C,E) | phtxtequiv(B,D,C,E) # label(axiom59) # label(axiom). -txtdep(A,B) | -present(A,C) | phtxtequiv(f32(A,B,C),C,B,f33(A,B,C)) # label(axiom60) # label(axiom). -txtdep(A,B) | -present(B,C) | present(A,C) # label(axiom61) # label(axiom). -phtxtequiv(A,B,C,D) | -txtdep(E,A) | txtdep(E,C) # label(axiom62) # label(axiom). -phtxtequiv(A,B,C,D) | txtdep(E,A) | -txtdep(E,C) # label(axiom62) # label(axiom). -txtdep(A,B) | -txtdep(C,D) | -ppt(A,C,E) | ppt(B,D,E) # label(axiom63) # label(axiom). -txtdep(A,B) | -txtdep(C,D) | ppt(A,C,E) | -ppt(B,D,E) # label(axiom63) # label(axiom). -txtdep(A,B) | -txtdep(C,D) | -phtxtprec(A,C,E) | phtxtprec(B,D,E) # label(axiom64) # label(axiom). -txtdep(A,B) | -txtdep(C,D) | phtxtprec(A,C,E) | -phtxtprec(B,D,E) # label(axiom64) # label(axiom). -txt(A,B) | -ppt(C,A,B) | txt(C,B) # label(axiom65) # label(axiom). -phtxt(A,B) | -txt(A,B) # label(axiom66) # label(axiom). -txtppt(A,B,C) | txtdep(A,f34(A,B,C)) # label(axiom68) # label(axiom). -txtppt(A,B,C) | txtdep(B,f35(A,B,C)) # label(axiom68) # label(axiom). -txtppt(A,B,C) | ppt(f34(A,B,C),f35(A,B,C),C) # label(axiom68) # label(axiom). txtppt(A,B,C) | -txtdep(A,D) | -txtdep(B,E) | -ppt(D,E,C) # label(axiom68) # label(axiom). -txtpt(A,B,C) | txtdep(A,f36(A,B,C)) # label(axiomLXX) # label(axiom). -txtpt(A,B,C) | txtdep(B,f37(A,B,C)) # label(axiomLXX) # label(axiom). -txtpt(A,B,C) | pt(f36(A,B,C),f37(A,B,C),C) # label(axiomLXX) # label(axiom). txtpt(A,B,C) | -txtdep(A,D) | -txtdep(B,E) | -pt(D,E,C) # label(axiomLXX) # label(axiom). -txtoverlap(A,B,C) | txtdep(A,f38(A,B,C)) # label(axiomLXXI) # label(axiom). -txtoverlap(A,B,C) | txtdep(B,f39(A,B,C)) # label(axiomLXXI) # label(axiom). -txtoverlap(A,B,C) | phoverlap(f38(A,B,C),f39(A,B,C),C) # label(axiomLXXI) # label(axiom). txtoverlap(A,B,C) | -txtdep(A,D) | -txtdep(B,E) | -phoverlap(D,E,C) # label(axiomLXXI) # label(axiom). -txtprec(A,B,C) | txtdep(A,f40(A,B,C)) # label(axiomLXXII) # label(axiom). -txtprec(A,B,C) | txtdep(B,f41(A,B,C)) # label(axiomLXXII) # label(axiom). -txtprec(A,B,C) | phtxtprec(f40(A,B,C),f41(A,B,C),C) # label(axiomLXXII) # label(axiom). txtprec(A,B,C) | -txtdep(A,D) | -txtdep(B,E) | -phtxtprec(D,E,C) # label(axiomLXXII) # label(axiom). -txtrep(A,B,C) | txtdep(A,f42(A,B,C)) # label(axiomLXXIII) # label(axiom). -txtrep(A,B,C) | phrep(f42(A,B,C),B,C) # label(axiomLXXIII) # label(axiom). txtrep(A,B,C) | -txtdep(A,D) | -phrep(D,B,C) # label(axiomLXXIII) # label(axiom). -txtsumpt(A,B,C,D) | txtdep(A,f43(A,B,C,D)) # label(axiomLXXIV) # label(axiom). -txtsumpt(A,B,C,D) | txtdep(B,f44(A,B,C,D)) # label(axiomLXXIV) # label(axiom). -txtsumpt(A,B,C,D) | txtdep(C,f45(A,B,C,D)) # label(axiomLXXIV) # label(axiom). -txtsumpt(A,B,C,D) | phsumpt(f43(A,B,C,D),f44(A,B,C,D),f45(A,B,C,D),D) # label(axiomLXXIV) # label(axiom). txtsumpt(A,B,C,D) | -txtdep(A,E) | -txtdep(B,F) | -txtdep(C,V6) | -phsumpt(E,F,V6,D) # label(axiomLXXIV) # label(axiom). -comptxt(A,B) | txtdep(A,f46(A,B)) # label(axiomLXXV) # label(axiom). -comptxt(A,B) | compphtxt(f46(A,B),B) # label(axiomLXXV) # label(axiom). comptxt(A,B) | -txtdep(A,C) | -compphtxt(C,B) # label(axiomLXXV) # label(axiom). -phtxt(A,B) | obj(A) # label(axiomC) # label(axiom). -phtxt(A,B) | time(B) # label(axiomC) # label(axiom). -txt(A,B) | obj(A) # label(axiomCI) # label(axiom). -txt(A,B) | time(B) # label(axiomCI) # label(axiom). -txtdep(A,B) | obj(A) # label(axiomCII) # label(axiom). -txtdep(A,B) | obj(B) # label(axiomCII) # label(axiom). -present(A,B) | nontime(A) # label(axiomCIII) # label(axiom). -present(A,B) | time(B) # label(axiomCIII) # label(axiom). -occ(A,B,C) | nontime(A) # label(axiomCIV) # label(axiom). -occ(A,B,C) | reg(B) # label(axiomCIV) # label(axiom). -occ(A,B,C) | time(C) # label(axiomCIV) # label(axiom). -ppt(A,B,C) | nontime(A) # label(axiomCV) # label(axiom). -ppt(A,B,C) | nontime(B) # label(axiomCV) # label(axiom). -ppt(A,B,C) | time(C) # label(axiomCV) # label(axiom). -phtxtprec(A,B,C) | obj(A) # label(axiomCVI) # label(axiom). -phtxtprec(A,B,C) | obj(B) # label(axiomCVI) # label(axiom). -phtxtprec(A,B,C) | time(C) # label(axiomCVI) # label(axiom). -phtxtequiv(A,B,C,D) | obj(A) # label(axiomCVII) # label(axiom). -phtxtequiv(A,B,C,D) | obj(C) # label(axiomCVII) # label(axiom). -phtxtequiv(A,B,C,D) | time(B) # label(axiomCVII) # label(axiom). -phtxtequiv(A,B,C,D) | time(D) # label(axiomCVII) # label(axiom). -phrep(A,B,C) | obj(A) # label(axiomCVIII) # label(axiom). -phrep(A,B,C) | obj(B) # label(axiomCVIII) # label(axiom). -phrep(A,B,C) | time(C) # label(axiomCVIII) # label(axiom). -obj(A) | nontime(A) # label(axiomCIX) # label(axiom). -reg(A) | nontime(A) # label(axiomCIX) # label(axiom). -time(A) | -nontime(A) # label(axiomCX) # label(axiom). -obj(A) | -reg(A) # label(axiomCXI) # label(axiom). end_of_list. ============================== end of clauses for search ============= % SZS output start FiniteModel % There are no natural numbers in the input. f1 : 0 1 ------- 0 0 f7 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f10 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f12 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f17 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f21 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f22 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f28 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f29 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f30 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f31 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f46 : | 0 1 --+---- 0 | 0 0 1 | 0 0 f2(0,0,0) = 0. f2(0,0,1) = 0. f2(0,1,0) = 0. f2(0,1,1) = 0. f2(1,0,0) = 0. f2(1,0,1) = 0. f2(1,1,0) = 0. f2(1,1,1) = 0. f4(0,0,0) = 0. f4(0,0,1) = 0. f4(0,1,0) = 0. f4(0,1,1) = 0. f4(1,0,0) = 0. f4(1,0,1) = 0. f4(1,1,0) = 0. f4(1,1,1) = 0. f5(0,0,0) = 0. f5(0,0,1) = 0. f5(0,1,0) = 0. f5(0,1,1) = 0. f5(1,0,0) = 0. f5(1,0,1) = 0. f5(1,1,0) = 0. f5(1,1,1) = 0. f8(0,0,0) = 0. f8(0,0,1) = 0. f8(0,1,0) = 0. f8(0,1,1) = 0. f8(1,0,0) = 0. f8(1,0,1) = 0. f8(1,1,0) = 0. f8(1,1,1) = 0. f11(0,0,0) = 0. f11(0,0,1) = 0. f11(0,1,0) = 0. f11(0,1,1) = 0. f11(1,0,0) = 0. f11(1,0,1) = 0. f11(1,1,0) = 0. f11(1,1,1) = 0. f13(0,0,0) = 0. f13(0,0,1) = 0. f13(0,1,0) = 0. f13(0,1,1) = 0. f13(1,0,0) = 0. f13(1,0,1) = 0. f13(1,1,0) = 0. f13(1,1,1) = 0. f14(0,0,0) = 0. f14(0,0,1) = 0. f14(0,1,0) = 0. f14(0,1,1) = 0. f14(1,0,0) = 0. f14(1,0,1) = 0. f14(1,1,0) = 0. f14(1,1,1) = 0. f15(0,0,0) = 0. f15(0,0,1) = 0. f15(0,1,0) = 0. f15(0,1,1) = 0. f15(1,0,0) = 0. f15(1,0,1) = 0. f15(1,1,0) = 0. f15(1,1,1) = 0. f16(0,0,0) = 0. f16(0,0,1) = 0. f16(0,1,0) = 0. f16(0,1,1) = 0. f16(1,0,0) = 0. f16(1,0,1) = 0. f16(1,1,0) = 0. f16(1,1,1) = 0. f18(0,0,0) = 0. f18(0,0,1) = 0. f18(0,1,0) = 0. f18(0,1,1) = 0. f18(1,0,0) = 0. f18(1,0,1) = 0. f18(1,1,0) = 0. f18(1,1,1) = 0. f19(0,0,0) = 0. f19(0,0,1) = 0. f19(0,1,0) = 0. f19(0,1,1) = 0. f19(1,0,0) = 0. f19(1,0,1) = 0. f19(1,1,0) = 0. f19(1,1,1) = 0. f20(0,0,0) = 0. f20(0,0,1) = 0. f20(0,1,0) = 0. f20(0,1,1) = 0. f20(1,0,0) = 0. f20(1,0,1) = 0. f20(1,1,0) = 0. f20(1,1,1) = 0. f23(0,0,0) = 0. f23(0,0,1) = 0. f23(0,1,0) = 0. f23(0,1,1) = 0. f23(1,0,0) = 0. f23(1,0,1) = 0. f23(1,1,0) = 0. f23(1,1,1) = 0. f24(0,0,0) = 0. f24(0,0,1) = 0. f24(0,1,0) = 0. f24(0,1,1) = 0. f24(1,0,0) = 0. f24(1,0,1) = 0. f24(1,1,0) = 0. f24(1,1,1) = 0. f32(0,0,0) = 0. f32(0,0,1) = 0. f32(0,1,0) = 0. f32(0,1,1) = 0. f32(1,0,0) = 0. f32(1,0,1) = 0. f32(1,1,0) = 0. f32(1,1,1) = 0. f33(0,0,0) = 0. f33(0,0,1) = 0. f33(0,1,0) = 0. f33(0,1,1) = 0. f33(1,0,0) = 0. f33(1,0,1) = 0. f33(1,1,0) = 0. f33(1,1,1) = 0. f34(0,0,0) = 0. f34(0,0,1) = 0. f34(0,1,0) = 0. f34(0,1,1) = 0. f34(1,0,0) = 0. f34(1,0,1) = 0. f34(1,1,0) = 0. f34(1,1,1) = 0. f35(0,0,0) = 0. f35(0,0,1) = 0. f35(0,1,0) = 0. f35(0,1,1) = 0. f35(1,0,0) = 0. f35(1,0,1) = 0. f35(1,1,0) = 0. f35(1,1,1) = 0. f36(0,0,0) = 0. f36(0,0,1) = 0. f36(0,1,0) = 0. f36(0,1,1) = 0. f36(1,0,0) = 0. f36(1,0,1) = 0. f36(1,1,0) = 0. f36(1,1,1) = 0. f37(0,0,0) = 0. f37(0,0,1) = 0. f37(0,1,0) = 0. f37(0,1,1) = 0. f37(1,0,0) = 0. f37(1,0,1) = 0. f37(1,1,0) = 0. f37(1,1,1) = 0. f38(0,0,0) = 0. f38(0,0,1) = 0. f38(0,1,0) = 0. f38(0,1,1) = 0. f38(1,0,0) = 0. f38(1,0,1) = 0. f38(1,1,0) = 0. f38(1,1,1) = 0. f39(0,0,0) = 0. f39(0,0,1) = 0. f39(0,1,0) = 0. f39(0,1,1) = 0. f39(1,0,0) = 0. f39(1,0,1) = 0. f39(1,1,0) = 0. f39(1,1,1) = 0. f40(0,0,0) = 0. f40(0,0,1) = 0. f40(0,1,0) = 0. f40(0,1,1) = 0. f40(1,0,0) = 0. f40(1,0,1) = 0. f40(1,1,0) = 0. f40(1,1,1) = 0. f41(0,0,0) = 0. f41(0,0,1) = 0. f41(0,1,0) = 0. f41(0,1,1) = 0. f41(1,0,0) = 0. f41(1,0,1) = 0. f41(1,1,0) = 0. f41(1,1,1) = 0. f42(0,0,0) = 0. f42(0,0,1) = 0. f42(0,1,0) = 0. f42(0,1,1) = 0. f42(1,0,0) = 0. f42(1,0,1) = 0. f42(1,1,0) = 0. f42(1,1,1) = 0. f3(0,0,0,0) = 0. f3(0,0,0,1) = 0. f3(0,0,1,0) = 0. f3(0,0,1,1) = 0. f3(0,1,0,0) = 0. f3(0,1,0,1) = 0. f3(0,1,1,0) = 0. f3(0,1,1,1) = 0. f3(1,0,0,0) = 0. f3(1,0,0,1) = 0. f3(1,0,1,0) = 0. f3(1,0,1,1) = 0. f3(1,1,0,0) = 0. f3(1,1,0,1) = 0. f3(1,1,1,0) = 0. f3(1,1,1,1) = 0. f6(0,0,0,0) = 0. f6(0,0,0,1) = 0. f6(0,0,1,0) = 0. f6(0,0,1,1) = 0. f6(0,1,0,0) = 0. f6(0,1,0,1) = 0. f6(0,1,1,0) = 0. f6(0,1,1,1) = 0. f6(1,0,0,0) = 0. f6(1,0,0,1) = 0. f6(1,0,1,0) = 0. f6(1,0,1,1) = 0. f6(1,1,0,0) = 0. f6(1,1,0,1) = 0. f6(1,1,1,0) = 0. f6(1,1,1,1) = 0. f9(0,0,0,0) = 0. f9(0,0,0,1) = 0. f9(0,0,1,0) = 0. f9(0,0,1,1) = 0. f9(0,1,0,0) = 0. f9(0,1,0,1) = 0. f9(0,1,1,0) = 0. f9(0,1,1,1) = 0. f9(1,0,0,0) = 0. f9(1,0,0,1) = 0. f9(1,0,1,0) = 0. f9(1,0,1,1) = 0. f9(1,1,0,0) = 0. f9(1,1,0,1) = 0. f9(1,1,1,0) = 0. f9(1,1,1,1) = 0. f25(0,0,0,0) = 0. f25(0,0,0,1) = 0. f25(0,0,1,0) = 0. f25(0,0,1,1) = 0. f25(0,1,0,0) = 0. f25(0,1,0,1) = 0. f25(0,1,1,0) = 0. f25(0,1,1,1) = 0. f25(1,0,0,0) = 0. f25(1,0,0,1) = 0. f25(1,0,1,0) = 0. f25(1,0,1,1) = 0. f25(1,1,0,0) = 0. f25(1,1,0,1) = 0. f25(1,1,1,0) = 0. f25(1,1,1,1) = 0. f26(0,0,0,0) = 0. f26(0,0,0,1) = 0. f26(0,0,1,0) = 0. f26(0,0,1,1) = 0. f26(0,1,0,0) = 0. f26(0,1,0,1) = 0. f26(0,1,1,0) = 0. f26(0,1,1,1) = 0. f26(1,0,0,0) = 0. f26(1,0,0,1) = 0. f26(1,0,1,0) = 0. f26(1,0,1,1) = 0. f26(1,1,0,0) = 0. f26(1,1,0,1) = 0. f26(1,1,1,0) = 0. f26(1,1,1,1) = 0. f27(0,0,0,0) = 0. f27(0,0,0,1) = 0. f27(0,0,1,0) = 0. f27(0,0,1,1) = 0. f27(0,1,0,0) = 0. f27(0,1,0,1) = 0. f27(0,1,1,0) = 0. f27(0,1,1,1) = 0. f27(1,0,0,0) = 0. f27(1,0,0,1) = 0. f27(1,0,1,0) = 0. f27(1,0,1,1) = 0. f27(1,1,0,0) = 0. f27(1,1,0,1) = 0. f27(1,1,1,0) = 0. f27(1,1,1,1) = 0. f43(0,0,0,0) = 0. f43(0,0,0,1) = 0. f43(0,0,1,0) = 0. f43(0,0,1,1) = 0. f43(0,1,0,0) = 0. f43(0,1,0,1) = 0. f43(0,1,1,0) = 0. f43(0,1,1,1) = 0. f43(1,0,0,0) = 0. f43(1,0,0,1) = 0. f43(1,0,1,0) = 0. f43(1,0,1,1) = 0. f43(1,1,0,0) = 0. f43(1,1,0,1) = 0. f43(1,1,1,0) = 0. f43(1,1,1,1) = 0. f44(0,0,0,0) = 0. f44(0,0,0,1) = 0. f44(0,0,1,0) = 0. f44(0,0,1,1) = 0. f44(0,1,0,0) = 0. f44(0,1,0,1) = 0. f44(0,1,1,0) = 0. f44(0,1,1,1) = 0. f44(1,0,0,0) = 0. f44(1,0,0,1) = 0. f44(1,0,1,0) = 0. f44(1,0,1,1) = 0. f44(1,1,0,0) = 0. f44(1,1,0,1) = 0. f44(1,1,1,0) = 0. f44(1,1,1,1) = 0. f45(0,0,0,0) = 0. f45(0,0,0,1) = 0. f45(0,0,1,0) = 0. f45(0,0,1,1) = 0. f45(0,1,0,0) = 0. f45(0,1,0,1) = 0. f45(0,1,1,0) = 0. f45(0,1,1,1) = 0. f45(1,0,0,0) = 0. f45(1,0,0,1) = 0. f45(1,0,1,0) = 0. f45(1,0,1,1) = 0. f45(1,1,0,0) = 0. f45(1,1,0,1) = 0. f45(1,1,1,0) = 0. f45(1,1,1,1) = 0. nontime : 0 1 ------- 0 0 obj : 0 1 ------- 0 0 reg : 0 1 ------- 0 0 time : 0 1 ------- 0 0 compphtxt : | 0 1 --+---- 0 | 0 0 1 | 0 0 comptxt : | 0 1 --+---- 0 | 0 0 1 | 0 0 phtxt : | 0 1 --+---- 0 | 0 0 1 | 0 0 present : | 0 1 --+---- 0 | 0 0 1 | 0 0 txt : | 0 1 --+---- 0 | 0 0 1 | 0 0 txtdep : | 0 1 --+---- 0 | 0 0 1 | 0 0 occ(0,0,0) = 0. occ(0,0,1) = 0. occ(0,1,0) = 0. occ(0,1,1) = 0. occ(1,0,0) = 0. occ(1,0,1) = 0. occ(1,1,0) = 0. occ(1,1,1) = 0. overlap(0,0,0) = 0. overlap(0,0,1) = 0. overlap(0,1,0) = 0. overlap(0,1,1) = 0. overlap(1,0,0) = 0. overlap(1,0,1) = 0. overlap(1,1,0) = 0. overlap(1,1,1) = 0. phoverlap(0,0,0) = 0. phoverlap(0,0,1) = 0. phoverlap(0,1,0) = 0. phoverlap(0,1,1) = 0. phoverlap(1,0,0) = 0. phoverlap(1,0,1) = 0. phoverlap(1,1,0) = 0. phoverlap(1,1,1) = 0. phppt(0,0,0) = 0. phppt(0,0,1) = 0. phppt(0,1,0) = 0. phppt(0,1,1) = 0. phppt(1,0,0) = 0. phppt(1,0,1) = 0. phppt(1,1,0) = 0. phppt(1,1,1) = 0. phpt(0,0,0) = 0. phpt(0,0,1) = 0. phpt(0,1,0) = 0. phpt(0,1,1) = 0. phpt(1,0,0) = 0. phpt(1,0,1) = 0. phpt(1,1,0) = 0. phpt(1,1,1) = 0. phrep(0,0,0) = 0. phrep(0,0,1) = 0. phrep(0,1,0) = 0. phrep(0,1,1) = 0. phrep(1,0,0) = 0. phrep(1,0,1) = 0. phrep(1,1,0) = 0. phrep(1,1,1) = 0. phtxtprec(0,0,0) = 0. phtxtprec(0,0,1) = 0. phtxtprec(0,1,0) = 0. phtxtprec(0,1,1) = 0. phtxtprec(1,0,0) = 0. phtxtprec(1,0,1) = 0. phtxtprec(1,1,0) = 0. phtxtprec(1,1,1) = 0. ppt(0,0,0) = 0. ppt(0,0,1) = 0. ppt(0,1,0) = 0. ppt(0,1,1) = 0. ppt(1,0,0) = 0. ppt(1,0,1) = 0. ppt(1,1,0) = 0. ppt(1,1,1) = 0. pt(0,0,0) = 0. pt(0,0,1) = 0. pt(0,1,0) = 0. pt(0,1,1) = 0. pt(1,0,0) = 0. pt(1,0,1) = 0. pt(1,1,0) = 0. pt(1,1,1) = 0. txtoverlap(0,0,0) = 0. txtoverlap(0,0,1) = 0. txtoverlap(0,1,0) = 0. txtoverlap(0,1,1) = 0. txtoverlap(1,0,0) = 0. txtoverlap(1,0,1) = 0. txtoverlap(1,1,0) = 0. txtoverlap(1,1,1) = 0. txtppt(0,0,0) = 0. txtppt(0,0,1) = 0. txtppt(0,1,0) = 0. txtppt(0,1,1) = 0. txtppt(1,0,0) = 0. txtppt(1,0,1) = 0. txtppt(1,1,0) = 0. txtppt(1,1,1) = 0. txtprec(0,0,0) = 0. txtprec(0,0,1) = 0. txtprec(0,1,0) = 0. txtprec(0,1,1) = 0. txtprec(1,0,0) = 0. txtprec(1,0,1) = 0. txtprec(1,1,0) = 0. txtprec(1,1,1) = 0. txtpt(0,0,0) = 0. txtpt(0,0,1) = 0. txtpt(0,1,0) = 0. txtpt(0,1,1) = 0. txtpt(1,0,0) = 0. txtpt(1,0,1) = 0. txtpt(1,1,0) = 0. txtpt(1,1,1) = 0. txtrep(0,0,0) = 0. txtrep(0,0,1) = 0. txtrep(0,1,0) = 0. txtrep(0,1,1) = 0. txtrep(1,0,0) = 0. txtrep(1,0,1) = 0. txtrep(1,1,0) = 0. txtrep(1,1,1) = 0. phsumpt(0,0,0,0) = 0. phsumpt(0,0,0,1) = 0. phsumpt(0,0,1,0) = 0. phsumpt(0,0,1,1) = 0. phsumpt(0,1,0,0) = 0. phsumpt(0,1,0,1) = 0. phsumpt(0,1,1,0) = 0. phsumpt(0,1,1,1) = 0. phsumpt(1,0,0,0) = 0. phsumpt(1,0,0,1) = 0. phsumpt(1,0,1,0) = 0. phsumpt(1,0,1,1) = 0. phsumpt(1,1,0,0) = 0. phsumpt(1,1,0,1) = 0. phsumpt(1,1,1,0) = 0. phsumpt(1,1,1,1) = 0. phtxtequiv(0,0,0,0) = 0. phtxtequiv(0,0,0,1) = 0. phtxtequiv(0,0,1,0) = 0. phtxtequiv(0,0,1,1) = 0. phtxtequiv(0,1,0,0) = 0. phtxtequiv(0,1,0,1) = 0. phtxtequiv(0,1,1,0) = 0. phtxtequiv(0,1,1,1) = 0. phtxtequiv(1,0,0,0) = 0. phtxtequiv(1,0,0,1) = 0. phtxtequiv(1,0,1,0) = 0. phtxtequiv(1,0,1,1) = 0. phtxtequiv(1,1,0,0) = 0. phtxtequiv(1,1,0,1) = 0. phtxtequiv(1,1,1,0) = 0. phtxtequiv(1,1,1,1) = 0. sumpt(0,0,0,0) = 0. sumpt(0,0,0,1) = 0. sumpt(0,0,1,0) = 0. sumpt(0,0,1,1) = 0. sumpt(0,1,0,0) = 0. sumpt(0,1,0,1) = 0. sumpt(0,1,1,0) = 0. sumpt(0,1,1,1) = 0. sumpt(1,0,0,0) = 0. sumpt(1,0,0,1) = 0. sumpt(1,0,1,0) = 0. sumpt(1,0,1,1) = 0. sumpt(1,1,0,0) = 0. sumpt(1,1,0,1) = 0. sumpt(1,1,1,0) = 0. sumpt(1,1,1,1) = 0. txtsumpt(0,0,0,0) = 0. txtsumpt(0,0,0,1) = 0. txtsumpt(0,0,1,0) = 0. txtsumpt(0,0,1,1) = 0. txtsumpt(0,1,0,0) = 0. txtsumpt(0,1,0,1) = 0. txtsumpt(0,1,1,0) = 0. txtsumpt(0,1,1,1) = 0. txtsumpt(1,0,0,0) = 0. txtsumpt(1,0,0,1) = 0. txtsumpt(1,0,1,0) = 0. txtsumpt(1,0,1,1) = 0. txtsumpt(1,1,0,0) = 0. txtsumpt(1,1,0,1) = 0. txtsumpt(1,1,1,0) = 0. txtsumpt(1,1,1,1) = 0. % SZS output end FiniteModel ------ process 25569 exit (max_models) ------ User_CPU=0.02, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 25569 exit (max_models) Wed May 18 05:16:17 2016 The process finished Wed May 18 05:16:17 2016 Mace4 ended % END OF SYSTEM OUTPUT % RESULT: SOT_LO76yo - Mace4---1109a says Satisfiable - CPU = 0.00 WC = 0.38 % OUTPUT: SOT_LO76yo - Mace4---1109a says FiniteModel - CPU = 0.00 WC = 0.38