%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM835+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:47 EDT 2024
% Result : Theorem 263.60s 263.82s
% Output : Refutation 263.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12 % Problem : NUM835+2 : TPTP v8.1.2. Released v4.1.0.
% 0.13/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n014.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 16:22:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 263.60/263.82 % Version: 1.5
% 263.60/263.82 % SZS status Theorem
% 263.60/263.82 % SZS output start CNFRefutation
% 263.60/263.82 fof('dis(case_distinction(conseq(110)))',conjecture,(((?[Vd180]:vd165=vplus(vd151,Vd180))|(?[Vd170]:vd151=vplus(vd165,Vd170)))|vd151=vd165),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'dis(case_distinction(conseq(110)))')).
% 263.60/263.82 fof(c76,negated_conjecture,(~(((?[Vd180]:vd165=vplus(vd151,Vd180))|(?[Vd170]:vd151=vplus(vd165,Vd170)))|vd151=vd165)),inference(assume_negation,[status(cth)],['dis(case_distinction(conseq(110)))'])).
% 263.60/263.82 fof(c77,negated_conjecture,(((![Vd180]:vd165!=vplus(vd151,Vd180))&(![Vd170]:vd151!=vplus(vd165,Vd170)))&vd151!=vd165),inference(fof_nnf,[status(thm)],[c76])).
% 263.60/263.82 fof(c79,negated_conjecture,(![X35]:(![X36]:((vd165!=vplus(vd151,X35)&vd151!=vplus(vd165,X36))&vd151!=vd165))),inference(shift_quantors,[status(thm)],[fof(c78,negated_conjecture,(((![X35]:vd165!=vplus(vd151,X35))&(![X36]:vd151!=vplus(vd165,X36)))&vd151!=vd165),inference(variable_rename,[status(thm)],[c77])).])).
% 263.60/263.82 cnf(c82,negated_conjecture,vd151!=vd165,inference(split_conjunct,[status(thm)],[c79])).
% 263.60/263.82 cnf(symmetry,axiom,X42!=X43|X43=X42,theory(equality)).
% 263.60/263.82 cnf(c81,negated_conjecture,vd151!=vplus(vd165,X46),inference(split_conjunct,[status(thm)],[c79])).
% 263.60/263.82 cnf(c80,negated_conjecture,vd165!=vplus(vd151,X45),inference(split_conjunct,[status(thm)],[c79])).
% 263.60/263.82 cnf(reflexivity,axiom,X37=X37,theory(equality)).
% 263.60/263.82 fof('def(cond(conseq(105), 0), 1)',axiom,(![Vd151]:(![Vd152]:(m(Vd152)<=>((Vd151=Vd152|(?[Vd155]:Vd151=vplus(Vd152,Vd155)))|(?[Vd157]:Vd152=vplus(Vd151,Vd157)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'def(cond(conseq(105), 0), 1)')).
% 263.60/263.82 fof(c22,plain,(![Vd151]:(![Vd152]:((~m(Vd152)|((Vd151=Vd152|(?[Vd155]:Vd151=vplus(Vd152,Vd155)))|(?[Vd157]:Vd152=vplus(Vd151,Vd157))))&(((Vd151!=Vd152&(![Vd155]:Vd151!=vplus(Vd152,Vd155)))&(![Vd157]:Vd152!=vplus(Vd151,Vd157)))|m(Vd152))))),inference(fof_nnf,[status(thm)],['def(cond(conseq(105), 0), 1)'])).
% 263.60/263.82 fof(c23,plain,((![Vd151]:(![Vd152]:(~m(Vd152)|((Vd151=Vd152|(?[Vd155]:Vd151=vplus(Vd152,Vd155)))|(?[Vd157]:Vd152=vplus(Vd151,Vd157))))))&(![Vd151]:(![Vd152]:(((Vd151!=Vd152&(![Vd155]:Vd151!=vplus(Vd152,Vd155)))&(![Vd157]:Vd152!=vplus(Vd151,Vd157)))|m(Vd152))))),inference(shift_quantors,[status(thm)],[c22])).
% 263.60/263.82 fof(c24,plain,((![X15]:(![X16]:(~m(X16)|((X15=X16|(?[X17]:X15=vplus(X16,X17)))|(?[X18]:X16=vplus(X15,X18))))))&(![X19]:(![X20]:(((X19!=X20&(![X21]:X19!=vplus(X20,X21)))&(![X22]:X20!=vplus(X19,X22)))|m(X20))))),inference(variable_rename,[status(thm)],[c23])).
% 263.60/263.82 fof(c26,plain,(![X15]:(![X16]:(![X19]:(![X20]:(![X21]:(![X22]:((~m(X16)|((X15=X16|X15=vplus(X16,skolem0001(X15,X16)))|X16=vplus(X15,skolem0002(X15,X16))))&(((X19!=X20&X19!=vplus(X20,X21))&X20!=vplus(X19,X22))|m(X20))))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X15]:(![X16]:(~m(X16)|((X15=X16|X15=vplus(X16,skolem0001(X15,X16)))|X16=vplus(X15,skolem0002(X15,X16))))))&(![X19]:(![X20]:(((X19!=X20&(![X21]:X19!=vplus(X20,X21)))&(![X22]:X20!=vplus(X19,X22)))|m(X20))))),inference(skolemize,[status(esa)],[c24])).])).
% 263.60/263.82 fof(c27,plain,(![X15]:(![X16]:(![X19]:(![X20]:(![X21]:(![X22]:((~m(X16)|((X15=X16|X15=vplus(X16,skolem0001(X15,X16)))|X16=vplus(X15,skolem0002(X15,X16))))&(((X19!=X20|m(X20))&(X19!=vplus(X20,X21)|m(X20)))&(X20!=vplus(X19,X22)|m(X20)))))))))),inference(distribute,[status(thm)],[c26])).
% 263.60/263.82 cnf(c29,plain,X39!=X40|m(X40),inference(split_conjunct,[status(thm)],[c27])).
% 263.60/263.82 cnf(c83,plain,m(X41),inference(resolution,[status(thm)],[c29, reflexivity])).
% 263.60/263.82 cnf(c28,plain,~m(X105)|X104=X105|X104=vplus(X105,skolem0001(X104,X105))|X105=vplus(X104,skolem0002(X104,X105)),inference(split_conjunct,[status(thm)],[c27])).
% 263.60/263.82 cnf(c190,plain,X782=X781|X782=vplus(X781,skolem0001(X782,X781))|X781=vplus(X782,skolem0002(X782,X781)),inference(resolution,[status(thm)],[c28, c83])).
% 263.60/263.82 cnf(c5659,plain,vd165=vd151|vd151=vplus(vd165,skolem0002(vd165,vd151)),inference(resolution,[status(thm)],[c190, c80])).
% 263.60/263.82 cnf(c256423,plain,vd165=vd151,inference(resolution,[status(thm)],[c5659, c81])).
% 263.60/263.82 cnf(c256492,plain,vd151=vd165,inference(resolution,[status(thm)],[c256423, symmetry])).
% 263.60/263.82 cnf(c256628,plain,$false,inference(resolution,[status(thm)],[c256492, c82])).
% 263.60/263.82 % SZS output end CNFRefutation
% 263.60/263.82
% 263.60/263.82 % Initial clauses : 37
% 263.60/263.82 % Processed clauses : 1573
% 263.60/263.82 % Factors computed : 21
% 263.60/263.82 % Resolvents computed: 256799
% 263.60/263.82 % Tautologies deleted: 2
% 263.60/263.82 % Forward subsumed : 4017
% 263.60/263.82 % Backward subsumed : 18
% 263.60/263.82 % -------- CPU Time ---------
% 263.60/263.82 % User time : 262.848 s
% 263.60/263.82 % System time : 0.565 s
% 263.60/263.82 % Total time : 263.413 s
%------------------------------------------------------------------------------