%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM837+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:36:48 EDT 2024
% Result : Theorem 2.87s 3.11s
% Output : Refutation 2.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : NUM837+1 : TPTP v8.1.2. Released v4.1.0.
% 0.03/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Wed May 8 17:01:37 EDT 2024
% 0.10/0.29 % CPUTime :
% 2.87/3.11 % Version: 1.5
% 2.87/3.11 % SZS status Theorem
% 2.87/3.11 % SZS output start CNFRefutation
% 2.87/3.11 fof('holds(conjunct1(170), 270, 0)',axiom,less(vd268,vd269),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(conjunct1(170), 270, 0)')).
% 2.87/3.11 cnf(c107,plain,less(vd268,vd269),inference(split_conjunct,[status(thm)],['holds(conjunct1(170), 270, 0)'])).
% 2.87/3.11 fof('ass(cond(147, 0), 0)',axiom,(![Vd226]:(![Vd227]:(less(Vd226,Vd227)=>greater(Vd227,Vd226)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(147, 0), 0)')).
% 2.87/3.11 fof(c82,plain,(![Vd226]:(![Vd227]:(~less(Vd226,Vd227)|greater(Vd227,Vd226)))),inference(fof_nnf,[status(thm)],['ass(cond(147, 0), 0)'])).
% 2.87/3.11 fof(c83,plain,(![X61]:(![X62]:(~less(X61,X62)|greater(X62,X61)))),inference(variable_rename,[status(thm)],[c82])).
% 2.87/3.11 cnf(c84,plain,~less(X99,X100)|greater(X100,X99),inference(split_conjunct,[status(thm)],[c83])).
% 2.87/3.11 cnf(c122,plain,greater(vd269,vd268),inference(resolution,[status(thm)],[c84, c107])).
% 2.87/3.11 fof('ass(cond(goal(130), 0), 2)',axiom,(![Vd203]:(![Vd204]:((~greater(Vd203,Vd204))|(~less(Vd203,Vd204))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 2)')).
% 2.87/3.11 fof(c71,plain,(![Vd203]:(![Vd204]:(~greater(Vd203,Vd204)|~less(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)'])).
% 2.87/3.11 fof(c72,plain,(![X53]:(![X54]:(~greater(X53,X54)|~less(X53,X54)))),inference(variable_rename,[status(thm)],[c71])).
% 2.87/3.11 cnf(c73,plain,~greater(X86,X87)|~less(X86,X87),inference(split_conjunct,[status(thm)],[c72])).
% 2.87/3.11 fof('ass(cond(goal(130), 0), 3)',axiom,(![Vd203]:(![Vd204]:(Vd203!=Vd204|(~greater(Vd203,Vd204))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 3)')).
% 2.87/3.11 fof(c68,plain,(![Vd203]:(![Vd204]:(Vd203!=Vd204|~greater(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)'])).
% 2.87/3.11 fof(c69,plain,(![X51]:(![X52]:(X51!=X52|~greater(X51,X52)))),inference(variable_rename,[status(thm)],[c68])).
% 2.87/3.11 cnf(c70,plain,X84!=X85|~greater(X84,X85),inference(split_conjunct,[status(thm)],[c69])).
% 2.87/3.11 cnf(c124,plain,vd269!=vd268,inference(resolution,[status(thm)],[c122, c70])).
% 2.87/3.11 fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,(![Vd198]:(![Vd199]:(less(Vd199,Vd198)<=>(?[Vd201]:Vd198=vplus(Vd199,Vd201))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'def(cond(conseq(axiom(3)), 12), 1)')).
% 2.87/3.11 fof(c61,plain,(![Vd198]:(![Vd199]:((~less(Vd199,Vd198)|(?[Vd201]:Vd198=vplus(Vd199,Vd201)))&((![Vd201]:Vd198!=vplus(Vd199,Vd201))|less(Vd199,Vd198))))),inference(fof_nnf,[status(thm)],['def(cond(conseq(axiom(3)), 12), 1)'])).
% 2.87/3.11 fof(c62,plain,((![Vd198]:(![Vd199]:(~less(Vd199,Vd198)|(?[Vd201]:Vd198=vplus(Vd199,Vd201)))))&(![Vd198]:(![Vd199]:((![Vd201]:Vd198!=vplus(Vd199,Vd201))|less(Vd199,Vd198))))),inference(shift_quantors,[status(thm)],[c61])).
% 2.87/3.11 fof(c63,plain,((![X45]:(![X46]:(~less(X46,X45)|(?[X47]:X45=vplus(X46,X47)))))&(![X48]:(![X49]:((![X50]:X48!=vplus(X49,X50))|less(X49,X48))))),inference(variable_rename,[status(thm)],[c62])).
% 2.87/3.11 fof(c65,plain,(![X45]:(![X46]:(![X48]:(![X49]:(![X50]:((~less(X46,X45)|X45=vplus(X46,skolem0004(X45,X46)))&(X48!=vplus(X49,X50)|less(X49,X48)))))))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X45]:(![X46]:(~less(X46,X45)|X45=vplus(X46,skolem0004(X45,X46)))))&(![X48]:(![X49]:((![X50]:X48!=vplus(X49,X50))|less(X49,X48))))),inference(skolemize,[status(esa)],[c63])).])).
% 2.87/3.11 cnf(c67,plain,X256!=vplus(X255,X254)|less(X255,X256),inference(split_conjunct,[status(thm)],[c65])).
% 2.87/3.11 fof('qe(171)',conjecture,(?[Vd273]:vd269=vplus(vd268,Vd273)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qe(171)')).
% 2.87/3.11 fof(c109,negated_conjecture,(~(?[Vd273]:vd269=vplus(vd268,Vd273))),inference(assume_negation,[status(cth)],['qe(171)'])).
% 2.87/3.11 fof(c110,negated_conjecture,(![Vd273]:vd269!=vplus(vd268,Vd273)),inference(fof_nnf,[status(thm)],[c109])).
% 2.87/3.11 fof(c111,negated_conjecture,(![X75]:vd269!=vplus(vd268,X75)),inference(variable_rename,[status(thm)],[c110])).
% 2.87/3.11 cnf(c112,negated_conjecture,vd269!=vplus(vd268,X138),inference(split_conjunct,[status(thm)],[c111])).
% 2.87/3.11 fof('ass(cond(goal(88), 0), 0)',axiom,(![Vd120]:(![Vd121]:((Vd120=Vd121|(?[Vd123]:Vd120=vplus(Vd121,Vd123)))|(?[Vd125]:Vd121=vplus(Vd120,Vd125))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(88), 0), 0)')).
% 2.87/3.11 fof(c51,plain,(![X35]:(![X36]:((X35=X36|(?[X37]:X35=vplus(X36,X37)))|(?[X38]:X36=vplus(X35,X38))))),inference(variable_rename,[status(thm)],['ass(cond(goal(88), 0), 0)'])).
% 2.87/3.11 fof(c52,plain,(![X35]:(![X36]:((X35=X36|X35=vplus(X36,skolem0001(X35,X36)))|X36=vplus(X35,skolem0002(X35,X36))))),inference(skolemize,[status(esa)],[c51])).
% 2.87/3.11 cnf(c53,plain,X224=X225|X224=vplus(X225,skolem0001(X224,X225))|X225=vplus(X224,skolem0002(X224,X225)),inference(split_conjunct,[status(thm)],[c52])).
% 2.87/3.11 cnf(c296,plain,vd269=vd268|vd268=vplus(vd269,skolem0002(vd269,vd268)),inference(resolution,[status(thm)],[c53, c112])).
% 2.87/3.11 cnf(c7614,plain,vd269=vd268|less(vd269,vd268),inference(resolution,[status(thm)],[c296, c67])).
% 2.87/3.11 cnf(c9491,plain,less(vd269,vd268),inference(resolution,[status(thm)],[c7614, c124])).
% 2.87/3.11 cnf(c9534,plain,~greater(vd269,vd268),inference(resolution,[status(thm)],[c9491, c73])).
% 2.87/3.11 cnf(c9540,plain,$false,inference(resolution,[status(thm)],[c9534, c122])).
% 2.87/3.11 % SZS output end CNFRefutation
% 2.87/3.11
% 2.87/3.11 % Initial clauses : 48
% 2.87/3.11 % Processed clauses : 405
% 2.87/3.11 % Factors computed : 11
% 2.87/3.11 % Resolvents computed: 9423
% 2.87/3.11 % Tautologies deleted: 12
% 2.87/3.11 % Forward subsumed : 475
% 2.87/3.11 % Backward subsumed : 2
% 2.87/3.11 % -------- CPU Time ---------
% 2.87/3.11 % User time : 2.791 s
% 2.87/3.11 % System time : 0.029 s
% 2.87/3.11 % Total time : 2.820 s
%------------------------------------------------------------------------------