%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ039-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n017.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 : Fri Sep 25 02:32:49 PM UTC 2026
% Result : Unsatisfiable 11.61s 2.10s
% Output : CNFRefutation 11.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 34
% Syntax : Number of formulae : 160 ( 160 unt; 18 def)
% Number of atoms : 1102 ( 159 equ)
% Maximal formula atoms : 1 ( 6 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 8 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 19 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 2 con; 0-12 aty)
% Number of variables : 1140 ( 0 sgn1140 !; 0 ?; 801 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f10,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_right) ).
fof(f11,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true),
inference(reorient_equations,[],[f10]) ).
fof(f12,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_left) ).
fof(f13,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_down) ).
fof(f15,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11),true),
inference(reorient_equations,[],[f14]) ).
fof(f18,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_right) ).
fof(f19,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true),
inference(reorient_equations,[],[f18]) ).
fof(f20,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s3_left) ).
fof(f21,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true),
inference(reorient_equations,[],[f20]) ).
fof(f26,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s4_right) ).
fof(f27,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true),
inference(reorient_equations,[],[f26]) ).
fof(f28,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s4_left) ).
fof(f29,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true),
inference(reorient_equations,[],[f28]) ).
fof(f30,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s4_down) ).
fof(f31,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true),
inference(reorient_equations,[],[f30]) ).
fof(f32,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s4_up) ).
fof(f33,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true),
inference(reorient_equations,[],[f32]) ).
fof(f54,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11),true,state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v3_down) ).
fof(f55,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11),true,state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11),true),
inference(reorient_equations,[],[f54]) ).
fof(f60,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5)),true,state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v4_left) ).
fof(f61,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5)),true,state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))),true),
inference(reorient_equations,[],[f60]) ).
fof(f68,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : ifeq(state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11),true,state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_left) ).
fof(f69,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] : true = ifeq(state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11),true,state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11),true),
inference(reorient_equations,[],[f68]) ).
fof(f82,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13)),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swap_blanks) ).
fof(f83,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] : true = ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13)),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)),true),
inference(reorient_equations,[],[f82]) ).
fof(f84,axiom,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initial_state) ).
fof(f85,plain,
true = state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : state(X0,X1,X2,X3,v4(s(s(o)),s(s(o))),X4,X5,X6,X7,X8,X9,X10) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_state) ).
fof(f87,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : true != state(X0,X1,X2,X3,v4(s(s(o)),s(s(o))),X4,X5,X6,X7,X8,X9,X10),
inference(reorient_equations,[],[f86]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(X0,X0,X1,X2) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true) = true,
inference(cnf_transformation,[],[f11]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true) = true,
inference(cnf_transformation,[],[f13]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11),true) = true,
inference(cnf_transformation,[],[f15]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true) = true,
inference(cnf_transformation,[],[f19]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true) = true,
inference(cnf_transformation,[],[f21]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true) = true,
inference(cnf_transformation,[],[f27]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true) = true,
inference(cnf_transformation,[],[f29]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true) = true,
inference(cnf_transformation,[],[f31]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true) = true,
inference(cnf_transformation,[],[f33]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11),true,state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11),true) = true,
inference(cnf_transformation,[],[f55]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5)),true,state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))),true) = true,
inference(cnf_transformation,[],[f61]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11),true,state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11),true) = true,
inference(cnf_transformation,[],[f69]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13)),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)),true) = true,
inference(cnf_transformation,[],[f83]) ).
tcf(c_135,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))) = true,
inference(cnf_transformation,[],[f85]) ).
tcf(c_136,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : state(X0,X1,X2,X3,v4(s(s(o)),s(s(o))),X4,X5,X6,X7,X8,X9,X10) != true,
inference(cnf_transformation,[],[f87]) ).
tcf(c_285,definition,
iPr_def_10 = s(o),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_286,definition,
iPr_def_11 = s(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_287,definition,
iPr_def_12 = v4(iPr_def_11,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_288,definition,
iPr_def_13 = bb(o,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_289,definition,
iPr_def_14 = v1(o,o),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_290,definition,
iPr_def_15 = s(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_291,definition,
iPr_def_16 = v2(o,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_292,definition,
iPr_def_17 = v3(iPr_def_11,o),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_293,definition,
iPr_def_18 = v4(iPr_def_11,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_294,definition,
iPr_def_19 = h(iPr_def_11,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_295,definition,
iPr_def_20 = s1(iPr_def_15,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_296,definition,
iPr_def_21 = s2(iPr_def_15,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_297,definition,
iPr_def_22 = s(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_298,definition,
iPr_def_23 = s3(iPr_def_22,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_299,definition,
iPr_def_24 = s4(iPr_def_22,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_300,definition,
iPr_def_25 = e1(iPr_def_22,o),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_301,definition,
iPr_def_26 = e2(iPr_def_22,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_302,definition,
iPr_def_27 = state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,iPr_def_21,iPr_def_23,iPr_def_24,iPr_def_25,iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_303,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : state(X0,X1,X2,X3,iPr_def_12,X4,X5,X6,X7,X8,X9,X10) != true,
inference(demodulation,[status(thm)],[c_136,c_285,c_286,c_287]) ).
tcf(c_304,plain,
iPr_def_27 = true,
inference(demodulation,[status(thm)],[c_135,c_301,c_300,c_299,c_297,c_298,c_296,c_295,c_294,c_293,c_292,c_290,c_291,c_289,c_288,c_302]) ).
tcf(c_305,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13)),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)),true) = true,
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_312,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11),true,state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11),true) = true,
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_316,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5)),true,state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))),true) = true,
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_319,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11),true,state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11),true) = true,
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true) = true,
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_331,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),true) = true,
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true) = true,
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_333,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),true) = true,
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_336,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true) = true,
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_337,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),true) = true,
inference(demodulation,[status(thm)],[c_102]) ).
tcf(c_339,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11),true) = true,
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true) = true,
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_341,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),true,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),true) = true,
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_346,plain,
! [X0: $i,X1: $i,X2: $i] : ifeq(X0,X0,X1,X2) = X1,
inference(demodulation,[status(thm)],[c_93]) ).
tcf(c_625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : state(X0,X1,X2,X3,iPr_def_12,X4,X5,X6,X7,X8,X9,X10) != iPr_def_27,
inference(light_normalisation,[status(thm)],[c_303,c_304]) ).
tcf(c_626,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13)),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_305,c_304]) ).
tcf(c_627,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,iPr_def_25,e2(X10,X11)),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_300,c_626]) ).
tcf(c_629,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(iPr_def_22,o)),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,iPr_def_25,e2(X10,X11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_300,c_626]) ).
tcf(c_630,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(iPr_def_22,iPr_def_15),e2(X10,X11)),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),iPr_def_26),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_301,c_626]) ).
tcf(c_673,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,iPr_def_25,iPr_def_26),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(iPr_def_22,iPr_def_15),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_301,c_627]) ).
tcf(c_677,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,iPr_def_21,iPr_def_23,iPr_def_24,e1(iPr_def_22,iPr_def_15),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_302,c_673]) ).
tcf(c_678,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,iPr_def_21,iPr_def_23,iPr_def_24,e1(iPr_def_22,iPr_def_15),e2(iPr_def_22,o)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_677,c_346]) ).
tcf(c_679,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_330,c_304]) ).
tcf(c_689,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_22,X9),e1(iPr_def_15,X9),X10),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_15,X9),e1(iPr_def_22,X9),X10),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_297,c_679]) ).
tcf(c_696,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_331,c_304]) ).
tcf(c_705,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_15,X9),e1(iPr_def_22,X9),X10),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_22,X9),e1(iPr_def_15,X9),X10),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_297,c_696]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_332,c_304]) ).
tcf(c_719,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_22,s(iPr_def_11)),e1(iPr_def_22,iPr_def_11),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,iPr_def_24,e1(iPr_def_22,s(iPr_def_11)),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_299,c_713]) ).
tcf(c_724,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_11),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,iPr_def_24,e1(iPr_def_22,iPr_def_15),X9),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_719,c_290]) ).
tcf(c_732,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_333,c_304]) ).
tcf(c_733,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,iPr_def_24,e1(iPr_def_22,s(iPr_def_11)),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_22,s(iPr_def_11)),e1(iPr_def_22,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_299,c_732]) ).
tcf(c_744,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,iPr_def_24,e1(iPr_def_22,iPr_def_15),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_733,c_290]) ).
tcf(c_942,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_336,c_304]) ).
tcf(c_947,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(iPr_def_22,s(o)),X8,iPr_def_25,X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(iPr_def_22,o),X8,e1(iPr_def_22,s(o)),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_300,c_942]) ).
tcf(c_954,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,iPr_def_23,X8,iPr_def_25,X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(iPr_def_22,o),X8,e1(iPr_def_22,iPr_def_10),X9),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_947,c_285,c_298]) ).
tcf(c_961,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_337,c_304]) ).
tcf(c_971,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(iPr_def_22,o),X8,e1(iPr_def_22,s(o)),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,s3(iPr_def_22,s(o)),X8,iPr_def_25,X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_300,c_961]) ).
tcf(c_972,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,s3(iPr_def_22,o),X8,e1(iPr_def_22,iPr_def_10),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,iPr_def_23,X8,iPr_def_25,X9),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_971,c_285,c_298]) ).
tcf(c_1015,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11),iPr_def_27,state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_312,c_304]) ).
tcf(c_1022,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,h(X5,iPr_def_10),X6,X7,X8,X9,e1(X5,o),X10),iPr_def_27,state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(X5,s(iPr_def_10)),X10),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_285,c_1015]) ).
tcf(c_1028,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,h(X5,iPr_def_10),X6,X7,X8,X9,e1(X5,o),X10),iPr_def_27,state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(X5,iPr_def_11),X10),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_1022,c_286]) ).
tcf(c_1140,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_339,c_304]) ).
tcf(c_1141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,iPr_def_21,X7,X8,e1(s(iPr_def_15),iPr_def_11),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(s(iPr_def_15),iPr_def_11),X7,X8,e1(iPr_def_15,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_296,c_1140]) ).
tcf(c_1151,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,iPr_def_21,X7,X8,e1(iPr_def_22,iPr_def_11),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(iPr_def_22,iPr_def_11),X7,X8,e1(iPr_def_15,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_1141,c_297]) ).
tcf(c_1158,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_340,c_304]) ).
tcf(c_1166,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,iPr_def_11),X8,X9,e1(X7,iPr_def_10),X10),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,iPr_def_10),X8,X9,e1(X7,iPr_def_11),X10),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_286,c_1158]) ).
tcf(c_1177,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_341,c_304]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,iPr_def_10),X8,X9,e1(X7,iPr_def_11),X10),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,iPr_def_11),X8,X9,e1(X7,iPr_def_10),X10),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_286,c_1177]) ).
tcf(c_1185,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,s2(X7,iPr_def_11),X8,X9,e1(X7,iPr_def_15),X10),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,s2(X7,iPr_def_15),X8,X9,e1(X7,iPr_def_11),X10),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_290,c_1177]) ).
tcf(c_1222,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : ifeq(state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5)),iPr_def_27,state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_316,c_304]) ).
tcf(c_1232,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : ifeq(state(X0,X1,X2,X3,v4(iPr_def_11,s(iPr_def_11)),X4,X5,X6,X7,X8,e1(iPr_def_11,iPr_def_11),e2(s(iPr_def_11),iPr_def_11)),iPr_def_27,state(X0,X1,X2,X3,iPr_def_12,X4,X5,X6,X7,X8,e1(iPr_def_11,s(iPr_def_11)),e2(s(iPr_def_11),s(iPr_def_11))),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_287,c_1222]) ).
tcf(c_1247,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : ifeq(state(X0,X1,X2,X3,iPr_def_18,X4,X5,X6,X7,X8,e1(iPr_def_11,iPr_def_11),e2(iPr_def_15,iPr_def_11)),iPr_def_27,state(X0,X1,X2,X3,iPr_def_12,X4,X5,X6,X7,X8,e1(iPr_def_11,iPr_def_15),e2(iPr_def_15,iPr_def_15)),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_1232,c_290,c_293]) ).
tcf(c_1436,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : ifeq(state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11),iPr_def_27,state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11),iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_319,c_304]) ).
tcf(c_1437,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,iPr_def_17,X3,X4,X5,X6,X7,X8,e1(s(s(iPr_def_11)),o),X9),iPr_def_27,state(X0,X1,X2,v3(s(iPr_def_11),o),X3,X4,X5,X6,X7,X8,e1(iPr_def_11,o),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_292,c_1436]) ).
tcf(c_1450,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,iPr_def_17,X3,X4,X5,X6,X7,X8,iPr_def_25,X9),iPr_def_27,state(X0,X1,X2,v3(iPr_def_15,o),X3,X4,X5,X6,X7,X8,e1(iPr_def_11,o),X9),iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_1437,c_290,c_297,c_300]) ).
tcf(c_1874,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,iPr_def_21,iPr_def_23,s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_11),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_678,c_744]) ).
tcf(c_1877,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,iPr_def_21,iPr_def_23,s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_11),e2(iPr_def_22,o)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_1874,c_346]) ).
tcf(c_2078,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_22,iPr_def_15),e1(iPr_def_15,iPr_def_11),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_1877,c_1151]) ).
tcf(c_2081,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_22,iPr_def_15),e1(iPr_def_15,iPr_def_11),e2(iPr_def_22,o)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_2078,c_346]) ).
tcf(c_2084,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,iPr_def_24,e1(iPr_def_15,iPr_def_11),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_299,c_689]) ).
tcf(c_2090,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_22,iPr_def_15),iPr_def_25,e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_2081,c_629]) ).
tcf(c_2094,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_22,iPr_def_15),iPr_def_25,e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_2090,c_346]) ).
tcf(c_2100,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),s3(iPr_def_22,o),s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_10),e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_2094,c_954]) ).
tcf(c_2104,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),s3(iPr_def_22,o),s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_10),e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_2100,c_346]) ).
tcf(c_2170,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_11),X9),iPr_def_27,state(X0,X1,X2,X3,X4,X5,X6,X7,X8,iPr_def_24,e1(iPr_def_15,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_299,c_705]) ).
tcf(c_2864,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : ifeq(state(X0,X1,X2,X3,X4,iPr_def_19,X5,X6,X7,X8,e1(iPr_def_11,o),X9),iPr_def_27,state(X0,X1,X2,X3,X4,h(iPr_def_11,o),X5,X6,X7,X8,e1(iPr_def_11,iPr_def_11),X9),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_294,c_1028]) ).
tcf(c_3309,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_11),e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_2104,c_1166]) ).
tcf(c_3311,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),s4(iPr_def_22,iPr_def_15),e1(iPr_def_22,iPr_def_11),e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_3309,c_346]) ).
tcf(c_4158,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),iPr_def_24,e1(iPr_def_22,iPr_def_15),e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_3311,c_724]) ).
tcf(c_4161,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),iPr_def_24,e1(iPr_def_22,iPr_def_15),e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4158,c_346]) ).
tcf(c_4168,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),iPr_def_24,e1(iPr_def_15,iPr_def_11),iPr_def_26),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4161,c_630]) ).
tcf(c_4174,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),iPr_def_24,e1(iPr_def_15,iPr_def_11),iPr_def_26) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4168,c_346]) ).
tcf(c_4257,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_11),iPr_def_26),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4174,c_2084]) ).
tcf(c_4258,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_10),s3(iPr_def_22,o),s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_11),iPr_def_26) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4257,c_346]) ).
tcf(c_4265,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),s3(iPr_def_22,o),s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_10),iPr_def_26),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4258,c_1184]) ).
tcf(c_4269,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),s3(iPr_def_22,o),s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_10),iPr_def_26) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4265,c_346]) ).
tcf(c_4310,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_15,iPr_def_11),iPr_def_25,iPr_def_26),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4269,c_972]) ).
tcf(c_4316,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_15,iPr_def_11),iPr_def_25,iPr_def_26) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4310,c_346]) ).
tcf(c_4336,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_15),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4316,c_673]) ).
tcf(c_4342,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_11),iPr_def_23,s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_15),e2(iPr_def_22,o)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4336,c_346]) ).
tcf(c_4522,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_11),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4342,c_1185]) ).
tcf(c_4524,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,s4(iPr_def_15,iPr_def_11),e1(iPr_def_22,iPr_def_11),e2(iPr_def_22,o)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4522,c_346]) ).
tcf(c_4585,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_15,iPr_def_11),e2(iPr_def_22,o)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4524,c_2170]) ).
tcf(c_4587,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_15,iPr_def_11),e2(iPr_def_22,o)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4585,c_346]) ).
tcf(c_4596,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,iPr_def_25,e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4587,c_629]) ).
tcf(c_4602,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,iPr_def_17,iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,iPr_def_25,e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4596,c_346]) ).
tcf(c_4704,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,v3(iPr_def_15,o),iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_11,o),e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4602,c_1450]) ).
tcf(c_4706,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,v3(iPr_def_15,o),iPr_def_18,iPr_def_19,iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_11,o),e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4704,c_346]) ).
tcf(c_4787,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,v3(iPr_def_15,o),iPr_def_18,h(iPr_def_11,o),iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_11,iPr_def_11),e2(iPr_def_15,iPr_def_11)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4706,c_2864]) ).
tcf(c_4789,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,v3(iPr_def_15,o),iPr_def_18,h(iPr_def_11,o),iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_11,iPr_def_11),e2(iPr_def_15,iPr_def_11)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_4787,c_346]) ).
tcf(c_6076,plain,
ifeq(iPr_def_27,iPr_def_27,state(iPr_def_13,iPr_def_14,iPr_def_16,v3(iPr_def_15,o),iPr_def_12,h(iPr_def_11,o),iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_11,iPr_def_15),e2(iPr_def_15,iPr_def_15)),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_4789,c_1247]) ).
tcf(c_6079,plain,
state(iPr_def_13,iPr_def_14,iPr_def_16,v3(iPr_def_15,o),iPr_def_12,h(iPr_def_11,o),iPr_def_20,s2(iPr_def_22,iPr_def_15),iPr_def_23,iPr_def_24,e1(iPr_def_11,iPr_def_15),e2(iPr_def_15,iPr_def_15)) = iPr_def_27,
inference(demodulation,[status(thm)],[c_6076,c_346]) ).
tcf(c_6080,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_6079,c_625]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ039-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 06:41:01 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running UEQ theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 11.61/2.10 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 11.61/2.10 % SZS status Started for theBenchmark.p
% 11.61/2.10 % SZS status Unsatisfiable for theBenchmark.p
% 11.61/2.10
% 11.61/2.10 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 11.61/2.10
% 11.61/2.10 % ------ iProver source info
% 11.61/2.10
% 11.61/2.10 % git: date: 2026-07-19 20:42:38 +0200
% 11.61/2.10 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 11.61/2.10 % git: non_committed_changes: false
% 11.61/2.10
% 11.61/2.10 % ------ Parsing...% successful
% 11.61/2.10
% 11.61/2.10
% 11.61/2.10 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 11.61/2.10
% 11.61/2.10 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 11.61/2.10
% 11.61/2.10 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 11.61/2.10
% 11.61/2.10 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 11.61/2.10 % ------ Proving...
% 11.61/2.10 % ------ Problem Properties
% 11.61/2.10
% 11.61/2.10 %
% 11.61/2.10 % clauses 62
% 11.61/2.10 % conjectures 1
% 11.61/2.10 % EPR 1
% 11.61/2.10 % Horn 62
% 11.61/2.10 % unary 62
% 11.61/2.10 % binary 0
% 11.61/2.10 % lits 62
% 11.61/2.10 % lits eq 62
% 11.61/2.10 % fd_pure 0
% 11.61/2.10 % fd_pseudo 0
% 11.61/2.10 % fd_cond 0
% 11.61/2.10 % fd_pseudo_cond 0
% 11.61/2.10 % AC symbols 0
% 11.61/2.10
% 11.61/2.10 % ------ Input Options Time Limit: Unbounded
% 11.61/2.10
% 11.61/2.10
% 11.61/2.10 % ------
% 11.61/2.10 % Current options:
% 11.61/2.10 % ------
% 11.61/2.10
% 11.61/2.10
% 11.61/2.10 %
% 11.61/2.10
% 11.61/2.10 % ------ Proving...
% 11.61/2.10 %
% 11.61/2.10
% 11.61/2.10 % SZS status Unsatisfiable for theBenchmark.p
% 11.61/2.10
% 11.61/2.10 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 11.61/2.11
% 11.61/2.11
%------------------------------------------------------------------------------