%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO081+1 : TPTP v8.1.2. Released v2.4.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:00 EDT 2024
% Result : Theorem 3.90s 4.09s
% Output : Refutation 3.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO081+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/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:00:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 3.90/4.09 % Version: 1.5
% 3.90/4.09 % SZS status Theorem
% 3.90/4.09 % SZS output start CNFRefutation
% 3.90/4.09 fof(part_of_transitivity,conjecture,(![C1]:(![C2]:(![C3]:((part_of(C1,C2)&part_of(C2,C3))=>part_of(C1,C3))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', part_of_transitivity)).
% 3.90/4.09 fof(c8,negated_conjecture,(~(![C1]:(![C2]:(![C3]:((part_of(C1,C2)&part_of(C2,C3))=>part_of(C1,C3)))))),inference(assume_negation,[status(cth)],[part_of_transitivity])).
% 3.90/4.09 fof(c9,negated_conjecture,(?[C1]:(?[C2]:(?[C3]:((part_of(C1,C2)&part_of(C2,C3))&~part_of(C1,C3))))),inference(fof_nnf,[status(thm)],[c8])).
% 3.90/4.09 fof(c10,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:((part_of(X2,X3)&part_of(X3,X4))&~part_of(X2,X4))))),inference(variable_rename,[status(thm)],[c9])).
% 3.90/4.09 fof(c11,negated_conjecture,((part_of(skolem0001,skolem0002)&part_of(skolem0002,skolem0003))&~part_of(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c10])).
% 3.90/4.09 cnf(c14,negated_conjecture,~part_of(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c11])).
% 3.90/4.09 fof(part_of_defn,axiom,(![C]:(![C1]:(part_of(C1,C)<=>(![P]:(incident_c(P,C1)=>incident_c(P,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+0.ax', part_of_defn)).
% 3.90/4.09 fof(c118,plain,(![C]:(![C1]:((~part_of(C1,C)|(![P]:(~incident_c(P,C1)|incident_c(P,C))))&((?[P]:(incident_c(P,C1)&~incident_c(P,C)))|part_of(C1,C))))),inference(fof_nnf,[status(thm)],[part_of_defn])).
% 3.90/4.09 fof(c119,plain,((![C]:(![C1]:(~part_of(C1,C)|(![P]:(~incident_c(P,C1)|incident_c(P,C))))))&(![C]:(![C1]:((?[P]:(incident_c(P,C1)&~incident_c(P,C)))|part_of(C1,C))))),inference(shift_quantors,[status(thm)],[c118])).
% 3.90/4.09 fof(c120,plain,((![X74]:(![X75]:(~part_of(X75,X74)|(![X76]:(~incident_c(X76,X75)|incident_c(X76,X74))))))&(![X77]:(![X78]:((?[X79]:(incident_c(X79,X78)&~incident_c(X79,X77)))|part_of(X78,X77))))),inference(variable_rename,[status(thm)],[c119])).
% 3.90/4.09 fof(c122,plain,(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:((~part_of(X75,X74)|(~incident_c(X76,X75)|incident_c(X76,X74)))&((incident_c(skolem0016(X77,X78),X78)&~incident_c(skolem0016(X77,X78),X77))|part_of(X78,X77)))))))),inference(shift_quantors,[status(thm)],[fof(c121,plain,((![X74]:(![X75]:(~part_of(X75,X74)|(![X76]:(~incident_c(X76,X75)|incident_c(X76,X74))))))&(![X77]:(![X78]:((incident_c(skolem0016(X77,X78),X78)&~incident_c(skolem0016(X77,X78),X77))|part_of(X78,X77))))),inference(skolemize,[status(esa)],[c120])).])).
% 3.90/4.10 fof(c123,plain,(![X74]:(![X75]:(![X76]:(![X77]:(![X78]:((~part_of(X75,X74)|(~incident_c(X76,X75)|incident_c(X76,X74)))&((incident_c(skolem0016(X77,X78),X78)|part_of(X78,X77))&(~incident_c(skolem0016(X77,X78),X77)|part_of(X78,X77))))))))),inference(distribute,[status(thm)],[c122])).
% 3.90/4.10 cnf(c126,plain,~incident_c(skolem0016(X164,X163),X164)|part_of(X163,X164),inference(split_conjunct,[status(thm)],[c123])).
% 3.90/4.10 cnf(c13,negated_conjecture,part_of(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c11])).
% 3.90/4.10 cnf(c124,plain,~part_of(X174,X176)|~incident_c(X175,X174)|incident_c(X175,X176),inference(split_conjunct,[status(thm)],[c123])).
% 3.90/4.10 cnf(c12,negated_conjecture,part_of(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c11])).
% 3.90/4.10 cnf(c125,plain,incident_c(skolem0016(X160,X159),X159)|part_of(X159,X160),inference(split_conjunct,[status(thm)],[c123])).
% 3.90/4.10 cnf(c203,plain,incident_c(skolem0016(skolem0003,skolem0001),skolem0001),inference(resolution,[status(thm)],[c125, c14])).
% 3.90/4.10 cnf(c231,plain,~part_of(skolem0001,X428)|incident_c(skolem0016(skolem0003,skolem0001),X428),inference(resolution,[status(thm)],[c124, c203])).
% 3.90/4.10 cnf(c1629,plain,incident_c(skolem0016(skolem0003,skolem0001),skolem0002),inference(resolution,[status(thm)],[c231, c12])).
% 3.90/4.10 cnf(c1636,plain,~part_of(skolem0002,X1758)|incident_c(skolem0016(skolem0003,skolem0001),X1758),inference(resolution,[status(thm)],[c1629, c124])).
% 3.90/4.10 cnf(c9756,plain,incident_c(skolem0016(skolem0003,skolem0001),skolem0003),inference(resolution,[status(thm)],[c1636, c13])).
% 3.90/4.10 cnf(c9762,plain,part_of(skolem0001,skolem0003),inference(resolution,[status(thm)],[c9756, c126])).
% 3.90/4.10 cnf(c9781,plain,$false,inference(resolution,[status(thm)],[c9762, c14])).
% 3.90/4.10 % SZS output end CNFRefutation
% 3.90/4.10
% 3.90/4.10 % Initial clauses : 57
% 3.90/4.10 % Processed clauses : 604
% 3.90/4.10 % Factors computed : 43
% 3.90/4.10 % Resolvents computed: 9624
% 3.90/4.10 % Tautologies deleted: 18
% 3.90/4.10 % Forward subsumed : 702
% 3.90/4.10 % Backward subsumed : 64
% 3.90/4.10 % -------- CPU Time ---------
% 3.90/4.10 % User time : 3.728 s
% 3.90/4.10 % System time : 0.029 s
% 3.90/4.10 % Total time : 3.757 s
%------------------------------------------------------------------------------