%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO147+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:11 EDT 2024
% Result : Theorem 2.36s 2.53s
% Output : Refutation 2.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : GEO147+1 : TPTP v8.1.2. Released v2.4.0.
% 0.05/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n021.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:11:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 2.36/2.53 % Version: 1.5
% 2.36/2.53 % SZS status Theorem
% 2.36/2.53 % SZS output start CNFRefutation
% 2.36/2.53 fof(at_on_trajectory,axiom,(![X]:(![P]:(once(at(X,P))<=>incident_o(P,trajectory_of(X))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+3.ax', at_on_trajectory)).
% 2.36/2.53 fof(c37,plain,(![X]:(![P]:((~once(at(X,P))|incident_o(P,trajectory_of(X)))&(~incident_o(P,trajectory_of(X))|once(at(X,P)))))),inference(fof_nnf,[status(thm)],[at_on_trajectory])).
% 2.36/2.53 fof(c38,plain,((![X]:(![P]:(~once(at(X,P))|incident_o(P,trajectory_of(X)))))&(![X]:(![P]:(~incident_o(P,trajectory_of(X))|once(at(X,P)))))),inference(shift_quantors,[status(thm)],[c37])).
% 2.36/2.53 fof(c40,plain,(![X16]:(![X17]:(![X18]:(![X19]:((~once(at(X16,X17))|incident_o(X17,trajectory_of(X16)))&(~incident_o(X19,trajectory_of(X18))|once(at(X18,X19)))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,((![X16]:(![X17]:(~once(at(X16,X17))|incident_o(X17,trajectory_of(X16)))))&(![X18]:(![X19]:(~incident_o(X19,trajectory_of(X18))|once(at(X18,X19)))))),inference(variable_rename,[status(thm)],[c38])).])).
% 2.36/2.53 cnf(c41,plain,~once(at(X382,X383))|incident_o(X383,trajectory_of(X382)),inference(split_conjunct,[status(thm)],[c40])).
% 2.36/2.53 fof(conjunction_at_the_same_time,axiom,(![A]:(![B]:(once(at_the_same_time(A,B))=>(once(A)&once(B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+3.ax', conjunction_at_the_same_time)).
% 2.36/2.53 fof(c43,plain,(![A]:(![B]:(~once(at_the_same_time(A,B))|(once(A)&once(B))))),inference(fof_nnf,[status(thm)],[conjunction_at_the_same_time])).
% 2.36/2.53 fof(c44,plain,(![X20]:(![X21]:(~once(at_the_same_time(X20,X21))|(once(X20)&once(X21))))),inference(variable_rename,[status(thm)],[c43])).
% 2.36/2.53 fof(c45,plain,(![X20]:(![X21]:((~once(at_the_same_time(X20,X21))|once(X20))&(~once(at_the_same_time(X20,X21))|once(X21))))),inference(distribute,[status(thm)],[c44])).
% 2.36/2.53 cnf(c46,plain,~once(at_the_same_time(X223,X222))|once(X223),inference(split_conjunct,[status(thm)],[c45])).
% 2.36/2.53 fof(t13,conjecture,(![P]:(![X]:(![Y]:(connect(X,Y,P)=>(incident_o(P,trajectory_of(X))&incident_o(P,trajectory_of(Y))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13)).
% 2.36/2.53 fof(c20,negated_conjecture,(~(![P]:(![X]:(![Y]:(connect(X,Y,P)=>(incident_o(P,trajectory_of(X))&incident_o(P,trajectory_of(Y)))))))),inference(assume_negation,[status(cth)],[t13])).
% 2.36/2.53 fof(c21,negated_conjecture,(?[P]:(?[X]:(?[Y]:(connect(X,Y,P)&(~incident_o(P,trajectory_of(X))|~incident_o(P,trajectory_of(Y))))))),inference(fof_nnf,[status(thm)],[c20])).
% 2.36/2.53 fof(c22,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(connect(X3,X4,X2)&(~incident_o(X2,trajectory_of(X3))|~incident_o(X2,trajectory_of(X4))))))),inference(variable_rename,[status(thm)],[c21])).
% 2.36/2.53 fof(c23,negated_conjecture,(connect(skolem0002,skolem0003,skolem0001)&(~incident_o(skolem0001,trajectory_of(skolem0002))|~incident_o(skolem0001,trajectory_of(skolem0003)))),inference(skolemize,[status(esa)],[c22])).
% 2.36/2.53 cnf(c24,negated_conjecture,connect(skolem0002,skolem0003,skolem0001),inference(split_conjunct,[status(thm)],[c23])).
% 2.36/2.53 fof(connect_defn,axiom,(![X]:(![Y]:(![P]:(connect(X,Y,P)<=>once(at_the_same_time(at(X,P),at(Y,P))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO004+3.ax', connect_defn)).
% 2.36/2.53 fof(c63,plain,(![X]:(![Y]:(![P]:((~connect(X,Y,P)|once(at_the_same_time(at(X,P),at(Y,P))))&(~once(at_the_same_time(at(X,P),at(Y,P)))|connect(X,Y,P)))))),inference(fof_nnf,[status(thm)],[connect_defn])).
% 2.36/2.53 fof(c64,plain,((![X]:(![Y]:(![P]:(~connect(X,Y,P)|once(at_the_same_time(at(X,P),at(Y,P)))))))&(![X]:(![Y]:(![P]:(~once(at_the_same_time(at(X,P),at(Y,P)))|connect(X,Y,P)))))),inference(shift_quantors,[status(thm)],[c63])).
% 2.36/2.53 fof(c66,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:((~connect(X33,X34,X35)|once(at_the_same_time(at(X33,X35),at(X34,X35))))&(~once(at_the_same_time(at(X36,X38),at(X37,X38)))|connect(X36,X37,X38))))))))),inference(shift_quantors,[status(thm)],[fof(c65,plain,((![X33]:(![X34]:(![X35]:(~connect(X33,X34,X35)|once(at_the_same_time(at(X33,X35),at(X34,X35)))))))&(![X36]:(![X37]:(![X38]:(~once(at_the_same_time(at(X36,X38),at(X37,X38)))|connect(X36,X37,X38)))))),inference(variable_rename,[status(thm)],[c64])).])).
% 2.36/2.53 cnf(c67,plain,~connect(X450,X451,X449)|once(at_the_same_time(at(X450,X449),at(X451,X449))),inference(split_conjunct,[status(thm)],[c66])).
% 2.36/2.53 cnf(c505,plain,once(at_the_same_time(at(skolem0002,skolem0001),at(skolem0003,skolem0001))),inference(resolution,[status(thm)],[c67, c24])).
% 2.36/2.53 cnf(c6774,plain,once(at(skolem0002,skolem0001)),inference(resolution,[status(thm)],[c505, c46])).
% 2.36/2.53 cnf(c6778,plain,incident_o(skolem0001,trajectory_of(skolem0002)),inference(resolution,[status(thm)],[c6774, c41])).
% 2.36/2.53 cnf(c25,negated_conjecture,~incident_o(skolem0001,trajectory_of(skolem0002))|~incident_o(skolem0001,trajectory_of(skolem0003)),inference(split_conjunct,[status(thm)],[c23])).
% 2.36/2.53 cnf(c47,plain,~once(at_the_same_time(X225,X224))|once(X224),inference(split_conjunct,[status(thm)],[c45])).
% 2.36/2.53 cnf(c6775,plain,once(at(skolem0003,skolem0001)),inference(resolution,[status(thm)],[c505, c47])).
% 2.36/2.53 cnf(c6782,plain,incident_o(skolem0001,trajectory_of(skolem0003)),inference(resolution,[status(thm)],[c6775, c41])).
% 2.36/2.53 cnf(c6797,plain,~incident_o(skolem0001,trajectory_of(skolem0002)),inference(resolution,[status(thm)],[c6782, c25])).
% 2.36/2.53 cnf(c6814,plain,$false,inference(resolution,[status(thm)],[c6797, c6778])).
% 2.36/2.53 % SZS output end CNFRefutation
% 2.36/2.53
% 2.36/2.53 % Initial clauses : 124
% 2.36/2.53 % Processed clauses : 563
% 2.36/2.53 % Factors computed : 29
% 2.36/2.53 % Resolvents computed: 6508
% 2.36/2.53 % Tautologies deleted: 13
% 2.36/2.53 % Forward subsumed : 465
% 2.36/2.53 % Backward subsumed : 1
% 2.36/2.53 % -------- CPU Time ---------
% 2.36/2.53 % User time : 2.143 s
% 2.36/2.53 % System time : 0.028 s
% 2.36/2.53 % Total time : 2.171 s
%------------------------------------------------------------------------------