%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX210-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 : Sun Sep 27 09:16:21 AM UTC 2026
% Result : Unsatisfiable 203.98s 27.00s
% Output : CNFRefutation 203.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 28
% Syntax : Number of formulae : 259 ( 259 unt; 0 def)
% Number of atoms : 259 ( 258 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 47 ( 47 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 7 con; 0-4 aty)
% Number of variables : 467 ( 78 sgn 39 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom,axiom,
! [VAR_0,VAR_1] : aux(VAR_0,VAR_1,btrue) = eps,
file('theBenchmark.p',axiom) ).
cnf(c_1,plain,
aux(A,B,btrue) = eps,
inference(clausify,[status(thm)],[axiom]) ).
fof(axiom_001,axiom,
! [VAR_0,VAR_1] : aux(VAR_0,VAR_1,bfalse) = nil2,
file('theBenchmark.p',axiom_001) ).
cnf(c_2,plain,
aux(A,B,bfalse) = nil2,
inference(clausify,[status(thm)],[axiom_001]) ).
fof(axiom_002,axiom,
! [VAR_0,VAR_1,VAR_2] : aux2(VAR_0,VAR_1,VAR_2,btrue) = x(y(step(VAR_1,VAR_0),VAR_2),step(VAR_2,VAR_0)),
file('theBenchmark.p',axiom_002) ).
cnf(c_3,plain,
aux2(A,B,C,btrue) = x(y(step(B,A),C),step(C,A)),
inference(clausify,[status(thm)],[axiom_002]) ).
fof(axiom_003,axiom,
! [VAR_0,VAR_1,VAR_2] : aux2(VAR_0,VAR_1,VAR_2,bfalse) = x(y(step(VAR_1,VAR_0),VAR_2),nil2),
file('theBenchmark.p',axiom_003) ).
cnf(c_4,plain,
aux2(A,B,C,bfalse) = x(y(step(B,A),C),nil2),
inference(clausify,[status(thm)],[axiom_003]) ).
fof(axiom_061,axiom,
! [VAR_0] : orb(btrue,VAR_0) = btrue,
file('theBenchmark.p',axiom_061) ).
cnf(c_62,plain,
orb(btrue,A) = btrue,
inference(clausify,[status(thm)],[axiom_061]) ).
fof(axiom_062,axiom,
! [VAR_0] : orb(bfalse,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_062) ).
cnf(c_63,plain,
orb(bfalse,A) = A,
inference(clausify,[status(thm)],[axiom_062]) ).
fof(axiom_063,axiom,
notb(btrue) = bfalse,
file('theBenchmark.p',axiom_063) ).
cnf(c_64,plain,
notb(btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_063]) ).
fof(axiom_065,axiom,
! [VAR_0] : andb(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_065) ).
cnf(c_66,plain,
andb(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_065]) ).
fof(axiom_066,axiom,
! [VAR_0] : andb(bfalse,VAR_0) = bfalse,
file('theBenchmark.p',axiom_066) ).
cnf(c_67,plain,
andb(bfalse,A) = bfalse,
inference(clausify,[status(thm)],[axiom_066]) ).
fof(axiom_067,axiom,
eps2(eps) = btrue,
file('theBenchmark.p',axiom_067) ).
cnf(c_68,plain,
eps2(eps) = btrue,
inference(clausify,[status(thm)],[axiom_067]) ).
fof(axiom_068,axiom,
! [VAR_0,VAR_1] : eps2(x(VAR_0,VAR_1)) = orb(eps2(VAR_0),eps2(VAR_1)),
file('theBenchmark.p',axiom_068) ).
cnf(c_69,plain,
eps2(x(A,B)) = orb(eps2(A),eps2(B)),
inference(clausify,[status(thm)],[axiom_068]) ).
fof(axiom_069,axiom,
! [VAR_0,VAR_1] : eps2(y(VAR_0,VAR_1)) = andb(eps2(VAR_0),eps2(VAR_1)),
file('theBenchmark.p',axiom_069) ).
cnf(c_70,plain,
eps2(y(A,B)) = andb(eps2(A),eps2(B)),
inference(clausify,[status(thm)],[axiom_069]) ).
fof(axiom_070,axiom,
! [VAR_0] : eps2(star(VAR_0)) = btrue,
file('theBenchmark.p',axiom_070) ).
cnf(c_71,plain,
eps2(star(A)) = btrue,
inference(clausify,[status(thm)],[axiom_070]) ).
fof(axiom_071,axiom,
eps2(nil2) = bfalse,
file('theBenchmark.p',axiom_071) ).
cnf(c_72,plain,
eps2(nil2) = bfalse,
inference(clausify,[status(thm)],[axiom_071]) ).
fof(axiom_073,axiom,
! [VAR_0,VAR_1] : step(atom(VAR_0),VAR_1) = aux(VAR_1,VAR_0,eq(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_073) ).
cnf(c_74,plain,
step(atom(A),B) = aux(B,A,eq(A,B)),
inference(clausify,[status(thm)],[axiom_073]) ).
cnf(c_75,plain,
aux(A,B,eq(B,A)) = step(atom(B),A),
inference(copy,[status(thm)],[c_74]) ).
fof(axiom_074,axiom,
! [VAR_0,VAR_1,VAR_2] : step(x(VAR_0,VAR_1),VAR_2) = x(step(VAR_0,VAR_2),step(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_074) ).
cnf(c_76,plain,
step(x(A,B),C) = x(step(A,C),step(B,C)),
inference(clausify,[status(thm)],[axiom_074]) ).
fof(axiom_075,axiom,
! [VAR_0,VAR_1,VAR_2] : step(y(VAR_0,VAR_1),VAR_2) = aux2(VAR_2,VAR_0,VAR_1,eps2(VAR_0)),
file('theBenchmark.p',axiom_075) ).
cnf(c_77,plain,
step(y(A,B),C) = aux2(C,A,B,eps2(A)),
inference(clausify,[status(thm)],[axiom_075]) ).
cnf(c_78,plain,
aux2(A,B,C,eps2(B)) = step(y(B,C),A),
inference(copy,[status(thm)],[c_77]) ).
fof(axiom_076,axiom,
! [VAR_0,VAR_1] : step(star(VAR_0),VAR_1) = y(step(VAR_0,VAR_1),star(VAR_0)),
file('theBenchmark.p',axiom_076) ).
cnf(c_79,plain,
step(star(A),B) = y(step(A,B),star(A)),
inference(clausify,[status(thm)],[axiom_076]) ).
fof(axiom_077,axiom,
! [VAR_0] : step(nil2,VAR_0) = nil2,
file('theBenchmark.p',axiom_077) ).
cnf(c_80,plain,
step(nil2,A) = nil2,
inference(clausify,[status(thm)],[axiom_077]) ).
fof(axiom_078,axiom,
! [VAR_0] : step(eps,VAR_0) = nil2,
file('theBenchmark.p',axiom_078) ).
cnf(c_81,plain,
step(eps,A) = nil2,
inference(clausify,[status(thm)],[axiom_078]) ).
fof(axiom_079,axiom,
! [VAR_0] : rec(VAR_0,nil) = eps2(VAR_0),
file('theBenchmark.p',axiom_079) ).
cnf(c_82,plain,
rec(A,nil) = eps2(A),
inference(clausify,[status(thm)],[axiom_079]) ).
cnf(c_83,plain,
eps2(A) = rec(A,nil),
inference(copy,[status(thm)],[c_82]) ).
fof(axiom_080,axiom,
! [VAR_0,VAR_1,VAR_2] : rec(VAR_0,cons(VAR_1,VAR_2)) = rec(step(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',axiom_080) ).
cnf(c_84,plain,
rec(A,cons(B,C)) = rec(step(A,B),C),
inference(clausify,[status(thm)],[axiom_080]) ).
cnf(c_85,plain,
rec(step(A,B),C) = rec(A,cons(B,C)),
inference(copy,[status(thm)],[c_84]) ).
fof(axiom_081,axiom,
! [VAR_0] : prop_find4(VAR_0) = notb(rec(VAR_0,cons(a,cons(b,cons(b,cons(a,nil)))))),
file('theBenchmark.p',axiom_081) ).
cnf(c_86,plain,
prop_find4(A) = notb(rec(A,cons(a,cons(b,cons(b,cons(a,nil)))))),
inference(clausify,[status(thm)],[axiom_081]) ).
fof(axiom_082,axiom,
eq(a,b) = bfalse,
file('theBenchmark.p',axiom_082) ).
cnf(c_87,plain,
eq(a,b) = bfalse,
inference(clausify,[status(thm)],[axiom_082]) ).
fof(axiom_084,axiom,
eq(b,a) = bfalse,
file('theBenchmark.p',axiom_084) ).
cnf(c_89,plain,
eq(b,a) = bfalse,
inference(clausify,[status(thm)],[axiom_084]) ).
fof(axiom_090,axiom,
! [VAR_0] : eq(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_090) ).
cnf(c_95,plain,
eq(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_090]) ).
fof(axiom_091,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_091) ).
cnf(c_96,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_091]) ).
fof(goal,axiom,
! [VAR_0] : eq2(prop_find4(VAR_0),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_97,plain,
eq2(prop_find4(A),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_98,plain,
eq2(notb(rec(A,cons(a,cons(b,cons(b,cons(a,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_86,c_97]) ).
cnf(c_99,plain,
aux2(A,B,C,rec(B,nil)) = step(y(B,C),A),
inference(paramod,[status(thm)],[c_83,c_78]) ).
cnf(c_101,plain,
rec(nil2,nil) = bfalse,
inference(paramod,[status(thm)],[c_83,c_72]) ).
cnf(c_102,plain,
rec(star(A),nil) = btrue,
inference(paramod,[status(thm)],[c_83,c_71]) ).
cnf(c_2981,plain,
rec(y(A,B),nil) = andb(eps2(A),eps2(B)),
inference(paramod,[status(thm)],[c_83,c_70]) ).
cnf(c_2982,plain,
rec(y(A,B),nil) = andb(rec(A,nil),eps2(B)),
inference(paramod,[status(thm)],[c_83,c_2981]) ).
cnf(c_2983,plain,
rec(y(A,B),nil) = andb(rec(A,nil),rec(B,nil)),
inference(paramod,[status(thm)],[c_83,c_2982]) ).
cnf(c_103,plain,
andb(rec(A,nil),rec(B,nil)) = rec(y(A,B),nil),
inference(copy,[status(thm)],[c_2983]) ).
cnf(c_2984,plain,
rec(x(A,B),nil) = orb(eps2(A),eps2(B)),
inference(paramod,[status(thm)],[c_83,c_69]) ).
cnf(c_2985,plain,
rec(x(A,B),nil) = orb(rec(A,nil),eps2(B)),
inference(paramod,[status(thm)],[c_83,c_2984]) ).
cnf(c_2986,plain,
rec(x(A,B),nil) = orb(rec(A,nil),rec(B,nil)),
inference(paramod,[status(thm)],[c_83,c_2985]) ).
cnf(c_104,plain,
orb(rec(A,nil),rec(B,nil)) = rec(x(A,B),nil),
inference(copy,[status(thm)],[c_2986]) ).
cnf(c_105,plain,
rec(eps,nil) = btrue,
inference(paramod,[status(thm)],[c_83,c_68]) ).
cnf(c_106,plain,
rec(x(step(A,B),step(C,B)),D) = rec(x(A,C),cons(B,D)),
inference(paramod,[status(thm)],[c_76,c_85]) ).
cnf(c_2987,plain,
rec(y(step(A,B),star(A)),C) = rec(star(A),cons(B,C)),
inference(paramod,[status(thm)],[c_79,c_85]) ).
cnf(c_107,plain,
rec(star(A),cons(B,C)) = rec(y(step(A,B),star(A)),C),
inference(copy,[status(thm)],[c_2987]) ).
cnf(c_108,plain,
rec(step(step(A,B),C),D) = rec(A,cons(B,cons(C,D))),
inference(paramod,[status(thm)],[c_85,c_85]) ).
cnf(c_2988,plain,
aux(b,a,bfalse) = step(atom(a),b),
inference(paramod,[status(thm)],[c_87,c_75]) ).
cnf(c_2989,plain,
nil2 = step(atom(a),b),
inference(paramod,[status(thm)],[c_2,c_2988]) ).
cnf(c_109,plain,
step(atom(a),b) = nil2,
inference(copy,[status(thm)],[c_2989]) ).
cnf(c_2990,plain,
aux(a,b,bfalse) = step(atom(b),a),
inference(paramod,[status(thm)],[c_89,c_75]) ).
cnf(c_2991,plain,
nil2 = step(atom(b),a),
inference(paramod,[status(thm)],[c_2,c_2990]) ).
cnf(c_111,plain,
step(atom(b),a) = nil2,
inference(copy,[status(thm)],[c_2991]) ).
cnf(c_2992,plain,
aux(A,A,btrue) = step(atom(A),A),
inference(paramod,[status(thm)],[c_95,c_75]) ).
cnf(c_2993,plain,
eps = step(atom(A),A),
inference(paramod,[status(thm)],[c_1,c_2992]) ).
cnf(c_115,plain,
step(atom(A),A) = eps,
inference(copy,[status(thm)],[c_2993]) ).
cnf(c_118,plain,
aux2(A,step(B,C),D,rec(B,cons(C,nil))) = step(y(step(B,C),D),A),
inference(paramod,[status(thm)],[c_85,c_99]) ).
cnf(c_2994,plain,
aux2(A,nil2,B,bfalse) = step(y(nil2,B),A),
inference(paramod,[status(thm)],[c_101,c_99]) ).
cnf(c_2995,plain,
x(y(step(nil2,A),B),nil2) = step(y(nil2,B),A),
inference(paramod,[status(thm)],[c_4,c_2994]) ).
cnf(c_2996,plain,
x(y(nil2,B),nil2) = step(y(nil2,B),A),
inference(paramod,[status(thm)],[c_80,c_2995]) ).
cnf(c_120,plain,
step(y(nil2,A),B) = x(y(nil2,A),nil2),
inference(copy,[status(thm)],[c_2996]) ).
cnf(c_2997,plain,
andb(bfalse,rec(A,nil)) = rec(y(nil2,A),nil),
inference(paramod,[status(thm)],[c_101,c_103]) ).
cnf(c_2998,plain,
bfalse = rec(y(nil2,A),nil),
inference(paramod,[status(thm)],[c_67,c_2997]) ).
cnf(c_126,plain,
rec(y(nil2,A),nil) = bfalse,
inference(copy,[status(thm)],[c_2998]) ).
cnf(c_2999,plain,
andb(rec(A,nil),btrue) = rec(y(A,star(B)),nil),
inference(paramod,[status(thm)],[c_102,c_103]) ).
cnf(c_129,plain,
rec(y(A,star(B)),nil) = andb(rec(A,nil),btrue),
inference(copy,[status(thm)],[c_2999]) ).
cnf(c_131,plain,
orb(rec(A,cons(B,nil)),rec(C,nil)) = rec(x(step(A,B),C),nil),
inference(paramod,[status(thm)],[c_85,c_104]) ).
cnf(c_3000,plain,
orb(bfalse,rec(A,nil)) = rec(x(nil2,A),nil),
inference(paramod,[status(thm)],[c_101,c_104]) ).
cnf(c_3001,plain,
rec(A,nil) = rec(x(nil2,A),nil),
inference(paramod,[status(thm)],[c_63,c_3000]) ).
cnf(c_135,plain,
rec(x(nil2,A),nil) = rec(A,nil),
inference(copy,[status(thm)],[c_3001]) ).
cnf(c_3002,plain,
andb(btrue,rec(A,nil)) = rec(y(eps,A),nil),
inference(paramod,[status(thm)],[c_105,c_103]) ).
cnf(c_3003,plain,
rec(A,nil) = rec(y(eps,A),nil),
inference(paramod,[status(thm)],[c_66,c_3002]) ).
cnf(c_141,plain,
rec(y(eps,A),nil) = rec(A,nil),
inference(copy,[status(thm)],[c_3003]) ).
cnf(c_142,plain,
andb(rec(A,nil),btrue) = rec(y(A,eps),nil),
inference(paramod,[status(thm)],[c_105,c_103]) ).
cnf(c_3004,plain,
orb(btrue,rec(A,nil)) = rec(x(eps,A),nil),
inference(paramod,[status(thm)],[c_105,c_104]) ).
cnf(c_3005,plain,
btrue = rec(x(eps,A),nil),
inference(paramod,[status(thm)],[c_62,c_3004]) ).
cnf(c_143,plain,
rec(x(eps,A),nil) = btrue,
inference(copy,[status(thm)],[c_3005]) ).
cnf(c_145,plain,
rec(y(A,star(B)),nil) = rec(y(A,eps),nil),
inference(paramod,[status(thm)],[c_142,c_129]) ).
cnf(c_153,plain,
rec(x(nil2,step(A,B)),C) = rec(x(eps,A),cons(B,C)),
inference(paramod,[status(thm)],[c_81,c_106]) ).
cnf(c_154,plain,
rec(x(step(A,B),nil2),C) = rec(x(A,eps),cons(B,C)),
inference(paramod,[status(thm)],[c_81,c_106]) ).
cnf(c_164,plain,
eq2(notb(rec(y(step(A,a),star(A)),cons(b,cons(b,cons(a,nil))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_107,c_98]) ).
cnf(c_166,plain,
rec(step(step(step(A,B),C),D),E) = rec(A,cons(B,cons(C,cons(D,E)))),
inference(paramod,[status(thm)],[c_108,c_85]) ).
cnf(c_207,plain,
eq2(notb(rec(y(x(step(A,a),step(B,a)),star(x(A,B))),cons(b,cons(b,cons(a,nil))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_164]) ).
cnf(c_3006,plain,
orb(bfalse,rec(A,nil)) = rec(x(y(nil2,B),A),nil),
inference(paramod,[status(thm)],[c_126,c_104]) ).
cnf(c_3007,plain,
rec(A,nil) = rec(x(y(nil2,B),A),nil),
inference(paramod,[status(thm)],[c_63,c_3006]) ).
cnf(c_219,plain,
rec(x(y(nil2,A),B),nil) = rec(B,nil),
inference(copy,[status(thm)],[c_3007]) ).
cnf(c_3008,plain,
aux2(A,x(eps,B),C,btrue) = step(y(x(eps,B),C),A),
inference(paramod,[status(thm)],[c_143,c_99]) ).
cnf(c_3009,plain,
x(y(step(x(eps,B),A),C),step(C,A)) = step(y(x(eps,B),C),A),
inference(paramod,[status(thm)],[c_3,c_3008]) ).
cnf(c_3010,plain,
x(y(x(step(eps,A),step(B,A)),C),step(C,A)) = step(y(x(eps,B),C),A),
inference(paramod,[status(thm)],[c_76,c_3009]) ).
cnf(c_3011,plain,
x(y(x(nil2,step(B,A)),C),step(C,A)) = step(y(x(eps,B),C),A),
inference(paramod,[status(thm)],[c_81,c_3010]) ).
cnf(c_221,plain,
step(y(x(eps,A),B),C) = x(y(x(nil2,step(A,C)),B),step(B,C)),
inference(copy,[status(thm)],[c_3011]) ).
cnf(c_3012,plain,
andb(rec(A,nil),rec(B,nil)) = rec(y(x(nil2,A),B),nil),
inference(paramod,[status(thm)],[c_135,c_103]) ).
cnf(c_3013,plain,
rec(y(A,B),nil) = rec(y(x(nil2,A),B),nil),
inference(paramod,[status(thm)],[c_103,c_3012]) ).
cnf(c_237,plain,
rec(y(x(nil2,A),B),nil) = rec(y(A,B),nil),
inference(copy,[status(thm)],[c_3013]) ).
cnf(c_253,plain,
rec(x(step(A,B),x(y(nil2,C),nil2)),D) = rec(x(A,y(nil2,C)),cons(B,D)),
inference(paramod,[status(thm)],[c_120,c_106]) ).
cnf(c_3014,plain,
orb(rec(A,nil),rec(B,nil)) = rec(x(A,y(eps,B)),nil),
inference(paramod,[status(thm)],[c_141,c_104]) ).
cnf(c_3015,plain,
rec(x(A,B),nil) = rec(x(A,y(eps,B)),nil),
inference(paramod,[status(thm)],[c_104,c_3014]) ).
cnf(c_269,plain,
rec(x(A,y(eps,B)),nil) = rec(x(A,B),nil),
inference(copy,[status(thm)],[c_3015]) ).
cnf(c_3016,plain,
orb(rec(A,nil),rec(B,nil)) = rec(x(x(y(nil2,C),A),B),nil),
inference(paramod,[status(thm)],[c_219,c_104]) ).
cnf(c_3017,plain,
rec(x(A,B),nil) = rec(x(x(y(nil2,C),A),B),nil),
inference(paramod,[status(thm)],[c_104,c_3016]) ).
cnf(c_316,plain,
rec(x(x(y(nil2,A),B),C),nil) = rec(x(B,C),nil),
inference(copy,[status(thm)],[c_3017]) ).
cnf(c_3018,plain,
orb(rec(A,nil),rec(B,nil)) = rec(x(A,x(y(nil2,C),B)),nil),
inference(paramod,[status(thm)],[c_219,c_104]) ).
cnf(c_3019,plain,
rec(x(A,B),nil) = rec(x(A,x(y(nil2,C),B)),nil),
inference(paramod,[status(thm)],[c_104,c_3018]) ).
cnf(c_317,plain,
rec(x(A,x(y(nil2,B),C)),nil) = rec(x(A,C),nil),
inference(copy,[status(thm)],[c_3019]) ).
cnf(c_3020,plain,
orb(rec(y(A,eps),nil),rec(B,nil)) = rec(x(y(A,star(C)),B),nil),
inference(paramod,[status(thm)],[c_145,c_104]) ).
cnf(c_3021,plain,
rec(x(y(A,eps),B),nil) = rec(x(y(A,star(C)),B),nil),
inference(paramod,[status(thm)],[c_104,c_3020]) ).
cnf(c_349,plain,
rec(x(y(A,star(B)),C),nil) = rec(x(y(A,eps),C),nil),
inference(copy,[status(thm)],[c_3021]) ).
cnf(c_3022,plain,
orb(rec(A,nil),rec(y(B,eps),nil)) = rec(x(A,y(B,star(C))),nil),
inference(paramod,[status(thm)],[c_145,c_104]) ).
cnf(c_3023,plain,
rec(x(A,y(B,eps)),nil) = rec(x(A,y(B,star(C))),nil),
inference(paramod,[status(thm)],[c_104,c_3022]) ).
cnf(c_350,plain,
rec(x(A,y(B,star(C))),nil) = rec(x(A,y(B,eps)),nil),
inference(copy,[status(thm)],[c_3023]) ).
cnf(c_3024,plain,
orb(rec(y(A,B),nil),rec(C,nil)) = rec(x(y(x(nil2,A),B),C),nil),
inference(paramod,[status(thm)],[c_237,c_104]) ).
cnf(c_3025,plain,
rec(x(y(A,B),C),nil) = rec(x(y(x(nil2,A),B),C),nil),
inference(paramod,[status(thm)],[c_104,c_3024]) ).
cnf(c_561,plain,
rec(x(y(x(nil2,A),B),C),nil) = rec(x(y(A,B),C),nil),
inference(copy,[status(thm)],[c_3025]) ).
cnf(c_3026,plain,
orb(rec(A,nil),rec(y(B,C),nil)) = rec(x(A,y(x(nil2,B),C)),nil),
inference(paramod,[status(thm)],[c_237,c_104]) ).
cnf(c_3027,plain,
rec(x(A,y(B,C)),nil) = rec(x(A,y(x(nil2,B),C)),nil),
inference(paramod,[status(thm)],[c_104,c_3026]) ).
cnf(c_562,plain,
rec(x(A,y(x(nil2,B),C)),nil) = rec(x(A,y(B,C)),nil),
inference(copy,[status(thm)],[c_3027]) ).
cnf(c_3028,plain,
rec(x(nil2,nil2),A) = rec(x(eps,atom(a)),cons(b,A)),
inference(paramod,[status(thm)],[c_109,c_153]) ).
cnf(c_566,plain,
rec(x(eps,atom(a)),cons(b,A)) = rec(x(nil2,nil2),A),
inference(copy,[status(thm)],[c_3028]) ).
cnf(c_3029,plain,
rec(x(nil2,eps),A) = rec(x(eps,atom(B)),cons(B,A)),
inference(paramod,[status(thm)],[c_115,c_153]) ).
cnf(c_572,plain,
rec(x(eps,atom(A)),cons(A,B)) = rec(x(nil2,eps),B),
inference(copy,[status(thm)],[c_3029]) ).
cnf(c_3030,plain,
orb(rec(A,nil),rec(x(B,C),nil)) = rec(x(A,x(B,y(eps,C))),nil),
inference(paramod,[status(thm)],[c_269,c_104]) ).
cnf(c_3031,plain,
rec(x(A,x(B,C)),nil) = rec(x(A,x(B,y(eps,C))),nil),
inference(paramod,[status(thm)],[c_104,c_3030]) ).
cnf(c_656,plain,
rec(x(A,x(B,y(eps,C))),nil) = rec(x(A,x(B,C)),nil),
inference(copy,[status(thm)],[c_3031]) ).
cnf(c_3032,plain,
aux2(A,step(x(eps,atom(a)),b),B,rec(x(nil2,nil2),nil)) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_566,c_118]) ).
cnf(c_3033,plain,
aux2(A,x(step(eps,b),step(atom(a),b)),B,rec(x(nil2,nil2),nil)) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_76,c_3032]) ).
cnf(c_3034,plain,
aux2(A,x(nil2,step(atom(a),b)),B,rec(x(nil2,nil2),nil)) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_81,c_3033]) ).
cnf(c_3035,plain,
aux2(A,x(nil2,nil2),B,rec(x(nil2,nil2),nil)) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_109,c_3034]) ).
cnf(c_3036,plain,
aux2(A,x(nil2,nil2),B,rec(nil2,nil)) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_135,c_3035]) ).
cnf(c_3037,plain,
aux2(A,x(nil2,nil2),B,bfalse) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_101,c_3036]) ).
cnf(c_3038,plain,
x(y(step(x(nil2,nil2),A),B),nil2) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_4,c_3037]) ).
cnf(c_3039,plain,
x(y(x(step(nil2,A),step(nil2,A)),B),nil2) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_76,c_3038]) ).
cnf(c_3040,plain,
x(y(x(nil2,step(nil2,A)),B),nil2) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_80,c_3039]) ).
cnf(c_3041,plain,
x(y(x(nil2,nil2),B),nil2) = step(y(step(x(eps,atom(a)),b),B),A),
inference(paramod,[status(thm)],[c_80,c_3040]) ).
cnf(c_3042,plain,
x(y(x(nil2,nil2),B),nil2) = step(y(x(step(eps,b),step(atom(a),b)),B),A),
inference(paramod,[status(thm)],[c_76,c_3041]) ).
cnf(c_3043,plain,
x(y(x(nil2,nil2),B),nil2) = step(y(x(nil2,step(atom(a),b)),B),A),
inference(paramod,[status(thm)],[c_81,c_3042]) ).
cnf(c_3044,plain,
x(y(x(nil2,nil2),B),nil2) = step(y(x(nil2,nil2),B),A),
inference(paramod,[status(thm)],[c_109,c_3043]) ).
cnf(c_778,plain,
step(y(x(nil2,nil2),A),B) = x(y(x(nil2,nil2),A),nil2),
inference(copy,[status(thm)],[c_3044]) ).
cnf(c_3045,plain,
aux2(A,step(x(eps,atom(B)),B),C,rec(x(nil2,eps),nil)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_572,c_118]) ).
cnf(c_3046,plain,
aux2(A,x(step(eps,B),step(atom(B),B)),C,rec(x(nil2,eps),nil)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_76,c_3045]) ).
cnf(c_3047,plain,
aux2(A,x(nil2,step(atom(B),B)),C,rec(x(nil2,eps),nil)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_81,c_3046]) ).
cnf(c_3048,plain,
aux2(A,x(nil2,eps),C,rec(x(nil2,eps),nil)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_115,c_3047]) ).
cnf(c_3049,plain,
aux2(A,x(nil2,eps),C,rec(eps,nil)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_135,c_3048]) ).
cnf(c_3050,plain,
aux2(A,x(nil2,eps),C,btrue) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_105,c_3049]) ).
cnf(c_3051,plain,
x(y(step(x(nil2,eps),A),C),step(C,A)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_3,c_3050]) ).
cnf(c_3052,plain,
x(y(x(step(nil2,A),step(eps,A)),C),step(C,A)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_76,c_3051]) ).
cnf(c_3053,plain,
x(y(x(nil2,step(eps,A)),C),step(C,A)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_80,c_3052]) ).
cnf(c_3054,plain,
x(y(x(nil2,nil2),C),step(C,A)) = step(y(step(x(eps,atom(B)),B),C),A),
inference(paramod,[status(thm)],[c_81,c_3053]) ).
cnf(c_3055,plain,
x(y(x(nil2,nil2),C),step(C,A)) = step(y(x(step(eps,B),step(atom(B),B)),C),A),
inference(paramod,[status(thm)],[c_76,c_3054]) ).
cnf(c_3056,plain,
x(y(x(nil2,nil2),C),step(C,A)) = step(y(x(nil2,step(atom(B),B)),C),A),
inference(paramod,[status(thm)],[c_81,c_3055]) ).
cnf(c_3057,plain,
x(y(x(nil2,nil2),C),step(C,A)) = step(y(x(nil2,eps),C),A),
inference(paramod,[status(thm)],[c_115,c_3056]) ).
cnf(c_797,plain,
step(y(x(nil2,eps),A),B) = x(y(x(nil2,nil2),A),step(A,B)),
inference(copy,[status(thm)],[c_3057]) ).
cnf(c_965,plain,
eq2(notb(rec(y(x(nil2,step(A,a)),star(x(atom(b),A))),cons(b,cons(b,cons(a,nil))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_111,c_207]) ).
cnf(c_3058,plain,
eps2(x(step(A,B),x(y(nil2,C),nil2))) = rec(x(A,y(nil2,C)),cons(B,nil)),
inference(paramod,[status(thm)],[c_253,c_83]) ).
cnf(c_3059,plain,
rec(x(step(A,B),x(y(nil2,C),nil2)),nil) = rec(x(A,y(nil2,C)),cons(B,nil)),
inference(paramod,[status(thm)],[c_83,c_3058]) ).
cnf(c_1188,plain,
rec(x(step(A,B),nil2),nil) = rec(x(A,y(nil2,C)),cons(B,nil)),
inference(paramod,[status(thm)],[c_317,c_3059]) ).
cnf(c_3060,plain,
orb(rec(x(y(A,eps),B),nil),rec(C,nil)) = rec(x(x(y(A,star(D)),B),C),nil),
inference(paramod,[status(thm)],[c_349,c_104]) ).
cnf(c_3061,plain,
rec(x(x(y(A,eps),B),C),nil) = rec(x(x(y(A,star(D)),B),C),nil),
inference(paramod,[status(thm)],[c_104,c_3060]) ).
cnf(c_1268,plain,
rec(x(x(y(A,star(B)),C),D),nil) = rec(x(x(y(A,eps),C),D),nil),
inference(copy,[status(thm)],[c_3061]) ).
cnf(c_3062,plain,
orb(rec(A,nil),rec(x(y(B,eps),C),nil)) = rec(x(A,x(y(B,star(D)),C)),nil),
inference(paramod,[status(thm)],[c_349,c_104]) ).
cnf(c_3063,plain,
rec(x(A,x(y(B,eps),C)),nil) = rec(x(A,x(y(B,star(D)),C)),nil),
inference(paramod,[status(thm)],[c_104,c_3062]) ).
cnf(c_1269,plain,
rec(x(A,x(y(B,star(C)),D)),nil) = rec(x(A,x(y(B,eps),D)),nil),
inference(copy,[status(thm)],[c_3063]) ).
cnf(c_3064,plain,
orb(rec(A,nil),rec(x(B,y(C,eps)),nil)) = rec(x(A,x(B,y(C,star(D)))),nil),
inference(paramod,[status(thm)],[c_350,c_104]) ).
cnf(c_3065,plain,
rec(x(A,x(B,y(C,eps))),nil) = rec(x(A,x(B,y(C,star(D)))),nil),
inference(paramod,[status(thm)],[c_104,c_3064]) ).
cnf(c_1275,plain,
rec(x(A,x(B,y(C,star(D)))),nil) = rec(x(A,x(B,y(C,eps))),nil),
inference(copy,[status(thm)],[c_3065]) ).
cnf(c_3066,plain,
orb(rec(x(y(A,B),C),nil),rec(D,nil)) = rec(x(x(y(x(nil2,A),B),C),D),nil),
inference(paramod,[status(thm)],[c_561,c_104]) ).
cnf(c_3067,plain,
rec(x(x(y(A,B),C),D),nil) = rec(x(x(y(x(nil2,A),B),C),D),nil),
inference(paramod,[status(thm)],[c_104,c_3066]) ).
cnf(c_1572,plain,
rec(x(x(y(x(nil2,A),B),C),D),nil) = rec(x(x(y(A,B),C),D),nil),
inference(copy,[status(thm)],[c_3067]) ).
cnf(c_3068,plain,
orb(rec(A,nil),rec(x(y(B,C),D),nil)) = rec(x(A,x(y(x(nil2,B),C),D)),nil),
inference(paramod,[status(thm)],[c_561,c_104]) ).
cnf(c_3069,plain,
rec(x(A,x(y(B,C),D)),nil) = rec(x(A,x(y(x(nil2,B),C),D)),nil),
inference(paramod,[status(thm)],[c_104,c_3068]) ).
cnf(c_1573,plain,
rec(x(A,x(y(x(nil2,B),C),D)),nil) = rec(x(A,x(y(B,C),D)),nil),
inference(copy,[status(thm)],[c_3069]) ).
cnf(c_3070,plain,
orb(rec(A,nil),rec(x(B,y(C,D)),nil)) = rec(x(A,x(B,y(x(nil2,C),D))),nil),
inference(paramod,[status(thm)],[c_562,c_104]) ).
cnf(c_3071,plain,
rec(x(A,x(B,y(C,D))),nil) = rec(x(A,x(B,y(x(nil2,C),D))),nil),
inference(paramod,[status(thm)],[c_104,c_3070]) ).
cnf(c_1584,plain,
rec(x(A,x(B,y(x(nil2,C),D))),nil) = rec(x(A,x(B,y(C,D))),nil),
inference(copy,[status(thm)],[c_3071]) ).
cnf(c_1654,plain,
rec(x(A,y(nil2,B)),cons(C,nil)) = rec(x(A,eps),cons(C,nil)),
inference(paramod,[status(thm)],[c_1188,c_154]) ).
cnf(c_3072,plain,
rec(x(x(y(x(nil2,nil2),A),nil2),nil2),nil) = rec(x(y(x(nil2,nil2),A),y(nil2,B)),cons(C,nil)),
inference(paramod,[status(thm)],[c_778,c_1188]) ).
cnf(c_3073,plain,
rec(x(x(y(nil2,A),nil2),nil2),nil) = rec(x(y(x(nil2,nil2),A),y(nil2,B)),cons(C,nil)),
inference(paramod,[status(thm)],[c_1572,c_3072]) ).
cnf(c_3074,plain,
rec(x(nil2,nil2),nil) = rec(x(y(x(nil2,nil2),A),y(nil2,B)),cons(C,nil)),
inference(paramod,[status(thm)],[c_316,c_3073]) ).
cnf(c_3075,plain,
rec(nil2,nil) = rec(x(y(x(nil2,nil2),A),y(nil2,B)),cons(C,nil)),
inference(paramod,[status(thm)],[c_135,c_3074]) ).
cnf(c_3076,plain,
bfalse = rec(x(y(x(nil2,nil2),A),y(nil2,B)),cons(C,nil)),
inference(paramod,[status(thm)],[c_101,c_3075]) ).
cnf(c_3077,plain,
bfalse = rec(x(y(x(nil2,nil2),A),eps),cons(C,nil)),
inference(paramod,[status(thm)],[c_1654,c_3076]) ).
cnf(c_1656,plain,
rec(x(y(x(nil2,nil2),A),eps),cons(B,nil)) = bfalse,
inference(copy,[status(thm)],[c_3077]) ).
cnf(c_3078,plain,
orb(bfalse,rec(A,nil)) = rec(x(step(x(y(x(nil2,nil2),B),eps),C),A),nil),
inference(paramod,[status(thm)],[c_1656,c_131]) ).
cnf(c_3079,plain,
rec(A,nil) = rec(x(step(x(y(x(nil2,nil2),B),eps),C),A),nil),
inference(paramod,[status(thm)],[c_63,c_3078]) ).
cnf(c_3080,plain,
rec(A,nil) = rec(x(x(step(y(x(nil2,nil2),B),C),step(eps,C)),A),nil),
inference(paramod,[status(thm)],[c_76,c_3079]) ).
cnf(c_3081,plain,
rec(A,nil) = rec(x(x(x(y(x(nil2,nil2),B),nil2),step(eps,C)),A),nil),
inference(paramod,[status(thm)],[c_778,c_3080]) ).
cnf(c_3082,plain,
rec(A,nil) = rec(x(x(x(y(x(nil2,nil2),B),nil2),nil2),A),nil),
inference(paramod,[status(thm)],[c_81,c_3081]) ).
cnf(c_1662,plain,
rec(x(x(x(y(x(nil2,nil2),A),nil2),nil2),B),nil) = rec(B,nil),
inference(copy,[status(thm)],[c_3082]) ).
cnf(c_2903,plain,
eq2(notb(rec(y(x(nil2,eps),star(x(atom(b),atom(a)))),cons(b,cons(b,cons(a,nil))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_115,c_965]) ).
cnf(c_3083,plain,
eq2(notb(rec(step(step(step(y(x(nil2,eps),star(x(atom(b),atom(a)))),b),b),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_166,c_2903]) ).
cnf(c_3084,plain,
eq2(notb(rec(step(step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),step(star(x(atom(b),atom(a))),b)),b),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_797,c_3083]) ).
cnf(c_3085,plain,
eq2(notb(rec(step(step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(step(x(atom(b),atom(a)),b),star(x(atom(b),atom(a))))),b),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_79,c_3084]) ).
cnf(c_3086,plain,
eq2(notb(rec(step(step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(step(atom(b),b),step(atom(a),b)),star(x(atom(b),atom(a))))),b),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3085]) ).
cnf(c_3087,plain,
eq2(notb(rec(step(step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,step(atom(a),b)),star(x(atom(b),atom(a))))),b),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_115,c_3086]) ).
cnf(c_3088,plain,
eq2(notb(rec(step(step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,nil2),star(x(atom(b),atom(a))))),b),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_109,c_3087]) ).
cnf(c_3089,plain,
eq2(notb(rec(step(x(step(y(x(nil2,nil2),star(x(atom(b),atom(a)))),b),step(y(x(eps,nil2),star(x(atom(b),atom(a)))),b)),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3088]) ).
cnf(c_3090,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),step(y(x(eps,nil2),star(x(atom(b),atom(a)))),b)),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_778,c_3089]) ).
cnf(c_3091,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,step(nil2,b)),star(x(atom(b),atom(a)))),step(star(x(atom(b),atom(a))),b))),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_221,c_3090]) ).
cnf(c_3092,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),step(star(x(atom(b),atom(a))),b))),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_80,c_3091]) ).
cnf(c_3093,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(step(x(atom(b),atom(a)),b),star(x(atom(b),atom(a)))))),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_79,c_3092]) ).
cnf(c_3094,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(step(atom(b),b),step(atom(a),b)),star(x(atom(b),atom(a)))))),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3093]) ).
cnf(c_3095,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,step(atom(a),b)),star(x(atom(b),atom(a)))))),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_115,c_3094]) ).
cnf(c_3096,plain,
eq2(notb(rec(step(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,nil2),star(x(atom(b),atom(a)))))),a),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_109,c_3095]) ).
cnf(c_3097,plain,
eq2(notb(rec(x(step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),a),step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,nil2),star(x(atom(b),atom(a))))),a)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3096]) ).
cnf(c_3098,plain,
eq2(notb(rec(x(x(step(y(x(nil2,nil2),star(x(atom(b),atom(a)))),a),step(nil2,a)),step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,nil2),star(x(atom(b),atom(a))))),a)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3097]) ).
cnf(c_3099,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),step(nil2,a)),step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,nil2),star(x(atom(b),atom(a))))),a)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_778,c_3098]) ).
cnf(c_3100,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),step(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(eps,nil2),star(x(atom(b),atom(a))))),a)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_80,c_3099]) ).
cnf(c_3101,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(step(y(x(nil2,nil2),star(x(atom(b),atom(a)))),a),step(y(x(eps,nil2),star(x(atom(b),atom(a)))),a))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3100]) ).
cnf(c_3102,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),step(y(x(eps,nil2),star(x(atom(b),atom(a)))),a))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_778,c_3101]) ).
cnf(c_3103,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,step(nil2,a)),star(x(atom(b),atom(a)))),step(star(x(atom(b),atom(a))),a)))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_221,c_3102]) ).
cnf(c_3104,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),step(star(x(atom(b),atom(a))),a)))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_80,c_3103]) ).
cnf(c_3105,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(step(x(atom(b),atom(a)),a),star(x(atom(b),atom(a))))))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_79,c_3104]) ).
cnf(c_3106,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(step(atom(b),a),step(atom(a),a)),star(x(atom(b),atom(a))))))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_76,c_3105]) ).
cnf(c_3107,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(nil2,step(atom(a),a)),star(x(atom(b),atom(a))))))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_111,c_3106]) ).
cnf(c_3108,plain,
eq2(notb(rec(x(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),nil2),x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(nil2,eps),star(x(atom(b),atom(a))))))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_115,c_3107]) ).
cnf(c_3109,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(nil2,eps),star(x(atom(b),atom(a)))))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1662,c_3108]) ).
cnf(c_3110,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(x(nil2,eps),eps))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1275,c_3109]) ).
cnf(c_3111,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),y(eps,eps))),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1584,c_3110]) ).
cnf(c_3112,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),eps)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_656,c_3111]) ).
cnf(c_3113,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(x(nil2,nil2),eps),eps)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1269,c_3112]) ).
cnf(c_3114,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),x(y(nil2,eps),eps)),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1573,c_3113]) ).
cnf(c_3115,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),star(x(atom(b),atom(a)))),nil2),eps),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_317,c_3114]) ).
cnf(c_3116,plain,
eq2(notb(rec(x(x(y(x(nil2,nil2),eps),nil2),eps),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1268,c_3115]) ).
cnf(c_3117,plain,
eq2(notb(rec(x(x(y(nil2,eps),nil2),eps),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1572,c_3116]) ).
cnf(c_3118,plain,
eq2(notb(rec(x(nil2,eps),nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_316,c_3117]) ).
cnf(c_3119,plain,
eq2(notb(rec(eps,nil)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_135,c_3118]) ).
cnf(c_3120,plain,
eq2(notb(btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_105,c_3119]) ).
cnf(c_3121,plain,
eq2(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_64,c_3120]) ).
cnf(c_3122,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_96,c_3121]) ).
cnf(c_2980,plain,
$false,
inference(copy,[status(thm)],[c_3122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX210-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n013.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 16:55:21 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 3201253 was started by sandbox2 on n013,
% 0.18/0.45 % Sat Sep 26 16:55:21 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.46
% 0.18/0.46 % From the command line: assign(max_seconds, 300).
% 203.98/27.00
% 203.98/27.00 % given #500 (T,wt=17): 556 rec(x(y(A,x(eps,B)),C),nil) = rec(x(y(A,eps),C),nil). [para(223(a,1),104(a,1,1)),rewrite([104(7)]),flip(a)].
% 203.98/27.00
% 203.98/27.00 % SZS status Unsatisfiable for theBenchmark
% 203.98/27.00
% 203.98/27.00 % Proof 1 at 1.99 (+ 0.40) seconds.
% 203.98/27.00 % Length of proof is 89.
% 203.98/27.00 % Level of proof is 10.
% 203.98/27.00 % Maximum clause weight is 29.000.
% 203.98/27.00 % Given clauses 901.
% 203.98/27.00
% 203.98/27.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------