%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO210+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:31 EDT 2024
% Result : Theorem 31.71s 31.91s
% Output : Refutation 31.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO210+3 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n019.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 07:48:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 31.71/31.91 % Version: 1.5
% 31.71/31.91 % SZS status Theorem
% 31.71/31.91 % SZS output start CNFRefutation
% 31.71/31.91 fof(con,conjecture,(![A]:(![L]:(![M]:((incident_point_and_line(A,L)&orthogonal_lines(L,M))=>equal_lines(L,orthogonal_through_point(M,A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 31.71/31.91 fof(c0,negated_conjecture,(~(![A]:(![L]:(![M]:((incident_point_and_line(A,L)&orthogonal_lines(L,M))=>equal_lines(L,orthogonal_through_point(M,A))))))),inference(assume_negation,[status(cth)],[con])).
% 31.71/31.91 fof(c1,negated_conjecture,(?[A]:(?[L]:(?[M]:((incident_point_and_line(A,L)&orthogonal_lines(L,M))&~equal_lines(L,orthogonal_through_point(M,A)))))),inference(fof_nnf,[status(thm)],[c0])).
% 31.71/31.91 fof(c2,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((incident_point_and_line(X2,X3)&orthogonal_lines(X3,X4))&~equal_lines(X3,orthogonal_through_point(X4,X2)))))),inference(variable_rename,[status(thm)],[c1])).
% 31.71/31.91 fof(c3,negated_conjecture,((incident_point_and_line(skolem0001,skolem0002)&orthogonal_lines(skolem0002,skolem0003))&~equal_lines(skolem0002,orthogonal_through_point(skolem0003,skolem0001))),inference(skolemize,[status(esa)],[c2])).
% 31.71/31.91 cnf(c5,negated_conjecture,orthogonal_lines(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c3])).
% 31.71/31.91 fof(a5,axiom,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>(~unorthogonal_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a5)).
% 31.71/31.91 fof(c7,plain,(![X]:(![Y]:(orthogonal_lines(X,Y)<=>~unorthogonal_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a5])).
% 31.71/31.91 fof(c8,plain,(![X]:(![Y]:((~orthogonal_lines(X,Y)|~unorthogonal_lines(X,Y))&(unorthogonal_lines(X,Y)|orthogonal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c7])).
% 31.71/31.91 fof(c9,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)],[c8])).
% 31.71/31.91 fof(c11,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(c10,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)],[c9])).])).
% 31.71/31.91 cnf(c12,plain,~orthogonal_lines(X108,X107)|~unorthogonal_lines(X108,X107),inference(split_conjunct,[status(thm)],[c11])).
% 31.71/31.91 fof(ax2,axiom,(![X]:(![Y]:(equal_lines(X,Y)<=>(~distinct_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', ax2)).
% 31.71/31.91 fof(c28,plain,(![X]:(![Y]:(equal_lines(X,Y)<=>~distinct_lines(X,Y)))),inference(fof_simplification,[status(thm)],[ax2])).
% 31.71/31.91 fof(c29,plain,(![X]:(![Y]:((~equal_lines(X,Y)|~distinct_lines(X,Y))&(distinct_lines(X,Y)|equal_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c28])).
% 31.71/31.91 fof(c30,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)],[c29])).
% 31.71/31.91 fof(c32,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(c31,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)],[c30])).])).
% 31.71/31.91 cnf(c33,plain,~equal_lines(X128,X129)|~distinct_lines(X128,X129),inference(split_conjunct,[status(thm)],[c32])).
% 31.71/31.91 fof(a3,axiom,(![X]:(![Y]:(parallel_lines(X,Y)<=>(~convergent_lines(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a3)).
% 31.71/31.91 fof(c21,plain,(![X]:(![Y]:(parallel_lines(X,Y)<=>~convergent_lines(X,Y)))),inference(fof_simplification,[status(thm)],[a3])).
% 31.71/31.91 fof(c22,plain,(![X]:(![Y]:((~parallel_lines(X,Y)|~convergent_lines(X,Y))&(convergent_lines(X,Y)|parallel_lines(X,Y))))),inference(fof_nnf,[status(thm)],[c21])).
% 31.71/31.91 fof(c23,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)],[c22])).
% 31.71/31.91 fof(c25,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(c24,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)],[c23])).])).
% 31.71/31.91 cnf(c26,plain,~parallel_lines(X122,X121)|~convergent_lines(X122,X121),inference(split_conjunct,[status(thm)],[c25])).
% 31.71/31.91 fof(coipo1,axiom,(![L]:(![M]:(~((~convergent_lines(L,M))&(~unorthogonal_lines(L,M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', coipo1)).
% 31.71/31.91 fof(c66,plain,(![L]:(![M]:(~(~convergent_lines(L,M)&~unorthogonal_lines(L,M))))),inference(fof_simplification,[status(thm)],[coipo1])).
% 31.71/31.91 fof(c67,plain,(![L]:(![M]:(convergent_lines(L,M)|unorthogonal_lines(L,M)))),inference(fof_nnf,[status(thm)],[c66])).
% 31.71/31.91 fof(c68,plain,(![X39]:(![X40]:(convergent_lines(X39,X40)|unorthogonal_lines(X39,X40)))),inference(variable_rename,[status(thm)],[c67])).
% 31.71/31.91 cnf(c69,plain,convergent_lines(X139,X138)|unorthogonal_lines(X139,X138),inference(split_conjunct,[status(thm)],[c68])).
% 31.71/31.91 cnf(c176,plain,unorthogonal_lines(X178,X177)|~parallel_lines(X178,X177),inference(resolution,[status(thm)],[c69, c26])).
% 31.71/31.91 fof(apart3,axiom,(![X]:(~convergent_lines(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart3)).
% 31.71/31.91 fof(c153,plain,(![X]:~convergent_lines(X,X)),inference(fof_simplification,[status(thm)],[apart3])).
% 31.71/31.91 fof(c154,plain,(![X93]:~convergent_lines(X93,X93)),inference(variable_rename,[status(thm)],[c153])).
% 31.71/31.91 cnf(c155,plain,~convergent_lines(X96,X96),inference(split_conjunct,[status(thm)],[c154])).
% 31.71/31.91 cnf(c27,plain,convergent_lines(X123,X124)|parallel_lines(X123,X124),inference(split_conjunct,[status(thm)],[c25])).
% 31.71/31.91 fof(ceq3,axiom,(![X]:(![Y]:(![Z]:(convergent_lines(X,Y)=>(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 31.71/31.91 fof(c104,plain,(![X]:(![Y]:(![Z]:(~convergent_lines(X,Y)|(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(fof_nnf,[status(thm)],[ceq3])).
% 31.71/31.91 fof(c105,plain,(![X]:(![Y]:(~convergent_lines(X,Y)|(![Z]:(distinct_lines(Y,Z)|convergent_lines(X,Z)))))),inference(shift_quantors,[status(thm)],[c104])).
% 31.71/31.91 fof(c107,plain,(![X63]:(![X64]:(![X65]:(~convergent_lines(X63,X64)|(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,(![X63]:(![X64]:(~convergent_lines(X63,X64)|(![X65]:(distinct_lines(X64,X65)|convergent_lines(X63,X65)))))),inference(variable_rename,[status(thm)],[c105])).])).
% 31.71/31.91 cnf(c108,plain,~convergent_lines(X300,X302)|distinct_lines(X302,X301)|convergent_lines(X300,X301),inference(split_conjunct,[status(thm)],[c107])).
% 31.71/31.91 cnf(c347,plain,distinct_lines(X1312,X1314)|convergent_lines(X1313,X1314)|parallel_lines(X1313,X1312),inference(resolution,[status(thm)],[c108, c27])).
% 31.71/31.91 cnf(c3090,plain,distinct_lines(X1318,X1317)|parallel_lines(X1317,X1318),inference(resolution,[status(thm)],[c347, c155])).
% 31.71/31.91 cnf(c3183,plain,distinct_lines(X1360,X1359)|unorthogonal_lines(X1359,X1360),inference(resolution,[status(thm)],[c3090, c176])).
% 31.71/31.91 cnf(c3571,plain,unorthogonal_lines(X1413,X1412)|~equal_lines(X1412,X1413),inference(resolution,[status(thm)],[c3183, c33])).
% 31.71/31.91 cnf(c34,plain,distinct_lines(X131,X130)|equal_lines(X131,X130),inference(split_conjunct,[status(thm)],[c32])).
% 31.71/31.91 fof(p1,axiom,(![X]:(![Y]:(distinct_lines(X,Y)=>convergent_lines(X,Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+1.ax', p1)).
% 31.71/31.91 fof(c101,plain,(![X]:(![Y]:(~distinct_lines(X,Y)|convergent_lines(X,Y)))),inference(fof_nnf,[status(thm)],[p1])).
% 31.71/31.91 fof(c102,plain,(![X61]:(![X62]:(~distinct_lines(X61,X62)|convergent_lines(X61,X62)))),inference(variable_rename,[status(thm)],[c101])).
% 31.71/31.91 cnf(c103,plain,~distinct_lines(X162,X161)|convergent_lines(X162,X161),inference(split_conjunct,[status(thm)],[c102])).
% 31.71/31.91 cnf(c186,plain,convergent_lines(X189,X190)|equal_lines(X189,X190),inference(resolution,[status(thm)],[c103, c34])).
% 31.71/31.91 cnf(c13,plain,unorthogonal_lines(X110,X109)|orthogonal_lines(X110,X109),inference(split_conjunct,[status(thm)],[c11])).
% 31.71/31.91 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/sandbox2/benchmark/Axioms/GEO006+4.ax', cotno1)).
% 31.71/31.91 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_simplification,[status(thm)],[cotno1])).
% 31.71/31.91 fof(c59,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)],[c58])).
% 31.71/31.91 fof(c60,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)],[c59])).
% 31.71/31.91 fof(c61,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)],[c60])).
% 31.71/31.91 cnf(c64,plain,unorthogonal_lines(X216,X215)|convergent_lines(X216,X214)|~convergent_lines(X215,X214)|~unorthogonal_lines(X215,X214),inference(split_conjunct,[status(thm)],[c61])).
% 31.71/31.91 cnf(c234,plain,unorthogonal_lines(X573,X572)|convergent_lines(X573,X574)|~convergent_lines(X572,X574)|orthogonal_lines(X572,X574),inference(resolution,[status(thm)],[c64, c13])).
% 31.71/31.91 cnf(c876,plain,unorthogonal_lines(X6350,X6349)|convergent_lines(X6350,X6348)|orthogonal_lines(X6349,X6348)|equal_lines(X6349,X6348),inference(resolution,[status(thm)],[c234, c186])).
% 31.71/31.91 cnf(c38284,plain,unorthogonal_lines(X7653,X7652)|orthogonal_lines(X7652,X7653)|equal_lines(X7652,X7653),inference(resolution,[status(thm)],[c876, c155])).
% 31.71/31.91 cnf(c50067,plain,unorthogonal_lines(X7658,X7657)|orthogonal_lines(X7657,X7658),inference(resolution,[status(thm)],[c38284, c3571])).
% 31.71/31.91 cnf(c50387,plain,orthogonal_lines(X7679,X7680)|~orthogonal_lines(X7680,X7679),inference(resolution,[status(thm)],[c50067, c12])).
% 31.71/31.91 cnf(c50501,plain,orthogonal_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c50387, c5])).
% 31.71/31.91 fof(ooc1,axiom,(![A]:(![L]:(~unorthogonal_lines(orthogonal_through_point(L,A),L)))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 31.71/31.91 fof(c78,plain,(![A]:(![L]:~unorthogonal_lines(orthogonal_through_point(L,A),L))),inference(fof_simplification,[status(thm)],[ooc1])).
% 31.71/31.91 fof(c79,plain,(![X47]:(![X48]:~unorthogonal_lines(orthogonal_through_point(X48,X47),X48))),inference(variable_rename,[status(thm)],[c78])).
% 31.71/31.91 cnf(c80,plain,~unorthogonal_lines(orthogonal_through_point(X101,X102),X101),inference(split_conjunct,[status(thm)],[c79])).
% 31.71/31.91 cnf(c50385,plain,orthogonal_lines(X7661,orthogonal_through_point(X7661,X7660)),inference(resolution,[status(thm)],[c50067, c80])).
% 31.71/31.91 fof(couo1,axiom,(![L]:(![M]:(![N]:(((~unorthogonal_lines(L,M))&(~unorthogonal_lines(L,N)))=>(~convergent_lines(M,N)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', couo1)).
% 31.71/31.91 fof(c54,plain,(![L]:(![M]:(![N]:((~unorthogonal_lines(L,M)&~unorthogonal_lines(L,N))=>~convergent_lines(M,N))))),inference(fof_simplification,[status(thm)],[couo1])).
% 31.71/31.91 fof(c55,plain,(![L]:(![M]:(![N]:((unorthogonal_lines(L,M)|unorthogonal_lines(L,N))|~convergent_lines(M,N))))),inference(fof_nnf,[status(thm)],[c54])).
% 31.71/31.91 fof(c56,plain,(![X33]:(![X34]:(![X35]:((unorthogonal_lines(X33,X34)|unorthogonal_lines(X33,X35))|~convergent_lines(X34,X35))))),inference(variable_rename,[status(thm)],[c55])).
% 31.71/31.91 cnf(c57,plain,unorthogonal_lines(X185,X184)|unorthogonal_lines(X185,X186)|~convergent_lines(X184,X186),inference(split_conjunct,[status(thm)],[c56])).
% 31.71/31.91 cnf(c6,negated_conjecture,~equal_lines(skolem0002,orthogonal_through_point(skolem0003,skolem0001)),inference(split_conjunct,[status(thm)],[c3])).
% 31.71/31.91 cnf(c209,plain,convergent_lines(skolem0002,orthogonal_through_point(skolem0003,skolem0001)),inference(resolution,[status(thm)],[c186, c6])).
% 31.71/31.91 cnf(c248,plain,unorthogonal_lines(X704,skolem0002)|unorthogonal_lines(X704,orthogonal_through_point(skolem0003,skolem0001)),inference(resolution,[status(thm)],[c209, c57])).
% 31.71/31.91 cnf(c1060,plain,unorthogonal_lines(X8051,skolem0002)|~orthogonal_lines(X8051,orthogonal_through_point(skolem0003,skolem0001)),inference(resolution,[status(thm)],[c248, c12])).
% 31.71/31.91 cnf(c56331,plain,unorthogonal_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c1060, c50385])).
% 31.71/31.91 cnf(c56340,plain,~orthogonal_lines(skolem0003,skolem0002),inference(resolution,[status(thm)],[c56331, c12])).
% 31.71/31.91 cnf(c56358,plain,$false,inference(resolution,[status(thm)],[c56340, c50501])).
% 31.71/31.91 % SZS output end CNFRefutation
% 31.71/31.91
% 31.71/31.91 % Initial clauses : 49
% 31.71/31.91 % Processed clauses : 916
% 31.71/31.91 % Factors computed : 137
% 31.71/31.91 % Resolvents computed: 56068
% 31.71/31.91 % Tautologies deleted: 12
% 31.71/31.91 % Forward subsumed : 2806
% 31.71/31.91 % Backward subsumed : 88
% 31.71/31.91 % -------- CPU Time ---------
% 31.71/31.91 % User time : 31.424 s
% 31.71/31.91 % System time : 0.143 s
% 31.71/31.91 % Total time : 31.567 s
%------------------------------------------------------------------------------