%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO117+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:21:06 EDT 2024
% Result : Theorem 60.75s 60.95s
% Output : Refutation 60.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO117+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n008.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 08:30:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 60.75/60.95 % Version: 1.5
% 60.75/60.95 % SZS status Theorem
% 60.75/60.95 % SZS output start CNFRefutation
% 60.75/60.95 cnf(reflexivity,axiom,X148=X148,theory(equality)).
% 60.75/60.95 fof(between_c_defn,axiom,(![C]:(![P]:(![Q]:(![R]:(between_c(C,P,Q,R)<=>(P!=R&(?[Cpp]:(((part_of(Cpp,C)&end_point(P,Cpp))&end_point(R,Cpp))&inner_point(Q,Cpp))))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+1.ax', between_c_defn)).
% 60.75/60.95 fof(c106,plain,(![C]:(![P]:(![Q]:(![R]:((~between_c(C,P,Q,R)|(P!=R&(?[Cpp]:(((part_of(Cpp,C)&end_point(P,Cpp))&end_point(R,Cpp))&inner_point(Q,Cpp)))))&((P=R|(![Cpp]:(((~part_of(Cpp,C)|~end_point(P,Cpp))|~end_point(R,Cpp))|~inner_point(Q,Cpp))))|between_c(C,P,Q,R))))))),inference(fof_nnf,[status(thm)],[between_c_defn])).
% 60.75/60.95 fof(c107,plain,((![C]:(![P]:(![Q]:(![R]:(~between_c(C,P,Q,R)|(P!=R&(?[Cpp]:(((part_of(Cpp,C)&end_point(P,Cpp))&end_point(R,Cpp))&inner_point(Q,Cpp)))))))))&(![C]:(![P]:(![Q]:(![R]:((P=R|(![Cpp]:(((~part_of(Cpp,C)|~end_point(P,Cpp))|~end_point(R,Cpp))|~inner_point(Q,Cpp))))|between_c(C,P,Q,R))))))),inference(shift_quantors,[status(thm)],[c106])).
% 60.75/60.95 fof(c108,plain,((![X63]:(![X64]:(![X65]:(![X66]:(~between_c(X63,X64,X65,X66)|(X64!=X66&(?[X67]:(((part_of(X67,X63)&end_point(X64,X67))&end_point(X66,X67))&inner_point(X65,X67)))))))))&(![X68]:(![X69]:(![X70]:(![X71]:((X69=X71|(![X72]:(((~part_of(X72,X68)|~end_point(X69,X72))|~end_point(X71,X72))|~inner_point(X70,X72))))|between_c(X68,X69,X70,X71))))))),inference(variable_rename,[status(thm)],[c107])).
% 60.75/60.95 fof(c110,plain,(![X63]:(![X64]:(![X65]:(![X66]:(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:((~between_c(X63,X64,X65,X66)|(X64!=X66&(((part_of(skolem0013(X63,X64,X65,X66),X63)&end_point(X64,skolem0013(X63,X64,X65,X66)))&end_point(X66,skolem0013(X63,X64,X65,X66)))&inner_point(X65,skolem0013(X63,X64,X65,X66)))))&((X69=X71|(((~part_of(X72,X68)|~end_point(X69,X72))|~end_point(X71,X72))|~inner_point(X70,X72)))|between_c(X68,X69,X70,X71)))))))))))),inference(shift_quantors,[status(thm)],[fof(c109,plain,((![X63]:(![X64]:(![X65]:(![X66]:(~between_c(X63,X64,X65,X66)|(X64!=X66&(((part_of(skolem0013(X63,X64,X65,X66),X63)&end_point(X64,skolem0013(X63,X64,X65,X66)))&end_point(X66,skolem0013(X63,X64,X65,X66)))&inner_point(X65,skolem0013(X63,X64,X65,X66)))))))))&(![X68]:(![X69]:(![X70]:(![X71]:((X69=X71|(![X72]:(((~part_of(X72,X68)|~end_point(X69,X72))|~end_point(X71,X72))|~inner_point(X70,X72))))|between_c(X68,X69,X70,X71))))))),inference(skolemize,[status(esa)],[c108])).])).
% 60.75/60.95 fof(c111,plain,(![X63]:(![X64]:(![X65]:(![X66]:(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(((~between_c(X63,X64,X65,X66)|X64!=X66)&((((~between_c(X63,X64,X65,X66)|part_of(skolem0013(X63,X64,X65,X66),X63))&(~between_c(X63,X64,X65,X66)|end_point(X64,skolem0013(X63,X64,X65,X66))))&(~between_c(X63,X64,X65,X66)|end_point(X66,skolem0013(X63,X64,X65,X66))))&(~between_c(X63,X64,X65,X66)|inner_point(X65,skolem0013(X63,X64,X65,X66)))))&((X69=X71|(((~part_of(X72,X68)|~end_point(X69,X72))|~end_point(X71,X72))|~inner_point(X70,X72)))|between_c(X68,X69,X70,X71)))))))))))),inference(distribute,[status(thm)],[c110])).
% 60.75/60.95 cnf(c112,plain,~between_c(X245,X242,X243,X244)|X242!=X244,inference(split_conjunct,[status(thm)],[c111])).
% 60.75/60.95 fof(o3,axiom,(![P]:(![Q]:(![R]:(![O]:(between_o(O,P,Q,R)<=>(?[C]:((![P]:(incident_o(P,O)<=>incident_c(P,C)))&between_c(C,P,Q,R)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax', o3)).
% 60.75/60.95 fof(c49,plain,(![P]:(![Q]:(![R]:(![O]:((~between_o(O,P,Q,R)|(?[C]:((![P]:((~incident_o(P,O)|incident_c(P,C))&(~incident_c(P,C)|incident_o(P,O))))&between_c(C,P,Q,R))))&((![C]:((?[P]:((~incident_o(P,O)|~incident_c(P,C))&(incident_o(P,O)|incident_c(P,C))))|~between_c(C,P,Q,R)))|between_o(O,P,Q,R))))))),inference(fof_nnf,[status(thm)],[o3])).
% 60.75/60.95 fof(c50,plain,((![P]:(![Q]:(![R]:(![O]:(~between_o(O,P,Q,R)|(?[C]:(((![P]:(~incident_o(P,O)|incident_c(P,C)))&(![P]:(~incident_c(P,C)|incident_o(P,O))))&between_c(C,P,Q,R))))))))&(![P]:(![Q]:(![R]:(![O]:((![C]:((?[P]:((~incident_o(P,O)|~incident_c(P,C))&(incident_o(P,O)|incident_c(P,C))))|~between_c(C,P,Q,R)))|between_o(O,P,Q,R))))))),inference(shift_quantors,[status(thm)],[c49])).
% 60.75/60.95 fof(c51,plain,((![X23]:(![X24]:(![X25]:(![X26]:(~between_o(X26,X23,X24,X25)|(?[X27]:(((![X28]:(~incident_o(X28,X26)|incident_c(X28,X27)))&(![X29]:(~incident_c(X29,X27)|incident_o(X29,X26))))&between_c(X27,X23,X24,X25))))))))&(![X30]:(![X31]:(![X32]:(![X33]:((![X34]:((?[X35]:((~incident_o(X35,X33)|~incident_c(X35,X34))&(incident_o(X35,X33)|incident_c(X35,X34))))|~between_c(X34,X30,X31,X32)))|between_o(X33,X30,X31,X32))))))),inference(variable_rename,[status(thm)],[c50])).
% 60.75/60.95 fof(c53,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((~between_o(X26,X23,X24,X25)|(((~incident_o(X28,X26)|incident_c(X28,skolem0008(X23,X24,X25,X26)))&(~incident_c(X29,skolem0008(X23,X24,X25,X26))|incident_o(X29,X26)))&between_c(skolem0008(X23,X24,X25,X26),X23,X24,X25)))&((((~incident_o(skolem0009(X30,X31,X32,X33,X34),X33)|~incident_c(skolem0009(X30,X31,X32,X33,X34),X34))&(incident_o(skolem0009(X30,X31,X32,X33,X34),X33)|incident_c(skolem0009(X30,X31,X32,X33,X34),X34)))|~between_c(X34,X30,X31,X32))|between_o(X33,X30,X31,X32)))))))))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X23]:(![X24]:(![X25]:(![X26]:(~between_o(X26,X23,X24,X25)|(((![X28]:(~incident_o(X28,X26)|incident_c(X28,skolem0008(X23,X24,X25,X26))))&(![X29]:(~incident_c(X29,skolem0008(X23,X24,X25,X26))|incident_o(X29,X26))))&between_c(skolem0008(X23,X24,X25,X26),X23,X24,X25)))))))&(![X30]:(![X31]:(![X32]:(![X33]:((![X34]:(((~incident_o(skolem0009(X30,X31,X32,X33,X34),X33)|~incident_c(skolem0009(X30,X31,X32,X33,X34),X34))&(incident_o(skolem0009(X30,X31,X32,X33,X34),X33)|incident_c(skolem0009(X30,X31,X32,X33,X34),X34)))|~between_c(X34,X30,X31,X32)))|between_o(X33,X30,X31,X32))))))),inference(skolemize,[status(esa)],[c51])).])).
% 60.75/60.95 fof(c54,plain,(![X23]:(![X24]:(![X25]:(![X26]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((((~between_o(X26,X23,X24,X25)|(~incident_o(X28,X26)|incident_c(X28,skolem0008(X23,X24,X25,X26))))&(~between_o(X26,X23,X24,X25)|(~incident_c(X29,skolem0008(X23,X24,X25,X26))|incident_o(X29,X26))))&(~between_o(X26,X23,X24,X25)|between_c(skolem0008(X23,X24,X25,X26),X23,X24,X25)))&((((~incident_o(skolem0009(X30,X31,X32,X33,X34),X33)|~incident_c(skolem0009(X30,X31,X32,X33,X34),X34))|~between_c(X34,X30,X31,X32))|between_o(X33,X30,X31,X32))&(((incident_o(skolem0009(X30,X31,X32,X33,X34),X33)|incident_c(skolem0009(X30,X31,X32,X33,X34),X34))|~between_c(X34,X30,X31,X32))|between_o(X33,X30,X31,X32))))))))))))))),inference(distribute,[status(thm)],[c53])).
% 60.75/60.95 cnf(c57,plain,~between_o(X429,X432,X430,X431)|between_c(skolem0008(X432,X430,X431,X429),X432,X430,X431),inference(split_conjunct,[status(thm)],[c54])).
% 60.75/60.95 fof(theorem_4_4,conjecture,(![O]:(![P]:(~ordered_by(O,P,P)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', theorem_4_4)).
% 60.75/60.95 fof(c15,negated_conjecture,(~(![O]:(![P]:(~ordered_by(O,P,P))))),inference(assume_negation,[status(cth)],[theorem_4_4])).
% 60.75/60.95 fof(c16,negated_conjecture,(~(![O]:(![P]:~ordered_by(O,P,P)))),inference(fof_simplification,[status(thm)],[c15])).
% 60.75/60.95 fof(c17,negated_conjecture,(?[O]:(?[P]:ordered_by(O,P,P))),inference(fof_nnf,[status(thm)],[c16])).
% 60.75/60.95 fof(c18,negated_conjecture,(?[X2]:(?[X3]:ordered_by(X2,X3,X3))),inference(variable_rename,[status(thm)],[c17])).
% 60.75/60.95 fof(c19,negated_conjecture,ordered_by(skolem0001,skolem0002,skolem0002),inference(skolemize,[status(esa)],[c18])).
% 60.75/60.95 cnf(c20,negated_conjecture,ordered_by(skolem0001,skolem0002,skolem0002),inference(split_conjunct,[status(thm)],[c19])).
% 60.75/60.95 fof(between_o_defn,axiom,(![O]:(![P]:(![Q]:(![R]:(between_o(O,P,Q,R)<=>((ordered_by(O,P,Q)&ordered_by(O,Q,R))|(ordered_by(O,R,Q)&ordered_by(O,Q,P)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+2.ax', between_o_defn)).
% 60.75/60.95 fof(c95,plain,(![O]:(![P]:(![Q]:(![R]:((~between_o(O,P,Q,R)|((ordered_by(O,P,Q)&ordered_by(O,Q,R))|(ordered_by(O,R,Q)&ordered_by(O,Q,P))))&(((~ordered_by(O,P,Q)|~ordered_by(O,Q,R))&(~ordered_by(O,R,Q)|~ordered_by(O,Q,P)))|between_o(O,P,Q,R))))))),inference(fof_nnf,[status(thm)],[between_o_defn])).
% 60.75/60.95 fof(c96,plain,((![O]:(![P]:(![Q]:(![R]:(~between_o(O,P,Q,R)|((ordered_by(O,P,Q)&ordered_by(O,Q,R))|(ordered_by(O,R,Q)&ordered_by(O,Q,P))))))))&(![O]:(![P]:(![Q]:(![R]:(((~ordered_by(O,P,Q)|~ordered_by(O,Q,R))&(~ordered_by(O,R,Q)|~ordered_by(O,Q,P)))|between_o(O,P,Q,R))))))),inference(shift_quantors,[status(thm)],[c95])).
% 60.75/60.95 fof(c98,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:((~between_o(X55,X56,X57,X58)|((ordered_by(X55,X56,X57)&ordered_by(X55,X57,X58))|(ordered_by(X55,X58,X57)&ordered_by(X55,X57,X56))))&(((~ordered_by(X59,X60,X61)|~ordered_by(X59,X61,X62))&(~ordered_by(X59,X62,X61)|~ordered_by(X59,X61,X60)))|between_o(X59,X60,X61,X62))))))))))),inference(shift_quantors,[status(thm)],[fof(c97,plain,((![X55]:(![X56]:(![X57]:(![X58]:(~between_o(X55,X56,X57,X58)|((ordered_by(X55,X56,X57)&ordered_by(X55,X57,X58))|(ordered_by(X55,X58,X57)&ordered_by(X55,X57,X56))))))))&(![X59]:(![X60]:(![X61]:(![X62]:(((~ordered_by(X59,X60,X61)|~ordered_by(X59,X61,X62))&(~ordered_by(X59,X62,X61)|~ordered_by(X59,X61,X60)))|between_o(X59,X60,X61,X62))))))),inference(variable_rename,[status(thm)],[c96])).])).
% 60.75/60.95 fof(c99,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:((((~between_o(X55,X56,X57,X58)|(ordered_by(X55,X56,X57)|ordered_by(X55,X58,X57)))&(~between_o(X55,X56,X57,X58)|(ordered_by(X55,X56,X57)|ordered_by(X55,X57,X56))))&((~between_o(X55,X56,X57,X58)|(ordered_by(X55,X57,X58)|ordered_by(X55,X58,X57)))&(~between_o(X55,X56,X57,X58)|(ordered_by(X55,X57,X58)|ordered_by(X55,X57,X56)))))&(((~ordered_by(X59,X60,X61)|~ordered_by(X59,X61,X62))|between_o(X59,X60,X61,X62))&((~ordered_by(X59,X62,X61)|~ordered_by(X59,X61,X60))|between_o(X59,X60,X61,X62)))))))))))),inference(distribute,[status(thm)],[c98])).
% 60.75/60.95 cnf(c104,plain,~ordered_by(X601,X602,X600)|~ordered_by(X601,X600,X603)|between_o(X601,X602,X600,X603),inference(split_conjunct,[status(thm)],[c99])).
% 60.75/60.95 cnf(c998,plain,~ordered_by(X607,X606,X606)|between_o(X607,X606,X606,X606),inference(factor,[status(thm)],[c104])).
% 60.75/60.95 cnf(c1002,plain,between_o(skolem0001,skolem0002,skolem0002,skolem0002),inference(resolution,[status(thm)],[c998, c20])).
% 60.75/60.95 cnf(c1007,plain,between_c(skolem0008(skolem0002,skolem0002,skolem0002,skolem0001),skolem0002,skolem0002,skolem0002),inference(resolution,[status(thm)],[c1002, c57])).
% 60.75/60.95 cnf(c83992,plain,skolem0002!=skolem0002,inference(resolution,[status(thm)],[c1007, c112])).
% 60.75/60.95 cnf(c84005,plain,$false,inference(resolution,[status(thm)],[c83992, reflexivity])).
% 60.75/60.95 % SZS output end CNFRefutation
% 60.75/60.95
% 60.75/60.95 % Initial clauses : 104
% 60.75/60.95 % Processed clauses : 1418
% 60.75/60.95 % Factors computed : 135
% 60.75/60.95 % Resolvents computed: 83661
% 60.75/60.95 % Tautologies deleted: 40
% 60.75/60.95 % Forward subsumed : 2497
% 60.75/60.95 % Backward subsumed : 71
% 60.75/60.95 % -------- CPU Time ---------
% 60.75/60.95 % User time : 60.419 s
% 60.75/60.95 % System time : 0.188 s
% 60.75/60.95 % Total time : 60.607 s
%------------------------------------------------------------------------------