%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM846+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:49 EDT 2024
% Result : Theorem 58.11s 58.29s
% Output : Refutation 58.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NUM846+1 : TPTP v8.1.2. Released v4.1.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n015.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 16:38:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 58.11/58.29 % Version: 1.5
% 58.11/58.29 % SZS status Theorem
% 58.11/58.29 % SZS output start CNFRefutation
% 58.11/58.29 fof('holds(286, 441, 2)',conjecture,vplus(vmul(vd436,vplus(vd437,vd439)),vd436)=vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(286, 441, 2)')).
% 58.11/58.29 fof(c187,negated_conjecture,(~vplus(vmul(vd436,vplus(vd437,vd439)),vd436)=vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436)),inference(assume_negation,[status(cth)],['holds(286, 441, 2)'])).
% 58.11/58.29 fof(c188,negated_conjecture,vplus(vmul(vd436,vplus(vd437,vd439)),vd436)!=vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),inference(fof_simplification,[status(thm)],[c187])).
% 58.11/58.29 cnf(c189,negated_conjecture,vplus(vmul(vd436,vplus(vd437,vd439)),vd436)!=vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),inference(split_conjunct,[status(thm)],[c188])).
% 58.11/58.29 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)')).
% 58.11/58.29 fof(c126,plain,(![Vd301]:(![Vd302]:(![Vd303]:(Vd301!=Vd302|vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),inference(fof_nnf,[status(thm)],['ass(cond(goal(193), 0), 1)'])).
% 58.11/58.29 fof(c127,plain,(![Vd301]:(![Vd302]:(Vd301!=Vd302|(![Vd303]:vplus(Vd301,Vd303)=vplus(Vd302,Vd303))))),inference(shift_quantors,[status(thm)],[c126])).
% 58.11/58.29 fof(c129,plain,(![X89]:(![X90]:(![X91]:(X89!=X90|vplus(X89,X91)=vplus(X90,X91))))),inference(shift_quantors,[status(thm)],[fof(c128,plain,(![X89]:(![X90]:(X89!=X90|(![X91]:vplus(X89,X91)=vplus(X90,X91))))),inference(variable_rename,[status(thm)],[c127])).])).
% 58.11/58.29 cnf(c130,plain,X460!=X461|vplus(X460,X459)=vplus(X461,X459),inference(split_conjunct,[status(thm)],[c129])).
% 58.11/58.29 fof('holds(285, 440, 0)',axiom,vmul(vd436,vplus(vd437,vd439))=vplus(vmul(vd436,vd437),vmul(vd436,vd439)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(285, 440, 0)')).
% 58.11/58.29 cnf(c184,plain,vmul(vd436,vplus(vd437,vd439))=vplus(vmul(vd436,vd437),vmul(vd436,vd439)),inference(split_conjunct,[status(thm)],['holds(285, 440, 0)'])).
% 58.11/58.29 cnf(c1088,plain,vplus(vmul(vd436,vplus(vd437,vd439)),X7311)=vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),X7311),inference(resolution,[status(thm)],[c184, c130])).
% 58.11/58.29 cnf(c79771,plain,$false,inference(resolution,[status(thm)],[c1088, c189])).
% 58.11/58.29 % SZS output end CNFRefutation
% 58.11/58.29
% 58.11/58.29 % Initial clauses : 76
% 58.11/58.29 % Processed clauses : 1215
% 58.11/58.29 % Factors computed : 23
% 58.11/58.29 % Resolvents computed: 79606
% 58.11/58.29 % Tautologies deleted: 17
% 58.11/58.29 % Forward subsumed : 2686
% 58.11/58.29 % Backward subsumed : 36
% 58.11/58.29 % -------- CPU Time ---------
% 58.11/58.29 % User time : 57.740 s
% 58.11/58.29 % System time : 0.186 s
% 58.11/58.29 % Total time : 57.926 s
%------------------------------------------------------------------------------