%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO221+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:36 EDT 2024
% Result : Theorem 25.22s 25.42s
% Output : Refutation 25.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO221+3 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 08:38:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 25.22/25.42 % Version: 1.5
% 25.22/25.42 % SZS status Theorem
% 25.22/25.42 % SZS output start CNFRefutation
% 25.22/25.42 fof(ooc1,axiom,(![A]:(![L]:(~unorthogonal_lines(orthogonal_through_point(L,A),L)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 25.22/25.42 fof(c77,plain,(![A]:(![L]:~unorthogonal_lines(orthogonal_through_point(L,A),L))),inference(fof_simplification,[status(thm)],[ooc1])).
% 25.22/25.42 fof(c78,plain,(![X47]:(![X48]:~unorthogonal_lines(orthogonal_through_point(X48,X47),X48))),inference(variable_rename,[status(thm)],[c77])).
% 25.22/25.42 cnf(c79,plain,~unorthogonal_lines(orthogonal_through_point(X102,X101),X102),inference(split_conjunct,[status(thm)],[c78])).
% 25.22/25.42 fof(apart3,axiom,(![X]:(~convergent_lines(X,X))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', apart3)).
% 25.22/25.42 fof(c152,plain,(![X]:~convergent_lines(X,X)),inference(fof_simplification,[status(thm)],[apart3])).
% 25.22/25.42 fof(c153,plain,(![X93]:~convergent_lines(X93,X93)),inference(variable_rename,[status(thm)],[c152])).
% 25.22/25.42 cnf(c154,plain,~convergent_lines(X96,X96),inference(split_conjunct,[status(thm)],[c153])).
% 25.22/25.42 fof(a5,axiom,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>(~unorthogonal_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a5)).
% 25.22/25.42 fof(c6,plain,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>~unorthogonal_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5])).
% 25.22/25.42 fof(c7,plain,(![X]:(![Y]:((~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))&(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c6])).
% 25.22/25.42 fof(c8,plain,((![X]:(![Y]:(~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))))&(![X]:(![Y]:(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c7])).
% 25.22/25.42 fof(c10,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~orthogonal_lines(X5,X6)|~unorthogonal_lines(X5,X6))&(unorthogonal_lines(X7,X8)|orthogonal_lines(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,((![X5]:(![X6]:(~orthogonal_lines(X5,X6)|~unorthogonal_lines(X5,X6))))&(![X7]:(![X8]:(unorthogonal_lines(X7,X8)|orthogonal_lines(X7,X8))))),inference(variable_rename,[status(thm)],[c8])).])).
% 25.22/25.42 cnf(c12,plain,unorthogonal_lines(X109,X110)|orthogonal_lines(X109,X110),inference(split_conjunct,[status(thm)],[c10])).
% 25.22/25.42 fof(cotno1,axiom,(![L]:(![M]:(![N]:((((~convergent_lines(L,M))|(~unorthogonal_lines(L,M)))&((~convergent_lines(L,N))|(~unorthogonal_lines(L,N))))=>((~convergent_lines(M,N))|(~unorthogonal_lines(M,N))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+4.ax', cotno1)).
% 25.22/25.42 fof(c57,plain,(![L]:(![M]:(![N]:(((~convergent_lines(L,M)|~unorthogonal_lines(L,M))&(~convergent_lines(L,N)|~unorthogonal_lines(L,N)))=>(~convergent_lines(M,N)|~unorthogonal_lines(M,N)))))),inference(fof_simplification,[status(thm)],[cotno1])).
% 25.22/25.42 fof(c58,plain,(![L]:(![M]:(![N]:(((convergent_lines(L,M)&unorthogonal_lines(L,M))|(convergent_lines(L,N)&unorthogonal_lines(L,N)))|(~convergent_lines(M,N)|~unorthogonal_lines(M,N)))))),inference(fof_nnf,[status(thm)],[c57])).
% 25.22/25.42 fof(c59,plain,(![X36]:(![X37]:(![X38]:(((convergent_lines(X36,X37)&unorthogonal_lines(X36,X37))|(convergent_lines(X36,X38)&unorthogonal_lines(X36,X38)))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))))),inference(variable_rename,[status(thm)],[c58])).
% 25.22/25.42 fof(c60,plain,(![X36]:(![X37]:(![X38]:((((convergent_lines(X36,X37)|convergent_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))&((convergent_lines(X36,X37)|unorthogonal_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38))))&(((unorthogonal_lines(X36,X37)|convergent_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))&((unorthogonal_lines(X36,X37)|unorthogonal_lines(X36,X38))|(~convergent_lines(X37,X38)|~unorthogonal_lines(X37,X38)))))))),inference(distribute,[status(thm)],[c59])).
% 25.22/25.42 cnf(c63,plain,unorthogonal_lines(X227,X229)|convergent_lines(X227,X228)|~convergent_lines(X229,X228)|~unorthogonal_lines(X229,X228),inference(split_conjunct,[status(thm)],[c60])).
% 25.22/25.42 cnf(c232,plain,unorthogonal_lines(X813,X815)|convergent_lines(X813,X814)|~convergent_lines(X815,X814)|orthogonal_lines(X815,X814),inference(resolution,[status(thm)],[c63, c12])).
% 25.22/25.42 fof(a3,axiom,(![X]:(![Y]:(parallel_lines(X,Y)<=>(~convergent_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', a3)).
% 25.22/25.42 fof(c20,plain,(![X]:(![Y]:(parallel_lines(X,Y)<=>~convergent_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a3])).
% 25.22/25.42 fof(c21,plain,(![X]:(![Y]:((~parallel_lines(X,Y)|~convergent_lines(X,Y))&(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c20])).
% 25.22/25.42 fof(c22,plain,((![X]:(![Y]:(~parallel_lines(X,Y)|~convergent_lines(X,Y))))&(![X]:(![Y]:(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c21])).
% 25.22/25.42 fof(c24,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~parallel_lines(X13,X14)|~convergent_lines(X13,X14))&(convergent_lines(X15,X16)|parallel_lines(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X13]:(![X14]:(~parallel_lines(X13,X14)|~convergent_lines(X13,X14))))&(![X15]:(![X16]:(convergent_lines(X15,X16)|parallel_lines(X15,X16))))),inference(variable_rename,[status(thm)],[c22])).])).
% 25.22/25.42 cnf(c25,plain,~parallel_lines(X122,X121)|~convergent_lines(X122,X121),inference(split_conjunct,[status(thm)],[c24])).
% 25.22/25.42 fof(coipo1,axiom,(![L]:(![M]:(~((~convergent_lines(L,M))&(~unorthogonal_lines(L,M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+4.ax', coipo1)).
% 25.22/25.42 fof(c65,plain,(![L]:(![M]:(~(~convergent_lines(L,M)&~unorthogonal_lines(L,M))))),inference(fof_simplification,[status(thm)],[coipo1])).
% 25.22/25.42 fof(c66,plain,(![L]:(![M]:(convergent_lines(L,M)|unorthogonal_lines(L,M)))),inference(fof_nnf,[status(thm)],[c65])).
% 25.22/25.42 fof(c67,plain,(![X39]:(![X40]:(convergent_lines(X39,X40)|unorthogonal_lines(X39,X40)))),inference(variable_rename,[status(thm)],[c66])).
% 25.22/25.42 cnf(c68,plain,convergent_lines(X139,X138)|unorthogonal_lines(X139,X138),inference(split_conjunct,[status(thm)],[c67])).
% 25.22/25.42 cnf(c174,plain,unorthogonal_lines(X176,X175)|~parallel_lines(X176,X175),inference(resolution,[status(thm)],[c68, c25])).
% 25.22/25.42 fof(p1,axiom,(![X]:(![Y]:(distinct_lines(X,Y)=>convergent_lines(X,Y)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+1.ax', p1)).
% 25.22/25.42 fof(c100,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|convergent_lines(X,Y)))),inference(fof_nnf,[status(thm)],[p1])).
% 25.22/25.42 fof(c101,plain,(![X61]:(![X62]:(~distinct_lines(X61,X62)|convergent_lines(X61,X62)))),inference(variable_rename,[status(thm)],[c100])).
% 25.22/25.42 cnf(c102,plain,~distinct_lines(X162,X161)|convergent_lines(X162,X161),inference(split_conjunct,[status(thm)],[c101])).
% 25.22/25.42 cnf(c26,plain,convergent_lines(X124,X123)|parallel_lines(X124,X123),inference(split_conjunct,[status(thm)],[c24])).
% 25.22/25.42 fof(ceq3,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 25.22/25.42 fof(c103,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq3])).
% 25.22/25.42 fof(c104,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(shift_quantors,[status(thm)],[c103])).
% 25.22/25.42 fof(c106,plain,(![X63]:(![X64]:(![X65]:(~convergent_lines(X63,X64)|(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(shift_quantors,[status(thm)],[fof(c105,plain,(![X63]:(![X64]:(~convergent_lines(X63,X64)|(![X65]:(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(variable_rename,[status(thm)],[c104])).])).
% 25.22/25.42 cnf(c107,plain,~convergent_lines(X337,X339)|distinct_lines(X339,X338)|convergent_lines(X337,X338),inference(split_conjunct,[status(thm)],[c106])).
% 25.22/25.42 cnf(c320,plain,distinct_lines(X760,X759)|convergent_lines(X761,X759)|parallel_lines(X761,X760),inference(resolution,[status(thm)],[c107, c26])).
% 25.22/25.42 cnf(c765,plain,distinct_lines(X769,X768)|parallel_lines(X768,X769),inference(resolution,[status(thm)],[c320, c154])).
% 25.22/25.42 cnf(c790,plain,parallel_lines(X780,X779)|convergent_lines(X779,X780),inference(resolution,[status(thm)],[c765, c102])).
% 25.22/25.42 cnf(c817,plain,convergent_lines(X841,X842)|unorthogonal_lines(X842,X841),inference(resolution,[status(thm)],[c790, c174])).
% 25.22/25.42 cnf(c962,plain,unorthogonal_lines(X8709,X8708)|unorthogonal_lines(X8707,X8708)|convergent_lines(X8707,X8709)|orthogonal_lines(X8708,X8709),inference(resolution,[status(thm)],[c817, c232])).
% 25.22/25.42 cnf(c53498,plain,unorthogonal_lines(X8710,X8711)|orthogonal_lines(X8711,X8710),inference(resolution,[status(thm)],[c962, c154])).
% 25.22/25.42 cnf(c53621,plain,orthogonal_lines(X8713,orthogonal_through_point(X8713,X8714)),inference(resolution,[status(thm)],[c53498, c79])).
% 25.22/25.42 cnf(c11,plain,~orthogonal_lines(X108,X107)|~unorthogonal_lines(X108,X107),inference(split_conjunct,[status(thm)],[c10])).
% 25.22/25.42 fof(con,conjecture,(![A]:(![B]:(![L]:(incident_point_and_line(B,orthogonal_through_point(L,A))=>equal_lines(orthogonal_through_point(L,A),orthogonal_through_point(L,B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 25.22/25.42 fof(c0,negated_conjecture,(~(![A]:(![B]:(![L]:(incident_point_and_line(B,orthogonal_through_point(L,A))=>equal_lines(orthogonal_through_point(L,A),orthogonal_through_point(L,B))))))),inference(assume_negation,[status(cth)],[con])).
% 25.22/25.42 fof(c1,negated_conjecture,(?[A]:(?[B]:(?[L]:(incident_point_and_line(B,orthogonal_through_point(L,A))&~equal_lines(orthogonal_through_point(L,A),orthogonal_through_point(L,B)))))),inference(fof_nnf,[status(thm)],[c0])).
% 25.22/25.42 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(incident_point_and_line(X3,orthogonal_through_point(X4,X2))&~equal_lines(orthogonal_through_point(X4,X2),orthogonal_through_point(X4,X3)))))),inference(variable_rename,[status(thm)],[c1])).
% 25.22/25.42 fof(c3,negated_conjecture,(incident_point_and_line(skolem0002,orthogonal_through_point(skolem0003,skolem0001))&~equal_lines(orthogonal_through_point(skolem0003,skolem0001),orthogonal_through_point(skolem0003,skolem0002))),inference(skolemize,[status(esa)],[c2])).
% 25.22/25.42 cnf(c5,negated_conjecture,~equal_lines(orthogonal_through_point(skolem0003,skolem0001),orthogonal_through_point(skolem0003,skolem0002)),inference(split_conjunct,[status(thm)],[c3])).
% 25.22/25.42 fof(ax2,axiom,(![X]:(![Y]:(equal_lines(X,Y)<=>(~distinct_lines(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+6.ax', ax2)).
% 25.22/25.42 fof(c27,plain,(![X]:(![Y]:(equal_lines(X,Y)<=>~distinct_lines(X,Y)))),inference(fof_simplification,[status(thm)],[ax2])).
% 25.22/25.42 fof(c28,plain,(![X]:(![Y]:((~equal_lines(X,Y)|~distinct_lines(X,Y))&(distinct_lines(X,Y)|equal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c27])).
% 25.22/25.42 fof(c29,plain,((![X]:(![Y]:(~equal_lines(X,Y)|~distinct_lines(X,Y))))&(![X]:(![Y]:(distinct_lines(X,Y)|equal_lines(X,Y))))),inference(shift_quantors,[status(thm)],[c28])).
% 25.22/25.42 fof(c31,plain,(![X17]:(![X18]:(![X19]:(![X20]:((~equal_lines(X17,X18)|~distinct_lines(X17,X18))&(distinct_lines(X19,X20)|equal_lines(X19,X20))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X17]:(![X18]:(~equal_lines(X17,X18)|~distinct_lines(X17,X18))))&(![X19]:(![X20]:(distinct_lines(X19,X20)|equal_lines(X19,X20))))),inference(variable_rename,[status(thm)],[c29])).])).
% 25.22/25.42 cnf(c33,plain,distinct_lines(X130,X131)|equal_lines(X130,X131),inference(split_conjunct,[status(thm)],[c31])).
% 25.22/25.42 cnf(c185,plain,convergent_lines(X187,X186)|equal_lines(X187,X186),inference(resolution,[status(thm)],[c102, c33])).
% 25.22/25.42 fof(couo1,axiom,(![L]:(![M]:(![N]:(((~unorthogonal_lines(L,M))&(~unorthogonal_lines(L,N)))=>(~convergent_lines(M,N)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO006+4.ax', couo1)).
% 25.22/25.42 fof(c53,plain,(![L]:(![M]:(![N]:((~unorthogonal_lines(L,M)&~unorthogonal_lines(L,N))=>~convergent_lines(M,N))))),inference(fof_simplification,[status(thm)],[couo1])).
% 25.22/25.42 fof(c54,plain,(![L]:(![M]:(![N]:((unorthogonal_lines(L,M)|unorthogonal_lines(L,N))|~convergent_lines(M,N))))),inference(fof_nnf,[status(thm)],[c53])).
% 25.22/25.42 fof(c55,plain,(![X33]:(![X34]:(![X35]:((unorthogonal_lines(X33,X34)|unorthogonal_lines(X33,X35))|~convergent_lines(X34,X35))))),inference(variable_rename,[status(thm)],[c54])).
% 25.22/25.42 cnf(c56,plain,unorthogonal_lines(X189,X188)|unorthogonal_lines(X189,X190)|~convergent_lines(X188,X190),inference(split_conjunct,[status(thm)],[c55])).
% 25.22/25.42 cnf(c202,plain,unorthogonal_lines(X557,X559)|unorthogonal_lines(X557,X558)|equal_lines(X559,X558),inference(resolution,[status(thm)],[c56, c185])).
% 25.22/25.42 cnf(c534,plain,unorthogonal_lines(X3927,X3928)|equal_lines(X3928,X3926)|~orthogonal_lines(X3927,X3926),inference(resolution,[status(thm)],[c202, c11])).
% 25.22/25.42 cnf(c53677,plain,unorthogonal_lines(X9145,X9144)|equal_lines(X9144,orthogonal_through_point(X9145,X9143)),inference(resolution,[status(thm)],[c53621, c534])).
% 25.22/25.42 cnf(c56886,plain,unorthogonal_lines(skolem0003,orthogonal_through_point(skolem0003,skolem0001)),inference(resolution,[status(thm)],[c53677, c5])).
% 25.22/25.42 cnf(c56951,plain,~orthogonal_lines(skolem0003,orthogonal_through_point(skolem0003,skolem0001)),inference(resolution,[status(thm)],[c56886, c11])).
% 25.22/25.42 cnf(c56959,plain,$false,inference(resolution,[status(thm)],[c56951, c53621])).
% 25.22/25.42 % SZS output end CNFRefutation
% 25.22/25.42
% 25.22/25.42 % Initial clauses : 48
% 25.22/25.42 % Processed clauses : 824
% 25.22/25.42 % Factors computed : 145
% 25.22/25.42 % Resolvents computed: 56671
% 25.22/25.42 % Tautologies deleted: 12
% 25.22/25.42 % Forward subsumed : 2430
% 25.22/25.42 % Backward subsumed : 87
% 25.22/25.42 % -------- CPU Time ---------
% 25.22/25.42 % User time : 24.950 s
% 25.22/25.42 % System time : 0.129 s
% 25.22/25.42 % Total time : 25.079 s
%------------------------------------------------------------------------------