%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM840+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 228.85s 229.10s
% Output : Refutation 228.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NUM840+1 : TPTP v8.1.2. Released v4.1.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n009.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 16:43:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 228.85/229.10 % Version: 1.5
% 228.85/229.10 % SZS status Theorem
% 228.85/229.10 % SZS output start CNFRefutation
% 228.85/229.10 fof('holds(conseq(conjunct2(conjunct2(204))), 336, 0)',conjecture,less(vd328,vd329),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(conseq(conjunct2(conjunct2(204))), 336, 0)')).
% 228.85/229.10 fof(c140,negated_conjecture,(~less(vd328,vd329)),inference(assume_negation,[status(cth)],['holds(conseq(conjunct2(conjunct2(204))), 336, 0)'])).
% 228.85/229.10 fof(c141,negated_conjecture,~less(vd328,vd329),inference(fof_simplification,[status(thm)],[c140])).
% 228.85/229.10 cnf(c142,negated_conjecture,~less(vd328,vd329),inference(split_conjunct,[status(thm)],[c141])).
% 228.85/229.10 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)')).
% 228.85/229.10 fof(c68,plain,(![Vd203]:(![Vd204]:(Vd203!=Vd204|~greater(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 3)'])).
% 228.85/229.10 fof(c69,plain,(![X51]:(![X52]:(X51!=X52|~greater(X51,X52)))),inference(variable_rename,[status(thm)],[c68])).
% 228.85/229.10 cnf(c70,plain,X105!=X106|~greater(X105,X106),inference(split_conjunct,[status(thm)],[c69])).
% 228.85/229.10 fof('ass(cond(goal(130), 0), 0)',axiom,(![Vd203]:(![Vd204]:((Vd203=Vd204|greater(Vd203,Vd204))|less(Vd203,Vd204)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 0)')).
% 228.85/229.10 fof(c77,plain,(![X57]:(![X58]:((X57=X58|greater(X57,X58))|less(X57,X58)))),inference(variable_rename,[status(thm)],['ass(cond(goal(130), 0), 0)'])).
% 228.85/229.10 cnf(c78,plain,X313=X314|greater(X313,X314)|less(X313,X314),inference(split_conjunct,[status(thm)],[c77])).
% 228.85/229.10 fof('ass(cond(goal(193), 0), 1)',axiom,(![Vd301]:(![Vd302]:(![Vd303]:(Vd301=Vd302=>vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(193), 0), 1)')).
% 228.85/229.10 fof(c125,plain,(![Vd301]:(![Vd302]:(![Vd303]:(Vd301!=Vd302|vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 1)'])).
% 228.85/229.10 fof(c126,plain,(![Vd301]:(![Vd302]:(Vd301!=Vd302|(![Vd303]:vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),inference(shift_quantors,[status(thm)],[c125])).
% 228.85/229.10 fof(c128,plain,(![X89]:(![X90]:(![X91]:(X89!=X90|vplus(X89,X91)=vplus(X90,X91))))),inference(shift_quantors,[status(thm)],[fof(c127,plain,(![X89]:(![X90]:(X89!=X90|(![X91]:vplus(X89,X91)=vplus(X90,X91))))),inference(variable_rename,[status(thm)],[c126])).])).
% 228.85/229.10 cnf(c129,plain,X411!=X412|vplus(X411,X410)=vplus(X412,X410),inference(split_conjunct,[status(thm)],[c128])).
% 228.85/229.10 cnf(c585,plain,vplus(X3372,X3373)=vplus(X3371,X3373)|greater(X3372,X3371)|less(X3372,X3371),inference(resolution,[status(thm)],[c129, c78])).
% 228.85/229.10 fof('ass(cond(goal(130), 0), 1)',axiom,(![Vd203]:(![Vd204]:(Vd203!=Vd204|(~less(Vd203,Vd204))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(130), 0), 1)')).
% 228.85/229.10 fof(c74,plain,(![Vd203]:(![Vd204]:(Vd203!=Vd204|~less(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 1)'])).
% 228.85/229.10 fof(c75,plain,(![X55]:(![X56]:(X55!=X56|~less(X55,X56)))),inference(variable_rename,[status(thm)],[c74])).
% 228.85/229.10 cnf(c76,plain,X115!=X114|~less(X115,X114),inference(split_conjunct,[status(thm)],[c75])).
% 228.85/229.10 fof('holds(antec(conjunct2(conjunct2(204))), 335, 0)',axiom,less(vplus(vd328,vd330),vplus(vd329,vd330)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(antec(conjunct2(conjunct2(204))), 335, 0)')).
% 228.85/229.10 cnf(c139,plain,less(vplus(vd328,vd330),vplus(vd329,vd330)),inference(split_conjunct,[status(thm)],['holds(antec(conjunct2(conjunct2(204))), 335, 0)'])).
% 228.85/229.10 cnf(c659,plain,vplus(vd328,vd330)!=vplus(vd329,vd330),inference(resolution,[status(thm)],[c139, c76])).
% 228.85/229.10 cnf(c37710,plain,greater(vd328,vd329)|less(vd328,vd329),inference(resolution,[status(thm)],[c659, c585])).
% 228.85/229.10 cnf(c174760,plain,greater(vd328,vd329),inference(resolution,[status(thm)],[c37710, c142])).
% 228.85/229.10 cnf(c174776,plain,vd328!=vd329,inference(resolution,[status(thm)],[c174760, c70])).
% 228.85/229.10 fof('ass(cond(goal(193), 0), 2)',axiom,(![Vd301]:(![Vd302]:(![Vd303]:(greater(Vd301,Vd302)=>greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'ass(cond(goal(193), 0), 2)')).
% 228.85/229.10 fof(c120,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)'])).
% 228.85/229.10 fof(c121,plain,(![Vd301]:(![Vd302]:(~greater(Vd301,Vd302)|(![Vd303]:greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)))))),inference(shift_quantors,[status(thm)],[c120])).
% 228.85/229.10 fof(c123,plain,(![X86]:(![X87]:(![X88]:(~greater(X86,X87)|greater(vplus(X86,X88),vplus(X87,X88)))))),inference(shift_quantors,[status(thm)],[fof(c122,plain,(![X86]:(![X87]:(~greater(X86,X87)|(![X88]:greater(vplus(X86,X88),vplus(X87,X88)))))),inference(variable_rename,[status(thm)],[c121])).])).
% 228.85/229.10 cnf(c124,plain,~greater(X399,X400)|greater(vplus(X399,X398),vplus(X400,X398)),inference(split_conjunct,[status(thm)],[c123])).
% 228.85/229.10 cnf(c560,plain,greater(vplus(X3214,X3215),vplus(X3213,X3215))|X3214=X3213|less(X3214,X3213),inference(resolution,[status(thm)],[c124, c78])).
% 228.85/229.10 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)')).
% 228.85/229.10 fof(c71,plain,(![Vd203]:(![Vd204]:(~greater(Vd203,Vd204)|~less(Vd203,Vd204)))),inference(fof_simplification,[status(thm)],['ass(cond(goal(130), 0), 2)'])).
% 228.85/229.10 fof(c72,plain,(![X53]:(![X54]:(~greater(X53,X54)|~less(X53,X54)))),inference(variable_rename,[status(thm)],[c71])).
% 228.85/229.10 cnf(c73,plain,~greater(X110,X109)|~less(X110,X109),inference(split_conjunct,[status(thm)],[c72])).
% 228.85/229.10 cnf(c662,plain,~greater(vplus(vd328,vd330),vplus(vd329,vd330)),inference(resolution,[status(thm)],[c139, c73])).
% 228.85/229.10 cnf(c37891,plain,vd328=vd329|less(vd328,vd329),inference(resolution,[status(thm)],[c662, c560])).
% 228.85/229.10 cnf(c210419,plain,less(vd328,vd329),inference(resolution,[status(thm)],[c37891, c174776])).
% 228.85/229.10 cnf(c210503,plain,$false,inference(resolution,[status(thm)],[c210419, c142])).
% 228.85/229.10 % SZS output end CNFRefutation
% 228.85/229.10
% 228.85/229.10 % Initial clauses : 57
% 228.85/229.10 % Processed clauses : 2017
% 228.85/229.10 % Factors computed : 20
% 228.85/229.10 % Resolvents computed: 210346
% 228.85/229.10 % Tautologies deleted: 27
% 228.85/229.10 % Forward subsumed : 5130
% 228.85/229.10 % Backward subsumed : 88
% 228.85/229.10 % -------- CPU Time ---------
% 228.85/229.10 % User time : 228.217 s
% 228.85/229.10 % System time : 0.489 s
% 228.85/229.10 % Total time : 228.706 s
%------------------------------------------------------------------------------