%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KLE056+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:28:11 EDT 2024
% Result : Theorem 77.93s 78.20s
% Output : Refutation 77.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KLE056+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n012.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:00:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 77.93/78.20 % Version: 1.5
% 77.93/78.20 % SZS status Theorem
% 77.93/78.20 % SZS output start CNFRefutation
% 77.93/78.20 fof(goals,conjecture,(![X0]:(domain(X0)=zero=>X0=zero)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 77.93/78.20 fof(c4,negated_conjecture,(~(![X0]:(domain(X0)=zero=>X0=zero))),inference(assume_negation,[status(cth)],[goals])).
% 77.93/78.20 fof(c5,negated_conjecture,(?[X0]:(domain(X0)=zero&X0!=zero)),inference(fof_nnf,[status(thm)],[c4])).
% 77.93/78.20 fof(c6,negated_conjecture,(?[X2]:(domain(X2)=zero&X2!=zero)),inference(variable_rename,[status(thm)],[c5])).
% 77.93/78.20 fof(c7,negated_conjecture,(domain(skolem0001)=zero&skolem0001!=zero),inference(skolemize,[status(esa)],[c6])).
% 77.93/78.20 cnf(c9,negated_conjecture,skolem0001!=zero,inference(split_conjunct,[status(thm)],[c7])).
% 77.93/78.20 cnf(symmetry,axiom,X35!=X36|X36=X35,theory(equality)).
% 77.93/78.20 cnf(transitivity,axiom,X38!=X40|X40!=X39|X38=X39,theory(equality)).
% 77.93/78.20 fof(additive_identity,axiom,(![A]:addition(A,zero)=A),file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', additive_identity)).
% 77.93/78.20 fof(c41,plain,(![X27]:addition(X27,zero)=X27),inference(variable_rename,[status(thm)],[additive_identity])).
% 77.93/78.20 cnf(c42,plain,addition(X49,zero)=X49,inference(split_conjunct,[status(thm)],[c41])).
% 77.93/78.20 cnf(c71,plain,X174!=addition(X175,zero)|X174=X175,inference(resolution,[status(thm)],[c42, transitivity])).
% 77.93/78.20 fof(order,axiom,(![A]:(![B]:(leq(A,B)<=>addition(A,B)=B))),file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', order)).
% 77.93/78.20 fof(c19,plain,(![A]:(![B]:((~leq(A,B)|addition(A,B)=B)&(addition(A,B)!=B|leq(A,B))))),inference(fof_nnf,[status(thm)],[order])).
% 77.93/78.20 fof(c20,plain,((![A]:(![B]:(~leq(A,B)|addition(A,B)=B)))&(![A]:(![B]:(addition(A,B)!=B|leq(A,B))))),inference(shift_quantors,[status(thm)],[c19])).
% 77.93/78.20 fof(c22,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~leq(X9,X10)|addition(X9,X10)=X10)&(addition(X11,X12)!=X12|leq(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X9]:(![X10]:(~leq(X9,X10)|addition(X9,X10)=X10)))&(![X11]:(![X12]:(addition(X11,X12)!=X12|leq(X11,X12))))),inference(variable_rename,[status(thm)],[c20])).])).
% 77.93/78.20 cnf(c23,plain,~leq(X84,X83)|addition(X84,X83)=X83,inference(split_conjunct,[status(thm)],[c22])).
% 77.93/78.20 cnf(reflexivity,axiom,X33=X33,theory(equality)).
% 77.93/78.20 cnf(c3,axiom,X68!=X67|X66!=X69|~leq(X68,X66)|leq(X67,X69),theory(equality)).
% 77.93/78.20 cnf(c24,plain,addition(X88,X87)!=X87|leq(X88,X87),inference(split_conjunct,[status(thm)],[c22])).
% 77.93/78.20 fof(domain1,axiom,(![X0]:addition(X0,multiplication(domain(X0),X0))=multiplication(domain(X0),X0)),file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax', domain1)).
% 77.93/78.20 fof(c17,plain,(![X8]:addition(X8,multiplication(domain(X8),X8))=multiplication(domain(X8),X8)),inference(variable_rename,[status(thm)],[domain1])).
% 77.93/78.20 cnf(c18,plain,addition(X92,multiplication(domain(X92),X92))=multiplication(domain(X92),X92),inference(split_conjunct,[status(thm)],[c17])).
% 77.93/78.20 cnf(c162,plain,leq(X93,multiplication(domain(X93),X93)),inference(resolution,[status(thm)],[c18, c24])).
% 77.93/78.20 cnf(c168,plain,X595!=X594|multiplication(domain(X595),X595)!=X596|leq(X594,X596),inference(resolution,[status(thm)],[c162, c3])).
% 77.93/78.20 fof(left_annihilation,axiom,(![A]:multiplication(zero,A)=zero),file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', left_annihilation)).
% 77.93/78.20 fof(c25,plain,(![X13]:multiplication(zero,X13)=zero),inference(variable_rename,[status(thm)],[left_annihilation])).
% 77.93/78.20 cnf(c26,plain,multiplication(zero,X70)=zero,inference(split_conjunct,[status(thm)],[c25])).
% 77.93/78.20 cnf(c115,plain,X321!=multiplication(zero,X322)|X321=zero,inference(resolution,[status(thm)],[c26, transitivity])).
% 77.93/78.20 cnf(c8,negated_conjecture,domain(skolem0001)=zero,inference(split_conjunct,[status(thm)],[c7])).
% 77.93/78.20 cnf(c1,axiom,X55!=X54|X53!=X56|multiplication(X55,X53)=multiplication(X54,X56),theory(equality)).
% 77.93/78.20 cnf(c83,plain,X251!=X250|multiplication(X251,X249)=multiplication(X250,X249),inference(resolution,[status(thm)],[c1, reflexivity])).
% 77.93/78.20 cnf(c1671,plain,multiplication(domain(skolem0001),X3792)=multiplication(zero,X3792),inference(resolution,[status(thm)],[c83, c8])).
% 77.93/78.20 cnf(c101552,plain,multiplication(domain(skolem0001),X3796)=zero,inference(resolution,[status(thm)],[c1671, c115])).
% 77.93/78.20 cnf(c102440,plain,skolem0001!=X3797|leq(X3797,zero),inference(resolution,[status(thm)],[c101552, c168])).
% 77.93/78.20 cnf(c102568,plain,leq(skolem0001,zero),inference(resolution,[status(thm)],[c102440, reflexivity])).
% 77.93/78.20 cnf(c102623,plain,addition(skolem0001,zero)=zero,inference(resolution,[status(thm)],[c102568, c23])).
% 77.93/78.20 cnf(c102933,plain,zero=addition(skolem0001,zero),inference(resolution,[status(thm)],[c102623, symmetry])).
% 77.93/78.20 cnf(c103075,plain,zero=skolem0001,inference(resolution,[status(thm)],[c102933, c71])).
% 77.93/78.20 cnf(c103165,plain,skolem0001=zero,inference(resolution,[status(thm)],[c103075, symmetry])).
% 77.93/78.20 cnf(c103344,plain,$false,inference(resolution,[status(thm)],[c103165, c9])).
% 77.93/78.20 % SZS output end CNFRefutation
% 77.93/78.20
% 77.93/78.20 % Initial clauses : 27
% 77.93/78.20 % Processed clauses : 1347
% 77.93/78.20 % Factors computed : 5
% 77.93/78.20 % Resolvents computed: 103409
% 77.93/78.20 % Tautologies deleted: 2
% 77.93/78.20 % Forward subsumed : 2253
% 77.93/78.20 % Backward subsumed : 130
% 77.93/78.20 % -------- CPU Time ---------
% 77.93/78.20 % User time : 77.472 s
% 77.93/78.20 % System time : 0.299 s
% 77.93/78.20 % Total time : 77.771 s
%------------------------------------------------------------------------------