%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV107-1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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 01:43:03 PM UTC 2026
% Result : Unsatisfiable 143.83s 28.19s
% Output : CNFRefutation 198.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 137
% Syntax : Number of formulae : 602 ( 8 unt; 0 def)
% Number of atoms : 6029 ( 15 equ)
% Maximal formula atoms : 63 ( 10 avg)
% Number of connectives : 6486 (1059 ~;5427 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 11 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 72 ( 70 usr; 60 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 61 con; 0-0 aty)
% Number of variables : 84 ( 0 sgn 84 !; 0 ?; 66 :)
% Comments :
%------------------------------------------------------------------------------
fof(f628,axiom,
! [X0] :
( ~ sP22_aig_name(X0)
| ~ v69(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u213802) ).
fof(f629,axiom,
! [X0] :
( ~ sP22_aig_name(X0)
| ~ v21(X0)
| ~ v23(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u213803) ).
fof(f35836,axiom,
! [X0,X1] :
( ~ v8162(X0,X1)
| v8157(X0,X1)
| v8163(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164283) ).
fof(f35837,axiom,
! [X0,X1] :
( ~ v8157(X0,X1)
| v8162(X0,X1)
| v8163(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164284) ).
fof(f35838,axiom,
! [X0,X1] :
( ~ v81(X0)
| v614(X0)
| ~ v8161(X0,X1)
| v8162(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164280) ).
fof(f35839,axiom,
! [X0,X1] :
( ~ v81(X0)
| v614(X0)
| ~ v8162(X0,X1)
| v8161(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164281) ).
fof(f35840,axiom,
! [X0,X1] :
( v81(X0)
| ~ v8161(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164275) ).
fof(f35841,axiom,
! [X0,X1] :
( ~ v614(X0)
| ~ v8161(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164276) ).
fof(f35842,axiom,
! [X0,X1] :
( sP22_aig_name(X0)
| ~ v6250(X0,X1)
| v8161(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164272) ).
fof(f35843,axiom,
! [X0,X1] :
( sP22_aig_name(X0)
| ~ v8161(X0,X1)
| v6250(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u164273) ).
fof(f36156,axiom,
( ~ sP5244
| v6250(sK5142_VarCurr,bitIndex59)
| v8157(sK5142_VarCurr,bitIndex59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163829) ).
fof(f36157,axiom,
( ~ sP5244
| ~ v6250(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163830) ).
fof(f36158,axiom,
( ~ sP5245
| v6250(sK5142_VarCurr,bitIndex58)
| v8157(sK5142_VarCurr,bitIndex58) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163825) ).
fof(f36159,axiom,
( ~ sP5245
| ~ v6250(sK5142_VarCurr,bitIndex58)
| ~ v8157(sK5142_VarCurr,bitIndex58) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163826) ).
fof(f36160,axiom,
( ~ sP5246
| v6250(sK5142_VarCurr,bitIndex57)
| v8157(sK5142_VarCurr,bitIndex57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163821) ).
fof(f36161,axiom,
( ~ sP5246
| ~ v6250(sK5142_VarCurr,bitIndex57)
| ~ v8157(sK5142_VarCurr,bitIndex57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163822) ).
fof(f36162,axiom,
( ~ sP5247
| v6250(sK5142_VarCurr,bitIndex56)
| v8157(sK5142_VarCurr,bitIndex56) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163817) ).
fof(f36163,axiom,
( ~ sP5247
| ~ v6250(sK5142_VarCurr,bitIndex56)
| ~ v8157(sK5142_VarCurr,bitIndex56) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163818) ).
fof(f36164,axiom,
( ~ sP5248
| v6250(sK5142_VarCurr,bitIndex55)
| v8157(sK5142_VarCurr,bitIndex55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163813) ).
fof(f36165,axiom,
( ~ sP5248
| ~ v6250(sK5142_VarCurr,bitIndex55)
| ~ v8157(sK5142_VarCurr,bitIndex55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163814) ).
fof(f36166,axiom,
( ~ sP5249
| v6250(sK5142_VarCurr,bitIndex54)
| v8157(sK5142_VarCurr,bitIndex54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163809) ).
fof(f36167,axiom,
( ~ sP5249
| ~ v6250(sK5142_VarCurr,bitIndex54)
| ~ v8157(sK5142_VarCurr,bitIndex54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163810) ).
fof(f36168,axiom,
( ~ sP5250
| v6250(sK5142_VarCurr,bitIndex53)
| v8157(sK5142_VarCurr,bitIndex53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163805) ).
fof(f36169,axiom,
( ~ sP5250
| ~ v6250(sK5142_VarCurr,bitIndex53)
| ~ v8157(sK5142_VarCurr,bitIndex53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163806) ).
fof(f36170,axiom,
( ~ sP5251
| v6250(sK5142_VarCurr,bitIndex52)
| v8157(sK5142_VarCurr,bitIndex52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163801) ).
fof(f36171,axiom,
( ~ sP5251
| ~ v6250(sK5142_VarCurr,bitIndex52)
| ~ v8157(sK5142_VarCurr,bitIndex52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163802) ).
fof(f36172,axiom,
( ~ sP5252
| v6250(sK5142_VarCurr,bitIndex51)
| v8157(sK5142_VarCurr,bitIndex51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163797) ).
fof(f36173,axiom,
( ~ sP5252
| ~ v6250(sK5142_VarCurr,bitIndex51)
| ~ v8157(sK5142_VarCurr,bitIndex51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163798) ).
fof(f36174,axiom,
( ~ sP5253
| v6250(sK5142_VarCurr,bitIndex50)
| v8157(sK5142_VarCurr,bitIndex50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163793) ).
fof(f36175,axiom,
( ~ sP5253
| ~ v6250(sK5142_VarCurr,bitIndex50)
| ~ v8157(sK5142_VarCurr,bitIndex50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163794) ).
fof(f36176,axiom,
( ~ sP5254
| v6250(sK5142_VarCurr,bitIndex49)
| v8157(sK5142_VarCurr,bitIndex49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163789) ).
fof(f36177,axiom,
( ~ sP5254
| ~ v6250(sK5142_VarCurr,bitIndex49)
| ~ v8157(sK5142_VarCurr,bitIndex49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163790) ).
fof(f36178,axiom,
( ~ sP5255
| v6250(sK5142_VarCurr,bitIndex48)
| v8157(sK5142_VarCurr,bitIndex48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163785) ).
fof(f36179,axiom,
( ~ sP5255
| ~ v6250(sK5142_VarCurr,bitIndex48)
| ~ v8157(sK5142_VarCurr,bitIndex48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163786) ).
fof(f36180,axiom,
( ~ sP5256
| v6250(sK5142_VarCurr,bitIndex47)
| v8157(sK5142_VarCurr,bitIndex47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163781) ).
fof(f36181,axiom,
( ~ sP5256
| ~ v6250(sK5142_VarCurr,bitIndex47)
| ~ v8157(sK5142_VarCurr,bitIndex47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163782) ).
fof(f36182,axiom,
( ~ sP5257
| v6250(sK5142_VarCurr,bitIndex46)
| v8157(sK5142_VarCurr,bitIndex46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163777) ).
fof(f36183,axiom,
( ~ sP5257
| ~ v6250(sK5142_VarCurr,bitIndex46)
| ~ v8157(sK5142_VarCurr,bitIndex46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163778) ).
fof(f36184,axiom,
( ~ sP5258
| v6250(sK5142_VarCurr,bitIndex45)
| v8157(sK5142_VarCurr,bitIndex45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163773) ).
fof(f36185,axiom,
( ~ sP5258
| ~ v6250(sK5142_VarCurr,bitIndex45)
| ~ v8157(sK5142_VarCurr,bitIndex45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163774) ).
fof(f36186,axiom,
( ~ sP5259
| v6250(sK5142_VarCurr,bitIndex44)
| v8157(sK5142_VarCurr,bitIndex44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163769) ).
fof(f36187,axiom,
( ~ sP5259
| ~ v6250(sK5142_VarCurr,bitIndex44)
| ~ v8157(sK5142_VarCurr,bitIndex44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163770) ).
fof(f36188,axiom,
( ~ sP5260
| v6250(sK5142_VarCurr,bitIndex43)
| v8157(sK5142_VarCurr,bitIndex43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163765) ).
fof(f36189,axiom,
( ~ sP5260
| ~ v6250(sK5142_VarCurr,bitIndex43)
| ~ v8157(sK5142_VarCurr,bitIndex43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163766) ).
fof(f36190,axiom,
( ~ sP5261
| v6250(sK5142_VarCurr,bitIndex42)
| v8157(sK5142_VarCurr,bitIndex42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163761) ).
fof(f36191,axiom,
( ~ sP5261
| ~ v6250(sK5142_VarCurr,bitIndex42)
| ~ v8157(sK5142_VarCurr,bitIndex42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163762) ).
fof(f36192,axiom,
( ~ sP5262
| v6250(sK5142_VarCurr,bitIndex41)
| v8157(sK5142_VarCurr,bitIndex41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163757) ).
fof(f36193,axiom,
( ~ sP5262
| ~ v6250(sK5142_VarCurr,bitIndex41)
| ~ v8157(sK5142_VarCurr,bitIndex41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163758) ).
fof(f36194,axiom,
( ~ sP5263
| v6250(sK5142_VarCurr,bitIndex40)
| v8157(sK5142_VarCurr,bitIndex40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163753) ).
fof(f36195,axiom,
( ~ sP5263
| ~ v6250(sK5142_VarCurr,bitIndex40)
| ~ v8157(sK5142_VarCurr,bitIndex40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163754) ).
fof(f36196,axiom,
( ~ sP5264
| v6250(sK5142_VarCurr,bitIndex39)
| v8157(sK5142_VarCurr,bitIndex39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163749) ).
fof(f36197,axiom,
( ~ sP5264
| ~ v6250(sK5142_VarCurr,bitIndex39)
| ~ v8157(sK5142_VarCurr,bitIndex39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163750) ).
fof(f36198,axiom,
( ~ sP5265
| v6250(sK5142_VarCurr,bitIndex38)
| v8157(sK5142_VarCurr,bitIndex38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163745) ).
fof(f36199,axiom,
( ~ sP5265
| ~ v6250(sK5142_VarCurr,bitIndex38)
| ~ v8157(sK5142_VarCurr,bitIndex38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163746) ).
fof(f36200,axiom,
( ~ sP5266
| v6250(sK5142_VarCurr,bitIndex37)
| v8157(sK5142_VarCurr,bitIndex37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163741) ).
fof(f36201,axiom,
( ~ sP5266
| ~ v6250(sK5142_VarCurr,bitIndex37)
| ~ v8157(sK5142_VarCurr,bitIndex37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163742) ).
fof(f36202,axiom,
( ~ sP5267
| v6250(sK5142_VarCurr,bitIndex36)
| v8157(sK5142_VarCurr,bitIndex36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163737) ).
fof(f36203,axiom,
( ~ sP5267
| ~ v6250(sK5142_VarCurr,bitIndex36)
| ~ v8157(sK5142_VarCurr,bitIndex36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163738) ).
fof(f36204,axiom,
( ~ sP5268
| v6250(sK5142_VarCurr,bitIndex35)
| v8157(sK5142_VarCurr,bitIndex35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163733) ).
fof(f36205,axiom,
( ~ sP5268
| ~ v6250(sK5142_VarCurr,bitIndex35)
| ~ v8157(sK5142_VarCurr,bitIndex35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163734) ).
fof(f36206,axiom,
( ~ sP5269
| v6250(sK5142_VarCurr,bitIndex34)
| v8157(sK5142_VarCurr,bitIndex34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163729) ).
fof(f36207,axiom,
( ~ sP5269
| ~ v6250(sK5142_VarCurr,bitIndex34)
| ~ v8157(sK5142_VarCurr,bitIndex34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163730) ).
fof(f36208,axiom,
( ~ sP5270
| v6250(sK5142_VarCurr,bitIndex33)
| v8157(sK5142_VarCurr,bitIndex33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163725) ).
fof(f36209,axiom,
( ~ sP5270
| ~ v6250(sK5142_VarCurr,bitIndex33)
| ~ v8157(sK5142_VarCurr,bitIndex33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163726) ).
fof(f36210,axiom,
( ~ sP5271
| v6250(sK5142_VarCurr,bitIndex32)
| v8157(sK5142_VarCurr,bitIndex32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163721) ).
fof(f36211,axiom,
( ~ sP5271
| ~ v6250(sK5142_VarCurr,bitIndex32)
| ~ v8157(sK5142_VarCurr,bitIndex32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163722) ).
fof(f36212,axiom,
( ~ sP5272
| v6250(sK5142_VarCurr,bitIndex31)
| v8157(sK5142_VarCurr,bitIndex31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163717) ).
fof(f36213,axiom,
( ~ sP5272
| ~ v6250(sK5142_VarCurr,bitIndex31)
| ~ v8157(sK5142_VarCurr,bitIndex31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163718) ).
fof(f36214,axiom,
( ~ sP5273
| v6250(sK5142_VarCurr,bitIndex30)
| v8157(sK5142_VarCurr,bitIndex30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163713) ).
fof(f36215,axiom,
( ~ sP5273
| ~ v6250(sK5142_VarCurr,bitIndex30)
| ~ v8157(sK5142_VarCurr,bitIndex30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163714) ).
fof(f36216,axiom,
( ~ sP5274
| v6250(sK5142_VarCurr,bitIndex29)
| v8157(sK5142_VarCurr,bitIndex29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163709) ).
fof(f36217,axiom,
( ~ sP5274
| ~ v6250(sK5142_VarCurr,bitIndex29)
| ~ v8157(sK5142_VarCurr,bitIndex29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163710) ).
fof(f36218,axiom,
( ~ sP5275
| v6250(sK5142_VarCurr,bitIndex28)
| v8157(sK5142_VarCurr,bitIndex28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163705) ).
fof(f36219,axiom,
( ~ sP5275
| ~ v6250(sK5142_VarCurr,bitIndex28)
| ~ v8157(sK5142_VarCurr,bitIndex28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163706) ).
fof(f36220,axiom,
( ~ sP5276
| v6250(sK5142_VarCurr,bitIndex27)
| v8157(sK5142_VarCurr,bitIndex27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163701) ).
fof(f36221,axiom,
( ~ sP5276
| ~ v6250(sK5142_VarCurr,bitIndex27)
| ~ v8157(sK5142_VarCurr,bitIndex27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163702) ).
fof(f36222,axiom,
( ~ sP5277
| v6250(sK5142_VarCurr,bitIndex26)
| v8157(sK5142_VarCurr,bitIndex26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163697) ).
fof(f36223,axiom,
( ~ sP5277
| ~ v6250(sK5142_VarCurr,bitIndex26)
| ~ v8157(sK5142_VarCurr,bitIndex26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163698) ).
fof(f36224,axiom,
( ~ sP5278
| v6250(sK5142_VarCurr,bitIndex25)
| v8157(sK5142_VarCurr,bitIndex25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163693) ).
fof(f36225,axiom,
( ~ sP5278
| ~ v6250(sK5142_VarCurr,bitIndex25)
| ~ v8157(sK5142_VarCurr,bitIndex25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163694) ).
fof(f36226,axiom,
( ~ sP5279
| v6250(sK5142_VarCurr,bitIndex24)
| v8157(sK5142_VarCurr,bitIndex24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163689) ).
fof(f36227,axiom,
( ~ sP5279
| ~ v6250(sK5142_VarCurr,bitIndex24)
| ~ v8157(sK5142_VarCurr,bitIndex24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163690) ).
fof(f36228,axiom,
( ~ sP5280
| v6250(sK5142_VarCurr,bitIndex23)
| v8157(sK5142_VarCurr,bitIndex23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163685) ).
fof(f36229,axiom,
( ~ sP5280
| ~ v6250(sK5142_VarCurr,bitIndex23)
| ~ v8157(sK5142_VarCurr,bitIndex23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163686) ).
fof(f36230,axiom,
( ~ sP5281
| v6250(sK5142_VarCurr,bitIndex22)
| v8157(sK5142_VarCurr,bitIndex22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163681) ).
fof(f36231,axiom,
( ~ sP5281
| ~ v6250(sK5142_VarCurr,bitIndex22)
| ~ v8157(sK5142_VarCurr,bitIndex22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163682) ).
fof(f36232,axiom,
( ~ sP5282
| v6250(sK5142_VarCurr,bitIndex21)
| v8157(sK5142_VarCurr,bitIndex21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163677) ).
fof(f36233,axiom,
( ~ sP5282
| ~ v6250(sK5142_VarCurr,bitIndex21)
| ~ v8157(sK5142_VarCurr,bitIndex21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163678) ).
fof(f36234,axiom,
( ~ sP5283
| v6250(sK5142_VarCurr,bitIndex20)
| v8157(sK5142_VarCurr,bitIndex20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163673) ).
fof(f36235,axiom,
( ~ sP5283
| ~ v6250(sK5142_VarCurr,bitIndex20)
| ~ v8157(sK5142_VarCurr,bitIndex20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163674) ).
fof(f36236,axiom,
( ~ sP5284
| v6250(sK5142_VarCurr,bitIndex19)
| v8157(sK5142_VarCurr,bitIndex19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163669) ).
fof(f36237,axiom,
( ~ sP5284
| ~ v6250(sK5142_VarCurr,bitIndex19)
| ~ v8157(sK5142_VarCurr,bitIndex19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163670) ).
fof(f36238,axiom,
( ~ sP5285
| v6250(sK5142_VarCurr,bitIndex18)
| v8157(sK5142_VarCurr,bitIndex18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163665) ).
fof(f36239,axiom,
( ~ sP5285
| ~ v6250(sK5142_VarCurr,bitIndex18)
| ~ v8157(sK5142_VarCurr,bitIndex18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163666) ).
fof(f36240,axiom,
( ~ sP5286
| v6250(sK5142_VarCurr,bitIndex17)
| v8157(sK5142_VarCurr,bitIndex17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163661) ).
fof(f36241,axiom,
( ~ sP5286
| ~ v6250(sK5142_VarCurr,bitIndex17)
| ~ v8157(sK5142_VarCurr,bitIndex17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163662) ).
fof(f36242,axiom,
( ~ sP5287
| v6250(sK5142_VarCurr,bitIndex16)
| v8157(sK5142_VarCurr,bitIndex16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163657) ).
fof(f36243,axiom,
( ~ sP5287
| ~ v6250(sK5142_VarCurr,bitIndex16)
| ~ v8157(sK5142_VarCurr,bitIndex16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163658) ).
fof(f36244,axiom,
( ~ sP5288
| v6250(sK5142_VarCurr,bitIndex15)
| v8157(sK5142_VarCurr,bitIndex15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163653) ).
fof(f36245,axiom,
( ~ sP5288
| ~ v6250(sK5142_VarCurr,bitIndex15)
| ~ v8157(sK5142_VarCurr,bitIndex15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163654) ).
fof(f36246,axiom,
( ~ sP5289
| v6250(sK5142_VarCurr,bitIndex14)
| v8157(sK5142_VarCurr,bitIndex14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163649) ).
fof(f36247,axiom,
( ~ sP5289
| ~ v6250(sK5142_VarCurr,bitIndex14)
| ~ v8157(sK5142_VarCurr,bitIndex14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163650) ).
fof(f36248,axiom,
( ~ sP5290
| v6250(sK5142_VarCurr,bitIndex13)
| v8157(sK5142_VarCurr,bitIndex13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163645) ).
fof(f36249,axiom,
( ~ sP5290
| ~ v6250(sK5142_VarCurr,bitIndex13)
| ~ v8157(sK5142_VarCurr,bitIndex13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163646) ).
fof(f36250,axiom,
( ~ sP5291
| v6250(sK5142_VarCurr,bitIndex12)
| v8157(sK5142_VarCurr,bitIndex12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163641) ).
fof(f36251,axiom,
( ~ sP5291
| ~ v6250(sK5142_VarCurr,bitIndex12)
| ~ v8157(sK5142_VarCurr,bitIndex12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163642) ).
fof(f36252,axiom,
( ~ sP5292
| v6250(sK5142_VarCurr,bitIndex11)
| v8157(sK5142_VarCurr,bitIndex11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163637) ).
fof(f36253,axiom,
( ~ sP5292
| ~ v6250(sK5142_VarCurr,bitIndex11)
| ~ v8157(sK5142_VarCurr,bitIndex11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163638) ).
fof(f36254,axiom,
( ~ sP5293
| v6250(sK5142_VarCurr,bitIndex10)
| v8157(sK5142_VarCurr,bitIndex10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163633) ).
fof(f36255,axiom,
( ~ sP5293
| ~ v6250(sK5142_VarCurr,bitIndex10)
| ~ v8157(sK5142_VarCurr,bitIndex10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163634) ).
fof(f36256,axiom,
( ~ sP5294
| v6250(sK5142_VarCurr,bitIndex9)
| v8157(sK5142_VarCurr,bitIndex9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163629) ).
fof(f36257,axiom,
( ~ sP5294
| ~ v6250(sK5142_VarCurr,bitIndex9)
| ~ v8157(sK5142_VarCurr,bitIndex9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163630) ).
fof(f36258,axiom,
( ~ sP5295
| v6250(sK5142_VarCurr,bitIndex8)
| v8157(sK5142_VarCurr,bitIndex8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163625) ).
fof(f36259,axiom,
( ~ sP5295
| ~ v6250(sK5142_VarCurr,bitIndex8)
| ~ v8157(sK5142_VarCurr,bitIndex8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163626) ).
fof(f36260,axiom,
( ~ sP5296
| v6250(sK5142_VarCurr,bitIndex7)
| v8157(sK5142_VarCurr,bitIndex7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163621) ).
fof(f36261,axiom,
( ~ sP5296
| ~ v6250(sK5142_VarCurr,bitIndex7)
| ~ v8157(sK5142_VarCurr,bitIndex7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163622) ).
fof(f36262,axiom,
( ~ sP5297
| v6250(sK5142_VarCurr,bitIndex6)
| v8157(sK5142_VarCurr,bitIndex6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163617) ).
fof(f36263,axiom,
( ~ sP5297
| ~ v6250(sK5142_VarCurr,bitIndex6)
| ~ v8157(sK5142_VarCurr,bitIndex6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163618) ).
fof(f36264,axiom,
( ~ sP5298
| v6250(sK5142_VarCurr,bitIndex5)
| v8157(sK5142_VarCurr,bitIndex5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163613) ).
fof(f36265,axiom,
( ~ sP5298
| ~ v6250(sK5142_VarCurr,bitIndex5)
| ~ v8157(sK5142_VarCurr,bitIndex5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163614) ).
fof(f36266,axiom,
( ~ sP5299
| v6250(sK5142_VarCurr,bitIndex4)
| v8157(sK5142_VarCurr,bitIndex4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163609) ).
fof(f36267,axiom,
( ~ sP5299
| ~ v6250(sK5142_VarCurr,bitIndex4)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163610) ).
fof(f36268,axiom,
( ~ sP5300
| v6250(sK5142_VarCurr,bitIndex3)
| v8157(sK5142_VarCurr,bitIndex3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163605) ).
fof(f36269,axiom,
( ~ sP5300
| ~ v6250(sK5142_VarCurr,bitIndex3)
| ~ v8157(sK5142_VarCurr,bitIndex3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163606) ).
fof(f36270,negated_conjecture,
v81(sK5142_VarCurr),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163589) ).
fof(f36271,negated_conjecture,
~ v614(sK5142_VarCurr),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163590) ).
fof(f36272,negated_conjecture,
~ v8163(sK5142_VarCurr),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163591) ).
fof(f36273,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163592) ).
fof(f36274,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163593) ).
fof(f36275,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163594) ).
fof(f36276,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163595) ).
fof(f36277,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163596) ).
fof(f36278,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163597) ).
fof(f36279,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163598) ).
fof(f36280,negated_conjecture,
( sP5244
| sP5245
| sP5246
| sP5247
| sP5248
| sP5249
| sP5250
| sP5251
| sP5252
| sP5253
| sP5254
| sP5255
| sP5256
| sP5257
| sP5258
| sP5259
| sP5260
| sP5261
| sP5262
| sP5263
| sP5264
| sP5265
| sP5266
| sP5267
| sP5268
| sP5269
| sP5270
| sP5271
| sP5272
| sP5273
| sP5274
| sP5275
| sP5276
| sP5277
| sP5278
| sP5279
| sP5280
| sP5281
| sP5282
| sP5283
| sP5284
| sP5285
| sP5286
| sP5287
| sP5288
| sP5289
| sP5290
| sP5291
| sP5292
| sP5293
| sP5294
| sP5295
| sP5296
| sP5297
| sP5298
| sP5299
| sP5300
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163599) ).
fof(f36281,negated_conjecture,
( v23(sK5142_VarCurr)
| v69(sK5142_VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163600) ).
fof(f36282,negated_conjecture,
( v21(sK5142_VarCurr)
| v69(sK5142_VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',u163601) ).
tcf(c_40318,negated_conjecture,
v81(sK5142_VarCurr),
inference(cnf_transformation,[],[f36270]) ).
tcf(c_40319,negated_conjecture,
~ v614(sK5142_VarCurr),
inference(cnf_transformation,[],[f36271]) ).
tcf(c_40320,negated_conjecture,
~ v8163(sK5142_VarCurr),
inference(cnf_transformation,[],[f36272]) ).
tcf(c_40321,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f36273]) ).
tcf(c_40322,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(cnf_transformation,[],[f36274]) ).
tcf(c_40323,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f36275]) ).
tcf(c_40324,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f36276]) ).
tcf(c_40325,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
inference(cnf_transformation,[],[f36277]) ).
tcf(c_40326,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(cnf_transformation,[],[f36278]) ).
tcf(c_40327,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f36279]) ).
tcf(c_40328,negated_conjecture,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f36280]) ).
tcf(c_40329,negated_conjecture,
( v23(sK5142_VarCurr)
| v69(sK5142_VarCurr) ),
inference(cnf_transformation,[],[f36281]) ).
tcf(c_40330,negated_conjecture,
( v21(sK5142_VarCurr)
| v69(sK5142_VarCurr) ),
inference(cnf_transformation,[],[f36282]) ).
tcf(c_40341,plain,
! [X0: $i,X1: $i] :
( v8163(X0)
| v8162(X0,X1)
| ~ v8157(X0,X1) ),
inference(cnf_transformation,[],[f35837]) ).
tcf(c_40342,plain,
! [X0: $i,X1: $i] :
( v8163(X0)
| v8157(X0,X1)
| ~ v8162(X0,X1) ),
inference(cnf_transformation,[],[f35836]) ).
tcf(c_40346,plain,
( ~ sP5244
| ~ v6250(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
inference(cnf_transformation,[],[f36157]) ).
tcf(c_40347,plain,
( v6250(sK5142_VarCurr,bitIndex59)
| v8157(sK5142_VarCurr,bitIndex59)
| ~ sP5244 ),
inference(cnf_transformation,[],[f36156]) ).
tcf(c_40348,plain,
( ~ sP5245
| ~ v6250(sK5142_VarCurr,bitIndex58)
| ~ v8157(sK5142_VarCurr,bitIndex58) ),
inference(cnf_transformation,[],[f36159]) ).
tcf(c_40349,plain,
( v6250(sK5142_VarCurr,bitIndex58)
| v8157(sK5142_VarCurr,bitIndex58)
| ~ sP5245 ),
inference(cnf_transformation,[],[f36158]) ).
tcf(c_40350,plain,
( ~ sP5246
| ~ v6250(sK5142_VarCurr,bitIndex57)
| ~ v8157(sK5142_VarCurr,bitIndex57) ),
inference(cnf_transformation,[],[f36161]) ).
tcf(c_40351,plain,
( v6250(sK5142_VarCurr,bitIndex57)
| v8157(sK5142_VarCurr,bitIndex57)
| ~ sP5246 ),
inference(cnf_transformation,[],[f36160]) ).
tcf(c_40352,plain,
( ~ sP5247
| ~ v6250(sK5142_VarCurr,bitIndex56)
| ~ v8157(sK5142_VarCurr,bitIndex56) ),
inference(cnf_transformation,[],[f36163]) ).
tcf(c_40353,plain,
( v6250(sK5142_VarCurr,bitIndex56)
| v8157(sK5142_VarCurr,bitIndex56)
| ~ sP5247 ),
inference(cnf_transformation,[],[f36162]) ).
tcf(c_40354,plain,
( ~ sP5248
| ~ v6250(sK5142_VarCurr,bitIndex55)
| ~ v8157(sK5142_VarCurr,bitIndex55) ),
inference(cnf_transformation,[],[f36165]) ).
tcf(c_40355,plain,
( v6250(sK5142_VarCurr,bitIndex55)
| v8157(sK5142_VarCurr,bitIndex55)
| ~ sP5248 ),
inference(cnf_transformation,[],[f36164]) ).
tcf(c_40356,plain,
( ~ sP5249
| ~ v6250(sK5142_VarCurr,bitIndex54)
| ~ v8157(sK5142_VarCurr,bitIndex54) ),
inference(cnf_transformation,[],[f36167]) ).
tcf(c_40357,plain,
( v6250(sK5142_VarCurr,bitIndex54)
| v8157(sK5142_VarCurr,bitIndex54)
| ~ sP5249 ),
inference(cnf_transformation,[],[f36166]) ).
tcf(c_40358,plain,
( ~ sP5250
| ~ v6250(sK5142_VarCurr,bitIndex53)
| ~ v8157(sK5142_VarCurr,bitIndex53) ),
inference(cnf_transformation,[],[f36169]) ).
tcf(c_40359,plain,
( v6250(sK5142_VarCurr,bitIndex53)
| v8157(sK5142_VarCurr,bitIndex53)
| ~ sP5250 ),
inference(cnf_transformation,[],[f36168]) ).
tcf(c_40360,plain,
( ~ sP5251
| ~ v6250(sK5142_VarCurr,bitIndex52)
| ~ v8157(sK5142_VarCurr,bitIndex52) ),
inference(cnf_transformation,[],[f36171]) ).
tcf(c_40361,plain,
( v6250(sK5142_VarCurr,bitIndex52)
| v8157(sK5142_VarCurr,bitIndex52)
| ~ sP5251 ),
inference(cnf_transformation,[],[f36170]) ).
tcf(c_40362,plain,
( ~ sP5252
| ~ v6250(sK5142_VarCurr,bitIndex51)
| ~ v8157(sK5142_VarCurr,bitIndex51) ),
inference(cnf_transformation,[],[f36173]) ).
tcf(c_40363,plain,
( v6250(sK5142_VarCurr,bitIndex51)
| v8157(sK5142_VarCurr,bitIndex51)
| ~ sP5252 ),
inference(cnf_transformation,[],[f36172]) ).
tcf(c_40364,plain,
( ~ sP5253
| ~ v6250(sK5142_VarCurr,bitIndex50)
| ~ v8157(sK5142_VarCurr,bitIndex50) ),
inference(cnf_transformation,[],[f36175]) ).
tcf(c_40365,plain,
( v6250(sK5142_VarCurr,bitIndex50)
| v8157(sK5142_VarCurr,bitIndex50)
| ~ sP5253 ),
inference(cnf_transformation,[],[f36174]) ).
tcf(c_40366,plain,
( ~ sP5254
| ~ v6250(sK5142_VarCurr,bitIndex49)
| ~ v8157(sK5142_VarCurr,bitIndex49) ),
inference(cnf_transformation,[],[f36177]) ).
tcf(c_40367,plain,
( v6250(sK5142_VarCurr,bitIndex49)
| v8157(sK5142_VarCurr,bitIndex49)
| ~ sP5254 ),
inference(cnf_transformation,[],[f36176]) ).
tcf(c_40368,plain,
( ~ sP5255
| ~ v6250(sK5142_VarCurr,bitIndex48)
| ~ v8157(sK5142_VarCurr,bitIndex48) ),
inference(cnf_transformation,[],[f36179]) ).
tcf(c_40369,plain,
( v6250(sK5142_VarCurr,bitIndex48)
| v8157(sK5142_VarCurr,bitIndex48)
| ~ sP5255 ),
inference(cnf_transformation,[],[f36178]) ).
tcf(c_40370,plain,
( ~ sP5256
| ~ v6250(sK5142_VarCurr,bitIndex47)
| ~ v8157(sK5142_VarCurr,bitIndex47) ),
inference(cnf_transformation,[],[f36181]) ).
tcf(c_40371,plain,
( v6250(sK5142_VarCurr,bitIndex47)
| v8157(sK5142_VarCurr,bitIndex47)
| ~ sP5256 ),
inference(cnf_transformation,[],[f36180]) ).
tcf(c_40372,plain,
( ~ sP5257
| ~ v6250(sK5142_VarCurr,bitIndex46)
| ~ v8157(sK5142_VarCurr,bitIndex46) ),
inference(cnf_transformation,[],[f36183]) ).
tcf(c_40373,plain,
( v6250(sK5142_VarCurr,bitIndex46)
| v8157(sK5142_VarCurr,bitIndex46)
| ~ sP5257 ),
inference(cnf_transformation,[],[f36182]) ).
tcf(c_40374,plain,
( ~ sP5258
| ~ v6250(sK5142_VarCurr,bitIndex45)
| ~ v8157(sK5142_VarCurr,bitIndex45) ),
inference(cnf_transformation,[],[f36185]) ).
tcf(c_40375,plain,
( v6250(sK5142_VarCurr,bitIndex45)
| v8157(sK5142_VarCurr,bitIndex45)
| ~ sP5258 ),
inference(cnf_transformation,[],[f36184]) ).
tcf(c_40376,plain,
( ~ sP5259
| ~ v6250(sK5142_VarCurr,bitIndex44)
| ~ v8157(sK5142_VarCurr,bitIndex44) ),
inference(cnf_transformation,[],[f36187]) ).
tcf(c_40377,plain,
( v6250(sK5142_VarCurr,bitIndex44)
| v8157(sK5142_VarCurr,bitIndex44)
| ~ sP5259 ),
inference(cnf_transformation,[],[f36186]) ).
tcf(c_40378,plain,
( ~ sP5260
| ~ v6250(sK5142_VarCurr,bitIndex43)
| ~ v8157(sK5142_VarCurr,bitIndex43) ),
inference(cnf_transformation,[],[f36189]) ).
tcf(c_40379,plain,
( v6250(sK5142_VarCurr,bitIndex43)
| v8157(sK5142_VarCurr,bitIndex43)
| ~ sP5260 ),
inference(cnf_transformation,[],[f36188]) ).
tcf(c_40380,plain,
( ~ sP5261
| ~ v6250(sK5142_VarCurr,bitIndex42)
| ~ v8157(sK5142_VarCurr,bitIndex42) ),
inference(cnf_transformation,[],[f36191]) ).
tcf(c_40381,plain,
( v6250(sK5142_VarCurr,bitIndex42)
| v8157(sK5142_VarCurr,bitIndex42)
| ~ sP5261 ),
inference(cnf_transformation,[],[f36190]) ).
tcf(c_40382,plain,
( ~ sP5262
| ~ v6250(sK5142_VarCurr,bitIndex41)
| ~ v8157(sK5142_VarCurr,bitIndex41) ),
inference(cnf_transformation,[],[f36193]) ).
tcf(c_40383,plain,
( v6250(sK5142_VarCurr,bitIndex41)
| v8157(sK5142_VarCurr,bitIndex41)
| ~ sP5262 ),
inference(cnf_transformation,[],[f36192]) ).
tcf(c_40384,plain,
( ~ sP5263
| ~ v6250(sK5142_VarCurr,bitIndex40)
| ~ v8157(sK5142_VarCurr,bitIndex40) ),
inference(cnf_transformation,[],[f36195]) ).
tcf(c_40385,plain,
( v6250(sK5142_VarCurr,bitIndex40)
| v8157(sK5142_VarCurr,bitIndex40)
| ~ sP5263 ),
inference(cnf_transformation,[],[f36194]) ).
tcf(c_40386,plain,
( ~ sP5264
| ~ v6250(sK5142_VarCurr,bitIndex39)
| ~ v8157(sK5142_VarCurr,bitIndex39) ),
inference(cnf_transformation,[],[f36197]) ).
tcf(c_40387,plain,
( v6250(sK5142_VarCurr,bitIndex39)
| v8157(sK5142_VarCurr,bitIndex39)
| ~ sP5264 ),
inference(cnf_transformation,[],[f36196]) ).
tcf(c_40388,plain,
( ~ sP5265
| ~ v6250(sK5142_VarCurr,bitIndex38)
| ~ v8157(sK5142_VarCurr,bitIndex38) ),
inference(cnf_transformation,[],[f36199]) ).
tcf(c_40389,plain,
( v6250(sK5142_VarCurr,bitIndex38)
| v8157(sK5142_VarCurr,bitIndex38)
| ~ sP5265 ),
inference(cnf_transformation,[],[f36198]) ).
tcf(c_40390,plain,
( ~ sP5266
| ~ v6250(sK5142_VarCurr,bitIndex37)
| ~ v8157(sK5142_VarCurr,bitIndex37) ),
inference(cnf_transformation,[],[f36201]) ).
tcf(c_40391,plain,
( v6250(sK5142_VarCurr,bitIndex37)
| v8157(sK5142_VarCurr,bitIndex37)
| ~ sP5266 ),
inference(cnf_transformation,[],[f36200]) ).
tcf(c_40392,plain,
( ~ sP5267
| ~ v6250(sK5142_VarCurr,bitIndex36)
| ~ v8157(sK5142_VarCurr,bitIndex36) ),
inference(cnf_transformation,[],[f36203]) ).
tcf(c_40393,plain,
( v6250(sK5142_VarCurr,bitIndex36)
| v8157(sK5142_VarCurr,bitIndex36)
| ~ sP5267 ),
inference(cnf_transformation,[],[f36202]) ).
tcf(c_40394,plain,
( ~ sP5268
| ~ v6250(sK5142_VarCurr,bitIndex35)
| ~ v8157(sK5142_VarCurr,bitIndex35) ),
inference(cnf_transformation,[],[f36205]) ).
tcf(c_40395,plain,
( v6250(sK5142_VarCurr,bitIndex35)
| v8157(sK5142_VarCurr,bitIndex35)
| ~ sP5268 ),
inference(cnf_transformation,[],[f36204]) ).
tcf(c_40396,plain,
( ~ sP5269
| ~ v6250(sK5142_VarCurr,bitIndex34)
| ~ v8157(sK5142_VarCurr,bitIndex34) ),
inference(cnf_transformation,[],[f36207]) ).
tcf(c_40397,plain,
( v6250(sK5142_VarCurr,bitIndex34)
| v8157(sK5142_VarCurr,bitIndex34)
| ~ sP5269 ),
inference(cnf_transformation,[],[f36206]) ).
tcf(c_40398,plain,
( ~ sP5270
| ~ v6250(sK5142_VarCurr,bitIndex33)
| ~ v8157(sK5142_VarCurr,bitIndex33) ),
inference(cnf_transformation,[],[f36209]) ).
tcf(c_40399,plain,
( v6250(sK5142_VarCurr,bitIndex33)
| v8157(sK5142_VarCurr,bitIndex33)
| ~ sP5270 ),
inference(cnf_transformation,[],[f36208]) ).
tcf(c_40400,plain,
( ~ sP5271
| ~ v6250(sK5142_VarCurr,bitIndex32)
| ~ v8157(sK5142_VarCurr,bitIndex32) ),
inference(cnf_transformation,[],[f36211]) ).
tcf(c_40401,plain,
( v6250(sK5142_VarCurr,bitIndex32)
| v8157(sK5142_VarCurr,bitIndex32)
| ~ sP5271 ),
inference(cnf_transformation,[],[f36210]) ).
tcf(c_40402,plain,
( ~ sP5272
| ~ v6250(sK5142_VarCurr,bitIndex31)
| ~ v8157(sK5142_VarCurr,bitIndex31) ),
inference(cnf_transformation,[],[f36213]) ).
tcf(c_40403,plain,
( v6250(sK5142_VarCurr,bitIndex31)
| v8157(sK5142_VarCurr,bitIndex31)
| ~ sP5272 ),
inference(cnf_transformation,[],[f36212]) ).
tcf(c_40404,plain,
( ~ sP5273
| ~ v6250(sK5142_VarCurr,bitIndex30)
| ~ v8157(sK5142_VarCurr,bitIndex30) ),
inference(cnf_transformation,[],[f36215]) ).
tcf(c_40405,plain,
( v6250(sK5142_VarCurr,bitIndex30)
| v8157(sK5142_VarCurr,bitIndex30)
| ~ sP5273 ),
inference(cnf_transformation,[],[f36214]) ).
tcf(c_40406,plain,
( ~ sP5274
| ~ v6250(sK5142_VarCurr,bitIndex29)
| ~ v8157(sK5142_VarCurr,bitIndex29) ),
inference(cnf_transformation,[],[f36217]) ).
tcf(c_40407,plain,
( v6250(sK5142_VarCurr,bitIndex29)
| v8157(sK5142_VarCurr,bitIndex29)
| ~ sP5274 ),
inference(cnf_transformation,[],[f36216]) ).
tcf(c_40408,plain,
( ~ sP5275
| ~ v6250(sK5142_VarCurr,bitIndex28)
| ~ v8157(sK5142_VarCurr,bitIndex28) ),
inference(cnf_transformation,[],[f36219]) ).
tcf(c_40409,plain,
( v6250(sK5142_VarCurr,bitIndex28)
| v8157(sK5142_VarCurr,bitIndex28)
| ~ sP5275 ),
inference(cnf_transformation,[],[f36218]) ).
tcf(c_40410,plain,
( ~ sP5276
| ~ v6250(sK5142_VarCurr,bitIndex27)
| ~ v8157(sK5142_VarCurr,bitIndex27) ),
inference(cnf_transformation,[],[f36221]) ).
tcf(c_40411,plain,
( v6250(sK5142_VarCurr,bitIndex27)
| v8157(sK5142_VarCurr,bitIndex27)
| ~ sP5276 ),
inference(cnf_transformation,[],[f36220]) ).
tcf(c_40412,plain,
( ~ sP5277
| ~ v6250(sK5142_VarCurr,bitIndex26)
| ~ v8157(sK5142_VarCurr,bitIndex26) ),
inference(cnf_transformation,[],[f36223]) ).
tcf(c_40413,plain,
( v6250(sK5142_VarCurr,bitIndex26)
| v8157(sK5142_VarCurr,bitIndex26)
| ~ sP5277 ),
inference(cnf_transformation,[],[f36222]) ).
tcf(c_40414,plain,
( ~ sP5278
| ~ v6250(sK5142_VarCurr,bitIndex25)
| ~ v8157(sK5142_VarCurr,bitIndex25) ),
inference(cnf_transformation,[],[f36225]) ).
tcf(c_40415,plain,
( v6250(sK5142_VarCurr,bitIndex25)
| v8157(sK5142_VarCurr,bitIndex25)
| ~ sP5278 ),
inference(cnf_transformation,[],[f36224]) ).
tcf(c_40416,plain,
( ~ sP5279
| ~ v6250(sK5142_VarCurr,bitIndex24)
| ~ v8157(sK5142_VarCurr,bitIndex24) ),
inference(cnf_transformation,[],[f36227]) ).
tcf(c_40417,plain,
( v6250(sK5142_VarCurr,bitIndex24)
| v8157(sK5142_VarCurr,bitIndex24)
| ~ sP5279 ),
inference(cnf_transformation,[],[f36226]) ).
tcf(c_40418,plain,
( ~ sP5280
| ~ v6250(sK5142_VarCurr,bitIndex23)
| ~ v8157(sK5142_VarCurr,bitIndex23) ),
inference(cnf_transformation,[],[f36229]) ).
tcf(c_40419,plain,
( v6250(sK5142_VarCurr,bitIndex23)
| v8157(sK5142_VarCurr,bitIndex23)
| ~ sP5280 ),
inference(cnf_transformation,[],[f36228]) ).
tcf(c_40420,plain,
( ~ sP5281
| ~ v6250(sK5142_VarCurr,bitIndex22)
| ~ v8157(sK5142_VarCurr,bitIndex22) ),
inference(cnf_transformation,[],[f36231]) ).
tcf(c_40421,plain,
( v6250(sK5142_VarCurr,bitIndex22)
| v8157(sK5142_VarCurr,bitIndex22)
| ~ sP5281 ),
inference(cnf_transformation,[],[f36230]) ).
tcf(c_40422,plain,
( ~ sP5282
| ~ v6250(sK5142_VarCurr,bitIndex21)
| ~ v8157(sK5142_VarCurr,bitIndex21) ),
inference(cnf_transformation,[],[f36233]) ).
tcf(c_40423,plain,
( v6250(sK5142_VarCurr,bitIndex21)
| v8157(sK5142_VarCurr,bitIndex21)
| ~ sP5282 ),
inference(cnf_transformation,[],[f36232]) ).
tcf(c_40424,plain,
( ~ sP5283
| ~ v6250(sK5142_VarCurr,bitIndex20)
| ~ v8157(sK5142_VarCurr,bitIndex20) ),
inference(cnf_transformation,[],[f36235]) ).
tcf(c_40425,plain,
( v6250(sK5142_VarCurr,bitIndex20)
| v8157(sK5142_VarCurr,bitIndex20)
| ~ sP5283 ),
inference(cnf_transformation,[],[f36234]) ).
tcf(c_40426,plain,
( ~ sP5284
| ~ v6250(sK5142_VarCurr,bitIndex19)
| ~ v8157(sK5142_VarCurr,bitIndex19) ),
inference(cnf_transformation,[],[f36237]) ).
tcf(c_40427,plain,
( v6250(sK5142_VarCurr,bitIndex19)
| v8157(sK5142_VarCurr,bitIndex19)
| ~ sP5284 ),
inference(cnf_transformation,[],[f36236]) ).
tcf(c_40428,plain,
( ~ sP5285
| ~ v6250(sK5142_VarCurr,bitIndex18)
| ~ v8157(sK5142_VarCurr,bitIndex18) ),
inference(cnf_transformation,[],[f36239]) ).
tcf(c_40429,plain,
( v6250(sK5142_VarCurr,bitIndex18)
| v8157(sK5142_VarCurr,bitIndex18)
| ~ sP5285 ),
inference(cnf_transformation,[],[f36238]) ).
tcf(c_40430,plain,
( ~ sP5286
| ~ v6250(sK5142_VarCurr,bitIndex17)
| ~ v8157(sK5142_VarCurr,bitIndex17) ),
inference(cnf_transformation,[],[f36241]) ).
tcf(c_40431,plain,
( v6250(sK5142_VarCurr,bitIndex17)
| v8157(sK5142_VarCurr,bitIndex17)
| ~ sP5286 ),
inference(cnf_transformation,[],[f36240]) ).
tcf(c_40432,plain,
( ~ sP5287
| ~ v6250(sK5142_VarCurr,bitIndex16)
| ~ v8157(sK5142_VarCurr,bitIndex16) ),
inference(cnf_transformation,[],[f36243]) ).
tcf(c_40433,plain,
( v6250(sK5142_VarCurr,bitIndex16)
| v8157(sK5142_VarCurr,bitIndex16)
| ~ sP5287 ),
inference(cnf_transformation,[],[f36242]) ).
tcf(c_40434,plain,
( ~ sP5288
| ~ v6250(sK5142_VarCurr,bitIndex15)
| ~ v8157(sK5142_VarCurr,bitIndex15) ),
inference(cnf_transformation,[],[f36245]) ).
tcf(c_40435,plain,
( v6250(sK5142_VarCurr,bitIndex15)
| v8157(sK5142_VarCurr,bitIndex15)
| ~ sP5288 ),
inference(cnf_transformation,[],[f36244]) ).
tcf(c_40436,plain,
( ~ sP5289
| ~ v6250(sK5142_VarCurr,bitIndex14)
| ~ v8157(sK5142_VarCurr,bitIndex14) ),
inference(cnf_transformation,[],[f36247]) ).
tcf(c_40437,plain,
( v6250(sK5142_VarCurr,bitIndex14)
| v8157(sK5142_VarCurr,bitIndex14)
| ~ sP5289 ),
inference(cnf_transformation,[],[f36246]) ).
tcf(c_40438,plain,
( ~ sP5290
| ~ v6250(sK5142_VarCurr,bitIndex13)
| ~ v8157(sK5142_VarCurr,bitIndex13) ),
inference(cnf_transformation,[],[f36249]) ).
tcf(c_40439,plain,
( v6250(sK5142_VarCurr,bitIndex13)
| v8157(sK5142_VarCurr,bitIndex13)
| ~ sP5290 ),
inference(cnf_transformation,[],[f36248]) ).
tcf(c_40440,plain,
( ~ sP5291
| ~ v6250(sK5142_VarCurr,bitIndex12)
| ~ v8157(sK5142_VarCurr,bitIndex12) ),
inference(cnf_transformation,[],[f36251]) ).
tcf(c_40441,plain,
( v6250(sK5142_VarCurr,bitIndex12)
| v8157(sK5142_VarCurr,bitIndex12)
| ~ sP5291 ),
inference(cnf_transformation,[],[f36250]) ).
tcf(c_40442,plain,
( ~ sP5292
| ~ v6250(sK5142_VarCurr,bitIndex11)
| ~ v8157(sK5142_VarCurr,bitIndex11) ),
inference(cnf_transformation,[],[f36253]) ).
tcf(c_40443,plain,
( v6250(sK5142_VarCurr,bitIndex11)
| v8157(sK5142_VarCurr,bitIndex11)
| ~ sP5292 ),
inference(cnf_transformation,[],[f36252]) ).
tcf(c_40444,plain,
( ~ sP5293
| ~ v6250(sK5142_VarCurr,bitIndex10)
| ~ v8157(sK5142_VarCurr,bitIndex10) ),
inference(cnf_transformation,[],[f36255]) ).
tcf(c_40445,plain,
( v6250(sK5142_VarCurr,bitIndex10)
| v8157(sK5142_VarCurr,bitIndex10)
| ~ sP5293 ),
inference(cnf_transformation,[],[f36254]) ).
tcf(c_40446,plain,
( ~ sP5294
| ~ v6250(sK5142_VarCurr,bitIndex9)
| ~ v8157(sK5142_VarCurr,bitIndex9) ),
inference(cnf_transformation,[],[f36257]) ).
tcf(c_40447,plain,
( v6250(sK5142_VarCurr,bitIndex9)
| v8157(sK5142_VarCurr,bitIndex9)
| ~ sP5294 ),
inference(cnf_transformation,[],[f36256]) ).
tcf(c_40448,plain,
( ~ sP5295
| ~ v6250(sK5142_VarCurr,bitIndex8)
| ~ v8157(sK5142_VarCurr,bitIndex8) ),
inference(cnf_transformation,[],[f36259]) ).
tcf(c_40449,plain,
( v6250(sK5142_VarCurr,bitIndex8)
| v8157(sK5142_VarCurr,bitIndex8)
| ~ sP5295 ),
inference(cnf_transformation,[],[f36258]) ).
tcf(c_40450,plain,
( ~ sP5296
| ~ v6250(sK5142_VarCurr,bitIndex7)
| ~ v8157(sK5142_VarCurr,bitIndex7) ),
inference(cnf_transformation,[],[f36261]) ).
tcf(c_40451,plain,
( v6250(sK5142_VarCurr,bitIndex7)
| v8157(sK5142_VarCurr,bitIndex7)
| ~ sP5296 ),
inference(cnf_transformation,[],[f36260]) ).
tcf(c_40452,plain,
( ~ sP5297
| ~ v6250(sK5142_VarCurr,bitIndex6)
| ~ v8157(sK5142_VarCurr,bitIndex6) ),
inference(cnf_transformation,[],[f36263]) ).
tcf(c_40453,plain,
( v6250(sK5142_VarCurr,bitIndex6)
| v8157(sK5142_VarCurr,bitIndex6)
| ~ sP5297 ),
inference(cnf_transformation,[],[f36262]) ).
tcf(c_40454,plain,
( ~ sP5298
| ~ v6250(sK5142_VarCurr,bitIndex5)
| ~ v8157(sK5142_VarCurr,bitIndex5) ),
inference(cnf_transformation,[],[f36265]) ).
tcf(c_40455,plain,
( v6250(sK5142_VarCurr,bitIndex5)
| v8157(sK5142_VarCurr,bitIndex5)
| ~ sP5298 ),
inference(cnf_transformation,[],[f36264]) ).
tcf(c_40456,plain,
( ~ sP5299
| ~ v6250(sK5142_VarCurr,bitIndex4)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(cnf_transformation,[],[f36267]) ).
tcf(c_40457,plain,
( v6250(sK5142_VarCurr,bitIndex4)
| v8157(sK5142_VarCurr,bitIndex4)
| ~ sP5299 ),
inference(cnf_transformation,[],[f36266]) ).
tcf(c_40458,plain,
( ~ sP5300
| ~ v6250(sK5142_VarCurr,bitIndex3)
| ~ v8157(sK5142_VarCurr,bitIndex3) ),
inference(cnf_transformation,[],[f36269]) ).
tcf(c_40459,plain,
( v6250(sK5142_VarCurr,bitIndex3)
| v8157(sK5142_VarCurr,bitIndex3)
| ~ sP5300 ),
inference(cnf_transformation,[],[f36268]) ).
tcf(c_40464,plain,
! [X0: $i] :
( ~ sP22_aig_name(X0)
| ~ v69(X0) ),
inference(cnf_transformation,[],[f628]) ).
tcf(c_40468,plain,
! [X0: $i] :
( ~ v21(X0)
| ~ v23(X0)
| ~ sP22_aig_name(X0) ),
inference(cnf_transformation,[],[f629]) ).
tcf(c_40528,plain,
! [X0: $i,X1: $i] :
( v614(X0)
| v8161(X0,X1)
| ~ v81(X0)
| ~ v8162(X0,X1) ),
inference(cnf_transformation,[],[f35839]) ).
tcf(c_40529,plain,
! [X0: $i,X1: $i] :
( v614(X0)
| v8162(X0,X1)
| ~ v81(X0)
| ~ v8161(X0,X1) ),
inference(cnf_transformation,[],[f35838]) ).
tcf(c_42178,plain,
! [X0: $i,X1: $i] :
( sP22_aig_name(X0)
| v6250(X0,X1)
| ~ v8161(X0,X1) ),
inference(cnf_transformation,[],[f35843]) ).
tcf(c_42179,plain,
! [X0: $i,X1: $i] :
( sP22_aig_name(X0)
| v8161(X0,X1)
| ~ v6250(X0,X1) ),
inference(cnf_transformation,[],[f35842]) ).
tcf(c_42366,plain,
! [X0: $i,X1: $i] :
( ~ v614(X0)
| ~ v8161(X0,X1) ),
inference(cnf_transformation,[],[f35841]) ).
tcf(c_42367,plain,
! [X0: $i,X1: $i] :
( v81(X0)
| ~ v8161(X0,X1) ),
inference(cnf_transformation,[],[f35840]) ).
tcf(c_57628,plain,
! [X0: $i,X1: $i] :
( v8162(X0,X1)
| ~ v8161(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_40529,c_42366,c_42367]) ).
tcf(c_65130,plain,
! [X0: $i] :
( v21(sK5142_VarCurr)
| ~ sP22_aig_name(X0)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_40464,c_40330]) ).
tcf(c_65131,plain,
( v21(sK5142_VarCurr)
| ~ sP22_aig_name(sK5142_VarCurr) ),
inference(unflattening,[status(thm)],[c_65130]) ).
tcf(c_65138,plain,
! [X0: $i] :
( v23(sK5142_VarCurr)
| ~ sP22_aig_name(X0)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_40464,c_40329]) ).
tcf(c_65139,plain,
( v23(sK5142_VarCurr)
| ~ sP22_aig_name(sK5142_VarCurr) ),
inference(unflattening,[status(thm)],[c_65138]) ).
tcf(c_65508,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP22_aig_name(X0)
| v8162(X1,X3)
| ~ v6250(X0,X2)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_42179,c_57628]) ).
tcf(c_65509,plain,
! [X0: $i,X1: $i] :
( sP22_aig_name(X0)
| v8162(X0,X1)
| ~ v6250(X0,X1) ),
inference(unflattening,[status(thm)],[c_65508]) ).
tcf(c_65548,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v614(X0)
| sP22_aig_name(X1)
| v6250(X1,X3)
| ~ v81(X0)
| ~ v8162(X0,X2)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_40528,c_42178]) ).
tcf(c_65549,plain,
! [X0: $i,X1: $i] :
( v614(X0)
| sP22_aig_name(X0)
| v6250(X0,X1)
| ~ v81(X0)
| ~ v8162(X0,X1) ),
inference(unflattening,[status(thm)],[c_65548]) ).
tcf(c_67455,plain,
! [X0: $i] :
( ~ sP22_aig_name(sK5142_VarCurr)
| ~ v23(X0)
| ~ sP22_aig_name(X0)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_40468,c_65131]) ).
tcf(c_67456,plain,
( ~ v23(sK5142_VarCurr)
| ~ sP22_aig_name(sK5142_VarCurr) ),
inference(unflattening,[status(thm)],[c_67455]) ).
tcf(c_67457,plain,
~ sP22_aig_name(sK5142_VarCurr),
inference(global_subsumption_just,[status(thm)],[c_67456,c_65139,c_67456]) ).
tcf(c_68016,plain,
! [X0: $i,X1: $i] :
( v614(X0)
| v6250(X0,X1)
| ~ v81(X0)
| ~ v8162(X0,X1)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_65549,c_67457]) ).
tcf(c_68017,plain,
! [X0: $i] :
( v614(sK5142_VarCurr)
| v6250(sK5142_VarCurr,X0)
| ~ v81(sK5142_VarCurr)
| ~ v8162(sK5142_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_68016]) ).
tcf(c_68019,plain,
! [X0: $i] :
( ~ v8162(sK5142_VarCurr,X0)
| v6250(sK5142_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_68017,c_40318,c_40319,c_68017]) ).
tcf(c_68020,plain,
! [X0: $i] :
( v6250(sK5142_VarCurr,X0)
| ~ v8162(sK5142_VarCurr,X0) ),
inference(renaming,[status(thm)],[c_68019]) ).
tcf(c_68032,plain,
! [X0: $i,X1: $i] :
( v8162(X0,X1)
| ~ v6250(X0,X1)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_65509,c_67457]) ).
tcf(c_68033,plain,
! [X0: $i] :
( v8162(sK5142_VarCurr,X0)
| ~ v6250(sK5142_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_68032]) ).
tcf(c_68034,plain,
( v8162(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex0) ),
inference(instantiation,[status(thm)],[c_68033]) ).
tcf(c_70513,plain,
! [X0: $i,X1: $i] :
( v8157(X0,X1)
| ~ v8162(X0,X1)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_40342,c_40320]) ).
tcf(c_70514,plain,
! [X0: $i] :
( v8157(sK5142_VarCurr,X0)
| ~ v8162(sK5142_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_70513]) ).
tcf(c_70515,plain,
( v8157(sK5142_VarCurr,bitIndex0)
| ~ v8162(sK5142_VarCurr,bitIndex0) ),
inference(instantiation,[status(thm)],[c_70514]) ).
tcf(c_92517,plain,
! [X0: $i,X1: $i] :
( v614(X0)
| sP22_aig_name(X0)
| v6250(X0,X1)
| ~ v8162(X0,X1)
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_65549,c_40318]) ).
tcf(c_92518,plain,
! [X0: $i] :
( v614(sK5142_VarCurr)
| sP22_aig_name(sK5142_VarCurr)
| v6250(sK5142_VarCurr,X0)
| ~ v8162(sK5142_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_92517]) ).
tcf(c_92520,plain,
! [X0: $i] :
( v6250(sK5142_VarCurr,X0)
| ~ v8162(sK5142_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_92518,c_68020]) ).
tcf(c_92832,plain,
! [X0: $i,X1: $i,X2: $i] :
( v8163(X0)
| v6250(sK5142_VarCurr,X2)
| ~ v8157(X0,X1)
| ( X1 != X2 )
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_40341,c_92520]) ).
tcf(c_92833,plain,
! [X0: $i] :
( v8163(sK5142_VarCurr)
| v6250(sK5142_VarCurr,X0)
| ~ v8157(sK5142_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_92832]) ).
tcf(c_92835,plain,
! [X0: $i] :
( ~ v8157(sK5142_VarCurr,X0)
| v6250(sK5142_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_92833,c_40320,c_92833]) ).
tcf(c_92836,plain,
! [X0: $i] :
( v6250(sK5142_VarCurr,X0)
| ~ v8157(sK5142_VarCurr,X0) ),
inference(renaming,[status(thm)],[c_92835]) ).
tcf(c_92837,plain,
( v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
inference(instantiation,[status(thm)],[c_92836]) ).
tcf(c_92863,plain,
( v6250(sK5142_VarCurr,bitIndex42)
| ~ sP5261 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40381,c_92836]) ).
tcf(c_92864,plain,
( v6250(sK5142_VarCurr,bitIndex10)
| ~ sP5293 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40445,c_92836]) ).
tcf(c_92865,plain,
( v6250(sK5142_VarCurr,bitIndex58)
| ~ sP5245 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40349,c_92836]) ).
tcf(c_92866,plain,
( v6250(sK5142_VarCurr,bitIndex16)
| ~ sP5287 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40433,c_92836]) ).
tcf(c_92867,plain,
( v6250(sK5142_VarCurr,bitIndex37)
| ~ sP5266 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40391,c_92836]) ).
tcf(c_92868,plain,
( v6250(sK5142_VarCurr,bitIndex34)
| ~ sP5269 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40397,c_92836]) ).
tcf(c_92869,plain,
( v6250(sK5142_VarCurr,bitIndex20)
| ~ sP5283 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40425,c_92836]) ).
tcf(c_92870,plain,
( v6250(sK5142_VarCurr,bitIndex9)
| ~ sP5294 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40447,c_92836]) ).
tcf(c_92871,plain,
( v6250(sK5142_VarCurr,bitIndex49)
| ~ sP5254 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40367,c_92836]) ).
tcf(c_92872,plain,
( v6250(sK5142_VarCurr,bitIndex46)
| ~ sP5257 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40373,c_92836]) ).
tcf(c_92873,plain,
( v6250(sK5142_VarCurr,bitIndex53)
| ~ sP5250 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40359,c_92836]) ).
tcf(c_92874,plain,
( v6250(sK5142_VarCurr,bitIndex14)
| ~ sP5289 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40437,c_92836]) ).
tcf(c_92875,plain,
( v6250(sK5142_VarCurr,bitIndex30)
| ~ sP5273 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40405,c_92836]) ).
tcf(c_92876,plain,
( v6250(sK5142_VarCurr,bitIndex29)
| ~ sP5274 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40407,c_92836]) ).
tcf(c_92877,plain,
( v6250(sK5142_VarCurr,bitIndex22)
| ~ sP5281 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40421,c_92836]) ).
tcf(c_92878,plain,
( v6250(sK5142_VarCurr,bitIndex56)
| ~ sP5247 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40353,c_92836]) ).
tcf(c_92879,plain,
( v6250(sK5142_VarCurr,bitIndex19)
| ~ sP5284 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40427,c_92836]) ).
tcf(c_92880,plain,
( v6250(sK5142_VarCurr,bitIndex3)
| ~ sP5300 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40459,c_92836]) ).
tcf(c_92881,plain,
( v6250(sK5142_VarCurr,bitIndex51)
| ~ sP5252 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40363,c_92836]) ).
tcf(c_92882,plain,
( v6250(sK5142_VarCurr,bitIndex36)
| ~ sP5267 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40393,c_92836]) ).
tcf(c_92883,plain,
( v6250(sK5142_VarCurr,bitIndex28)
| ~ sP5275 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40409,c_92836]) ).
tcf(c_92884,plain,
( v6250(sK5142_VarCurr,bitIndex12)
| ~ sP5291 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40441,c_92836]) ).
tcf(c_92885,plain,
( v6250(sK5142_VarCurr,bitIndex41)
| ~ sP5262 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40383,c_92836]) ).
tcf(c_92886,plain,
( v6250(sK5142_VarCurr,bitIndex43)
| ~ sP5260 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40379,c_92836]) ).
tcf(c_92887,plain,
( v6250(sK5142_VarCurr,bitIndex17)
| ~ sP5286 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40431,c_92836]) ).
tcf(c_92888,plain,
( v6250(sK5142_VarCurr,bitIndex35)
| ~ sP5268 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40395,c_92836]) ).
tcf(c_92889,plain,
( v6250(sK5142_VarCurr,bitIndex25)
| ~ sP5278 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40415,c_92836]) ).
tcf(c_92890,plain,
( v6250(sK5142_VarCurr,bitIndex55)
| ~ sP5248 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40355,c_92836]) ).
tcf(c_92891,plain,
( v6250(sK5142_VarCurr,bitIndex15)
| ~ sP5288 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40435,c_92836]) ).
tcf(c_92892,plain,
( v6250(sK5142_VarCurr,bitIndex33)
| ~ sP5270 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40399,c_92836]) ).
tcf(c_92893,plain,
( v6250(sK5142_VarCurr,bitIndex23)
| ~ sP5280 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40419,c_92836]) ).
tcf(c_92894,plain,
( v6250(sK5142_VarCurr,bitIndex45)
| ~ sP5258 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40375,c_92836]) ).
tcf(c_92895,plain,
( v6250(sK5142_VarCurr,bitIndex39)
| ~ sP5264 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40387,c_92836]) ).
tcf(c_92896,plain,
( v6250(sK5142_VarCurr,bitIndex47)
| ~ sP5256 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40371,c_92836]) ).
tcf(c_92897,plain,
( v6250(sK5142_VarCurr,bitIndex31)
| ~ sP5272 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40403,c_92836]) ).
tcf(c_92898,plain,
( v6250(sK5142_VarCurr,bitIndex24)
| ~ sP5279 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40417,c_92836]) ).
tcf(c_92899,plain,
( v6250(sK5142_VarCurr,bitIndex7)
| ~ sP5296 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40451,c_92836]) ).
tcf(c_92900,plain,
( v6250(sK5142_VarCurr,bitIndex21)
| ~ sP5282 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40423,c_92836]) ).
tcf(c_92901,plain,
( v6250(sK5142_VarCurr,bitIndex59)
| ~ sP5244 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40347,c_92836]) ).
tcf(c_92902,plain,
( v6250(sK5142_VarCurr,bitIndex38)
| ~ sP5265 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40389,c_92836]) ).
tcf(c_92903,plain,
( v6250(sK5142_VarCurr,bitIndex6)
| ~ sP5297 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40453,c_92836]) ).
tcf(c_92904,plain,
( v6250(sK5142_VarCurr,bitIndex54)
| ~ sP5249 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40357,c_92836]) ).
tcf(c_92905,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex0)
| v8157(sK5142_VarCurr,bitIndex2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40321,c_92836]) ).
tcf(c_92906,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40325,c_92836]) ).
tcf(c_92907,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40322,c_92836]) ).
tcf(c_92908,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40326,c_92836]) ).
tcf(c_92909,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| v6250(sK5142_VarCurr,bitIndex2)
| v8157(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40323,c_92836]) ).
tcf(c_92910,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40327,c_92836]) ).
tcf(c_92911,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40324,c_92836]) ).
tcf(c_92912,plain,
( v6250(sK5142_VarCurr,bitIndex18)
| ~ sP5285 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40429,c_92836]) ).
tcf(c_92913,plain,
( v6250(sK5142_VarCurr,bitIndex26)
| ~ sP5277 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40413,c_92836]) ).
tcf(c_92914,plain,
( v6250(sK5142_VarCurr,bitIndex50)
| ~ sP5253 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40365,c_92836]) ).
tcf(c_92915,plain,
( v6250(sK5142_VarCurr,bitIndex27)
| ~ sP5276 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40411,c_92836]) ).
tcf(c_92916,plain,
( v6250(sK5142_VarCurr,bitIndex11)
| ~ sP5292 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40443,c_92836]) ).
tcf(c_92917,plain,
( v6250(sK5142_VarCurr,bitIndex57)
| ~ sP5246 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40351,c_92836]) ).
tcf(c_92918,plain,
( v6250(sK5142_VarCurr,bitIndex48)
| ~ sP5255 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40369,c_92836]) ).
tcf(c_92919,plain,
( v6250(sK5142_VarCurr,bitIndex44)
| ~ sP5259 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40377,c_92836]) ).
tcf(c_92920,plain,
( v6250(sK5142_VarCurr,bitIndex8)
| ~ sP5295 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40449,c_92836]) ).
tcf(c_92921,plain,
( v6250(sK5142_VarCurr,bitIndex40)
| ~ sP5263 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40385,c_92836]) ).
tcf(c_92922,plain,
( v6250(sK5142_VarCurr,bitIndex4)
| ~ sP5299 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40457,c_92836]) ).
tcf(c_92923,plain,
( v6250(sK5142_VarCurr,bitIndex5)
| ~ sP5298 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40455,c_92836]) ).
tcf(c_92924,plain,
( v6250(sK5142_VarCurr,bitIndex52)
| ~ sP5251 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40361,c_92836]) ).
tcf(c_92925,plain,
( v6250(sK5142_VarCurr,bitIndex32)
| ~ sP5271 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40401,c_92836]) ).
tcf(c_92926,plain,
( v6250(sK5142_VarCurr,bitIndex13)
| ~ sP5290 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40439,c_92836]) ).
tcf(c_92928,plain,
( ~ sP5245
| ~ v8157(sK5142_VarCurr,bitIndex58) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40348,c_92836]) ).
tcf(c_92929,plain,
( ~ sP5261
| ~ v8157(sK5142_VarCurr,bitIndex42) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40380,c_92836]) ).
tcf(c_92930,plain,
( ~ sP5293
| ~ v8157(sK5142_VarCurr,bitIndex10) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40444,c_92836]) ).
tcf(c_92931,plain,
( ~ sP5287
| ~ v8157(sK5142_VarCurr,bitIndex16) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40432,c_92836]) ).
tcf(c_92932,plain,
( ~ sP5266
| ~ v8157(sK5142_VarCurr,bitIndex37) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40390,c_92836]) ).
tcf(c_92933,plain,
( ~ sP5269
| ~ v8157(sK5142_VarCurr,bitIndex34) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40396,c_92836]) ).
tcf(c_92934,plain,
( ~ sP5283
| ~ v8157(sK5142_VarCurr,bitIndex20) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40424,c_92836]) ).
tcf(c_92935,plain,
( ~ sP5254
| ~ v8157(sK5142_VarCurr,bitIndex49) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40366,c_92836]) ).
tcf(c_92936,plain,
( ~ sP5294
| ~ v8157(sK5142_VarCurr,bitIndex9) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40446,c_92836]) ).
tcf(c_92937,plain,
( ~ sP5250
| ~ v8157(sK5142_VarCurr,bitIndex53) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40358,c_92836]) ).
tcf(c_92938,plain,
( ~ sP5289
| ~ v8157(sK5142_VarCurr,bitIndex14) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40436,c_92836]) ).
tcf(c_92939,plain,
( ~ sP5257
| ~ v8157(sK5142_VarCurr,bitIndex46) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40372,c_92836]) ).
tcf(c_92940,plain,
( ~ sP5273
| ~ v8157(sK5142_VarCurr,bitIndex30) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40404,c_92836]) ).
tcf(c_92941,plain,
( ~ sP5274
| ~ v8157(sK5142_VarCurr,bitIndex29) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40406,c_92836]) ).
tcf(c_92942,plain,
( ~ sP5281
| ~ v8157(sK5142_VarCurr,bitIndex22) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40420,c_92836]) ).
tcf(c_92943,plain,
( ~ sP5247
| ~ v8157(sK5142_VarCurr,bitIndex56) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40352,c_92836]) ).
tcf(c_92944,plain,
( ~ sP5284
| ~ v8157(sK5142_VarCurr,bitIndex19) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40426,c_92836]) ).
tcf(c_92945,plain,
( ~ sP5300
| ~ v8157(sK5142_VarCurr,bitIndex3) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40458,c_92836]) ).
tcf(c_92946,plain,
( ~ sP5252
| ~ v8157(sK5142_VarCurr,bitIndex51) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40362,c_92836]) ).
tcf(c_92947,plain,
( ~ sP5267
| ~ v8157(sK5142_VarCurr,bitIndex36) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40392,c_92836]) ).
tcf(c_92948,plain,
( ~ sP5275
| ~ v8157(sK5142_VarCurr,bitIndex28) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40408,c_92836]) ).
tcf(c_92949,plain,
( ~ sP5291
| ~ v8157(sK5142_VarCurr,bitIndex12) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40440,c_92836]) ).
tcf(c_92950,plain,
( ~ sP5260
| ~ v8157(sK5142_VarCurr,bitIndex43) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40378,c_92836]) ).
tcf(c_92951,plain,
( ~ sP5262
| ~ v8157(sK5142_VarCurr,bitIndex41) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40382,c_92836]) ).
tcf(c_92952,plain,
( ~ sP5286
| ~ v8157(sK5142_VarCurr,bitIndex17) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40430,c_92836]) ).
tcf(c_92953,plain,
( ~ sP5268
| ~ v8157(sK5142_VarCurr,bitIndex35) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40394,c_92836]) ).
tcf(c_92954,plain,
( ~ sP5278
| ~ v8157(sK5142_VarCurr,bitIndex25) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40414,c_92836]) ).
tcf(c_92955,plain,
( ~ sP5248
| ~ v8157(sK5142_VarCurr,bitIndex55) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40354,c_92836]) ).
tcf(c_92956,plain,
( ~ sP5288
| ~ v8157(sK5142_VarCurr,bitIndex15) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40434,c_92836]) ).
tcf(c_92957,plain,
( ~ sP5270
| ~ v8157(sK5142_VarCurr,bitIndex33) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40398,c_92836]) ).
tcf(c_92958,plain,
( ~ sP5280
| ~ v8157(sK5142_VarCurr,bitIndex23) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40418,c_92836]) ).
tcf(c_92959,plain,
( ~ sP5256
| ~ v8157(sK5142_VarCurr,bitIndex47) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40370,c_92836]) ).
tcf(c_92960,plain,
( ~ sP5258
| ~ v8157(sK5142_VarCurr,bitIndex45) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40374,c_92836]) ).
tcf(c_92961,plain,
( ~ sP5264
| ~ v8157(sK5142_VarCurr,bitIndex39) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40386,c_92836]) ).
tcf(c_92962,plain,
( ~ sP5272
| ~ v8157(sK5142_VarCurr,bitIndex31) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40402,c_92836]) ).
tcf(c_92963,plain,
( ~ sP5279
| ~ v8157(sK5142_VarCurr,bitIndex24) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40416,c_92836]) ).
tcf(c_92964,plain,
( ~ sP5296
| ~ v8157(sK5142_VarCurr,bitIndex7) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40450,c_92836]) ).
tcf(c_92965,plain,
( ~ sP5282
| ~ v8157(sK5142_VarCurr,bitIndex21) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40422,c_92836]) ).
tcf(c_92966,plain,
( ~ sP5244
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40346,c_92836]) ).
tcf(c_92967,plain,
( ~ sP5249
| ~ v8157(sK5142_VarCurr,bitIndex54) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40356,c_92836]) ).
tcf(c_92968,plain,
( ~ sP5265
| ~ v8157(sK5142_VarCurr,bitIndex38) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40388,c_92836]) ).
tcf(c_92969,plain,
( ~ sP5297
| ~ v8157(sK5142_VarCurr,bitIndex6) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40452,c_92836]) ).
tcf(c_92970,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| sP5244
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40328,c_92836]) ).
tcf(c_92971,plain,
( ~ sP5277
| ~ v8157(sK5142_VarCurr,bitIndex26) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40412,c_92836]) ).
tcf(c_92972,plain,
( ~ sP5285
| ~ v8157(sK5142_VarCurr,bitIndex18) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40428,c_92836]) ).
tcf(c_92973,plain,
( ~ sP5253
| ~ v8157(sK5142_VarCurr,bitIndex50) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40364,c_92836]) ).
tcf(c_92974,plain,
( ~ sP5276
| ~ v8157(sK5142_VarCurr,bitIndex27) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40410,c_92836]) ).
tcf(c_92975,plain,
( ~ sP5292
| ~ v8157(sK5142_VarCurr,bitIndex11) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40442,c_92836]) ).
tcf(c_92976,plain,
( ~ sP5246
| ~ v8157(sK5142_VarCurr,bitIndex57) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40350,c_92836]) ).
tcf(c_92977,plain,
( ~ sP5255
| ~ v8157(sK5142_VarCurr,bitIndex48) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40368,c_92836]) ).
tcf(c_92978,plain,
( ~ sP5251
| ~ v8157(sK5142_VarCurr,bitIndex52) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40360,c_92836]) ).
tcf(c_92979,plain,
( ~ sP5259
| ~ v8157(sK5142_VarCurr,bitIndex44) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40376,c_92836]) ).
tcf(c_92980,plain,
( ~ sP5295
| ~ v8157(sK5142_VarCurr,bitIndex8) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40448,c_92836]) ).
tcf(c_92981,plain,
( ~ sP5263
| ~ v8157(sK5142_VarCurr,bitIndex40) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40384,c_92836]) ).
tcf(c_92982,plain,
( ~ sP5299
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40456,c_92836]) ).
tcf(c_92983,plain,
( ~ sP5298
| ~ v8157(sK5142_VarCurr,bitIndex5) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40454,c_92836]) ).
tcf(c_92984,plain,
( ~ sP5271
| ~ v8157(sK5142_VarCurr,bitIndex32) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40400,c_92836]) ).
tcf(c_92985,plain,
( ~ sP5290
| ~ v8157(sK5142_VarCurr,bitIndex13) ),
inference(backward_subsumption_resolution,[status(thm)],[c_40438,c_92836]) ).
tcf(c_93830,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_92970,c_92966]) ).
tcf(c_93831,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_93830,c_68034,c_70515,c_93830]) ).
tcf(c_93832,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_93831]) ).
tcf(c_93833,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_93832,c_92837,c_92911,c_92907,c_92966,c_93832]) ).
tcf(c_93834,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_93833]) ).
tcf(c_93955,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_92970,c_92901]) ).
tcf(c_93956,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_93955,c_68034,c_70515,c_92901,c_92970]) ).
tcf(c_93957,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_93956]) ).
tcf(c_93958,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_93957,c_92837,c_92911,c_92907,c_92901,c_93957]) ).
tcf(c_93959,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_93958]) ).
tcf(c_94086,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_92910,c_92966]) ).
tcf(c_94087,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_94086,c_68034,c_70515,c_94086]) ).
tcf(c_94089,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_94087,c_92837,c_92909,c_92966,c_94087]) ).
tcf(c_94090,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_94089]) ).
tcf(c_94211,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_92910,c_92901]) ).
tcf(c_94212,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_94211,c_68034,c_70515,c_94211]) ).
tcf(c_94214,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_94212,c_92837,c_92909,c_92901,c_94212]) ).
tcf(c_94215,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_94214]) ).
tcf(c_94342,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(resolution,[status(thm)],[c_92908,c_92966]) ).
tcf(c_94343,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_94342,c_68034,c_70515,c_92908,c_92966]) ).
tcf(c_94345,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_94343,c_40322,c_92837,c_92966,c_93834,c_94343]) ).
tcf(c_94346,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(renaming,[status(thm)],[c_94345]) ).
tcf(c_94467,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(resolution,[status(thm)],[c_92908,c_92901]) ).
tcf(c_94468,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_94467,c_68034,c_70515,c_92908,c_92901]) ).
tcf(c_94470,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_94468,c_40322,c_92837,c_92911,c_92907,c_92901,c_93957,c_94468]) ).
tcf(c_94471,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(renaming,[status(thm)],[c_94470]) ).
tcf(c_94598,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
inference(resolution,[status(thm)],[c_92906,c_92966]) ).
tcf(c_94599,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
inference(global_subsumption_just,[status(thm)],[c_94598,c_68034,c_70515,c_92906,c_92966]) ).
tcf(c_94601,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
inference(global_subsumption_just,[status(thm)],[c_94599,c_92837,c_92905,c_92966,c_94599]) ).
tcf(c_94723,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0)
| ~ v8157(sK5142_VarCurr,bitIndex0) ),
inference(resolution,[status(thm)],[c_92906,c_92901]) ).
tcf(c_94724,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex0) ),
inference(global_subsumption_just,[status(thm)],[c_94723,c_68034,c_70515,c_92906,c_92901]) ).
tcf(c_94726,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v8157(sK5142_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_94724,c_92837,c_92905,c_92901,c_94724]) ).
tcf(c_199882,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_94471,c_92982]) ).
tcf(c_200003,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(resolution,[status(thm)],[c_94471,c_92922]) ).
tcf(c_200124,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_94346,c_92982]) ).
tcf(c_200245,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2) ),
inference(resolution,[status(thm)],[c_94346,c_92922]) ).
tcf(c_200366,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_94215,c_92982]) ).
tcf(c_200487,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_94215,c_92922]) ).
tcf(c_200850,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_93959,c_92982]) ).
tcf(c_200971,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_93959,c_92922]) ).
tcf(c_201092,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_93834,c_92982]) ).
tcf(c_201213,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_93834,c_92922]) ).
tcf(c_205110,plain,
! [X0: $i,X1: $i,X2: $i] :
( v8163(X0)
| v6250(sK5142_VarCurr,X2)
| ~ v8157(X0,X1)
| ( X1 != X2 )
| ( X0 != sK5142_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_40341,c_92520]) ).
tcf(c_205111,plain,
! [X0: $i] :
( v8163(sK5142_VarCurr)
| v6250(sK5142_VarCurr,X0)
| ~ v8157(sK5142_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_205110]) ).
tcf(c_205112,plain,
! [X0: $i] :
( ~ v8157(sK5142_VarCurr,X0)
| v6250(sK5142_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_205111,c_40320,c_92833]) ).
tcf(c_205113,plain,
! [X0: $i] :
( v6250(sK5142_VarCurr,X0)
| ~ v8157(sK5142_VarCurr,X0) ),
inference(renaming,[status(thm)],[c_205112]) ).
tcf(c_205139,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
inference(backward_subsumption_resolution,[status(thm)],[c_94601,c_205113]) ).
tcf(c_205140,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_94726,c_205113]) ).
tcf(c_205144,plain,
( sP5300
| sP5299
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_94090,c_205113]) ).
tcf(c_309482,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_205144,c_92982]) ).
tcf(c_309601,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_205144,c_92922]) ).
tcf(c_310196,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_205140,c_92982]) ).
tcf(c_310315,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex59)
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_205140,c_92922]) ).
tcf(c_310434,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| ~ v8157(sK5142_VarCurr,bitIndex59)
| ~ v8157(sK5142_VarCurr,bitIndex4) ),
inference(resolution,[status(thm)],[c_205139,c_92982]) ).
tcf(c_310553,plain,
( sP5300
| sP5298
| sP5297
| sP5296
| sP5295
| sP5294
| sP5293
| sP5292
| sP5291
| sP5290
| sP5289
| sP5288
| sP5287
| sP5286
| sP5285
| sP5284
| sP5283
| sP5282
| sP5281
| sP5280
| sP5279
| sP5278
| sP5277
| sP5276
| sP5275
| sP5274
| sP5273
| sP5272
| sP5271
| sP5270
| sP5269
| sP5268
| sP5267
| sP5266
| sP5265
| sP5264
| sP5263
| sP5262
| sP5261
| sP5260
| sP5259
| sP5258
| sP5257
| sP5256
| sP5255
| sP5254
| sP5253
| sP5252
| sP5251
| sP5250
| sP5249
| sP5248
| sP5247
| sP5246
| sP5245
| v6250(sK5142_VarCurr,bitIndex2)
| v6250(sK5142_VarCurr,bitIndex1)
| v6250(sK5142_VarCurr,bitIndex4)
| ~ v8157(sK5142_VarCurr,bitIndex59) ),
inference(resolution,[status(thm)],[c_205139,c_92922]) ).
tcf(c_312704,plain,
! [X0_iProver_nextState_2: iProver_nextState_2,X0_iProver_v8157_2: iProver_v8157_2] :
( sP22_aig_name(X0_iProver_nextState_2)
| v8162(X0_iProver_nextState_2,X0_iProver_v8157_2)
| ~ v6250(X0_iProver_nextState_2,X0_iProver_v8157_2) ),
inference(subtyping,[status(esa)],[c_65509]) ).
tcf(c_312754,plain,
! [X0_iProver_nextState_2: iProver_nextState_2,X0_iProver_v8157_2: iProver_v8157_2] :
( v8163(X0_iProver_nextState_2)
| v8157(X0_iProver_nextState_2,X0_iProver_v8157_2)
| ~ v8162(X0_iProver_nextState_2,X0_iProver_v8157_2) ),
inference(subtyping,[status(esa)],[c_40342]) ).
tcf(c_312771,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex3)
| ~ v6250(sK5142_VarCurr,bitIndex3) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_312820,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex4)
| ~ v6250(sK5142_VarCurr,bitIndex4) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_312928,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex4)
| ~ v8162(sK5142_VarCurr,bitIndex4) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_312947,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex5)
| ~ v6250(sK5142_VarCurr,bitIndex5) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313127,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex5)
| ~ v8162(sK5142_VarCurr,bitIndex5) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313304,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex6)
| ~ v6250(sK5142_VarCurr,bitIndex6) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313388,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex6)
| ~ v8162(sK5142_VarCurr,bitIndex6) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313421,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex7)
| ~ v6250(sK5142_VarCurr,bitIndex7) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313437,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex7)
| ~ v8162(sK5142_VarCurr,bitIndex7) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313460,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex8)
| ~ v6250(sK5142_VarCurr,bitIndex8) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313464,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex8)
| ~ v8162(sK5142_VarCurr,bitIndex8) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313503,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex9)
| ~ v6250(sK5142_VarCurr,bitIndex9) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313519,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex9)
| ~ v8162(sK5142_VarCurr,bitIndex9) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313556,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex10)
| ~ v6250(sK5142_VarCurr,bitIndex10) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313572,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex10)
| ~ v8162(sK5142_VarCurr,bitIndex10) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313609,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex11)
| ~ v6250(sK5142_VarCurr,bitIndex11) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313625,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex11)
| ~ v8162(sK5142_VarCurr,bitIndex11) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313666,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex12)
| ~ v6250(sK5142_VarCurr,bitIndex12) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313682,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex12)
| ~ v8162(sK5142_VarCurr,bitIndex12) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313725,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex13)
| ~ v6250(sK5142_VarCurr,bitIndex13) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313741,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex13)
| ~ v8162(sK5142_VarCurr,bitIndex13) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313786,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex14)
| ~ v6250(sK5142_VarCurr,bitIndex14) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313802,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex14)
| ~ v8162(sK5142_VarCurr,bitIndex14) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313849,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex15)
| ~ v6250(sK5142_VarCurr,bitIndex15) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313865,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex15)
| ~ v8162(sK5142_VarCurr,bitIndex15) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_313912,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex16)
| ~ v6250(sK5142_VarCurr,bitIndex16) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313928,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex17)
| ~ v6250(sK5142_VarCurr,bitIndex17) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_313956,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex17)
| ~ v8162(sK5142_VarCurr,bitIndex17) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314028,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex18)
| ~ v6250(sK5142_VarCurr,bitIndex18) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314236,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex18)
| ~ v8162(sK5142_VarCurr,bitIndex18) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314396,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex19)
| ~ v6250(sK5142_VarCurr,bitIndex19) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314473,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex19)
| ~ v8162(sK5142_VarCurr,bitIndex19) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314508,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex20)
| ~ v6250(sK5142_VarCurr,bitIndex20) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314524,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex20)
| ~ v8162(sK5142_VarCurr,bitIndex20) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314549,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex21)
| ~ v6250(sK5142_VarCurr,bitIndex21) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314553,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex21)
| ~ v8162(sK5142_VarCurr,bitIndex21) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314594,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex22)
| ~ v6250(sK5142_VarCurr,bitIndex22) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314610,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex22)
| ~ v8162(sK5142_VarCurr,bitIndex22) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314647,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex23)
| ~ v6250(sK5142_VarCurr,bitIndex23) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314663,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex23)
| ~ v8162(sK5142_VarCurr,bitIndex23) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314704,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex24)
| ~ v6250(sK5142_VarCurr,bitIndex24) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314720,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex24)
| ~ v8162(sK5142_VarCurr,bitIndex24) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314763,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex25)
| ~ v6250(sK5142_VarCurr,bitIndex25) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314776,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex25)
| ~ v8162(sK5142_VarCurr,bitIndex25) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314820,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex26)
| ~ v6250(sK5142_VarCurr,bitIndex26) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314834,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex26)
| ~ v8162(sK5142_VarCurr,bitIndex26) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314879,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex27)
| ~ v6250(sK5142_VarCurr,bitIndex27) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314900,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex27)
| ~ v8162(sK5142_VarCurr,bitIndex27) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_314952,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex28)
| ~ v6250(sK5142_VarCurr,bitIndex28) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_314980,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex28)
| ~ v8162(sK5142_VarCurr,bitIndex28) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315011,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex29)
| ~ v6250(sK5142_VarCurr,bitIndex29) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315033,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex29)
| ~ v8162(sK5142_VarCurr,bitIndex29) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315086,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex30)
| ~ v6250(sK5142_VarCurr,bitIndex30) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315108,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex30)
| ~ v8162(sK5142_VarCurr,bitIndex30) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315135,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex31)
| ~ v6250(sK5142_VarCurr,bitIndex31) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315149,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex31)
| ~ v8162(sK5142_VarCurr,bitIndex31) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315163,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex32)
| ~ v6250(sK5142_VarCurr,bitIndex32) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315165,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex32)
| ~ v8162(sK5142_VarCurr,bitIndex32) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315179,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex33)
| ~ v6250(sK5142_VarCurr,bitIndex33) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315181,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex33)
| ~ v8162(sK5142_VarCurr,bitIndex33) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315195,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex34)
| ~ v6250(sK5142_VarCurr,bitIndex34) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315197,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex34)
| ~ v8162(sK5142_VarCurr,bitIndex34) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315211,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex35)
| ~ v6250(sK5142_VarCurr,bitIndex35) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315213,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex35)
| ~ v8162(sK5142_VarCurr,bitIndex35) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315227,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex36)
| ~ v6250(sK5142_VarCurr,bitIndex36) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315229,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex36)
| ~ v8162(sK5142_VarCurr,bitIndex36) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315243,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex37)
| ~ v6250(sK5142_VarCurr,bitIndex37) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315245,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex37)
| ~ v8162(sK5142_VarCurr,bitIndex37) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315259,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex38)
| ~ v6250(sK5142_VarCurr,bitIndex38) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315261,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex38)
| ~ v8162(sK5142_VarCurr,bitIndex38) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315275,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex39)
| ~ v6250(sK5142_VarCurr,bitIndex39) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315277,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex39)
| ~ v8162(sK5142_VarCurr,bitIndex39) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315291,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex40)
| ~ v6250(sK5142_VarCurr,bitIndex40) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315293,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex40)
| ~ v8162(sK5142_VarCurr,bitIndex40) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315307,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex41)
| ~ v6250(sK5142_VarCurr,bitIndex41) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315309,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex41)
| ~ v8162(sK5142_VarCurr,bitIndex41) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315323,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex42)
| ~ v6250(sK5142_VarCurr,bitIndex42) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315325,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex42)
| ~ v8162(sK5142_VarCurr,bitIndex42) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315340,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex43)
| ~ v6250(sK5142_VarCurr,bitIndex43) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315342,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex43)
| ~ v8162(sK5142_VarCurr,bitIndex43) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315356,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex44)
| ~ v6250(sK5142_VarCurr,bitIndex44) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315358,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex44)
| ~ v8162(sK5142_VarCurr,bitIndex44) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315372,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex45)
| ~ v6250(sK5142_VarCurr,bitIndex45) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315374,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex45)
| ~ v8162(sK5142_VarCurr,bitIndex45) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315388,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex46)
| ~ v6250(sK5142_VarCurr,bitIndex46) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315390,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex46)
| ~ v8162(sK5142_VarCurr,bitIndex46) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315404,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex47)
| ~ v6250(sK5142_VarCurr,bitIndex47) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315406,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex47)
| ~ v8162(sK5142_VarCurr,bitIndex47) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315420,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex48)
| ~ v6250(sK5142_VarCurr,bitIndex48) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315422,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex48)
| ~ v8162(sK5142_VarCurr,bitIndex48) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315436,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex49)
| ~ v6250(sK5142_VarCurr,bitIndex49) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315438,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex49)
| ~ v8162(sK5142_VarCurr,bitIndex49) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315452,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex50)
| ~ v6250(sK5142_VarCurr,bitIndex50) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315454,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex50)
| ~ v8162(sK5142_VarCurr,bitIndex50) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315466,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex51)
| ~ v6250(sK5142_VarCurr,bitIndex51) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315468,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex51)
| ~ v8162(sK5142_VarCurr,bitIndex51) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315482,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex52)
| ~ v6250(sK5142_VarCurr,bitIndex52) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315484,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex52)
| ~ v8162(sK5142_VarCurr,bitIndex52) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315498,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex53)
| ~ v6250(sK5142_VarCurr,bitIndex53) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315500,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex53)
| ~ v8162(sK5142_VarCurr,bitIndex53) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315512,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex54)
| ~ v6250(sK5142_VarCurr,bitIndex54) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315514,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex54)
| ~ v8162(sK5142_VarCurr,bitIndex54) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315528,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex55)
| ~ v6250(sK5142_VarCurr,bitIndex55) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315530,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex55)
| ~ v8162(sK5142_VarCurr,bitIndex55) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315544,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex56)
| ~ v6250(sK5142_VarCurr,bitIndex56) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315546,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex56)
| ~ v8162(sK5142_VarCurr,bitIndex56) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315560,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex57)
| ~ v6250(sK5142_VarCurr,bitIndex57) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315562,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex57)
| ~ v8162(sK5142_VarCurr,bitIndex57) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315574,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex58)
| ~ v6250(sK5142_VarCurr,bitIndex58) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315576,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex58)
| ~ v8162(sK5142_VarCurr,bitIndex58) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315590,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex59)
| ~ v6250(sK5142_VarCurr,bitIndex59) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315592,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex59)
| ~ v8162(sK5142_VarCurr,bitIndex59) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315606,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex1)
| ~ v6250(sK5142_VarCurr,bitIndex1) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315608,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex1)
| ~ v8162(sK5142_VarCurr,bitIndex1) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315619,plain,
( sP22_aig_name(sK5142_VarCurr)
| v8162(sK5142_VarCurr,bitIndex2)
| ~ v6250(sK5142_VarCurr,bitIndex2) ),
inference(instantiation,[status(thm)],[c_312704]) ).
tcf(c_315621,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex2)
| ~ v8162(sK5142_VarCurr,bitIndex2) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315635,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex3)
| ~ v8162(sK5142_VarCurr,bitIndex3) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315668,plain,
( v8163(sK5142_VarCurr)
| v8157(sK5142_VarCurr,bitIndex16)
| ~ v8162(sK5142_VarCurr,bitIndex16) ),
inference(instantiation,[status(thm)],[c_312754]) ).
tcf(c_315697,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_315668,c_315635,c_315621,c_315619,c_315608,c_315606,c_315592,c_315590,c_315576,c_315574,c_315562,c_315560,c_315546,c_315544,c_315530,c_315528,c_315514,c_315512,c_315500,c_315498,c_315484,c_315482,c_315468,c_315466,c_315454,c_315452,c_315438,c_315436,c_315422,c_315420,c_315406,c_315404,c_315390,c_315388,c_315374,c_315372,c_315358,c_315356,c_315342,c_315340,c_315325,c_315323,c_315309,c_315307,c_315293,c_315291,c_315277,c_315275,c_315261,c_315259,c_315245,c_315243,c_315229,c_315227,c_315213,c_315211,c_315197,c_315195,c_315181,c_315179,c_315165,c_315163,c_315149,c_315135,c_315108,c_315086,c_315033,c_315011,c_314980,c_314952,c_314900,c_314879,c_314834,c_314820,c_314776,c_314763,c_314720,c_314704,c_314663,c_314647,c_314610,c_314594,c_314553,c_314549,c_314524,c_314508,c_314473,c_314396,c_314236,c_314028,c_313956,c_313928,c_313912,c_313865,c_313849,c_313802,c_313786,c_313741,c_313725,c_313682,c_313666,c_313625,c_313609,c_313572,c_313556,c_313519,c_313503,c_313464,c_313460,c_313437,c_313421,c_313388,c_313304,c_313127,c_312947,c_312928,c_312820,c_312771,c_310553,c_310434,c_310315,c_310196,c_309601,c_309482,c_201213,c_201092,c_200971,c_200850,c_200487,c_200366,c_200245,c_200124,c_200003,c_199882,c_92928,c_92929,c_92930,c_92931,c_92932,c_92933,c_92934,c_92935,c_92936,c_92937,c_92938,c_92939,c_92940,c_92941,c_92942,c_92943,c_92944,c_92945,c_92946,c_92947,c_92948,c_92949,c_92950,c_92951,c_92952,c_92953,c_92954,c_92955,c_92956,c_92957,c_92958,c_92959,c_92960,c_92961,c_92962,c_92963,c_92964,c_92965,c_92967,c_92968,c_92969,c_92971,c_92972,c_92973,c_92974,c_92975,c_92976,c_92977,c_92978,c_92979,c_92980,c_92981,c_92983,c_92984,c_92985,c_92863,c_92864,c_92865,c_92866,c_92867,c_92868,c_92869,c_92870,c_92871,c_92872,c_92873,c_92874,c_92875,c_92876,c_92877,c_92878,c_92879,c_92880,c_92881,c_92882,c_92883,c_92884,c_92885,c_92886,c_92887,c_92888,c_92889,c_92890,c_92891,c_92892,c_92893,c_92894,c_92895,c_92896,c_92897,c_92898,c_92899,c_92900,c_92902,c_92903,c_92904,c_92912,c_92913,c_92914,c_92915,c_92916,c_92917,c_92918,c_92919,c_92920,c_92921,c_92923,c_92924,c_92925,c_92926,c_67457,c_40320]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV107-1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 17:10:32 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running EPR theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 143.83/28.19 % SZS status Started for theBenchmark.p
% 143.83/28.19 % SZS status Unsatisfiable for theBenchmark.p
% 143.83/28.19
% 143.83/28.19 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 143.83/28.19
% 143.83/28.19 % ------ iProver source info
% 143.83/28.19
% 143.83/28.19 % git: date: 2026-07-19 20:42:38 +0200
% 143.83/28.19 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 143.83/28.19 % git: non_committed_changes: false
% 143.83/28.19
% 143.83/28.19 % ------ Parsing...% successful
% 143.83/28.19
% 143.83/28.19
% 143.83/28.19 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_eq
% 143.83/28.19 %
% 143.83/28.19
% 143.83/28.19 % ------ Preprocessing... sup_sim: 1 sf_s rm: 2637 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe_e sup_sim: 0 sf_s rm: 244 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 54 0s sf_e pe_s pe_e %
% 143.83/28.19
% 143.83/28.19 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_eq
% 143.83/28.19 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Option_epr_non_horn_eq
% 143.83/28.19 %
% 143.83/28.19
% 143.83/28.19 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 143.83/28.19 % ------ Proving...
% 143.83/28.19 % ------ Problem Properties
% 143.83/28.19
% 143.83/28.19 %
% 143.83/28.19 % clauses 180
% 143.83/28.19 % conjectures 2
% 143.83/28.19 % EPR 180
% 143.83/28.19 % Horn 167
% 143.83/28.19 % unary 48
% 143.83/28.19 % binary 115
% 143.83/28.19 % lits 799
% 143.83/28.19 % lits eq 23
% 143.83/28.19 % fd_pure 0
% 143.83/28.19 % fd_pseudo 0
% 143.83/28.19 % fd_cond 1
% 143.83/28.19 % fd_pseudo_cond 0
% 143.83/28.19 % AC symbols 0
% 143.83/28.19
% 143.83/28.19 % ------ Schedule EPR non Horn eq is on
% 143.83/28.19
% 143.83/28.19 % ------ Option_epr_non_horn_eq Time Limit: Unbounded
% 143.83/28.19
% 143.83/28.19
% 143.83/28.19 % ------
% 143.83/28.19 % Current options:
% 143.83/28.19 % ------
% 143.83/28.19
% 143.83/28.19
% 143.83/28.19 %
% 143.83/28.19
% 143.83/28.19 % ------ Proving...
% 143.83/28.19 %
% 143.83/28.19
% 143.83/28.19 % SZS status Unsatisfiable for theBenchmark.p
% 143.83/28.19
% 143.83/28.19 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 198.49/28.21
% 198.49/28.21
%------------------------------------------------------------------------------