%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO258+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:48 EDT 2024
% Result : Theorem 0.86s 1.07s
% Output : Refutation 0.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO258+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n024.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 08:14:37 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.86/1.07 % Version: 1.5
% 0.86/1.07 % SZS status Theorem
% 0.86/1.07 % SZS output start CNFRefutation
% 0.86/1.07 fof(con,conjecture,(![L]:(![A]:(![B]:(![C]:(between_on_line(L,A,B,C)=>between_on_line(L,C,B,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 0.86/1.07 fof(c0,negated_conjecture,(~(![L]:(![A]:(![B]:(![C]:(between_on_line(L,A,B,C)=>between_on_line(L,C,B,A))))))),inference(assume_negation,[status(cth)],[con])).
% 0.86/1.07 fof(c1,negated_conjecture,(?[L]:(?[A]:(?[B]:(?[C]:(between_on_line(L,A,B,C)&~between_on_line(L,C,B,A)))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.86/1.07 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(between_on_line(X2,X3,X4,X5)&~between_on_line(X2,X5,X4,X3)))))),inference(variable_rename,[status(thm)],[c1])).
% 0.86/1.07 fof(c3,negated_conjecture,(between_on_line(skolem0001,skolem0002,skolem0003,skolem0004)&~between_on_line(skolem0001,skolem0004,skolem0003,skolem0002)),inference(skolemize,[status(esa)],[c2])).
% 0.86/1.07 cnf(c5,negated_conjecture,~between_on_line(skolem0001,skolem0004,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c3])).
% 0.86/1.07 cnf(c4,negated_conjecture,between_on_line(skolem0001,skolem0002,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c3])).
% 0.86/1.07 fof(bet_def,axiom,(![L]:(![A]:(![B]:(![C]:(between_on_line(L,A,B,C)<=>((before_on_line(L,A,B)&before_on_line(L,B,C))|(before_on_line(L,C,B)&before_on_line(L,B,A)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', bet_def)).
% 0.86/1.07 fof(c110,plain,(![L]:(![A]:(![B]:(![C]:((~between_on_line(L,A,B,C)|((before_on_line(L,A,B)&before_on_line(L,B,C))|(before_on_line(L,C,B)&before_on_line(L,B,A))))&(((~before_on_line(L,A,B)|~before_on_line(L,B,C))&(~before_on_line(L,C,B)|~before_on_line(L,B,A)))|between_on_line(L,A,B,C))))))),inference(fof_nnf,[status(thm)],[bet_def])).
% 0.86/1.07 fof(c111,plain,((![L]:(![A]:(![B]:(![C]:(~between_on_line(L,A,B,C)|((before_on_line(L,A,B)&before_on_line(L,B,C))|(before_on_line(L,C,B)&before_on_line(L,B,A))))))))&(![L]:(![A]:(![B]:(![C]:(((~before_on_line(L,A,B)|~before_on_line(L,B,C))&(~before_on_line(L,C,B)|~before_on_line(L,B,A)))|between_on_line(L,A,B,C))))))),inference(shift_quantors,[status(thm)],[c110])).
% 0.86/1.07 fof(c113,plain,(![X67]:(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:((~between_on_line(X67,X68,X69,X70)|((before_on_line(X67,X68,X69)&before_on_line(X67,X69,X70))|(before_on_line(X67,X70,X69)&before_on_line(X67,X69,X68))))&(((~before_on_line(X71,X72,X73)|~before_on_line(X71,X73,X74))&(~before_on_line(X71,X74,X73)|~before_on_line(X71,X73,X72)))|between_on_line(X71,X72,X73,X74))))))))))),inference(shift_quantors,[status(thm)],[fof(c112,plain,((![X67]:(![X68]:(![X69]:(![X70]:(~between_on_line(X67,X68,X69,X70)|((before_on_line(X67,X68,X69)&before_on_line(X67,X69,X70))|(before_on_line(X67,X70,X69)&before_on_line(X67,X69,X68))))))))&(![X71]:(![X72]:(![X73]:(![X74]:(((~before_on_line(X71,X72,X73)|~before_on_line(X71,X73,X74))&(~before_on_line(X71,X74,X73)|~before_on_line(X71,X73,X72)))|between_on_line(X71,X72,X73,X74))))))),inference(variable_rename,[status(thm)],[c111])).])).
% 0.86/1.07 fof(c114,plain,(![X67]:(![X68]:(![X69]:(![X70]:(![X71]:(![X72]:(![X73]:(![X74]:((((~between_on_line(X67,X68,X69,X70)|(before_on_line(X67,X68,X69)|before_on_line(X67,X70,X69)))&(~between_on_line(X67,X68,X69,X70)|(before_on_line(X67,X68,X69)|before_on_line(X67,X69,X68))))&((~between_on_line(X67,X68,X69,X70)|(before_on_line(X67,X69,X70)|before_on_line(X67,X70,X69)))&(~between_on_line(X67,X68,X69,X70)|(before_on_line(X67,X69,X70)|before_on_line(X67,X69,X68)))))&(((~before_on_line(X71,X72,X73)|~before_on_line(X71,X73,X74))|between_on_line(X71,X72,X73,X74))&((~before_on_line(X71,X74,X73)|~before_on_line(X71,X73,X72))|between_on_line(X71,X72,X73,X74)))))))))))),inference(distribute,[status(thm)],[c113])).
% 0.86/1.07 cnf(c115,plain,~between_on_line(X199,X197,X198,X200)|before_on_line(X199,X197,X198)|before_on_line(X199,X200,X198),inference(split_conjunct,[status(thm)],[c114])).
% 0.86/1.07 cnf(c162,plain,before_on_line(skolem0001,skolem0002,skolem0003)|before_on_line(skolem0001,skolem0004,skolem0003),inference(resolution,[status(thm)],[c115, c4])).
% 0.86/1.07 cnf(c120,plain,~before_on_line(X226,X223,X225)|~before_on_line(X226,X225,X224)|between_on_line(X226,X224,X225,X223),inference(split_conjunct,[status(thm)],[c114])).
% 0.86/1.07 cnf(c117,plain,~between_on_line(X209,X207,X208,X210)|before_on_line(X209,X208,X210)|before_on_line(X209,X210,X208),inference(split_conjunct,[status(thm)],[c114])).
% 0.86/1.07 cnf(c164,plain,before_on_line(skolem0001,skolem0003,skolem0004)|before_on_line(skolem0001,skolem0004,skolem0003),inference(resolution,[status(thm)],[c117, c4])).
% 0.86/1.07 cnf(c210,plain,before_on_line(skolem0001,skolem0004,skolem0003)|~before_on_line(skolem0001,X425,skolem0003)|between_on_line(skolem0001,skolem0004,skolem0003,X425),inference(resolution,[status(thm)],[c164, c120])).
% 0.86/1.07 cnf(c633,plain,before_on_line(skolem0001,skolem0004,skolem0003)|between_on_line(skolem0001,skolem0004,skolem0003,skolem0002),inference(resolution,[status(thm)],[c210, c162])).
% 0.86/1.07 cnf(c1074,plain,before_on_line(skolem0001,skolem0004,skolem0003),inference(resolution,[status(thm)],[c633, c5])).
% 0.86/1.07 cnf(c119,plain,~before_on_line(X218,X216,X217)|~before_on_line(X218,X217,X215)|between_on_line(X218,X216,X217,X215),inference(split_conjunct,[status(thm)],[c114])).
% 0.86/1.07 cnf(c116,plain,~between_on_line(X205,X203,X204,X206)|before_on_line(X205,X203,X204)|before_on_line(X205,X204,X203),inference(split_conjunct,[status(thm)],[c114])).
% 0.86/1.07 cnf(c163,plain,before_on_line(skolem0001,skolem0002,skolem0003)|before_on_line(skolem0001,skolem0003,skolem0002),inference(resolution,[status(thm)],[c116, c4])).
% 0.86/1.07 cnf(c118,plain,~between_on_line(X213,X211,X212,X214)|before_on_line(X213,X212,X214)|before_on_line(X213,X212,X211),inference(split_conjunct,[status(thm)],[c114])).
% 0.86/1.07 cnf(c165,plain,before_on_line(skolem0001,skolem0003,skolem0004)|before_on_line(skolem0001,skolem0003,skolem0002),inference(resolution,[status(thm)],[c118, c4])).
% 0.86/1.07 cnf(c230,plain,before_on_line(skolem0001,skolem0003,skolem0002)|~before_on_line(skolem0001,X523,skolem0003)|between_on_line(skolem0001,skolem0004,skolem0003,X523),inference(resolution,[status(thm)],[c165, c120])).
% 0.86/1.07 cnf(c775,plain,before_on_line(skolem0001,skolem0003,skolem0002)|between_on_line(skolem0001,skolem0004,skolem0003,skolem0002),inference(resolution,[status(thm)],[c230, c163])).
% 0.86/1.07 cnf(c1154,plain,before_on_line(skolem0001,skolem0003,skolem0002),inference(resolution,[status(thm)],[c775, c5])).
% 0.86/1.07 cnf(c1160,plain,~before_on_line(skolem0001,X841,skolem0003)|between_on_line(skolem0001,X841,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1154, c119])).
% 0.86/1.07 cnf(c1173,plain,between_on_line(skolem0001,skolem0004,skolem0003,skolem0002),inference(resolution,[status(thm)],[c1160, c1074])).
% 0.86/1.07 cnf(c1176,plain,$false,inference(resolution,[status(thm)],[c1173, c5])).
% 0.86/1.07 % SZS output end CNFRefutation
% 0.86/1.07
% 0.86/1.07 % Initial clauses : 60
% 0.86/1.07 % Processed clauses : 153
% 0.86/1.07 % Factors computed : 150
% 0.86/1.07 % Resolvents computed: 869
% 0.86/1.07 % Tautologies deleted: 0
% 0.86/1.07 % Forward subsumed : 418
% 0.86/1.07 % Backward subsumed : 44
% 0.86/1.07 % -------- CPU Time ---------
% 0.86/1.07 % User time : 0.714 s
% 0.86/1.07 % System time : 0.010 s
% 0.86/1.07 % Total time : 0.724 s
%------------------------------------------------------------------------------