%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM840+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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 7.61s 7.84s
% Output : Refutation 7.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : NUM840+2 : TPTP v8.1.2. Released v4.1.0.
% 0.11/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n017.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 : Wed May 8 15:50:07 EDT 2024
% 0.14/0.35 % CPUTime :
% 7.61/7.84 % Version: 1.5
% 7.61/7.84 % SZS status Theorem
% 7.61/7.84 % SZS output start CNFRefutation
% 7.61/7.84 fof('ass(cond(goal(130), 0), 1)',axiom,(![Vd203]:(![Vd204]:(Vd203!=Vd204|(~less(Vd203,Vd204))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 1)')).
% 7.61/7.84 fof(c58,plain,(![Vd203]:(![Vd204]:(Vd203!=Vd204|~less(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)'])).
% 7.61/7.84 fof(c59,plain,(![X48]:(![X49]:(X48!=X49|~less(X48,X49)))),inference(variable_rename,[status(thm)],[c58])).
% 7.61/7.84 cnf(c60,plain,X79!=X78|~less(X79,X78),inference(split_conjunct,[status(thm)],[c59])).
% 7.61/7.84 fof('holds(antec(conjunct2(conjunct2(204))), 335, 0)',axiom,less(vplus(vd328,vd330),vplus(vd329,vd330)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(antec(conjunct2(conjunct2(204))), 335, 0)')).
% 7.61/7.84 cnf(c88,plain,less(vplus(vd328,vd330),vplus(vd329,vd330)),inference(split_conjunct,[status(thm)],['holds(antec(conjunct2(conjunct2(204))), 335, 0)'])).
% 7.61/7.84 cnf(c489,plain,vplus(vd328,vd330)!=vplus(vd329,vd330),inference(resolution,[status(thm)],[c88, c60])).
% 7.61/7.84 fof('ass(cond(goal(193), 0), 1)',axiom,(![Vd301]:(![Vd302]:(![Vd303]:(Vd301=Vd302=>vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'ass(cond(goal(193), 0), 1)')).
% 7.61/7.84 fof(c74,plain,(![Vd301]:(![Vd302]:(![Vd303]:(Vd301!=Vd302|vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 1)'])).
% 7.61/7.84 fof(c75,plain,(![Vd301]:(![Vd302]:(Vd301!=Vd302|(![Vd303]:vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),inference(shift_quantors,[status(thm)],[c74])).
% 7.61/7.84 fof(c77,plain,(![X59]:(![X60]:(![X61]:(X59!=X60|vplus(X59,X61)=vplus(X60,X61))))),inference(shift_quantors,[status(thm)],[fof(c76,plain,(![X59]:(![X60]:(X59!=X60|(![X61]:vplus(X59,X61)=vplus(X60,X61))))),inference(variable_rename,[status(thm)],[c75])).])).
% 7.61/7.84 cnf(c78,plain,X259!=X257|vplus(X259,X258)=vplus(X257,X258),inference(split_conjunct,[status(thm)],[c77])).
% 7.61/7.84 fof('holds(conseq(conjunct2(conjunct2(204))), 336, 0)',conjecture,less(vd328,vd329),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(conseq(conjunct2(conjunct2(204))), 336, 0)')).
% 7.61/7.84 fof(c89,negated_conjecture,(~less(vd328,vd329)),inference(assume_negation,[status(cth)],['holds(conseq(conjunct2(conjunct2(204))), 336, 0)'])).
% 7.61/7.84 fof(c90,negated_conjecture,~less(vd328,vd329),inference(fof_simplification,[status(thm)],[c89])).
% 7.61/7.84 cnf(c91,negated_conjecture,~less(vd328,vd329),inference(split_conjunct,[status(thm)],[c90])).
% 7.61/7.84 fof('ass(cond(goal(130), 0), 2)',axiom,(![Vd203]:(![Vd204]:((~greater(Vd203,Vd204))|(~less(Vd203,Vd204))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 2)')).
% 7.61/7.84 fof(c55,plain,(![Vd203]:(![Vd204]:(~greater(Vd203,Vd204)|~less(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)'])).
% 7.61/7.84 fof(c56,plain,(![X46]:(![X47]:(~greater(X46,X47)|~less(X46,X47)))),inference(variable_rename,[status(thm)],[c55])).
% 7.61/7.84 cnf(c57,plain,~greater(X76,X77)|~less(X76,X77),inference(split_conjunct,[status(thm)],[c56])).
% 7.61/7.84 cnf(c486,plain,~greater(vplus(vd328,vd330),vplus(vd329,vd330)),inference(resolution,[status(thm)],[c88, c57])).
% 7.61/7.84 fof('ass(cond(goal(130), 0), 0)',axiom,(![Vd203]:(![Vd204]:((Vd203=Vd204|greater(Vd203,Vd204))|less(Vd203,Vd204)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 0)')).
% 7.61/7.84 fof(c61,plain,(![X50]:(![X51]:((X50=X51|greater(X50,X51))|less(X50,X51)))),inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)'])).
% 7.61/7.84 cnf(c62,plain,X236=X237|greater(X236,X237)|less(X236,X237),inference(split_conjunct,[status(thm)],[c61])).
% 7.61/7.84 fof('ass(cond(goal(193), 0), 2)',axiom,(![Vd301]:(![Vd302]:(![Vd303]:(greater(Vd301,Vd302)=>greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'ass(cond(goal(193), 0), 2)')).
% 7.61/7.84 fof(c69,plain,(![Vd301]:(![Vd302]:(![Vd303]:(~greater(Vd301,Vd302)|greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)))))),inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 2)'])).
% 7.61/7.84 fof(c70,plain,(![Vd301]:(![Vd302]:(~greater(Vd301,Vd302)|(![Vd303]:greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)))))),inference(shift_quantors,[status(thm)],[c69])).
% 7.61/7.84 fof(c72,plain,(![X56]:(![X57]:(![X58]:(~greater(X56,X57)|greater(vplus(X56,X58),vplus(X57,X58)))))),inference(shift_quantors,[status(thm)],[fof(c71,plain,(![X56]:(![X57]:(~greater(X56,X57)|(![X58]:greater(vplus(X56,X58),vplus(X57,X58)))))),inference(variable_rename,[status(thm)],[c70])).])).
% 7.61/7.84 cnf(c73,plain,~greater(X248,X247)|greater(vplus(X248,X249),vplus(X247,X249)),inference(split_conjunct,[status(thm)],[c72])).
% 7.61/7.84 cnf(c370,plain,greater(vplus(X2138,X2140),vplus(X2139,X2140))|X2138=X2139|less(X2138,X2139),inference(resolution,[status(thm)],[c73, c62])).
% 7.61/7.84 cnf(c17474,plain,vd328=vd329|less(vd328,vd329),inference(resolution,[status(thm)],[c370, c486])).
% 7.61/7.84 cnf(c17728,plain,vd328=vd329,inference(resolution,[status(thm)],[c17474, c91])).
% 7.61/7.84 cnf(c17739,plain,vplus(vd328,X2279)=vplus(vd329,X2279),inference(resolution,[status(thm)],[c17728, c78])).
% 7.61/7.84 cnf(c21333,plain,$false,inference(resolution,[status(thm)],[c17739, c489])).
% 7.61/7.84 % SZS output end CNFRefutation
% 7.61/7.84
% 7.61/7.84 % Initial clauses : 36
% 7.61/7.84 % Processed clauses : 576
% 7.61/7.84 % Factors computed : 24
% 7.61/7.84 % Resolvents computed: 21254
% 7.61/7.84 % Tautologies deleted: 25
% 7.61/7.84 % Forward subsumed : 565
% 7.61/7.84 % Backward subsumed : 37
% 7.61/7.84 % -------- CPU Time ---------
% 7.61/7.84 % User time : 7.431 s
% 7.61/7.84 % System time : 0.055 s
% 7.61/7.84 % Total time : 7.486 s
%------------------------------------------------------------------------------