%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV125+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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 : Tue Sep 29 10:50:42 AM UTC 2026
% Result : Theorem 182.10s 40.34s
% Output : Refutation 257.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 76
% Syntax : Number of formulae : 640 ( 51 unt; 27 def)
% Number of atoms : 1873 ( 30 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 2044 ( 811 ~;1067 |; 44 &)
% ( 76 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 69 ( 67 usr; 28 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 285 ( 0 sgn 284 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f195,conjecture,
! [X0] :
( reachableState(X0)
=> v4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssertion) ).
fof(f196,negated_conjecture,
~ ! [X0] :
( reachableState(X0)
=> v4(X0) ),
inference(negated_conjecture,[status(cth)],[f195]) ).
fof(f197,axiom,
! [X0] :
( ~ v4(X0)
<=> v154847(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11893) ).
fof(f198,axiom,
! [X0] :
( ~ v154847(X0)
<=> v154848(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11892) ).
fof(f199,axiom,
! [X0] :
( v154848(X0)
<=> ( v154850(X0)
& v154868(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20766) ).
fof(f200,axiom,
! [X0] :
( v154868(X0)
<=> ( v154869(X0)
| v154853(X0,bitIndex3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7474) ).
fof(f201,axiom,
! [X0] :
( v154869(X0)
<=> ( v154870(X0)
| v154853(X0,bitIndex2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7473) ).
fof(f202,axiom,
! [X0] :
( v154870(X0)
<=> ( v154853(X0,bitIndex0)
| v154853(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7472) ).
fof(f203,axiom,
! [X0] :
( v154850(X0)
<=> ( v154851(X0)
| v154859(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20765) ).
fof(f204,axiom,
! [X0] :
( v154859(X0)
<=> ( v154860(X0)
| v154861(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20764) ).
fof(f205,axiom,
! [X0] :
( v154861(X0)
<=> ( v154852(X0)
& v154862(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20763) ).
fof(f206,axiom,
! [X0] :
( v154862(X0)
<=> ( v154863(X0)
| v154864(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20762) ).
fof(f207,axiom,
! [X0] :
( v154864(X0)
<=> ( v154855(X0)
& v154865(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20761) ).
fof(f208,axiom,
! [X0] :
( v154865(X0)
<=> ( v154866(X0)
| v154867(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20760) ).
fof(f209,axiom,
! [X0] :
( v154867(X0)
<=> ( v154853(X0,bitIndex0)
& v154858(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20759) ).
fof(f210,axiom,
! [X0] :
( v154866(X0)
<=> ( v154857(X0)
& v154853(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7471) ).
fof(f211,axiom,
! [X0] :
( v154863(X0)
<=> ( v154853(X0,bitIndex2)
& v154856(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7470) ).
fof(f212,axiom,
! [X0] :
( v154860(X0)
<=> ( v154853(X0,bitIndex3)
& v154854(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7469) ).
fof(f213,axiom,
! [X0] :
( v154851(X0)
<=> ( v154852(X0)
& v154854(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20758) ).
fof(f214,axiom,
! [X0] :
( v154854(X0)
<=> ( v154855(X0)
& v154856(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20757) ).
fof(f215,axiom,
! [X0] :
( v154856(X0)
<=> ( v154857(X0)
& v154858(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20756) ).
fof(f216,axiom,
! [X0] :
( ~ v154858(X0)
<=> v154853(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11891) ).
fof(f217,axiom,
! [X0] :
( ~ v154857(X0)
<=> v154853(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11890) ).
fof(f218,axiom,
! [X0] :
( ~ v154855(X0)
<=> v154853(X0,bitIndex2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11889) ).
fof(f219,axiom,
! [X0] :
( ~ v154852(X0)
<=> v154853(X0,bitIndex3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11888) ).
fof(f220,axiom,
! [X0,X1] :
( range_3_0(X1)
=> ( v154853(X0,X1)
<=> v6(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86259) ).
fof(f221,axiom,
! [X0] :
( ~ v154836(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> v154838(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_1769) ).
fof(f222,axiom,
! [X0] :
( v154836(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> b0001(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1782) ).
fof(f223,axiom,
! [X0] :
( ~ v154839(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v154838(X0,X1)
<=> v154841(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_1768) ).
fof(f224,axiom,
! [X0] :
( v154839(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v154838(X0,X1)
<=> b0010(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1781) ).
fof(f225,axiom,
! [X0] :
( ~ v1051(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v154841(X0,X1)
<=> v154844(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_1767) ).
fof(f226,axiom,
! [X0] :
( v1051(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v154841(X0,X1)
<=> v154842(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1780) ).
fof(f227,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v154844(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86258) ).
fof(f228,axiom,
! [X0] :
( v154844(X0,bitIndex2)
<=> v154845(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86257) ).
fof(f229,axiom,
! [X0] :
( v154844(X0,bitIndex3)
<=> v83122(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86256) ).
fof(f230,axiom,
! [X0] :
( ~ v154845(X0)
<=> v83122(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11887) ).
fof(f231,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v154842(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86255) ).
fof(f232,axiom,
! [X0] :
( v154842(X0,bitIndex2)
<=> v154843(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86254) ).
fof(f233,axiom,
! [X0] :
( v154842(X0,bitIndex3)
<=> v83122(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86253) ).
fof(f234,axiom,
! [X0] :
( ~ v154843(X0)
<=> v83122(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11886) ).
fof(f138193,axiom,
~ b0010(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_280) ).
fof(f138194,axiom,
~ b0010(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_279) ).
fof(f138195,axiom,
b0010(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_278) ).
fof(f138196,axiom,
~ b0010(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_277) ).
fof(f138220,axiom,
~ b0001(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_276) ).
fof(f138221,axiom,
~ b0001(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_275) ).
fof(f138222,axiom,
~ b0001(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_274) ).
fof(f138223,axiom,
b0001(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_273) ).
fof(f141550,axiom,
! [X0] :
( range_1_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_axiom_4) ).
fof(f142409,axiom,
! [X0] :
( range_3_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_axiom) ).
fof(f142495,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154842(X0,X1) ),
inference(true_and_false_elimination,[],[f231]) ).
fof(f142496,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154842(X0,X1) ),
inference(flattening,[],[f142495]) ).
fof(f142497,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154844(X0,X1) ),
inference(true_and_false_elimination,[],[f227]) ).
fof(f142498,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154844(X0,X1) ),
inference(flattening,[],[f142497]) ).
fof(f142591,plain,
! [X0] :
( range_3_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
inference(true_and_false_elimination,[],[f142409]) ).
fof(f142595,plain,
! [X0] :
( range_1_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0 ) ),
inference(true_and_false_elimination,[],[f141550]) ).
fof(f142822,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0 )
=> range_1_0(X0) ),
inference(unused_predicate_definition_removal,[],[f142595]) ).
fof(f142823,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 )
=> range_3_0(X0) ),
inference(unused_predicate_definition_removal,[],[f142591]) ).
fof(f142824,plain,
! [X0] :
( ~ v4(X0)
=> v154847(X0) ),
inference(unused_predicate_definition_removal,[],[f197]) ).
fof(f142825,plain,
! [X0] :
( v154848(X0)
=> ~ v154847(X0) ),
inference(unused_predicate_definition_removal,[],[f198]) ).
fof(f142826,plain,
! [X0] :
( ( v154850(X0)
& v154868(X0) )
=> v154848(X0) ),
inference(unused_predicate_definition_removal,[],[f199]) ).
fof(f142827,plain,
! [X0] :
( ( v154851(X0)
| v154859(X0) )
=> v154850(X0) ),
inference(unused_predicate_definition_removal,[],[f203]) ).
fof(f142828,plain,
! [X0] :
( ( v154852(X0)
& v154854(X0) )
=> v154851(X0) ),
inference(unused_predicate_definition_removal,[],[f213]) ).
fof(f142829,plain,
! [X0] :
( ( v154860(X0)
| v154861(X0) )
=> v154859(X0) ),
inference(unused_predicate_definition_removal,[],[f204]) ).
fof(f142830,plain,
! [X0] :
( ( v154853(X0,bitIndex3)
& v154854(X0) )
=> v154860(X0) ),
inference(unused_predicate_definition_removal,[],[f212]) ).
fof(f142831,plain,
! [X0] :
( ( v154855(X0)
& v154856(X0) )
=> v154854(X0) ),
inference(unused_predicate_definition_removal,[],[f214]) ).
fof(f142832,plain,
! [X0] :
( ( v154852(X0)
& v154862(X0) )
=> v154861(X0) ),
inference(unused_predicate_definition_removal,[],[f205]) ).
fof(f142833,plain,
! [X0] :
( ~ v154852(X0)
=> v154853(X0,bitIndex3) ),
inference(unused_predicate_definition_removal,[],[f219]) ).
fof(f142834,plain,
! [X0] :
( ( v154863(X0)
| v154864(X0) )
=> v154862(X0) ),
inference(unused_predicate_definition_removal,[],[f206]) ).
fof(f142835,plain,
! [X0] :
( ( v154853(X0,bitIndex2)
& v154856(X0) )
=> v154863(X0) ),
inference(unused_predicate_definition_removal,[],[f211]) ).
fof(f142836,plain,
! [X0] :
( ( v154857(X0)
& v154858(X0) )
=> v154856(X0) ),
inference(unused_predicate_definition_removal,[],[f215]) ).
fof(f142837,plain,
! [X0] :
( ( v154855(X0)
& v154865(X0) )
=> v154864(X0) ),
inference(unused_predicate_definition_removal,[],[f207]) ).
fof(f142838,plain,
! [X0] :
( ~ v154855(X0)
=> v154853(X0,bitIndex2) ),
inference(unused_predicate_definition_removal,[],[f218]) ).
fof(f142839,plain,
! [X0] :
( ( v154866(X0)
| v154867(X0) )
=> v154865(X0) ),
inference(unused_predicate_definition_removal,[],[f208]) ).
fof(f142840,plain,
! [X0] :
( ( v154857(X0)
& v154853(X0,bitIndex1) )
=> v154866(X0) ),
inference(unused_predicate_definition_removal,[],[f210]) ).
fof(f142841,plain,
! [X0] :
( ~ v154857(X0)
=> v154853(X0,bitIndex0) ),
inference(unused_predicate_definition_removal,[],[f217]) ).
fof(f142842,plain,
! [X0] :
( ( v154853(X0,bitIndex0)
& v154858(X0) )
=> v154867(X0) ),
inference(unused_predicate_definition_removal,[],[f209]) ).
fof(f142843,plain,
! [X0] :
( ~ v154858(X0)
=> v154853(X0,bitIndex1) ),
inference(unused_predicate_definition_removal,[],[f216]) ).
fof(f142844,plain,
! [X0] :
( ( v154869(X0)
| v154853(X0,bitIndex3) )
=> v154868(X0) ),
inference(unused_predicate_definition_removal,[],[f200]) ).
fof(f142845,plain,
! [X0] :
( ( v154870(X0)
| v154853(X0,bitIndex2) )
=> v154869(X0) ),
inference(unused_predicate_definition_removal,[],[f201]) ).
fof(f142846,plain,
! [X0] :
( ( v154853(X0,bitIndex0)
| v154853(X0,bitIndex1) )
=> v154870(X0) ),
inference(unused_predicate_definition_removal,[],[f202]) ).
fof(f142871,plain,
~ ! [X0] : v4(X0),
inference(pure_predicate_removal,[],[f196]) ).
fof(f142959,plain,
? [X0] : ~ v4(X0),
inference(ennf_transformation,[],[f142871]) ).
fof(f142960,plain,
! [X0] :
( v154847(X0)
| v4(X0) ),
inference(ennf_transformation,[],[f142824]) ).
fof(f142961,plain,
! [X0] :
( ~ v154847(X0)
| ~ v154848(X0) ),
inference(ennf_transformation,[],[f142825]) ).
fof(f142962,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(ennf_transformation,[],[f142826]) ).
fof(f142963,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(flattening,[],[f142962]) ).
fof(f142964,plain,
! [X0] :
( v154850(X0)
| ( ~ v154851(X0)
& ~ v154859(X0) ) ),
inference(ennf_transformation,[],[f142827]) ).
fof(f142965,plain,
! [X0] :
( v154868(X0)
| ( ~ v154869(X0)
& ~ v154853(X0,bitIndex3) ) ),
inference(ennf_transformation,[],[f142844]) ).
fof(f142966,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(ennf_transformation,[],[f142828]) ).
fof(f142967,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(flattening,[],[f142966]) ).
fof(f142968,plain,
! [X0] :
( v154859(X0)
| ( ~ v154860(X0)
& ~ v154861(X0) ) ),
inference(ennf_transformation,[],[f142829]) ).
fof(f142969,plain,
! [X0] :
( v154869(X0)
| ( ~ v154870(X0)
& ~ v154853(X0,bitIndex2) ) ),
inference(ennf_transformation,[],[f142845]) ).
fof(f142970,plain,
! [X0,X1] :
( ( v154853(X0,X1)
<=> v6(X0,X1) )
| ~ range_3_0(X1) ),
inference(ennf_transformation,[],[f220]) ).
fof(f142971,plain,
! [X0] :
( v154853(X0,bitIndex3)
| v154852(X0) ),
inference(ennf_transformation,[],[f142833]) ).
fof(f142972,plain,
! [X0] :
( v154853(X0,bitIndex2)
| v154855(X0) ),
inference(ennf_transformation,[],[f142838]) ).
fof(f142973,plain,
! [X0] :
( v154853(X0,bitIndex0)
| v154857(X0) ),
inference(ennf_transformation,[],[f142841]) ).
fof(f142974,plain,
! [X0] :
( v154853(X0,bitIndex1)
| v154858(X0) ),
inference(ennf_transformation,[],[f142843]) ).
fof(f142975,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(ennf_transformation,[],[f142830]) ).
fof(f142976,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(flattening,[],[f142975]) ).
fof(f142977,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(ennf_transformation,[],[f142835]) ).
fof(f142978,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(flattening,[],[f142977]) ).
fof(f142979,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(ennf_transformation,[],[f142840]) ).
fof(f142980,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(flattening,[],[f142979]) ).
fof(f142981,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(ennf_transformation,[],[f142842]) ).
fof(f142982,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(flattening,[],[f142981]) ).
fof(f142983,plain,
! [X0] :
( v154870(X0)
| ( ~ v154853(X0,bitIndex0)
& ~ v154853(X0,bitIndex1) ) ),
inference(ennf_transformation,[],[f142846]) ).
fof(f142984,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(ennf_transformation,[],[f142832]) ).
fof(f142985,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(flattening,[],[f142984]) ).
fof(f142986,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(ennf_transformation,[],[f142831]) ).
fof(f142987,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(flattening,[],[f142986]) ).
fof(f142988,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> b0001(X1) )
| ~ range_3_0(X1) )
| ~ v154836(X0) ),
inference(ennf_transformation,[],[f222]) ).
fof(f142989,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> v154838(X0,X1) )
| ~ range_3_0(X1) )
| v154836(X0) ),
inference(ennf_transformation,[],[f221]) ).
fof(f142990,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(ennf_transformation,[],[f142837]) ).
fof(f142991,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(flattening,[],[f142990]) ).
fof(f142992,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(ennf_transformation,[],[f142836]) ).
fof(f142993,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(flattening,[],[f142992]) ).
fof(f142994,plain,
! [X0] :
( v154862(X0)
| ( ~ v154863(X0)
& ~ v154864(X0) ) ),
inference(ennf_transformation,[],[f142834]) ).
fof(f142995,plain,
! [X0] :
( v154865(X0)
| ( ~ v154866(X0)
& ~ v154867(X0) ) ),
inference(ennf_transformation,[],[f142839]) ).
fof(f143000,plain,
! [X0] :
( ! [X1] :
( ( v154838(X0,X1)
<=> b0010(X1) )
| ~ range_3_0(X1) )
| ~ v154839(X0) ),
inference(ennf_transformation,[],[f224]) ).
fof(f143001,plain,
! [X0] :
( ! [X1] :
( ( v154838(X0,X1)
<=> v154841(X0,X1) )
| ~ range_3_0(X1) )
| v154839(X0) ),
inference(ennf_transformation,[],[f223]) ).
fof(f143016,plain,
! [X0] :
( ! [X1] :
( ( v154841(X0,X1)
<=> v154842(X0,X1) )
| ~ range_3_0(X1) )
| ~ v1051(X0) ),
inference(ennf_transformation,[],[f226]) ).
fof(f143017,plain,
! [X0] :
( ! [X1] :
( ( v154841(X0,X1)
<=> v154844(X0,X1) )
| ~ range_3_0(X1) )
| v1051(X0) ),
inference(ennf_transformation,[],[f225]) ).
fof(f143063,plain,
! [X0,X1] :
( ~ v154842(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f142496]) ).
fof(f143064,plain,
! [X0,X1] :
( ~ v154844(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f142498]) ).
fof(f143290,plain,
! [X0] :
( range_3_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0
& bitIndex2 != X0
& bitIndex3 != X0 ) ),
inference(ennf_transformation,[],[f142823]) ).
fof(f143293,plain,
! [X0] :
( range_1_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0 ) ),
inference(ennf_transformation,[],[f142822]) ).
fof(f143610,plain,
~ v4(sK54),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X0,sK54)],[f142959]) ).
fof(f143611,plain,
! [X0,X1] :
( ( ( v154853(X0,X1)
| ~ v6(X0,X1) )
& ( v6(X0,X1)
| ~ v154853(X0,X1) ) )
| ~ range_3_0(X1) ),
inference(nnf_transformation,[],[f142970]) ).
fof(f143612,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ b0001(X1) )
& ( b0001(X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v154836(X0) ),
inference(nnf_transformation,[],[f142988]) ).
fof(f143613,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ v154838(X0,X1) )
& ( v154838(X0,X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| v154836(X0) ),
inference(nnf_transformation,[],[f142989]) ).
fof(f143620,plain,
! [X0] :
( ! [X1] :
( ( ( v154838(X0,X1)
| ~ b0010(X1) )
& ( b0010(X1)
| ~ v154838(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v154839(X0) ),
inference(nnf_transformation,[],[f143000]) ).
fof(f143621,plain,
! [X0] :
( ! [X1] :
( ( ( v154838(X0,X1)
| ~ v154841(X0,X1) )
& ( v154841(X0,X1)
| ~ v154838(X0,X1) ) )
| ~ range_3_0(X1) )
| v154839(X0) ),
inference(nnf_transformation,[],[f143001]) ).
fof(f143656,plain,
! [X0] :
( ! [X1] :
( ( ( v154841(X0,X1)
| ~ v154842(X0,X1) )
& ( v154842(X0,X1)
| ~ v154841(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v1051(X0) ),
inference(nnf_transformation,[],[f143016]) ).
fof(f143657,plain,
! [X0] :
( ! [X1] :
( ( ( v154841(X0,X1)
| ~ v154844(X0,X1) )
& ( v154844(X0,X1)
| ~ v154841(X0,X1) ) )
| ~ range_3_0(X1) )
| v1051(X0) ),
inference(nnf_transformation,[],[f143017]) ).
fof(f143748,plain,
! [X0] :
( ( v154842(X0,bitIndex3)
| ~ v83122(X0,bitIndex1) )
& ( v83122(X0,bitIndex1)
| ~ v154842(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f233]) ).
fof(f143749,plain,
! [X0] :
( ( v154842(X0,bitIndex2)
| ~ v154843(X0) )
& ( v154843(X0)
| ~ v154842(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f232]) ).
fof(f143750,plain,
! [X0] :
( ( v154844(X0,bitIndex3)
| ~ v83122(X0,bitIndex0) )
& ( v83122(X0,bitIndex0)
| ~ v154844(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f229]) ).
fof(f143751,plain,
! [X0] :
( ( v154844(X0,bitIndex2)
| ~ v154845(X0) )
& ( v154845(X0)
| ~ v154844(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f228]) ).
fof(f144016,plain,
! [X0] :
( ( ~ v154843(X0)
| ~ v83122(X0,bitIndex1) )
& ( v83122(X0,bitIndex1)
| v154843(X0) ) ),
inference(nnf_transformation,[],[f234]) ).
fof(f144017,plain,
! [X0] :
( ( ~ v154845(X0)
| ~ v83122(X0,bitIndex0) )
& ( v83122(X0,bitIndex0)
| v154845(X0) ) ),
inference(nnf_transformation,[],[f230]) ).
fof(f146055,plain,
~ v4(sK54),
inference(cnf_transformation,[],[f143610]) ).
fof(f146056,plain,
! [X0] :
( v154847(X0)
| v4(X0) ),
inference(cnf_transformation,[],[f142960]) ).
fof(f146057,plain,
! [X0] :
( ~ v154847(X0)
| ~ v154848(X0) ),
inference(cnf_transformation,[],[f142961]) ).
fof(f146058,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(cnf_transformation,[],[f142963]) ).
fof(f146059,plain,
! [X0] :
( v154850(X0)
| ~ v154859(X0) ),
inference(cnf_transformation,[],[f142964]) ).
fof(f146060,plain,
! [X0] :
( v154850(X0)
| ~ v154851(X0) ),
inference(cnf_transformation,[],[f142964]) ).
fof(f146061,plain,
! [X0] :
( v154868(X0)
| ~ v154853(X0,bitIndex3) ),
inference(cnf_transformation,[],[f142965]) ).
fof(f146062,plain,
! [X0] :
( v154868(X0)
| ~ v154869(X0) ),
inference(cnf_transformation,[],[f142965]) ).
fof(f146063,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(cnf_transformation,[],[f142967]) ).
fof(f146064,plain,
! [X0] :
( v154859(X0)
| ~ v154861(X0) ),
inference(cnf_transformation,[],[f142968]) ).
fof(f146065,plain,
! [X0] :
( v154859(X0)
| ~ v154860(X0) ),
inference(cnf_transformation,[],[f142968]) ).
fof(f146066,plain,
! [X0] :
( v154869(X0)
| ~ v154853(X0,bitIndex2) ),
inference(cnf_transformation,[],[f142969]) ).
fof(f146067,plain,
! [X0] :
( v154869(X0)
| ~ v154870(X0) ),
inference(cnf_transformation,[],[f142969]) ).
fof(f146068,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v154853(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f143611]) ).
fof(f146069,plain,
! [X0,X1] :
( v154853(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f143611]) ).
fof(f146070,plain,
! [X0] :
( v154853(X0,bitIndex3)
| v154852(X0) ),
inference(cnf_transformation,[],[f142971]) ).
fof(f146071,plain,
! [X0] :
( v154853(X0,bitIndex2)
| v154855(X0) ),
inference(cnf_transformation,[],[f142972]) ).
fof(f146072,plain,
! [X0] :
( v154853(X0,bitIndex0)
| v154857(X0) ),
inference(cnf_transformation,[],[f142973]) ).
fof(f146073,plain,
! [X0] :
( v154853(X0,bitIndex1)
| v154858(X0) ),
inference(cnf_transformation,[],[f142974]) ).
fof(f146074,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(cnf_transformation,[],[f142976]) ).
fof(f146075,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(cnf_transformation,[],[f142978]) ).
fof(f146076,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(cnf_transformation,[],[f142980]) ).
fof(f146077,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(cnf_transformation,[],[f142982]) ).
fof(f146078,plain,
! [X0] :
( v154870(X0)
| ~ v154853(X0,bitIndex1) ),
inference(cnf_transformation,[],[f142983]) ).
fof(f146079,plain,
! [X0] :
( v154870(X0)
| ~ v154853(X0,bitIndex0) ),
inference(cnf_transformation,[],[f142983]) ).
fof(f146080,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(cnf_transformation,[],[f142985]) ).
fof(f146081,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(cnf_transformation,[],[f142987]) ).
fof(f146082,plain,
! [X0,X1] :
( b0001(X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| ~ v154836(X0) ),
inference(cnf_transformation,[],[f143612]) ).
fof(f146083,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ b0001(X1)
| ~ range_3_0(X1)
| ~ v154836(X0) ),
inference(cnf_transformation,[],[f143612]) ).
fof(f146084,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| v154836(X0) ),
inference(cnf_transformation,[],[f143613]) ).
fof(f146085,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| v154836(X0) ),
inference(cnf_transformation,[],[f143613]) ).
fof(f146086,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(cnf_transformation,[],[f142991]) ).
fof(f146087,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(cnf_transformation,[],[f142993]) ).
fof(f146088,plain,
! [X0] :
( v154862(X0)
| ~ v154864(X0) ),
inference(cnf_transformation,[],[f142994]) ).
fof(f146089,plain,
! [X0] :
( v154862(X0)
| ~ v154863(X0) ),
inference(cnf_transformation,[],[f142994]) ).
fof(f146090,plain,
! [X0] :
( v154865(X0)
| ~ v154867(X0) ),
inference(cnf_transformation,[],[f142995]) ).
fof(f146091,plain,
! [X0] :
( v154865(X0)
| ~ v154866(X0) ),
inference(cnf_transformation,[],[f142995]) ).
fof(f146095,plain,
b0001(bitIndex0),
inference(cnf_transformation,[],[f138223]) ).
fof(f146096,plain,
~ b0001(bitIndex1),
inference(cnf_transformation,[],[f138222]) ).
fof(f146097,plain,
~ b0001(bitIndex2),
inference(cnf_transformation,[],[f138221]) ).
fof(f146098,plain,
~ b0001(bitIndex3),
inference(cnf_transformation,[],[f138220]) ).
fof(f146111,plain,
! [X0,X1] :
( b0010(X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| ~ v154839(X0) ),
inference(cnf_transformation,[],[f143620]) ).
fof(f146112,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ b0010(X1)
| ~ range_3_0(X1)
| ~ v154839(X0) ),
inference(cnf_transformation,[],[f143620]) ).
fof(f146113,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| v154839(X0) ),
inference(cnf_transformation,[],[f143621]) ).
fof(f146114,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| v154839(X0) ),
inference(cnf_transformation,[],[f143621]) ).
fof(f146179,plain,
~ b0010(bitIndex0),
inference(cnf_transformation,[],[f138196]) ).
fof(f146180,plain,
b0010(bitIndex1),
inference(cnf_transformation,[],[f138195]) ).
fof(f146181,plain,
~ b0010(bitIndex2),
inference(cnf_transformation,[],[f138194]) ).
fof(f146182,plain,
~ b0010(bitIndex3),
inference(cnf_transformation,[],[f138193]) ).
fof(f146187,plain,
! [X0,X1] :
( v154842(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| ~ v1051(X0) ),
inference(cnf_transformation,[],[f143656]) ).
fof(f146188,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154842(X0,X1)
| ~ range_3_0(X1)
| ~ v1051(X0) ),
inference(cnf_transformation,[],[f143656]) ).
fof(f146189,plain,
! [X0,X1] :
( v154844(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| v1051(X0) ),
inference(cnf_transformation,[],[f143657]) ).
fof(f146190,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154844(X0,X1)
| ~ range_3_0(X1)
| v1051(X0) ),
inference(cnf_transformation,[],[f143657]) ).
fof(f146364,plain,
! [X0] :
( v83122(X0,bitIndex1)
| ~ v154842(X0,bitIndex3) ),
inference(cnf_transformation,[],[f143748]) ).
fof(f146365,plain,
! [X0] :
( v154842(X0,bitIndex3)
| ~ v83122(X0,bitIndex1) ),
inference(cnf_transformation,[],[f143748]) ).
fof(f146366,plain,
! [X0] :
( v154843(X0)
| ~ v154842(X0,bitIndex2) ),
inference(cnf_transformation,[],[f143749]) ).
fof(f146367,plain,
! [X0] :
( v154842(X0,bitIndex2)
| ~ v154843(X0) ),
inference(cnf_transformation,[],[f143749]) ).
fof(f146368,plain,
! [X0,X1] :
( ~ v154842(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f143063]) ).
fof(f146369,plain,
! [X0] :
( v83122(X0,bitIndex0)
| ~ v154844(X0,bitIndex3) ),
inference(cnf_transformation,[],[f143750]) ).
fof(f146370,plain,
! [X0] :
( v154844(X0,bitIndex3)
| ~ v83122(X0,bitIndex0) ),
inference(cnf_transformation,[],[f143750]) ).
fof(f146371,plain,
! [X0] :
( v154845(X0)
| ~ v154844(X0,bitIndex2) ),
inference(cnf_transformation,[],[f143751]) ).
fof(f146372,plain,
! [X0] :
( v154844(X0,bitIndex2)
| ~ v154845(X0) ),
inference(cnf_transformation,[],[f143751]) ).
fof(f146373,plain,
! [X0,X1] :
( ~ v154844(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f143064]) ).
fof(f146892,plain,
! [X0] :
( v83122(X0,bitIndex1)
| v154843(X0) ),
inference(cnf_transformation,[],[f144016]) ).
fof(f146893,plain,
! [X0] :
( ~ v154843(X0)
| ~ v83122(X0,bitIndex1) ),
inference(cnf_transformation,[],[f144016]) ).
fof(f146894,plain,
! [X0] :
( v83122(X0,bitIndex0)
| v154845(X0) ),
inference(cnf_transformation,[],[f144017]) ).
fof(f146895,plain,
! [X0] :
( ~ v154845(X0)
| ~ v83122(X0,bitIndex0) ),
inference(cnf_transformation,[],[f144017]) ).
fof(f148451,plain,
! [X0] :
( range_3_0(X0)
| bitIndex3 != X0 ),
inference(cnf_transformation,[],[f143290]) ).
fof(f148452,plain,
! [X0] :
( range_3_0(X0)
| bitIndex2 != X0 ),
inference(cnf_transformation,[],[f143290]) ).
fof(f148453,plain,
! [X0] :
( range_3_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f143290]) ).
fof(f148454,plain,
! [X0] :
( range_3_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f143290]) ).
fof(f148466,plain,
! [X0] :
( range_1_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f143293]) ).
fof(f148467,plain,
! [X0] :
( range_1_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f143293]) ).
fof(f151127,plain,
range_3_0(bitIndex0),
inference(equality_resolution,[],[f148454]) ).
fof(f151128,plain,
range_3_0(bitIndex1),
inference(equality_resolution,[],[f148453]) ).
fof(f151129,plain,
range_3_0(bitIndex2),
inference(equality_resolution,[],[f148452]) ).
fof(f151130,plain,
range_3_0(bitIndex3),
inference(equality_resolution,[],[f148451]) ).
fof(f151142,plain,
range_1_0(bitIndex0),
inference(equality_resolution,[],[f148467]) ).
fof(f151143,plain,
range_1_0(bitIndex1),
inference(equality_resolution,[],[f148466]) ).
fof(f151246,plain,
v154847(sK54),
inference(resolution,[],[f146055,f146056]) ).
fof(f151247,plain,
~ v154848(sK54),
inference(resolution,[],[f151246,f146057]) ).
fof(f151248,plain,
( ~ v154850(sK54)
| ~ v154868(sK54) ),
inference(resolution,[],[f151247,f146058]) ).
fof(f151250,definition,
( spl55_1
<=> v154868(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_1])],[avatar_definition]) ).
fof(f151252,plain,
( ~ v154868(sK54)
| spl55_1 ),
inference(avatar_component_clause,[],[f151250]) ).
fof(f151254,definition,
( spl55_2
<=> v154850(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_2])],[avatar_definition]) ).
fof(f151256,plain,
( ~ v154850(sK54)
| spl55_2 ),
inference(avatar_component_clause,[],[f151254]) ).
fof(f151257,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(avatar_split_clause,[],[f151248,f151254,f151250]) ).
fof(f151258,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_1 ),
inference(resolution,[],[f151252,f146061]) ).
fof(f151259,plain,
( ~ v154869(sK54)
| spl55_1 ),
inference(resolution,[],[f151252,f146062]) ).
fof(f151261,plain,
( ~ v154870(sK54)
| spl55_1 ),
inference(resolution,[],[f151259,f146067]) ).
fof(f151263,plain,
( ~ v6(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl55_1 ),
inference(resolution,[],[f151258,f146069]) ).
fof(f151264,plain,
( ~ v6(sK54,bitIndex3)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f151263,f151130]) ).
fof(f151270,definition,
( spl55_3
<=> v154854(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_3])],[avatar_definition]) ).
fof(f151271,plain,
( v154854(sK54)
| ~ spl55_3 ),
inference(avatar_component_clause,[],[f151270]) ).
fof(f151272,plain,
( ~ v154854(sK54)
| spl55_3 ),
inference(avatar_component_clause,[],[f151270]) ).
fof(f151274,definition,
( spl55_4
<=> v154851(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_4])],[avatar_definition]) ).
fof(f151275,plain,
( ~ v154851(sK54)
| spl55_4 ),
inference(avatar_component_clause,[],[f151274]) ).
fof(f151279,definition,
( spl55_5
<=> v154862(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_5])],[avatar_definition]) ).
fof(f151280,plain,
( v154862(sK54)
| ~ spl55_5 ),
inference(avatar_component_clause,[],[f151279]) ).
fof(f151281,plain,
( ~ v154862(sK54)
| spl55_5 ),
inference(avatar_component_clause,[],[f151279]) ).
fof(f151283,definition,
( spl55_6
<=> v154861(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_6])],[avatar_definition]) ).
fof(f151284,plain,
( ~ v154861(sK54)
| spl55_6 ),
inference(avatar_component_clause,[],[f151283]) ).
fof(f151287,plain,
( ~ v154855(sK54)
| ~ v154856(sK54)
| spl55_3 ),
inference(resolution,[],[f151272,f146081]) ).
fof(f151289,definition,
( spl55_7
<=> v154856(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_7])],[avatar_definition]) ).
fof(f151290,plain,
( v154856(sK54)
| ~ spl55_7 ),
inference(avatar_component_clause,[],[f151289]) ).
fof(f151291,plain,
( ~ v154856(sK54)
| spl55_7 ),
inference(avatar_component_clause,[],[f151289]) ).
fof(f151293,definition,
( spl55_8
<=> v154855(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_8])],[avatar_definition]) ).
fof(f151294,plain,
( v154855(sK54)
| ~ spl55_8 ),
inference(avatar_component_clause,[],[f151293]) ).
fof(f151295,plain,
( ~ v154855(sK54)
| spl55_8 ),
inference(avatar_component_clause,[],[f151293]) ).
fof(f151296,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_3 ),
inference(avatar_split_clause,[],[f151287,f151270,f151293,f151289]) ).
fof(f151301,plain,
( ~ v154864(sK54)
| spl55_5 ),
inference(resolution,[],[f151281,f146088]) ).
fof(f151302,plain,
( ~ v154863(sK54)
| spl55_5 ),
inference(resolution,[],[f151281,f146089]) ).
fof(f151303,plain,
( ~ v154838(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154836(sK54)
| spl55_1 ),
inference(resolution,[],[f151264,f146085]) ).
fof(f151306,plain,
( ~ v154838(sK54,bitIndex3)
| v154836(sK54)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f151303,f151130]) ).
fof(f151308,definition,
( spl55_9
<=> v154836(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_9])],[avatar_definition]) ).
fof(f151309,plain,
( ~ v154836(sK54)
| spl55_9 ),
inference(avatar_component_clause,[],[f151308]) ).
fof(f151310,plain,
( v154836(sK54)
| ~ spl55_9 ),
inference(avatar_component_clause,[],[f151308]) ).
fof(f151312,definition,
( spl55_10
<=> v154838(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_10])],[avatar_definition]) ).
fof(f151313,plain,
( v154838(sK54,bitIndex3)
| ~ spl55_10 ),
inference(avatar_component_clause,[],[f151312]) ).
fof(f151314,plain,
( ~ v154838(sK54,bitIndex3)
| spl55_10 ),
inference(avatar_component_clause,[],[f151312]) ).
fof(f151315,plain,
( spl55_9
| ~ spl55_10
| spl55_1 ),
inference(avatar_split_clause,[],[f151306,f151250,f151312,f151308]) ).
fof(f151316,plain,
( ~ v154857(sK54)
| ~ v154858(sK54)
| spl55_7 ),
inference(resolution,[],[f151291,f146087]) ).
fof(f151318,definition,
( spl55_11
<=> v154858(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_11])],[avatar_definition]) ).
fof(f151320,plain,
( ~ v154858(sK54)
| spl55_11 ),
inference(avatar_component_clause,[],[f151318]) ).
fof(f151322,definition,
( spl55_12
<=> v154857(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_12])],[avatar_definition]) ).
fof(f151323,plain,
( v154857(sK54)
| ~ spl55_12 ),
inference(avatar_component_clause,[],[f151322]) ).
fof(f151324,plain,
( ~ v154857(sK54)
| spl55_12 ),
inference(avatar_component_clause,[],[f151322]) ).
fof(f151325,plain,
( ~ spl55_11
| ~ spl55_12
| spl55_7 ),
inference(avatar_split_clause,[],[f151316,f151289,f151322,f151318]) ).
fof(f151332,plain,
( ~ v154859(sK54)
| spl55_2 ),
inference(resolution,[],[f151256,f146059]) ).
fof(f151333,plain,
( ~ v154851(sK54)
| spl55_2 ),
inference(resolution,[],[f151256,f146060]) ).
fof(f151334,plain,
( ~ spl55_4
| spl55_2 ),
inference(avatar_split_clause,[],[f151333,f151254,f151274]) ).
fof(f151335,plain,
( ~ v154861(sK54)
| spl55_2 ),
inference(resolution,[],[f151332,f146064]) ).
fof(f151336,plain,
( ~ v154860(sK54)
| spl55_2 ),
inference(resolution,[],[f151332,f146065]) ).
fof(f151337,plain,
( ~ spl55_6
| spl55_2 ),
inference(avatar_split_clause,[],[f151335,f151254,f151283]) ).
fof(f151341,plain,
( v154864(sK54)
| ~ v154865(sK54)
| ~ spl55_8 ),
inference(resolution,[],[f151294,f146086]) ).
fof(f151343,plain,
( ~ v154865(sK54)
| spl55_5
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f151341,f151301]) ).
fof(f151344,plain,
( ~ v154841(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154839(sK54)
| spl55_10 ),
inference(resolution,[],[f151314,f146114]) ).
fof(f151346,plain,
( ~ v6(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154836(sK54)
| spl55_10 ),
inference(resolution,[],[f151314,f146084]) ).
fof(f151347,plain,
( ~ v6(sK54,bitIndex3)
| v154836(sK54)
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f151346,f151130]) ).
fof(f151348,plain,
( ~ v154841(sK54,bitIndex3)
| v154839(sK54)
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f151344,f151130]) ).
fof(f151350,definition,
( spl55_13
<=> v6(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_13])],[avatar_definition]) ).
fof(f151351,plain,
( v6(sK54,bitIndex3)
| ~ spl55_13 ),
inference(avatar_component_clause,[],[f151350]) ).
fof(f151352,plain,
( ~ v6(sK54,bitIndex3)
| spl55_13 ),
inference(avatar_component_clause,[],[f151350]) ).
fof(f151353,plain,
( spl55_9
| ~ spl55_13
| spl55_10 ),
inference(avatar_split_clause,[],[f151347,f151312,f151350,f151308]) ).
fof(f151355,definition,
( spl55_14
<=> v154839(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_14])],[avatar_definition]) ).
fof(f151356,plain,
( ~ v154839(sK54)
| spl55_14 ),
inference(avatar_component_clause,[],[f151355]) ).
fof(f151357,plain,
( v154839(sK54)
| ~ spl55_14 ),
inference(avatar_component_clause,[],[f151355]) ).
fof(f151359,definition,
( spl55_15
<=> v154841(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_15])],[avatar_definition]) ).
fof(f151360,plain,
( v154841(sK54,bitIndex3)
| ~ spl55_15 ),
inference(avatar_component_clause,[],[f151359]) ).
fof(f151361,plain,
( ~ v154841(sK54,bitIndex3)
| spl55_15 ),
inference(avatar_component_clause,[],[f151359]) ).
fof(f151362,plain,
( spl55_14
| ~ spl55_15
| spl55_10 ),
inference(avatar_split_clause,[],[f151348,f151312,f151359,f151355]) ).
fof(f151365,plain,
( v154853(sK54,bitIndex1)
| spl55_11 ),
inference(resolution,[],[f151320,f146073]) ).
fof(f151368,plain,
( ~ v154853(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl55_13 ),
inference(resolution,[],[f151352,f146068]) ).
fof(f151369,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151368,f151130]) ).
fof(f151370,plain,
( ~ v154867(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151343,f146090]) ).
fof(f151371,plain,
( ~ v154866(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151343,f146091]) ).
fof(f151372,plain,
( ~ v154844(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v1051(sK54)
| spl55_15 ),
inference(resolution,[],[f151361,f146190]) ).
fof(f151373,plain,
( ~ v154842(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| spl55_15 ),
inference(resolution,[],[f151361,f146188]) ).
fof(f151375,plain,
( ~ v154842(sK54,bitIndex3)
| ~ v1051(sK54)
| spl55_15 ),
inference(forward_subsumption_resolution,[],[f151373,f151130]) ).
fof(f151376,plain,
( ~ v154844(sK54,bitIndex3)
| v1051(sK54)
| spl55_15 ),
inference(forward_subsumption_resolution,[],[f151372,f151130]) ).
fof(f151378,definition,
( spl55_16
<=> v1051(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_16])],[avatar_definition]) ).
fof(f151379,plain,
( v1051(sK54)
| ~ spl55_16 ),
inference(avatar_component_clause,[],[f151378]) ).
fof(f151380,plain,
( ~ v1051(sK54)
| spl55_16 ),
inference(avatar_component_clause,[],[f151378]) ).
fof(f151382,definition,
( spl55_17
<=> v154842(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_17])],[avatar_definition]) ).
fof(f151383,plain,
( v154842(sK54,bitIndex3)
| ~ spl55_17 ),
inference(avatar_component_clause,[],[f151382]) ).
fof(f151384,plain,
( ~ v154842(sK54,bitIndex3)
| spl55_17 ),
inference(avatar_component_clause,[],[f151382]) ).
fof(f151385,plain,
( ~ spl55_16
| ~ spl55_17
| spl55_15 ),
inference(avatar_split_clause,[],[f151375,f151359,f151382,f151378]) ).
fof(f151387,definition,
( spl55_18
<=> v154844(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_18])],[avatar_definition]) ).
fof(f151388,plain,
( v154844(sK54,bitIndex3)
| ~ spl55_18 ),
inference(avatar_component_clause,[],[f151387]) ).
fof(f151389,plain,
( ~ v154844(sK54,bitIndex3)
| spl55_18 ),
inference(avatar_component_clause,[],[f151387]) ).
fof(f151390,plain,
( spl55_16
| ~ spl55_18
| spl55_15 ),
inference(avatar_split_clause,[],[f151376,f151359,f151387,f151378]) ).
fof(f151433,plain,
( v154852(sK54)
| spl55_13 ),
inference(resolution,[],[f151369,f146070]) ).
fof(f151435,plain,
( ~ v154853(sK54,bitIndex0)
| ~ v154858(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151370,f146077]) ).
fof(f151436,plain,
( ~ v83122(sK54,bitIndex0)
| spl55_18 ),
inference(resolution,[],[f151389,f146370]) ).
fof(f151438,plain,
( ~ v154857(sK54)
| ~ v154853(sK54,bitIndex1)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151371,f146076]) ).
fof(f151439,plain,
( ~ v154857(sK54)
| spl55_5
| ~ spl55_8
| spl55_11 ),
inference(forward_subsumption_resolution,[],[f151438,f151365]) ).
fof(f151440,plain,
( ~ spl55_12
| spl55_5
| ~ spl55_8
| spl55_11 ),
inference(avatar_split_clause,[],[f151439,f151318,f151293,f151279,f151322]) ).
fof(f151441,plain,
( v154853(sK54,bitIndex0)
| spl55_12 ),
inference(resolution,[],[f151324,f146072]) ).
fof(f151485,plain,
( v154861(sK54)
| ~ v154862(sK54)
| spl55_13 ),
inference(resolution,[],[f151433,f146080]) ).
fof(f151525,plain,
( v154845(sK54)
| spl55_18 ),
inference(resolution,[],[f151436,f146894]) ).
fof(f151529,definition,
( spl55_31
<=> v83122(sK54,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl55_31])],[avatar_definition]) ).
fof(f151530,plain,
( ~ v83122(sK54,bitIndex1)
| spl55_31 ),
inference(avatar_component_clause,[],[f151529]) ).
fof(f151531,plain,
( v83122(sK54,bitIndex1)
| ~ spl55_31 ),
inference(avatar_component_clause,[],[f151529]) ).
fof(f151548,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| b0010(X0)
| ~ range_3_0(X0) )
| ~ spl55_14 ),
inference(resolution,[],[f151357,f146111]) ).
fof(f151560,plain,
( v83122(sK54,bitIndex0)
| ~ spl55_18 ),
inference(resolution,[],[f151388,f146369]) ).
fof(f151565,plain,
( ! [X0] :
( b0010(X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0)
| v154836(sK54) )
| ~ spl55_14 ),
inference(resolution,[],[f151548,f146084]) ).
fof(f151566,plain,
( ! [X0] :
( b0010(X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| v154836(sK54) )
| ~ spl55_14 ),
inference(duplicate_literal_removal,[],[f151565]) ).
fof(f151570,definition,
( spl55_35
<=> ! [X0] :
( b0010(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_35])],[avatar_definition]) ).
fof(f151571,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| b0010(X0)
| ~ range_3_0(X0) )
| ~ spl55_35 ),
inference(avatar_component_clause,[],[f151570]) ).
fof(f151572,plain,
( spl55_9
| spl55_35
| ~ spl55_14 ),
inference(avatar_split_clause,[],[f151566,f151355,f151570,f151308]) ).
fof(f151576,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| spl55_14 ),
inference(resolution,[],[f151356,f146113]) ).
fof(f151591,plain,
( ! [X0] :
( ~ v154842(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_16 ),
inference(resolution,[],[f151379,f146188]) ).
fof(f151649,plain,
( ~ v83122(sK54,bitIndex1)
| spl55_17 ),
inference(resolution,[],[f151384,f146365]) ).
fof(f151651,plain,
( ~ spl55_31
| spl55_17 ),
inference(avatar_split_clause,[],[f151649,f151382,f151529]) ).
fof(f151658,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0)
| v154836(sK54) )
| spl55_14 ),
inference(resolution,[],[f151576,f146084]) ).
fof(f151659,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| v154836(sK54) )
| spl55_14 ),
inference(duplicate_literal_removal,[],[f151658]) ).
fof(f151663,definition,
( spl55_45
<=> ! [X0] :
( v154841(sK54,X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_45])],[avatar_definition]) ).
fof(f151664,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_45 ),
inference(avatar_component_clause,[],[f151663]) ).
fof(f151665,plain,
( spl55_9
| spl55_45
| spl55_14 ),
inference(avatar_split_clause,[],[f151659,f151355,f151663,f151308]) ).
fof(f151668,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151310,f146082]) ).
fof(f151678,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151668,f146068]) ).
fof(f151679,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl55_9 ),
inference(duplicate_literal_removal,[],[f151678]) ).
fof(f151711,plain,
( ~ range_3_0(bitIndex2)
| b0001(bitIndex2)
| v154855(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f151679,f146071]) ).
fof(f151713,plain,
( ~ range_3_0(bitIndex1)
| b0001(bitIndex1)
| v154858(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f151679,f146073]) ).
fof(f151715,plain,
( b0001(bitIndex1)
| v154858(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151713,f151128]) ).
fof(f151717,plain,
( v154858(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151715,f146096]) ).
fof(f151722,plain,
( ~ v154858(sK54)
| spl55_5
| ~ spl55_8
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151435,f151441]) ).
fof(f151735,plain,
( ~ v154862(sK54)
| spl55_6
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151485,f151284]) ).
fof(f151738,plain,
( $false
| ~ spl55_5
| spl55_6
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151735,f151280]) ).
fof(f151739,plain,
( ~ spl55_5
| spl55_6
| spl55_13 ),
inference(avatar_contradiction_clause,[],[f151738]) ).
fof(f151750,plain,
( b0001(bitIndex2)
| v154855(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151711,f151129]) ).
fof(f151751,plain,
( v154855(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151750,f146097]) ).
fof(f151752,plain,
( $false
| spl55_8
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151751,f151295]) ).
fof(f151753,plain,
( spl55_8
| ~ spl55_9 ),
inference(avatar_contradiction_clause,[],[f151752]) ).
fof(f151764,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151309,f146084]) ).
fof(f151765,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| v6(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151309,f146085]) ).
fof(f151767,plain,
( v154853(sK54,bitIndex2)
| spl55_8 ),
inference(resolution,[],[f151295,f146071]) ).
fof(f151778,plain,
( ! [X0] :
( v154838(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151764,f146068]) ).
fof(f151779,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154838(sK54,X0) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151778]) ).
fof(f151784,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ v154841(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| spl55_9 ),
inference(resolution,[],[f151765,f146114]) ).
fof(f151785,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ range_3_0(X0)
| ~ v154839(sK54) )
| spl55_9 ),
inference(resolution,[],[f151765,f146112]) ).
fof(f151788,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ v154839(sK54) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151785]) ).
fof(f151789,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ v154841(sK54,X0)
| v154839(sK54) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151784]) ).
fof(f151797,plain,
( v154863(sK54)
| ~ v154856(sK54)
| spl55_8 ),
inference(resolution,[],[f151767,f146075]) ).
fof(f151799,plain,
( v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_8 ),
inference(resolution,[],[f151767,f146068]) ).
fof(f151800,plain,
( v6(sK54,bitIndex2)
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f151799,f151129]) ).
fof(f151816,plain,
( ~ range_3_0(bitIndex2)
| v154838(sK54,bitIndex2)
| spl55_8
| spl55_9 ),
inference(resolution,[],[f151779,f151767]) ).
fof(f151820,plain,
( ~ range_3_0(bitIndex0)
| v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(resolution,[],[f151779,f146072]) ).
fof(f151821,plain,
( ~ range_3_0(bitIndex1)
| v154838(sK54,bitIndex1)
| v154858(sK54)
| spl55_9 ),
inference(resolution,[],[f151779,f146073]) ).
fof(f151823,plain,
( v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151820,f151127]) ).
fof(f151825,plain,
( v154838(sK54,bitIndex2)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151816,f151129]) ).
fof(f151826,plain,
( v154838(sK54,bitIndex0)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151823,f151324]) ).
fof(f151851,plain,
( ~ v154845(sK54)
| ~ spl55_18 ),
inference(resolution,[],[f151560,f146895]) ).
fof(f151913,plain,
( b0010(bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(resolution,[],[f151825,f146111]) ).
fof(f151921,plain,
( v154841(sK54,bitIndex0)
| ~ range_3_0(bitIndex0)
| v154839(sK54)
| spl55_9
| spl55_12 ),
inference(resolution,[],[f151826,f146113]) ).
fof(f151922,plain,
( b0010(bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(resolution,[],[f151826,f146111]) ).
fof(f151924,plain,
( v154841(sK54,bitIndex0)
| v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151921,f151127]) ).
fof(f152068,plain,
( ~ v154844(sK54,bitIndex2)
| ~ spl55_18 ),
inference(resolution,[],[f151851,f146371]) ).
fof(f152071,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154843(sK54)
| ~ spl55_16 ),
inference(resolution,[],[f151591,f146367]) ).
fof(f152075,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_8
| ~ spl55_45 ),
inference(resolution,[],[f151664,f151800]) ).
fof(f152078,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_45 ),
inference(resolution,[],[f151664,f146068]) ).
fof(f152079,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154841(sK54,X0) )
| ~ spl55_45 ),
inference(duplicate_literal_removal,[],[f152078]) ).
fof(f152152,plain,
( v154843(sK54)
| spl55_31 ),
inference(resolution,[],[f151530,f146892]) ).
fof(f152201,plain,
( ~ range_3_0(bitIndex2)
| ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151913,f146181]) ).
fof(f152202,plain,
( ~ range_3_0(bitIndex0)
| ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151922,f146179]) ).
fof(f152203,plain,
( v154841(sK54,bitIndex2)
| ~ v154843(sK54)
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152071,f151129]) ).
fof(f152205,plain,
( v154841(sK54,bitIndex2)
| spl55_8
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152075,f151129]) ).
fof(f152210,plain,
( ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f152201,f151129]) ).
fof(f152211,plain,
( ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f152202,f151127]) ).
fof(f152213,definition,
( spl55_72
<=> v154843(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_72])],[avatar_definition]) ).
fof(f152214,plain,
( v154843(sK54)
| ~ spl55_72 ),
inference(avatar_component_clause,[],[f152213]) ).
fof(f152215,plain,
( ~ v154843(sK54)
| spl55_72 ),
inference(avatar_component_clause,[],[f152213]) ).
fof(f152217,definition,
( spl55_73
<=> v154841(sK54,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl55_73])],[avatar_definition]) ).
fof(f152219,plain,
( v154841(sK54,bitIndex2)
| ~ spl55_73 ),
inference(avatar_component_clause,[],[f152217]) ).
fof(f152220,plain,
( ~ spl55_72
| spl55_73
| ~ spl55_16 ),
inference(avatar_split_clause,[],[f152203,f151378,f152217,f152213]) ).
fof(f152221,plain,
( spl55_73
| spl55_8
| ~ spl55_45 ),
inference(avatar_split_clause,[],[f152205,f151663,f151293,f152217]) ).
fof(f152228,plain,
( $false
| spl55_8
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f152210,f151357]) ).
fof(f152229,plain,
( spl55_8
| spl55_9
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f152228]) ).
fof(f152232,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| ~ range_3_0(X0)
| v6(sK54,X0) )
| spl55_9
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f151789,f151356]) ).
fof(f152233,plain,
( v154841(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f151924,f151356]) ).
fof(f152252,plain,
( spl55_72
| spl55_31 ),
inference(avatar_split_clause,[],[f152152,f151529,f152213]) ).
fof(f152259,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_14 ),
inference(resolution,[],[f151356,f146114]) ).
fof(f152263,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154842(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_16 ),
inference(resolution,[],[f151379,f146187]) ).
fof(f152422,plain,
( ! [X0] :
( v154842(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| ~ spl55_16 ),
inference(resolution,[],[f152263,f146113]) ).
fof(f152423,plain,
( ! [X0] :
( v154842(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| v154839(sK54) )
| ~ spl55_16 ),
inference(duplicate_literal_removal,[],[f152422]) ).
fof(f152426,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154842(sK54,X0) )
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152423,f151356]) ).
fof(f152548,plain,
( v154838(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_14
| ~ spl55_73 ),
inference(resolution,[],[f152219,f152259]) ).
fof(f152549,plain,
( ~ range_3_0(bitIndex2)
| v6(sK54,bitIndex2)
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(resolution,[],[f152219,f152232]) ).
fof(f152555,plain,
( v154842(sK54,bitIndex0)
| ~ range_3_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f152233,f152263]) ).
fof(f152562,plain,
( v154842(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152555,f151127]) ).
fof(f152702,plain,
( ~ range_3_0(bitIndex3)
| v154841(sK54,bitIndex3)
| v154852(sK54)
| ~ spl55_45 ),
inference(resolution,[],[f152079,f146070]) ).
fof(f152705,plain,
( ~ range_3_0(bitIndex1)
| v154841(sK54,bitIndex1)
| v154858(sK54)
| ~ spl55_45 ),
inference(resolution,[],[f152079,f146073]) ).
fof(f153817,plain,
( ~ range_1_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f152562,f146368]) ).
fof(f153819,plain,
( $false
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153817,f151142]) ).
fof(f153820,plain,
( spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f153819]) ).
fof(f153821,plain,
( v154838(sK54,bitIndex1)
| v154858(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151821,f151128]) ).
fof(f153822,plain,
( v154841(sK54,bitIndex1)
| v154858(sK54)
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152705,f151128]) ).
fof(f153823,plain,
( v154838(sK54,bitIndex1)
| spl55_9
| spl55_11 ),
inference(forward_subsumption_resolution,[],[f153821,f151320]) ).
fof(f153824,plain,
( v154841(sK54,bitIndex1)
| spl55_11
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f153822,f151320]) ).
fof(f153827,plain,
( v154866(sK54)
| ~ v154853(sK54,bitIndex1)
| ~ spl55_12 ),
inference(resolution,[],[f151323,f146076]) ).
fof(f153830,plain,
( ~ range_3_0(bitIndex1)
| v154842(sK54,bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f153823,f152426]) ).
fof(f153838,plain,
( v154842(sK54,bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153830,f151128]) ).
fof(f154072,plain,
( v154844(sK54,bitIndex1)
| ~ range_3_0(bitIndex1)
| v1051(sK54)
| spl55_11
| ~ spl55_45 ),
inference(resolution,[],[f153824,f146189]) ).
fof(f154080,plain,
( ~ range_1_0(bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f153838,f146368]) ).
fof(f154082,plain,
( $false
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f154080,f151143]) ).
fof(f154083,plain,
( spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f154082]) ).
fof(f154085,definition,
( spl55_295
<=> v154853(sK54,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl55_295])],[avatar_definition]) ).
fof(f154087,plain,
( ~ v154853(sK54,bitIndex1)
| spl55_295 ),
inference(avatar_component_clause,[],[f154085]) ).
fof(f154089,definition,
( spl55_296
<=> v154866(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_296])],[avatar_definition]) ).
fof(f154092,plain,
( ~ spl55_295
| spl55_296
| ~ spl55_12 ),
inference(avatar_split_clause,[],[f153827,f151322,f154089,f154085]) ).
fof(f154094,plain,
( ~ v154856(sK54)
| spl55_5
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f151797,f151302]) ).
fof(f154097,plain,
( $false
| spl55_5
| ~ spl55_7
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f154094,f151290]) ).
fof(f154098,plain,
( spl55_5
| ~ spl55_7
| spl55_8 ),
inference(avatar_contradiction_clause,[],[f154097]) ).
fof(f154103,plain,
( v6(sK54,bitIndex2)
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f152549,f151129]) ).
fof(f154104,plain,
( v154838(sK54,bitIndex2)
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f152548,f151129]) ).
fof(f154113,plain,
( ~ v154853(sK54,bitIndex2)
| spl55_1 ),
inference(resolution,[],[f151259,f146066]) ).
fof(f154117,plain,
( v154860(sK54)
| ~ v154853(sK54,bitIndex3)
| ~ spl55_3 ),
inference(resolution,[],[f151271,f146074]) ).
fof(f154118,plain,
( v154851(sK54)
| ~ v154852(sK54)
| ~ spl55_3 ),
inference(resolution,[],[f151271,f146063]) ).
fof(f154120,plain,
( ~ v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_1 ),
inference(resolution,[],[f154113,f146069]) ).
fof(f154121,plain,
( ~ range_3_0(bitIndex2)
| spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154120,f154103]) ).
fof(f154122,plain,
( $false
| spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154121,f151129]) ).
fof(f154123,plain,
( spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f154122]) ).
fof(f154125,plain,
( ~ v154852(sK54)
| ~ spl55_3
| spl55_4 ),
inference(forward_subsumption_resolution,[],[f154118,f151275]) ).
fof(f154137,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0) )
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f151788,f151357]) ).
fof(f154153,plain,
( ~ v154852(sK54)
| ~ v154862(sK54)
| spl55_6 ),
inference(resolution,[],[f151284,f146080]) ).
fof(f154155,plain,
( v154863(sK54)
| ~ v154853(sK54,bitIndex2)
| ~ spl55_7 ),
inference(resolution,[],[f151290,f146075]) ).
fof(f154193,plain,
( v83122(sK54,bitIndex1)
| ~ spl55_17 ),
inference(resolution,[],[f151383,f146364]) ).
fof(f154209,plain,
( ! [X0] :
( ~ range_3_0(X0)
| ~ b0010(X0)
| v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9
| ~ spl55_14 ),
inference(resolution,[],[f154137,f146069]) ).
fof(f154210,plain,
( ! [X0] :
( v154853(sK54,X0)
| ~ b0010(X0)
| ~ range_3_0(X0) )
| spl55_9
| ~ spl55_14 ),
inference(duplicate_literal_removal,[],[f154209]) ).
fof(f154241,plain,
( ~ v154842(sK54,bitIndex2)
| spl55_72 ),
inference(resolution,[],[f152215,f146366]) ).
fof(f154281,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(resolution,[],[f154210,f154087]) ).
fof(f154289,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(resolution,[],[f154210,f146078]) ).
fof(f154295,plain,
( ~ range_3_0(bitIndex1)
| v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154289,f146180]) ).
fof(f154296,plain,
( ~ range_3_0(bitIndex1)
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(forward_subsumption_resolution,[],[f154281,f146180]) ).
fof(f154298,plain,
( v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154295,f151128]) ).
fof(f154299,plain,
( $false
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(forward_subsumption_resolution,[],[f154296,f151128]) ).
fof(f154300,plain,
( spl55_9
| ~ spl55_14
| spl55_295 ),
inference(avatar_contradiction_clause,[],[f154299]) ).
fof(f154302,plain,
( $false
| spl55_1
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154298,f151261]) ).
fof(f154303,plain,
( spl55_1
| spl55_9
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f154302]) ).
fof(f154306,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_2
| ~ spl55_3 ),
inference(forward_subsumption_resolution,[],[f154117,f151336]) ).
fof(f154308,definition,
( spl55_301
<=> v154853(sK54,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl55_301])],[avatar_definition]) ).
fof(f154310,plain,
( ~ v154853(sK54,bitIndex2)
| spl55_301 ),
inference(avatar_component_clause,[],[f154308]) ).
fof(f154312,definition,
( spl55_302
<=> v154863(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_302])],[avatar_definition]) ).
fof(f154315,plain,
( ~ spl55_301
| spl55_302
| ~ spl55_7 ),
inference(avatar_split_clause,[],[f154155,f151289,f154312,f154308]) ).
fof(f154333,plain,
( v154853(sK54,bitIndex3)
| ~ spl55_3
| spl55_4 ),
inference(resolution,[],[f154125,f146070]) ).
fof(f154334,plain,
( $false
| spl55_2
| ~ spl55_3
| spl55_4 ),
inference(forward_subsumption_resolution,[],[f154333,f154306]) ).
fof(f154335,plain,
( spl55_2
| ~ spl55_3
| spl55_4 ),
inference(avatar_contradiction_clause,[],[f154334]) ).
fof(f154339,plain,
( ~ v154852(sK54)
| ~ spl55_5
| spl55_6 ),
inference(forward_subsumption_resolution,[],[f154153,f151280]) ).
fof(f154347,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v154839(sK54)
| ~ spl55_10 ),
inference(resolution,[],[f151313,f146111]) ).
fof(f154349,plain,
( ~ range_3_0(bitIndex3)
| ~ v154839(sK54)
| ~ spl55_10 ),
inference(forward_subsumption_resolution,[],[f154347,f146182]) ).
fof(f154350,plain,
( ~ v154839(sK54)
| ~ spl55_10 ),
inference(forward_subsumption_resolution,[],[f154349,f151130]) ).
fof(f154351,plain,
( $false
| ~ spl55_10
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154350,f151357]) ).
fof(f154352,plain,
( ~ spl55_10
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f154351]) ).
fof(f154353,plain,
( spl55_11
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f151717,f151308,f151318]) ).
fof(f154363,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ b0001(X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151310,f146083]) ).
fof(f154369,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ spl55_13
| ~ spl55_35 ),
inference(resolution,[],[f151351,f151571]) ).
fof(f154372,plain,
( b0001(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v154836(sK54)
| ~ spl55_13 ),
inference(resolution,[],[f151351,f146082]) ).
fof(f154374,plain,
( ~ range_3_0(bitIndex3)
| ~ v154836(sK54)
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154372,f146098]) ).
fof(f154375,plain,
( ~ range_3_0(bitIndex3)
| ~ spl55_13
| ~ spl55_35 ),
inference(forward_subsumption_resolution,[],[f154369,f146182]) ).
fof(f154376,plain,
( ~ v154836(sK54)
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154374,f151130]) ).
fof(f154377,plain,
( $false
| ~ spl55_13
| ~ spl55_35 ),
inference(forward_subsumption_resolution,[],[f154375,f151130]) ).
fof(f154378,plain,
( ~ spl55_13
| ~ spl55_35 ),
inference(avatar_contradiction_clause,[],[f154377]) ).
fof(f154379,plain,
( $false
| ~ spl55_9
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154376,f151310]) ).
fof(f154380,plain,
( ~ spl55_9
| ~ spl55_13 ),
inference(avatar_contradiction_clause,[],[f154379]) ).
fof(f154420,plain,
( ! [X0] :
( ~ b0001(X0)
| ~ range_3_0(X0)
| v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f154363,f146069]) ).
fof(f154421,plain,
( ! [X0] :
( v154853(sK54,X0)
| ~ range_3_0(X0)
| ~ b0001(X0) )
| ~ spl55_9 ),
inference(duplicate_literal_removal,[],[f154420]) ).
fof(f154434,plain,
( ~ v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_301 ),
inference(resolution,[],[f154310,f146069]) ).
fof(f154435,plain,
( ~ v6(sK54,bitIndex2)
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154434,f151129]) ).
fof(f154463,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v154870(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f154421,f146079]) ).
fof(f154470,plain,
( ~ b0001(bitIndex0)
| v154870(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154463,f151127]) ).
fof(f154471,plain,
( v154870(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154470,f146095]) ).
fof(f154472,plain,
( $false
| spl55_1
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154471,f151261]) ).
fof(f154473,plain,
( spl55_1
| ~ spl55_9 ),
inference(avatar_contradiction_clause,[],[f154472]) ).
fof(f154474,plain,
( ~ spl55_302
| spl55_5 ),
inference(avatar_split_clause,[],[f151302,f151279,f154312]) ).
fof(f154478,plain,
( ~ spl55_296
| spl55_5
| ~ spl55_8 ),
inference(avatar_split_clause,[],[f151371,f151293,f151279,f154089]) ).
fof(f154479,plain,
( ~ spl55_11
| spl55_5
| ~ spl55_8
| spl55_12 ),
inference(avatar_split_clause,[],[f151722,f151322,f151293,f151279,f151318]) ).
fof(f154480,plain,
( ~ spl55_14
| spl55_9
| spl55_12 ),
inference(avatar_split_clause,[],[f152211,f151322,f151308,f151355]) ).
fof(f154482,plain,
( v154844(sK54,bitIndex1)
| v1051(sK54)
| spl55_11
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154072,f151128]) ).
fof(f154505,plain,
( v154841(sK54,bitIndex3)
| v154852(sK54)
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152702,f151130]) ).
fof(f154508,plain,
( v154844(sK54,bitIndex1)
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154482,f151380]) ).
fof(f154581,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151309,f146084]) ).
fof(f154598,plain,
( ! [X0] :
( v154838(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f154581,f146068]) ).
fof(f154599,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154838(sK54,X0) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f154598]) ).
fof(f154602,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154844(sK54,X0)
| ~ range_3_0(X0) )
| spl55_16 ),
inference(resolution,[],[f151380,f146189]) ).
fof(f154603,plain,
( ! [X0] :
( ~ v154844(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| spl55_16 ),
inference(resolution,[],[f151380,f146190]) ).
fof(f154641,plain,
( ~ v154841(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v1051(sK54)
| spl55_18 ),
inference(resolution,[],[f151389,f146189]) ).
fof(f154664,plain,
( ~ range_3_0(bitIndex0)
| v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(resolution,[],[f154599,f146072]) ).
fof(f154667,plain,
( v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f154664,f151127]) ).
fof(f154668,plain,
( v154838(sK54,bitIndex0)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f154667,f151324]) ).
fof(f154734,plain,
( ~ v154838(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| v154836(sK54)
| spl55_301 ),
inference(resolution,[],[f154435,f146085]) ).
fof(f154737,plain,
( ~ v154838(sK54,bitIndex2)
| v154836(sK54)
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154734,f151129]) ).
fof(f154738,plain,
( ~ v154838(sK54,bitIndex2)
| spl55_9
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154737,f151309]) ).
fof(f154862,plain,
( ! [X0] :
( v154844(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| spl55_16 ),
inference(resolution,[],[f154602,f146113]) ).
fof(f154863,plain,
( ! [X0] :
( v154844(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| v154839(sK54) )
| spl55_16 ),
inference(duplicate_literal_removal,[],[f154862]) ).
fof(f154866,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154844(sK54,X0) )
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f154863,f151356]) ).
fof(f154873,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154845(sK54)
| spl55_16 ),
inference(resolution,[],[f154603,f146372]) ).
fof(f154875,plain,
( v154841(sK54,bitIndex2)
| ~ v154845(sK54)
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f154873,f151129]) ).
fof(f154876,plain,
( v154841(sK54,bitIndex2)
| spl55_16
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f154875,f151525]) ).
fof(f154877,plain,
( spl55_73
| spl55_16
| spl55_18 ),
inference(avatar_split_clause,[],[f154876,f151387,f151378,f152217]) ).
fof(f154880,plain,
( $false
| spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154104,f154738]) ).
fof(f154881,plain,
( spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(avatar_contradiction_clause,[],[f154880]) ).
fof(f154938,plain,
( ~ v154843(sK54)
| ~ spl55_31 ),
inference(resolution,[],[f151531,f146893]) ).
fof(f154968,plain,
( v154844(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| v1051(sK54)
| ~ spl55_73 ),
inference(resolution,[],[f152219,f146189]) ).
fof(f155165,plain,
( ~ range_3_0(bitIndex0)
| v154844(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(resolution,[],[f154866,f154668]) ).
fof(f155173,plain,
( v154844(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f155165,f151127]) ).
fof(f155854,plain,
( ~ v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v1051(sK54)
| spl55_72 ),
inference(resolution,[],[f154241,f146187]) ).
fof(f155924,plain,
( ~ range_1_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(resolution,[],[f155173,f146373]) ).
fof(f155926,plain,
( $false
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f155924,f151142]) ).
fof(f155927,plain,
( spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(avatar_contradiction_clause,[],[f155926]) ).
fof(f155932,plain,
( v154852(sK54)
| spl55_15
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154505,f151361]) ).
fof(f155943,plain,
( $false
| ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f155932,f154339]) ).
fof(f155944,plain,
( ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(avatar_contradiction_clause,[],[f155943]) ).
fof(f155948,plain,
( ~ range_3_0(bitIndex3)
| v1051(sK54)
| ~ spl55_15
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f154641,f151360]) ).
fof(f155949,plain,
( v1051(sK54)
| ~ spl55_15
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f155948,f151130]) ).
fof(f155950,plain,
( $false
| ~ spl55_15
| spl55_16
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f155949,f151380]) ).
fof(f155951,plain,
( ~ spl55_15
| spl55_16
| spl55_18 ),
inference(avatar_contradiction_clause,[],[f155950]) ).
fof(f155958,plain,
( ~ range_3_0(bitIndex2)
| v1051(sK54)
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154968,f152068]) ).
fof(f155964,plain,
( v1051(sK54)
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155958,f151129]) ).
fof(f155971,plain,
( $false
| spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155964,f151380]) ).
fof(f155972,plain,
( spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f155971]) ).
fof(f155997,plain,
( v154842(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| ~ spl55_15 ),
inference(resolution,[],[f151360,f146187]) ).
fof(f156866,plain,
( ~ range_1_0(bitIndex1)
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(resolution,[],[f154508,f146373]) ).
fof(f156868,plain,
( $false
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f156866,f151143]) ).
fof(f156869,plain,
( spl55_11
| spl55_16
| ~ spl55_45 ),
inference(avatar_contradiction_clause,[],[f156868]) ).
fof(f156880,plain,
( ~ range_3_0(bitIndex2)
| ~ v1051(sK54)
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155854,f152219]) ).
fof(f156886,plain,
( ~ v1051(sK54)
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f156880,f151129]) ).
fof(f156887,plain,
( $false
| ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f156886,f151379]) ).
fof(f156888,plain,
( ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f156887]) ).
fof(f156889,plain,
( $false
| ~ spl55_31
| ~ spl55_72 ),
inference(forward_subsumption_resolution,[],[f154938,f152214]) ).
fof(f156890,plain,
( ~ spl55_31
| ~ spl55_72 ),
inference(avatar_contradiction_clause,[],[f156889]) ).
fof(f156908,plain,
( $false
| ~ spl55_17
| spl55_31 ),
inference(forward_subsumption_resolution,[],[f154193,f151530]) ).
fof(f156909,plain,
( ~ spl55_17
| spl55_31 ),
inference(avatar_contradiction_clause,[],[f156908]) ).
fof(f156922,plain,
( ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| ~ spl55_15
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f155997,f151384]) ).
fof(f156924,plain,
( ~ v1051(sK54)
| ~ spl55_15
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f156922,f151130]) ).
fof(f156925,plain,
( $false
| ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f156924,f151379]) ).
fof(f156926,plain,
( ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(avatar_contradiction_clause,[],[f156925]) ).
cnf(s1,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(sat_conversion,[],[f151257]) ).
cnf(s4,plain,
( spl55_3
| ~ spl55_7
| ~ spl55_8 ),
inference(sat_conversion,[],[f151296]) ).
cnf(s6,plain,
( spl55_1
| spl55_9
| ~ spl55_10 ),
inference(sat_conversion,[],[f151315]) ).
cnf(s7,plain,
( spl55_7
| ~ spl55_11
| ~ spl55_12 ),
inference(sat_conversion,[],[f151325]) ).
cnf(s9,plain,
( spl55_2
| ~ spl55_4 ),
inference(sat_conversion,[],[f151334]) ).
cnf(s10,plain,
( spl55_2
| ~ spl55_6 ),
inference(sat_conversion,[],[f151337]) ).
cnf(s11,plain,
( spl55_9
| spl55_10
| ~ spl55_13 ),
inference(sat_conversion,[],[f151353]) ).
cnf(s12,plain,
( spl55_10
| spl55_14
| ~ spl55_15 ),
inference(sat_conversion,[],[f151362]) ).
cnf(s13,plain,
( spl55_15
| ~ spl55_16
| ~ spl55_17 ),
inference(sat_conversion,[],[f151385]) ).
cnf(s14,plain,
( spl55_15
| spl55_16
| ~ spl55_18 ),
inference(sat_conversion,[],[f151390]) ).
cnf(s19,plain,
( spl55_5
| ~ spl55_8
| spl55_11
| ~ spl55_12 ),
inference(sat_conversion,[],[f151440]) ).
cnf(s26,plain,
( spl55_9
| ~ spl55_14
| spl55_35 ),
inference(sat_conversion,[],[f151572]) ).
cnf(s32,plain,
( spl55_17
| ~ spl55_31 ),
inference(sat_conversion,[],[f151651]) ).
cnf(s33,plain,
( spl55_9
| spl55_14
| spl55_45 ),
inference(sat_conversion,[],[f151665]) ).
cnf(s43,plain,
( ~ spl55_5
| spl55_6
| spl55_13 ),
inference(sat_conversion,[],[f151739]) ).
cnf(s47,plain,
( spl55_8
| ~ spl55_9 ),
inference(sat_conversion,[],[f151753]) ).
cnf(s83,plain,
( ~ spl55_16
| ~ spl55_72
| spl55_73 ),
inference(sat_conversion,[],[f152220]) ).
cnf(s84,plain,
( spl55_8
| ~ spl55_45
| spl55_73 ),
inference(sat_conversion,[],[f152221]) ).
cnf(s88,plain,
( spl55_8
| spl55_9
| ~ spl55_14 ),
inference(sat_conversion,[],[f152229]) ).
cnf(s100,plain,
( spl55_31
| spl55_72 ),
inference(sat_conversion,[],[f152252]) ).
cnf(s197,plain,
( spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(sat_conversion,[],[f153820]) ).
cnf(s219,plain,
( spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(sat_conversion,[],[f154083]) ).
cnf(s220,plain,
( ~ spl55_12
| ~ spl55_295
| spl55_296 ),
inference(sat_conversion,[],[f154092]) ).
cnf(s222,plain,
( spl55_5
| ~ spl55_7
| spl55_8 ),
inference(sat_conversion,[],[f154098]) ).
cnf(s225,plain,
( spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(sat_conversion,[],[f154123]) ).
cnf(s239,plain,
( spl55_9
| ~ spl55_14
| spl55_295 ),
inference(sat_conversion,[],[f154300]) ).
cnf(s240,plain,
( spl55_1
| spl55_9
| ~ spl55_14 ),
inference(sat_conversion,[],[f154303]) ).
cnf(s244,plain,
( ~ spl55_7
| ~ spl55_301
| spl55_302 ),
inference(sat_conversion,[],[f154315]) ).
cnf(s246,plain,
( spl55_2
| ~ spl55_3
| spl55_4 ),
inference(sat_conversion,[],[f154335]) ).
cnf(s247,plain,
( ~ spl55_10
| ~ spl55_14 ),
inference(sat_conversion,[],[f154352]) ).
cnf(s249,plain,
( ~ spl55_9
| spl55_11 ),
inference(sat_conversion,[],[f154353]) ).
cnf(s251,plain,
( ~ spl55_13
| ~ spl55_35 ),
inference(sat_conversion,[],[f154378]) ).
cnf(s252,plain,
( ~ spl55_9
| ~ spl55_13 ),
inference(sat_conversion,[],[f154380]) ).
cnf(s255,plain,
( spl55_1
| ~ spl55_9 ),
inference(sat_conversion,[],[f154473]) ).
cnf(s263,plain,
( spl55_5
| ~ spl55_302 ),
inference(sat_conversion,[],[f154474]) ).
cnf(s267,plain,
( spl55_5
| ~ spl55_8
| ~ spl55_296 ),
inference(sat_conversion,[],[f154478]) ).
cnf(s268,plain,
( spl55_5
| ~ spl55_8
| ~ spl55_11
| spl55_12 ),
inference(sat_conversion,[],[f154479]) ).
cnf(s271,plain,
( spl55_9
| spl55_12
| ~ spl55_14 ),
inference(sat_conversion,[],[f154480]) ).
cnf(s319,plain,
( spl55_16
| spl55_18
| spl55_73 ),
inference(sat_conversion,[],[f154877]) ).
cnf(s321,plain,
( spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(sat_conversion,[],[f154881]) ).
cnf(s431,plain,
( spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(sat_conversion,[],[f155927]) ).
cnf(s436,plain,
( ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(sat_conversion,[],[f155944]) ).
cnf(s438,plain,
( ~ spl55_15
| spl55_16
| spl55_18 ),
inference(sat_conversion,[],[f155951]) ).
cnf(s445,plain,
( spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(sat_conversion,[],[f155972]) ).
cnf(s510,plain,
( spl55_11
| spl55_16
| ~ spl55_45 ),
inference(sat_conversion,[],[f156869]) ).
cnf(s514,plain,
( ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(sat_conversion,[],[f156888]) ).
cnf(s515,plain,
( ~ spl55_31
| ~ spl55_72 ),
inference(sat_conversion,[],[f156890]) ).
cnf(s526,plain,
( ~ spl55_17
| spl55_31 ),
inference(sat_conversion,[],[f156909]) ).
cnf(s529,plain,
( ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(sat_conversion,[],[f156926]) ).
cnf(s550,plain,
( spl55_16
| spl55_1 ),
inference(rat,[],[s319,s14,s225,s12,s6,s240,s255]) ).
cnf(s551,plain,
( spl55_1
| spl55_9 ),
inference(rat,[],[s100,s32,s83,s13,s550,s12,s225,s6,s240]) ).
cnf(s552,plain,
spl55_1,
inference(rat,[],[s551,s255]) ).
cnf(s553,plain,
~ spl55_2,
inference(rat,[],[s1,s552]) ).
cnf(s554,plain,
~ spl55_6,
inference(rat,[],[s10,s553]) ).
cnf(s555,plain,
~ spl55_4,
inference(rat,[],[s9,s553]) ).
cnf(s556,plain,
~ spl55_3,
inference(rat,[],[s246,s553,s555]) ).
cnf(s557,plain,
( spl55_14
| spl55_302
| spl55_9
| ~ spl55_73
| spl55_16 ),
inference(rat,[],[s7,s244,s510,s431,s321,s33]) ).
cnf(s558,plain,
( spl55_5
| spl55_9
| ~ spl55_73
| spl55_16 ),
inference(rat,[],[s267,s220,s88,s271,s239,s557,s263]) ).
cnf(s559,plain,
( spl55_9
| spl55_16
| spl55_15 ),
inference(rat,[],[s247,s11,s33,s43,s436,s558,s319,s14,s554]) ).
cnf(s560,plain,
( ~ spl55_8
| spl55_5
| ~ spl55_11 ),
inference(rat,[],[s7,s4,s268,s556]) ).
cnf(s561,plain,
~ spl55_9,
inference(rat,[],[s560,s43,s47,s249,s252,s554]) ).
cnf(s562,plain,
( spl55_14
| spl55_302
| spl55_15 ),
inference(rat,[],[s244,s7,s321,s197,s219,s83,s100,s32,s13,s559,s561]) ).
cnf(s563,plain,
( spl55_5
| spl55_15 ),
inference(rat,[],[s19,s560,s88,s271,s562,s263,s561]) ).
cnf(s564,plain,
( ~ spl55_5
| spl55_15 ),
inference(rat,[],[s247,s11,s33,s43,s436,s554,s561]) ).
cnf(s565,plain,
spl55_15,
inference(rat,[],[s564,s563]) ).
cnf(s566,plain,
( spl55_16
| ~ spl55_45
| spl55_5 ),
inference(rat,[],[s560,s84,s510,s558,s561]) ).
cnf(s567,plain,
( spl55_14
| spl55_5 ),
inference(rat,[],[s222,s7,s560,s197,s219,s566,s33,s561]) ).
cnf(s568,plain,
spl55_5,
inference(rat,[],[s19,s560,s88,s271,s567,s561]) ).
cnf(s569,plain,
spl55_13,
inference(rat,[],[s43,s554,s568]) ).
cnf(s570,plain,
~ spl55_35,
inference(rat,[],[s251,s569]) ).
cnf(s572,plain,
~ spl55_14,
inference(rat,[],[s26,s561,s570]) ).
cnf(s573,plain,
spl55_45,
inference(rat,[],[s33,s561,s572]) ).
cnf(s574,plain,
spl55_16,
inference(rat,[],[s4,s84,s7,s445,s510,s431,s438,s556,s573,s561,s572,s565]) ).
cnf(s577,plain,
spl55_17,
inference(rat,[],[s529,s565,s574]) ).
cnf(s578,plain,
spl55_11,
inference(rat,[],[s219,s572,s561,s574]) ).
cnf(s579,plain,
spl55_12,
inference(rat,[],[s197,s572,s561,s574]) ).
cnf(s580,plain,
spl55_31,
inference(rat,[],[s526,s577]) ).
cnf(s581,plain,
spl55_7,
inference(rat,[],[s7,s579,s578]) ).
cnf(s582,plain,
~ spl55_72,
inference(rat,[],[s515,s580]) ).
cnf(s583,plain,
~ spl55_8,
inference(rat,[],[s4,s556,s581]) ).
cnf(s584,plain,
~ spl55_73,
inference(rat,[],[s514,s574,s582]) ).
cnf(s585,plain,
$false,
inference(rat,[],[s84,s573,s584,s583]) ).
fof(f156927,plain,
$false,
inference(avatar_sat_refutation,[],[s585]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HWV125+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.13 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.53 % Computer : n007.cluster.edu
% 0.21/0.53 % Model : x86_64 x86_64
% 0.21/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.53 % Memory : 8046.5625MB
% 0.21/0.53 % OS : Linux 6.8.0-71-generic
% 0.21/0.53 % CPULimit : 300
% 0.21/0.53 % WCLimit : 300
% 0.21/0.53 % DateTime : Sun Sep 27 11:40:56 UTC 2026
% 0.21/0.53 % CPUTime :
% 0.21/0.53 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.32/0.64 Running first-order theorem proving
% 0.32/0.64 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.52/7.70 % (1268109)Detected formulas, will run a generic FOF schedule.
% 25.52/7.70 % (1268147)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2714837498:i=141193_2966 on theBenchmark for (2966ds/141193Mi)
% 25.52/7.70 % (1268148)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2054583480:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2966 on theBenchmark for (2966ds/134677Mi)
% 25.52/7.70 % (1268149)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1142424884:i=141695:sd=1:nm=32:gsp=on:ss=included_2966 on theBenchmark for (2966ds/141695Mi)
% 25.52/7.70 % (1268150)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2738560904:i=109:sd=1:ins=1:gsp=on:ss=axioms_2966 on theBenchmark for (2966ds/109Mi)
% 25.52/7.70 % (1268151)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2028750959:i=119:av=off:ss=axioms_2966 on theBenchmark for (2966ds/119Mi)
% 25.52/7.70 % (1268153)dis-21_1_sil=8000:lcm=predicate:random_seed=2271105276:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2966 on theBenchmark for (2966ds/129Mi)
% 25.52/7.70 % (1268152)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3653989868:s2a=on:i=139:gtg=position_2966 on theBenchmark for (2966ds/139Mi)
% 25.52/7.70 % (1268150)Instruction limit reached!
% 25.52/7.70 % (1268150)------------------------------
% 25.52/7.70 % (1268150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/7.70 % (1268150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/7.70 % (1268150)CaDiCaL version: 2.1.3
% 25.52/7.70 % (1268150)Termination reason: Instruction limit
% 25.52/7.70 % (1268150)Termination phase: SInE selection
% 25.52/7.70 % (1268150)Time elapsed: 0.067 s
% 25.52/7.70 % (1268150)Peak memory usage: 205 MB
% 25.52/7.70 % (1268150)Instructions burned: 110 (million)
% 25.52/7.70 % (1268151)Instruction limit reached!
% 25.52/7.70 % (1268151)------------------------------
% 25.52/7.70 % (1268151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/7.70 % (1268151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/7.70 % (1268151)CaDiCaL version: 2.1.3
% 25.52/7.70 % (1268151)Termination reason: Instruction limit
% 25.52/7.70 % (1268151)Termination phase: SInE selection
% 25.52/7.70 % (1268151)Time elapsed: 0.073 s
% 25.52/7.70 % (1268151)Peak memory usage: 205 MB
% 25.52/7.70 % (1268151)Instructions burned: 120 (million)
% 25.52/7.70 % (1268153)Instruction limit reached!
% 25.52/7.70 % (1268153)------------------------------
% 25.52/7.70 % (1268153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/7.70 % (1268153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/7.70 % (1268153)CaDiCaL version: 2.1.3
% 25.52/7.70 % (1268153)Termination reason: Instruction limit
% 25.52/7.70 % (1268153)Termination phase: SInE selection
% 25.52/7.70 % (1268153)Time elapsed: 0.079 s
% 25.52/7.70 % (1268153)Peak memory usage: 205 MB
% 25.52/7.70 % (1268153)Instructions burned: 129 (million)
% 25.52/7.70 % (1268152)Instruction limit reached!
% 25.52/7.70 % (1268152)------------------------------
% 25.52/7.70 % (1268152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/7.70 % (1268152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.52/7.70 % (1268152)CaDiCaL version: 2.1.3
% 25.52/7.70 % (1268152)Termination reason: Instruction limit
% 25.52/7.70 % (1268152)Termination phase: Property scanning
% 25.52/7.70 % (1268152)Time elapsed: 0.142 s
% 25.52/7.70 % (1268152)Peak memory usage: 206 MB
% 25.52/7.70 % (1268152)Instructions burned: 140 (million)
% 25.52/7.70 % (1268161)lrs+10_1_sil=8000:sp=occurrence:random_seed=2313547026:i=285:sd=3:ss=axioms:sgt=8_2963 on theBenchmark for (2963ds/285Mi)
% 25.52/7.70 % (1268162)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4205465240:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/157Mi)
% 25.52/7.70 % (1268163)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2593082150:i=325:sd=1:ss=axioms:sgt=32_2962 on theBenchmark for (2962ds/325Mi)
% 25.52/7.70 % (1268161)Instruction limit reached!
% 25.52/7.70 % (1268161)------------------------------
% 25.52/7.70 % (1268161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.52/7.70 % (1268161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.72/9.33 % (1268161)CaDiCaL version: 2.1.3
% 37.72/9.33 % (1268161)Termination reason: Instruction limit
% 37.72/9.33 % (1268161)Termination phase: SInE selection
% 37.72/9.33 % (1268161)Time elapsed: 0.144 s
% 37.72/9.33 % (1268161)Peak memory usage: 205 MB
% 37.72/9.33 % (1268161)Instructions burned: 285 (million)
% 37.72/9.33 % (1268164)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4279782866:s2a=on:i=248:s2at=1.23:gtg=position_2961 on theBenchmark for (2961ds/248Mi)
% 37.72/9.33 % (1268162)Instruction limit reached!
% 37.72/9.33 % (1268162)------------------------------
% 37.72/9.33 % (1268162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.72/9.33 % (1268162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.72/9.33 % (1268162)CaDiCaL version: 2.1.3
% 37.72/9.33 % (1268162)Termination reason: Instruction limit
% 37.72/9.33 % (1268162)Termination phase: Property scanning
% 37.72/9.33 % (1268162)Time elapsed: 0.159 s
% 37.72/9.33 % (1268162)Peak memory usage: 206 MB
% 37.72/9.33 % (1268162)Instructions burned: 157 (million)
% 37.72/9.33 % (1268163)Instruction limit reached!
% 37.72/9.33 % (1268163)------------------------------
% 37.72/9.33 % (1268163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.72/9.33 % (1268163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.72/9.33 % (1268163)CaDiCaL version: 2.1.3
% 37.72/9.33 % (1268163)Termination reason: Instruction limit
% 37.72/9.33 % (1268163)Termination phase: SInE selection
% 37.72/9.33 % (1268163)Time elapsed: 0.207 s
% 37.72/9.33 % (1268163)Peak memory usage: 205 MB
% 37.72/9.33 % (1268163)Instructions burned: 325 (million)
% 37.72/9.33 % (1268164)Instruction limit reached!
% 37.72/9.33 % (1268164)------------------------------
% 37.72/9.33 % (1268164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.72/9.33 % (1268164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.72/9.33 % (1268164)CaDiCaL version: 2.1.3
% 37.72/9.33 % (1268164)Termination reason: Instruction limit
% 37.72/9.33 % (1268164)Termination phase: Property scanning
% 37.72/9.33 % (1268164)Time elapsed: 0.214 s
% 37.72/9.33 % (1268164)Peak memory usage: 206 MB
% 37.72/9.33 % (1268164)Instructions burned: 248 (million)
% 37.72/9.33 % (1268170)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3337379839:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2959 on theBenchmark for (2959ds/294Mi)
% 37.72/9.33 % (1268172)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3723176830:i=2350_2957 on theBenchmark for (2957ds/2350Mi)
% 37.72/9.33 % (1268173)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2751934338:cts=off:i=113:fsr=off:ss=included:sgt=4_2957 on theBenchmark for (2957ds/113Mi)
% 37.72/9.33 % (1268170)Instruction limit reached!
% 37.72/9.33 % (1268170)------------------------------
% 37.72/9.33 % (1268170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.72/9.33 % (1268170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.72/9.33 % (1268170)CaDiCaL version: 2.1.3
% 37.72/9.33 % (1268170)Termination reason: Instruction limit
% 37.72/9.33 % (1268170)Termination phase: SInE selection
% 37.72/9.33 % (1268170)Time elapsed: 0.186 s
% 37.72/9.33 % (1268170)Peak memory usage: 205 MB
% 37.72/9.33 % (1268170)Instructions burned: 295 (million)
% 37.72/9.33 % (1268173)Instruction limit reached!
% 37.72/9.33 % (1268173)------------------------------
% 37.72/9.33 % (1268173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.72/9.33 % (1268173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.72/9.33 % (1268173)CaDiCaL version: 2.1.3
% 37.72/9.33 % (1268173)Termination reason: Instruction limit
% 37.72/9.33 % (1268173)Termination phase: SInE selection
% 37.72/9.33 % (1268173)Time elapsed: 0.070 s
% 37.72/9.33 % (1268173)Peak memory usage: 205 MB
% 37.72/9.33 % (1268173)Instructions burned: 113 (million)
% 37.72/9.33 % (1268176)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=449374721:i=127:av=off:fsr=off:sup=off_2956 on theBenchmark for (2956ds/127Mi)
% 37.72/9.33 % (1268179)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1385058674:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2954 on theBenchmark for (2954ds/114Mi)
% 37.72/9.33 % (1268176)Instruction limit reached!
% 37.72/9.33 % (1268176)------------------------------
% 37.72/9.33 % (1268176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.63/9.69 % (1268176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.63/9.69 % (1268176)CaDiCaL version: 2.1.3
% 39.63/9.69 % (1268176)Termination reason: Instruction limit
% 39.63/9.69 % (1268176)Termination phase: Preprocessing 1
% 39.63/9.69 % (1268176)Time elapsed: 0.158 s
% 39.63/9.69 % (1268176)Peak memory usage: 206 MB
% 39.63/9.69 % (1268176)Instructions burned: 127 (million)
% 39.63/9.69 % (1268181)lrs+10_1_sil=8000:sp=occurrence:random_seed=2372685805:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2953 on theBenchmark for (2953ds/907Mi)
% 39.63/9.69 % (1268179)Instruction limit reached!
% 39.63/9.69 % (1268179)------------------------------
% 39.63/9.69 % (1268179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.63/9.69 % (1268179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.63/9.69 % (1268179)CaDiCaL version: 2.1.3
% 39.63/9.69 % (1268179)Termination reason: Instruction limit
% 39.63/9.69 % (1268179)Termination phase: Property scanning
% 39.63/9.69 % (1268179)Time elapsed: 0.120 s
% 39.63/9.69 % (1268179)Peak memory usage: 206 MB
% 39.63/9.69 % (1268179)Instructions burned: 116 (million)
% 39.63/9.69 % (1268186)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3420736097:i=437:sd=1:aac=none:ss=included_2951 on theBenchmark for (2951ds/437Mi)
% 39.63/9.69 % (1268189)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1348985024:i=5202:ss=axioms:sgt=16_2950 on theBenchmark for (2950ds/5202Mi)
% 39.63/9.69 % (1268186)Instruction limit reached!
% 39.63/9.69 % (1268186)------------------------------
% 39.63/9.69 % (1268186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.63/9.69 % (1268186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.63/9.69 % (1268186)CaDiCaL version: 2.1.3
% 39.63/9.69 % (1268186)Termination reason: Instruction limit
% 39.63/9.69 % (1268186)Termination phase: SInE selection
% 39.63/9.69 % (1268186)Time elapsed: 0.308 s
% 39.63/9.69 % (1268186)Peak memory usage: 213 MB
% 39.63/9.69 % (1268186)Instructions burned: 439 (million)
% 39.63/9.69 % (1268181)Instruction limit reached!
% 39.63/9.69 % (1268181)------------------------------
% 39.63/9.69 % (1268181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.63/9.69 % (1268181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.63/9.69 % (1268181)CaDiCaL version: 2.1.3
% 39.63/9.69 % (1268181)Termination reason: Instruction limit
% 39.63/9.69 % (1268181)Termination phase: Preprocessing 3
% 39.63/9.69 % (1268181)Time elapsed: 0.695 s
% 39.63/9.69 % (1268181)Peak memory usage: 260 MB
% 39.63/9.69 % (1268181)Instructions burned: 907 (million)
% 39.63/9.69 % (1268193)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4021984061:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2945 on theBenchmark for (2945ds/134Mi)
% 39.63/9.69 % (1268195)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3844956663:st=8:i=592:sd=3:ep=RST:ss=axioms_2943 on theBenchmark for (2943ds/592Mi)
% 39.63/9.69 % (1268193)Instruction limit reached!
% 39.63/9.69 % (1268193)------------------------------
% 39.63/9.69 % (1268193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.63/9.69 % (1268193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.63/9.69 % (1268193)CaDiCaL version: 2.1.3
% 39.63/9.69 % (1268193)Termination reason: Instruction limit
% 39.63/9.69 % (1268193)Termination phase: SInE selection
% 39.63/9.69 % (1268193)Time elapsed: 0.088 s
% 39.63/9.69 % (1268193)Peak memory usage: 205 MB
% 39.63/9.69 % (1268193)Instructions burned: 134 (million)
% 39.63/9.69 % (1268200)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3504714893:st=3:i=13193:sd=3:ss=axioms_2940 on theBenchmark for (2940ds/13193Mi)
% 39.63/9.69 % (1268195)Instruction limit reached!
% 39.63/9.69 % (1268195)------------------------------
% 39.63/9.69 % (1268195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.63/9.69 % (1268195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.63/9.69 % (1268195)CaDiCaL version: 2.1.3
% 39.63/9.69 % (1268195)Termination reason: Instruction limit
% 39.63/9.69 % (1268195)Termination phase: SInE selection
% 39.63/9.69 % (1268195)Time elapsed: 0.358 s
% 39.63/9.69 % (1268195)Peak memory usage: 207 MB
% 39.63/9.69 % (1268195)Instructions burned: 592 (million)
% 39.63/9.69 % (1268203)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2425653077:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2937 on theBenchmark for (2937ds/125Mi)
% 74.56/14.53 % (1268203)Instruction limit reached!
% 74.56/14.53 % (1268203)------------------------------
% 74.56/14.53 % (1268203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.56/14.53 % (1268203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.56/14.53 % (1268203)CaDiCaL version: 2.1.3
% 74.56/14.53 % (1268203)Termination reason: Instruction limit
% 74.56/14.53 % (1268203)Termination phase: Property scanning
% 74.56/14.53 % (1268203)Time elapsed: 0.143 s
% 74.56/14.53 % (1268203)Peak memory usage: 206 MB
% 74.56/14.53 % (1268203)Instructions burned: 126 (million)
% 74.56/14.53 % (1268172)Instruction limit reached!
% 74.56/14.53 % (1268172)------------------------------
% 74.56/14.53 % (1268172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.56/14.53 % (1268172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.56/14.53 % (1268172)CaDiCaL version: 2.1.3
% 74.56/14.53 % (1268172)Termination reason: Instruction limit
% 74.56/14.53 % (1268172)Termination phase: Preprocessing 3
% 74.56/14.53 % (1268172)Time elapsed: 2.343 s
% 74.56/14.53 % (1268172)Peak memory usage: 277 MB
% 74.56/14.53 % (1268172)Instructions burned: 2350 (million)
% 74.56/14.53 % (1268206)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=325635136:i=134:gtgl=5:slsql=off:gtg=exists_sym_2933 on theBenchmark for (2933ds/134Mi)
% 74.56/14.53 % (1268206)Instruction limit reached!
% 74.56/14.53 % (1268206)------------------------------
% 74.56/14.53 % (1268206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.56/14.53 % (1268206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.56/14.53 % (1268206)CaDiCaL version: 2.1.3
% 74.56/14.53 % (1268206)Termination reason: Instruction limit
% 74.56/14.53 % (1268206)Termination phase: Property scanning
% 74.56/14.53 % (1268206)Time elapsed: 0.138 s
% 74.56/14.53 % (1268206)Peak memory usage: 206 MB
% 74.56/14.53 % (1268206)Instructions burned: 135 (million)
% 74.56/14.53 % (1268208)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1414153769:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2931 on theBenchmark for (2931ds/141Mi)
% 74.56/14.53 % (1268208)Instruction limit reached!
% 74.56/14.53 % (1268208)------------------------------
% 74.56/14.53 % (1268208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.56/14.53 % (1268208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.56/14.53 % (1268208)CaDiCaL version: 2.1.3
% 74.56/14.53 % (1268208)Termination reason: Instruction limit
% 74.56/14.53 % (1268208)Termination phase: SInE selection
% 74.56/14.53 % (1268208)Time elapsed: 0.093 s
% 74.56/14.53 % (1268208)Peak memory usage: 205 MB
% 74.56/14.53 % (1268208)Instructions burned: 141 (million)
% 74.56/14.53 % (1268210)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2899382050:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2928 on theBenchmark for (2928ds/431Mi)
% 74.56/14.53 % (1268212)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2153048484:i=6060:aac=none:ins=25_2927 on theBenchmark for (2927ds/6060Mi)
% 74.56/14.53 % (1268210)Instruction limit reached!
% 74.56/14.53 % (1268210)------------------------------
% 74.56/14.53 % (1268210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.56/14.53 % (1268210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.56/14.53 % (1268210)CaDiCaL version: 2.1.3
% 74.56/14.53 % (1268210)Termination reason: Instruction limit
% 74.56/14.53 % (1268210)Termination phase: SInE selection
% 74.56/14.53 % (1268210)Time elapsed: 0.284 s
% 74.56/14.53 % (1268210)Peak memory usage: 206 MB
% 74.56/14.53 % (1268210)Instructions burned: 431 (million)
% 74.56/14.53 % (1268217)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2214487064:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2922 on theBenchmark for (2922ds/150Mi)
% 74.56/14.53 % (1268217)Instruction limit reached!
% 74.56/14.53 % (1268217)------------------------------
% 74.56/14.53 % (1268217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.56/14.53 % (1268217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.56/14.53 % (1268217)CaDiCaL version: 2.1.3
% 74.56/14.53 % (1268217)Termination reason: Instruction limit
% 139.98/23.71 % (1268217)Termination phase: SInE selection
% 139.98/23.71 % (1268217)Time elapsed: 0.099 s
% 139.98/23.71 % (1268217)Peak memory usage: 205 MB
% 139.98/23.71 % (1268217)Instructions burned: 151 (million)
% 139.98/23.71 [W927 11:41:05.425469593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425512510 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425562273 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425575507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425601100 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425613057 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425639710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425651897 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425677277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425689147 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425715453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 [W927 11:41:05.425727377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.98/23.71 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.98/23.71 % (1268221)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3130082810:i=14155:bd=all_2918 on theBenchmark for (2918ds/14155Mi)
% 181.92/29.65 % (1268189)Instruction limit reached!
% 181.92/29.65 % (1268189)------------------------------
% 181.92/29.65 % (1268189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.92/29.65 % (1268189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.92/29.65 % (1268189)CaDiCaL version: 2.1.3
% 181.92/29.65 % (1268189)Termination reason: Instruction limit
% 181.92/29.65 % (1268189)Termination phase: Saturation
% 181.92/29.65 % (1268189)Time elapsed: 4.652 s
% 181.92/29.65 % (1268189)Peak memory usage: 333 MB
% 181.92/29.65 % (1268189)Instructions burned: 5203 (million)
% 181.92/29.65 % (1268227)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=992173219:i=667:av=off:fsr=off_2900 on theBenchmark for (2900ds/667Mi)
% 181.92/29.65 % (1268200)Refutation not found, incomplete strategy
% 181.92/29.65 % (1268200)------------------------------
% 181.92/29.65 % (1268200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.92/29.65 % (1268200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.92/29.65 % (1268200)CaDiCaL version: 2.1.3
% 181.92/29.65 % (1268200)Termination reason: Refutation not found, incomplete strategy
% 181.92/29.65 % (1268200)Time elapsed: 4.402 s
% 181.92/29.65 % (1268200)Peak memory usage: 576 MB
% 181.92/29.65 % (1268200)Instructions burned: 4976 (million)
% 181.92/29.65 % (1268200)------------------------------
% 181.92/29.65 % (1268200)------------------------------
% 181.92/29.65 % (1268227)Instruction limit reached!
% 181.92/29.65 % (1268227)------------------------------
% 181.92/29.65 % (1268227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.92/29.65 % (1268227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.92/29.65 % (1268227)CaDiCaL version: 2.1.3
% 181.92/29.65 % (1268227)Termination reason: Instruction limit
% 181.92/29.65 % (1268227)Termination phase: Preprocessing 2
% 181.92/29.65 % (1268227)Time elapsed: 0.877 s
% 181.92/29.65 % (1268227)Peak memory usage: 257 MB
% 181.92/29.65 % (1268227)Instructions burned: 667 (million)
% 181.92/29.65 % (1268231)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2870392751:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2888 on theBenchmark for (2888ds/193Mi)
% 181.92/29.65 % (1268230)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=484931993:s2a=on:i=185:s2at=1.8:fdi=4_2888 on theBenchmark for (2888ds/185Mi)
% 181.92/29.65 % (1268230)Instruction limit reached!
% 181.92/29.65 % (1268230)------------------------------
% 181.92/29.65 % (1268230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.92/29.65 % (1268230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.92/29.65 % (1268230)CaDiCaL version: 2.1.3
% 181.92/29.65 % (1268230)Termination reason: Instruction limit
% 181.92/29.65 % (1268230)Termination phase: SInE selection
% 181.92/29.65 % (1268230)Time elapsed: 0.094 s
% 181.92/29.65 % (1268230)Peak memory usage: 205 MB
% 181.92/29.65 % (1268230)Instructions burned: 185 (million)
% 181.92/29.65 % (1268231)Instruction limit reached!
% 181.92/29.65 % (1268231)------------------------------
% 181.92/29.65 % (1268231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.92/29.65 % (1268231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.92/29.65 % (1268231)CaDiCaL version: 2.1.3
% 181.92/29.65 % (1268231)Termination reason: Instruction limit
% 181.92/29.65 % (1268231)Termination phase: SInE selection
% 181.92/29.65 % (1268231)Time elapsed: 0.118 s
% 181.92/29.65 % (1268231)Peak memory usage: 205 MB
% 181.92/29.65 % (1268231)Instructions burned: 193 (million)
% 181.92/29.65 % (1268236)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2801385549:i=12111:sd=1:ss=included_2884 on theBenchmark for (2884ds/12111Mi)
% 181.92/29.65 % (1268235)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=782529514:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2884 on theBenchmark for (2884ds/4850Mi)
% 181.92/29.65 % (1268212)Instruction limit reached!
% 181.92/29.65 % (1268212)------------------------------
% 181.92/29.65 % (1268212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.92/29.65 % (1268212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.92/29.65 % (1268212)CaDiCaL version: 2.1.3
% 181.92/29.65 % (1268212)Termination reason: Instruction limit
% 181.92/29.65 % (1268212)Termination phase: Property scanning
% 201.09/32.31 % (1268212)Time elapsed: 5.747 s
% 201.09/32.31 % (1268212)Peak memory usage: 357 MB
% 201.09/32.31 % (1268212)Instructions burned: 6061 (million)
% 201.09/32.31 % (1268245)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2652340850:i=319:kws=precedence:fsr=off_2865 on theBenchmark for (2865ds/319Mi)
% 201.09/32.31 % (1268245)Instruction limit reached!
% 201.09/32.31 % (1268245)------------------------------
% 201.09/32.31 % (1268245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.09/32.31 % (1268245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.09/32.31 % (1268245)CaDiCaL version: 2.1.3
% 201.09/32.31 % (1268245)Termination reason: Instruction limit
% 201.09/32.31 % (1268245)Termination phase: Preprocessing 1
% 201.09/32.31 % (1268245)Time elapsed: 0.407 s
% 201.09/32.31 % (1268245)Peak memory usage: 206 MB
% 201.09/32.31 % (1268245)Instructions burned: 320 (million)
% 201.09/32.31 % (1268249)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3259200707:i=2064:ep=RST_2858 on theBenchmark for (2858ds/2064Mi)
% 201.09/32.31 % (1268235)Instruction limit reached!
% 201.09/32.31 % (1268235)------------------------------
% 201.09/32.31 % (1268235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.09/32.31 % (1268235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.09/32.31 % (1268235)CaDiCaL version: 2.1.3
% 201.09/32.31 % (1268235)Termination reason: Instruction limit
% 201.09/32.31 % (1268235)Termination phase: Property scanning
% 201.09/32.31 % (1268235)Time elapsed: 4.519 s
% 201.09/32.31 % (1268235)Peak memory usage: 392 MB
% 201.09/32.31 % (1268235)Instructions burned: 4851 (million)
% 201.09/32.31 % (1268260)dis-1011_128_sil=32000:random_seed=1599348890:i=3706:ep=RST:av=off_2836 on theBenchmark for (2836ds/3706Mi)
% 201.09/32.31 % (1268249)Instruction limit reached!
% 201.09/32.31 % (1268249)------------------------------
% 201.09/32.31 % (1268249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.09/32.31 % (1268249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.09/32.31 % (1268249)CaDiCaL version: 2.1.3
% 201.09/32.31 % (1268249)Termination reason: Instruction limit
% 201.09/32.31 % (1268249)Termination phase: Preprocessing 3
% 201.09/32.31 % (1268249)Time elapsed: 2.231 s
% 201.09/32.31 % (1268249)Peak memory usage: 317 MB
% 201.09/32.31 % (1268249)Instructions burned: 2064 (million)
% 201.09/32.31 % (1268263)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3611549992:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2832 on theBenchmark for (2832ds/757Mi)
% 201.09/32.31 % (1268263)Instruction limit reached!
% 201.09/32.31 % (1268263)------------------------------
% 201.09/32.31 % (1268263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.09/32.31 % (1268263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.09/32.31 % (1268263)CaDiCaL version: 2.1.3
% 201.09/32.31 % (1268263)Termination reason: Instruction limit
% 201.09/32.31 % (1268263)Termination phase: Unused predicate definition removal
% 201.09/32.31 % (1268263)Time elapsed: 0.537 s
% 201.09/32.31 % (1268263)Peak memory usage: 225 MB
% 201.09/32.31 % (1268263)Instructions burned: 757 (million)
% 201.09/32.31 % (1268266)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3211935287:i=13913:ss=axioms:sgt=8_2823 on theBenchmark for (2823ds/13913Mi)
% 201.09/32.31 % (1268260)Instruction limit reached!
% 201.09/32.31 % (1268260)------------------------------
% 201.09/32.31 % (1268260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.09/32.31 % (1268260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.09/32.31 % (1268260)CaDiCaL version: 2.1.3
% 201.09/32.31 % (1268260)Termination reason: Instruction limit
% 201.09/32.31 % (1268260)Termination phase: Property scanning
% 201.09/32.31 % (1268260)Time elapsed: 3.745 s
% 201.09/32.31 % (1268260)Peak memory usage: 392 MB
% 201.09/32.31 % (1268260)Instructions burned: 3707 (million)
% 201.09/32.31 % (1268279)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1932908723:i=9925:aac=none_2794 on theBenchmark for (2794ds/9925Mi)
% 201.09/32.31 % (1268266)Refutation not found, incomplete strategy
% 201.09/32.31 % (1268266)------------------------------
% 201.09/32.31 % (1268266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 201.09/32.31 % (1268266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.09/32.31 % (1268266)CaDiCaL version: 2.1.3
% 201.09/32.31 % (1268266)Termination reason: Refutation not found, incomplete strategy
% 238.84/37.61 % (1268266)Time elapsed: 4.540 s
% 238.84/37.61 % (1268266)Peak memory usage: 531 MB
% 238.84/37.61 % (1268266)Instructions burned: 4531 (million)
% 238.84/37.61 % (1268266)------------------------------
% 238.84/37.61 % (1268266)------------------------------
% 238.84/37.61 % (1268288)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=145139280:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2768 on theBenchmark for (2768ds/2479Mi)
% 238.84/37.61 % (1268288)Refutation not found, incomplete strategy
% 238.84/37.61 % (1268288)------------------------------
% 238.84/37.61 % (1268288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.84/37.61 % (1268288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.84/37.61 % (1268288)CaDiCaL version: 2.1.3
% 238.84/37.61 % (1268288)Termination reason: Refutation not found, incomplete strategy
% 238.84/37.61 % (1268288)Time elapsed: 1.292 s
% 238.84/37.61 % (1268288)Peak memory usage: 259 MB
% 238.84/37.61 % (1268288)Instructions burned: 1750 (million)
% 238.84/37.61 % (1268288)------------------------------
% 238.84/37.61 % (1268288)------------------------------
% 238.84/37.61 % (1268297)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3957347646:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2747 on theBenchmark for (2747ds/440Mi)
% 238.84/37.61 % (1268297)Instruction limit reached!
% 238.84/37.61 % (1268297)------------------------------
% 238.84/37.61 % (1268297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.84/37.61 % (1268297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.84/37.61 % (1268297)CaDiCaL version: 2.1.3
% 238.84/37.61 % (1268297)Termination reason: Instruction limit
% 238.84/37.61 % (1268297)Termination phase: Property scanning
% 238.84/37.61 % (1268297)Time elapsed: 0.339 s
% 238.84/37.61 % (1268297)Peak memory usage: 206 MB
% 238.84/37.61 % (1268297)Instructions burned: 440 (million)
% 238.84/37.61 % (1268299)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=924114311:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2741 on theBenchmark for (2741ds/11145Mi)
% 238.84/37.61 % (1268236)Instruction limit reached!
% 238.84/37.61 % (1268236)------------------------------
% 238.84/37.61 % (1268236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.84/37.61 % (1268236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.84/37.61 % (1268236)CaDiCaL version: 2.1.3
% 238.84/37.61 % (1268236)Termination reason: Instruction limit
% 238.84/37.61 % (1268236)Termination phase: Saturation
% 238.84/37.61 % (1268236)Time elapsed: 15.718 s
% 238.84/37.61 % (1268236)Peak memory usage: 1293 MB
% 238.84/37.61 % (1268236)Instructions burned: 12113 (million)
% 238.84/37.61 % (1268305)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=4216791204:cts=off:i=3034:av=off:er=known:fsd=on_2722 on theBenchmark for (2722ds/3034Mi)
% 238.84/37.61 [W927 11:41:25.669308454 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 238.84/37.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 238.84/37.61 [W927 11:41:25.669359371 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 238.84/37.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 238.84/37.61 [W927 11:41:25.669433635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 238.84/37.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 238.84/37.61 [W927 11:41:25.669452671 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 238.84/37.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 238.84/37.61 [W927 11:41:25.669494661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669512628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669557715 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669574745 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669618275 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669634628 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669675528 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 [W927 11:41:25.669692055 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 255.85/40.03 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 255.85/40.03 % (1268221)Instruction limit reached!
% 255.85/40.03 % (1268221)------------------------------
% 255.85/40.03 % (1268221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 255.85/40.03 % (1268221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.85/40.03 % (1268221)CaDiCaL version: 2.1.3
% 255.85/40.03 % (1268221)Termination reason: Instruction limit
% 255.85/40.03 % (1268221)Termination phase: Saturation
% 255.85/40.03 % (1268221)Time elapsed: 21.755 s
% 255.85/40.03 % (1268221)Peak memory usage: 1273 MB
% 255.85/40.03 % (1268221)Instructions burned: 14156 (million)
% 255.85/40.03 % (1268309)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=859805258:st=2:s2a=on:i=524:s2at=2:ss=axioms_2694 on theBenchmark for (2694ds/524Mi)
% 255.85/40.03 % (1268305)Instruction limit reached!
% 255.85/40.03 % (1268305)------------------------------
% 255.85/40.03 % (1268305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 255.85/40.03 % (1268305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.85/40.03 % (1268305)CaDiCaL version: 2.1.3
% 255.85/40.03 % (1268305)Termination reason: Instruction limit
% 255.85/40.03 % (1268305)Termination phase: Preprocessing 3
% 255.85/40.03 % (1268305)Time elapsed: 2.903 s
% 255.85/40.03 % (1268305)Peak memory usage: 337 MB
% 255.85/40.03 % (1268305)Instructions burned: 3034 (million)
% 255.85/40.03 % (1268299)Refutation not found, incomplete strategy
% 255.85/40.03 % (1268299)------------------------------
% 255.85/40.03 % (1268299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 255.85/40.03 % (1268299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.85/40.03 % (1268299)CaDiCaL version: 2.1.3
% 255.85/40.03 % (1268299)Termination reason: Refutation not found, incomplete strategy
% 255.85/40.03 % (1268299)Time elapsed: 4.909 s
% 255.85/40.03 % (1268299)Peak memory usage: 578 MB
% 255.85/40.03 % (1268299)Instructions burned: 5344 (million)
% 255.85/40.03 % (1268309)Instruction limit reached!
% 182.10/40.34 % (1268309)------------------------------
% 182.10/40.34 % (1268309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268309)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268309)Termination reason: Instruction limit
% 182.10/40.34 % (1268309)Termination phase: SInE selection
% 182.10/40.34 % (1268309)Time elapsed: 0.327 s
% 182.10/40.34 % (1268309)Peak memory usage: 206 MB
% 182.10/40.34 % (1268309)Instructions burned: 524 (million)
% 182.10/40.34 % (1268312)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1246789573:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2689 on theBenchmark for (2689ds/1016Mi)
% 182.10/40.34 % (1268313)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3054970853:i=14123:bd=preordered:ins=4_2688 on theBenchmark for (2688ds/14123Mi)
% 182.10/40.34 % (1268299)------------------------------
% 182.10/40.34 % (1268299)------------------------------
% 182.10/40.34 % (1268319)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=4139570697:i=5781:kws=precedence:bd=all:rawr=on_2684 on theBenchmark for (2684ds/5781Mi)
% 182.10/40.34 % (1268312)Refutation not found, incomplete strategy
% 182.10/40.34 % (1268312)------------------------------
% 182.10/40.34 % (1268312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268312)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268312)Termination reason: Refutation not found, incomplete strategy
% 182.10/40.34 % (1268312)Time elapsed: 0.715 s
% 182.10/40.34 % (1268312)Peak memory usage: 258 MB
% 182.10/40.34 % (1268312)Instructions burned: 970 (million)
% 182.10/40.34 % (1268279)Instruction limit reached!
% 182.10/40.34 % (1268279)------------------------------
% 182.10/40.34 % (1268279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268279)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268279)Termination reason: Instruction limit
% 182.10/40.34 % (1268279)Termination phase: Saturation
% 182.10/40.34 % (1268279)Time elapsed: 11.786 s
% 182.10/40.34 % (1268279)Peak memory usage: 1114 MB
% 182.10/40.34 % (1268279)Instructions burned: 9925 (million)
% 182.10/40.34 % (1268312)------------------------------
% 182.10/40.34 % (1268312)------------------------------
% 182.10/40.34 % (1268323)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=1711973466:i=2448:gtgl=5:bd=preordered:gtg=all_2672 on theBenchmark for (2672ds/2448Mi)
% 182.10/40.34 % (1268324)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3893101031:i=3223:kws=precedence:fgj=on:av=off_2672 on theBenchmark for (2672ds/3223Mi)
% 182.10/40.34 % (1268323)Instruction limit reached!
% 182.10/40.34 % (1268323)------------------------------
% 182.10/40.34 % (1268323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268323)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268323)Termination reason: Instruction limit
% 182.10/40.34 % (1268323)Termination phase: SInE selection
% 182.10/40.34 % (1268323)Time elapsed: 1.676 s
% 182.10/40.34 % (1268323)Peak memory usage: 208 MB
% 182.10/40.34 % (1268323)Instructions burned: 2449 (million)
% 182.10/40.34 % (1268333)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2025166455:st=5.6:i=2033:sd=3:ss=axioms_2653 on theBenchmark for (2653ds/2033Mi)
% 182.10/40.34 % (1268333)Instruction limit reached!
% 182.10/40.34 % (1268333)------------------------------
% 182.10/40.34 % (1268333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268333)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268333)Termination reason: Instruction limit
% 182.10/40.34 % (1268333)Termination phase: Saturation
% 182.10/40.34 % (1268333)Time elapsed: 1.471 s
% 182.10/40.34 % (1268333)Peak memory usage: 263 MB
% 182.10/40.34 % (1268333)Instructions burned: 2033 (million)
% 182.10/40.34 % (1268324)Instruction limit reached!
% 182.10/40.34 % (1268324)------------------------------
% 182.10/40.34 % (1268324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268324)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268324)Termination reason: Instruction limit
% 182.10/40.34 % (1268324)Termination phase: Clausification
% 182.10/40.34 % (1268324)Time elapsed: 3.359 s
% 182.10/40.34 % (1268324)Peak memory usage: 357 MB
% 182.10/40.34 % (1268324)Instructions burned: 3223 (million)
% 182.10/40.34 % (1268335)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1431313247:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2636 on theBenchmark for (2636ds/2055Mi)
% 182.10/40.34 % (1268336)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=1018539425:i=21611:sd=3:ss=axioms_2634 on theBenchmark for (2634ds/21611Mi)
% 182.10/40.34 % (1268319)Instruction limit reached!
% 182.10/40.34 % (1268319)------------------------------
% 182.10/40.34 % (1268319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268319)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268319)Termination reason: Instruction limit
% 182.10/40.34 % (1268319)Termination phase: Property scanning
% 182.10/40.34 % (1268319)Time elapsed: 5.212 s
% 182.10/40.34 % (1268319)Peak memory usage: 393 MB
% 182.10/40.34 % (1268319)Instructions burned: 5782 (million)
% 182.10/40.34 % (1268339)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=1917747242:i=4835:sd=13:ss=axioms:sgt=23_2627 on theBenchmark for (2627ds/4835Mi)
% 182.10/40.34 % (1268335)Instruction limit reached!
% 182.10/40.34 % (1268335)------------------------------
% 182.10/40.34 % (1268335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268335)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268335)Termination reason: Instruction limit
% 182.10/40.34 % (1268335)Termination phase: SInE selection
% 182.10/40.34 % (1268335)Time elapsed: 1.350 s
% 182.10/40.34 % (1268335)Peak memory usage: 210 MB
% 182.10/40.34 % (1268335)Instructions burned: 2057 (million)
% 182.10/40.34 % (1268343)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1579924574:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2619 on theBenchmark for (2619ds/797Mi)
% 182.10/40.34 % (1268339)First to succeed.
% 182.10/40.34 % (1268339)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1268109"
% 182.10/40.34 % (1268343)Instruction limit reached!
% 182.10/40.34 % (1268343)------------------------------
% 182.10/40.34 % (1268343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.10/40.34 % (1268343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.10/40.34 % (1268343)CaDiCaL version: 2.1.3
% 182.10/40.34 % (1268343)Termination reason: Instruction limit
% 182.10/40.34 % (1268343)Termination phase: SInE selection
% 182.10/40.34 % (1268343)Time elapsed: 0.424 s
% 182.10/40.34 % (1268343)Peak memory usage: 208 MB
% 182.10/40.34 % (1268343)Instructions burned: 800 (million)
% 182.10/40.34 [W927 11:41:35.043692668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043745345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043819015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043839048 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043885825 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043933285 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043976271 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.043993135 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.044046838 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.044064812 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.044107728 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 [W927 11:41:35.044125475 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 182.10/40.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 182.10/40.34 % (1268339)Refutation found. Thanks to Tanya!
% 182.10/40.34 % SZS status Theorem for theBenchmark
% 182.10/40.34 % SZS output start Proof for theBenchmark
% See solution above
% 257.71/40.67 % (1268339)------------------------------
% 257.71/40.67 % (1268339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 257.71/40.67 % (1268339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 257.71/40.67 % (1268339)CaDiCaL version: 2.1.3
% 257.71/40.67 % (1268339)Termination reason: Refutation
% 257.71/40.67 % (1268339)Time elapsed: 0.956 s
% 257.71/40.67 % (1268339)Peak memory usage: 260 MB
% 257.71/40.67 % (1268339)Instructions burned: 1170 (million)
% 257.71/40.67 % (1268339)------------------------------
% 257.71/40.67 % (1268339)------------------------------
% 257.71/40.67 % (1268109)Success in time 39.163 s
% 257.71/40.67 % Vampire exiting
%------------------------------------------------------------------------------