%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX194+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:13:24 PM UTC 2026
% Result : Theorem 140.75s 23.36s
% Output : CNFRefutation 125.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 33
% Syntax : Number of formulae : 152 ( 107 unt; 0 def)
% Number of atoms : 216 ( 215 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 99 ( 35 ~; 53 |; 0 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 1 con; 0-2 aty)
% Number of variables : 303 ( 299 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X] : proj1Suc(suc(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : zero != suc(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,X2,X3] : n(X) != add(X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X,X2,X3] : n(X) != mul(X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X,X2,X3] : n(X) != eq(X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X,X2] : n(X) != v(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [X,X2,X3] : add(X,X2) != v(X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X,X2,X3] : mul(X,X2) != v(X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X,X2,X3] : eq(X,X2) != v(X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [Z,Y2] :
( Z != Y2
=> ( Z = Z
=> fail1(v(Z),v(Y2)) = mul(n(suc(suc(zero))),v(Z)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [Y,B] :
( B != n(proj1N(B))
=> fail(Y,B) = fail1(Y,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [C] : fail12(n(suc(zero)),C) = C,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X6] : fail2(X6,n(zero)) = n(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X6,X14] : fail2(X6,n(suc(X14))) = fail12(X6,n(suc(X14))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> ( X != mul(proj1Mul(X),proj2Mul(X))
=> ( X != eq(proj1Eq(X),proj2Eq(X))
=> step1(X) = X ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [Y,B] :
( Y != n(proj1N(Y))
=> step1(add(Y,B)) = fail(Y,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [C,X16] : step1(mul(n(suc(X16)),C)) = fail2(n(suc(X16)),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [A3,B2] :
( A3 = B2
=> step1(eq(A3,B2)) = n(suc(zero)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [X] :
( X != add(proj1Add(X),proj2Add(X))
=> ( X != mul(proj1Mul(X),proj2Mul(X))
=> ( X != eq(proj1Eq(X),proj2Eq(X))
=> simp1(X) = step1(X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A,B] : simp1(add(A,B)) = step1(add(simp1(A),simp1(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [C,B2] : simp1(mul(C,B2)) = step1(mul(simp1(C),simp1(B2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [A2,B3] : simp1(eq(A2,B3)) = step1(eq(simp1(A2),simp1(B3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
! [N,St] : fetch(cons(N,St),zero) = N,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [N,St,Z] : fetch(cons(N,St),suc(Z)) = fetch(St,Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [Y] : addNat(zero,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [Y,Z] : addNat(suc(Z),Y) = suc(addNat(Z,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [Y] : mulNat(zero,Y) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,axiom,
! [Y,Z] : mulNat(suc(Z),Y) = addNat(Y,mulNat(Z,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X,N] : eval(X,n(N)) = N,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X,A,B] : eval(X,add(A,B)) = addNat(eval(X,A),eval(X,B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X,C,B2] : eval(X,mul(C,B2)) = mulNat(eval(X,C),eval(X,B2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X,Z] : eval(X,v(Z)) = fetch(X,Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,conjecture,
? [St,A] : eval(St,A) != eval(St,simp1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,negated_conjecture,
~ ? [St,A] : eval(St,A) != eval(St,simp1(A)),
inference(negated_conjecture,[status(cth)],[f72]) ).
fof(f77,plain,
! [X0] : proj1Suc(suc(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f78,plain,
! [X0] : zero != suc(X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f87,plain,
! [X0,X1,X2] : n(X0) != add(X1,X2),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f88,plain,
! [X0,X1,X2] : n(X0) != mul(X1,X2),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f89,plain,
! [X0,X1,X2] : n(X0) != eq(X1,X2),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f90,plain,
! [X0,X1] : n(X0) != v(X1),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f93,plain,
! [X0,X1,X2] : add(X0,X1) != v(X2),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f95,plain,
! [X0,X1,X2] : mul(X0,X1) != v(X2),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f96,plain,
! [X0,X1,X2] : eq(X0,X1) != v(X2),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f105,plain,
! [Z,Y2] :
( fail1(v(Z),v(Y2)) = mul(n(suc(suc(zero))),v(Z))
| Z != Z
| Z = Y2 ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f106,plain,
! [X0,X1] :
( fail1(v(X0),v(X1)) = mul(n(suc(suc(zero))),v(X0))
| X0 != X0
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f109,plain,
! [Y,B] :
( fail(Y,B) = fail1(Y,B)
| B = n(proj1N(B)) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f110,plain,
! [B] :
( ! [Y] : fail(Y,B) = fail1(Y,B)
| B = n(proj1N(B)) ),
inference(miniscoping,[status(thm)],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( fail(X1,X0) = fail1(X1,X0)
| X0 = n(proj1N(X0)) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f128,plain,
! [X0] : fail12(n(suc(zero)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f133,plain,
! [X0] : fail2(X0,n(zero)) = n(zero),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f134,plain,
! [X0,X1] : fail2(X0,n(suc(X1))) = fail12(X0,n(suc(X1))),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f135,plain,
! [X] :
( step1(X) = X
| X = eq(proj1Eq(X),proj2Eq(X))
| X = mul(proj1Mul(X),proj2Mul(X))
| X = add(proj1Add(X),proj2Add(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f136,plain,
! [X0] :
( step1(X0) = X0
| X0 = eq(proj1Eq(X0),proj2Eq(X0))
| X0 = mul(proj1Mul(X0),proj2Mul(X0))
| X0 = add(proj1Add(X0),proj2Add(X0)) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
! [Y,B] :
( step1(add(Y,B)) = fail(Y,B)
| Y = n(proj1N(Y)) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f138,plain,
! [Y] :
( ! [B] : step1(add(Y,B)) = fail(Y,B)
| Y = n(proj1N(Y)) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0,X1] :
( step1(add(X0,X1)) = fail(X0,X1)
| X0 = n(proj1N(X0)) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f146,plain,
! [X0,X1] : step1(mul(n(suc(X0)),X1)) = fail2(n(suc(X0)),X1),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f147,plain,
! [A3,B2] :
( step1(eq(A3,B2)) = n(suc(zero))
| A3 != B2 ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f148,plain,
! [X0,X1] :
( step1(eq(X0,X1)) = n(suc(zero))
| X0 != X1 ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f151,plain,
! [X] :
( simp1(X) = step1(X)
| X = eq(proj1Eq(X),proj2Eq(X))
| X = mul(proj1Mul(X),proj2Mul(X))
| X = add(proj1Add(X),proj2Add(X)) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f152,plain,
! [X0] :
( simp1(X0) = step1(X0)
| X0 = eq(proj1Eq(X0),proj2Eq(X0))
| X0 = mul(proj1Mul(X0),proj2Mul(X0))
| X0 = add(proj1Add(X0),proj2Add(X0)) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0,X1] : simp1(add(X0,X1)) = step1(add(simp1(X0),simp1(X1))),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f154,plain,
! [X0,X1] : simp1(mul(X0,X1)) = step1(mul(simp1(X0),simp1(X1))),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f155,plain,
! [X0,X1] : simp1(eq(X0,X1)) = step1(eq(simp1(X0),simp1(X1))),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f157,plain,
! [X0,X1] : fetch(cons(X0,X1),zero) = X0,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f158,plain,
! [X0,X1,X2] : fetch(cons(X0,X1),suc(X2)) = fetch(X1,X2),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f159,plain,
! [X0] : addNat(zero,X0) = X0,
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f160,plain,
! [X0,X1] : addNat(suc(X0),X1) = suc(addNat(X0,X1)),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f161,plain,
! [X0] : mulNat(zero,X0) = zero,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f162,plain,
! [X0,X1] : mulNat(suc(X0),X1) = addNat(X1,mulNat(X0,X1)),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f163,plain,
! [X0,X1] : eval(X0,n(X1)) = X1,
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f164,plain,
! [X0,X1,X2] : eval(X0,add(X1,X2)) = addNat(eval(X0,X1),eval(X0,X2)),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f165,plain,
! [X0,X1,X2] : eval(X0,mul(X1,X2)) = mulNat(eval(X0,X1),eval(X0,X2)),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f170,plain,
! [X0,X1] : eval(X0,v(X1)) = fetch(X0,X1),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f171,plain,
! [St,A] : eval(St,A) = eval(St,simp1(A)),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f172,plain,
! [X0,X1] : eval(X0,X1) = eval(X0,simp1(X1)),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f174,plain,
! [X0,X1] :
( fail1(v(X0),v(X1)) = mul(n(suc(suc(zero))),v(X0))
| X0 = X1 ),
inference(trivial_equality_resolution,[status(thm)],[f106]) ).
fof(f175,plain,
! [X0] : step1(eq(X0,X0)) = n(suc(zero)),
inference(destructive_equality_resolution,[status(thm)],[f148]) ).
fof(f176,plain,
! [X0] : simp1(eq(X0,X0)) = n(suc(zero)),
inference(paramodulation,[status(thm)],[f155,f175]) ).
fof(f197,plain,
! [X0,X1] : simp1(mul(eq(X0,X0),X1)) = step1(mul(n(suc(zero)),simp1(X1))),
inference(paramodulation,[status(thm)],[f176,f154]) ).
fof(f200,plain,
! [X0,X1] : eval(X0,eq(X1,X1)) = eval(X0,n(suc(zero))),
inference(paramodulation,[status(thm)],[f176,f172]) ).
fof(f201,plain,
! [X0,X1] : eval(X0,eq(X1,X1)) = suc(zero),
inference(forward_demodulation,[status(thm)],[f163,f200]) ).
fof(f592,plain,
! [X0,X1] : mulNat(suc(X0),suc(X1)) = suc(addNat(X1,mulNat(X0,suc(X1)))),
inference(paramodulation,[status(thm)],[f160,f162]) ).
fof(f593,plain,
! [X0] : mulNat(suc(X0),zero) = mulNat(X0,zero),
inference(paramodulation,[status(thm)],[f159,f162]) ).
fof(f594,plain,
! [X0] : mulNat(suc(zero),X0) = addNat(X0,zero),
inference(paramodulation,[status(thm)],[f161,f162]) ).
fof(f1376,plain,
! [X0,X1] :
( simp1(add(X0,X1)) = fail(simp1(X0),simp1(X1))
| simp1(X0) = n(proj1N(simp1(X0))) ),
inference(paramodulation,[status(thm)],[f153,f139]) ).
fof(f1420,plain,
! [X0,X1,X2] : eval(X0,add(v(X1),X2)) = addNat(fetch(X0,X1),eval(X0,X2)),
inference(paramodulation,[status(thm)],[f170,f164]) ).
fof(f1598,plain,
! [X0] :
( step1(n(X0)) = n(X0)
| n(X0) = eq(proj1Eq(n(X0)),proj2Eq(n(X0)))
| n(X0) = add(proj1Add(n(X0)),proj2Add(n(X0))) ),
inference(resolution,[status(thm)],[f136,f88]) ).
fof(f1601,plain,
! [X0] :
( step1(v(X0)) = v(X0)
| v(X0) = eq(proj1Eq(v(X0)),proj2Eq(v(X0)))
| v(X0) = add(proj1Add(v(X0)),proj2Add(v(X0))) ),
inference(resolution,[status(thm)],[f136,f95]) ).
fof(f1623,plain,
! [X0] :
( step1(n(X0)) = n(X0)
| n(X0) = eq(proj1Eq(n(X0)),proj2Eq(n(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1598,f87]) ).
fof(f1626,plain,
! [X0] :
( step1(v(X0)) = v(X0)
| v(X0) = eq(proj1Eq(v(X0)),proj2Eq(v(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1601,f93]) ).
fof(f2045,plain,
! [X0,X1,X2] : eval(X0,mul(eq(X1,X1),X2)) = mulNat(suc(zero),eval(X0,X2)),
inference(paramodulation,[status(thm)],[f201,f165]) ).
fof(f2047,plain,
! [X0,X1,X2] : eval(X0,mul(n(X1),X2)) = mulNat(X1,eval(X0,X2)),
inference(paramodulation,[status(thm)],[f163,f165]) ).
fof(f2102,plain,
! [X0,X1,X2] : eval(X0,mul(eq(X1,X1),X2)) = addNat(eval(X0,X2),zero),
inference(forward_demodulation,[status(thm)],[f594,f2045]) ).
fof(f2128,plain,
! [X0,X1,X2] :
( X1 = X2
| eval(X0,fail1(v(X1),v(X2))) = mulNat(suc(suc(zero)),eval(X0,v(X1))) ),
inference(paramodulation,[status(thm)],[f174,f2047]) ).
fof(f2142,plain,
! [X0,X1,X2] :
( X1 = X2
| eval(X0,fail1(v(X1),v(X2))) = mulNat(suc(suc(zero)),fetch(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f170,f2128]) ).
fof(f2375,plain,
! [X0,X1] : simp1(mul(eq(X0,X0),X1)) = fail2(n(suc(zero)),simp1(X1)),
inference(backward_demodulation,[status(thm)],[f146,f197]) ).
fof(f2528,plain,
! [X0,X1,X2] : addNat(mulNat(suc(X0),suc(X1)),X2) = suc(addNat(addNat(X1,mulNat(X0,suc(X1))),X2)),
inference(paramodulation,[status(thm)],[f592,f160]) ).
fof(f2529,plain,
! [X0,X1] : proj1Suc(mulNat(suc(X0),suc(X1))) = addNat(X1,mulNat(X0,suc(X1))),
inference(paramodulation,[status(thm)],[f592,f77]) ).
fof(f2541,plain,
! [X0] :
( simp1(n(X0)) = step1(n(X0))
| n(X0) = eq(proj1Eq(n(X0)),proj2Eq(n(X0)))
| n(X0) = add(proj1Add(n(X0)),proj2Add(n(X0))) ),
inference(resolution,[status(thm)],[f152,f88]) ).
fof(f2544,plain,
! [X0] :
( simp1(v(X0)) = step1(v(X0))
| v(X0) = eq(proj1Eq(v(X0)),proj2Eq(v(X0)))
| v(X0) = add(proj1Add(v(X0)),proj2Add(v(X0))) ),
inference(resolution,[status(thm)],[f152,f95]) ).
fof(f2568,plain,
! [X0] :
( simp1(n(X0)) = step1(n(X0))
| n(X0) = eq(proj1Eq(n(X0)),proj2Eq(n(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2541,f87]) ).
fof(f2571,plain,
! [X0] :
( simp1(v(X0)) = step1(v(X0))
| v(X0) = eq(proj1Eq(v(X0)),proj2Eq(v(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2544,f93]) ).
fof(f2926,plain,
! [X0,X1,X2] : eval(X0,mul(eq(X1,X1),X2)) = eval(X0,fail2(n(suc(zero)),simp1(X2))),
inference(paramodulation,[status(thm)],[f2375,f172]) ).
fof(f2967,plain,
! [X0,X1] : addNat(eval(X0,X1),zero) = eval(X0,fail2(n(suc(zero)),simp1(X1))),
inference(forward_demodulation,[status(thm)],[f2102,f2926]) ).
fof(f4148,plain,
! [X0,X1,X2] : eval(cons(X0,X1),add(v(zero),X2)) = addNat(X0,eval(cons(X0,X1),X2)),
inference(paramodulation,[status(thm)],[f157,f1420]) ).
fof(f4519,plain,
! [X0] : step1(n(X0)) = n(X0),
inference(forward_subsumption_resolution,[status(thm)],[f1623,f89]) ).
fof(f4520,plain,
! [X0] : step1(v(X0)) = v(X0),
inference(forward_subsumption_resolution,[status(thm)],[f1626,f96]) ).
fof(f11520,plain,
! [X0] :
( simp1(n(X0)) = n(X0)
| n(X0) = eq(proj1Eq(n(X0)),proj2Eq(n(X0))) ),
inference(forward_demodulation,[status(thm)],[f4519,f2568]) ).
fof(f11541,plain,
! [X0] : simp1(n(X0)) = n(X0),
inference(forward_subsumption_resolution,[status(thm)],[f11520,f89]) ).
fof(f11546,plain,
! [X0,X1] : addNat(eval(X0,n(X1)),zero) = eval(X0,fail2(n(suc(zero)),n(X1))),
inference(paramodulation,[status(thm)],[f11541,f2967]) ).
fof(f11582,plain,
! [X0,X1] : simp1(mul(X0,n(X1))) = step1(mul(simp1(X0),n(X1))),
inference(paramodulation,[status(thm)],[f11541,f154]) ).
fof(f11605,plain,
! [X0,X1] : addNat(X0,zero) = eval(X1,fail2(n(suc(zero)),n(X0))),
inference(forward_demodulation,[status(thm)],[f163,f11546]) ).
fof(f11646,plain,
! [X0,X1] : addNat(suc(X0),zero) = eval(X1,fail12(n(suc(zero)),n(suc(X0)))),
inference(paramodulation,[status(thm)],[f134,f11605]) ).
fof(f11670,plain,
! [X0,X1] : suc(addNat(X0,zero)) = eval(X1,fail12(n(suc(zero)),n(suc(X0)))),
inference(forward_demodulation,[status(thm)],[f160,f11646]) ).
fof(f11671,plain,
! [X0,X1] : suc(addNat(X0,zero)) = eval(X1,n(suc(X0))),
inference(forward_demodulation,[status(thm)],[f128,f11670]) ).
fof(f11672,plain,
! [X0] : suc(addNat(X0,zero)) = suc(X0),
inference(forward_demodulation,[status(thm)],[f163,f11671]) ).
fof(f11739,plain,
! [X0] : proj1Suc(suc(X0)) = addNat(X0,zero),
inference(paramodulation,[status(thm)],[f11672,f77]) ).
fof(f11754,plain,
! [X0] : X0 = addNat(X0,zero),
inference(forward_demodulation,[status(thm)],[f77,f11739]) ).
fof(f11771,plain,
! [X0] : mulNat(suc(zero),X0) = X0,
inference(backward_demodulation,[status(thm)],[f11754,f594]) ).
fof(f12379,plain,
! [X0,X1] : simp1(mul(n(X0),n(X1))) = step1(mul(n(X0),n(X1))),
inference(paramodulation,[status(thm)],[f11541,f11582]) ).
fof(f14198,plain,
! [X0] :
( simp1(v(X0)) = v(X0)
| v(X0) = eq(proj1Eq(v(X0)),proj2Eq(v(X0))) ),
inference(forward_demodulation,[status(thm)],[f4520,f2571]) ).
fof(f14199,plain,
! [X0] : simp1(v(X0)) = v(X0),
inference(forward_subsumption_resolution,[status(thm)],[f14198,f96]) ).
fof(f14230,plain,
! [X0,X1] :
( simp1(add(v(X0),X1)) = fail(v(X0),simp1(X1))
| simp1(v(X0)) = n(proj1N(simp1(v(X0)))) ),
inference(paramodulation,[status(thm)],[f14199,f1376]) ).
fof(f14254,plain,
! [X0,X1] :
( simp1(add(v(X0),X1)) = fail(v(X0),simp1(X1))
| v(X0) = n(proj1N(simp1(v(X0)))) ),
inference(forward_demodulation,[status(thm)],[f14199,f14230]) ).
fof(f14255,plain,
! [X0,X1] :
( simp1(add(v(X0),X1)) = fail(v(X0),simp1(X1))
| v(X0) = n(proj1N(v(X0))) ),
inference(forward_demodulation,[status(thm)],[f14199,f14254]) ).
fof(f14256,plain,
! [X0,X1] : simp1(add(v(X0),X1)) = fail(v(X0),simp1(X1)),
inference(forward_subsumption_resolution,[status(thm)],[f14255,f90]) ).
fof(f14566,plain,
! [X0,X1,X2] : eval(X0,add(v(X1),X2)) = eval(X0,fail(v(X1),simp1(X2))),
inference(paramodulation,[status(thm)],[f14256,f172]) ).
fof(f19600,plain,
! [X0,X1,X2] : eval(X0,mul(n(X1),n(X2))) = eval(X0,step1(mul(n(X1),n(X2)))),
inference(paramodulation,[status(thm)],[f12379,f172]) ).
fof(f19618,plain,
! [X0,X1,X2] : mulNat(X0,eval(X1,n(X2))) = eval(X1,step1(mul(n(X0),n(X2)))),
inference(forward_demodulation,[status(thm)],[f2047,f19600]) ).
fof(f19619,plain,
! [X0,X1,X2] : mulNat(X0,X1) = eval(X2,step1(mul(n(X0),n(X1)))),
inference(forward_demodulation,[status(thm)],[f163,f19618]) ).
fof(f19621,plain,
! [X0,X1,X2] : mulNat(suc(X0),X1) = eval(X2,fail2(n(suc(X0)),n(X1))),
inference(paramodulation,[status(thm)],[f146,f19619]) ).
fof(f19658,plain,
! [X0,X1] : mulNat(suc(X0),zero) = eval(X1,n(zero)),
inference(paramodulation,[status(thm)],[f133,f19621]) ).
fof(f19693,plain,
! [X0] : mulNat(suc(X0),zero) = zero,
inference(forward_demodulation,[status(thm)],[f163,f19658]) ).
fof(f19697,plain,
! [X0] : zero = mulNat(X0,zero),
inference(backward_demodulation,[status(thm)],[f19693,f593]) ).
fof(f30009,plain,
! [X0,X1,X2] : eval(X0,add(v(X1),v(X2))) = eval(X0,fail(v(X1),v(X2))),
inference(paramodulation,[status(thm)],[f14199,f14566]) ).
fof(f43037,plain,
! [X0,X1,X2] : addNat(mulNat(suc(X0),suc(X1)),X2) = suc(addNat(proj1Suc(mulNat(suc(X0),suc(X1))),X2)),
inference(forward_demodulation,[status(thm)],[f2529,f2528]) ).
fof(f43129,plain,
! [X0,X1,X2] : zero != addNat(mulNat(suc(X0),suc(X1)),X2),
inference(paramodulation,[status(thm)],[f43037,f78]) ).
fof(f78875,plain,
! [X0,X1,X2,X3] : zero != eval(cons(mulNat(suc(X0),suc(X1)),X2),add(v(zero),X3)),
inference(paramodulation,[status(thm)],[f4148,f43129]) ).
fof(f92992,plain,
! [X0,X1,X2] :
( v(X2) = n(proj1N(v(X2)))
| eval(X0,add(v(X1),v(X2))) = eval(X0,fail1(v(X1),v(X2))) ),
inference(paramodulation,[status(thm)],[f111,f30009]) ).
fof(f93077,plain,
! [X0,X1,X2] : eval(X0,add(v(X1),v(X2))) = eval(X0,fail1(v(X1),v(X2))),
inference(forward_subsumption_resolution,[status(thm)],[f92992,f90]) ).
fof(f101006,plain,
! [X0,X1,X2] : zero != eval(cons(suc(X0),X1),add(v(zero),X2)),
inference(paramodulation,[status(thm)],[f11771,f78875]) ).
fof(f106502,plain,
! [X0,X1,X2] :
( X1 = X2
| eval(X0,add(v(X1),v(X2))) = mulNat(suc(suc(zero)),fetch(X0,X1)) ),
inference(backward_demodulation,[status(thm)],[f93077,f2142]) ).
fof(f151547,plain,
! [X0,X1,X2] :
( zero = X2
| addNat(X0,eval(cons(X0,X1),v(X2))) = mulNat(suc(suc(zero)),fetch(cons(X0,X1),zero)) ),
inference(paramodulation,[status(thm)],[f4148,f106502]) ).
fof(f151667,plain,
! [X0,X1,X2] :
( zero = X2
| addNat(X0,fetch(cons(X0,X1),X2)) = mulNat(suc(suc(zero)),fetch(cons(X0,X1),zero)) ),
inference(forward_demodulation,[status(thm)],[f170,f151547]) ).
fof(f151668,plain,
! [X0,X1,X2] :
( zero = X2
| addNat(X0,fetch(cons(X0,X1),X2)) = mulNat(suc(suc(zero)),X0) ),
inference(forward_demodulation,[status(thm)],[f157,f151667]) ).
fof(f151703,plain,
! [X0,X1] :
( zero = X1
| fetch(cons(zero,X0),X1) = mulNat(suc(suc(zero)),zero) ),
inference(paramodulation,[status(thm)],[f159,f151668]) ).
fof(f151745,plain,
! [X0,X1] :
( zero = X1
| fetch(cons(zero,X0),X1) = zero ),
inference(forward_demodulation,[status(thm)],[f19697,f151703]) ).
fof(f151754,plain,
! [X0,X1] :
( zero = suc(X1)
| fetch(X0,X1) = zero ),
inference(paramodulation,[status(thm)],[f158,f151745]) ).
fof(f151791,plain,
! [X0,X1] : fetch(X0,X1) = zero,
inference(forward_subsumption_resolution,[status(thm)],[f151754,f78]) ).
fof(f151828,plain,
! [X0] : zero = X0,
inference(backward_demodulation,[status(thm)],[f151791,f157]) ).
fof(f151925,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f101006,f151828]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX194+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n002.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 10:34:39 UTC 2026
% 0.16/5.43 % CPUTime :
% 0.16/5.45 % Drodi V4.1.1
% 140.75/23.36 % Refutation found
% 140.75/23.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 140.75/23.36 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 125.73/23.60 % Elapsed time: 18.138230 seconds
% 125.73/23.60 % CPU time: 142.565238 seconds
% 125.73/23.60 % Total memory used: 899.401 MB
% 125.73/23.60 % Net memory used: 812.304 MB
%------------------------------------------------------------------------------