%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV108-1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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 247.97s 39.89s
% Output : CNFRefutation 247.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 137
% Syntax : Number of formulae : 589 ( 8 unt; 0 def)
% Number of atoms : 5254 ( 15 equ)
% Maximal formula atoms : 63 ( 8 avg)
% Number of connectives : 5689 (1024 ~;4665 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 10 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(f2576,axiom,
! [X0] :
( ~ sP38_aig_name(X0)
| ~ v69(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u705125) ).
fof(f2577,axiom,
! [X0] :
( ~ sP38_aig_name(X0)
| ~ v21(X0)
| ~ v23(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u705126) ).
fof(f137653,axiom,
! [X0,X1] :
( ~ v28946(X0,X1)
| v28941(X0,X1)
| v28947(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490806) ).
fof(f137654,axiom,
! [X0,X1] :
( ~ v28941(X0,X1)
| v28946(X0,X1)
| v28947(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490807) ).
fof(f137655,axiom,
! [X0,X1] :
( ~ v81(X0)
| v4914(X0)
| ~ v28945(X0,X1)
| v28946(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490803) ).
fof(f137656,axiom,
! [X0,X1] :
( ~ v81(X0)
| v4914(X0)
| ~ v28946(X0,X1)
| v28945(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490804) ).
fof(f137657,axiom,
! [X0,X1] :
( v81(X0)
| ~ v28945(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490798) ).
fof(f137658,axiom,
! [X0,X1] :
( ~ v4914(X0)
| ~ v28945(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490799) ).
fof(f137659,axiom,
! [X0,X1] :
( sP38_aig_name(X0)
| ~ v26522(X0,X1)
| v28945(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490795) ).
fof(f137660,axiom,
! [X0,X1] :
( sP38_aig_name(X0)
| ~ v28945(X0,X1)
| v26522(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490796) ).
fof(f137973,axiom,
( ~ sP24007
| v26522(sK23533_VarCurr,bitIndex59)
| v28941(sK23533_VarCurr,bitIndex59) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490352) ).
fof(f137974,axiom,
( ~ sP24007
| ~ v26522(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex59) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490353) ).
fof(f137975,axiom,
( ~ sP24008
| v26522(sK23533_VarCurr,bitIndex58)
| v28941(sK23533_VarCurr,bitIndex58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490348) ).
fof(f137976,axiom,
( ~ sP24008
| ~ v26522(sK23533_VarCurr,bitIndex58)
| ~ v28941(sK23533_VarCurr,bitIndex58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490349) ).
fof(f137977,axiom,
( ~ sP24009
| v26522(sK23533_VarCurr,bitIndex57)
| v28941(sK23533_VarCurr,bitIndex57) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490344) ).
fof(f137978,axiom,
( ~ sP24009
| ~ v26522(sK23533_VarCurr,bitIndex57)
| ~ v28941(sK23533_VarCurr,bitIndex57) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490345) ).
fof(f137979,axiom,
( ~ sP24010
| v26522(sK23533_VarCurr,bitIndex56)
| v28941(sK23533_VarCurr,bitIndex56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490340) ).
fof(f137980,axiom,
( ~ sP24010
| ~ v26522(sK23533_VarCurr,bitIndex56)
| ~ v28941(sK23533_VarCurr,bitIndex56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490341) ).
fof(f137981,axiom,
( ~ sP24011
| v26522(sK23533_VarCurr,bitIndex55)
| v28941(sK23533_VarCurr,bitIndex55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490336) ).
fof(f137982,axiom,
( ~ sP24011
| ~ v26522(sK23533_VarCurr,bitIndex55)
| ~ v28941(sK23533_VarCurr,bitIndex55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490337) ).
fof(f137983,axiom,
( ~ sP24012
| v26522(sK23533_VarCurr,bitIndex54)
| v28941(sK23533_VarCurr,bitIndex54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490332) ).
fof(f137984,axiom,
( ~ sP24012
| ~ v26522(sK23533_VarCurr,bitIndex54)
| ~ v28941(sK23533_VarCurr,bitIndex54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490333) ).
fof(f137985,axiom,
( ~ sP24013
| v26522(sK23533_VarCurr,bitIndex53)
| v28941(sK23533_VarCurr,bitIndex53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490328) ).
fof(f137986,axiom,
( ~ sP24013
| ~ v26522(sK23533_VarCurr,bitIndex53)
| ~ v28941(sK23533_VarCurr,bitIndex53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490329) ).
fof(f137987,axiom,
( ~ sP24014
| v26522(sK23533_VarCurr,bitIndex52)
| v28941(sK23533_VarCurr,bitIndex52) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490324) ).
fof(f137988,axiom,
( ~ sP24014
| ~ v26522(sK23533_VarCurr,bitIndex52)
| ~ v28941(sK23533_VarCurr,bitIndex52) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490325) ).
fof(f137989,axiom,
( ~ sP24015
| v26522(sK23533_VarCurr,bitIndex51)
| v28941(sK23533_VarCurr,bitIndex51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490320) ).
fof(f137990,axiom,
( ~ sP24015
| ~ v26522(sK23533_VarCurr,bitIndex51)
| ~ v28941(sK23533_VarCurr,bitIndex51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490321) ).
fof(f137991,axiom,
( ~ sP24016
| v26522(sK23533_VarCurr,bitIndex50)
| v28941(sK23533_VarCurr,bitIndex50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490316) ).
fof(f137992,axiom,
( ~ sP24016
| ~ v26522(sK23533_VarCurr,bitIndex50)
| ~ v28941(sK23533_VarCurr,bitIndex50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490317) ).
fof(f137993,axiom,
( ~ sP24017
| v26522(sK23533_VarCurr,bitIndex49)
| v28941(sK23533_VarCurr,bitIndex49) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490312) ).
fof(f137994,axiom,
( ~ sP24017
| ~ v26522(sK23533_VarCurr,bitIndex49)
| ~ v28941(sK23533_VarCurr,bitIndex49) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490313) ).
fof(f137995,axiom,
( ~ sP24018
| v26522(sK23533_VarCurr,bitIndex48)
| v28941(sK23533_VarCurr,bitIndex48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490308) ).
fof(f137996,axiom,
( ~ sP24018
| ~ v26522(sK23533_VarCurr,bitIndex48)
| ~ v28941(sK23533_VarCurr,bitIndex48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490309) ).
fof(f137997,axiom,
( ~ sP24019
| v26522(sK23533_VarCurr,bitIndex47)
| v28941(sK23533_VarCurr,bitIndex47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490304) ).
fof(f137998,axiom,
( ~ sP24019
| ~ v26522(sK23533_VarCurr,bitIndex47)
| ~ v28941(sK23533_VarCurr,bitIndex47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490305) ).
fof(f137999,axiom,
( ~ sP24020
| v26522(sK23533_VarCurr,bitIndex46)
| v28941(sK23533_VarCurr,bitIndex46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490300) ).
fof(f138000,axiom,
( ~ sP24020
| ~ v26522(sK23533_VarCurr,bitIndex46)
| ~ v28941(sK23533_VarCurr,bitIndex46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490301) ).
fof(f138001,axiom,
( ~ sP24021
| v26522(sK23533_VarCurr,bitIndex45)
| v28941(sK23533_VarCurr,bitIndex45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490296) ).
fof(f138002,axiom,
( ~ sP24021
| ~ v26522(sK23533_VarCurr,bitIndex45)
| ~ v28941(sK23533_VarCurr,bitIndex45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490297) ).
fof(f138003,axiom,
( ~ sP24022
| v26522(sK23533_VarCurr,bitIndex44)
| v28941(sK23533_VarCurr,bitIndex44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490292) ).
fof(f138004,axiom,
( ~ sP24022
| ~ v26522(sK23533_VarCurr,bitIndex44)
| ~ v28941(sK23533_VarCurr,bitIndex44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490293) ).
fof(f138005,axiom,
( ~ sP24023
| v26522(sK23533_VarCurr,bitIndex43)
| v28941(sK23533_VarCurr,bitIndex43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490288) ).
fof(f138006,axiom,
( ~ sP24023
| ~ v26522(sK23533_VarCurr,bitIndex43)
| ~ v28941(sK23533_VarCurr,bitIndex43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490289) ).
fof(f138007,axiom,
( ~ sP24024
| v26522(sK23533_VarCurr,bitIndex42)
| v28941(sK23533_VarCurr,bitIndex42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490284) ).
fof(f138008,axiom,
( ~ sP24024
| ~ v26522(sK23533_VarCurr,bitIndex42)
| ~ v28941(sK23533_VarCurr,bitIndex42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490285) ).
fof(f138009,axiom,
( ~ sP24025
| v26522(sK23533_VarCurr,bitIndex41)
| v28941(sK23533_VarCurr,bitIndex41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490280) ).
fof(f138010,axiom,
( ~ sP24025
| ~ v26522(sK23533_VarCurr,bitIndex41)
| ~ v28941(sK23533_VarCurr,bitIndex41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490281) ).
fof(f138011,axiom,
( ~ sP24026
| v26522(sK23533_VarCurr,bitIndex40)
| v28941(sK23533_VarCurr,bitIndex40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490276) ).
fof(f138012,axiom,
( ~ sP24026
| ~ v26522(sK23533_VarCurr,bitIndex40)
| ~ v28941(sK23533_VarCurr,bitIndex40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490277) ).
fof(f138013,axiom,
( ~ sP24027
| v26522(sK23533_VarCurr,bitIndex39)
| v28941(sK23533_VarCurr,bitIndex39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490272) ).
fof(f138014,axiom,
( ~ sP24027
| ~ v26522(sK23533_VarCurr,bitIndex39)
| ~ v28941(sK23533_VarCurr,bitIndex39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490273) ).
fof(f138015,axiom,
( ~ sP24028
| v26522(sK23533_VarCurr,bitIndex38)
| v28941(sK23533_VarCurr,bitIndex38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490268) ).
fof(f138016,axiom,
( ~ sP24028
| ~ v26522(sK23533_VarCurr,bitIndex38)
| ~ v28941(sK23533_VarCurr,bitIndex38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490269) ).
fof(f138017,axiom,
( ~ sP24029
| v26522(sK23533_VarCurr,bitIndex37)
| v28941(sK23533_VarCurr,bitIndex37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490264) ).
fof(f138018,axiom,
( ~ sP24029
| ~ v26522(sK23533_VarCurr,bitIndex37)
| ~ v28941(sK23533_VarCurr,bitIndex37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490265) ).
fof(f138019,axiom,
( ~ sP24030
| v26522(sK23533_VarCurr,bitIndex36)
| v28941(sK23533_VarCurr,bitIndex36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490260) ).
fof(f138020,axiom,
( ~ sP24030
| ~ v26522(sK23533_VarCurr,bitIndex36)
| ~ v28941(sK23533_VarCurr,bitIndex36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490261) ).
fof(f138021,axiom,
( ~ sP24031
| v26522(sK23533_VarCurr,bitIndex35)
| v28941(sK23533_VarCurr,bitIndex35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490256) ).
fof(f138022,axiom,
( ~ sP24031
| ~ v26522(sK23533_VarCurr,bitIndex35)
| ~ v28941(sK23533_VarCurr,bitIndex35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490257) ).
fof(f138023,axiom,
( ~ sP24032
| v26522(sK23533_VarCurr,bitIndex34)
| v28941(sK23533_VarCurr,bitIndex34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490252) ).
fof(f138024,axiom,
( ~ sP24032
| ~ v26522(sK23533_VarCurr,bitIndex34)
| ~ v28941(sK23533_VarCurr,bitIndex34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490253) ).
fof(f138025,axiom,
( ~ sP24033
| v26522(sK23533_VarCurr,bitIndex33)
| v28941(sK23533_VarCurr,bitIndex33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490248) ).
fof(f138026,axiom,
( ~ sP24033
| ~ v26522(sK23533_VarCurr,bitIndex33)
| ~ v28941(sK23533_VarCurr,bitIndex33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490249) ).
fof(f138027,axiom,
( ~ sP24034
| v26522(sK23533_VarCurr,bitIndex32)
| v28941(sK23533_VarCurr,bitIndex32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490244) ).
fof(f138028,axiom,
( ~ sP24034
| ~ v26522(sK23533_VarCurr,bitIndex32)
| ~ v28941(sK23533_VarCurr,bitIndex32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490245) ).
fof(f138029,axiom,
( ~ sP24035
| v26522(sK23533_VarCurr,bitIndex31)
| v28941(sK23533_VarCurr,bitIndex31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490240) ).
fof(f138030,axiom,
( ~ sP24035
| ~ v26522(sK23533_VarCurr,bitIndex31)
| ~ v28941(sK23533_VarCurr,bitIndex31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490241) ).
fof(f138031,axiom,
( ~ sP24036
| v26522(sK23533_VarCurr,bitIndex30)
| v28941(sK23533_VarCurr,bitIndex30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490236) ).
fof(f138032,axiom,
( ~ sP24036
| ~ v26522(sK23533_VarCurr,bitIndex30)
| ~ v28941(sK23533_VarCurr,bitIndex30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490237) ).
fof(f138033,axiom,
( ~ sP24037
| v26522(sK23533_VarCurr,bitIndex29)
| v28941(sK23533_VarCurr,bitIndex29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490232) ).
fof(f138034,axiom,
( ~ sP24037
| ~ v26522(sK23533_VarCurr,bitIndex29)
| ~ v28941(sK23533_VarCurr,bitIndex29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490233) ).
fof(f138035,axiom,
( ~ sP24038
| v26522(sK23533_VarCurr,bitIndex28)
| v28941(sK23533_VarCurr,bitIndex28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490228) ).
fof(f138036,axiom,
( ~ sP24038
| ~ v26522(sK23533_VarCurr,bitIndex28)
| ~ v28941(sK23533_VarCurr,bitIndex28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490229) ).
fof(f138037,axiom,
( ~ sP24039
| v26522(sK23533_VarCurr,bitIndex27)
| v28941(sK23533_VarCurr,bitIndex27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490224) ).
fof(f138038,axiom,
( ~ sP24039
| ~ v26522(sK23533_VarCurr,bitIndex27)
| ~ v28941(sK23533_VarCurr,bitIndex27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490225) ).
fof(f138039,axiom,
( ~ sP24040
| v26522(sK23533_VarCurr,bitIndex26)
| v28941(sK23533_VarCurr,bitIndex26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490220) ).
fof(f138040,axiom,
( ~ sP24040
| ~ v26522(sK23533_VarCurr,bitIndex26)
| ~ v28941(sK23533_VarCurr,bitIndex26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490221) ).
fof(f138041,axiom,
( ~ sP24041
| v26522(sK23533_VarCurr,bitIndex25)
| v28941(sK23533_VarCurr,bitIndex25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490216) ).
fof(f138042,axiom,
( ~ sP24041
| ~ v26522(sK23533_VarCurr,bitIndex25)
| ~ v28941(sK23533_VarCurr,bitIndex25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490217) ).
fof(f138043,axiom,
( ~ sP24042
| v26522(sK23533_VarCurr,bitIndex24)
| v28941(sK23533_VarCurr,bitIndex24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490212) ).
fof(f138044,axiom,
( ~ sP24042
| ~ v26522(sK23533_VarCurr,bitIndex24)
| ~ v28941(sK23533_VarCurr,bitIndex24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490213) ).
fof(f138045,axiom,
( ~ sP24043
| v26522(sK23533_VarCurr,bitIndex23)
| v28941(sK23533_VarCurr,bitIndex23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490208) ).
fof(f138046,axiom,
( ~ sP24043
| ~ v26522(sK23533_VarCurr,bitIndex23)
| ~ v28941(sK23533_VarCurr,bitIndex23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490209) ).
fof(f138047,axiom,
( ~ sP24044
| v26522(sK23533_VarCurr,bitIndex22)
| v28941(sK23533_VarCurr,bitIndex22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490204) ).
fof(f138048,axiom,
( ~ sP24044
| ~ v26522(sK23533_VarCurr,bitIndex22)
| ~ v28941(sK23533_VarCurr,bitIndex22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490205) ).
fof(f138049,axiom,
( ~ sP24045
| v26522(sK23533_VarCurr,bitIndex21)
| v28941(sK23533_VarCurr,bitIndex21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490200) ).
fof(f138050,axiom,
( ~ sP24045
| ~ v26522(sK23533_VarCurr,bitIndex21)
| ~ v28941(sK23533_VarCurr,bitIndex21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490201) ).
fof(f138051,axiom,
( ~ sP24046
| v26522(sK23533_VarCurr,bitIndex20)
| v28941(sK23533_VarCurr,bitIndex20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490196) ).
fof(f138052,axiom,
( ~ sP24046
| ~ v26522(sK23533_VarCurr,bitIndex20)
| ~ v28941(sK23533_VarCurr,bitIndex20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490197) ).
fof(f138053,axiom,
( ~ sP24047
| v26522(sK23533_VarCurr,bitIndex19)
| v28941(sK23533_VarCurr,bitIndex19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490192) ).
fof(f138054,axiom,
( ~ sP24047
| ~ v26522(sK23533_VarCurr,bitIndex19)
| ~ v28941(sK23533_VarCurr,bitIndex19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490193) ).
fof(f138055,axiom,
( ~ sP24048
| v26522(sK23533_VarCurr,bitIndex18)
| v28941(sK23533_VarCurr,bitIndex18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490188) ).
fof(f138056,axiom,
( ~ sP24048
| ~ v26522(sK23533_VarCurr,bitIndex18)
| ~ v28941(sK23533_VarCurr,bitIndex18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490189) ).
fof(f138057,axiom,
( ~ sP24049
| v26522(sK23533_VarCurr,bitIndex17)
| v28941(sK23533_VarCurr,bitIndex17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490184) ).
fof(f138058,axiom,
( ~ sP24049
| ~ v26522(sK23533_VarCurr,bitIndex17)
| ~ v28941(sK23533_VarCurr,bitIndex17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490185) ).
fof(f138059,axiom,
( ~ sP24050
| v26522(sK23533_VarCurr,bitIndex16)
| v28941(sK23533_VarCurr,bitIndex16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490180) ).
fof(f138060,axiom,
( ~ sP24050
| ~ v26522(sK23533_VarCurr,bitIndex16)
| ~ v28941(sK23533_VarCurr,bitIndex16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490181) ).
fof(f138061,axiom,
( ~ sP24051
| v26522(sK23533_VarCurr,bitIndex15)
| v28941(sK23533_VarCurr,bitIndex15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490176) ).
fof(f138062,axiom,
( ~ sP24051
| ~ v26522(sK23533_VarCurr,bitIndex15)
| ~ v28941(sK23533_VarCurr,bitIndex15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490177) ).
fof(f138063,axiom,
( ~ sP24052
| v26522(sK23533_VarCurr,bitIndex14)
| v28941(sK23533_VarCurr,bitIndex14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490172) ).
fof(f138064,axiom,
( ~ sP24052
| ~ v26522(sK23533_VarCurr,bitIndex14)
| ~ v28941(sK23533_VarCurr,bitIndex14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490173) ).
fof(f138065,axiom,
( ~ sP24053
| v26522(sK23533_VarCurr,bitIndex13)
| v28941(sK23533_VarCurr,bitIndex13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490168) ).
fof(f138066,axiom,
( ~ sP24053
| ~ v26522(sK23533_VarCurr,bitIndex13)
| ~ v28941(sK23533_VarCurr,bitIndex13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490169) ).
fof(f138067,axiom,
( ~ sP24054
| v26522(sK23533_VarCurr,bitIndex12)
| v28941(sK23533_VarCurr,bitIndex12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490164) ).
fof(f138068,axiom,
( ~ sP24054
| ~ v26522(sK23533_VarCurr,bitIndex12)
| ~ v28941(sK23533_VarCurr,bitIndex12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490165) ).
fof(f138069,axiom,
( ~ sP24055
| v26522(sK23533_VarCurr,bitIndex11)
| v28941(sK23533_VarCurr,bitIndex11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490160) ).
fof(f138070,axiom,
( ~ sP24055
| ~ v26522(sK23533_VarCurr,bitIndex11)
| ~ v28941(sK23533_VarCurr,bitIndex11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490161) ).
fof(f138071,axiom,
( ~ sP24056
| v26522(sK23533_VarCurr,bitIndex10)
| v28941(sK23533_VarCurr,bitIndex10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490156) ).
fof(f138072,axiom,
( ~ sP24056
| ~ v26522(sK23533_VarCurr,bitIndex10)
| ~ v28941(sK23533_VarCurr,bitIndex10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490157) ).
fof(f138073,axiom,
( ~ sP24057
| v26522(sK23533_VarCurr,bitIndex9)
| v28941(sK23533_VarCurr,bitIndex9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490152) ).
fof(f138074,axiom,
( ~ sP24057
| ~ v26522(sK23533_VarCurr,bitIndex9)
| ~ v28941(sK23533_VarCurr,bitIndex9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490153) ).
fof(f138075,axiom,
( ~ sP24058
| v26522(sK23533_VarCurr,bitIndex8)
| v28941(sK23533_VarCurr,bitIndex8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490148) ).
fof(f138076,axiom,
( ~ sP24058
| ~ v26522(sK23533_VarCurr,bitIndex8)
| ~ v28941(sK23533_VarCurr,bitIndex8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490149) ).
fof(f138077,axiom,
( ~ sP24059
| v26522(sK23533_VarCurr,bitIndex7)
| v28941(sK23533_VarCurr,bitIndex7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490144) ).
fof(f138078,axiom,
( ~ sP24059
| ~ v26522(sK23533_VarCurr,bitIndex7)
| ~ v28941(sK23533_VarCurr,bitIndex7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490145) ).
fof(f138079,axiom,
( ~ sP24060
| v26522(sK23533_VarCurr,bitIndex6)
| v28941(sK23533_VarCurr,bitIndex6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490140) ).
fof(f138080,axiom,
( ~ sP24060
| ~ v26522(sK23533_VarCurr,bitIndex6)
| ~ v28941(sK23533_VarCurr,bitIndex6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490141) ).
fof(f138081,axiom,
( ~ sP24061
| v26522(sK23533_VarCurr,bitIndex5)
| v28941(sK23533_VarCurr,bitIndex5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490136) ).
fof(f138082,axiom,
( ~ sP24061
| ~ v26522(sK23533_VarCurr,bitIndex5)
| ~ v28941(sK23533_VarCurr,bitIndex5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490137) ).
fof(f138083,axiom,
( ~ sP24062
| v26522(sK23533_VarCurr,bitIndex4)
| v28941(sK23533_VarCurr,bitIndex4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490132) ).
fof(f138084,axiom,
( ~ sP24062
| ~ v26522(sK23533_VarCurr,bitIndex4)
| ~ v28941(sK23533_VarCurr,bitIndex4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490133) ).
fof(f138085,axiom,
( ~ sP24063
| v26522(sK23533_VarCurr,bitIndex3)
| v28941(sK23533_VarCurr,bitIndex3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490128) ).
fof(f138086,axiom,
( ~ sP24063
| ~ v26522(sK23533_VarCurr,bitIndex3)
| ~ v28941(sK23533_VarCurr,bitIndex3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490129) ).
fof(f138087,negated_conjecture,
~ v4914(sK23533_VarCurr),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490112) ).
fof(f138088,negated_conjecture,
v81(sK23533_VarCurr),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490113) ).
fof(f138089,negated_conjecture,
~ v28947(sK23533_VarCurr),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490114) ).
fof(f138090,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490115) ).
fof(f138091,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490116) ).
fof(f138092,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490117) ).
fof(f138093,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490118) ).
fof(f138094,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490119) ).
fof(f138095,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490120) ).
fof(f138096,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490121) ).
fof(f138097,negated_conjecture,
( sP24007
| sP24008
| sP24009
| sP24010
| sP24011
| sP24012
| sP24013
| sP24014
| sP24015
| sP24016
| sP24017
| sP24018
| sP24019
| sP24020
| sP24021
| sP24022
| sP24023
| sP24024
| sP24025
| sP24026
| sP24027
| sP24028
| sP24029
| sP24030
| sP24031
| sP24032
| sP24033
| sP24034
| sP24035
| sP24036
| sP24037
| sP24038
| sP24039
| sP24040
| sP24041
| sP24042
| sP24043
| sP24044
| sP24045
| sP24046
| sP24047
| sP24048
| sP24049
| sP24050
| sP24051
| sP24052
| sP24053
| sP24054
| sP24055
| sP24056
| sP24057
| sP24058
| sP24059
| sP24060
| sP24061
| sP24062
| sP24063
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490122) ).
fof(f138098,negated_conjecture,
( v23(sK23533_VarCurr)
| v69(sK23533_VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490123) ).
fof(f138099,negated_conjecture,
( v21(sK23533_VarCurr)
| v69(sK23533_VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u490124) ).
tcf(c_156702,negated_conjecture,
~ v4914(sK23533_VarCurr),
inference(cnf_transformation,[],[f138087]) ).
tcf(c_156703,negated_conjecture,
v81(sK23533_VarCurr),
inference(cnf_transformation,[],[f138088]) ).
tcf(c_156704,negated_conjecture,
~ v28947(sK23533_VarCurr),
inference(cnf_transformation,[],[f138089]) ).
tcf(c_156705,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f138090]) ).
tcf(c_156706,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(cnf_transformation,[],[f138091]) ).
tcf(c_156707,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f138092]) ).
tcf(c_156708,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f138093]) ).
tcf(c_156709,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
inference(cnf_transformation,[],[f138094]) ).
tcf(c_156710,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(cnf_transformation,[],[f138095]) ).
tcf(c_156711,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f138096]) ).
tcf(c_156712,negated_conjecture,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(cnf_transformation,[],[f138097]) ).
tcf(c_156713,negated_conjecture,
( v23(sK23533_VarCurr)
| v69(sK23533_VarCurr) ),
inference(cnf_transformation,[],[f138098]) ).
tcf(c_156714,negated_conjecture,
( v21(sK23533_VarCurr)
| v69(sK23533_VarCurr) ),
inference(cnf_transformation,[],[f138099]) ).
tcf(c_156725,plain,
! [X0: $i,X1: $i] :
( v28947(X0)
| v28946(X0,X1)
| ~ v28941(X0,X1) ),
inference(cnf_transformation,[],[f137654]) ).
tcf(c_156726,plain,
! [X0: $i,X1: $i] :
( v28947(X0)
| v28941(X0,X1)
| ~ v28946(X0,X1) ),
inference(cnf_transformation,[],[f137653]) ).
tcf(c_156736,plain,
( ~ sP24007
| ~ v26522(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex59) ),
inference(cnf_transformation,[],[f137974]) ).
tcf(c_156737,plain,
( v26522(sK23533_VarCurr,bitIndex59)
| v28941(sK23533_VarCurr,bitIndex59)
| ~ sP24007 ),
inference(cnf_transformation,[],[f137973]) ).
tcf(c_156738,plain,
( ~ sP24008
| ~ v26522(sK23533_VarCurr,bitIndex58)
| ~ v28941(sK23533_VarCurr,bitIndex58) ),
inference(cnf_transformation,[],[f137976]) ).
tcf(c_156739,plain,
( v26522(sK23533_VarCurr,bitIndex58)
| v28941(sK23533_VarCurr,bitIndex58)
| ~ sP24008 ),
inference(cnf_transformation,[],[f137975]) ).
tcf(c_156740,plain,
( ~ sP24009
| ~ v26522(sK23533_VarCurr,bitIndex57)
| ~ v28941(sK23533_VarCurr,bitIndex57) ),
inference(cnf_transformation,[],[f137978]) ).
tcf(c_156741,plain,
( v26522(sK23533_VarCurr,bitIndex57)
| v28941(sK23533_VarCurr,bitIndex57)
| ~ sP24009 ),
inference(cnf_transformation,[],[f137977]) ).
tcf(c_156742,plain,
( ~ sP24010
| ~ v26522(sK23533_VarCurr,bitIndex56)
| ~ v28941(sK23533_VarCurr,bitIndex56) ),
inference(cnf_transformation,[],[f137980]) ).
tcf(c_156743,plain,
( v26522(sK23533_VarCurr,bitIndex56)
| v28941(sK23533_VarCurr,bitIndex56)
| ~ sP24010 ),
inference(cnf_transformation,[],[f137979]) ).
tcf(c_156744,plain,
( ~ sP24011
| ~ v26522(sK23533_VarCurr,bitIndex55)
| ~ v28941(sK23533_VarCurr,bitIndex55) ),
inference(cnf_transformation,[],[f137982]) ).
tcf(c_156745,plain,
( v26522(sK23533_VarCurr,bitIndex55)
| v28941(sK23533_VarCurr,bitIndex55)
| ~ sP24011 ),
inference(cnf_transformation,[],[f137981]) ).
tcf(c_156746,plain,
( ~ sP24012
| ~ v26522(sK23533_VarCurr,bitIndex54)
| ~ v28941(sK23533_VarCurr,bitIndex54) ),
inference(cnf_transformation,[],[f137984]) ).
tcf(c_156747,plain,
( v26522(sK23533_VarCurr,bitIndex54)
| v28941(sK23533_VarCurr,bitIndex54)
| ~ sP24012 ),
inference(cnf_transformation,[],[f137983]) ).
tcf(c_156748,plain,
( ~ sP24013
| ~ v26522(sK23533_VarCurr,bitIndex53)
| ~ v28941(sK23533_VarCurr,bitIndex53) ),
inference(cnf_transformation,[],[f137986]) ).
tcf(c_156749,plain,
( v26522(sK23533_VarCurr,bitIndex53)
| v28941(sK23533_VarCurr,bitIndex53)
| ~ sP24013 ),
inference(cnf_transformation,[],[f137985]) ).
tcf(c_156750,plain,
( ~ sP24014
| ~ v26522(sK23533_VarCurr,bitIndex52)
| ~ v28941(sK23533_VarCurr,bitIndex52) ),
inference(cnf_transformation,[],[f137988]) ).
tcf(c_156751,plain,
( v26522(sK23533_VarCurr,bitIndex52)
| v28941(sK23533_VarCurr,bitIndex52)
| ~ sP24014 ),
inference(cnf_transformation,[],[f137987]) ).
tcf(c_156752,plain,
( ~ sP24015
| ~ v26522(sK23533_VarCurr,bitIndex51)
| ~ v28941(sK23533_VarCurr,bitIndex51) ),
inference(cnf_transformation,[],[f137990]) ).
tcf(c_156753,plain,
( v26522(sK23533_VarCurr,bitIndex51)
| v28941(sK23533_VarCurr,bitIndex51)
| ~ sP24015 ),
inference(cnf_transformation,[],[f137989]) ).
tcf(c_156754,plain,
( ~ sP24016
| ~ v26522(sK23533_VarCurr,bitIndex50)
| ~ v28941(sK23533_VarCurr,bitIndex50) ),
inference(cnf_transformation,[],[f137992]) ).
tcf(c_156755,plain,
( v26522(sK23533_VarCurr,bitIndex50)
| v28941(sK23533_VarCurr,bitIndex50)
| ~ sP24016 ),
inference(cnf_transformation,[],[f137991]) ).
tcf(c_156756,plain,
( ~ sP24017
| ~ v26522(sK23533_VarCurr,bitIndex49)
| ~ v28941(sK23533_VarCurr,bitIndex49) ),
inference(cnf_transformation,[],[f137994]) ).
tcf(c_156757,plain,
( v26522(sK23533_VarCurr,bitIndex49)
| v28941(sK23533_VarCurr,bitIndex49)
| ~ sP24017 ),
inference(cnf_transformation,[],[f137993]) ).
tcf(c_156758,plain,
( ~ sP24018
| ~ v26522(sK23533_VarCurr,bitIndex48)
| ~ v28941(sK23533_VarCurr,bitIndex48) ),
inference(cnf_transformation,[],[f137996]) ).
tcf(c_156759,plain,
( v26522(sK23533_VarCurr,bitIndex48)
| v28941(sK23533_VarCurr,bitIndex48)
| ~ sP24018 ),
inference(cnf_transformation,[],[f137995]) ).
tcf(c_156760,plain,
( ~ sP24019
| ~ v26522(sK23533_VarCurr,bitIndex47)
| ~ v28941(sK23533_VarCurr,bitIndex47) ),
inference(cnf_transformation,[],[f137998]) ).
tcf(c_156761,plain,
( v26522(sK23533_VarCurr,bitIndex47)
| v28941(sK23533_VarCurr,bitIndex47)
| ~ sP24019 ),
inference(cnf_transformation,[],[f137997]) ).
tcf(c_156762,plain,
( ~ sP24020
| ~ v26522(sK23533_VarCurr,bitIndex46)
| ~ v28941(sK23533_VarCurr,bitIndex46) ),
inference(cnf_transformation,[],[f138000]) ).
tcf(c_156763,plain,
( v26522(sK23533_VarCurr,bitIndex46)
| v28941(sK23533_VarCurr,bitIndex46)
| ~ sP24020 ),
inference(cnf_transformation,[],[f137999]) ).
tcf(c_156764,plain,
( ~ sP24021
| ~ v26522(sK23533_VarCurr,bitIndex45)
| ~ v28941(sK23533_VarCurr,bitIndex45) ),
inference(cnf_transformation,[],[f138002]) ).
tcf(c_156765,plain,
( v26522(sK23533_VarCurr,bitIndex45)
| v28941(sK23533_VarCurr,bitIndex45)
| ~ sP24021 ),
inference(cnf_transformation,[],[f138001]) ).
tcf(c_156766,plain,
( ~ sP24022
| ~ v26522(sK23533_VarCurr,bitIndex44)
| ~ v28941(sK23533_VarCurr,bitIndex44) ),
inference(cnf_transformation,[],[f138004]) ).
tcf(c_156767,plain,
( v26522(sK23533_VarCurr,bitIndex44)
| v28941(sK23533_VarCurr,bitIndex44)
| ~ sP24022 ),
inference(cnf_transformation,[],[f138003]) ).
tcf(c_156768,plain,
( ~ sP24023
| ~ v26522(sK23533_VarCurr,bitIndex43)
| ~ v28941(sK23533_VarCurr,bitIndex43) ),
inference(cnf_transformation,[],[f138006]) ).
tcf(c_156769,plain,
( v26522(sK23533_VarCurr,bitIndex43)
| v28941(sK23533_VarCurr,bitIndex43)
| ~ sP24023 ),
inference(cnf_transformation,[],[f138005]) ).
tcf(c_156770,plain,
( ~ sP24024
| ~ v26522(sK23533_VarCurr,bitIndex42)
| ~ v28941(sK23533_VarCurr,bitIndex42) ),
inference(cnf_transformation,[],[f138008]) ).
tcf(c_156771,plain,
( v26522(sK23533_VarCurr,bitIndex42)
| v28941(sK23533_VarCurr,bitIndex42)
| ~ sP24024 ),
inference(cnf_transformation,[],[f138007]) ).
tcf(c_156772,plain,
( ~ sP24025
| ~ v26522(sK23533_VarCurr,bitIndex41)
| ~ v28941(sK23533_VarCurr,bitIndex41) ),
inference(cnf_transformation,[],[f138010]) ).
tcf(c_156773,plain,
( v26522(sK23533_VarCurr,bitIndex41)
| v28941(sK23533_VarCurr,bitIndex41)
| ~ sP24025 ),
inference(cnf_transformation,[],[f138009]) ).
tcf(c_156774,plain,
( ~ sP24026
| ~ v26522(sK23533_VarCurr,bitIndex40)
| ~ v28941(sK23533_VarCurr,bitIndex40) ),
inference(cnf_transformation,[],[f138012]) ).
tcf(c_156775,plain,
( v26522(sK23533_VarCurr,bitIndex40)
| v28941(sK23533_VarCurr,bitIndex40)
| ~ sP24026 ),
inference(cnf_transformation,[],[f138011]) ).
tcf(c_156776,plain,
( ~ sP24027
| ~ v26522(sK23533_VarCurr,bitIndex39)
| ~ v28941(sK23533_VarCurr,bitIndex39) ),
inference(cnf_transformation,[],[f138014]) ).
tcf(c_156777,plain,
( v26522(sK23533_VarCurr,bitIndex39)
| v28941(sK23533_VarCurr,bitIndex39)
| ~ sP24027 ),
inference(cnf_transformation,[],[f138013]) ).
tcf(c_156778,plain,
( ~ sP24028
| ~ v26522(sK23533_VarCurr,bitIndex38)
| ~ v28941(sK23533_VarCurr,bitIndex38) ),
inference(cnf_transformation,[],[f138016]) ).
tcf(c_156779,plain,
( v26522(sK23533_VarCurr,bitIndex38)
| v28941(sK23533_VarCurr,bitIndex38)
| ~ sP24028 ),
inference(cnf_transformation,[],[f138015]) ).
tcf(c_156780,plain,
( ~ sP24029
| ~ v26522(sK23533_VarCurr,bitIndex37)
| ~ v28941(sK23533_VarCurr,bitIndex37) ),
inference(cnf_transformation,[],[f138018]) ).
tcf(c_156781,plain,
( v26522(sK23533_VarCurr,bitIndex37)
| v28941(sK23533_VarCurr,bitIndex37)
| ~ sP24029 ),
inference(cnf_transformation,[],[f138017]) ).
tcf(c_156782,plain,
( ~ sP24030
| ~ v26522(sK23533_VarCurr,bitIndex36)
| ~ v28941(sK23533_VarCurr,bitIndex36) ),
inference(cnf_transformation,[],[f138020]) ).
tcf(c_156783,plain,
( v26522(sK23533_VarCurr,bitIndex36)
| v28941(sK23533_VarCurr,bitIndex36)
| ~ sP24030 ),
inference(cnf_transformation,[],[f138019]) ).
tcf(c_156784,plain,
( ~ sP24031
| ~ v26522(sK23533_VarCurr,bitIndex35)
| ~ v28941(sK23533_VarCurr,bitIndex35) ),
inference(cnf_transformation,[],[f138022]) ).
tcf(c_156785,plain,
( v26522(sK23533_VarCurr,bitIndex35)
| v28941(sK23533_VarCurr,bitIndex35)
| ~ sP24031 ),
inference(cnf_transformation,[],[f138021]) ).
tcf(c_156786,plain,
( ~ sP24032
| ~ v26522(sK23533_VarCurr,bitIndex34)
| ~ v28941(sK23533_VarCurr,bitIndex34) ),
inference(cnf_transformation,[],[f138024]) ).
tcf(c_156787,plain,
( v26522(sK23533_VarCurr,bitIndex34)
| v28941(sK23533_VarCurr,bitIndex34)
| ~ sP24032 ),
inference(cnf_transformation,[],[f138023]) ).
tcf(c_156788,plain,
( ~ sP24033
| ~ v26522(sK23533_VarCurr,bitIndex33)
| ~ v28941(sK23533_VarCurr,bitIndex33) ),
inference(cnf_transformation,[],[f138026]) ).
tcf(c_156789,plain,
( v26522(sK23533_VarCurr,bitIndex33)
| v28941(sK23533_VarCurr,bitIndex33)
| ~ sP24033 ),
inference(cnf_transformation,[],[f138025]) ).
tcf(c_156790,plain,
( ~ sP24034
| ~ v26522(sK23533_VarCurr,bitIndex32)
| ~ v28941(sK23533_VarCurr,bitIndex32) ),
inference(cnf_transformation,[],[f138028]) ).
tcf(c_156791,plain,
( v26522(sK23533_VarCurr,bitIndex32)
| v28941(sK23533_VarCurr,bitIndex32)
| ~ sP24034 ),
inference(cnf_transformation,[],[f138027]) ).
tcf(c_156792,plain,
( ~ sP24035
| ~ v26522(sK23533_VarCurr,bitIndex31)
| ~ v28941(sK23533_VarCurr,bitIndex31) ),
inference(cnf_transformation,[],[f138030]) ).
tcf(c_156793,plain,
( v26522(sK23533_VarCurr,bitIndex31)
| v28941(sK23533_VarCurr,bitIndex31)
| ~ sP24035 ),
inference(cnf_transformation,[],[f138029]) ).
tcf(c_156794,plain,
( ~ sP24036
| ~ v26522(sK23533_VarCurr,bitIndex30)
| ~ v28941(sK23533_VarCurr,bitIndex30) ),
inference(cnf_transformation,[],[f138032]) ).
tcf(c_156795,plain,
( v26522(sK23533_VarCurr,bitIndex30)
| v28941(sK23533_VarCurr,bitIndex30)
| ~ sP24036 ),
inference(cnf_transformation,[],[f138031]) ).
tcf(c_156796,plain,
( ~ sP24037
| ~ v26522(sK23533_VarCurr,bitIndex29)
| ~ v28941(sK23533_VarCurr,bitIndex29) ),
inference(cnf_transformation,[],[f138034]) ).
tcf(c_156797,plain,
( v26522(sK23533_VarCurr,bitIndex29)
| v28941(sK23533_VarCurr,bitIndex29)
| ~ sP24037 ),
inference(cnf_transformation,[],[f138033]) ).
tcf(c_156798,plain,
( ~ sP24038
| ~ v26522(sK23533_VarCurr,bitIndex28)
| ~ v28941(sK23533_VarCurr,bitIndex28) ),
inference(cnf_transformation,[],[f138036]) ).
tcf(c_156799,plain,
( v26522(sK23533_VarCurr,bitIndex28)
| v28941(sK23533_VarCurr,bitIndex28)
| ~ sP24038 ),
inference(cnf_transformation,[],[f138035]) ).
tcf(c_156800,plain,
( ~ sP24039
| ~ v26522(sK23533_VarCurr,bitIndex27)
| ~ v28941(sK23533_VarCurr,bitIndex27) ),
inference(cnf_transformation,[],[f138038]) ).
tcf(c_156801,plain,
( v26522(sK23533_VarCurr,bitIndex27)
| v28941(sK23533_VarCurr,bitIndex27)
| ~ sP24039 ),
inference(cnf_transformation,[],[f138037]) ).
tcf(c_156802,plain,
( ~ sP24040
| ~ v26522(sK23533_VarCurr,bitIndex26)
| ~ v28941(sK23533_VarCurr,bitIndex26) ),
inference(cnf_transformation,[],[f138040]) ).
tcf(c_156803,plain,
( v26522(sK23533_VarCurr,bitIndex26)
| v28941(sK23533_VarCurr,bitIndex26)
| ~ sP24040 ),
inference(cnf_transformation,[],[f138039]) ).
tcf(c_156804,plain,
( ~ sP24041
| ~ v26522(sK23533_VarCurr,bitIndex25)
| ~ v28941(sK23533_VarCurr,bitIndex25) ),
inference(cnf_transformation,[],[f138042]) ).
tcf(c_156805,plain,
( v26522(sK23533_VarCurr,bitIndex25)
| v28941(sK23533_VarCurr,bitIndex25)
| ~ sP24041 ),
inference(cnf_transformation,[],[f138041]) ).
tcf(c_156806,plain,
( ~ sP24042
| ~ v26522(sK23533_VarCurr,bitIndex24)
| ~ v28941(sK23533_VarCurr,bitIndex24) ),
inference(cnf_transformation,[],[f138044]) ).
tcf(c_156807,plain,
( v26522(sK23533_VarCurr,bitIndex24)
| v28941(sK23533_VarCurr,bitIndex24)
| ~ sP24042 ),
inference(cnf_transformation,[],[f138043]) ).
tcf(c_156808,plain,
( ~ sP24043
| ~ v26522(sK23533_VarCurr,bitIndex23)
| ~ v28941(sK23533_VarCurr,bitIndex23) ),
inference(cnf_transformation,[],[f138046]) ).
tcf(c_156809,plain,
( v26522(sK23533_VarCurr,bitIndex23)
| v28941(sK23533_VarCurr,bitIndex23)
| ~ sP24043 ),
inference(cnf_transformation,[],[f138045]) ).
tcf(c_156810,plain,
( ~ sP24044
| ~ v26522(sK23533_VarCurr,bitIndex22)
| ~ v28941(sK23533_VarCurr,bitIndex22) ),
inference(cnf_transformation,[],[f138048]) ).
tcf(c_156811,plain,
( v26522(sK23533_VarCurr,bitIndex22)
| v28941(sK23533_VarCurr,bitIndex22)
| ~ sP24044 ),
inference(cnf_transformation,[],[f138047]) ).
tcf(c_156812,plain,
( ~ sP24045
| ~ v26522(sK23533_VarCurr,bitIndex21)
| ~ v28941(sK23533_VarCurr,bitIndex21) ),
inference(cnf_transformation,[],[f138050]) ).
tcf(c_156813,plain,
( v26522(sK23533_VarCurr,bitIndex21)
| v28941(sK23533_VarCurr,bitIndex21)
| ~ sP24045 ),
inference(cnf_transformation,[],[f138049]) ).
tcf(c_156814,plain,
( ~ sP24046
| ~ v26522(sK23533_VarCurr,bitIndex20)
| ~ v28941(sK23533_VarCurr,bitIndex20) ),
inference(cnf_transformation,[],[f138052]) ).
tcf(c_156815,plain,
( v26522(sK23533_VarCurr,bitIndex20)
| v28941(sK23533_VarCurr,bitIndex20)
| ~ sP24046 ),
inference(cnf_transformation,[],[f138051]) ).
tcf(c_156816,plain,
( ~ sP24047
| ~ v26522(sK23533_VarCurr,bitIndex19)
| ~ v28941(sK23533_VarCurr,bitIndex19) ),
inference(cnf_transformation,[],[f138054]) ).
tcf(c_156817,plain,
( v26522(sK23533_VarCurr,bitIndex19)
| v28941(sK23533_VarCurr,bitIndex19)
| ~ sP24047 ),
inference(cnf_transformation,[],[f138053]) ).
tcf(c_156818,plain,
( ~ sP24048
| ~ v26522(sK23533_VarCurr,bitIndex18)
| ~ v28941(sK23533_VarCurr,bitIndex18) ),
inference(cnf_transformation,[],[f138056]) ).
tcf(c_156819,plain,
( v26522(sK23533_VarCurr,bitIndex18)
| v28941(sK23533_VarCurr,bitIndex18)
| ~ sP24048 ),
inference(cnf_transformation,[],[f138055]) ).
tcf(c_156820,plain,
( ~ sP24049
| ~ v26522(sK23533_VarCurr,bitIndex17)
| ~ v28941(sK23533_VarCurr,bitIndex17) ),
inference(cnf_transformation,[],[f138058]) ).
tcf(c_156821,plain,
( v26522(sK23533_VarCurr,bitIndex17)
| v28941(sK23533_VarCurr,bitIndex17)
| ~ sP24049 ),
inference(cnf_transformation,[],[f138057]) ).
tcf(c_156822,plain,
( ~ sP24050
| ~ v26522(sK23533_VarCurr,bitIndex16)
| ~ v28941(sK23533_VarCurr,bitIndex16) ),
inference(cnf_transformation,[],[f138060]) ).
tcf(c_156823,plain,
( v26522(sK23533_VarCurr,bitIndex16)
| v28941(sK23533_VarCurr,bitIndex16)
| ~ sP24050 ),
inference(cnf_transformation,[],[f138059]) ).
tcf(c_156824,plain,
( ~ sP24051
| ~ v26522(sK23533_VarCurr,bitIndex15)
| ~ v28941(sK23533_VarCurr,bitIndex15) ),
inference(cnf_transformation,[],[f138062]) ).
tcf(c_156825,plain,
( v26522(sK23533_VarCurr,bitIndex15)
| v28941(sK23533_VarCurr,bitIndex15)
| ~ sP24051 ),
inference(cnf_transformation,[],[f138061]) ).
tcf(c_156826,plain,
( ~ sP24052
| ~ v26522(sK23533_VarCurr,bitIndex14)
| ~ v28941(sK23533_VarCurr,bitIndex14) ),
inference(cnf_transformation,[],[f138064]) ).
tcf(c_156827,plain,
( v26522(sK23533_VarCurr,bitIndex14)
| v28941(sK23533_VarCurr,bitIndex14)
| ~ sP24052 ),
inference(cnf_transformation,[],[f138063]) ).
tcf(c_156828,plain,
( ~ sP24053
| ~ v26522(sK23533_VarCurr,bitIndex13)
| ~ v28941(sK23533_VarCurr,bitIndex13) ),
inference(cnf_transformation,[],[f138066]) ).
tcf(c_156829,plain,
( v26522(sK23533_VarCurr,bitIndex13)
| v28941(sK23533_VarCurr,bitIndex13)
| ~ sP24053 ),
inference(cnf_transformation,[],[f138065]) ).
tcf(c_156830,plain,
( ~ sP24054
| ~ v26522(sK23533_VarCurr,bitIndex12)
| ~ v28941(sK23533_VarCurr,bitIndex12) ),
inference(cnf_transformation,[],[f138068]) ).
tcf(c_156831,plain,
( v26522(sK23533_VarCurr,bitIndex12)
| v28941(sK23533_VarCurr,bitIndex12)
| ~ sP24054 ),
inference(cnf_transformation,[],[f138067]) ).
tcf(c_156832,plain,
( ~ sP24055
| ~ v26522(sK23533_VarCurr,bitIndex11)
| ~ v28941(sK23533_VarCurr,bitIndex11) ),
inference(cnf_transformation,[],[f138070]) ).
tcf(c_156833,plain,
( v26522(sK23533_VarCurr,bitIndex11)
| v28941(sK23533_VarCurr,bitIndex11)
| ~ sP24055 ),
inference(cnf_transformation,[],[f138069]) ).
tcf(c_156834,plain,
( ~ sP24056
| ~ v26522(sK23533_VarCurr,bitIndex10)
| ~ v28941(sK23533_VarCurr,bitIndex10) ),
inference(cnf_transformation,[],[f138072]) ).
tcf(c_156835,plain,
( v26522(sK23533_VarCurr,bitIndex10)
| v28941(sK23533_VarCurr,bitIndex10)
| ~ sP24056 ),
inference(cnf_transformation,[],[f138071]) ).
tcf(c_156836,plain,
( ~ sP24057
| ~ v26522(sK23533_VarCurr,bitIndex9)
| ~ v28941(sK23533_VarCurr,bitIndex9) ),
inference(cnf_transformation,[],[f138074]) ).
tcf(c_156837,plain,
( v26522(sK23533_VarCurr,bitIndex9)
| v28941(sK23533_VarCurr,bitIndex9)
| ~ sP24057 ),
inference(cnf_transformation,[],[f138073]) ).
tcf(c_156838,plain,
( ~ sP24058
| ~ v26522(sK23533_VarCurr,bitIndex8)
| ~ v28941(sK23533_VarCurr,bitIndex8) ),
inference(cnf_transformation,[],[f138076]) ).
tcf(c_156839,plain,
( v26522(sK23533_VarCurr,bitIndex8)
| v28941(sK23533_VarCurr,bitIndex8)
| ~ sP24058 ),
inference(cnf_transformation,[],[f138075]) ).
tcf(c_156840,plain,
( ~ sP24059
| ~ v26522(sK23533_VarCurr,bitIndex7)
| ~ v28941(sK23533_VarCurr,bitIndex7) ),
inference(cnf_transformation,[],[f138078]) ).
tcf(c_156841,plain,
( v26522(sK23533_VarCurr,bitIndex7)
| v28941(sK23533_VarCurr,bitIndex7)
| ~ sP24059 ),
inference(cnf_transformation,[],[f138077]) ).
tcf(c_156842,plain,
( ~ sP24060
| ~ v26522(sK23533_VarCurr,bitIndex6)
| ~ v28941(sK23533_VarCurr,bitIndex6) ),
inference(cnf_transformation,[],[f138080]) ).
tcf(c_156843,plain,
( v26522(sK23533_VarCurr,bitIndex6)
| v28941(sK23533_VarCurr,bitIndex6)
| ~ sP24060 ),
inference(cnf_transformation,[],[f138079]) ).
tcf(c_156844,plain,
( ~ sP24061
| ~ v26522(sK23533_VarCurr,bitIndex5)
| ~ v28941(sK23533_VarCurr,bitIndex5) ),
inference(cnf_transformation,[],[f138082]) ).
tcf(c_156845,plain,
( v26522(sK23533_VarCurr,bitIndex5)
| v28941(sK23533_VarCurr,bitIndex5)
| ~ sP24061 ),
inference(cnf_transformation,[],[f138081]) ).
tcf(c_156846,plain,
( ~ sP24062
| ~ v26522(sK23533_VarCurr,bitIndex4)
| ~ v28941(sK23533_VarCurr,bitIndex4) ),
inference(cnf_transformation,[],[f138084]) ).
tcf(c_156847,plain,
( v26522(sK23533_VarCurr,bitIndex4)
| v28941(sK23533_VarCurr,bitIndex4)
| ~ sP24062 ),
inference(cnf_transformation,[],[f138083]) ).
tcf(c_156848,plain,
( ~ sP24063
| ~ v26522(sK23533_VarCurr,bitIndex3)
| ~ v28941(sK23533_VarCurr,bitIndex3) ),
inference(cnf_transformation,[],[f138086]) ).
tcf(c_156849,plain,
( v26522(sK23533_VarCurr,bitIndex3)
| v28941(sK23533_VarCurr,bitIndex3)
| ~ sP24063 ),
inference(cnf_transformation,[],[f138085]) ).
tcf(c_156857,plain,
! [X0: $i] :
( ~ v21(X0)
| ~ v23(X0)
| ~ sP38_aig_name(X0) ),
inference(cnf_transformation,[],[f2577]) ).
tcf(c_157006,plain,
! [X0: $i,X1: $i] :
( v4914(X0)
| v28945(X0,X1)
| ~ v81(X0)
| ~ v28946(X0,X1) ),
inference(cnf_transformation,[],[f137656]) ).
tcf(c_157007,plain,
! [X0: $i,X1: $i] :
( v4914(X0)
| v28946(X0,X1)
| ~ v81(X0)
| ~ v28945(X0,X1) ),
inference(cnf_transformation,[],[f137655]) ).
tcf(c_157490,plain,
! [X0: $i,X1: $i] :
( sP38_aig_name(X0)
| v26522(X0,X1)
| ~ v28945(X0,X1) ),
inference(cnf_transformation,[],[f137660]) ).
tcf(c_157491,plain,
! [X0: $i,X1: $i] :
( sP38_aig_name(X0)
| v28945(X0,X1)
| ~ v26522(X0,X1) ),
inference(cnf_transformation,[],[f137659]) ).
tcf(c_157495,plain,
! [X0: $i] :
( ~ sP38_aig_name(X0)
| ~ v69(X0) ),
inference(cnf_transformation,[],[f2576]) ).
tcf(c_157727,plain,
! [X0: $i,X1: $i] :
( ~ v4914(X0)
| ~ v28945(X0,X1) ),
inference(cnf_transformation,[],[f137658]) ).
tcf(c_157728,plain,
! [X0: $i,X1: $i] :
( v81(X0)
| ~ v28945(X0,X1) ),
inference(cnf_transformation,[],[f137657]) ).
tcf(c_170196,plain,
! [X0: $i,X1: $i] :
( v28946(X0,X1)
| ~ v28945(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_157007,c_157727,c_157728]) ).
tcf(c_175390,plain,
! [X0: $i] :
( v21(sK23533_VarCurr)
| ~ sP38_aig_name(X0)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_157495,c_156714]) ).
tcf(c_175391,plain,
( v21(sK23533_VarCurr)
| ~ sP38_aig_name(sK23533_VarCurr) ),
inference(unflattening,[status(thm)],[c_175390]) ).
tcf(c_175398,plain,
! [X0: $i] :
( v23(sK23533_VarCurr)
| ~ sP38_aig_name(X0)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_157495,c_156713]) ).
tcf(c_175399,plain,
( v23(sK23533_VarCurr)
| ~ sP38_aig_name(sK23533_VarCurr) ),
inference(unflattening,[status(thm)],[c_175398]) ).
tcf(c_175768,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP38_aig_name(X0)
| v28946(X1,X3)
| ~ v26522(X0,X2)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_157491,c_170196]) ).
tcf(c_175769,plain,
! [X0: $i,X1: $i] :
( sP38_aig_name(X0)
| v28946(X0,X1)
| ~ v26522(X0,X1) ),
inference(unflattening,[status(thm)],[c_175768]) ).
tcf(c_175808,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( v4914(X0)
| sP38_aig_name(X1)
| v26522(X1,X3)
| ~ v81(X0)
| ~ v28946(X0,X2)
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution_lifted,[status(thm)],[c_157006,c_157490]) ).
tcf(c_175809,plain,
! [X0: $i,X1: $i] :
( v4914(X0)
| sP38_aig_name(X0)
| v26522(X0,X1)
| ~ v81(X0)
| ~ v28946(X0,X1) ),
inference(unflattening,[status(thm)],[c_175808]) ).
tcf(c_177762,plain,
! [X0: $i] :
( ~ sP38_aig_name(sK23533_VarCurr)
| ~ v23(X0)
| ~ sP38_aig_name(X0)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_156857,c_175391]) ).
tcf(c_177763,plain,
( ~ v23(sK23533_VarCurr)
| ~ sP38_aig_name(sK23533_VarCurr) ),
inference(unflattening,[status(thm)],[c_177762]) ).
tcf(c_177764,plain,
~ sP38_aig_name(sK23533_VarCurr),
inference(global_subsumption_just,[status(thm)],[c_177763,c_175399,c_177763]) ).
tcf(c_178321,plain,
! [X0: $i,X1: $i] :
( v4914(X0)
| v26522(X0,X1)
| ~ v81(X0)
| ~ v28946(X0,X1)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_175809,c_177764]) ).
tcf(c_178322,plain,
! [X0: $i] :
( v4914(sK23533_VarCurr)
| v26522(sK23533_VarCurr,X0)
| ~ v81(sK23533_VarCurr)
| ~ v28946(sK23533_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_178321]) ).
tcf(c_178324,plain,
! [X0: $i] :
( ~ v28946(sK23533_VarCurr,X0)
| v26522(sK23533_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_178322,c_156703,c_156702,c_178322]) ).
tcf(c_178325,plain,
! [X0: $i] :
( v26522(sK23533_VarCurr,X0)
| ~ v28946(sK23533_VarCurr,X0) ),
inference(renaming,[status(thm)],[c_178324]) ).
tcf(c_178337,plain,
! [X0: $i,X1: $i] :
( v28946(X0,X1)
| ~ v26522(X0,X1)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_175769,c_177764]) ).
tcf(c_178338,plain,
! [X0: $i] :
( v28946(sK23533_VarCurr,X0)
| ~ v26522(sK23533_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_178337]) ).
tcf(c_178339,plain,
( v28946(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex0) ),
inference(instantiation,[status(thm)],[c_178338]) ).
tcf(c_180821,plain,
! [X0: $i,X1: $i] :
( v28941(X0,X1)
| ~ v28946(X0,X1)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_156726,c_156704]) ).
tcf(c_180822,plain,
! [X0: $i] :
( v28941(sK23533_VarCurr,X0)
| ~ v28946(sK23533_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_180821]) ).
tcf(c_180823,plain,
( v28941(sK23533_VarCurr,bitIndex0)
| ~ v28946(sK23533_VarCurr,bitIndex0) ),
inference(instantiation,[status(thm)],[c_180822]) ).
tcf(c_202858,plain,
! [X0: $i,X1: $i] :
( v4914(X0)
| sP38_aig_name(X0)
| v26522(X0,X1)
| ~ v28946(X0,X1)
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_175809,c_156703]) ).
tcf(c_202859,plain,
! [X0: $i] :
( v4914(sK23533_VarCurr)
| sP38_aig_name(sK23533_VarCurr)
| v26522(sK23533_VarCurr,X0)
| ~ v28946(sK23533_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_202858]) ).
tcf(c_202861,plain,
! [X0: $i] :
( v26522(sK23533_VarCurr,X0)
| ~ v28946(sK23533_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_202859,c_178325]) ).
tcf(c_203173,plain,
! [X0: $i,X1: $i,X2: $i] :
( v28947(X0)
| v26522(sK23533_VarCurr,X2)
| ~ v28941(X0,X1)
| ( X1 != X2 )
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_156725,c_202861]) ).
tcf(c_203174,plain,
! [X0: $i] :
( v28947(sK23533_VarCurr)
| v26522(sK23533_VarCurr,X0)
| ~ v28941(sK23533_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_203173]) ).
tcf(c_203176,plain,
! [X0: $i] :
( ~ v28941(sK23533_VarCurr,X0)
| v26522(sK23533_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_203174,c_156704,c_203174]) ).
tcf(c_203177,plain,
! [X0: $i] :
( v26522(sK23533_VarCurr,X0)
| ~ v28941(sK23533_VarCurr,X0) ),
inference(renaming,[status(thm)],[c_203176]) ).
tcf(c_203178,plain,
( v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
inference(instantiation,[status(thm)],[c_203177]) ).
tcf(c_203204,plain,
( v26522(sK23533_VarCurr,bitIndex20)
| ~ sP24046 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156815,c_203177]) ).
tcf(c_203205,plain,
( v26522(sK23533_VarCurr,bitIndex16)
| ~ sP24050 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156823,c_203177]) ).
tcf(c_203206,plain,
( v26522(sK23533_VarCurr,bitIndex8)
| ~ sP24058 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156839,c_203177]) ).
tcf(c_203207,plain,
( v26522(sK23533_VarCurr,bitIndex40)
| ~ sP24026 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156775,c_203177]) ).
tcf(c_203208,plain,
( v26522(sK23533_VarCurr,bitIndex56)
| ~ sP24010 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156743,c_203177]) ).
tcf(c_203209,plain,
( v26522(sK23533_VarCurr,bitIndex32)
| ~ sP24034 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156791,c_203177]) ).
tcf(c_203210,plain,
( v26522(sK23533_VarCurr,bitIndex36)
| ~ sP24030 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156783,c_203177]) ).
tcf(c_203211,plain,
( v26522(sK23533_VarCurr,bitIndex29)
| ~ sP24037 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156797,c_203177]) ).
tcf(c_203212,plain,
( v26522(sK23533_VarCurr,bitIndex52)
| ~ sP24014 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156751,c_203177]) ).
tcf(c_203213,plain,
( v26522(sK23533_VarCurr,bitIndex48)
| ~ sP24018 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156759,c_203177]) ).
tcf(c_203214,plain,
( v26522(sK23533_VarCurr,bitIndex44)
| ~ sP24022 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156767,c_203177]) ).
tcf(c_203215,plain,
( v26522(sK23533_VarCurr,bitIndex24)
| ~ sP24042 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156807,c_203177]) ).
tcf(c_203216,plain,
( v26522(sK23533_VarCurr,bitIndex19)
| ~ sP24047 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156817,c_203177]) ).
tcf(c_203217,plain,
( v26522(sK23533_VarCurr,bitIndex43)
| ~ sP24023 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156769,c_203177]) ).
tcf(c_203218,plain,
( v26522(sK23533_VarCurr,bitIndex59)
| ~ sP24007 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156737,c_203177]) ).
tcf(c_203219,plain,
( v26522(sK23533_VarCurr,bitIndex53)
| ~ sP24013 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156749,c_203177]) ).
tcf(c_203220,plain,
( v26522(sK23533_VarCurr,bitIndex51)
| ~ sP24015 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156753,c_203177]) ).
tcf(c_203221,plain,
( v26522(sK23533_VarCurr,bitIndex28)
| ~ sP24038 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156799,c_203177]) ).
tcf(c_203222,plain,
( v26522(sK23533_VarCurr,bitIndex45)
| ~ sP24021 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156765,c_203177]) ).
tcf(c_203223,plain,
( v26522(sK23533_VarCurr,bitIndex15)
| ~ sP24051 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156825,c_203177]) ).
tcf(c_203224,plain,
( v26522(sK23533_VarCurr,bitIndex23)
| ~ sP24043 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156809,c_203177]) ).
tcf(c_203225,plain,
( v26522(sK23533_VarCurr,bitIndex7)
| ~ sP24059 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156841,c_203177]) ).
tcf(c_203226,plain,
( v26522(sK23533_VarCurr,bitIndex13)
| ~ sP24053 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156829,c_203177]) ).
tcf(c_203227,plain,
( v26522(sK23533_VarCurr,bitIndex39)
| ~ sP24027 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156777,c_203177]) ).
tcf(c_203228,plain,
( v26522(sK23533_VarCurr,bitIndex37)
| ~ sP24029 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156781,c_203177]) ).
tcf(c_203229,plain,
( v26522(sK23533_VarCurr,bitIndex41)
| ~ sP24025 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156773,c_203177]) ).
tcf(c_203230,plain,
( v26522(sK23533_VarCurr,bitIndex57)
| ~ sP24009 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156741,c_203177]) ).
tcf(c_203231,plain,
( v26522(sK23533_VarCurr,bitIndex55)
| ~ sP24011 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156745,c_203177]) ).
tcf(c_203232,plain,
( v26522(sK23533_VarCurr,bitIndex49)
| ~ sP24017 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156757,c_203177]) ).
tcf(c_203233,plain,
( v26522(sK23533_VarCurr,bitIndex31)
| ~ sP24035 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156793,c_203177]) ).
tcf(c_203234,plain,
( v26522(sK23533_VarCurr,bitIndex47)
| ~ sP24019 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156761,c_203177]) ).
tcf(c_203235,plain,
( v26522(sK23533_VarCurr,bitIndex11)
| ~ sP24055 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156833,c_203177]) ).
tcf(c_203236,plain,
( v26522(sK23533_VarCurr,bitIndex35)
| ~ sP24031 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156785,c_203177]) ).
tcf(c_203237,plain,
( v26522(sK23533_VarCurr,bitIndex33)
| ~ sP24033 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156789,c_203177]) ).
tcf(c_203238,plain,
( v26522(sK23533_VarCurr,bitIndex27)
| ~ sP24039 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156801,c_203177]) ).
tcf(c_203239,plain,
( v26522(sK23533_VarCurr,bitIndex4)
| ~ sP24062 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156847,c_203177]) ).
tcf(c_203240,plain,
( v26522(sK23533_VarCurr,bitIndex9)
| ~ sP24057 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156837,c_203177]) ).
tcf(c_203241,plain,
( v26522(sK23533_VarCurr,bitIndex42)
| ~ sP24024 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156771,c_203177]) ).
tcf(c_203242,plain,
( v26522(sK23533_VarCurr,bitIndex58)
| ~ sP24008 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156739,c_203177]) ).
tcf(c_203243,plain,
( v26522(sK23533_VarCurr,bitIndex54)
| ~ sP24012 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156747,c_203177]) ).
tcf(c_203244,plain,
( v26522(sK23533_VarCurr,bitIndex50)
| ~ sP24016 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156755,c_203177]) ).
tcf(c_203245,plain,
( v26522(sK23533_VarCurr,bitIndex34)
| ~ sP24032 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156787,c_203177]) ).
tcf(c_203246,plain,
( v26522(sK23533_VarCurr,bitIndex46)
| ~ sP24020 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156763,c_203177]) ).
tcf(c_203247,plain,
( v26522(sK23533_VarCurr,bitIndex18)
| ~ sP24048 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156819,c_203177]) ).
tcf(c_203248,plain,
( v26522(sK23533_VarCurr,bitIndex5)
| ~ sP24061 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156845,c_203177]) ).
tcf(c_203249,plain,
( v26522(sK23533_VarCurr,bitIndex21)
| ~ sP24045 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156813,c_203177]) ).
tcf(c_203250,plain,
( v26522(sK23533_VarCurr,bitIndex25)
| ~ sP24041 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156805,c_203177]) ).
tcf(c_203251,plain,
( v26522(sK23533_VarCurr,bitIndex30)
| ~ sP24036 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156795,c_203177]) ).
tcf(c_203252,plain,
( v26522(sK23533_VarCurr,bitIndex10)
| ~ sP24056 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156835,c_203177]) ).
tcf(c_203253,plain,
( v26522(sK23533_VarCurr,bitIndex26)
| ~ sP24040 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156803,c_203177]) ).
tcf(c_203254,plain,
( v26522(sK23533_VarCurr,bitIndex3)
| ~ sP24063 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156849,c_203177]) ).
tcf(c_203255,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex0)
| v28941(sK23533_VarCurr,bitIndex2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156705,c_203177]) ).
tcf(c_203256,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156709,c_203177]) ).
tcf(c_203257,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156706,c_203177]) ).
tcf(c_203258,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156710,c_203177]) ).
tcf(c_203259,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| v26522(sK23533_VarCurr,bitIndex2)
| v28941(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156707,c_203177]) ).
tcf(c_203260,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156711,c_203177]) ).
tcf(c_203261,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156708,c_203177]) ).
tcf(c_203262,plain,
( v26522(sK23533_VarCurr,bitIndex12)
| ~ sP24054 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156831,c_203177]) ).
tcf(c_203263,plain,
( v26522(sK23533_VarCurr,bitIndex6)
| ~ sP24060 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156843,c_203177]) ).
tcf(c_203264,plain,
( v26522(sK23533_VarCurr,bitIndex22)
| ~ sP24044 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156811,c_203177]) ).
tcf(c_203265,plain,
( v26522(sK23533_VarCurr,bitIndex38)
| ~ sP24028 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156779,c_203177]) ).
tcf(c_203266,plain,
( v26522(sK23533_VarCurr,bitIndex17)
| ~ sP24049 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156821,c_203177]) ).
tcf(c_203267,plain,
( v26522(sK23533_VarCurr,bitIndex14)
| ~ sP24052 ),
inference(backward_subsumption_resolution,[status(thm)],[c_156827,c_203177]) ).
tcf(c_203269,plain,
( ~ sP24046
| ~ v28941(sK23533_VarCurr,bitIndex20) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156814,c_203177]) ).
tcf(c_203270,plain,
( ~ sP24050
| ~ v28941(sK23533_VarCurr,bitIndex16) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156822,c_203177]) ).
tcf(c_203271,plain,
( ~ sP24058
| ~ v28941(sK23533_VarCurr,bitIndex8) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156838,c_203177]) ).
tcf(c_203272,plain,
( ~ sP24010
| ~ v28941(sK23533_VarCurr,bitIndex56) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156742,c_203177]) ).
tcf(c_203273,plain,
( ~ sP24018
| ~ v28941(sK23533_VarCurr,bitIndex48) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156758,c_203177]) ).
tcf(c_203274,plain,
( ~ sP24034
| ~ v28941(sK23533_VarCurr,bitIndex32) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156790,c_203177]) ).
tcf(c_203275,plain,
( ~ sP24030
| ~ v28941(sK23533_VarCurr,bitIndex36) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156782,c_203177]) ).
tcf(c_203276,plain,
( ~ sP24037
| ~ v28941(sK23533_VarCurr,bitIndex29) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156796,c_203177]) ).
tcf(c_203277,plain,
( ~ sP24014
| ~ v28941(sK23533_VarCurr,bitIndex52) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156750,c_203177]) ).
tcf(c_203278,plain,
( ~ sP24026
| ~ v28941(sK23533_VarCurr,bitIndex40) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156774,c_203177]) ).
tcf(c_203279,plain,
( ~ sP24022
| ~ v28941(sK23533_VarCurr,bitIndex44) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156766,c_203177]) ).
tcf(c_203280,plain,
( ~ sP24023
| ~ v28941(sK23533_VarCurr,bitIndex43) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156768,c_203177]) ).
tcf(c_203281,plain,
( ~ sP24042
| ~ v28941(sK23533_VarCurr,bitIndex24) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156806,c_203177]) ).
tcf(c_203282,plain,
( ~ sP24047
| ~ v28941(sK23533_VarCurr,bitIndex19) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156816,c_203177]) ).
tcf(c_203283,plain,
( ~ sP24007
| ~ v28941(sK23533_VarCurr,bitIndex59) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156736,c_203177]) ).
tcf(c_203284,plain,
( ~ sP24021
| ~ v28941(sK23533_VarCurr,bitIndex45) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156764,c_203177]) ).
tcf(c_203285,plain,
( ~ sP24013
| ~ v28941(sK23533_VarCurr,bitIndex53) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156748,c_203177]) ).
tcf(c_203286,plain,
( ~ sP24015
| ~ v28941(sK23533_VarCurr,bitIndex51) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156752,c_203177]) ).
tcf(c_203287,plain,
( ~ sP24038
| ~ v28941(sK23533_VarCurr,bitIndex28) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156798,c_203177]) ).
tcf(c_203288,plain,
( ~ sP24051
| ~ v28941(sK23533_VarCurr,bitIndex15) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156824,c_203177]) ).
tcf(c_203289,plain,
( ~ sP24043
| ~ v28941(sK23533_VarCurr,bitIndex23) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156808,c_203177]) ).
tcf(c_203290,plain,
( ~ sP24059
| ~ v28941(sK23533_VarCurr,bitIndex7) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156840,c_203177]) ).
tcf(c_203291,plain,
( ~ sP24027
| ~ v28941(sK23533_VarCurr,bitIndex39) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156776,c_203177]) ).
tcf(c_203292,plain,
( ~ sP24029
| ~ v28941(sK23533_VarCurr,bitIndex37) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156780,c_203177]) ).
tcf(c_203293,plain,
( ~ sP24053
| ~ v28941(sK23533_VarCurr,bitIndex13) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156828,c_203177]) ).
tcf(c_203294,plain,
( ~ sP24009
| ~ v28941(sK23533_VarCurr,bitIndex57) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156740,c_203177]) ).
tcf(c_203295,plain,
( ~ sP24019
| ~ v28941(sK23533_VarCurr,bitIndex47) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156760,c_203177]) ).
tcf(c_203296,plain,
( ~ sP24011
| ~ v28941(sK23533_VarCurr,bitIndex55) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156744,c_203177]) ).
tcf(c_203297,plain,
( ~ sP24017
| ~ v28941(sK23533_VarCurr,bitIndex49) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156756,c_203177]) ).
tcf(c_203298,plain,
( ~ sP24035
| ~ v28941(sK23533_VarCurr,bitIndex31) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156792,c_203177]) ).
tcf(c_203299,plain,
( ~ sP24025
| ~ v28941(sK23533_VarCurr,bitIndex41) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156772,c_203177]) ).
tcf(c_203300,plain,
( ~ sP24031
| ~ v28941(sK23533_VarCurr,bitIndex35) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156784,c_203177]) ).
tcf(c_203301,plain,
( ~ sP24033
| ~ v28941(sK23533_VarCurr,bitIndex33) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156788,c_203177]) ).
tcf(c_203302,plain,
( ~ sP24039
| ~ v28941(sK23533_VarCurr,bitIndex27) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156800,c_203177]) ).
tcf(c_203303,plain,
( ~ sP24055
| ~ v28941(sK23533_VarCurr,bitIndex11) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156832,c_203177]) ).
tcf(c_203304,plain,
( ~ sP24057
| ~ v28941(sK23533_VarCurr,bitIndex9) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156836,c_203177]) ).
tcf(c_203305,plain,
( ~ sP24062
| ~ v28941(sK23533_VarCurr,bitIndex4) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156846,c_203177]) ).
tcf(c_203306,plain,
( ~ sP24008
| ~ v28941(sK23533_VarCurr,bitIndex58) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156738,c_203177]) ).
tcf(c_203307,plain,
( ~ sP24020
| ~ v28941(sK23533_VarCurr,bitIndex46) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156762,c_203177]) ).
tcf(c_203308,plain,
( ~ sP24012
| ~ v28941(sK23533_VarCurr,bitIndex54) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156746,c_203177]) ).
tcf(c_203309,plain,
( ~ sP24016
| ~ v28941(sK23533_VarCurr,bitIndex50) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156754,c_203177]) ).
tcf(c_203310,plain,
( ~ sP24032
| ~ v28941(sK23533_VarCurr,bitIndex34) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156786,c_203177]) ).
tcf(c_203311,plain,
( ~ sP24024
| ~ v28941(sK23533_VarCurr,bitIndex42) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156770,c_203177]) ).
tcf(c_203312,plain,
( ~ sP24048
| ~ v28941(sK23533_VarCurr,bitIndex18) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156818,c_203177]) ).
tcf(c_203313,plain,
( ~ sP24061
| ~ v28941(sK23533_VarCurr,bitIndex5) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156844,c_203177]) ).
tcf(c_203314,plain,
( ~ sP24045
| ~ v28941(sK23533_VarCurr,bitIndex21) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156812,c_203177]) ).
tcf(c_203315,plain,
( ~ sP24041
| ~ v28941(sK23533_VarCurr,bitIndex25) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156804,c_203177]) ).
tcf(c_203316,plain,
( ~ sP24036
| ~ v28941(sK23533_VarCurr,bitIndex30) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156794,c_203177]) ).
tcf(c_203317,plain,
( ~ sP24040
| ~ v28941(sK23533_VarCurr,bitIndex26) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156802,c_203177]) ).
tcf(c_203318,plain,
( ~ sP24056
| ~ v28941(sK23533_VarCurr,bitIndex10) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156834,c_203177]) ).
tcf(c_203319,plain,
( ~ sP24063
| ~ v28941(sK23533_VarCurr,bitIndex3) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156848,c_203177]) ).
tcf(c_203320,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| sP24007
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156712,c_203177]) ).
tcf(c_203321,plain,
( ~ sP24044
| ~ v28941(sK23533_VarCurr,bitIndex22) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156810,c_203177]) ).
tcf(c_203322,plain,
( ~ sP24054
| ~ v28941(sK23533_VarCurr,bitIndex12) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156830,c_203177]) ).
tcf(c_203323,plain,
( ~ sP24060
| ~ v28941(sK23533_VarCurr,bitIndex6) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156842,c_203177]) ).
tcf(c_203324,plain,
( ~ sP24028
| ~ v28941(sK23533_VarCurr,bitIndex38) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156778,c_203177]) ).
tcf(c_203325,plain,
( ~ sP24049
| ~ v28941(sK23533_VarCurr,bitIndex17) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156820,c_203177]) ).
tcf(c_203326,plain,
( ~ sP24052
| ~ v28941(sK23533_VarCurr,bitIndex14) ),
inference(backward_subsumption_resolution,[status(thm)],[c_156826,c_203177]) ).
tcf(c_204171,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_203320,c_203283]) ).
tcf(c_204172,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204171,c_178339,c_180823,c_203320,c_203283]) ).
tcf(c_204173,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_204172]) ).
tcf(c_204174,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204173,c_203178,c_203261,c_203257,c_203283,c_204173]) ).
tcf(c_204175,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_204174]) ).
tcf(c_204296,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_203320,c_203218]) ).
tcf(c_204297,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204296,c_178339,c_180823,c_203218,c_203320]) ).
tcf(c_204298,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_204297]) ).
tcf(c_204299,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204298,c_203178,c_203261,c_203257,c_203218,c_204298]) ).
tcf(c_204300,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_204299]) ).
tcf(c_204427,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_203260,c_203283]) ).
tcf(c_204428,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_204427,c_178339,c_180823,c_204427]) ).
tcf(c_204430,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_204428,c_203178,c_203259,c_203283,c_204428]) ).
tcf(c_204431,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_204430]) ).
tcf(c_204552,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_203260,c_203218]) ).
tcf(c_204553,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_204552,c_178339,c_180823,c_204552]) ).
tcf(c_204555,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex1) ),
inference(global_subsumption_just,[status(thm)],[c_204553,c_203178,c_203259,c_203218,c_204553]) ).
tcf(c_204556,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(renaming,[status(thm)],[c_204555]) ).
tcf(c_204683,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(resolution,[status(thm)],[c_203258,c_203283]) ).
tcf(c_204684,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204683,c_178339,c_180823,c_203258,c_203283]) ).
tcf(c_204686,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204684,c_203178,c_203257,c_203283,c_204684]) ).
tcf(c_204687,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(renaming,[status(thm)],[c_204686]) ).
tcf(c_204808,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(resolution,[status(thm)],[c_203258,c_203218]) ).
tcf(c_204809,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204808,c_178339,c_180823,c_204808]) ).
tcf(c_204811,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_204809,c_203178,c_203257,c_203218,c_204809]) ).
tcf(c_204812,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2) ),
inference(renaming,[status(thm)],[c_204811]) ).
tcf(c_204939,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
inference(resolution,[status(thm)],[c_203256,c_203283]) ).
tcf(c_204940,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex59) ),
inference(global_subsumption_just,[status(thm)],[c_204939,c_178339,c_180823,c_203256,c_203283]) ).
tcf(c_204942,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59) ),
inference(global_subsumption_just,[status(thm)],[c_204940,c_203178,c_203255,c_203283,c_204940]) ).
tcf(c_205064,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0)
| ~ v28941(sK23533_VarCurr,bitIndex0) ),
inference(resolution,[status(thm)],[c_203256,c_203218]) ).
tcf(c_205065,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex0) ),
inference(global_subsumption_just,[status(thm)],[c_205064,c_178339,c_180823,c_203256,c_203218]) ).
tcf(c_205067,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| v28941(sK23533_VarCurr,bitIndex2) ),
inference(global_subsumption_just,[status(thm)],[c_205065,c_203178,c_203255,c_203218,c_205065]) ).
tcf(c_308892,plain,
( sP24063
| sP24062
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex5)
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_204556,c_203248]) ).
tcf(c_309376,plain,
( sP24063
| sP24062
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex5)
| ~ v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(resolution,[status(thm)],[c_204300,c_203248]) ).
tcf(c_315451,plain,
! [X0: $i,X1: $i,X2: $i] :
( v28947(X0)
| v26522(sK23533_VarCurr,X2)
| ~ v28941(X0,X1)
| ( X1 != X2 )
| ( X0 != sK23533_VarCurr ) ),
inference(resolution_lifted,[status(thm)],[c_156725,c_202861]) ).
tcf(c_315452,plain,
! [X0: $i] :
( v28947(sK23533_VarCurr)
| v26522(sK23533_VarCurr,X0)
| ~ v28941(sK23533_VarCurr,X0) ),
inference(unflattening,[status(thm)],[c_315451]) ).
tcf(c_315453,plain,
! [X0: $i] :
( ~ v28941(sK23533_VarCurr,X0)
| v26522(sK23533_VarCurr,X0) ),
inference(global_subsumption_just,[status(thm)],[c_315452,c_156704,c_203174]) ).
tcf(c_315454,plain,
! [X0: $i] :
( v26522(sK23533_VarCurr,X0)
| ~ v28941(sK23533_VarCurr,X0) ),
inference(renaming,[status(thm)],[c_315453]) ).
tcf(c_315480,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex59) ),
inference(backward_subsumption_resolution,[status(thm)],[c_204942,c_315454]) ).
tcf(c_315481,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex59)
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_205067,c_315454]) ).
tcf(c_315485,plain,
( sP24063
| sP24062
| sP24061
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_204431,c_315454]) ).
tcf(c_418871,plain,
( sP24063
| sP24062
| sP24060
| sP24059
| sP24058
| sP24057
| sP24056
| sP24055
| sP24054
| sP24053
| sP24052
| sP24051
| sP24050
| sP24049
| sP24048
| sP24047
| sP24046
| sP24045
| sP24044
| sP24043
| sP24042
| sP24041
| sP24040
| sP24039
| sP24038
| sP24037
| sP24036
| sP24035
| sP24034
| sP24033
| sP24032
| sP24031
| sP24030
| sP24029
| sP24028
| sP24027
| sP24026
| sP24025
| sP24024
| sP24023
| sP24022
| sP24021
| sP24020
| sP24019
| sP24018
| sP24017
| sP24016
| sP24015
| sP24014
| sP24013
| sP24012
| sP24011
| sP24010
| sP24009
| sP24008
| v26522(sK23533_VarCurr,bitIndex2)
| v26522(sK23533_VarCurr,bitIndex1)
| ~ v28941(sK23533_VarCurr,bitIndex59)
| ~ v28941(sK23533_VarCurr,bitIndex5) ),
inference(resolution,[status(thm)],[c_315480,c_203313]) ).
tcf(c_423045,plain,
! [X0_iProver_nextState_2: iProver_nextState_2,X0_iProver_v28941_2: iProver_v28941_2] :
( sP38_aig_name(X0_iProver_nextState_2)
| v28946(X0_iProver_nextState_2,X0_iProver_v28941_2)
| ~ v26522(X0_iProver_nextState_2,X0_iProver_v28941_2) ),
inference(subtyping,[status(esa)],[c_175769]) ).
tcf(c_423095,plain,
! [X0_iProver_nextState_2: iProver_nextState_2,X0_iProver_v28941_2: iProver_v28941_2] :
( v28947(X0_iProver_nextState_2)
| v28941(X0_iProver_nextState_2,X0_iProver_v28941_2)
| ~ v28946(X0_iProver_nextState_2,X0_iProver_v28941_2) ),
inference(subtyping,[status(esa)],[c_156726]) ).
tcf(c_423112,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex3)
| ~ v26522(sK23533_VarCurr,bitIndex3) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423161,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex4)
| ~ v26522(sK23533_VarCurr,bitIndex4) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423269,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex4)
| ~ v28946(sK23533_VarCurr,bitIndex4) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423288,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex5)
| ~ v26522(sK23533_VarCurr,bitIndex5) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423468,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex5)
| ~ v28946(sK23533_VarCurr,bitIndex5) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423645,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex6)
| ~ v26522(sK23533_VarCurr,bitIndex6) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423729,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex6)
| ~ v28946(sK23533_VarCurr,bitIndex6) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423762,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex7)
| ~ v26522(sK23533_VarCurr,bitIndex7) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423778,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex7)
| ~ v28946(sK23533_VarCurr,bitIndex7) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423801,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex8)
| ~ v26522(sK23533_VarCurr,bitIndex8) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423805,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex8)
| ~ v28946(sK23533_VarCurr,bitIndex8) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423844,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex9)
| ~ v26522(sK23533_VarCurr,bitIndex9) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423860,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex9)
| ~ v28946(sK23533_VarCurr,bitIndex9) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423897,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex10)
| ~ v26522(sK23533_VarCurr,bitIndex10) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423913,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex10)
| ~ v28946(sK23533_VarCurr,bitIndex10) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_423950,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex11)
| ~ v26522(sK23533_VarCurr,bitIndex11) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_423966,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex11)
| ~ v28946(sK23533_VarCurr,bitIndex11) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424007,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex12)
| ~ v26522(sK23533_VarCurr,bitIndex12) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424023,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex12)
| ~ v28946(sK23533_VarCurr,bitIndex12) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424066,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex13)
| ~ v26522(sK23533_VarCurr,bitIndex13) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424082,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex13)
| ~ v28946(sK23533_VarCurr,bitIndex13) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424127,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex14)
| ~ v26522(sK23533_VarCurr,bitIndex14) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424143,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex14)
| ~ v28946(sK23533_VarCurr,bitIndex14) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424190,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex15)
| ~ v26522(sK23533_VarCurr,bitIndex15) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424206,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex15)
| ~ v28946(sK23533_VarCurr,bitIndex15) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424253,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex16)
| ~ v26522(sK23533_VarCurr,bitIndex16) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424269,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex17)
| ~ v26522(sK23533_VarCurr,bitIndex17) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424297,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex17)
| ~ v28946(sK23533_VarCurr,bitIndex17) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424369,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex18)
| ~ v26522(sK23533_VarCurr,bitIndex18) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424577,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex18)
| ~ v28946(sK23533_VarCurr,bitIndex18) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424737,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex19)
| ~ v26522(sK23533_VarCurr,bitIndex19) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424814,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex19)
| ~ v28946(sK23533_VarCurr,bitIndex19) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424849,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex20)
| ~ v26522(sK23533_VarCurr,bitIndex20) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424865,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex20)
| ~ v28946(sK23533_VarCurr,bitIndex20) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424890,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex21)
| ~ v26522(sK23533_VarCurr,bitIndex21) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424894,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex21)
| ~ v28946(sK23533_VarCurr,bitIndex21) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424935,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex22)
| ~ v26522(sK23533_VarCurr,bitIndex22) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_424951,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex22)
| ~ v28946(sK23533_VarCurr,bitIndex22) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_424988,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex23)
| ~ v26522(sK23533_VarCurr,bitIndex23) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425004,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex23)
| ~ v28946(sK23533_VarCurr,bitIndex23) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425045,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex24)
| ~ v26522(sK23533_VarCurr,bitIndex24) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425061,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex24)
| ~ v28946(sK23533_VarCurr,bitIndex24) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425104,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex25)
| ~ v26522(sK23533_VarCurr,bitIndex25) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425117,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex25)
| ~ v28946(sK23533_VarCurr,bitIndex25) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425161,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex26)
| ~ v26522(sK23533_VarCurr,bitIndex26) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425175,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex26)
| ~ v28946(sK23533_VarCurr,bitIndex26) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425220,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex27)
| ~ v26522(sK23533_VarCurr,bitIndex27) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425241,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex27)
| ~ v28946(sK23533_VarCurr,bitIndex27) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425293,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex28)
| ~ v26522(sK23533_VarCurr,bitIndex28) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425321,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex28)
| ~ v28946(sK23533_VarCurr,bitIndex28) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425352,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex29)
| ~ v26522(sK23533_VarCurr,bitIndex29) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425374,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex29)
| ~ v28946(sK23533_VarCurr,bitIndex29) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425427,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex30)
| ~ v26522(sK23533_VarCurr,bitIndex30) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425449,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex30)
| ~ v28946(sK23533_VarCurr,bitIndex30) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425476,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex31)
| ~ v26522(sK23533_VarCurr,bitIndex31) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425490,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex31)
| ~ v28946(sK23533_VarCurr,bitIndex31) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425504,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex32)
| ~ v26522(sK23533_VarCurr,bitIndex32) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425506,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex32)
| ~ v28946(sK23533_VarCurr,bitIndex32) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425520,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex33)
| ~ v26522(sK23533_VarCurr,bitIndex33) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425522,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex33)
| ~ v28946(sK23533_VarCurr,bitIndex33) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425536,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex34)
| ~ v26522(sK23533_VarCurr,bitIndex34) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425538,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex34)
| ~ v28946(sK23533_VarCurr,bitIndex34) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425552,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex35)
| ~ v26522(sK23533_VarCurr,bitIndex35) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425554,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex35)
| ~ v28946(sK23533_VarCurr,bitIndex35) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425568,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex36)
| ~ v26522(sK23533_VarCurr,bitIndex36) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425570,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex36)
| ~ v28946(sK23533_VarCurr,bitIndex36) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425584,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex37)
| ~ v26522(sK23533_VarCurr,bitIndex37) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425586,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex37)
| ~ v28946(sK23533_VarCurr,bitIndex37) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425600,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex38)
| ~ v26522(sK23533_VarCurr,bitIndex38) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425602,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex38)
| ~ v28946(sK23533_VarCurr,bitIndex38) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425616,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex39)
| ~ v26522(sK23533_VarCurr,bitIndex39) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425618,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex39)
| ~ v28946(sK23533_VarCurr,bitIndex39) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425632,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex40)
| ~ v26522(sK23533_VarCurr,bitIndex40) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425634,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex40)
| ~ v28946(sK23533_VarCurr,bitIndex40) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425648,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex41)
| ~ v26522(sK23533_VarCurr,bitIndex41) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425650,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex41)
| ~ v28946(sK23533_VarCurr,bitIndex41) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425664,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex42)
| ~ v26522(sK23533_VarCurr,bitIndex42) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425666,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex42)
| ~ v28946(sK23533_VarCurr,bitIndex42) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425681,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex43)
| ~ v26522(sK23533_VarCurr,bitIndex43) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425683,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex43)
| ~ v28946(sK23533_VarCurr,bitIndex43) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425697,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex44)
| ~ v26522(sK23533_VarCurr,bitIndex44) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425699,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex44)
| ~ v28946(sK23533_VarCurr,bitIndex44) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425713,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex45)
| ~ v26522(sK23533_VarCurr,bitIndex45) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425715,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex45)
| ~ v28946(sK23533_VarCurr,bitIndex45) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425729,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex46)
| ~ v26522(sK23533_VarCurr,bitIndex46) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425731,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex46)
| ~ v28946(sK23533_VarCurr,bitIndex46) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425745,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex47)
| ~ v26522(sK23533_VarCurr,bitIndex47) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425747,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex47)
| ~ v28946(sK23533_VarCurr,bitIndex47) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425761,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex48)
| ~ v26522(sK23533_VarCurr,bitIndex48) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425763,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex48)
| ~ v28946(sK23533_VarCurr,bitIndex48) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425777,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex49)
| ~ v26522(sK23533_VarCurr,bitIndex49) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425779,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex49)
| ~ v28946(sK23533_VarCurr,bitIndex49) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425793,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex50)
| ~ v26522(sK23533_VarCurr,bitIndex50) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425795,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex50)
| ~ v28946(sK23533_VarCurr,bitIndex50) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425807,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex51)
| ~ v26522(sK23533_VarCurr,bitIndex51) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425809,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex51)
| ~ v28946(sK23533_VarCurr,bitIndex51) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425823,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex52)
| ~ v26522(sK23533_VarCurr,bitIndex52) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425825,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex52)
| ~ v28946(sK23533_VarCurr,bitIndex52) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425839,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex53)
| ~ v26522(sK23533_VarCurr,bitIndex53) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425841,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex53)
| ~ v28946(sK23533_VarCurr,bitIndex53) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425853,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex54)
| ~ v26522(sK23533_VarCurr,bitIndex54) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425855,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex54)
| ~ v28946(sK23533_VarCurr,bitIndex54) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425869,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex55)
| ~ v26522(sK23533_VarCurr,bitIndex55) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425871,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex55)
| ~ v28946(sK23533_VarCurr,bitIndex55) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425885,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex56)
| ~ v26522(sK23533_VarCurr,bitIndex56) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425887,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex56)
| ~ v28946(sK23533_VarCurr,bitIndex56) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425901,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex57)
| ~ v26522(sK23533_VarCurr,bitIndex57) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425903,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex57)
| ~ v28946(sK23533_VarCurr,bitIndex57) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425915,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex58)
| ~ v26522(sK23533_VarCurr,bitIndex58) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425917,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex58)
| ~ v28946(sK23533_VarCurr,bitIndex58) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425931,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex59)
| ~ v26522(sK23533_VarCurr,bitIndex59) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425933,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex59)
| ~ v28946(sK23533_VarCurr,bitIndex59) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425947,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex1)
| ~ v26522(sK23533_VarCurr,bitIndex1) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425949,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex1)
| ~ v28946(sK23533_VarCurr,bitIndex1) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425960,plain,
( sP38_aig_name(sK23533_VarCurr)
| v28946(sK23533_VarCurr,bitIndex2)
| ~ v26522(sK23533_VarCurr,bitIndex2) ),
inference(instantiation,[status(thm)],[c_423045]) ).
tcf(c_425962,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex2)
| ~ v28946(sK23533_VarCurr,bitIndex2) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_425976,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex3)
| ~ v28946(sK23533_VarCurr,bitIndex3) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_426009,plain,
( v28947(sK23533_VarCurr)
| v28941(sK23533_VarCurr,bitIndex16)
| ~ v28946(sK23533_VarCurr,bitIndex16) ),
inference(instantiation,[status(thm)],[c_423095]) ).
tcf(c_426038,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_426009,c_425976,c_425962,c_425960,c_425949,c_425947,c_425933,c_425931,c_425917,c_425915,c_425903,c_425901,c_425887,c_425885,c_425871,c_425869,c_425855,c_425853,c_425841,c_425839,c_425825,c_425823,c_425809,c_425807,c_425795,c_425793,c_425779,c_425777,c_425763,c_425761,c_425747,c_425745,c_425731,c_425729,c_425715,c_425713,c_425699,c_425697,c_425683,c_425681,c_425666,c_425664,c_425650,c_425648,c_425634,c_425632,c_425618,c_425616,c_425602,c_425600,c_425586,c_425584,c_425570,c_425568,c_425554,c_425552,c_425538,c_425536,c_425522,c_425520,c_425506,c_425504,c_425490,c_425476,c_425449,c_425427,c_425374,c_425352,c_425321,c_425293,c_425241,c_425220,c_425175,c_425161,c_425117,c_425104,c_425061,c_425045,c_425004,c_424988,c_424951,c_424935,c_424894,c_424890,c_424865,c_424849,c_424814,c_424737,c_424577,c_424369,c_424297,c_424269,c_424253,c_424206,c_424190,c_424143,c_424127,c_424082,c_424066,c_424023,c_424007,c_423966,c_423950,c_423913,c_423897,c_423860,c_423844,c_423805,c_423801,c_423778,c_423762,c_423729,c_423645,c_423468,c_423288,c_423269,c_423161,c_423112,c_418871,c_315485,c_315480,c_315481,c_309376,c_308892,c_204812,c_204687,c_204556,c_204431,c_204300,c_204175,c_203269,c_203270,c_203271,c_203272,c_203273,c_203274,c_203275,c_203276,c_203277,c_203278,c_203279,c_203280,c_203281,c_203282,c_203284,c_203285,c_203286,c_203287,c_203288,c_203289,c_203290,c_203291,c_203292,c_203293,c_203294,c_203295,c_203296,c_203297,c_203298,c_203299,c_203300,c_203301,c_203302,c_203303,c_203304,c_203305,c_203306,c_203307,c_203308,c_203309,c_203310,c_203311,c_203312,c_203313,c_203314,c_203315,c_203316,c_203317,c_203318,c_203319,c_203321,c_203322,c_203323,c_203324,c_203325,c_203326,c_203204,c_203205,c_203206,c_203207,c_203208,c_203209,c_203210,c_203211,c_203212,c_203213,c_203214,c_203215,c_203216,c_203217,c_203219,c_203220,c_203221,c_203222,c_203223,c_203224,c_203225,c_203226,c_203227,c_203228,c_203229,c_203230,c_203231,c_203232,c_203233,c_203234,c_203235,c_203236,c_203237,c_203238,c_203239,c_203240,c_203241,c_203242,c_203243,c_203244,c_203245,c_203246,c_203247,c_203248,c_203249,c_203250,c_203251,c_203252,c_203253,c_203254,c_203262,c_203263,c_203264,c_203265,c_203266,c_203267,c_177764,c_156704]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV108-1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.42 % Computer : n006.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Wed Sep 23 17:10:41 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.18/0.49 Running EPR theorem proving
% 0.18/0.49 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.50
% 0.18/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.18/0.50
% 0.18/0.50 % Detected problem language: tptp
% 0.18/0.51 % Proving...
% 247.97/39.89 % SZS status Started for theBenchmark.p
% 247.97/39.89 % SZS status Unsatisfiable for theBenchmark.p
% 247.97/39.89
% 247.97/39.89 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 247.97/39.89
% 247.97/39.89 % ------ iProver source info
% 247.97/39.89
% 247.97/39.89 % git: date: 2026-07-19 20:42:38 +0200
% 247.97/39.89 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 247.97/39.89 % git: non_committed_changes: false
% 247.97/39.89
% 247.97/39.89 % ------ Parsing...% successful
% 247.97/39.89
% 247.97/39.89
% 247.97/39.89 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_eq
% 247.97/39.89 %
% 247.97/39.89
% 247.97/39.89 % ------ Preprocessing... sup_sim: 2 sf_s rm: 2268 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: 250 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 52 0s sf_e pe_s pe_e %
% 247.97/39.89
% 247.97/39.89 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_eq
% 247.97/39.89 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e % ------ preprocesses with Option_epr_non_horn_eq
% 247.97/39.89 %
% 247.97/39.89
% 247.97/39.89 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 247.97/39.89 % ------ Proving...
% 247.97/39.89 % ------ Problem Properties
% 247.97/39.89
% 247.97/39.89 %
% 247.97/39.89 % clauses 180
% 247.97/39.89 % conjectures 2
% 247.97/39.89 % EPR 180
% 247.97/39.89 % Horn 167
% 247.97/39.89 % unary 48
% 247.97/39.89 % binary 115
% 247.97/39.89 % lits 799
% 247.97/39.89 % lits eq 23
% 247.97/39.89 % fd_pure 0
% 247.97/39.89 % fd_pseudo 0
% 247.97/39.89 % fd_cond 1
% 247.97/39.89 % fd_pseudo_cond 0
% 247.97/39.89 % AC symbols 0
% 247.97/39.89
% 247.97/39.89 % ------ Schedule EPR non Horn eq is on
% 247.97/39.89
% 247.97/39.89 % ------ Option_epr_non_horn_eq Time Limit: Unbounded
% 247.97/39.89
% 247.97/39.89
% 247.97/39.89 % ------
% 247.97/39.89 % Current options:
% 247.97/39.89 % ------
% 247.97/39.89
% 247.97/39.89
% 247.97/39.89 %
% 247.97/39.89
% 247.97/39.89 % ------ Proving...
% 247.97/39.89 %
% 247.97/39.89
% 247.97/39.89 % SZS status Unsatisfiable for theBenchmark.p
% 247.97/39.89
% 247.97/39.89 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 247.97/39.92
% 247.97/39.92
%------------------------------------------------------------------------------