%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO086+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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.47s 0.64s
% Output : Refutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO086+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n010.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:27:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.47/0.64 % Version: 1.5
% 0.47/0.64 % SZS status Theorem
% 0.47/0.64 % SZS output start CNFRefutation
% 0.47/0.64 fof(closed_defn,axiom,(![C]:(closed(C)<=>(~(?[P]:end_point(P,C))))),file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax', closed_defn)).
% 0.47/0.64 fof(c63,plain,(![C]:((~closed(C)|(![P]:~end_point(P,C)))&((?[P]:end_point(P,C))|closed(C)))),inference(fof_nnf,[status(thm)],[closed_defn])).
% 0.47/0.64 fof(c64,plain,((![C]:(~closed(C)|(![P]:~end_point(P,C))))&(![C]:((?[P]:end_point(P,C))|closed(C)))),inference(shift_quantors,[status(thm)],[c63])).
% 0.47/0.64 fof(c65,plain,((![X40]:(~closed(X40)|(![X41]:~end_point(X41,X40))))&(![X42]:((?[X43]:end_point(X43,X42))|closed(X42)))),inference(variable_rename,[status(thm)],[c64])).
% 0.47/0.64 fof(c67,plain,(![X40]:(![X41]:(![X42]:((~closed(X40)|~end_point(X41,X40))&(end_point(skolem0010(X42),X42)|closed(X42)))))),inference(shift_quantors,[status(thm)],[fof(c66,plain,((![X40]:(~closed(X40)|(![X41]:~end_point(X41,X40))))&(![X42]:(end_point(skolem0010(X42),X42)|closed(X42)))),inference(skolemize,[status(esa)],[c65])).])).
% 0.47/0.64 cnf(c68,plain,~closed(X86)|~end_point(X87,X86),inference(split_conjunct,[status(thm)],[c67])).
% 0.47/0.64 fof(theorem_2_7_2,conjecture,(![C]:(![Cpp]:((open(C)&part_of(Cpp,C))=>open(Cpp)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', theorem_2_7_2)).
% 0.47/0.64 fof(c8,negated_conjecture,(~(![C]:(![Cpp]:((open(C)&part_of(Cpp,C))=>open(Cpp))))),inference(assume_negation,[status(cth)],[theorem_2_7_2])).
% 0.47/0.64 fof(c9,negated_conjecture,(?[C]:(?[Cpp]:((open(C)&part_of(Cpp,C))&~open(Cpp)))),inference(fof_nnf,[status(thm)],[c8])).
% 0.47/0.64 fof(c10,negated_conjecture,(?[X2]:(?[X3]:((open(X2)&part_of(X3,X2))&~open(X3)))),inference(variable_rename,[status(thm)],[c9])).
% 0.47/0.64 fof(c11,negated_conjecture,((open(skolem0001)&part_of(skolem0002,skolem0001))&~open(skolem0002)),inference(skolemize,[status(esa)],[c10])).
% 0.47/0.64 cnf(c12,negated_conjecture,open(skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.64 fof(open_defn,axiom,(![C]:(open(C)<=>(?[P]:end_point(P,C)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax', open_defn)).
% 0.47/0.64 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.47/0.64 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.47/0.64 fof(c58,plain,((![X36]:(~open(X36)|(?[X37]:end_point(X37,X36))))&(![X38]:((![X39]:~end_point(X39,X38))|open(X38)))),inference(variable_rename,[status(thm)],[c57])).
% 0.47/0.64 fof(c60,plain,(![X36]:(![X38]:(![X39]:((~open(X36)|end_point(skolem0009(X36),X36))&(~end_point(X39,X38)|open(X38)))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,((![X36]:(~open(X36)|end_point(skolem0009(X36),X36)))&(![X38]:((![X39]:~end_point(X39,X38))|open(X38)))),inference(skolemize,[status(esa)],[c58])).])).
% 0.47/0.64 cnf(c61,plain,~open(X101)|end_point(skolem0009(X101),X101),inference(split_conjunct,[status(thm)],[c60])).
% 0.47/0.64 cnf(c131,plain,end_point(skolem0009(skolem0001),skolem0001),inference(resolution,[status(thm)],[c61, c12])).
% 0.47/0.64 cnf(c134,plain,~closed(skolem0001),inference(resolution,[status(thm)],[c131, c68])).
% 0.47/0.64 cnf(c14,negated_conjecture,~open(skolem0002),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.64 cnf(c62,plain,~end_point(X84,X85)|open(X85),inference(split_conjunct,[status(thm)],[c60])).
% 0.47/0.64 cnf(c69,plain,end_point(skolem0010(X110),X110)|closed(X110),inference(split_conjunct,[status(thm)],[c67])).
% 0.47/0.64 cnf(c141,plain,closed(X112)|open(X112),inference(resolution,[status(thm)],[c69, c62])).
% 0.47/0.64 cnf(c145,plain,closed(skolem0002),inference(resolution,[status(thm)],[c141, c14])).
% 0.47/0.64 cnf(c6,axiom,X144!=X145|~closed(X144)|closed(X145),theory(equality)).
% 0.47/0.64 cnf(c13,negated_conjecture,part_of(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.64 fof(c1,axiom,(![C]:(![C1]:((part_of(C1,C)&C1!=C)=>open(C1)))),file('/export/starexec/sandbox/benchmark/Axioms/GEO004+0.ax', c1)).
% 0.47/0.64 fof(c53,plain,(![C]:(![C1]:((~part_of(C1,C)|C1=C)|open(C1)))),inference(fof_nnf,[status(thm)],[c1])).
% 0.47/0.64 fof(c54,plain,(![X34]:(![X35]:((~part_of(X35,X34)|X35=X34)|open(X35)))),inference(variable_rename,[status(thm)],[c53])).
% 0.47/0.64 cnf(c55,plain,~part_of(X157,X156)|X157=X156|open(X157),inference(split_conjunct,[status(thm)],[c54])).
% 0.47/0.64 cnf(c175,plain,skolem0002=skolem0001|open(skolem0002),inference(resolution,[status(thm)],[c55, c13])).
% 0.47/0.64 cnf(c181,plain,skolem0002=skolem0001,inference(resolution,[status(thm)],[c175, c14])).
% 0.47/0.64 cnf(c196,plain,~closed(skolem0002)|closed(skolem0001),inference(resolution,[status(thm)],[c181, c6])).
% 0.47/0.64 cnf(c204,plain,closed(skolem0001),inference(resolution,[status(thm)],[c196, c145])).
% 0.47/0.64 cnf(c210,plain,$false,inference(resolution,[status(thm)],[c204, c134])).
% 0.47/0.64 % SZS output end CNFRefutation
% 0.47/0.64
% 0.47/0.64 % Initial clauses : 57
% 0.47/0.64 % Processed clauses : 50
% 0.47/0.64 % Factors computed : 4
% 0.47/0.64 % Resolvents computed: 80
% 0.47/0.64 % Tautologies deleted: 6
% 0.47/0.64 % Forward subsumed : 10
% 0.47/0.64 % Backward subsumed : 2
% 0.47/0.64 % -------- CPU Time ---------
% 0.47/0.64 % User time : 0.265 s
% 0.47/0.64 % System time : 0.015 s
% 0.47/0.64 % Total time : 0.280 s
%------------------------------------------------------------------------------