%------------------------------------------------------------------------------
% File : iProver-SAT---3.9.4
% Problem : SWV238+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 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 03:25:01 PM UTC 2026
% Result : CounterSatisfiable 7.59s 7.66s
% Output : Saturation 7.59s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : enc(i(X0),enc(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',enc_dec_cancel) ).
fof(f2,axiom,
! [X0,X1] : enc(X0,enc(i(X0),X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dec_enc_cancel) ).
fof(f3,axiom,
! [X0] : i(i(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',double_inverse_cancel) ).
fof(f4,axiom,
! [X0] :
( p(X0)
=> p(i(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',keys_are_symmetric) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',key_translate_from_ZCMK_to_TMK) ).
fof(f6,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',key_translate_from_TMK_to_ZCMK) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(wk,enc(i(tmk),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',receive_working_key_from_switch) ).
fof(f8,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(enc(i(tmk),X1),enc(i(tmk),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',encrypt_a_PIN_derivation_key_under_a_TMK) ).
fof(f9,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(enc(i(tmk),X1),enc(i(tc),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',encrypt_a_stored_comms_key) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(enc(i(tc),X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',data_encrypt) ).
fof(f11,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(i(enc(i(tc),X0)),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',data_decrypt) ).
fof(f12,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(enc(i(wk),X2),enc(i(enc(i(tmk),X1)),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',data_translate_PIN_from_local_to_interchange_key) ).
fof(f13,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(enc(i(wk),X2),enc(i(enc(i(wk),X1)),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',data_translate_between_interchange_keys) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(enc(i(wk),X1),enc(i(lp),X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',data_translate_PIN_from_local_storage_to_interchange_key) ).
fof(f15,axiom,
! [X0,X1,X2] :
( ( p(X2)
& p(X1)
& p(X0) )
=> p(enc(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',attacker_can_encrypt) ).
fof(f16,axiom,
p(enc(tmk,pp)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_1) ).
fof(f17,axiom,
p(enc(wk,w)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_2) ).
fof(f18,axiom,
p(enc(w,t1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_3) ).
fof(f19,axiom,
p(enc(lp,t2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_4) ).
fof(f20,axiom,
p(enc(tc,k)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_5) ).
fof(f21,axiom,
p(kk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_6) ).
fof(f22,axiom,
p(i(kk)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_7) ).
fof(f23,axiom,
p(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intruder_knows_8) ).
fof(f24,conjecture,
p(enc(pp,a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f25,negated_conjecture,
~ p(enc(pp,a)),
inference(negated_conjecture,[status(cth)],[f24]) ).
fof(f26,plain,
~ p(enc(pp,a)),
inference(flattening,[],[f25]) ).
fof(f27,plain,
! [X0] :
( ~ p(X0)
| p(i(X0)) ),
inference(ennf_transformation,[],[f4]) ).
fof(f28,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0))) ),
inference(ennf_transformation,[],[f5]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0))) ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0))) ),
inference(ennf_transformation,[],[f6]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0))) ),
inference(flattening,[],[f30]) ).
fof(f32,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(wk,enc(i(tmk),X0))) ),
inference(ennf_transformation,[],[f7]) ).
fof(f33,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(wk,enc(i(tmk),X0))) ),
inference(flattening,[],[f32]) ).
fof(f34,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tmk),X1),enc(i(tmk),X0))) ),
inference(ennf_transformation,[],[f8]) ).
fof(f35,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tmk),X1),enc(i(tmk),X0))) ),
inference(flattening,[],[f34]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tmk),X1),enc(i(tc),X0))) ),
inference(ennf_transformation,[],[f9]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tmk),X1),enc(i(tc),X0))) ),
inference(flattening,[],[f36]) ).
fof(f38,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tc),X0),X1)) ),
inference(ennf_transformation,[],[f10]) ).
fof(f39,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tc),X0),X1)) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(i(enc(i(tc),X0)),X1)) ),
inference(ennf_transformation,[],[f11]) ).
fof(f41,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(i(enc(i(tc),X0)),X1)) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X2),enc(i(enc(i(tmk),X1)),X0))) ),
inference(ennf_transformation,[],[f12]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X2),enc(i(enc(i(tmk),X1)),X0))) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X2),enc(i(enc(i(wk),X1)),X0))) ),
inference(ennf_transformation,[],[f13]) ).
fof(f45,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X2),enc(i(enc(i(wk),X1)),X0))) ),
inference(flattening,[],[f44]) ).
fof(f46,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X1),enc(i(lp),X0))) ),
inference(ennf_transformation,[],[f14]) ).
fof(f47,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X1),enc(i(lp),X0))) ),
inference(flattening,[],[f46]) ).
fof(f48,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(X0,X1)) ),
inference(ennf_transformation,[],[f15]) ).
fof(f49,plain,
! [X0,X1,X2] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(X0,X1)) ),
inference(flattening,[],[f48]) ).
fof(f50,plain,
! [X0,X1] : enc(i(X0),enc(X0,X1)) = X1,
inference(cnf_transformation,[],[f1]) ).
fof(f51,plain,
! [X0,X1] : enc(X0,enc(i(X0),X1)) = X1,
inference(cnf_transformation,[],[f2]) ).
fof(f52,plain,
! [X0] : i(i(X0)) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f53,plain,
! [X0] :
( ~ p(X0)
| p(i(X0)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f54,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0))) ),
inference(cnf_transformation,[],[f29]) ).
fof(f55,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0))) ),
inference(cnf_transformation,[],[f31]) ).
fof(f56,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(wk,enc(i(tmk),X0))) ),
inference(cnf_transformation,[],[f33]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tmk),X1),enc(i(tmk),X0))) ),
inference(cnf_transformation,[],[f35]) ).
fof(f58,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tmk),X1),enc(i(tc),X0))) ),
inference(cnf_transformation,[],[f37]) ).
fof(f59,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(tc),X0),X1)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f60,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(i(enc(i(tc),X0)),X1)) ),
inference(cnf_transformation,[],[f41]) ).
fof(f61,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X2),enc(i(enc(i(tmk),X1)),X0))) ),
inference(cnf_transformation,[],[f43]) ).
fof(f62,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X2),enc(i(enc(i(wk),X1)),X0))) ),
inference(cnf_transformation,[],[f45]) ).
fof(f63,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(enc(i(wk),X1),enc(i(lp),X0))) ),
inference(cnf_transformation,[],[f47]) ).
fof(f64,plain,
! [X2,X0,X1] :
( ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| p(enc(X0,X1)) ),
inference(cnf_transformation,[],[f49]) ).
fof(f65,plain,
p(enc(tmk,pp)),
inference(cnf_transformation,[],[f16]) ).
fof(f66,plain,
p(enc(wk,w)),
inference(cnf_transformation,[],[f17]) ).
fof(f67,plain,
p(enc(w,t1)),
inference(cnf_transformation,[],[f18]) ).
fof(f68,plain,
p(enc(lp,t2)),
inference(cnf_transformation,[],[f19]) ).
fof(f69,plain,
p(enc(tc,k)),
inference(cnf_transformation,[],[f20]) ).
fof(f70,plain,
p(kk),
inference(cnf_transformation,[],[f21]) ).
fof(f71,plain,
p(i(kk)),
inference(cnf_transformation,[],[f22]) ).
fof(f72,plain,
p(a),
inference(cnf_transformation,[],[f23]) ).
fof(f73,plain,
~ p(enc(pp,a)),
inference(cnf_transformation,[],[f26]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : enc(i(X0),enc(X0,X1)) = X1,
inference(cnf_transformation,[],[f50]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i] : enc(X0,enc(i(X0),X1)) = X1,
inference(cnf_transformation,[],[f51]) ).
tcf(c_51,plain,
! [X0: $i] : i(i(X0)) = X0,
inference(cnf_transformation,[],[f52]) ).
tcf(c_52,plain,
! [X0: $i] :
( p(i(X0))
| ~ p(X0) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(wk,enc(i(tmk),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X1),enc(i(tmk),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X1),enc(i(tc),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tc),X0),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(tc),X0)),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(i(enc(i(tmk),X1)),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(i(enc(i(wk),X1)),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X1),enc(i(lp),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_64,plain,
p(enc(tmk,pp)),
inference(cnf_transformation,[],[f65]) ).
tcf(c_65,plain,
p(enc(wk,w)),
inference(cnf_transformation,[],[f66]) ).
tcf(c_66,plain,
p(enc(w,t1)),
inference(cnf_transformation,[],[f67]) ).
tcf(c_67,plain,
p(enc(lp,t2)),
inference(cnf_transformation,[],[f68]) ).
tcf(c_68,plain,
p(enc(tc,k)),
inference(cnf_transformation,[],[f69]) ).
tcf(c_69,plain,
p(kk),
inference(cnf_transformation,[],[f70]) ).
tcf(c_70,plain,
p(i(kk)),
inference(cnf_transformation,[],[f71]) ).
tcf(c_71,plain,
p(a),
inference(cnf_transformation,[],[f72]) ).
tcf(c_72,negated_conjecture,
~ p(enc(pp,a)),
inference(cnf_transformation,[],[f73]) ).
tcf(c_100,plain,
! [X0: $i] :
( p(X0)
| ~ p(i(X0)) ),
inference(superposition,[status(thm)],[c_51,c_52]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,X1))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(i(X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_127]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(i(X0),X1)) ),
inference(superposition,[status(thm)],[c_50,c_127]) ).
tcf(c_149,plain,
( ~ p(a)
| ~ p(pp) ),
inference(superposition,[status(thm)],[c_127,c_72]) ).
tcf(c_150,plain,
~ p(pp),
inference(forward_subsumption_resolution,[status(thm)],[c_149,c_71]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_55]) ).
tcf(c_188,plain,
( p(pp)
| ~ p(i(tmk)) ),
inference(superposition,[status(thm)],[c_64,c_147]) ).
tcf(c_191,plain,
( p(t2)
| ~ p(i(lp)) ),
inference(superposition,[status(thm)],[c_67,c_147]) ).
tcf(c_192,plain,
( p(k)
| ~ p(i(tc)) ),
inference(superposition,[status(thm)],[c_68,c_147]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X0),X1))
| ~ p(X1)
| ~ p(i(X0)) ),
inference(superposition,[status(thm)],[c_50,c_147]) ).
tcf(c_203,plain,
~ p(i(tmk)),
inference(forward_subsumption_resolution,[status(thm)],[c_188,c_150]) ).
tcf(c_218,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tc),X0),X1))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_58]) ).
tcf(c_232,plain,
~ p(tmk),
inference(superposition,[status(thm)],[c_52,c_203]) ).
tcf(c_243,plain,
! [X0: $i,X1: $i] :
( p(enc(i(enc(i(tc),X0)),X1))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_59]) ).
tcf(c_278,plain,
! [X0: $i,X1: $i] :
( p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_53]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_56]) ).
tcf(c_348,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),enc(i(tc),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_57]) ).
tcf(c_383,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(lp),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_62]) ).
tcf(c_418,plain,
! [X0: $i,X1: $i] :
( p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_54]) ).
tcf(c_440,plain,
! [X0: $i] :
( p(enc(wk,enc(i(tmk),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_167]) ).
tcf(c_456,plain,
! [X0: $i] :
( p(enc(wk,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_440]) ).
tcf(c_476,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(enc(i(tmk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_60]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(tmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_60]) ).
tcf(c_480,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X1),enc(i(X0),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_60]) ).
tcf(c_517,plain,
p(enc(wk,pp)),
inference(superposition,[status(thm)],[c_64,c_456]) ).
tcf(c_519,plain,
( p(pp)
| ~ p(i(wk)) ),
inference(superposition,[status(thm)],[c_517,c_147]) ).
tcf(c_520,plain,
~ p(i(wk)),
inference(forward_subsumption_resolution,[status(thm)],[c_519,c_150]) ).
tcf(c_530,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(enc(i(wk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_61]) ).
tcf(c_532,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(wk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_61]) ).
tcf(c_534,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X1),enc(i(X0),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_61]) ).
tcf(c_566,plain,
~ p(wk),
inference(superposition,[status(thm)],[c_52,c_520]) ).
tcf(c_574,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(i(enc(i(tc),X0)),X1)) ),
inference(superposition,[status(thm)],[c_50,c_218]) ).
tcf(c_575,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,X1))
| ~ p(X1)
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_218]) ).
tcf(c_602,plain,
! [X0: $i] :
( p(enc(k,X0))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_68,c_575]) ).
tcf(c_614,plain,
! [X0: $i] :
( p(X0)
| ~ p(enc(i(k),X0)) ),
inference(superposition,[status(thm)],[c_50,c_602]) ).
tcf(c_637,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(tc),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_243]) ).
tcf(c_639,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X0),X1))
| ~ p(X1)
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_243]) ).
tcf(c_664,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_637]) ).
tcf(c_686,plain,
( p(pp)
| ~ p(enc(tc,tmk)) ),
inference(superposition,[status(thm)],[c_64,c_664]) ).
tcf(c_689,plain,
( p(t2)
| ~ p(enc(tc,lp)) ),
inference(superposition,[status(thm)],[c_67,c_664]) ).
tcf(c_690,plain,
( p(k)
| ~ p(enc(tc,tc)) ),
inference(superposition,[status(thm)],[c_68,c_664]) ).
tcf(c_691,plain,
( p(pp)
| ~ p(enc(tc,wk)) ),
inference(superposition,[status(thm)],[c_517,c_664]) ).
tcf(c_693,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,X1))
| ~ p(X1)
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_664]) ).
tcf(c_695,plain,
~ p(enc(tc,wk)),
inference(forward_subsumption_resolution,[status(thm)],[c_691,c_150]) ).
tcf(c_702,plain,
~ p(enc(tc,tmk)),
inference(forward_subsumption_resolution,[status(thm)],[c_686,c_150]) ).
tcf(c_747,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X0),X1))
| ~ p(tc)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_127,c_639]) ).
tcf(c_748,plain,
! [X0: $i] :
( p(enc(i(k),X0))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_68,c_639]) ).
tcf(c_760,plain,
! [X0: $i] :
( p(X0)
| ~ p(enc(k,X0)) ),
inference(superposition,[status(thm)],[c_49,c_748]) ).
tcf(c_818,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(i(X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_574]) ).
tcf(c_841,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(X0,X1))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_818]) ).
tcf(c_861,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X0),X1))
| ~ p(X0)
| ~ p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_747,c_52,c_194]) ).
tcf(c_862,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X0),X1))
| ~ p(X1)
| ~ p(X0) ),
inference(renaming,[status(thm)],[c_861]) ).
tcf(c_869,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_862]) ).
tcf(c_871,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,X1))
| ~ p(X1)
| ~ p(i(X0)) ),
inference(superposition,[status(thm)],[c_51,c_862]) ).
tcf(c_925,plain,
! [X0: $i] :
( p(enc(kk,X0))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_70,c_871]) ).
tcf(c_933,plain,
! [X0: $i] :
( p(X0)
| ~ p(enc(i(kk),X0)) ),
inference(superposition,[status(thm)],[c_50,c_925]) ).
tcf(c_965,plain,
! [X0: $i,X1: $i] :
( p(enc(tmk,X1))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_278]) ).
tcf(c_967,plain,
! [X0: $i,X1: $i] :
( p(enc(tmk,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_278]) ).
tcf(c_972,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_456]) ).
tcf(c_996,plain,
! [X0: $i,X1: $i] :
( p(enc(tmk,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_965]) ).
tcf(c_1033,plain,
( p(enc(tmk,w))
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_996]) ).
tcf(c_1035,plain,
( p(enc(tmk,t2))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_996]) ).
tcf(c_1036,plain,
( p(enc(tmk,k))
| ~ p(enc(zcmk,tc)) ),
inference(superposition,[status(thm)],[c_68,c_996]) ).
tcf(c_1042,plain,
! [X0: $i,X1: $i] :
( p(enc(tmk,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_996]) ).
tcf(c_1184,plain,
! [X0: $i,X1: $i] :
( p(enc(tmk,enc(X0,X1)))
| ~ p(zcmk)
| ~ p(X1)
| ~ p(i(X0)) ),
inference(superposition,[status(thm)],[c_127,c_1042]) ).
tcf(c_1220,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(tmk),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_313]) ).
tcf(c_1222,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_313]) ).
tcf(c_1226,plain,
! [X0: $i,X1: $i] :
( p(enc(i(tmk),X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tc,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_313,c_664]) ).
tcf(c_1321,plain,
! [X0: $i] :
( p(enc(pp,enc(i(tmk),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_1220]) ).
tcf(c_1359,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1321]) ).
tcf(c_1396,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_1359]) ).
tcf(c_1398,plain,
p(enc(pp,pp)),
inference(superposition,[status(thm)],[c_64,c_1359]) ).
tcf(c_1425,plain,
( p(pp)
| ~ p(enc(tc,pp)) ),
inference(superposition,[status(thm)],[c_1398,c_664]) ).
tcf(c_1426,plain,
( p(pp)
| ~ p(i(pp)) ),
inference(superposition,[status(thm)],[c_1398,c_147]) ).
tcf(c_1427,plain,
~ p(i(pp)),
inference(forward_subsumption_resolution,[status(thm)],[c_1426,c_150]) ).
tcf(c_1428,plain,
~ p(enc(tc,pp)),
inference(forward_subsumption_resolution,[status(thm)],[c_1425,c_150]) ).
tcf(c_1458,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(tmk,enc(i(enc(i(tmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_50,c_1222]) ).
tcf(c_1459,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,X1))
| ~ p(enc(tmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1222]) ).
tcf(c_1464,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(tmk,X1))
| ~ p(i(enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_1222,c_147]) ).
tcf(c_1523,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X1),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_278,c_1459]) ).
tcf(c_1592,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(tc),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_348]) ).
tcf(c_1594,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_348]) ).
tcf(c_1649,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),enc(i(tc),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_1592]) ).
tcf(c_1651,plain,
! [X0: $i] :
( p(enc(pp,enc(i(tc),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_1592]) ).
tcf(c_1691,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1651]) ).
tcf(c_1709,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(tc)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_127,c_1691]) ).
tcf(c_1710,plain,
p(enc(pp,k)),
inference(superposition,[status(thm)],[c_68,c_1691]) ).
tcf(c_1744,plain,
( p(enc(tmk,k))
| ~ p(enc(zcmk,pp)) ),
inference(superposition,[status(thm)],[c_1710,c_996]) ).
tcf(c_1766,plain,
( ~ p(a)
| ~ p(tc) ),
inference(superposition,[status(thm)],[c_1709,c_72]) ).
tcf(c_1767,plain,
~ p(tc),
inference(forward_subsumption_resolution,[status(thm)],[c_1766,c_71]) ).
tcf(c_1776,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),k))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_68,c_1594]) ).
tcf(c_1784,plain,
! [X0: $i] :
( p(enc(X0,k))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1776]) ).
tcf(c_1786,plain,
! [X0: $i] :
( p(enc(tmk,k))
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_1776,c_996]) ).
tcf(c_1788,plain,
! [X0: $i] :
( p(k)
| ~ p(X0)
| ~ p(enc(tc,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_1776,c_664]) ).
tcf(c_1812,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),k))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_1784]) ).
tcf(c_1894,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(lp),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_383]) ).
tcf(c_1896,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(enc(lp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_383]) ).
tcf(c_1900,plain,
! [X0: $i,X1: $i] :
( p(enc(i(lp),X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tc,enc(i(wk),X0))) ),
inference(superposition,[status(thm)],[c_383,c_664]) ).
tcf(c_2018,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X0),enc(i(lp),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_440,c_1894]) ).
tcf(c_2020,plain,
! [X0: $i] :
( p(enc(w,enc(i(lp),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_65,c_1894]) ).
tcf(c_2021,plain,
! [X0: $i] :
( p(enc(pp,enc(i(lp),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_517,c_1894]) ).
tcf(c_2047,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(enc(lp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2020]) ).
tcf(c_2084,plain,
p(enc(w,t2)),
inference(superposition,[status(thm)],[c_67,c_2047]) ).
tcf(c_2162,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),t2))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_67,c_1896]) ).
tcf(c_2174,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(enc(lp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2021]) ).
tcf(c_2207,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(lp)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_127,c_2174]) ).
tcf(c_2208,plain,
p(enc(pp,t2)),
inference(superposition,[status(thm)],[c_67,c_2174]) ).
tcf(c_2247,plain,
! [X0: $i] :
( p(enc(X0,t2))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2162]) ).
tcf(c_2275,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),t2))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_440,c_2247]) ).
tcf(c_2363,plain,
( ~ p(a)
| ~ p(lp) ),
inference(superposition,[status(thm)],[c_2207,c_72]) ).
tcf(c_2364,plain,
~ p(lp),
inference(forward_subsumption_resolution,[status(thm)],[c_2363,c_71]) ).
tcf(c_2371,plain,
! [X0: $i] :
( p(enc(X0,t2))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2275]) ).
tcf(c_2374,plain,
! [X0: $i] :
( p(t2)
| ~ p(X0)
| ~ p(enc(i(tmk),X0)) ),
inference(superposition,[status(thm)],[c_2275,c_869]) ).
tcf(c_2375,plain,
! [X0: $i] :
( p(t2)
| ~ p(X0)
| ~ p(enc(tc,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_2275,c_664]) ).
tcf(c_2399,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),t2))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_2371]) ).
tcf(c_2516,plain,
! [X0: $i] :
( p(t2)
| ~ p(X0)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2374]) ).
tcf(c_2530,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(i(enc(i(zcmk),X0)),X1)) ),
inference(superposition,[status(thm)],[c_278,c_2516]) ).
tcf(c_2683,plain,
! [X0: $i] :
( p(k)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1788]) ).
tcf(c_2697,plain,
! [X0: $i,X1: $i] :
( p(k)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tc,enc(i(enc(i(zcmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_278,c_2683]) ).
tcf(c_2758,plain,
! [X0: $i] :
( p(t2)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2375]) ).
tcf(c_2798,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tc,enc(i(enc(i(zcmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_278,c_2758]) ).
tcf(c_2837,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(tmk,X0))
| ~ p(enc(tmk,enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_1458]) ).
tcf(c_2908,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(tmk,i(X0)))
| ~ p(enc(tmk,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_51,c_2837]) ).
tcf(c_2959,plain,
! [X0: $i] :
( p(enc(tmk,k))
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1786]) ).
tcf(c_3084,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,X1))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_972]) ).
tcf(c_3086,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_972]) ).
tcf(c_3097,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),enc(i(lp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_972,c_1894]) ).
tcf(c_3122,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_3084]) ).
tcf(c_3148,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_3122]) ).
tcf(c_3156,plain,
( p(enc(wk,t2))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_3122]) ).
tcf(c_3158,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_3122]) ).
tcf(c_3161,plain,
! [X0: $i] :
( p(enc(wk,X0))
| ~ p(X0)
| ~ p(enc(zcmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_3122]) ).
tcf(c_3162,plain,
! [X0: $i] :
( p(enc(wk,X0))
| ~ p(X0)
| ~ p(enc(zcmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_3122]) ).
tcf(c_3176,plain,
! [X0: $i,X1: $i] :
( p(enc(wk,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_3122]) ).
tcf(c_3639,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X0),enc(i(tmk),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_418]) ).
tcf(c_3641,plain,
! [X0: $i,X1: $i] :
( p(enc(i(enc(i(zcmk),X1)),X0))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_418]) ).
tcf(c_3755,plain,
! [X0: $i] :
( p(enc(tmk,enc(kk,X0)))
| ~ p(zcmk)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_70,c_1184]) ).
tcf(c_3790,plain,
! [X0: $i] :
( p(enc(pp,enc(kk,X0)))
| ~ p(zcmk)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_3755,c_1359]) ).
tcf(c_4501,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(tmk,enc(enc(i(zcmk),X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_3641]) ).
tcf(c_4503,plain,
! [X0: $i,X1: $i] :
( p(enc(i(X1),X0))
| ~ p(enc(zcmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_3641]) ).
tcf(c_4619,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_49,c_4501]) ).
tcf(c_4637,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(zcmk)
| ~ p(enc(i(kk),X0)) ),
inference(superposition,[status(thm)],[c_50,c_3790]) ).
tcf(c_4654,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(kk)
| ~ p(zcmk)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_862,c_4637]) ).
tcf(c_4659,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(zcmk)
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4654,c_69]) ).
tcf(c_4723,plain,
( ~ p(a)
| ~ p(zcmk) ),
inference(superposition,[status(thm)],[c_4659,c_72]) ).
tcf(c_4724,plain,
~ p(zcmk),
inference(forward_subsumption_resolution,[status(thm)],[c_4723,c_71]) ).
tcf(c_4734,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,X1))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_4619]) ).
tcf(c_4755,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(X0),enc(i(enc(i(zcmk),X2)),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_278,c_4503]) ).
tcf(c_4757,plain,
! [X0: $i] :
( p(enc(i(X0),pp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_64,c_4503]) ).
tcf(c_4771,plain,
! [X0: $i] :
( p(enc(i(enc(i(zcmk),X0)),pp))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_4757]) ).
tcf(c_4782,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(i(enc(i(zcmk),X0))) ),
inference(superposition,[status(thm)],[c_4771,c_869]) ).
tcf(c_4783,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(enc(tc,i(enc(i(zcmk),X0)))) ),
inference(superposition,[status(thm)],[c_4771,c_664]) ).
tcf(c_4785,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(enc(tc,enc(i(zcmk),X0))) ),
inference(superposition,[status(thm)],[c_4771,c_818]) ).
tcf(c_4786,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(enc(i(zcmk),X0)) ),
inference(superposition,[status(thm)],[c_4771,c_148]) ).
tcf(c_4787,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(i(zcmk),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4786,c_150]) ).
tcf(c_4790,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(i(enc(i(zcmk),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4782,c_150]) ).
tcf(c_4795,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(tc,enc(i(zcmk),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4785,c_150]) ).
tcf(c_4801,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(tc,i(enc(i(zcmk),X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4783,c_150]) ).
tcf(c_4810,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(i(zcmk)) ),
inference(superposition,[status(thm)],[c_127,c_4787]) ).
tcf(c_4812,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_4787]) ).
tcf(c_4825,plain,
! [X0: $i] :
( ~ p(i(X0))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_4790]) ).
tcf(c_4847,plain,
! [X0: $i] :
( ~ p(enc(tc,X0))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_4795]) ).
tcf(c_4866,plain,
~ p(enc(zcmk,k)),
inference(superposition,[status(thm)],[c_68,c_4847]) ).
tcf(c_4867,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_50,c_4847]) ).
tcf(c_4876,plain,
! [X0: $i] :
( ~ p(enc(zcmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_4801]) ).
tcf(c_4900,plain,
! [X0: $i] :
( ~ p(enc(tc,X0))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_4876]) ).
tcf(c_4985,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_1396]) ).
tcf(c_4987,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1396]) ).
tcf(c_5014,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_4985]) ).
tcf(c_5045,plain,
( p(enc(pp,w))
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_5014]) ).
tcf(c_5070,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_5014]) ).
tcf(c_5238,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,k))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_1812]) ).
tcf(c_5240,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),k))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1812]) ).
tcf(c_5268,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,k))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_5238]) ).
tcf(c_5300,plain,
( p(enc(t2,k))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_5268]) ).
tcf(c_5325,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),k))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_5268]) ).
tcf(c_5871,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(lp),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2018]) ).
tcf(c_5873,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(enc(lp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2018]) ).
tcf(c_5965,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,t2))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_2399]) ).
tcf(c_5967,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),t2))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_2399]) ).
tcf(c_5999,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,t2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_5965]) ).
tcf(c_6047,plain,
( p(enc(t2,t2))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_5999]) ).
tcf(c_6077,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),t2))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_5999]) ).
tcf(c_6864,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(i(X0))
| ~ p(enc(tmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1464]) ).
tcf(c_7663,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_2530]) ).
tcf(c_7703,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_7663]) ).
tcf(c_7753,plain,
! [X0: $i] :
( p(t2)
| ~ p(k)
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_1776,c_7703]) ).
tcf(c_8060,plain,
! [X0: $i] :
( p(t2)
| ~ p(k)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_7753]) ).
tcf(c_9618,plain,
! [X0: $i,X1: $i] :
( p(enc(i(tmk),X1))
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1226]) ).
tcf(c_9637,plain,
! [X0: $i] :
( p(enc(i(tmk),X0))
| ~ p(X0)
| ~ p(enc(tmk,k)) ),
inference(superposition,[status(thm)],[c_68,c_9618]) ).
tcf(c_9638,plain,
! [X0: $i,X1: $i] :
( p(enc(i(tmk),X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_50,c_9618]) ).
tcf(c_9740,plain,
! [X0: $i,X1: $i] :
( p(enc(i(lp),X1))
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1900]) ).
tcf(c_9759,plain,
! [X0: $i] :
( p(enc(i(lp),X0))
| ~ p(X0)
| ~ p(enc(wk,k)) ),
inference(superposition,[status(thm)],[c_68,c_9740]) ).
tcf(c_9760,plain,
! [X0: $i,X1: $i] :
( p(enc(i(lp),X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_50,c_9740]) ).
tcf(c_9784,plain,
! [X0: $i,X1: $i] :
( p(k)
| ~ p(X0)
| ~ p(enc(tc,X1))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_2697]) ).
tcf(c_9814,plain,
! [X0: $i,X1: $i] :
( p(k)
| ~ p(enc(tc,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_9784]) ).
tcf(c_9867,plain,
! [X0: $i] :
( p(k)
| ~ p(X0)
| ~ p(enc(tc,k))
| ~ p(enc(zcmk,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_1776,c_9814]) ).
tcf(c_9923,plain,
! [X0: $i] :
( p(k)
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(tmk),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9867,c_68]) ).
tcf(c_10273,plain,
! [X0: $i] :
( p(k)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_9923]) ).
tcf(c_10289,plain,
! [X0: $i] :
( p(t2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_8060,c_10273]) ).
tcf(c_10304,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(enc(i(zcmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_278,c_10289]) ).
tcf(c_10470,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X0)
| ~ p(enc(tc,X1))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_2798]) ).
tcf(c_10515,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(enc(tc,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_10470]) ).
tcf(c_10552,plain,
( p(t2)
| ~ p(enc(tc,t2))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_10515]) ).
tcf(c_11707,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(X0)
| ~ p(enc(zcmk,X1))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_10304]) ).
tcf(c_11754,plain,
! [X0: $i,X1: $i] :
( p(t2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_11707]) ).
tcf(c_11801,plain,
( p(t2)
| ~ p(enc(zcmk,t2))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_11754]) ).
tcf(c_12137,plain,
( ~ p(enc(zcmk,t2))
| ~ p(enc(zcmk,lp)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11801,c_4812]) ).
tcf(c_12961,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X0),enc(i(enc(i(tmk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_440,c_476]) ).
tcf(c_12963,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_65,c_476]) ).
tcf(c_12964,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_517,c_476]) ).
tcf(c_12992,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X0)
| ~ p(enc(enc(i(tmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_12963]) ).
tcf(c_12994,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_12963]) ).
tcf(c_13103,plain,
! [X0: $i] :
( p(enc(w,k))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_1776,c_12992]) ).
tcf(c_13107,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_12992]) ).
tcf(c_13375,plain,
p(enc(w,k)),
inference(superposition,[status(thm)],[c_2084,c_13103]) ).
tcf(c_13401,plain,
( p(enc(tmk,k))
| ~ p(enc(zcmk,w)) ),
inference(superposition,[status(thm)],[c_13375,c_996]) ).
tcf(c_13468,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_13107]) ).
tcf(c_13474,plain,
( p(enc(w,w))
| ~ p(enc(tmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_13107]) ).
tcf(c_13478,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_13107]) ).
tcf(c_13481,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(X0)
| ~ p(enc(tmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_13107]) ).
tcf(c_13482,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(X0)
| ~ p(enc(tmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_13107]) ).
tcf(c_13486,plain,
! [X0: $i] :
( p(enc(w,enc(i(tmk),X0)))
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1321,c_13107]) ).
tcf(c_13487,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1396,c_13107]) ).
tcf(c_13488,plain,
( p(enc(w,pp))
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1398,c_13107]) ).
tcf(c_13491,plain,
! [X0: $i] :
( p(enc(w,enc(i(tc),X0)))
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1651,c_13107]) ).
tcf(c_13503,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(tmk,pp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_4987,c_13107]) ).
tcf(c_13511,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_13107]) ).
tcf(c_13513,plain,
p(enc(w,pp)),
inference(forward_subsumption_resolution,[status(thm)],[c_13488,c_64]) ).
tcf(c_13528,plain,
! [X0: $i] :
( p(enc(w,enc(i(tc),X0)))
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13491,c_64]) ).
tcf(c_13531,plain,
! [X0: $i] :
( p(enc(w,enc(i(tmk),X0)))
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13486,c_64]) ).
tcf(c_13550,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13503,c_64]) ).
tcf(c_13558,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13487,c_64]) ).
tcf(c_13657,plain,
( p(pp)
| ~ p(w) ),
inference(superposition,[status(thm)],[c_13513,c_869]) ).
tcf(c_13658,plain,
( p(pp)
| ~ p(enc(tc,w)) ),
inference(superposition,[status(thm)],[c_13513,c_664]) ).
tcf(c_13659,plain,
( p(pp)
| ~ p(i(w)) ),
inference(superposition,[status(thm)],[c_13513,c_147]) ).
tcf(c_13660,plain,
~ p(w),
inference(forward_subsumption_resolution,[status(thm)],[c_13657,c_150]) ).
tcf(c_13661,plain,
~ p(i(w)),
inference(forward_subsumption_resolution,[status(thm)],[c_13659,c_150]) ).
tcf(c_13662,plain,
~ p(enc(tc,w)),
inference(forward_subsumption_resolution,[status(thm)],[c_13658,c_150]) ).
tcf(c_13813,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_13528]) ).
tcf(c_13893,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_13531]) ).
tcf(c_13981,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_478]) ).
tcf(c_14050,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_13981]) ).
tcf(c_14056,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),w))
| ~ p(X0)
| ~ p(enc(tmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_13981]) ).
tcf(c_14060,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_13981]) ).
tcf(c_14063,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_13981]) ).
tcf(c_14064,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_13981]) ).
tcf(c_14068,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1321,c_13981]) ).
tcf(c_14070,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),pp))
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1398,c_13981]) ).
tcf(c_14072,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),k))
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1710,c_13981]) ).
tcf(c_14073,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(tc),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,pp)) ),
inference(superposition,[status(thm)],[c_1651,c_13981]) ).
tcf(c_14085,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(i(X0),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,pp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_4987,c_13981]) ).
tcf(c_14097,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(X0,X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_13981]) ).
tcf(c_14105,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),k))
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14072,c_64]) ).
tcf(c_14108,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),pp))
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14070,c_64]) ).
tcf(c_14145,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(tc),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14073,c_64]) ).
tcf(c_14149,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14068,c_64]) ).
tcf(c_14182,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(i(X0),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14085,c_64]) ).
tcf(c_14258,plain,
! [X0: $i] :
( p(enc(X0,k))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14105]) ).
tcf(c_14266,plain,
! [X0: $i] :
( p(k)
| ~ p(X0)
| ~ p(enc(tc,k))
| ~ p(enc(zcmk,enc(i(wk),X0))) ),
inference(superposition,[status(thm)],[c_14105,c_9814]) ).
tcf(c_14275,plain,
! [X0: $i] :
( p(enc(tmk,k))
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(wk),X0))) ),
inference(superposition,[status(thm)],[c_14105,c_996]) ).
tcf(c_14316,plain,
! [X0: $i] :
( p(k)
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(wk),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14266,c_68]) ).
tcf(c_14325,plain,
( p(enc(tmk,k))
| ~ p(enc(wk,tmk)) ),
inference(instantiation,[status(thm)],[c_14258]) ).
tcf(c_14414,plain,
! [X0: $i] :
( p(enc(X0,pp))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14108]) ).
tcf(c_14432,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(enc(i(wk),X0)) ),
inference(superposition,[status(thm)],[c_14108,c_869]) ).
tcf(c_14433,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(enc(tc,enc(i(wk),X0))) ),
inference(superposition,[status(thm)],[c_14108,c_664]) ).
tcf(c_14434,plain,
! [X0: $i] :
( p(pp)
| ~ p(X0)
| ~ p(i(enc(i(wk),X0))) ),
inference(superposition,[status(thm)],[c_14108,c_147]) ).
tcf(c_14437,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(i(wk),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14432,c_150]) ).
tcf(c_14442,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(i(enc(i(wk),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14434,c_150]) ).
tcf(c_14445,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(tc,enc(i(wk),X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_14433,c_150]) ).
tcf(c_14466,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14437]) ).
tcf(c_14476,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,i(enc(i(tc),X0)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3148,c_14466]) ).
tcf(c_14477,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,kk)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3162,c_14466]) ).
tcf(c_14478,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,i(X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3158,c_14466]) ).
tcf(c_14479,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,i(k))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3161,c_14466]) ).
tcf(c_14490,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(i(tmk),X0)) ),
inference(superposition,[status(thm)],[c_440,c_14466]) ).
tcf(c_14494,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(i(enc(i(zcmk),X0)),X1)) ),
inference(superposition,[status(thm)],[c_972,c_14466]) ).
tcf(c_14511,plain,
! [X0: $i] :
( ~ p(i(X0))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14442]) ).
tcf(c_14521,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),pp))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_440,c_14414]) ).
tcf(c_14525,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),pp))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_972,c_14414]) ).
tcf(c_14542,plain,
! [X0: $i] :
( ~ p(enc(tc,X0))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14445]) ).
tcf(c_14552,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(i(enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_440,c_14511]) ).
tcf(c_14556,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(i(enc(i(enc(i(zcmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_972,c_14511]) ).
tcf(c_14569,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(tmk,k)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_9637,c_14490]) ).
tcf(c_14570,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,enc(i(tc),X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_9638,c_14490]) ).
tcf(c_14592,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14490]) ).
tcf(c_14604,plain,
! [X0: $i,X1: $i] :
( ~ p(i(X0))
| ~ p(enc(tmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6864,c_14592]) ).
tcf(c_14627,plain,
~ p(enc(zcmk,pp)),
inference(backward_subsumption_resolution,[status(thm)],[c_1744,c_14569]) ).
tcf(c_14628,plain,
~ p(enc(zcmk,w)),
inference(backward_subsumption_resolution,[status(thm)],[c_13401,c_14569]) ).
tcf(c_14629,plain,
! [X0: $i] :
( ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2959,c_14569]) ).
tcf(c_14630,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,enc(i(tmk),X0))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1786,c_14569]) ).
tcf(c_14631,plain,
~ p(enc(zcmk,tc)),
inference(backward_subsumption_resolution,[status(thm)],[c_1036,c_14569]) ).
tcf(c_14642,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(tc,enc(i(tmk),X0))) ),
inference(superposition,[status(thm)],[c_440,c_14542]) ).
tcf(c_14646,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(tc,enc(i(enc(i(zcmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_972,c_14542]) ).
tcf(c_14659,plain,
! [X0: $i] :
( ~ p(i(X0))
| ~ p(enc(tmk,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_14604,c_456,c_14511]) ).
tcf(c_14684,plain,
! [X0: $i] :
( p(enc(X0,pp))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14521]) ).
tcf(c_14719,plain,
! [X0: $i] :
( ~ p(enc(tc,X0))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14642]) ).
tcf(c_14737,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,enc(i(enc(i(zcmk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_278,c_14629]) ).
tcf(c_14784,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_14494]) ).
tcf(c_14786,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(i(X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_14494]) ).
tcf(c_14818,plain,
! [X0: $i,X1: $i] :
( ~ p(X0)
| ~ p(i(X1))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_14556]) ).
tcf(c_14820,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(i(enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_14556]) ).
tcf(c_14842,plain,
! [X0: $i,X1: $i] :
( ~ p(X0)
| ~ p(enc(tc,X1))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_14646]) ).
tcf(c_14844,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tc,enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_14646]) ).
tcf(c_14866,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_14784]) ).
tcf(c_14894,plain,
( ~ p(t2)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_14866]) ).
tcf(c_14930,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(X0,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_14866]) ).
tcf(c_14996,plain,
( ~ p(enc(tc,t2))
| ~ p(enc(zcmk,lp)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_10552,c_14894]) ).
tcf(c_15054,plain,
! [X0: $i,X1: $i] :
( ~ p(i(X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_14818]) ).
tcf(c_15083,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(i(enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_51,c_14820]) ).
tcf(c_15108,plain,
( ~ p(i(t2))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_15054]) ).
tcf(c_15251,plain,
! [X0: $i] :
( p(enc(X0,w))
| ~ p(enc(tmk,wk))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14056]) ).
tcf(c_15317,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),w))
| ~ p(X0)
| ~ p(enc(tmk,wk)) ),
inference(superposition,[status(thm)],[c_440,c_15251]) ).
tcf(c_15320,plain,
( p(enc(pp,w))
| ~ p(enc(tmk,wk)) ),
inference(superposition,[status(thm)],[c_517,c_15251]) ).
tcf(c_15321,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),w))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,wk)) ),
inference(superposition,[status(thm)],[c_972,c_15251]) ).
tcf(c_15490,plain,
! [X0: $i,X1: $i] :
( ~ p(enc(tc,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_14842]) ).
tcf(c_15513,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(tc,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_51,c_14844]) ).
tcf(c_15526,plain,
! [X0: $i] :
( ~ p(enc(zcmk,enc(i(wk),X0)))
| ~ p(X0) ),
inference(global_subsumption_just,[status(thm)],[c_14316,c_14275,c_14569]) ).
tcf(c_15527,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,enc(i(wk),X0))) ),
inference(renaming,[status(thm)],[c_15526]) ).
tcf(c_15533,plain,
! [X0: $i] :
( ~ p(enc(wk,X0))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15527]) ).
tcf(c_15744,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(X0),X2)))
| ~ p(X2)
| ~ p(enc(wk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_480]) ).
tcf(c_15873,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X0,enc(i(enc(i(enc(i(zcmk),X2)),X1)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_278,c_15744]) ).
tcf(c_15875,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(pp),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_64,c_15744]) ).
tcf(c_15893,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X0),enc(i(pp),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_440,c_15875]) ).
tcf(c_15895,plain,
! [X0: $i] :
( p(enc(w,enc(i(pp),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_65,c_15875]) ).
tcf(c_15897,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),enc(i(pp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_972,c_15875]) ).
tcf(c_15898,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X0),enc(i(pp),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_15875]) ).
tcf(c_15917,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(enc(pp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15895]) ).
tcf(c_15972,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_13550]) ).
tcf(c_15974,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_13550]) ).
tcf(c_16027,plain,
( p(enc(w,w))
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_15972]) ).
tcf(c_16120,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(enc(pp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15898]) ).
tcf(c_16223,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X0),enc(i(enc(i(wk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_440,c_530]) ).
tcf(c_16225,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(enc(i(wk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_65,c_530]) ).
tcf(c_16226,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(i(enc(i(wk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_517,c_530]) ).
tcf(c_16227,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),enc(i(enc(i(wk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_972,c_530]) ).
tcf(c_16255,plain,
! [X0: $i,X1: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,X1))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_14737]) ).
tcf(c_16257,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(zcmk,enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_14737]) ).
tcf(c_16277,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X0)
| ~ p(enc(enc(i(wk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_16225]) ).
tcf(c_16279,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_16225]) ).
tcf(c_16335,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(enc(wk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_16277]) ).
tcf(c_16381,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_218,c_16335]) ).
tcf(c_16382,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_16335]) ).
tcf(c_16388,plain,
( p(enc(w,w))
| ~ p(enc(wk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_16335]) ).
tcf(c_16392,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_16335]) ).
tcf(c_16395,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(X0)
| ~ p(enc(wk,k)) ),
inference(superposition,[status(thm)],[c_602,c_16335]) ).
tcf(c_16396,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(X0)
| ~ p(enc(wk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_16335]) ).
tcf(c_16397,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(X0)
| ~ p(enc(wk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_16335]) ).
tcf(c_16433,plain,
! [X0: $i,X1: $i] :
( p(enc(w,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_16335]) ).
tcf(c_16587,plain,
! [X0: $i,X1: $i] :
( ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_16255]) ).
tcf(c_16667,plain,
! [X0: $i,X1: $i] :
( ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(zcmk,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_49,c_16587]) ).
tcf(c_16759,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(zcmk,zcmk)) ),
inference(superposition,[status(thm)],[c_50,c_16257]) ).
tcf(c_16811,plain,
! [X0: $i] :
( p(enc(X0,w))
| ~ p(enc(tmk,wk))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15317]) ).
tcf(c_16979,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X0)
| ~ p(enc(enc(i(tmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_12964]) ).
tcf(c_16981,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_12964]) ).
tcf(c_17032,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_16979]) ).
tcf(c_17074,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_17032]) ).
tcf(c_17084,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_17032]) ).
tcf(c_17088,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(X0)
| ~ p(enc(tmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_17032]) ).
tcf(c_17089,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(X0)
| ~ p(enc(tmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_17032]) ).
tcf(c_17129,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_17032]) ).
tcf(c_17310,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_13558]) ).
tcf(c_17382,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(tc),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14145]) ).
tcf(c_17384,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14145]) ).
tcf(c_17483,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(tmk),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14149]) ).
tcf(c_17485,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14149]) ).
tcf(c_17573,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(X0)
| ~ p(enc(tmk,enc(i(enc(i(wk),X0)),X1))) ),
inference(superposition,[status(thm)],[c_50,c_17485]) ).
tcf(c_17574,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,X0))
| ~ p(enc(wk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_17485]) ).
tcf(c_17690,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,pp))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_14525]) ).
tcf(c_17692,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),pp))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_14525]) ).
tcf(c_17738,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,pp))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_17690]) ).
tcf(c_17769,plain,
( p(enc(t2,pp))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_17738]) ).
tcf(c_17822,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),pp))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_17738]) ).
tcf(c_17893,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(pp),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15893]) ).
tcf(c_17895,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(enc(pp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15893]) ).
tcf(c_17990,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),enc(i(X0),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_16981,c_17895]) ).
tcf(c_17991,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),enc(i(X0),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_4987,c_17895]) ).
tcf(c_18019,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X0)
| ~ p(enc(enc(i(wk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_16226]) ).
tcf(c_18021,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_16226]) ).
tcf(c_18087,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(enc(wk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_18019]) ).
tcf(c_18127,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_218,c_18087]) ).
tcf(c_18128,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_18087]) ).
tcf(c_18134,plain,
( p(enc(pp,w))
| ~ p(enc(wk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_18087]) ).
tcf(c_18135,plain,
( p(enc(pp,t1))
| ~ p(enc(wk,w)) ),
inference(superposition,[status(thm)],[c_66,c_18087]) ).
tcf(c_18138,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_18087]) ).
tcf(c_18141,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(X0)
| ~ p(enc(wk,k)) ),
inference(superposition,[status(thm)],[c_602,c_18087]) ).
tcf(c_18142,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(X0)
| ~ p(enc(wk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_18087]) ).
tcf(c_18143,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(X0)
| ~ p(enc(wk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_18087]) ).
tcf(c_18191,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_18087]) ).
tcf(c_18193,plain,
p(enc(pp,t1)),
inference(forward_subsumption_resolution,[status(thm)],[c_18135,c_65]) ).
tcf(c_18308,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),t1))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_18193,c_17895]) ).
tcf(c_18309,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),t1))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_18193,c_16120]) ).
tcf(c_18326,plain,
! [X0: $i] :
( p(enc(X0,t1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_18308]) ).
tcf(c_18374,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),t1))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_18326]) ).
tcf(c_18385,plain,
! [X0: $i] :
( p(enc(X0,t1))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_18309]) ).
tcf(c_18477,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),enc(i(X0),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_18021,c_17895]) ).
tcf(c_18529,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(wk,X0))
| ~ p(enc(tmk,enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_17573]) ).
tcf(c_18553,plain,
! [X0: $i,X1: $i] :
( p(X1)
| ~ p(enc(wk,i(X0)))
| ~ p(enc(tmk,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_51,c_18529]) ).
tcf(c_18646,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,t1))
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_18374]) ).
tcf(c_18648,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),t1))
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_18374]) ).
tcf(c_18708,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,t1))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_18646]) ).
tcf(c_18740,plain,
( p(enc(t2,t1))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_18708]) ).
tcf(c_18798,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),t1))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_18708]) ).
tcf(c_18930,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(enc(wk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_532]) ).
tcf(c_18976,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_218,c_18930]) ).
tcf(c_18977,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_18930]) ).
tcf(c_18983,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),w))
| ~ p(X0)
| ~ p(enc(wk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_18930]) ).
tcf(c_18987,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_18930]) ).
tcf(c_18990,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,k)) ),
inference(superposition,[status(thm)],[c_602,c_18930]) ).
tcf(c_18991,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_18930]) ).
tcf(c_18992,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_18930]) ).
tcf(c_19043,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(X0,X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_18930]) ).
tcf(c_19206,plain,
! [X0: $i] :
( p(enc(X0,w))
| ~ p(enc(wk,wk))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_18983]) ).
tcf(c_19274,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),w))
| ~ p(X0)
| ~ p(enc(wk,wk)) ),
inference(superposition,[status(thm)],[c_440,c_19206]) ).
tcf(c_19278,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),w))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,wk)) ),
inference(superposition,[status(thm)],[c_972,c_19206]) ).
tcf(c_19305,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(wk,X1))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_534]) ).
tcf(c_19481,plain,
! [X0: $i] :
( p(enc(X0,w))
| ~ p(enc(wk,wk))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_19274]) ).
tcf(c_19579,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X1),enc(i(X0),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_972,c_19305]) ).
tcf(c_19751,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_13468]) ).
tcf(c_19770,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(enc(tmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_19751]) ).
tcf(c_19805,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_16382]) ).
tcf(c_19824,plain,
! [X0: $i,X1: $i] :
( p(enc(w,X1))
| ~ p(X1)
| ~ p(enc(wk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_19805]) ).
tcf(c_19848,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_17074]) ).
tcf(c_19867,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(enc(tmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_19848]) ).
tcf(c_19892,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_18128]) ).
tcf(c_19911,plain,
! [X0: $i,X1: $i] :
( p(enc(pp,X1))
| ~ p(X1)
| ~ p(enc(wk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_19892]) ).
tcf(c_20069,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,enc(i(enc(i(enc(i(zcmk),X0)),X1)),X2))) ),
inference(superposition,[status(thm)],[c_50,c_1523]) ).
tcf(c_20070,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,X2))
| ~ p(X0)
| ~ p(enc(tmk,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_1523]) ).
tcf(c_20072,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X1),X2),X0))
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1523]) ).
tcf(c_20214,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_20070]) ).
tcf(c_20255,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_67,c_20214]) ).
tcf(c_20317,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X2),X1))
| ~ p(X2)
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_20214]) ).
tcf(c_20842,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_278,c_20255]) ).
tcf(c_20845,plain,
! [X0: $i] :
( p(enc(t2,enc(i(tmk),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_50,c_20255]) ).
tcf(c_20906,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(X0),X3),enc(i(enc(i(zcmk),X2)),X1)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_278,c_20072]) ).
tcf(c_20909,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X2),enc(i(tmk),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_50,c_20072]) ).
tcf(c_20949,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X0)),X2),enc(i(tmk),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_20909]) ).
tcf(c_20969,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X0)
| ~ p(enc(tmk,enc(i(X1),X2)))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_20069]) ).
tcf(c_20971,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,enc(i(enc(i(X0),X1)),X2))) ),
inference(superposition,[status(thm)],[c_49,c_20069]) ).
tcf(c_21003,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X1)
| ~ p(enc(zcmk,X2))
| ~ p(enc(X2,X0))
| ~ p(enc(tmk,enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_20969]) ).
tcf(c_21046,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X1)
| ~ p(enc(zcmk,X2))
| ~ p(enc(X2,i(X0)))
| ~ p(enc(tmk,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_51,c_21003]) ).
tcf(c_21091,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(tmk,enc(i(enc(X0,X1)),X2))) ),
inference(superposition,[status(thm)],[c_51,c_20971]) ).
tcf(c_21147,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(tmk),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_20949]) ).
tcf(c_21280,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(tmk),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_21147]) ).
tcf(c_21380,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X1),enc(i(tmk),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_21280]) ).
tcf(c_21564,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(i(enc(i(zcmk),X0)),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_14182]) ).
tcf(c_21579,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_21564]) ).
tcf(c_21581,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_21564]) ).
tcf(c_21751,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_21581]) ).
tcf(c_21781,plain,
! [X0: $i] :
( p(enc(enc(i(wk),X0),w))
| ~ p(X0)
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_21751]) ).
tcf(c_21848,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),enc(X0,X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_21751]) ).
tcf(c_21942,plain,
! [X0: $i] :
( p(enc(X0,w))
| ~ p(enc(zcmk,wk))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_21781]) ).
tcf(c_22023,plain,
! [X0: $i] :
( p(enc(enc(i(tmk),X0),w))
| ~ p(X0)
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_440,c_21942]) ).
tcf(c_22027,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),w))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_972,c_21942]) ).
tcf(c_22047,plain,
! [X0: $i] :
( p(enc(X0,w))
| ~ p(enc(zcmk,wk))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_22023]) ).
tcf(c_22122,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,w))
| ~ p(X0)
| ~ p(enc(tmk,wk))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_15321]) ).
tcf(c_22124,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),w))
| ~ p(X1)
| ~ p(enc(tmk,wk))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15321]) ).
tcf(c_22273,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,w))
| ~ p(enc(tmk,wk))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_22122]) ).
tcf(c_22315,plain,
( p(enc(t2,w))
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,wk)) ),
inference(superposition,[status(thm)],[c_67,c_22273]) ).
tcf(c_22383,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),w))
| ~ p(X1)
| ~ p(enc(tmk,wk))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_22273]) ).
tcf(c_23312,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(tmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_17990]) ).
tcf(c_23314,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_17990]) ).
tcf(c_23316,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X1),enc(X0,X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_17990]) ).
tcf(c_24005,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X1),enc(i(X0),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_278,c_23312]) ).
tcf(c_24036,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_23314]) ).
tcf(c_24046,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_23314]) ).
tcf(c_24051,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_23314]) ).
tcf(c_24052,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_23314]) ).
tcf(c_24435,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),enc(i(enc(i(zcmk),X0)),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_17991]) ).
tcf(c_24455,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_24435]) ).
tcf(c_24457,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_24435]) ).
tcf(c_24626,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_24457]) ).
tcf(c_27432,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),enc(X0,X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_24626]) ).
tcf(c_27583,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),enc(i(w),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_65,c_18477]) ).
tcf(c_27601,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(w),X1)))
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27583]) ).
tcf(c_27603,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(enc(w,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27583]) ).
tcf(c_27754,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X0),enc(i(w),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_278,c_27601]) ).
tcf(c_27756,plain,
! [X0: $i] :
( p(enc(pp,enc(i(w),X0)))
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_64,c_27601]) ).
tcf(c_27771,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(enc(w,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27756]) ).
tcf(c_27801,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(w),X0)))
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_27756,c_16120]) ).
tcf(c_27891,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(w),X1)))
| ~ p(X1)
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27801]) ).
tcf(c_27893,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(enc(w,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27801]) ).
tcf(c_28145,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,w))
| ~ p(X0)
| ~ p(enc(wk,wk))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_19278]) ).
tcf(c_28147,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),w))
| ~ p(X1)
| ~ p(enc(wk,wk))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_19278]) ).
tcf(c_28315,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,w))
| ~ p(enc(wk,wk))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_28145]) ).
tcf(c_28410,plain,
( p(enc(t2,w))
| ~ p(enc(wk,wk))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_28315]) ).
tcf(c_28484,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),w))
| ~ p(X1)
| ~ p(enc(wk,wk))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_28315]) ).
tcf(c_28933,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_20842]) ).
tcf(c_28935,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_20842]) ).
tcf(c_28996,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_28933]) ).
tcf(c_29036,plain,
( p(enc(t2,w))
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_28996]) ).
tcf(c_29113,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_28996]) ).
tcf(c_29816,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,w))
| ~ p(X0)
| ~ p(enc(zcmk,wk))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_22027]) ).
tcf(c_29818,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(X0),X1),w))
| ~ p(X1)
| ~ p(enc(zcmk,wk))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_22027]) ).
tcf(c_29998,plain,
! [X0: $i,X1: $i] :
( p(enc(X1,w))
| ~ p(enc(zcmk,wk))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_29816]) ).
tcf(c_30135,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(X0,X1),w))
| ~ p(X1)
| ~ p(enc(zcmk,wk))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_29998]) ).
tcf(c_30456,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(tc),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_1649]) ).
tcf(c_30458,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X1),enc(i(tc),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1649]) ).
tcf(c_30460,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_1649]) ).
tcf(c_30660,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(tc),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_30456]) ).
tcf(c_30716,plain,
! [X0: $i] :
( p(enc(t2,enc(i(tc),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_30660]) ).
tcf(c_30794,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X1),enc(i(tc),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_30660]) ).
tcf(c_31081,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(tc,X0)) ),
inference(superposition,[status(thm)],[c_49,c_30716]) ).
tcf(c_31159,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tc,enc(i(enc(i(enc(i(zcmk),X0)),X1)),X2))) ),
inference(superposition,[status(thm)],[c_50,c_30460]) ).
tcf(c_31160,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,X2))
| ~ p(X0)
| ~ p(enc(tc,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_30460]) ).
tcf(c_31162,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X2),X1))
| ~ p(X2)
| ~ p(enc(tc,X1))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_30460]) ).
tcf(c_31339,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,X2))
| ~ p(enc(tc,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_31160]) ).
tcf(c_31385,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,X2))
| ~ p(X0)
| ~ p(enc(tc,X2))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(enc(i(zcmk),X0)))) ),
inference(superposition,[status(thm)],[c_3641,c_31339]) ).
tcf(c_31456,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X2),X1))
| ~ p(X2)
| ~ p(enc(tc,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_31339]) ).
tcf(c_31851,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X0)
| ~ p(enc(tc,enc(i(X1),X2)))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_31159]) ).
tcf(c_31853,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tc,enc(i(enc(i(X0),X1)),X2))) ),
inference(superposition,[status(thm)],[c_49,c_31159]) ).
tcf(c_31889,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X1)
| ~ p(enc(zcmk,X2))
| ~ p(enc(X2,X0))
| ~ p(enc(tc,enc(i(X0),X1))) ),
inference(superposition,[status(thm)],[c_49,c_31851]) ).
tcf(c_31925,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X1)
| ~ p(enc(zcmk,X2))
| ~ p(enc(X2,i(X0)))
| ~ p(enc(tc,enc(X0,X1))) ),
inference(superposition,[status(thm)],[c_51,c_31889]) ).
tcf(c_31968,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(tc,enc(i(enc(X0,X1)),X2))) ),
inference(superposition,[status(thm)],[c_51,c_31853]) ).
tcf(c_32068,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(lp),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_3097]) ).
tcf(c_32070,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X1),enc(i(lp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_3097]) ).
tcf(c_32072,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(lp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_3097]) ).
tcf(c_32336,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(lp),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_32068]) ).
tcf(c_32537,plain,
! [X0: $i] :
( p(enc(t2,enc(i(lp),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_32336]) ).
tcf(c_32618,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X1),enc(i(lp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_32336]) ).
tcf(c_32735,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(lp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_32537]) ).
tcf(c_32849,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(zcmk),X0)),enc(i(enc(i(zcmk),X2)),X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_4755]) ).
tcf(c_32909,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(zcmk),X2)),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_32849]) ).
tcf(c_32911,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(zcmk),X1)),enc(i(X0),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_32849]) ).
tcf(c_33189,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(zcmk),X2)),X1))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_32909]) ).
tcf(c_33223,plain,
! [X0: $i] :
( p(enc(i(enc(i(zcmk),X0)),w))
| ~ p(X0)
| ~ p(enc(zcmk,wk)) ),
inference(superposition,[status(thm)],[c_65,c_33189]) ).
tcf(c_33225,plain,
! [X0: $i] :
( p(enc(i(enc(i(zcmk),X0)),t2))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_33189]) ).
tcf(c_33308,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(enc(i(zcmk),X2)),enc(X0,X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_33189]) ).
tcf(c_33456,plain,
! [X0: $i] :
( p(enc(i(X0),w))
| ~ p(enc(zcmk,wk))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_33223]) ).
tcf(c_33651,plain,
! [X0: $i] :
( p(enc(i(X0),t2))
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_33225]) ).
tcf(c_34137,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(i(X0),enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_32911]) ).
tcf(c_34611,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(enc(i(tmk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_12961]) ).
tcf(c_34613,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(tmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_12961]) ).
tcf(c_34905,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(pp),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_15897]) ).
tcf(c_34907,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X1),enc(i(pp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15897]) ).
tcf(c_34909,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(pp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_15897]) ).
tcf(c_35063,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(pp),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_34905]) ).
tcf(c_35193,plain,
! [X0: $i] :
( p(enc(t2,enc(i(pp),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_35063]) ).
tcf(c_35281,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X1),enc(i(pp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_35063]) ).
tcf(c_35428,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(pp,X0)) ),
inference(superposition,[status(thm)],[c_49,c_35193]) ).
tcf(c_35629,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X0,enc(i(enc(i(wk),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_16223]) ).
tcf(c_35631,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(wk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_16223]) ).
tcf(c_35841,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(enc(wk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_35631]) ).
tcf(c_35888,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_218,c_35841]) ).
tcf(c_35889,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_35841]) ).
tcf(c_35899,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_35841]) ).
tcf(c_35903,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,k)) ),
inference(superposition,[status(thm)],[c_602,c_35841]) ).
tcf(c_35904,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_35841]) ).
tcf(c_35905,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_35841]) ).
tcf(c_35987,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),enc(X0,X1)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_35841]) ).
tcf(c_36700,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(w),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_27754]) ).
tcf(c_36702,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X1),enc(i(w),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27754]) ).
tcf(c_36704,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(w,X0)) ),
inference(superposition,[status(thm)],[c_49,c_27754]) ).
tcf(c_36866,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(w),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_36700]) ).
tcf(c_36902,plain,
! [X0: $i] :
( p(enc(t2,enc(i(w),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_36866]) ).
tcf(c_36993,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X1),enc(i(w),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_36866]) ).
tcf(c_37204,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(w,X0)) ),
inference(superposition,[status(thm)],[c_49,c_36902]) ).
tcf(c_37502,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_14050]) ).
tcf(c_37525,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_37502]) ).
tcf(c_37555,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_18977]) ).
tcf(c_37578,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(wk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_37555]) ).
tcf(c_37640,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_24036]) ).
tcf(c_37663,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_37640]) ).
tcf(c_37745,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_35889]) ).
tcf(c_37768,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(tmk),X2),X1))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_37745]) ).
tcf(c_38158,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,X2))
| ~ p(enc(tc,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_31385]) ).
tcf(c_38299,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,enc(i(enc(i(enc(i(zcmk),X1)),X0)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_65,c_15873]) ).
tcf(c_38300,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,enc(i(enc(i(enc(i(zcmk),X1)),X0)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_517,c_15873]) ).
tcf(c_38302,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X0),enc(i(enc(i(enc(i(zcmk),X2)),X1)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_15873]) ).
tcf(c_38335,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,X2))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_38299]) ).
tcf(c_38337,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_38299]) ).
tcf(c_38339,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,enc(i(enc(i(X0),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_38299]) ).
tcf(c_38441,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,X2))
| ~ p(X0)
| ~ p(enc(X1,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_38335]) ).
tcf(c_38443,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,X2))
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(enc(i(X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_38335]) ).
tcf(c_38515,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_38441]) ).
tcf(c_38556,plain,
! [X0: $i] :
( p(enc(w,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(t2,X0)) ),
inference(superposition,[status(thm)],[c_67,c_38515]) ).
tcf(c_38649,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,X2))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(enc(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_38515]) ).
tcf(c_39303,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,enc(i(enc(X0,X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_50,c_38649]) ).
tcf(c_39509,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(w,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_38337]) ).
tcf(c_39541,plain,
! [X0: $i] :
( p(enc(w,enc(i(t2),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_67,c_39509]) ).
tcf(c_39741,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(t2),X0)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_39541,c_36704]) ).
tcf(c_39742,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),enc(i(t2),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_39541,c_27893]) ).
tcf(c_39743,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),enc(i(t2),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_39541,c_27603]) ).
tcf(c_39744,plain,
! [X0: $i] :
( p(enc(pp,enc(i(t2),X0)))
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_39541,c_27771]) ).
tcf(c_39775,plain,
! [X0: $i] :
( p(enc(pp,X0))
| ~ p(enc(zcmk,lp))
| ~ p(enc(t2,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39744]) ).
tcf(c_39896,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X3)),X4),enc(i(enc(i(X0),X1)),X2)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_38339,c_36704]) ).
tcf(c_39898,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),enc(i(enc(i(X0),X1)),X2)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_38339,c_27603]) ).
tcf(c_39899,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,enc(i(enc(i(X0),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_38339,c_27771]) ).
tcf(c_40013,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),enc(i(enc(X0,X1)),X2)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_39303,c_27603]) ).
tcf(c_40014,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,enc(i(enc(X0,X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_39303,c_27771]) ).
tcf(c_40121,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(t2),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39742]) ).
tcf(c_40123,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(wk),X1),X0))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(t2,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39742]) ).
tcf(c_40690,plain,
! [X0: $i,X1: $i] :
( p(enc(X0,enc(i(t2),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39743]) ).
tcf(c_40692,plain,
! [X0: $i,X1: $i] :
( p(enc(enc(i(tmk),X1),X0))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(t2,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39743]) ).
tcf(c_41112,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,X2))
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(enc(i(X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_39899]) ).
tcf(c_41114,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_39899]) ).
tcf(c_41245,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_41112]) ).
tcf(c_41247,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,X2))
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(enc(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_51,c_41112]) ).
tcf(c_42941,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,X2))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_38300]) ).
tcf(c_42943,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_38300]) ).
tcf(c_43036,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(pp,X2))
| ~ p(X0)
| ~ p(enc(X1,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_42941]) ).
tcf(c_43332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_38302]) ).
tcf(c_43334,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_38302]) ).
tcf(c_43336,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X1),enc(i(enc(i(X0),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_38302]) ).
tcf(c_43558,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(X1,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_43332]) ).
tcf(c_43560,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(enc(i(X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_43332]) ).
tcf(c_43709,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_43558]) ).
tcf(c_43861,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(enc(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_43709]) ).
tcf(c_45451,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_43334]) ).
tcf(c_45599,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(wk),X2),enc(i(enc(X0,X1)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_45451]) ).
tcf(c_46185,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(wk,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_19579]) ).
tcf(c_46187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(X0),X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(wk,X1))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_19579]) ).
tcf(c_46189,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(wk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_19579]) ).
tcf(c_46191,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(X0,X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_19579]) ).
tcf(c_46625,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(enc(wk,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_46185]) ).
tcf(c_46720,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,X0)) ),
inference(superposition,[status(thm)],[c_67,c_46625]) ).
tcf(c_46729,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(wk,X2))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(enc(i(zcmk),X0)))) ),
inference(superposition,[status(thm)],[c_3641,c_46625]) ).
tcf(c_46824,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(X0,X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(wk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_46625]) ).
tcf(c_47611,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_46720]) ).
tcf(c_47613,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_46720]) ).
tcf(c_47739,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,tmk))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_278,c_47611]) ).
tcf(c_47744,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_218,c_47611]) ).
tcf(c_47745,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_47611]) ).
tcf(c_47755,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_47611]) ).
tcf(c_47759,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(X0)
| ~ p(enc(wk,k))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_602,c_47611]) ).
tcf(c_47760,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_47611]) ).
tcf(c_47761,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(X0)
| ~ p(enc(wk,kk))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_925,c_47611]) ).
tcf(c_47796,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,pp))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_12964,c_47611]) ).
tcf(c_47799,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(wk,w))
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_12994,c_47611]) ).
tcf(c_47827,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(enc(i(wk),X0)),X1)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,pp))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_16226,c_47611]) ).
tcf(c_47848,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(enc(i(enc(i(zcmk),X1)),X0)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,pp))
| ~ p(enc(zcmk,lp)) ),
inference(superposition,[status(thm)],[c_38300,c_47611]) ).
tcf(c_47856,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(enc(i(X0),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,pp))
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_39899,c_47611]) ).
tcf(c_47857,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(enc(X0,X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,pp))
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_40014,c_47611]) ).
tcf(c_48029,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(X0),X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47799,c_65]) ).
tcf(c_48079,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(enc(i(wk),X0)),X1)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47827,c_517]) ).
tcf(c_48116,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47796,c_517]) ).
tcf(c_48173,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(enc(X0,X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,i(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47857,c_517]) ).
tcf(c_48179,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(enc(i(X0),X1)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47856,c_517]) ).
tcf(c_48235,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(enc(i(enc(i(zcmk),X1)),X0)),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_47848,c_517]) ).
tcf(c_48631,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,enc(i(tc),X0))) ),
inference(superposition,[status(thm)],[c_218,c_46189]) ).
tcf(c_48632,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_46189]) ).
tcf(c_48642,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_46189]) ).
tcf(c_48646,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,k)) ),
inference(superposition,[status(thm)],[c_602,c_46189]) ).
tcf(c_48647,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_46189]) ).
tcf(c_48648,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(wk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_46189]) ).
tcf(c_50146,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_48029]) ).
tcf(c_50148,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,enc(X0,X1)))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_48029]) ).
tcf(c_50313,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_50146]) ).
tcf(c_50323,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_50146]) ).
tcf(c_50328,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_50146]) ).
tcf(c_50329,plain,
! [X0: $i] :
( p(enc(t2,X0))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_50146]) ).
tcf(c_52014,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(enc(i(wk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_48079]) ).
tcf(c_52378,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(enc(i(tmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_48116]) ).
tcf(c_52917,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tc,X0))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_47745]) ).
tcf(c_52940,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(wk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_52917]) ).
tcf(c_52992,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_50313]) ).
tcf(c_53015,plain,
! [X0: $i,X1: $i] :
( p(enc(t2,X1))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(tmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_52992]) ).
tcf(c_53143,plain,
! [X0: $i] :
( ~ p(X0)
| ~ p(enc(wk,tmk)) ),
inference(global_subsumption_just,[status(thm)],[c_47739,c_14325,c_14569]) ).
tcf(c_53203,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,X2))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(enc(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_48173]) ).
tcf(c_53205,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,lp))
| ~ p(enc(X0,X1))
| ~ p(enc(zcmk,i(i(X0)))) ),
inference(superposition,[status(thm)],[c_49,c_48173]) ).
tcf(c_53272,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(light_normalisation,[status(thm)],[c_53205,c_51]) ).
tcf(c_53723,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,X2))
| ~ p(enc(zcmk,lp))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1))
| ~ p(enc(zcmk,i(i(X0)))) ),
inference(superposition,[status(thm)],[c_49,c_53203]) ).
tcf(c_53770,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,X2))
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1)) ),
inference(light_normalisation,[status(thm)],[c_53723,c_51]) ).
tcf(c_54029,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,X2))
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0))
| ~ p(enc(enc(i(X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_50,c_53770]) ).
tcf(c_56055,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X0)),X3),enc(i(enc(i(zcmk),X2)),X1)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_20906]) ).
tcf(c_56073,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(enc(i(zcmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_56055]) ).
tcf(c_56077,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_56055]) ).
tcf(c_56079,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(X0),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_56055]) ).
tcf(c_56441,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(enc(i(zcmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_56073]) ).
tcf(c_56595,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(X0,X1),enc(i(enc(i(zcmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_56441]) ).
tcf(c_56832,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_56077]) ).
tcf(c_56984,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),enc(X0,X1)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_56832]) ).
tcf(c_57134,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(zcmk,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_56079]) ).
tcf(c_57136,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(X0),X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_56079]) ).
tcf(c_57746,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(enc(zcmk,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_57134]) ).
tcf(c_57799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(zcmk,X2))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(enc(i(zcmk),X0)))) ),
inference(superposition,[status(thm)],[c_3641,c_57746]) ).
tcf(c_57902,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(X0,X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_57746]) ).
tcf(c_58946,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(tmk,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_24005]) ).
tcf(c_58948,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(X1),X2),enc(i(X0),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_24005]) ).
tcf(c_58950,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_24005]) ).
tcf(c_58952,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(X0,X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_24005]) ).
tcf(c_59709,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_58946]) ).
tcf(c_59871,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(X0,X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_59709]) ).
tcf(c_60583,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(X0),X3),enc(i(enc(i(enc(i(zcmk),X2)),X1)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_278,c_58948]) ).
tcf(c_60586,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(X0),X2),enc(i(enc(i(tmk),X1)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_50,c_58948]) ).
tcf(c_60616,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(enc(i(tc),X0)))) ),
inference(superposition,[status(thm)],[c_243,c_58950]) ).
tcf(c_60626,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_862,c_58950]) ).
tcf(c_60631,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,i(k))) ),
inference(superposition,[status(thm)],[c_748,c_58950]) ).
tcf(c_60632,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(tmk,kk)) ),
inference(superposition,[status(thm)],[c_925,c_58950]) ).
tcf(c_61876,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X0)),X2),enc(i(enc(i(tmk),X1)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_60586]) ).
tcf(c_61918,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(enc(i(tmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_61876]) ).
tcf(c_61922,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(tmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_61876]) ).
tcf(c_62259,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(enc(i(tmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_61918]) ).
tcf(c_62416,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(X0,X1),enc(i(enc(i(tmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_62259]) ).
tcf(c_62997,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(t2),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_39741]) ).
tcf(c_62999,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(X0),X1),enc(i(t2),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39741]) ).
tcf(c_63001,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(t2,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39741]) ).
tcf(c_63564,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(X1,enc(i(t2),X2)))
| ~ p(X2)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_62997]) ).
tcf(c_63798,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(enc(X0,X1),enc(i(t2),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,lp))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_63564]) ).
tcf(c_64619,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),enc(i(enc(i(enc(i(zcmk),X0)),X1)),X2)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_39898]) ).
tcf(c_64653,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X0,enc(i(enc(i(enc(i(zcmk),X1)),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_64619]) ).
tcf(c_64655,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_64619]) ).
tcf(c_64657,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_64619]) ).
tcf(c_65289,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(X1,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_64655]) ).
tcf(c_65291,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(enc(i(X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_64655]) ).
tcf(c_65508,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_65289]) ).
tcf(c_65666,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(enc(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_65508]) ).
tcf(c_67588,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(tmk),X2),enc(i(X1),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_64657]) ).
tcf(c_68480,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,X2))
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_48235]) ).
tcf(c_68482,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,enc(i(X1),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_48235]) ).
tcf(c_68616,plain,
! [X0: $i,X1: $i,X2: $i] :
( p(enc(t2,X2))
| ~ p(X0)
| ~ p(enc(zcmk,lp))
| ~ p(enc(X1,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_68480]) ).
tcf(c_68938,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(enc(i(wk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_16227]) ).
tcf(c_68940,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(X0),X1),enc(i(enc(i(wk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_16227]) ).
tcf(c_68942,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(wk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_16227]) ).
tcf(c_69235,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(enc(i(wk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_68938]) ).
tcf(c_69396,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(X0,X1),enc(i(enc(i(wk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_69235]) ).
tcf(c_70135,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(wk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_48632]) ).
tcf(c_70162,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(wk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_70135]) ).
tcf(c_70327,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tc,X0))
| ~ p(enc(tmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_60616]) ).
tcf(c_70354,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(tmk,X0))
| ~ p(enc(tc,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_70327]) ).
tcf(c_70833,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(enc(wk,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_46729]) ).
tcf(c_71052,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p(enc(X1,enc(i(X2),X3)))
| ~ p(X3)
| ~ p(enc(zcmk,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_57799]) ).
tcf(c_71396,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(i(X2),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(zcmk,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_39896]) ).
tcf(c_71398,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(X0),X2),enc(i(enc(i(X1),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,X0)) ),
inference(superposition,[status(thm)],[c_49,c_39896]) ).
tcf(c_71400,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X4)
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(zcmk,X0))
| ~ p(enc(enc(i(X0),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_39896]) ).
tcf(c_71402,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),enc(i(X1),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_39896]) ).
tcf(c_71404,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(enc(X0,X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_51,c_39896]) ).
tcf(c_72100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(i(X2),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(enc(zcmk,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_71396]) ).
tcf(c_72166,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(i(X2),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(zcmk,X2))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(enc(i(zcmk),X0)))) ),
inference(superposition,[status(thm)],[c_3641,c_72100]) ).
tcf(c_72276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(X0,X2),enc(i(enc(i(X1),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_72100]) ).
tcf(c_72950,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X4)
| ~ p(X3)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X1,X2))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_71400]) ).
tcf(c_72952,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X4)
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0)))
| ~ p(enc(enc(X0,X1),X2)) ),
inference(superposition,[status(thm)],[c_51,c_71400]) ).
tcf(c_75884,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(X2,X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(zcmk,i(X2)))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_71404]) ).
tcf(c_75886,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(X1),X2),enc(i(enc(X0,X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_71404]) ).
tcf(c_76752,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X2,enc(i(enc(X0,X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(enc(zcmk,X1))
| ~ p(enc(X1,X2))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_75884]) ).
tcf(c_77040,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X0)),X3),enc(i(enc(i(enc(i(zcmk),X2)),X1)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ),
inference(superposition,[status(thm)],[c_50,c_60583]) ).
tcf(c_77064,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(i(enc(i(zcmk),X2)),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_77040]) ).
tcf(c_77068,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X4)
| ~ p(X3)
| ~ p(X1)
| ~ p(X0)
| ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2)) ),
inference(superposition,[status(thm)],[c_49,c_77040]) ).
tcf(c_77070,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X2)),X3),enc(i(X1),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X0)
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_77040]) ).
tcf(c_77526,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(i(enc(i(zcmk),X2)),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1)) ),
inference(superposition,[status(thm)],[c_49,c_77064]) ).
tcf(c_77693,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(X0,X1),enc(i(enc(i(enc(i(zcmk),X2)),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_77526]) ).
tcf(c_77991,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X4)
| ~ p(X3)
| ~ p(X0)
| ~ p(enc(X1,X2))
| ~ p(enc(enc(i(zcmk),X0),X1)) ),
inference(superposition,[status(thm)],[c_49,c_77068]) ).
tcf(c_79257,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p(enc(X1,enc(i(enc(i(X2),X3)),X4)))
| ~ p(X4)
| ~ p(X3)
| ~ p(enc(zcmk,X2))
| ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,X1))
| ~ p(enc(zcmk,i(X0))) ),
inference(superposition,[status(thm)],[c_49,c_72166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV238+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.08/0.33 % Computer : n017.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Thu Sep 24 18:44:46 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.08/0.33 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.08/0.37 Running model finding
% 0.08/0.37 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fnt_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38
% 0.11/0.38 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.38
% 0.11/0.38 % Detected problem language: tptp
% 0.11/0.39 % Proving...
% 7.59/7.66 % SZS status Started for theBenchmark.p
% 7.59/7.66 % SZS status CounterSatisfiable for theBenchmark.p
% 7.59/7.66
% 7.59/7.66 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 7.59/7.66
% 7.59/7.66 ------ iProver source info
% 7.59/7.66
% 7.59/7.66 git: date: 2026-07-19 20:42:38 +0200
% 7.59/7.66 git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 7.59/7.66 git: non_committed_changes: false
% 7.59/7.66
% 7.59/7.66 ------ Parsing...
% 7.59/7.66 ------ Clausification by vclausify_rel & Parsing by iProver...
% 7.59/7.66 ------ Proving...
% 7.59/7.66 ------ Problem Properties
% 7.59/7.66
% 7.59/7.66
% 7.59/7.66 clauses 24
% 7.59/7.66 conjectures 1
% 7.59/7.66 EPR 2
% 7.59/7.66 Horn 24
% 7.59/7.66 unary 12
% 7.59/7.66 binary 1
% 7.59/7.66 lits 58
% 7.59/7.66 lits eq 3
% 7.59/7.66 fd_pure 0
% 7.59/7.66 fd_pseudo 0
% 7.59/7.66 fd_cond 0
% 7.59/7.66 fd_pseudo_cond 0
% 7.59/7.66 AC symbols 0
% 7.59/7.66
% 7.59/7.66 ------ Schedule Sat is on
% 7.59/7.66
% 7.59/7.66 ------ Input Options sat_mode off Time Limit: 30.
% 7.59/7.66
% 7.59/7.66
% 7.59/7.66 ------
% 7.59/7.66 Current options:
% 7.59/7.66 ------
% 7.59/7.66
% 7.59/7.66 ------ Input Options
% 7.59/7.66
% 7.59/7.66 --out_options all
% 7.59/7.66 --tptp_safe_out true
% 7.59/7.66 --problem_path ""
% 7.59/7.66 --include_path ""
% 7.59/7.66 --clausifier res/vclausify_rel
% 7.59/7.66 --clausifier_options --mode clausify -t 101.66 -updr off
% 7.59/7.66 --stdin false
% 7.59/7.66 --proof_out true
% 7.59/7.66 --proof_dot_file ""
% 7.59/7.66 --proof_reduce_dot []
% 7.59/7.66 --suppress_sat_res false
% 7.59/7.66 --suppress_unsat_res true
% 7.59/7.66 --stats_out none
% 7.59/7.66 --stats_mem false
% 7.59/7.66 --theory_stats_out false
% 7.59/7.66
% 7.59/7.66 ------ General Options
% 7.59/7.66
% 7.59/7.66 --fof false
% 7.59/7.66 --time_out_real 304.99
% 7.59/7.66 --time_out_virtual -1.
% 7.59/7.66 --rnd_seed 13
% 7.59/7.66 --symbol_type_check false
% 7.59/7.66 --clausify_out false
% 7.59/7.66 --sig_cnt_out false
% 7.59/7.66 --trig_cnt_out false
% 7.59/7.66 --trig_cnt_out_tolerance 1.
% 7.59/7.66 --trig_cnt_out_sk_spl false
% 7.59/7.66 --abstr_cl_out false
% 7.59/7.66
% 7.59/7.66 ------ Interactive Mode
% 7.59/7.66
% 7.59/7.66 --interactive_mode false
% 7.59/7.66 --external_ip_address ""
% 7.59/7.66 --external_port 0
% 7.59/7.66
% 7.59/7.66 ------ Global Options
% 7.59/7.66
% 7.59/7.66 --schedule sat
% 7.59/7.66 --add_important_lit false
% 7.59/7.66 --prop_solver_per_cl 500
% 7.59/7.66 --subs_bck_mult 8
% 7.59/7.66 --min_unsat_core false
% 7.59/7.66 --soft_assumptions false
% 7.59/7.66 --soft_lemma_size 3
% 7.59/7.66 --prop_impl_unit_size 0
% 7.59/7.66 --prop_impl_unit []
% 7.59/7.66 --share_sel_clauses true
% 7.59/7.66 --reset_solvers false
% 7.59/7.66 --bc_imp_inh [conj_cone]
% 7.59/7.66 --conj_cone_tolerance 3.
% 7.59/7.66 --extra_neg_conj none
% 7.59/7.66 --large_theory_mode true
% 7.59/7.66 --prolific_symb_bound 200
% 7.59/7.66 --lt_threshold 2000
% 7.59/7.66 --clause_weak_htbl true
% 7.59/7.66 --gc_record_bc_elim false
% 7.59/7.66
% 7.59/7.66 ------ Preprocessing Options
% 7.59/7.66
% 7.59/7.66 --preprocessing_flag false
% 7.59/7.66 --time_out_prep_mult 0.1
% 7.59/7.66 --splitting_mode input
% 7.59/7.66 --splitting_grd true
% 7.59/7.66 --splitting_cvd false
% 7.59/7.66 --splitting_cvd_svl false
% 7.59/7.66 --splitting_nvd 32
% 7.59/7.66 --sub_typing false
% 7.59/7.66 --prep_eq_flat_conj false
% 7.59/7.66 --prep_ineq_split false
% 7.59/7.66 --prep_eq_flat_all_gr false
% 7.59/7.66 --prep_gs_sim true
% 7.59/7.66 --prep_unflatten true
% 7.59/7.66 --prep_res_sim true
% 7.59/7.66 --prep_sup_sim_all true
% 7.59/7.66 --prep_sup_sim_sup false
% 7.59/7.66 --prep_upred true
% 7.59/7.66 --prep_well_definedness true
% 7.59/7.66 --prep_sem_filter exhaustive
% 7.59/7.66 --prep_sem_filter_out false
% 7.59/7.66 --pred_elim true
% 7.59/7.66 --res_sim_input true
% 7.59/7.66 --eq_ax_congr_red true
% 7.59/7.66 --pure_diseq_elim true
% 7.59/7.66 --brand_transform false
% 7.59/7.66 --non_eq_to_eq false
% 7.59/7.66 --prep_eq_proxy false
% 7.59/7.66 --prep_def_merge true
% 7.59/7.66 --prep_def_merge_prop_impl false
% 7.59/7.66 --prep_def_merge_mbd true
% 7.59/7.66 --prep_def_merge_tr_red false
% 7.59/7.66 --prep_def_merge_tr_cl false
% 7.59/7.66 --smt_preprocessing false
% 7.59/7.66 --smt_ac_axioms fast
% 7.59/7.66 --preprocessed_out false
% 7.59/7.66 --preprocessed_stats false
% 7.59/7.66
% 7.59/7.66 ------ Abstraction refinement Options
% 7.59/7.66
% 7.59/7.66 --abstr_ref []
% 7.59/7.66 --abstr_ref_prep false
% 7.59/7.66 --abstr_ref_until_sat false
% 7.59/7.66 --abstr_ref_sig_restrict funpre
% 7.59/7.66 --abstr_ref_af_restrict_to_split_sk false
% 7.59/7.66 --abstr_ref_under []
% 7.59/7.66
% 7.59/7.66 ------ SAT Options
% 7.59/7.66
% 7.59/7.66 --sat_mode false
% 7.59/7.66 --sat_fm_restart_options ""
% 7.59/7.66 --sat_gr_def false
% 7.59/7.66 --sat_epr_types true
% 7.59/7.66 --sat_non_cyclic_types false
% 7.59/7.66 --sat_finite_models false
% 7.59/7.66 --sat_fm_lemmas false
% 7.59/7.66 --sat_fm_prep false
% 7.59/7.66 --sat_fm_uc_incr true
% 7.59/7.66 --sat_out_model small
% 7.59/7.66 --sat_out_clauses false
% 7.59/7.66
% 7.59/7.66 ------ QBF Options
% 7.59/7.66
% 7.59/7.66 --qbf_mode false
% 7.59/7.66 --qbf_elim_univ false
% 7.59/7.66 --qbf_dom_inst none
% 7.59/7.66 --qbf_dom_pre_inst false
% 7.59/7.66 --qbf_sk_in false
% 7.59/7.66 --qbf_pred_elim true
% 7.59/7.66 --qbf_split 512
% 7.59/7.66
% 7.59/7.66 ------ BMC1 Options
% 7.59/7.66
% 7.59/7.66 --bmc1_incremental false
% 7.59/7.66 --bmc1_axioms reachable_all
% 7.59/7.66 --bmc1_min_bound 0
% 7.59/7.66 --bmc1_max_bound -1
% 7.59/7.66 --bmc1_max_bound_default -1
% 7.59/7.66 --bmc1_symbol_reachability true
% 7.59/7.66 --bmc1_property_lemmas false
% 7.59/7.66 --bmc1_k_induction false
% 7.59/7.66 --bmc1_non_equiv_states false
% 7.59/7.66 --bmc1_deadlock false
% 7.59/7.66 --bmc1_ucm false
% 7.59/7.66 --bmc1_add_unsat_core none
% 7.59/7.66 --bmc1_unsat_core_children false
% 7.59/7.66 --bmc1_unsat_core_extrapolate_axioms false
% 7.59/7.66 --bmc1_out_stat full
% 7.59/7.66 --bmc1_ground_init false
% 7.59/7.66 --bmc1_pre_inst_next_state false
% 7.59/7.66 --bmc1_pre_inst_state false
% 7.59/7.66 --bmc1_pre_inst_reach_state false
% 7.59/7.66 --bmc1_out_unsat_core false
% 7.59/7.66 --bmc1_aig_witness_out false
% 7.59/7.66 --bmc1_verbose false
% 7.59/7.66 --bmc1_dump_clauses_tptp false
% 7.59/7.66 --bmc1_dump_unsat_core_tptp false
% 7.59/7.66 --bmc1_dump_file -
% 7.59/7.66 --bmc1_ucm_expand_uc_limit 128
% 7.59/7.66 --bmc1_ucm_n_expand_iterations 6
% 7.59/7.66 --bmc1_ucm_extend_mode 1
% 7.59/7.66 --bmc1_ucm_init_mode 2
% 7.59/7.66 --bmc1_ucm_cone_mode none
% 7.59/7.66 --bmc1_ucm_reduced_relation_type 0
% 7.59/7.66 --bmc1_ucm_relax_model 4
% 7.59/7.66 --bmc1_ucm_full_tr_after_sat true
% 7.59/7.66 --bmc1_ucm_expand_neg_assumptions false
% 7.59/7.66 --bmc1_ucm_layered_model none
% 7.59/7.66 --bmc1_ucm_max_lemma_size 10
% 7.59/7.66
% 7.59/7.66 ------ AIG Options
% 7.59/7.66
% 7.59/7.66 --aig_mode false
% 7.59/7.66
% 7.59/7.66 ------ Instantiation Options
% 7.59/7.66
% 7.59/7.66 --instantiation_flag true
% 7.59/7.66 --inst_sos_flag false
% 7.59/7.66 --inst_sos_phase true
% 7.59/7.66 --inst_sos_sth_lit_sel [+prop;+non_prol_conj_symb;-eq;+ground;-num_var;-num_symb]
% 7.59/7.66 --inst_lit_sel [-sign;+ground;-num_var;-num_symb]
% 7.59/7.66 --inst_lit_sel_side num_symb
% 7.59/7.66 --inst_solver_per_active 1400
% 7.59/7.66 --inst_solver_calls_frac 1.
% 7.59/7.66 --inst_to_smt_solver true
% 7.59/7.66 --inst_passive_queue_type priority_queues
% 7.59/7.66 --inst_passive_queues [[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]
% 7.59/7.66 --inst_passive_queues_freq [25;2]
% 7.59/7.66 --inst_dismatching true
% 7.59/7.66 --inst_eager_unprocessed_to_passive true
% 7.59/7.66 --inst_unprocessed_bound 1000
% 7.59/7.66 --inst_prop_sim_given true
% 7.59/7.66 --inst_prop_sim_new false
% 7.59/7.66 --inst_subs_new false
% 7.59/7.66 --inst_eq_res_simp false
% 7.59/7.66 --inst_subs_given false
% 7.59/7.66 --inst_orphan_elimination true
% 7.59/7.66 --inst_learning_loop_flag true
% 7.59/7.66 --inst_learning_start 3000
% 7.59/7.66 --inst_learning_factor 2
% 7.59/7.66 --inst_start_prop_sim_after_learn 3
% 7.59/7.66 --inst_sel_renew solver
% 7.59/7.66 --inst_lit_activity_flag true
% 7.59/7.66 --inst_restr_to_given false
% 7.59/7.66 --inst_activity_threshold 500
% 7.59/7.66
% 7.59/7.66 ------ Resolution Options
% 7.59/7.66
% 7.59/7.66 --resolution_flag true
% 7.59/7.66 --res_lit_sel neg_min
% 7.59/7.66 --res_lit_sel_side none
% 7.59/7.66 --res_ordering kbo
% 7.59/7.66 --res_to_prop_solver active
% 7.59/7.66 --res_prop_simpl_new false
% 7.59/7.66 --res_prop_simpl_given true
% 7.59/7.66 --res_to_smt_solver true
% 7.59/7.66 --res_passive_queue_type priority_queues
% 7.59/7.66 --res_passive_queues [[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]
% 7.59/7.66 --res_passive_queues_freq [15;5]
% 7.59/7.66 --res_forward_subs full
% 7.59/7.66 --res_backward_subs full
% 7.59/7.66 --res_forward_subs_resolution true
% 7.59/7.66 --res_backward_subs_resolution true
% 7.59/7.66 --res_orphan_elimination true
% 7.59/7.66 --res_time_limit 300.
% 7.59/7.66
% 7.59/7.66 ------ Superposition Options
% 7.59/7.66
% 7.59/7.66 --superposition_flag true
% 7.59/7.66 --sup_passive_queue_type priority_queues
% 7.59/7.66 --sup_passive_queues [[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]
% 7.59/7.66 --sup_passive_queues_freq [1;1;1]
% 7.59/7.66 --twee_lhs_weight 4
% 7.59/7.66 --sup_set_join false
% 7.59/7.66 --sup_set_join_goals true
% 7.59/7.66 --sup_set_join_limit 1000
% 7.59/7.66 --demod_completeness_check fast
% 7.59/7.66 --demod_use_ground true
% 7.59/7.66 --sup_unprocessed_bound 0
% 7.59/7.66 --sup_to_prop_solver passive
% 7.59/7.66 --sup_prop_simpl_new true
% 7.59/7.66 --sup_prop_simpl_given true
% 7.59/7.66 --sup_fun_splitting false
% 7.59/7.66 --sup_iter_deepening 2
% 7.59/7.66 --sup_restarts_mult 12
% 7.59/7.66 --sup_score sim_d_gen
% 7.59/7.66 --sup_share_score_frac 0.2
% 7.59/7.66 --sup_share_max_num_cl 500
% 7.59/7.66 --sup_ordering lpo
% 7.59/7.66 --sup_symb_ordering invfreq
% 7.59/7.66 --sup_term_weight default
% 7.59/7.66
% 7.59/7.66 ------ Superposition Simplification Setup
% 7.59/7.66
% 7.59/7.66 --sup_indices_passive [LightNormIndex;FwDemodIndex]
% 7.59/7.66 --sup_full_triv [SMTSimplify;PropSubs]
% 7.59/7.66 --sup_full_fw [ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 7.59/7.66 --sup_full_bw [BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 7.59/7.66 --sup_immed_triv []
% 7.59/7.66 --sup_immed_fw_main [ACNormalisation;FwLightNorm;FwUnitSubsAndRes]
% 7.59/7.66 --sup_immed_fw_immed [ACNormalisation;FwUnitSubsAndRes]
% 7.59/7.66 --sup_immed_bw_main [BwUnitSubsAndRes;BwDemod]
% 7.59/7.66 --sup_immed_bw_immed [BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 7.59/7.66 --sup_input_triv [Unflattening;SMTSimplify]
% 7.59/7.66 --sup_input_fw [FwACDemod;ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 7.59/7.66 --sup_input_bw [BwACDemod;BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 7.59/7.66 --sup_full_fixpoint true
% 7.59/7.66 --sup_main_fixpoint true
% 7.59/7.66 --sup_immed_fixpoint false
% 7.59/7.66 --sup_input_fixpoint true
% 7.59/7.66 --sup_cache_sim none
% 7.59/7.66 --sup_smt_interval 500
% 7.59/7.66 --sup_bw_gjoin_interval 0
% 7.59/7.66
% 7.59/7.66 ------ Combination Options
% 7.59/7.66
% 7.59/7.66 --comb_mode clause_based
% 7.59/7.66 --comb_inst_mult 5
% 7.59/7.66 --comb_res_mult 1
% 7.59/7.66 --comb_sup_mult 8
% 7.59/7.66 --comb_sup_deep_mult 2
% 7.59/7.66
% 7.59/7.66 ------ Debug Options
% 7.59/7.66
% 7.59/7.66 --dbg_backtrace false
% 7.59/7.66 --dbg_dump_prop_clauses false
% 7.59/7.66 --dbg_dump_prop_clauses_file -
% 7.59/7.66 --dbg_out_stat false
% 7.59/7.66 --dbg_just_parse false
% 7.59/7.66
% 7.59/7.66
% 7.59/7.66
% 7.59/7.66
% 7.59/7.66 ------ Proving...
% 7.59/7.66
% 7.59/7.66
% 7.59/7.66 % SZS status CounterSatisfiable for theBenchmark.p
% 7.59/7.66
% 7.59/7.66 % SZS output start Saturation for theBenchmark.p
% See solution above
% 7.59/7.69
% 7.59/7.69
%------------------------------------------------------------------------------