%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO085+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:01 EDT 2024
% Result : Theorem 0.68s 0.89s
% Output : Refutation 0.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO085+1 : TPTP v8.1.2. Released v2.4.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:18:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.68/0.89 % Version: 1.5
% 0.68/0.89 % SZS status Theorem
% 0.68/0.89 % SZS output start CNFRefutation
% 0.68/0.89 fof(theorem_2_7_1,conjecture,(![C]:(open(C)=>(?[P]:(?[Q]:((P!=Q&end_point(P,C))&end_point(Q,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_2_7_1)).
% 0.68/0.89 fof(c8,negated_conjecture,(~(![C]:(open(C)=>(?[P]:(?[Q]:((P!=Q&end_point(P,C))&end_point(Q,C))))))),inference(assume_negation,[status(cth)],[theorem_2_7_1])).
% 0.68/0.89 fof(c9,negated_conjecture,(?[C]:(open(C)&(![P]:(![Q]:((P=Q|~end_point(P,C))|~end_point(Q,C)))))),inference(fof_nnf,[status(thm)],[c8])).
% 0.68/0.89 fof(c10,negated_conjecture,(?[X2]:(open(X2)&(![X3]:(![X4]:((X3=X4|~end_point(X3,X2))|~end_point(X4,X2)))))),inference(variable_rename,[status(thm)],[c9])).
% 0.68/0.89 fof(c12,negated_conjecture,(![X3]:(![X4]:(open(skolem0001)&((X3=X4|~end_point(X3,skolem0001))|~end_point(X4,skolem0001))))),inference(shift_quantors,[status(thm)],[fof(c11,negated_conjecture,(open(skolem0001)&(![X3]:(![X4]:((X3=X4|~end_point(X3,skolem0001))|~end_point(X4,skolem0001))))),inference(skolemize,[status(esa)],[c10])).])).
% 0.68/0.89 cnf(c13,negated_conjecture,open(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 0.68/0.89 fof(open_defn,axiom,(![C]:(open(C)<=>(?[P]:end_point(P,C)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax', open_defn)).
% 0.68/0.89 fof(c56,plain,(![C]:((~open(C)|(?[P]:end_point(P,C)))&((![P]:~end_point(P,C))|open(C)))),inference(fof_nnf,[status(thm)],[open_defn])).
% 0.68/0.89 fof(c57,plain,((![C]:(~open(C)|(?[P]:end_point(P,C))))&(![C]:((![P]:~end_point(P,C))|open(C)))),inference(shift_quantors,[status(thm)],[c56])).
% 0.68/0.89 fof(c58,plain,((![X37]:(~open(X37)|(?[X38]:end_point(X38,X37))))&(![X39]:((![X40]:~end_point(X40,X39))|open(X39)))),inference(variable_rename,[status(thm)],[c57])).
% 0.68/0.89 fof(c60,plain,(![X37]:(![X39]:(![X40]:((~open(X37)|end_point(skolem0008(X37),X37))&(~end_point(X40,X39)|open(X39)))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X37]:(~open(X37)|end_point(skolem0008(X37),X37)))&(![X39]:((![X40]:~end_point(X40,X39))|open(X39)))),inference(skolemize,[status(esa)],[c58])).])).
% 0.68/0.89 cnf(c61,plain,~open(X102)|end_point(skolem0008(X102),X102),inference(split_conjunct,[status(thm)],[c60])).
% 0.68/0.89 cnf(c131,plain,end_point(skolem0008(skolem0001),skolem0001),inference(resolution,[status(thm)],[c61, c13])).
% 0.68/0.89 fof(c6,axiom,(![C]:(![P]:(end_point(P,C)=>(?[Q]:(end_point(Q,C)&P!=Q))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax', c6)).
% 0.68/0.89 fof(c31,plain,(![C]:(![P]:(~end_point(P,C)|(?[Q]:(end_point(Q,C)&P!=Q))))),inference(fof_nnf,[status(thm)],[c6])).
% 0.68/0.89 fof(c32,plain,(![X17]:(![X18]:(~end_point(X18,X17)|(?[X19]:(end_point(X19,X17)&X18!=X19))))),inference(variable_rename,[status(thm)],[c31])).
% 0.68/0.89 fof(c33,plain,(![X17]:(![X18]:(~end_point(X18,X17)|(end_point(skolem0004(X17,X18),X17)&X18!=skolem0004(X17,X18))))),inference(skolemize,[status(esa)],[c32])).
% 0.68/0.89 fof(c34,plain,(![X17]:(![X18]:((~end_point(X18,X17)|end_point(skolem0004(X17,X18),X17))&(~end_point(X18,X17)|X18!=skolem0004(X17,X18))))),inference(distribute,[status(thm)],[c33])).
% 0.68/0.89 cnf(c36,plain,~end_point(X154,X153)|X154!=skolem0004(X153,X154),inference(split_conjunct,[status(thm)],[c34])).
% 0.68/0.89 cnf(symmetry,axiom,X86!=X87|X87=X86,theory(equality)).
% 0.68/0.89 cnf(c35,plain,~end_point(X152,X151)|end_point(skolem0004(X151,X152),X151),inference(split_conjunct,[status(thm)],[c34])).
% 0.68/0.89 cnf(c168,plain,end_point(skolem0004(skolem0001,skolem0008(skolem0001)),skolem0001),inference(resolution,[status(thm)],[c35, c131])).
% 0.68/0.89 cnf(c14,negated_conjecture,X156=X155|~end_point(X156,skolem0001)|~end_point(X155,skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 0.68/0.89 cnf(c173,plain,X194=skolem0008(skolem0001)|~end_point(X194,skolem0001),inference(resolution,[status(thm)],[c14, c131])).
% 0.68/0.89 cnf(c251,plain,skolem0004(skolem0001,skolem0008(skolem0001))=skolem0008(skolem0001),inference(resolution,[status(thm)],[c173, c168])).
% 0.68/0.89 cnf(c550,plain,skolem0008(skolem0001)=skolem0004(skolem0001,skolem0008(skolem0001)),inference(resolution,[status(thm)],[c251, symmetry])).
% 0.68/0.89 cnf(c1095,plain,~end_point(skolem0008(skolem0001),skolem0001),inference(resolution,[status(thm)],[c550, c36])).
% 0.68/0.89 cnf(c1110,plain,$false,inference(resolution,[status(thm)],[c1095, c131])).
% 0.68/0.89 % SZS output end CNFRefutation
% 0.68/0.89
% 0.68/0.89 % Initial clauses : 56
% 0.68/0.89 % Processed clauses : 160
% 0.68/0.89 % Factors computed : 19
% 0.68/0.89 % Resolvents computed: 972
% 0.68/0.89 % Tautologies deleted: 8
% 0.68/0.89 % Forward subsumed : 84
% 0.68/0.89 % Backward subsumed : 0
% 0.68/0.89 % -------- CPU Time ---------
% 0.68/0.89 % User time : 0.513 s
% 0.68/0.89 % System time : 0.020 s
% 0.68/0.89 % Total time : 0.533 s
%------------------------------------------------------------------------------