%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO231+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:39 EDT 2024
% Result : Theorem 35.72s 35.89s
% Output : Refutation 35.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GEO231+1 : TPTP v8.1.2. Bugfixed v6.4.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 08:00:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 35.72/35.89 % Version: 1.5
% 35.72/35.89 % SZS status Theorem
% 35.72/35.89 % SZS output start CNFRefutation
% 35.72/35.89 fof(oag11,axiom,(![L]:(![M]:(~(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag11)).
% 35.72/35.89 fof(c61,plain,(![L]:(![M]:(~left_convergent_lines(L,M)&~left_convergent_lines(L,reverse_line(M))))),inference(fof_nnf,[status(thm)],[oag11])).
% 35.72/35.89 fof(c62,plain,((![L]:(![M]:~left_convergent_lines(L,M)))&(![L]:(![M]:~left_convergent_lines(L,reverse_line(M))))),inference(shift_quantors,[status(thm)],[c61])).
% 35.72/35.89 fof(c64,plain,(![X39]:(![X40]:(![X41]:(![X42]:(~left_convergent_lines(X39,X40)&~left_convergent_lines(X41,reverse_line(X42))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X39]:(![X40]:~left_convergent_lines(X39,X40)))&(![X41]:(![X42]:~left_convergent_lines(X41,reverse_line(X42))))),inference(variable_rename,[status(thm)],[c62])).])).
% 35.72/35.89 cnf(c65,plain,~left_convergent_lines(X95,X94),inference(split_conjunct,[status(thm)],[c64])).
% 35.72/35.89 fof(con,conjecture,(![L]:(![M]:(![N]:(((~unequally_directed_lines(L,reverse_line(M)))&(~unequally_directed_lines(L,N)))=>(~unequally_directed_lines(M,reverse_line(N))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 35.72/35.89 fof(c0,negated_conjecture,(~(![L]:(![M]:(![N]:(((~unequally_directed_lines(L,reverse_line(M)))&(~unequally_directed_lines(L,N)))=>(~unequally_directed_lines(M,reverse_line(N)))))))),inference(assume_negation,[status(cth)],[con])).
% 35.72/35.89 fof(c1,negated_conjecture,(~(![L]:(![M]:(![N]:((~unequally_directed_lines(L,reverse_line(M))&~unequally_directed_lines(L,N))=>~unequally_directed_lines(M,reverse_line(N))))))),inference(fof_simplification,[status(thm)],[c0])).
% 35.72/35.89 fof(c2,negated_conjecture,(?[L]:(?[M]:(?[N]:((~unequally_directed_lines(L,reverse_line(M))&~unequally_directed_lines(L,N))&unequally_directed_lines(M,reverse_line(N)))))),inference(fof_nnf,[status(thm)],[c1])).
% 35.72/35.89 fof(c3,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((~unequally_directed_lines(X2,reverse_line(X3))&~unequally_directed_lines(X2,X4))&unequally_directed_lines(X3,reverse_line(X4)))))),inference(variable_rename,[status(thm)],[c2])).
% 35.72/35.89 fof(c4,negated_conjecture,((~unequally_directed_lines(skolem0001,reverse_line(skolem0002))&~unequally_directed_lines(skolem0001,skolem0003))&unequally_directed_lines(skolem0002,reverse_line(skolem0003))),inference(skolemize,[status(esa)],[c3])).
% 35.72/35.89 cnf(c7,negated_conjecture,unequally_directed_lines(skolem0002,reverse_line(skolem0003)),inference(split_conjunct,[status(thm)],[c4])).
% 35.72/35.89 fof(oag9,axiom,(![L]:(![M]:((unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M)))=>(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag9)).
% 35.72/35.89 fof(c73,plain,(![L]:(![M]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),inference(fof_nnf,[status(thm)],[oag9])).
% 35.72/35.89 fof(c74,plain,(![X47]:(![X48]:((~unequally_directed_lines(X47,X48)|~unequally_directed_lines(X47,reverse_line(X48)))|(left_convergent_lines(X47,X48)|left_convergent_lines(X47,reverse_line(X48)))))),inference(variable_rename,[status(thm)],[c73])).
% 35.72/35.89 cnf(c75,plain,~unequally_directed_lines(X214,X215)|~unequally_directed_lines(X214,reverse_line(X215))|left_convergent_lines(X214,X215)|left_convergent_lines(X214,reverse_line(X215)),inference(split_conjunct,[status(thm)],[c74])).
% 35.72/35.89 cnf(c184,plain,~unequally_directed_lines(skolem0002,skolem0003)|left_convergent_lines(skolem0002,skolem0003)|left_convergent_lines(skolem0002,reverse_line(skolem0003)),inference(resolution,[status(thm)],[c75, c7])).
% 35.72/35.89 cnf(c6,negated_conjecture,~unequally_directed_lines(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c4])).
% 35.72/35.89 fof(oag6,axiom,(![L]:(![M]:(![N]:(unequally_directed_lines(L,M)=>(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag6)).
% 35.72/35.89 fof(c88,plain,(![L]:(![M]:(![N]:(~unequally_directed_lines(L,M)|(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(fof_nnf,[status(thm)],[oag6])).
% 35.72/35.89 fof(c89,plain,(![L]:(![M]:(~unequally_directed_lines(L,M)|(![N]:(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c88])).
% 35.72/35.89 fof(c91,plain,(![X54]:(![X55]:(![X56]:(~unequally_directed_lines(X54,X55)|(unequally_directed_lines(X54,X56)|unequally_directed_lines(X55,X56)))))),inference(shift_quantors,[status(thm)],[fof(c90,plain,(![X54]:(![X55]:(~unequally_directed_lines(X54,X55)|(![X56]:(unequally_directed_lines(X54,X56)|unequally_directed_lines(X55,X56)))))),inference(variable_rename,[status(thm)],[c89])).])).
% 35.72/35.89 cnf(c92,plain,~unequally_directed_lines(X154,X156)|unequally_directed_lines(X154,X155)|unequally_directed_lines(X156,X155),inference(split_conjunct,[status(thm)],[c91])).
% 35.72/35.89 fof(oag5,axiom,(![L]:(~unequally_directed_lines(L,L))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag5)).
% 35.72/35.89 fof(c93,plain,(![L]:~unequally_directed_lines(L,L)),inference(fof_simplification,[status(thm)],[oag5])).
% 35.72/35.89 fof(c94,plain,(![X57]:~unequally_directed_lines(X57,X57)),inference(variable_rename,[status(thm)],[c93])).
% 35.72/35.89 cnf(c95,plain,~unequally_directed_lines(X98,X98),inference(split_conjunct,[status(thm)],[c94])).
% 35.72/35.89 cnf(c163,plain,unequally_directed_lines(skolem0002,X170)|unequally_directed_lines(reverse_line(skolem0003),X170),inference(resolution,[status(thm)],[c92, c7])).
% 35.72/35.89 cnf(c165,plain,unequally_directed_lines(reverse_line(skolem0003),skolem0002),inference(resolution,[status(thm)],[c163, c95])).
% 35.72/35.89 fof(oag7,axiom,(![L]:(![M]:(![N]:((unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M)))=>((unequally_directed_lines(L,N)&unequally_directed_lines(L,reverse_line(N)))|(unequally_directed_lines(M,N)&unequally_directed_lines(M,reverse_line(N)))))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag7)).
% 35.72/35.89 fof(c79,plain,(![L]:(![M]:(![N]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|((unequally_directed_lines(L,N)&unequally_directed_lines(L,reverse_line(N)))|(unequally_directed_lines(M,N)&unequally_directed_lines(M,reverse_line(N)))))))),inference(fof_nnf,[status(thm)],[oag7])).
% 35.72/35.89 fof(c80,plain,(![L]:(![M]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|(![N]:((unequally_directed_lines(L,N)&unequally_directed_lines(L,reverse_line(N)))|(unequally_directed_lines(M,N)&unequally_directed_lines(M,reverse_line(N)))))))),inference(shift_quantors,[status(thm)],[c79])).
% 35.72/35.89 fof(c82,plain,(![X51]:(![X52]:(![X53]:((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|((unequally_directed_lines(X51,X53)&unequally_directed_lines(X51,reverse_line(X53)))|(unequally_directed_lines(X52,X53)&unequally_directed_lines(X52,reverse_line(X53)))))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,(![X51]:(![X52]:((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(![X53]:((unequally_directed_lines(X51,X53)&unequally_directed_lines(X51,reverse_line(X53)))|(unequally_directed_lines(X52,X53)&unequally_directed_lines(X52,reverse_line(X53)))))))),inference(variable_rename,[status(thm)],[c80])).])).
% 35.72/35.89 fof(c83,plain,(![X51]:(![X52]:(![X53]:((((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,X53)|unequally_directed_lines(X52,X53)))&((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,X53)|unequally_directed_lines(X52,reverse_line(X53)))))&(((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,reverse_line(X53))|unequally_directed_lines(X52,X53)))&((~unequally_directed_lines(X51,X52)|~unequally_directed_lines(X51,reverse_line(X52)))|(unequally_directed_lines(X51,reverse_line(X53))|unequally_directed_lines(X52,reverse_line(X53))))))))),inference(distribute,[status(thm)],[c82])).
% 35.72/35.89 cnf(c86,plain,~unequally_directed_lines(X247,X248)|~unequally_directed_lines(X247,reverse_line(X248))|unequally_directed_lines(X247,reverse_line(X249))|unequally_directed_lines(X248,X249),inference(split_conjunct,[status(thm)],[c83])).
% 35.72/35.89 cnf(c5,negated_conjecture,~unequally_directed_lines(skolem0001,reverse_line(skolem0002)),inference(split_conjunct,[status(thm)],[c4])).
% 35.72/35.89 cnf(c169,plain,unequally_directed_lines(skolem0002,X268)|unequally_directed_lines(reverse_line(skolem0003),X267)|unequally_directed_lines(X268,X267),inference(resolution,[status(thm)],[c163, c92])).
% 35.72/35.89 cnf(c304,plain,unequally_directed_lines(skolem0002,skolem0001)|unequally_directed_lines(reverse_line(skolem0003),reverse_line(skolem0002)),inference(resolution,[status(thm)],[c169, c5])).
% 35.72/35.89 cnf(c596,plain,unequally_directed_lines(skolem0002,skolem0001)|~unequally_directed_lines(reverse_line(skolem0003),skolem0002)|unequally_directed_lines(reverse_line(skolem0003),reverse_line(X2278))|unequally_directed_lines(skolem0002,X2278),inference(resolution,[status(thm)],[c304, c86])).
% 35.72/35.89 cnf(c59694,plain,unequally_directed_lines(skolem0002,skolem0001)|unequally_directed_lines(reverse_line(skolem0003),reverse_line(X2285))|unequally_directed_lines(skolem0002,X2285),inference(resolution,[status(thm)],[c596, c165])).
% 35.72/35.89 cnf(c60164,plain,unequally_directed_lines(skolem0002,skolem0001)|unequally_directed_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c59694, c95])).
% 35.72/35.89 cnf(c60321,plain,unequally_directed_lines(skolem0002,skolem0003)|unequally_directed_lines(skolem0002,X2287)|unequally_directed_lines(skolem0001,X2287),inference(resolution,[status(thm)],[c60164, c92])).
% 35.72/35.89 cnf(c60920,plain,unequally_directed_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c60321, c6])).
% 35.72/35.89 cnf(c60965,plain,left_convergent_lines(skolem0002,skolem0003)|left_convergent_lines(skolem0002,reverse_line(skolem0003)),inference(resolution,[status(thm)],[c60920, c184])).
% 35.72/35.89 cnf(c61940,plain,left_convergent_lines(skolem0002,skolem0003),inference(resolution,[status(thm)],[c60965, c65])).
% 35.72/35.89 cnf(c61941,plain,$false,inference(resolution,[status(thm)],[c61940, c65])).
% 35.72/35.89 % SZS output end CNFRefutation
% 35.72/35.89
% 35.72/35.89 % Initial clauses : 61
% 35.72/35.89 % Processed clauses : 689
% 35.72/35.89 % Factors computed : 168
% 35.72/35.89 % Resolvents computed: 61611
% 35.72/35.89 % Tautologies deleted: 1
% 35.72/35.89 % Forward subsumed : 1238
% 35.72/35.89 % Backward subsumed : 152
% 35.72/35.89 % -------- CPU Time ---------
% 35.72/35.89 % User time : 35.355 s
% 35.72/35.89 % System time : 0.177 s
% 35.72/35.89 % Total time : 35.532 s
%------------------------------------------------------------------------------