%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KLE086+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:14 EDT 2024
% Result : Theorem 60.65s 60.90s
% Output : Refutation 60.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KLE086+1 : TPTP v8.1.2. Released v4.0.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.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 : Thu May 9 06:45:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 60.65/60.90 % Version: 1.5
% 60.65/60.90 % SZS status Theorem
% 60.65/60.90 % SZS output start CNFRefutation
% 60.65/60.90 fof(goals,conjecture,domain(zero)=zero,file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 60.65/60.90 fof(c7,negated_conjecture,(~domain(zero)=zero),inference(assume_negation,[status(cth)],[goals])).
% 60.65/60.90 fof(c8,negated_conjecture,domain(zero)!=zero,inference(fof_simplification,[status(thm)],[c7])).
% 60.65/60.90 cnf(c9,negated_conjecture,domain(zero)!=zero,inference(split_conjunct,[status(thm)],[c8])).
% 60.65/60.90 cnf(symmetry,axiom,X39!=X38|X38=X39,theory(equality)).
% 60.65/60.90 cnf(transitivity,axiom,X44!=X42|X42!=X43|X44=X43,theory(equality)).
% 60.65/60.90 fof(domain4,axiom,(![X0]:domain(X0)=antidomain(antidomain(X0))),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax', domain4)).
% 60.65/60.90 fof(c18,plain,(![X7]:domain(X7)=antidomain(antidomain(X7))),inference(variable_rename,[status(thm)],[domain4])).
% 60.65/60.90 cnf(c19,plain,domain(X80)=antidomain(antidomain(X80)),inference(split_conjunct,[status(thm)],[c18])).
% 60.65/60.90 cnf(c151,plain,antidomain(antidomain(X89))=domain(X89),inference(resolution,[status(thm)],[c19, symmetry])).
% 60.65/60.90 cnf(c199,plain,X695!=antidomain(antidomain(X694))|X695=domain(X694),inference(resolution,[status(thm)],[c151, transitivity])).
% 60.65/60.90 fof(domain1,axiom,(![X0]:multiplication(antidomain(X0),X0)=zero),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax', domain1)).
% 60.65/60.90 fof(c24,plain,(![X11]:multiplication(antidomain(X11),X11)=zero),inference(variable_rename,[status(thm)],[domain1])).
% 60.65/60.90 cnf(c25,plain,multiplication(antidomain(X81),X81)=zero,inference(split_conjunct,[status(thm)],[c24])).
% 60.65/60.90 cnf(c157,plain,zero=multiplication(antidomain(X93),X93),inference(resolution,[status(thm)],[c25, symmetry])).
% 60.65/60.90 fof(multiplicative_right_identity,axiom,(![A]:multiplication(A,one)=A),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', multiplicative_right_identity)).
% 60.65/60.90 fof(c42,plain,(![X25]:multiplication(X25,one)=X25),inference(variable_rename,[status(thm)],[multiplicative_right_identity])).
% 60.65/60.90 cnf(c43,plain,multiplication(X47,one)=X47,inference(split_conjunct,[status(thm)],[c42])).
% 60.65/60.90 cnf(c64,plain,X172!=multiplication(X171,one)|X172=X171,inference(resolution,[status(thm)],[c43, transitivity])).
% 60.65/60.90 cnf(c531,plain,zero=antidomain(one),inference(resolution,[status(thm)],[c64, c157])).
% 60.65/60.90 cnf(c626,plain,antidomain(one)=zero,inference(resolution,[status(thm)],[c531, symmetry])).
% 60.65/60.90 cnf(c711,plain,X558!=antidomain(one)|X558=zero,inference(resolution,[status(thm)],[c626, transitivity])).
% 60.65/60.90 cnf(c2,axiom,X68!=X69|antidomain(X68)=antidomain(X69),theory(equality)).
% 60.65/60.90 cnf(c627,plain,antidomain(zero)=antidomain(antidomain(one)),inference(resolution,[status(thm)],[c531, c2])).
% 60.65/60.90 cnf(c13267,plain,antidomain(zero)=domain(one),inference(resolution,[status(thm)],[c199, c627])).
% 60.65/60.90 fof(domain3,axiom,(![X0]:addition(antidomain(antidomain(X0)),antidomain(X0))=one),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax', domain3)).
% 60.65/60.90 fof(c20,plain,(![X8]:addition(antidomain(antidomain(X8)),antidomain(X8))=one),inference(variable_rename,[status(thm)],[domain3])).
% 60.65/60.90 cnf(c21,plain,addition(antidomain(antidomain(X122)),antidomain(X122))=one,inference(split_conjunct,[status(thm)],[c20])).
% 60.65/60.90 cnf(c288,plain,X1016!=addition(antidomain(antidomain(X1015)),antidomain(X1015))|X1016=one,inference(resolution,[status(thm)],[c21, transitivity])).
% 60.65/60.90 fof(additive_commutativity,axiom,(![A]:(![B]:addition(A,B)=addition(B,A))),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_commutativity)).
% 60.65/60.90 fof(c52,plain,(![X34]:(![X35]:addition(X34,X35)=addition(X35,X34))),inference(variable_rename,[status(thm)],[additive_commutativity])).
% 60.65/60.90 cnf(c53,plain,addition(X85,X86)=addition(X86,X85),inference(split_conjunct,[status(thm)],[c52])).
% 60.65/60.90 cnf(c178,plain,X593!=addition(X592,X591)|X593=addition(X591,X592),inference(resolution,[status(thm)],[c53, transitivity])).
% 60.65/60.90 fof(order,axiom,(![A]:(![B]:(leq(A,B)<=>addition(A,B)=B))),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', order)).
% 60.65/60.90 fof(c26,plain,(![A]:(![B]:((~leq(A,B)|addition(A,B)=B)&(addition(A,B)!=B|leq(A,B))))),inference(fof_nnf,[status(thm)],[order])).
% 60.65/60.90 fof(c27,plain,((![A]:(![B]:(~leq(A,B)|addition(A,B)=B)))&(![A]:(![B]:(addition(A,B)!=B|leq(A,B))))),inference(shift_quantors,[status(thm)],[c26])).
% 60.65/60.90 fof(c29,plain,(![X12]:(![X13]:(![X14]:(![X15]:((~leq(X12,X13)|addition(X12,X13)=X13)&(addition(X14,X15)!=X15|leq(X14,X15))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X12]:(![X13]:(~leq(X12,X13)|addition(X12,X13)=X13)))&(![X14]:(![X15]:(addition(X14,X15)!=X15|leq(X14,X15))))),inference(variable_rename,[status(thm)],[c27])).])).
% 60.65/60.90 cnf(c30,plain,~leq(X105,X104)|addition(X105,X104)=X104,inference(split_conjunct,[status(thm)],[c29])).
% 60.65/60.90 fof(additive_identity,axiom,(![A]:addition(A,zero)=A),file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax', additive_identity)).
% 60.65/60.90 fof(c48,plain,(![X30]:addition(X30,zero)=X30),inference(variable_rename,[status(thm)],[additive_identity])).
% 60.65/60.90 cnf(c49,plain,addition(X48,zero)=X48,inference(split_conjunct,[status(thm)],[c48])).
% 60.65/60.90 cnf(c66,plain,X177!=addition(X176,zero)|X177=X176,inference(resolution,[status(thm)],[c49, transitivity])).
% 60.65/60.90 cnf(c558,plain,addition(zero,X184)=X184,inference(resolution,[status(thm)],[c66, c53])).
% 60.65/60.90 cnf(c637,plain,addition(zero,multiplication(X547,one))=X547,inference(resolution,[status(thm)],[c558, c64])).
% 60.65/60.90 cnf(c6,axiom,X98!=X100|X99!=X101|~leq(X98,X99)|leq(X100,X101),theory(equality)).
% 60.65/60.90 cnf(c31,plain,addition(X106,X107)!=X107|leq(X106,X107),inference(split_conjunct,[status(thm)],[c29])).
% 60.65/60.90 cnf(c633,plain,leq(zero,X185),inference(resolution,[status(thm)],[c558, c31])).
% 60.65/60.90 cnf(c644,plain,zero!=X1496|X1494!=X1495|leq(X1496,X1495),inference(resolution,[status(thm)],[c633, c6])).
% 60.65/60.90 cnf(c40670,plain,zero!=X1499|leq(X1499,X1498),inference(resolution,[status(thm)],[c644, c637])).
% 60.65/60.90 cnf(c41086,plain,leq(antidomain(one),X1505),inference(resolution,[status(thm)],[c40670, c531])).
% 60.65/60.90 cnf(c41224,plain,addition(antidomain(one),X1657)=X1657,inference(resolution,[status(thm)],[c41086, c30])).
% 60.65/60.90 cnf(c43946,plain,X1668=addition(antidomain(one),X1668),inference(resolution,[status(thm)],[c41224, symmetry])).
% 60.65/60.90 cnf(c44514,plain,X1677=addition(X1677,antidomain(one)),inference(resolution,[status(thm)],[c43946, c178])).
% 60.65/60.90 cnf(c44920,plain,antidomain(antidomain(one))=one,inference(resolution,[status(thm)],[c44514, c288])).
% 60.65/60.90 cnf(c46088,plain,one=antidomain(antidomain(one)),inference(resolution,[status(thm)],[c44920, symmetry])).
% 60.65/60.90 cnf(c46899,plain,one=domain(one),inference(resolution,[status(thm)],[c46088, c199])).
% 60.65/60.90 cnf(c47156,plain,domain(one)=one,inference(resolution,[status(thm)],[c46899, symmetry])).
% 60.65/60.90 cnf(c47245,plain,X2136!=domain(one)|X2136=one,inference(resolution,[status(thm)],[c47156, transitivity])).
% 60.65/60.90 cnf(c68568,plain,antidomain(zero)=one,inference(resolution,[status(thm)],[c47245, c13267])).
% 60.65/60.90 cnf(c68851,plain,antidomain(antidomain(zero))=antidomain(one),inference(resolution,[status(thm)],[c68568, c2])).
% 60.65/60.90 cnf(c103742,plain,antidomain(antidomain(zero))=zero,inference(resolution,[status(thm)],[c68851, c711])).
% 60.65/60.90 cnf(c103885,plain,zero=antidomain(antidomain(zero)),inference(resolution,[status(thm)],[c103742, symmetry])).
% 60.65/60.90 cnf(c103955,plain,zero=domain(zero),inference(resolution,[status(thm)],[c103885, c199])).
% 60.65/60.90 cnf(c104150,plain,domain(zero)=zero,inference(resolution,[status(thm)],[c103955, symmetry])).
% 60.65/60.90 cnf(c104428,plain,$false,inference(resolution,[status(thm)],[c104150, c9])).
% 60.65/60.90 % SZS output end CNFRefutation
% 60.65/60.90
% 60.65/60.90 % Initial clauses : 32
% 60.65/60.90 % Processed clauses : 1330
% 60.65/60.90 % Factors computed : 5
% 60.65/60.90 % Resolvents computed: 104421
% 60.65/60.90 % Tautologies deleted: 2
% 60.65/60.90 % Forward subsumed : 1591
% 60.65/60.90 % Backward subsumed : 67
% 60.65/60.90 % -------- CPU Time ---------
% 60.65/60.90 % User time : 60.309 s
% 60.65/60.90 % System time : 0.218 s
% 60.65/60.90 % Total time : 60.527 s
%------------------------------------------------------------------------------