%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV124+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 : n009.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:48:41 AM UTC 2026
% Result : Theorem 163.53s 37.30s
% Output : Refutation 0.32s
% 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(f95,conjecture,
! [X0] :
( reachableState(X0)
=> v4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssertion) ).
fof(f96,negated_conjecture,
~ ! [X0] :
( reachableState(X0)
=> v4(X0) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f97,axiom,
! [X0] :
( ~ v4(X0)
<=> v154847(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11893) ).
fof(f98,axiom,
! [X0] :
( ~ v154847(X0)
<=> v154848(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11892) ).
fof(f99,axiom,
! [X0] :
( v154848(X0)
<=> ( v154850(X0)
& v154868(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20766) ).
fof(f100,axiom,
! [X0] :
( v154868(X0)
<=> ( v154869(X0)
| v154853(X0,bitIndex3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7474) ).
fof(f101,axiom,
! [X0] :
( v154869(X0)
<=> ( v154870(X0)
| v154853(X0,bitIndex2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7473) ).
fof(f102,axiom,
! [X0] :
( v154870(X0)
<=> ( v154853(X0,bitIndex0)
| v154853(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7472) ).
fof(f103,axiom,
! [X0] :
( v154850(X0)
<=> ( v154851(X0)
| v154859(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20765) ).
fof(f104,axiom,
! [X0] :
( v154859(X0)
<=> ( v154860(X0)
| v154861(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20764) ).
fof(f105,axiom,
! [X0] :
( v154861(X0)
<=> ( v154852(X0)
& v154862(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20763) ).
fof(f106,axiom,
! [X0] :
( v154862(X0)
<=> ( v154863(X0)
| v154864(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20762) ).
fof(f107,axiom,
! [X0] :
( v154864(X0)
<=> ( v154855(X0)
& v154865(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20761) ).
fof(f108,axiom,
! [X0] :
( v154865(X0)
<=> ( v154866(X0)
| v154867(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20760) ).
fof(f109,axiom,
! [X0] :
( v154867(X0)
<=> ( v154853(X0,bitIndex0)
& v154858(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20759) ).
fof(f110,axiom,
! [X0] :
( v154866(X0)
<=> ( v154857(X0)
& v154853(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7471) ).
fof(f111,axiom,
! [X0] :
( v154863(X0)
<=> ( v154853(X0,bitIndex2)
& v154856(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7470) ).
fof(f112,axiom,
! [X0] :
( v154860(X0)
<=> ( v154853(X0,bitIndex3)
& v154854(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7469) ).
fof(f113,axiom,
! [X0] :
( v154851(X0)
<=> ( v154852(X0)
& v154854(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20758) ).
fof(f114,axiom,
! [X0] :
( v154854(X0)
<=> ( v154855(X0)
& v154856(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20757) ).
fof(f115,axiom,
! [X0] :
( v154856(X0)
<=> ( v154857(X0)
& v154858(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20756) ).
fof(f116,axiom,
! [X0] :
( ~ v154858(X0)
<=> v154853(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11891) ).
fof(f117,axiom,
! [X0] :
( ~ v154857(X0)
<=> v154853(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11890) ).
fof(f118,axiom,
! [X0] :
( ~ v154855(X0)
<=> v154853(X0,bitIndex2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11889) ).
fof(f119,axiom,
! [X0] :
( ~ v154852(X0)
<=> v154853(X0,bitIndex3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11888) ).
fof(f120,axiom,
! [X0,X1] :
( range_3_0(X1)
=> ( v154853(X0,X1)
<=> v6(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86259) ).
fof(f121,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(f122,axiom,
! [X0] :
( v154836(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> b0001(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1782) ).
fof(f123,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(f124,axiom,
! [X0] :
( v154839(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v154838(X0,X1)
<=> b0010(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1781) ).
fof(f125,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(f126,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(f127,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v154844(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86258) ).
fof(f128,axiom,
! [X0] :
( v154844(X0,bitIndex2)
<=> v154845(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86257) ).
fof(f129,axiom,
! [X0] :
( v154844(X0,bitIndex3)
<=> v83122(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86256) ).
fof(f130,axiom,
! [X0] :
( ~ v154845(X0)
<=> v83122(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11887) ).
fof(f131,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v154842(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86255) ).
fof(f132,axiom,
! [X0] :
( v154842(X0,bitIndex2)
<=> v154843(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86254) ).
fof(f133,axiom,
! [X0] :
( v154842(X0,bitIndex3)
<=> v83122(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86253) ).
fof(f134,axiom,
! [X0] :
( ~ v154843(X0)
<=> v83122(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11886) ).
fof(f138093,axiom,
~ b0010(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_280) ).
fof(f138094,axiom,
~ b0010(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_279) ).
fof(f138095,axiom,
b0010(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_278) ).
fof(f138096,axiom,
~ b0010(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_277) ).
fof(f138120,axiom,
~ b0001(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_276) ).
fof(f138121,axiom,
~ b0001(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_275) ).
fof(f138122,axiom,
~ b0001(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_274) ).
fof(f138123,axiom,
b0001(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_273) ).
fof(f141450,axiom,
! [X0] :
( range_1_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_axiom_4) ).
fof(f142309,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(f142395,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154842(X0,X1) ),
inference(true_and_false_elimination,[],[f131]) ).
fof(f142396,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154842(X0,X1) ),
inference(flattening,[],[f142395]) ).
fof(f142397,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154844(X0,X1) ),
inference(true_and_false_elimination,[],[f127]) ).
fof(f142398,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154844(X0,X1) ),
inference(flattening,[],[f142397]) ).
fof(f142491,plain,
! [X0] :
( range_3_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
inference(true_and_false_elimination,[],[f142309]) ).
fof(f142495,plain,
! [X0] :
( range_1_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0 ) ),
inference(true_and_false_elimination,[],[f141450]) ).
fof(f142722,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0 )
=> range_1_0(X0) ),
inference(unused_predicate_definition_removal,[],[f142495]) ).
fof(f142723,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 )
=> range_3_0(X0) ),
inference(unused_predicate_definition_removal,[],[f142491]) ).
fof(f142724,plain,
! [X0] :
( ~ v4(X0)
=> v154847(X0) ),
inference(unused_predicate_definition_removal,[],[f97]) ).
fof(f142725,plain,
! [X0] :
( v154848(X0)
=> ~ v154847(X0) ),
inference(unused_predicate_definition_removal,[],[f98]) ).
fof(f142726,plain,
! [X0] :
( ( v154850(X0)
& v154868(X0) )
=> v154848(X0) ),
inference(unused_predicate_definition_removal,[],[f99]) ).
fof(f142727,plain,
! [X0] :
( ( v154851(X0)
| v154859(X0) )
=> v154850(X0) ),
inference(unused_predicate_definition_removal,[],[f103]) ).
fof(f142728,plain,
! [X0] :
( ( v154852(X0)
& v154854(X0) )
=> v154851(X0) ),
inference(unused_predicate_definition_removal,[],[f113]) ).
fof(f142729,plain,
! [X0] :
( ( v154860(X0)
| v154861(X0) )
=> v154859(X0) ),
inference(unused_predicate_definition_removal,[],[f104]) ).
fof(f142730,plain,
! [X0] :
( ( v154853(X0,bitIndex3)
& v154854(X0) )
=> v154860(X0) ),
inference(unused_predicate_definition_removal,[],[f112]) ).
fof(f142731,plain,
! [X0] :
( ( v154855(X0)
& v154856(X0) )
=> v154854(X0) ),
inference(unused_predicate_definition_removal,[],[f114]) ).
fof(f142732,plain,
! [X0] :
( ( v154852(X0)
& v154862(X0) )
=> v154861(X0) ),
inference(unused_predicate_definition_removal,[],[f105]) ).
fof(f142733,plain,
! [X0] :
( ~ v154852(X0)
=> v154853(X0,bitIndex3) ),
inference(unused_predicate_definition_removal,[],[f119]) ).
fof(f142734,plain,
! [X0] :
( ( v154863(X0)
| v154864(X0) )
=> v154862(X0) ),
inference(unused_predicate_definition_removal,[],[f106]) ).
fof(f142735,plain,
! [X0] :
( ( v154853(X0,bitIndex2)
& v154856(X0) )
=> v154863(X0) ),
inference(unused_predicate_definition_removal,[],[f111]) ).
fof(f142736,plain,
! [X0] :
( ( v154857(X0)
& v154858(X0) )
=> v154856(X0) ),
inference(unused_predicate_definition_removal,[],[f115]) ).
fof(f142737,plain,
! [X0] :
( ( v154855(X0)
& v154865(X0) )
=> v154864(X0) ),
inference(unused_predicate_definition_removal,[],[f107]) ).
fof(f142738,plain,
! [X0] :
( ~ v154855(X0)
=> v154853(X0,bitIndex2) ),
inference(unused_predicate_definition_removal,[],[f118]) ).
fof(f142739,plain,
! [X0] :
( ( v154866(X0)
| v154867(X0) )
=> v154865(X0) ),
inference(unused_predicate_definition_removal,[],[f108]) ).
fof(f142740,plain,
! [X0] :
( ( v154857(X0)
& v154853(X0,bitIndex1) )
=> v154866(X0) ),
inference(unused_predicate_definition_removal,[],[f110]) ).
fof(f142741,plain,
! [X0] :
( ~ v154857(X0)
=> v154853(X0,bitIndex0) ),
inference(unused_predicate_definition_removal,[],[f117]) ).
fof(f142742,plain,
! [X0] :
( ( v154853(X0,bitIndex0)
& v154858(X0) )
=> v154867(X0) ),
inference(unused_predicate_definition_removal,[],[f109]) ).
fof(f142743,plain,
! [X0] :
( ~ v154858(X0)
=> v154853(X0,bitIndex1) ),
inference(unused_predicate_definition_removal,[],[f116]) ).
fof(f142744,plain,
! [X0] :
( ( v154869(X0)
| v154853(X0,bitIndex3) )
=> v154868(X0) ),
inference(unused_predicate_definition_removal,[],[f100]) ).
fof(f142745,plain,
! [X0] :
( ( v154870(X0)
| v154853(X0,bitIndex2) )
=> v154869(X0) ),
inference(unused_predicate_definition_removal,[],[f101]) ).
fof(f142746,plain,
! [X0] :
( ( v154853(X0,bitIndex0)
| v154853(X0,bitIndex1) )
=> v154870(X0) ),
inference(unused_predicate_definition_removal,[],[f102]) ).
fof(f142771,plain,
~ ! [X0] : v4(X0),
inference(pure_predicate_removal,[],[f96]) ).
fof(f142859,plain,
? [X0] : ~ v4(X0),
inference(ennf_transformation,[],[f142771]) ).
fof(f142860,plain,
! [X0] :
( v154847(X0)
| v4(X0) ),
inference(ennf_transformation,[],[f142724]) ).
fof(f142861,plain,
! [X0] :
( ~ v154847(X0)
| ~ v154848(X0) ),
inference(ennf_transformation,[],[f142725]) ).
fof(f142862,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(ennf_transformation,[],[f142726]) ).
fof(f142863,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(flattening,[],[f142862]) ).
fof(f142864,plain,
! [X0] :
( v154850(X0)
| ( ~ v154851(X0)
& ~ v154859(X0) ) ),
inference(ennf_transformation,[],[f142727]) ).
fof(f142865,plain,
! [X0] :
( v154868(X0)
| ( ~ v154869(X0)
& ~ v154853(X0,bitIndex3) ) ),
inference(ennf_transformation,[],[f142744]) ).
fof(f142866,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(ennf_transformation,[],[f142728]) ).
fof(f142867,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(flattening,[],[f142866]) ).
fof(f142868,plain,
! [X0] :
( v154859(X0)
| ( ~ v154860(X0)
& ~ v154861(X0) ) ),
inference(ennf_transformation,[],[f142729]) ).
fof(f142869,plain,
! [X0] :
( v154869(X0)
| ( ~ v154870(X0)
& ~ v154853(X0,bitIndex2) ) ),
inference(ennf_transformation,[],[f142745]) ).
fof(f142870,plain,
! [X0,X1] :
( ( v154853(X0,X1)
<=> v6(X0,X1) )
| ~ range_3_0(X1) ),
inference(ennf_transformation,[],[f120]) ).
fof(f142871,plain,
! [X0] :
( v154853(X0,bitIndex3)
| v154852(X0) ),
inference(ennf_transformation,[],[f142733]) ).
fof(f142872,plain,
! [X0] :
( v154853(X0,bitIndex2)
| v154855(X0) ),
inference(ennf_transformation,[],[f142738]) ).
fof(f142873,plain,
! [X0] :
( v154853(X0,bitIndex0)
| v154857(X0) ),
inference(ennf_transformation,[],[f142741]) ).
fof(f142874,plain,
! [X0] :
( v154853(X0,bitIndex1)
| v154858(X0) ),
inference(ennf_transformation,[],[f142743]) ).
fof(f142875,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(ennf_transformation,[],[f142730]) ).
fof(f142876,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(flattening,[],[f142875]) ).
fof(f142877,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(ennf_transformation,[],[f142735]) ).
fof(f142878,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(flattening,[],[f142877]) ).
fof(f142879,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(ennf_transformation,[],[f142740]) ).
fof(f142880,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(flattening,[],[f142879]) ).
fof(f142881,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(ennf_transformation,[],[f142742]) ).
fof(f142882,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(flattening,[],[f142881]) ).
fof(f142883,plain,
! [X0] :
( v154870(X0)
| ( ~ v154853(X0,bitIndex0)
& ~ v154853(X0,bitIndex1) ) ),
inference(ennf_transformation,[],[f142746]) ).
fof(f142884,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(ennf_transformation,[],[f142732]) ).
fof(f142885,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(flattening,[],[f142884]) ).
fof(f142886,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(ennf_transformation,[],[f142731]) ).
fof(f142887,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(flattening,[],[f142886]) ).
fof(f142888,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> b0001(X1) )
| ~ range_3_0(X1) )
| ~ v154836(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f142889,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> v154838(X0,X1) )
| ~ range_3_0(X1) )
| v154836(X0) ),
inference(ennf_transformation,[],[f121]) ).
fof(f142890,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(ennf_transformation,[],[f142737]) ).
fof(f142891,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(flattening,[],[f142890]) ).
fof(f142892,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(ennf_transformation,[],[f142736]) ).
fof(f142893,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(flattening,[],[f142892]) ).
fof(f142894,plain,
! [X0] :
( v154862(X0)
| ( ~ v154863(X0)
& ~ v154864(X0) ) ),
inference(ennf_transformation,[],[f142734]) ).
fof(f142895,plain,
! [X0] :
( v154865(X0)
| ( ~ v154866(X0)
& ~ v154867(X0) ) ),
inference(ennf_transformation,[],[f142739]) ).
fof(f142900,plain,
! [X0] :
( ! [X1] :
( ( v154838(X0,X1)
<=> b0010(X1) )
| ~ range_3_0(X1) )
| ~ v154839(X0) ),
inference(ennf_transformation,[],[f124]) ).
fof(f142901,plain,
! [X0] :
( ! [X1] :
( ( v154838(X0,X1)
<=> v154841(X0,X1) )
| ~ range_3_0(X1) )
| v154839(X0) ),
inference(ennf_transformation,[],[f123]) ).
fof(f142916,plain,
! [X0] :
( ! [X1] :
( ( v154841(X0,X1)
<=> v154842(X0,X1) )
| ~ range_3_0(X1) )
| ~ v1051(X0) ),
inference(ennf_transformation,[],[f126]) ).
fof(f142917,plain,
! [X0] :
( ! [X1] :
( ( v154841(X0,X1)
<=> v154844(X0,X1) )
| ~ range_3_0(X1) )
| v1051(X0) ),
inference(ennf_transformation,[],[f125]) ).
fof(f142963,plain,
! [X0,X1] :
( ~ v154842(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f142396]) ).
fof(f142964,plain,
! [X0,X1] :
( ~ v154844(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f142398]) ).
fof(f143190,plain,
! [X0] :
( range_3_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0
& bitIndex2 != X0
& bitIndex3 != X0 ) ),
inference(ennf_transformation,[],[f142723]) ).
fof(f143193,plain,
! [X0] :
( range_1_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0 ) ),
inference(ennf_transformation,[],[f142722]) ).
fof(f143510,plain,
~ v4(sK54),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X0,sK54)],[f142859]) ).
fof(f143511,plain,
! [X0,X1] :
( ( ( v154853(X0,X1)
| ~ v6(X0,X1) )
& ( v6(X0,X1)
| ~ v154853(X0,X1) ) )
| ~ range_3_0(X1) ),
inference(nnf_transformation,[],[f142870]) ).
fof(f143512,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ b0001(X1) )
& ( b0001(X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v154836(X0) ),
inference(nnf_transformation,[],[f142888]) ).
fof(f143513,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ v154838(X0,X1) )
& ( v154838(X0,X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| v154836(X0) ),
inference(nnf_transformation,[],[f142889]) ).
fof(f143520,plain,
! [X0] :
( ! [X1] :
( ( ( v154838(X0,X1)
| ~ b0010(X1) )
& ( b0010(X1)
| ~ v154838(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v154839(X0) ),
inference(nnf_transformation,[],[f142900]) ).
fof(f143521,plain,
! [X0] :
( ! [X1] :
( ( ( v154838(X0,X1)
| ~ v154841(X0,X1) )
& ( v154841(X0,X1)
| ~ v154838(X0,X1) ) )
| ~ range_3_0(X1) )
| v154839(X0) ),
inference(nnf_transformation,[],[f142901]) ).
fof(f143556,plain,
! [X0] :
( ! [X1] :
( ( ( v154841(X0,X1)
| ~ v154842(X0,X1) )
& ( v154842(X0,X1)
| ~ v154841(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v1051(X0) ),
inference(nnf_transformation,[],[f142916]) ).
fof(f143557,plain,
! [X0] :
( ! [X1] :
( ( ( v154841(X0,X1)
| ~ v154844(X0,X1) )
& ( v154844(X0,X1)
| ~ v154841(X0,X1) ) )
| ~ range_3_0(X1) )
| v1051(X0) ),
inference(nnf_transformation,[],[f142917]) ).
fof(f143648,plain,
! [X0] :
( ( v154842(X0,bitIndex3)
| ~ v83122(X0,bitIndex1) )
& ( v83122(X0,bitIndex1)
| ~ v154842(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f133]) ).
fof(f143649,plain,
! [X0] :
( ( v154842(X0,bitIndex2)
| ~ v154843(X0) )
& ( v154843(X0)
| ~ v154842(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f132]) ).
fof(f143650,plain,
! [X0] :
( ( v154844(X0,bitIndex3)
| ~ v83122(X0,bitIndex0) )
& ( v83122(X0,bitIndex0)
| ~ v154844(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f129]) ).
fof(f143651,plain,
! [X0] :
( ( v154844(X0,bitIndex2)
| ~ v154845(X0) )
& ( v154845(X0)
| ~ v154844(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f128]) ).
fof(f143916,plain,
! [X0] :
( ( ~ v154843(X0)
| ~ v83122(X0,bitIndex1) )
& ( v83122(X0,bitIndex1)
| v154843(X0) ) ),
inference(nnf_transformation,[],[f134]) ).
fof(f143917,plain,
! [X0] :
( ( ~ v154845(X0)
| ~ v83122(X0,bitIndex0) )
& ( v83122(X0,bitIndex0)
| v154845(X0) ) ),
inference(nnf_transformation,[],[f130]) ).
fof(f145955,plain,
~ v4(sK54),
inference(cnf_transformation,[],[f143510]) ).
fof(f145956,plain,
! [X0] :
( v154847(X0)
| v4(X0) ),
inference(cnf_transformation,[],[f142860]) ).
fof(f145957,plain,
! [X0] :
( ~ v154847(X0)
| ~ v154848(X0) ),
inference(cnf_transformation,[],[f142861]) ).
fof(f145958,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(cnf_transformation,[],[f142863]) ).
fof(f145959,plain,
! [X0] :
( v154850(X0)
| ~ v154859(X0) ),
inference(cnf_transformation,[],[f142864]) ).
fof(f145960,plain,
! [X0] :
( v154850(X0)
| ~ v154851(X0) ),
inference(cnf_transformation,[],[f142864]) ).
fof(f145961,plain,
! [X0] :
( v154868(X0)
| ~ v154853(X0,bitIndex3) ),
inference(cnf_transformation,[],[f142865]) ).
fof(f145962,plain,
! [X0] :
( v154868(X0)
| ~ v154869(X0) ),
inference(cnf_transformation,[],[f142865]) ).
fof(f145963,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(cnf_transformation,[],[f142867]) ).
fof(f145964,plain,
! [X0] :
( v154859(X0)
| ~ v154861(X0) ),
inference(cnf_transformation,[],[f142868]) ).
fof(f145965,plain,
! [X0] :
( v154859(X0)
| ~ v154860(X0) ),
inference(cnf_transformation,[],[f142868]) ).
fof(f145966,plain,
! [X0] :
( v154869(X0)
| ~ v154853(X0,bitIndex2) ),
inference(cnf_transformation,[],[f142869]) ).
fof(f145967,plain,
! [X0] :
( v154869(X0)
| ~ v154870(X0) ),
inference(cnf_transformation,[],[f142869]) ).
fof(f145968,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v154853(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f143511]) ).
fof(f145969,plain,
! [X0,X1] :
( v154853(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f143511]) ).
fof(f145970,plain,
! [X0] :
( v154853(X0,bitIndex3)
| v154852(X0) ),
inference(cnf_transformation,[],[f142871]) ).
fof(f145971,plain,
! [X0] :
( v154853(X0,bitIndex2)
| v154855(X0) ),
inference(cnf_transformation,[],[f142872]) ).
fof(f145972,plain,
! [X0] :
( v154853(X0,bitIndex0)
| v154857(X0) ),
inference(cnf_transformation,[],[f142873]) ).
fof(f145973,plain,
! [X0] :
( v154853(X0,bitIndex1)
| v154858(X0) ),
inference(cnf_transformation,[],[f142874]) ).
fof(f145974,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(cnf_transformation,[],[f142876]) ).
fof(f145975,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(cnf_transformation,[],[f142878]) ).
fof(f145976,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(cnf_transformation,[],[f142880]) ).
fof(f145977,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(cnf_transformation,[],[f142882]) ).
fof(f145978,plain,
! [X0] :
( v154870(X0)
| ~ v154853(X0,bitIndex1) ),
inference(cnf_transformation,[],[f142883]) ).
fof(f145979,plain,
! [X0] :
( v154870(X0)
| ~ v154853(X0,bitIndex0) ),
inference(cnf_transformation,[],[f142883]) ).
fof(f145980,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(cnf_transformation,[],[f142885]) ).
fof(f145981,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(cnf_transformation,[],[f142887]) ).
fof(f145982,plain,
! [X0,X1] :
( b0001(X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| ~ v154836(X0) ),
inference(cnf_transformation,[],[f143512]) ).
fof(f145983,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ b0001(X1)
| ~ range_3_0(X1)
| ~ v154836(X0) ),
inference(cnf_transformation,[],[f143512]) ).
fof(f145984,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| v154836(X0) ),
inference(cnf_transformation,[],[f143513]) ).
fof(f145985,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| v154836(X0) ),
inference(cnf_transformation,[],[f143513]) ).
fof(f145986,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(cnf_transformation,[],[f142891]) ).
fof(f145987,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(cnf_transformation,[],[f142893]) ).
fof(f145988,plain,
! [X0] :
( v154862(X0)
| ~ v154864(X0) ),
inference(cnf_transformation,[],[f142894]) ).
fof(f145989,plain,
! [X0] :
( v154862(X0)
| ~ v154863(X0) ),
inference(cnf_transformation,[],[f142894]) ).
fof(f145990,plain,
! [X0] :
( v154865(X0)
| ~ v154867(X0) ),
inference(cnf_transformation,[],[f142895]) ).
fof(f145991,plain,
! [X0] :
( v154865(X0)
| ~ v154866(X0) ),
inference(cnf_transformation,[],[f142895]) ).
fof(f145995,plain,
b0001(bitIndex0),
inference(cnf_transformation,[],[f138123]) ).
fof(f145996,plain,
~ b0001(bitIndex1),
inference(cnf_transformation,[],[f138122]) ).
fof(f145997,plain,
~ b0001(bitIndex2),
inference(cnf_transformation,[],[f138121]) ).
fof(f145998,plain,
~ b0001(bitIndex3),
inference(cnf_transformation,[],[f138120]) ).
fof(f146011,plain,
! [X0,X1] :
( b0010(X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| ~ v154839(X0) ),
inference(cnf_transformation,[],[f143520]) ).
fof(f146012,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ b0010(X1)
| ~ range_3_0(X1)
| ~ v154839(X0) ),
inference(cnf_transformation,[],[f143520]) ).
fof(f146013,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| v154839(X0) ),
inference(cnf_transformation,[],[f143521]) ).
fof(f146014,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| v154839(X0) ),
inference(cnf_transformation,[],[f143521]) ).
fof(f146079,plain,
~ b0010(bitIndex0),
inference(cnf_transformation,[],[f138096]) ).
fof(f146080,plain,
b0010(bitIndex1),
inference(cnf_transformation,[],[f138095]) ).
fof(f146081,plain,
~ b0010(bitIndex2),
inference(cnf_transformation,[],[f138094]) ).
fof(f146082,plain,
~ b0010(bitIndex3),
inference(cnf_transformation,[],[f138093]) ).
fof(f146087,plain,
! [X0,X1] :
( v154842(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| ~ v1051(X0) ),
inference(cnf_transformation,[],[f143556]) ).
fof(f146088,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154842(X0,X1)
| ~ range_3_0(X1)
| ~ v1051(X0) ),
inference(cnf_transformation,[],[f143556]) ).
fof(f146089,plain,
! [X0,X1] :
( v154844(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| v1051(X0) ),
inference(cnf_transformation,[],[f143557]) ).
fof(f146090,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154844(X0,X1)
| ~ range_3_0(X1)
| v1051(X0) ),
inference(cnf_transformation,[],[f143557]) ).
fof(f146264,plain,
! [X0] :
( v83122(X0,bitIndex1)
| ~ v154842(X0,bitIndex3) ),
inference(cnf_transformation,[],[f143648]) ).
fof(f146265,plain,
! [X0] :
( v154842(X0,bitIndex3)
| ~ v83122(X0,bitIndex1) ),
inference(cnf_transformation,[],[f143648]) ).
fof(f146266,plain,
! [X0] :
( v154843(X0)
| ~ v154842(X0,bitIndex2) ),
inference(cnf_transformation,[],[f143649]) ).
fof(f146267,plain,
! [X0] :
( v154842(X0,bitIndex2)
| ~ v154843(X0) ),
inference(cnf_transformation,[],[f143649]) ).
fof(f146268,plain,
! [X0,X1] :
( ~ v154842(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f142963]) ).
fof(f146269,plain,
! [X0] :
( v83122(X0,bitIndex0)
| ~ v154844(X0,bitIndex3) ),
inference(cnf_transformation,[],[f143650]) ).
fof(f146270,plain,
! [X0] :
( v154844(X0,bitIndex3)
| ~ v83122(X0,bitIndex0) ),
inference(cnf_transformation,[],[f143650]) ).
fof(f146271,plain,
! [X0] :
( v154845(X0)
| ~ v154844(X0,bitIndex2) ),
inference(cnf_transformation,[],[f143651]) ).
fof(f146272,plain,
! [X0] :
( v154844(X0,bitIndex2)
| ~ v154845(X0) ),
inference(cnf_transformation,[],[f143651]) ).
fof(f146273,plain,
! [X0,X1] :
( ~ v154844(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f142964]) ).
fof(f146792,plain,
! [X0] :
( v83122(X0,bitIndex1)
| v154843(X0) ),
inference(cnf_transformation,[],[f143916]) ).
fof(f146793,plain,
! [X0] :
( ~ v154843(X0)
| ~ v83122(X0,bitIndex1) ),
inference(cnf_transformation,[],[f143916]) ).
fof(f146794,plain,
! [X0] :
( v83122(X0,bitIndex0)
| v154845(X0) ),
inference(cnf_transformation,[],[f143917]) ).
fof(f146795,plain,
! [X0] :
( ~ v154845(X0)
| ~ v83122(X0,bitIndex0) ),
inference(cnf_transformation,[],[f143917]) ).
fof(f148351,plain,
! [X0] :
( range_3_0(X0)
| bitIndex3 != X0 ),
inference(cnf_transformation,[],[f143190]) ).
fof(f148352,plain,
! [X0] :
( range_3_0(X0)
| bitIndex2 != X0 ),
inference(cnf_transformation,[],[f143190]) ).
fof(f148353,plain,
! [X0] :
( range_3_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f143190]) ).
fof(f148354,plain,
! [X0] :
( range_3_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f143190]) ).
fof(f148366,plain,
! [X0] :
( range_1_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f143193]) ).
fof(f148367,plain,
! [X0] :
( range_1_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f143193]) ).
fof(f151027,plain,
range_3_0(bitIndex0),
inference(equality_resolution,[],[f148354]) ).
fof(f151028,plain,
range_3_0(bitIndex1),
inference(equality_resolution,[],[f148353]) ).
fof(f151029,plain,
range_3_0(bitIndex2),
inference(equality_resolution,[],[f148352]) ).
fof(f151030,plain,
range_3_0(bitIndex3),
inference(equality_resolution,[],[f148351]) ).
fof(f151042,plain,
range_1_0(bitIndex0),
inference(equality_resolution,[],[f148367]) ).
fof(f151043,plain,
range_1_0(bitIndex1),
inference(equality_resolution,[],[f148366]) ).
fof(f151146,plain,
v154847(sK54),
inference(resolution,[],[f145955,f145956]) ).
fof(f151147,plain,
~ v154848(sK54),
inference(resolution,[],[f151146,f145957]) ).
fof(f151148,plain,
( ~ v154850(sK54)
| ~ v154868(sK54) ),
inference(resolution,[],[f151147,f145958]) ).
fof(f151150,definition,
( spl55_1
<=> v154868(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_1])],[avatar_definition]) ).
fof(f151152,plain,
( ~ v154868(sK54)
| spl55_1 ),
inference(avatar_component_clause,[],[f151150]) ).
fof(f151154,definition,
( spl55_2
<=> v154850(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_2])],[avatar_definition]) ).
fof(f151156,plain,
( ~ v154850(sK54)
| spl55_2 ),
inference(avatar_component_clause,[],[f151154]) ).
fof(f151157,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(avatar_split_clause,[],[f151148,f151154,f151150]) ).
fof(f151158,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_1 ),
inference(resolution,[],[f151152,f145961]) ).
fof(f151159,plain,
( ~ v154869(sK54)
| spl55_1 ),
inference(resolution,[],[f151152,f145962]) ).
fof(f151161,plain,
( ~ v154870(sK54)
| spl55_1 ),
inference(resolution,[],[f151159,f145967]) ).
fof(f151163,plain,
( ~ v6(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl55_1 ),
inference(resolution,[],[f151158,f145969]) ).
fof(f151164,plain,
( ~ v6(sK54,bitIndex3)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f151163,f151030]) ).
fof(f151170,definition,
( spl55_3
<=> v154854(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_3])],[avatar_definition]) ).
fof(f151171,plain,
( v154854(sK54)
| ~ spl55_3 ),
inference(avatar_component_clause,[],[f151170]) ).
fof(f151172,plain,
( ~ v154854(sK54)
| spl55_3 ),
inference(avatar_component_clause,[],[f151170]) ).
fof(f151174,definition,
( spl55_4
<=> v154851(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_4])],[avatar_definition]) ).
fof(f151175,plain,
( ~ v154851(sK54)
| spl55_4 ),
inference(avatar_component_clause,[],[f151174]) ).
fof(f151179,definition,
( spl55_5
<=> v154862(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_5])],[avatar_definition]) ).
fof(f151180,plain,
( v154862(sK54)
| ~ spl55_5 ),
inference(avatar_component_clause,[],[f151179]) ).
fof(f151181,plain,
( ~ v154862(sK54)
| spl55_5 ),
inference(avatar_component_clause,[],[f151179]) ).
fof(f151183,definition,
( spl55_6
<=> v154861(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_6])],[avatar_definition]) ).
fof(f151184,plain,
( ~ v154861(sK54)
| spl55_6 ),
inference(avatar_component_clause,[],[f151183]) ).
fof(f151187,plain,
( ~ v154855(sK54)
| ~ v154856(sK54)
| spl55_3 ),
inference(resolution,[],[f151172,f145981]) ).
fof(f151189,definition,
( spl55_7
<=> v154856(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_7])],[avatar_definition]) ).
fof(f151190,plain,
( v154856(sK54)
| ~ spl55_7 ),
inference(avatar_component_clause,[],[f151189]) ).
fof(f151191,plain,
( ~ v154856(sK54)
| spl55_7 ),
inference(avatar_component_clause,[],[f151189]) ).
fof(f151193,definition,
( spl55_8
<=> v154855(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_8])],[avatar_definition]) ).
fof(f151194,plain,
( v154855(sK54)
| ~ spl55_8 ),
inference(avatar_component_clause,[],[f151193]) ).
fof(f151195,plain,
( ~ v154855(sK54)
| spl55_8 ),
inference(avatar_component_clause,[],[f151193]) ).
fof(f151196,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_3 ),
inference(avatar_split_clause,[],[f151187,f151170,f151193,f151189]) ).
fof(f151201,plain,
( ~ v154864(sK54)
| spl55_5 ),
inference(resolution,[],[f151181,f145988]) ).
fof(f151202,plain,
( ~ v154863(sK54)
| spl55_5 ),
inference(resolution,[],[f151181,f145989]) ).
fof(f151203,plain,
( ~ v154838(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154836(sK54)
| spl55_1 ),
inference(resolution,[],[f151164,f145985]) ).
fof(f151206,plain,
( ~ v154838(sK54,bitIndex3)
| v154836(sK54)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f151203,f151030]) ).
fof(f151208,definition,
( spl55_9
<=> v154836(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_9])],[avatar_definition]) ).
fof(f151209,plain,
( ~ v154836(sK54)
| spl55_9 ),
inference(avatar_component_clause,[],[f151208]) ).
fof(f151210,plain,
( v154836(sK54)
| ~ spl55_9 ),
inference(avatar_component_clause,[],[f151208]) ).
fof(f151212,definition,
( spl55_10
<=> v154838(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_10])],[avatar_definition]) ).
fof(f151213,plain,
( v154838(sK54,bitIndex3)
| ~ spl55_10 ),
inference(avatar_component_clause,[],[f151212]) ).
fof(f151214,plain,
( ~ v154838(sK54,bitIndex3)
| spl55_10 ),
inference(avatar_component_clause,[],[f151212]) ).
fof(f151215,plain,
( spl55_9
| ~ spl55_10
| spl55_1 ),
inference(avatar_split_clause,[],[f151206,f151150,f151212,f151208]) ).
fof(f151216,plain,
( ~ v154857(sK54)
| ~ v154858(sK54)
| spl55_7 ),
inference(resolution,[],[f151191,f145987]) ).
fof(f151218,definition,
( spl55_11
<=> v154858(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_11])],[avatar_definition]) ).
fof(f151220,plain,
( ~ v154858(sK54)
| spl55_11 ),
inference(avatar_component_clause,[],[f151218]) ).
fof(f151222,definition,
( spl55_12
<=> v154857(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_12])],[avatar_definition]) ).
fof(f151223,plain,
( v154857(sK54)
| ~ spl55_12 ),
inference(avatar_component_clause,[],[f151222]) ).
fof(f151224,plain,
( ~ v154857(sK54)
| spl55_12 ),
inference(avatar_component_clause,[],[f151222]) ).
fof(f151225,plain,
( ~ spl55_11
| ~ spl55_12
| spl55_7 ),
inference(avatar_split_clause,[],[f151216,f151189,f151222,f151218]) ).
fof(f151232,plain,
( ~ v154859(sK54)
| spl55_2 ),
inference(resolution,[],[f151156,f145959]) ).
fof(f151233,plain,
( ~ v154851(sK54)
| spl55_2 ),
inference(resolution,[],[f151156,f145960]) ).
fof(f151234,plain,
( ~ spl55_4
| spl55_2 ),
inference(avatar_split_clause,[],[f151233,f151154,f151174]) ).
fof(f151235,plain,
( ~ v154861(sK54)
| spl55_2 ),
inference(resolution,[],[f151232,f145964]) ).
fof(f151236,plain,
( ~ v154860(sK54)
| spl55_2 ),
inference(resolution,[],[f151232,f145965]) ).
fof(f151237,plain,
( ~ spl55_6
| spl55_2 ),
inference(avatar_split_clause,[],[f151235,f151154,f151183]) ).
fof(f151241,plain,
( v154864(sK54)
| ~ v154865(sK54)
| ~ spl55_8 ),
inference(resolution,[],[f151194,f145986]) ).
fof(f151243,plain,
( ~ v154865(sK54)
| spl55_5
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f151241,f151201]) ).
fof(f151244,plain,
( ~ v154841(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154839(sK54)
| spl55_10 ),
inference(resolution,[],[f151214,f146014]) ).
fof(f151246,plain,
( ~ v6(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154836(sK54)
| spl55_10 ),
inference(resolution,[],[f151214,f145984]) ).
fof(f151247,plain,
( ~ v6(sK54,bitIndex3)
| v154836(sK54)
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f151246,f151030]) ).
fof(f151248,plain,
( ~ v154841(sK54,bitIndex3)
| v154839(sK54)
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f151244,f151030]) ).
fof(f151250,definition,
( spl55_13
<=> v6(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_13])],[avatar_definition]) ).
fof(f151251,plain,
( v6(sK54,bitIndex3)
| ~ spl55_13 ),
inference(avatar_component_clause,[],[f151250]) ).
fof(f151252,plain,
( ~ v6(sK54,bitIndex3)
| spl55_13 ),
inference(avatar_component_clause,[],[f151250]) ).
fof(f151253,plain,
( spl55_9
| ~ spl55_13
| spl55_10 ),
inference(avatar_split_clause,[],[f151247,f151212,f151250,f151208]) ).
fof(f151255,definition,
( spl55_14
<=> v154839(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_14])],[avatar_definition]) ).
fof(f151256,plain,
( ~ v154839(sK54)
| spl55_14 ),
inference(avatar_component_clause,[],[f151255]) ).
fof(f151257,plain,
( v154839(sK54)
| ~ spl55_14 ),
inference(avatar_component_clause,[],[f151255]) ).
fof(f151259,definition,
( spl55_15
<=> v154841(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_15])],[avatar_definition]) ).
fof(f151260,plain,
( v154841(sK54,bitIndex3)
| ~ spl55_15 ),
inference(avatar_component_clause,[],[f151259]) ).
fof(f151261,plain,
( ~ v154841(sK54,bitIndex3)
| spl55_15 ),
inference(avatar_component_clause,[],[f151259]) ).
fof(f151262,plain,
( spl55_14
| ~ spl55_15
| spl55_10 ),
inference(avatar_split_clause,[],[f151248,f151212,f151259,f151255]) ).
fof(f151265,plain,
( v154853(sK54,bitIndex1)
| spl55_11 ),
inference(resolution,[],[f151220,f145973]) ).
fof(f151268,plain,
( ~ v154853(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl55_13 ),
inference(resolution,[],[f151252,f145968]) ).
fof(f151269,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151268,f151030]) ).
fof(f151270,plain,
( ~ v154867(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151243,f145990]) ).
fof(f151271,plain,
( ~ v154866(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151243,f145991]) ).
fof(f151272,plain,
( ~ v154844(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v1051(sK54)
| spl55_15 ),
inference(resolution,[],[f151261,f146090]) ).
fof(f151273,plain,
( ~ v154842(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| spl55_15 ),
inference(resolution,[],[f151261,f146088]) ).
fof(f151275,plain,
( ~ v154842(sK54,bitIndex3)
| ~ v1051(sK54)
| spl55_15 ),
inference(forward_subsumption_resolution,[],[f151273,f151030]) ).
fof(f151276,plain,
( ~ v154844(sK54,bitIndex3)
| v1051(sK54)
| spl55_15 ),
inference(forward_subsumption_resolution,[],[f151272,f151030]) ).
fof(f151278,definition,
( spl55_16
<=> v1051(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_16])],[avatar_definition]) ).
fof(f151279,plain,
( v1051(sK54)
| ~ spl55_16 ),
inference(avatar_component_clause,[],[f151278]) ).
fof(f151280,plain,
( ~ v1051(sK54)
| spl55_16 ),
inference(avatar_component_clause,[],[f151278]) ).
fof(f151282,definition,
( spl55_17
<=> v154842(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_17])],[avatar_definition]) ).
fof(f151283,plain,
( v154842(sK54,bitIndex3)
| ~ spl55_17 ),
inference(avatar_component_clause,[],[f151282]) ).
fof(f151284,plain,
( ~ v154842(sK54,bitIndex3)
| spl55_17 ),
inference(avatar_component_clause,[],[f151282]) ).
fof(f151285,plain,
( ~ spl55_16
| ~ spl55_17
| spl55_15 ),
inference(avatar_split_clause,[],[f151275,f151259,f151282,f151278]) ).
fof(f151287,definition,
( spl55_18
<=> v154844(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_18])],[avatar_definition]) ).
fof(f151288,plain,
( v154844(sK54,bitIndex3)
| ~ spl55_18 ),
inference(avatar_component_clause,[],[f151287]) ).
fof(f151289,plain,
( ~ v154844(sK54,bitIndex3)
| spl55_18 ),
inference(avatar_component_clause,[],[f151287]) ).
fof(f151290,plain,
( spl55_16
| ~ spl55_18
| spl55_15 ),
inference(avatar_split_clause,[],[f151276,f151259,f151287,f151278]) ).
fof(f151333,plain,
( v154852(sK54)
| spl55_13 ),
inference(resolution,[],[f151269,f145970]) ).
fof(f151335,plain,
( ~ v154853(sK54,bitIndex0)
| ~ v154858(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151270,f145977]) ).
fof(f151336,plain,
( ~ v83122(sK54,bitIndex0)
| spl55_18 ),
inference(resolution,[],[f151289,f146270]) ).
fof(f151338,plain,
( ~ v154857(sK54)
| ~ v154853(sK54,bitIndex1)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151271,f145976]) ).
fof(f151339,plain,
( ~ v154857(sK54)
| spl55_5
| ~ spl55_8
| spl55_11 ),
inference(forward_subsumption_resolution,[],[f151338,f151265]) ).
fof(f151340,plain,
( ~ spl55_12
| spl55_5
| ~ spl55_8
| spl55_11 ),
inference(avatar_split_clause,[],[f151339,f151218,f151193,f151179,f151222]) ).
fof(f151341,plain,
( v154853(sK54,bitIndex0)
| spl55_12 ),
inference(resolution,[],[f151224,f145972]) ).
fof(f151385,plain,
( v154861(sK54)
| ~ v154862(sK54)
| spl55_13 ),
inference(resolution,[],[f151333,f145980]) ).
fof(f151425,plain,
( v154845(sK54)
| spl55_18 ),
inference(resolution,[],[f151336,f146794]) ).
fof(f151429,definition,
( spl55_31
<=> v83122(sK54,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl55_31])],[avatar_definition]) ).
fof(f151430,plain,
( ~ v83122(sK54,bitIndex1)
| spl55_31 ),
inference(avatar_component_clause,[],[f151429]) ).
fof(f151431,plain,
( v83122(sK54,bitIndex1)
| ~ spl55_31 ),
inference(avatar_component_clause,[],[f151429]) ).
fof(f151448,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| b0010(X0)
| ~ range_3_0(X0) )
| ~ spl55_14 ),
inference(resolution,[],[f151257,f146011]) ).
fof(f151460,plain,
( v83122(sK54,bitIndex0)
| ~ spl55_18 ),
inference(resolution,[],[f151288,f146269]) ).
fof(f151465,plain,
( ! [X0] :
( b0010(X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0)
| v154836(sK54) )
| ~ spl55_14 ),
inference(resolution,[],[f151448,f145984]) ).
fof(f151466,plain,
( ! [X0] :
( b0010(X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| v154836(sK54) )
| ~ spl55_14 ),
inference(duplicate_literal_removal,[],[f151465]) ).
fof(f151470,definition,
( spl55_35
<=> ! [X0] :
( b0010(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_35])],[avatar_definition]) ).
fof(f151471,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| b0010(X0)
| ~ range_3_0(X0) )
| ~ spl55_35 ),
inference(avatar_component_clause,[],[f151470]) ).
fof(f151472,plain,
( spl55_9
| spl55_35
| ~ spl55_14 ),
inference(avatar_split_clause,[],[f151466,f151255,f151470,f151208]) ).
fof(f151476,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| spl55_14 ),
inference(resolution,[],[f151256,f146013]) ).
fof(f151491,plain,
( ! [X0] :
( ~ v154842(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_16 ),
inference(resolution,[],[f151279,f146088]) ).
fof(f151549,plain,
( ~ v83122(sK54,bitIndex1)
| spl55_17 ),
inference(resolution,[],[f151284,f146265]) ).
fof(f151551,plain,
( ~ spl55_31
| spl55_17 ),
inference(avatar_split_clause,[],[f151549,f151282,f151429]) ).
fof(f151558,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0)
| v154836(sK54) )
| spl55_14 ),
inference(resolution,[],[f151476,f145984]) ).
fof(f151559,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| v154836(sK54) )
| spl55_14 ),
inference(duplicate_literal_removal,[],[f151558]) ).
fof(f151563,definition,
( spl55_45
<=> ! [X0] :
( v154841(sK54,X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_45])],[avatar_definition]) ).
fof(f151564,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_45 ),
inference(avatar_component_clause,[],[f151563]) ).
fof(f151565,plain,
( spl55_9
| spl55_45
| spl55_14 ),
inference(avatar_split_clause,[],[f151559,f151255,f151563,f151208]) ).
fof(f151568,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151210,f145982]) ).
fof(f151578,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151568,f145968]) ).
fof(f151579,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl55_9 ),
inference(duplicate_literal_removal,[],[f151578]) ).
fof(f151611,plain,
( ~ range_3_0(bitIndex2)
| b0001(bitIndex2)
| v154855(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f151579,f145971]) ).
fof(f151613,plain,
( ~ range_3_0(bitIndex1)
| b0001(bitIndex1)
| v154858(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f151579,f145973]) ).
fof(f151615,plain,
( b0001(bitIndex1)
| v154858(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151613,f151028]) ).
fof(f151617,plain,
( v154858(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151615,f145996]) ).
fof(f151622,plain,
( ~ v154858(sK54)
| spl55_5
| ~ spl55_8
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151335,f151341]) ).
fof(f151635,plain,
( ~ v154862(sK54)
| spl55_6
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151385,f151184]) ).
fof(f151638,plain,
( $false
| ~ spl55_5
| spl55_6
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151635,f151180]) ).
fof(f151639,plain,
( ~ spl55_5
| spl55_6
| spl55_13 ),
inference(avatar_contradiction_clause,[],[f151638]) ).
fof(f151650,plain,
( b0001(bitIndex2)
| v154855(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151611,f151029]) ).
fof(f151651,plain,
( v154855(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151650,f145997]) ).
fof(f151652,plain,
( $false
| spl55_8
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151651,f151195]) ).
fof(f151653,plain,
( spl55_8
| ~ spl55_9 ),
inference(avatar_contradiction_clause,[],[f151652]) ).
fof(f151664,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151209,f145984]) ).
fof(f151665,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| v6(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151209,f145985]) ).
fof(f151667,plain,
( v154853(sK54,bitIndex2)
| spl55_8 ),
inference(resolution,[],[f151195,f145971]) ).
fof(f151678,plain,
( ! [X0] :
( v154838(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151664,f145968]) ).
fof(f151679,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154838(sK54,X0) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151678]) ).
fof(f151684,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ v154841(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| spl55_9 ),
inference(resolution,[],[f151665,f146014]) ).
fof(f151685,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ range_3_0(X0)
| ~ v154839(sK54) )
| spl55_9 ),
inference(resolution,[],[f151665,f146012]) ).
fof(f151688,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ v154839(sK54) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151685]) ).
fof(f151689,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ v154841(sK54,X0)
| v154839(sK54) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151684]) ).
fof(f151697,plain,
( v154863(sK54)
| ~ v154856(sK54)
| spl55_8 ),
inference(resolution,[],[f151667,f145975]) ).
fof(f151699,plain,
( v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_8 ),
inference(resolution,[],[f151667,f145968]) ).
fof(f151700,plain,
( v6(sK54,bitIndex2)
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f151699,f151029]) ).
fof(f151716,plain,
( ~ range_3_0(bitIndex2)
| v154838(sK54,bitIndex2)
| spl55_8
| spl55_9 ),
inference(resolution,[],[f151679,f151667]) ).
fof(f151720,plain,
( ~ range_3_0(bitIndex0)
| v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(resolution,[],[f151679,f145972]) ).
fof(f151721,plain,
( ~ range_3_0(bitIndex1)
| v154838(sK54,bitIndex1)
| v154858(sK54)
| spl55_9 ),
inference(resolution,[],[f151679,f145973]) ).
fof(f151723,plain,
( v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151720,f151027]) ).
fof(f151725,plain,
( v154838(sK54,bitIndex2)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151716,f151029]) ).
fof(f151726,plain,
( v154838(sK54,bitIndex0)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151723,f151224]) ).
fof(f151751,plain,
( ~ v154845(sK54)
| ~ spl55_18 ),
inference(resolution,[],[f151460,f146795]) ).
fof(f151813,plain,
( b0010(bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(resolution,[],[f151725,f146011]) ).
fof(f151821,plain,
( v154841(sK54,bitIndex0)
| ~ range_3_0(bitIndex0)
| v154839(sK54)
| spl55_9
| spl55_12 ),
inference(resolution,[],[f151726,f146013]) ).
fof(f151822,plain,
( b0010(bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(resolution,[],[f151726,f146011]) ).
fof(f151824,plain,
( v154841(sK54,bitIndex0)
| v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151821,f151027]) ).
fof(f151968,plain,
( ~ v154844(sK54,bitIndex2)
| ~ spl55_18 ),
inference(resolution,[],[f151751,f146271]) ).
fof(f151971,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154843(sK54)
| ~ spl55_16 ),
inference(resolution,[],[f151491,f146267]) ).
fof(f151975,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_8
| ~ spl55_45 ),
inference(resolution,[],[f151564,f151700]) ).
fof(f151978,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_45 ),
inference(resolution,[],[f151564,f145968]) ).
fof(f151979,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154841(sK54,X0) )
| ~ spl55_45 ),
inference(duplicate_literal_removal,[],[f151978]) ).
fof(f152052,plain,
( v154843(sK54)
| spl55_31 ),
inference(resolution,[],[f151430,f146792]) ).
fof(f152101,plain,
( ~ range_3_0(bitIndex2)
| ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151813,f146081]) ).
fof(f152102,plain,
( ~ range_3_0(bitIndex0)
| ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151822,f146079]) ).
fof(f152103,plain,
( v154841(sK54,bitIndex2)
| ~ v154843(sK54)
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f151971,f151029]) ).
fof(f152105,plain,
( v154841(sK54,bitIndex2)
| spl55_8
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f151975,f151029]) ).
fof(f152110,plain,
( ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f152101,f151029]) ).
fof(f152111,plain,
( ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f152102,f151027]) ).
fof(f152113,definition,
( spl55_72
<=> v154843(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_72])],[avatar_definition]) ).
fof(f152114,plain,
( v154843(sK54)
| ~ spl55_72 ),
inference(avatar_component_clause,[],[f152113]) ).
fof(f152115,plain,
( ~ v154843(sK54)
| spl55_72 ),
inference(avatar_component_clause,[],[f152113]) ).
fof(f152117,definition,
( spl55_73
<=> v154841(sK54,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl55_73])],[avatar_definition]) ).
fof(f152119,plain,
( v154841(sK54,bitIndex2)
| ~ spl55_73 ),
inference(avatar_component_clause,[],[f152117]) ).
fof(f152120,plain,
( ~ spl55_72
| spl55_73
| ~ spl55_16 ),
inference(avatar_split_clause,[],[f152103,f151278,f152117,f152113]) ).
fof(f152121,plain,
( spl55_73
| spl55_8
| ~ spl55_45 ),
inference(avatar_split_clause,[],[f152105,f151563,f151193,f152117]) ).
fof(f152128,plain,
( $false
| spl55_8
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f152110,f151257]) ).
fof(f152129,plain,
( spl55_8
| spl55_9
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f152128]) ).
fof(f152132,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| ~ range_3_0(X0)
| v6(sK54,X0) )
| spl55_9
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f151689,f151256]) ).
fof(f152133,plain,
( v154841(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f151824,f151256]) ).
fof(f152152,plain,
( spl55_72
| spl55_31 ),
inference(avatar_split_clause,[],[f152052,f151429,f152113]) ).
fof(f152159,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_14 ),
inference(resolution,[],[f151256,f146014]) ).
fof(f152163,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154842(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_16 ),
inference(resolution,[],[f151279,f146087]) ).
fof(f152322,plain,
( ! [X0] :
( v154842(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| ~ spl55_16 ),
inference(resolution,[],[f152163,f146013]) ).
fof(f152323,plain,
( ! [X0] :
( v154842(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| v154839(sK54) )
| ~ spl55_16 ),
inference(duplicate_literal_removal,[],[f152322]) ).
fof(f152326,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154842(sK54,X0) )
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152323,f151256]) ).
fof(f152448,plain,
( v154838(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_14
| ~ spl55_73 ),
inference(resolution,[],[f152119,f152159]) ).
fof(f152449,plain,
( ~ range_3_0(bitIndex2)
| v6(sK54,bitIndex2)
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(resolution,[],[f152119,f152132]) ).
fof(f152455,plain,
( v154842(sK54,bitIndex0)
| ~ range_3_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f152133,f152163]) ).
fof(f152462,plain,
( v154842(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152455,f151027]) ).
fof(f152602,plain,
( ~ range_3_0(bitIndex3)
| v154841(sK54,bitIndex3)
| v154852(sK54)
| ~ spl55_45 ),
inference(resolution,[],[f151979,f145970]) ).
fof(f152605,plain,
( ~ range_3_0(bitIndex1)
| v154841(sK54,bitIndex1)
| v154858(sK54)
| ~ spl55_45 ),
inference(resolution,[],[f151979,f145973]) ).
fof(f153717,plain,
( ~ range_1_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f152462,f146268]) ).
fof(f153719,plain,
( $false
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153717,f151042]) ).
fof(f153720,plain,
( spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f153719]) ).
fof(f153721,plain,
( v154838(sK54,bitIndex1)
| v154858(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151721,f151028]) ).
fof(f153722,plain,
( v154841(sK54,bitIndex1)
| v154858(sK54)
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152605,f151028]) ).
fof(f153723,plain,
( v154838(sK54,bitIndex1)
| spl55_9
| spl55_11 ),
inference(forward_subsumption_resolution,[],[f153721,f151220]) ).
fof(f153724,plain,
( v154841(sK54,bitIndex1)
| spl55_11
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f153722,f151220]) ).
fof(f153727,plain,
( v154866(sK54)
| ~ v154853(sK54,bitIndex1)
| ~ spl55_12 ),
inference(resolution,[],[f151223,f145976]) ).
fof(f153730,plain,
( ~ range_3_0(bitIndex1)
| v154842(sK54,bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f153723,f152326]) ).
fof(f153738,plain,
( v154842(sK54,bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153730,f151028]) ).
fof(f153972,plain,
( v154844(sK54,bitIndex1)
| ~ range_3_0(bitIndex1)
| v1051(sK54)
| spl55_11
| ~ spl55_45 ),
inference(resolution,[],[f153724,f146089]) ).
fof(f153980,plain,
( ~ range_1_0(bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f153738,f146268]) ).
fof(f153982,plain,
( $false
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153980,f151043]) ).
fof(f153983,plain,
( spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f153982]) ).
fof(f153985,definition,
( spl55_295
<=> v154853(sK54,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl55_295])],[avatar_definition]) ).
fof(f153987,plain,
( ~ v154853(sK54,bitIndex1)
| spl55_295 ),
inference(avatar_component_clause,[],[f153985]) ).
fof(f153989,definition,
( spl55_296
<=> v154866(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_296])],[avatar_definition]) ).
fof(f153992,plain,
( ~ spl55_295
| spl55_296
| ~ spl55_12 ),
inference(avatar_split_clause,[],[f153727,f151222,f153989,f153985]) ).
fof(f153994,plain,
( ~ v154856(sK54)
| spl55_5
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f151697,f151202]) ).
fof(f153997,plain,
( $false
| spl55_5
| ~ spl55_7
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f153994,f151190]) ).
fof(f153998,plain,
( spl55_5
| ~ spl55_7
| spl55_8 ),
inference(avatar_contradiction_clause,[],[f153997]) ).
fof(f154003,plain,
( v6(sK54,bitIndex2)
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f152449,f151029]) ).
fof(f154004,plain,
( v154838(sK54,bitIndex2)
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f152448,f151029]) ).
fof(f154013,plain,
( ~ v154853(sK54,bitIndex2)
| spl55_1 ),
inference(resolution,[],[f151159,f145966]) ).
fof(f154017,plain,
( v154860(sK54)
| ~ v154853(sK54,bitIndex3)
| ~ spl55_3 ),
inference(resolution,[],[f151171,f145974]) ).
fof(f154018,plain,
( v154851(sK54)
| ~ v154852(sK54)
| ~ spl55_3 ),
inference(resolution,[],[f151171,f145963]) ).
fof(f154020,plain,
( ~ v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_1 ),
inference(resolution,[],[f154013,f145969]) ).
fof(f154021,plain,
( ~ range_3_0(bitIndex2)
| spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154020,f154003]) ).
fof(f154022,plain,
( $false
| spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154021,f151029]) ).
fof(f154023,plain,
( spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f154022]) ).
fof(f154025,plain,
( ~ v154852(sK54)
| ~ spl55_3
| spl55_4 ),
inference(forward_subsumption_resolution,[],[f154018,f151175]) ).
fof(f154037,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0) )
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f151688,f151257]) ).
fof(f154053,plain,
( ~ v154852(sK54)
| ~ v154862(sK54)
| spl55_6 ),
inference(resolution,[],[f151184,f145980]) ).
fof(f154055,plain,
( v154863(sK54)
| ~ v154853(sK54,bitIndex2)
| ~ spl55_7 ),
inference(resolution,[],[f151190,f145975]) ).
fof(f154093,plain,
( v83122(sK54,bitIndex1)
| ~ spl55_17 ),
inference(resolution,[],[f151283,f146264]) ).
fof(f154109,plain,
( ! [X0] :
( ~ range_3_0(X0)
| ~ b0010(X0)
| v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9
| ~ spl55_14 ),
inference(resolution,[],[f154037,f145969]) ).
fof(f154110,plain,
( ! [X0] :
( v154853(sK54,X0)
| ~ b0010(X0)
| ~ range_3_0(X0) )
| spl55_9
| ~ spl55_14 ),
inference(duplicate_literal_removal,[],[f154109]) ).
fof(f154141,plain,
( ~ v154842(sK54,bitIndex2)
| spl55_72 ),
inference(resolution,[],[f152115,f146266]) ).
fof(f154181,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(resolution,[],[f154110,f153987]) ).
fof(f154189,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(resolution,[],[f154110,f145978]) ).
fof(f154195,plain,
( ~ range_3_0(bitIndex1)
| v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154189,f146080]) ).
fof(f154196,plain,
( ~ range_3_0(bitIndex1)
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(forward_subsumption_resolution,[],[f154181,f146080]) ).
fof(f154198,plain,
( v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154195,f151028]) ).
fof(f154199,plain,
( $false
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(forward_subsumption_resolution,[],[f154196,f151028]) ).
fof(f154200,plain,
( spl55_9
| ~ spl55_14
| spl55_295 ),
inference(avatar_contradiction_clause,[],[f154199]) ).
fof(f154202,plain,
( $false
| spl55_1
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154198,f151161]) ).
fof(f154203,plain,
( spl55_1
| spl55_9
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f154202]) ).
fof(f154206,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_2
| ~ spl55_3 ),
inference(forward_subsumption_resolution,[],[f154017,f151236]) ).
fof(f154208,definition,
( spl55_301
<=> v154853(sK54,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl55_301])],[avatar_definition]) ).
fof(f154210,plain,
( ~ v154853(sK54,bitIndex2)
| spl55_301 ),
inference(avatar_component_clause,[],[f154208]) ).
fof(f154212,definition,
( spl55_302
<=> v154863(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_302])],[avatar_definition]) ).
fof(f154215,plain,
( ~ spl55_301
| spl55_302
| ~ spl55_7 ),
inference(avatar_split_clause,[],[f154055,f151189,f154212,f154208]) ).
fof(f154233,plain,
( v154853(sK54,bitIndex3)
| ~ spl55_3
| spl55_4 ),
inference(resolution,[],[f154025,f145970]) ).
fof(f154234,plain,
( $false
| spl55_2
| ~ spl55_3
| spl55_4 ),
inference(forward_subsumption_resolution,[],[f154233,f154206]) ).
fof(f154235,plain,
( spl55_2
| ~ spl55_3
| spl55_4 ),
inference(avatar_contradiction_clause,[],[f154234]) ).
fof(f154239,plain,
( ~ v154852(sK54)
| ~ spl55_5
| spl55_6 ),
inference(forward_subsumption_resolution,[],[f154053,f151180]) ).
fof(f154247,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v154839(sK54)
| ~ spl55_10 ),
inference(resolution,[],[f151213,f146011]) ).
fof(f154249,plain,
( ~ range_3_0(bitIndex3)
| ~ v154839(sK54)
| ~ spl55_10 ),
inference(forward_subsumption_resolution,[],[f154247,f146082]) ).
fof(f154250,plain,
( ~ v154839(sK54)
| ~ spl55_10 ),
inference(forward_subsumption_resolution,[],[f154249,f151030]) ).
fof(f154251,plain,
( $false
| ~ spl55_10
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154250,f151257]) ).
fof(f154252,plain,
( ~ spl55_10
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f154251]) ).
fof(f154253,plain,
( spl55_11
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f151617,f151208,f151218]) ).
fof(f154263,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ b0001(X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151210,f145983]) ).
fof(f154269,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ spl55_13
| ~ spl55_35 ),
inference(resolution,[],[f151251,f151471]) ).
fof(f154272,plain,
( b0001(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v154836(sK54)
| ~ spl55_13 ),
inference(resolution,[],[f151251,f145982]) ).
fof(f154274,plain,
( ~ range_3_0(bitIndex3)
| ~ v154836(sK54)
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154272,f145998]) ).
fof(f154275,plain,
( ~ range_3_0(bitIndex3)
| ~ spl55_13
| ~ spl55_35 ),
inference(forward_subsumption_resolution,[],[f154269,f146082]) ).
fof(f154276,plain,
( ~ v154836(sK54)
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154274,f151030]) ).
fof(f154277,plain,
( $false
| ~ spl55_13
| ~ spl55_35 ),
inference(forward_subsumption_resolution,[],[f154275,f151030]) ).
fof(f154278,plain,
( ~ spl55_13
| ~ spl55_35 ),
inference(avatar_contradiction_clause,[],[f154277]) ).
fof(f154279,plain,
( $false
| ~ spl55_9
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154276,f151210]) ).
fof(f154280,plain,
( ~ spl55_9
| ~ spl55_13 ),
inference(avatar_contradiction_clause,[],[f154279]) ).
fof(f154320,plain,
( ! [X0] :
( ~ b0001(X0)
| ~ range_3_0(X0)
| v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f154263,f145969]) ).
fof(f154321,plain,
( ! [X0] :
( v154853(sK54,X0)
| ~ range_3_0(X0)
| ~ b0001(X0) )
| ~ spl55_9 ),
inference(duplicate_literal_removal,[],[f154320]) ).
fof(f154334,plain,
( ~ v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_301 ),
inference(resolution,[],[f154210,f145969]) ).
fof(f154335,plain,
( ~ v6(sK54,bitIndex2)
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154334,f151029]) ).
fof(f154363,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v154870(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f154321,f145979]) ).
fof(f154370,plain,
( ~ b0001(bitIndex0)
| v154870(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154363,f151027]) ).
fof(f154371,plain,
( v154870(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154370,f145995]) ).
fof(f154372,plain,
( $false
| spl55_1
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154371,f151161]) ).
fof(f154373,plain,
( spl55_1
| ~ spl55_9 ),
inference(avatar_contradiction_clause,[],[f154372]) ).
fof(f154374,plain,
( ~ spl55_302
| spl55_5 ),
inference(avatar_split_clause,[],[f151202,f151179,f154212]) ).
fof(f154378,plain,
( ~ spl55_296
| spl55_5
| ~ spl55_8 ),
inference(avatar_split_clause,[],[f151271,f151193,f151179,f153989]) ).
fof(f154379,plain,
( ~ spl55_11
| spl55_5
| ~ spl55_8
| spl55_12 ),
inference(avatar_split_clause,[],[f151622,f151222,f151193,f151179,f151218]) ).
fof(f154380,plain,
( ~ spl55_14
| spl55_9
| spl55_12 ),
inference(avatar_split_clause,[],[f152111,f151222,f151208,f151255]) ).
fof(f154382,plain,
( v154844(sK54,bitIndex1)
| v1051(sK54)
| spl55_11
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f153972,f151028]) ).
fof(f154405,plain,
( v154841(sK54,bitIndex3)
| v154852(sK54)
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152602,f151030]) ).
fof(f154408,plain,
( v154844(sK54,bitIndex1)
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154382,f151280]) ).
fof(f154481,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151209,f145984]) ).
fof(f154498,plain,
( ! [X0] :
( v154838(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f154481,f145968]) ).
fof(f154499,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154838(sK54,X0) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f154498]) ).
fof(f154502,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154844(sK54,X0)
| ~ range_3_0(X0) )
| spl55_16 ),
inference(resolution,[],[f151280,f146089]) ).
fof(f154503,plain,
( ! [X0] :
( ~ v154844(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| spl55_16 ),
inference(resolution,[],[f151280,f146090]) ).
fof(f154541,plain,
( ~ v154841(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v1051(sK54)
| spl55_18 ),
inference(resolution,[],[f151289,f146089]) ).
fof(f154564,plain,
( ~ range_3_0(bitIndex0)
| v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(resolution,[],[f154499,f145972]) ).
fof(f154567,plain,
( v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f154564,f151027]) ).
fof(f154568,plain,
( v154838(sK54,bitIndex0)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f154567,f151224]) ).
fof(f154634,plain,
( ~ v154838(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| v154836(sK54)
| spl55_301 ),
inference(resolution,[],[f154335,f145985]) ).
fof(f154637,plain,
( ~ v154838(sK54,bitIndex2)
| v154836(sK54)
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154634,f151029]) ).
fof(f154638,plain,
( ~ v154838(sK54,bitIndex2)
| spl55_9
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154637,f151209]) ).
fof(f154762,plain,
( ! [X0] :
( v154844(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| spl55_16 ),
inference(resolution,[],[f154502,f146013]) ).
fof(f154763,plain,
( ! [X0] :
( v154844(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| v154839(sK54) )
| spl55_16 ),
inference(duplicate_literal_removal,[],[f154762]) ).
fof(f154766,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154844(sK54,X0) )
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f154763,f151256]) ).
fof(f154773,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154845(sK54)
| spl55_16 ),
inference(resolution,[],[f154503,f146272]) ).
fof(f154775,plain,
( v154841(sK54,bitIndex2)
| ~ v154845(sK54)
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f154773,f151029]) ).
fof(f154776,plain,
( v154841(sK54,bitIndex2)
| spl55_16
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f154775,f151425]) ).
fof(f154777,plain,
( spl55_73
| spl55_16
| spl55_18 ),
inference(avatar_split_clause,[],[f154776,f151287,f151278,f152117]) ).
fof(f154780,plain,
( $false
| spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154004,f154638]) ).
fof(f154781,plain,
( spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(avatar_contradiction_clause,[],[f154780]) ).
fof(f154838,plain,
( ~ v154843(sK54)
| ~ spl55_31 ),
inference(resolution,[],[f151431,f146793]) ).
fof(f154868,plain,
( v154844(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| v1051(sK54)
| ~ spl55_73 ),
inference(resolution,[],[f152119,f146089]) ).
fof(f155065,plain,
( ~ range_3_0(bitIndex0)
| v154844(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(resolution,[],[f154766,f154568]) ).
fof(f155073,plain,
( v154844(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f155065,f151027]) ).
fof(f155754,plain,
( ~ v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v1051(sK54)
| spl55_72 ),
inference(resolution,[],[f154141,f146087]) ).
fof(f155824,plain,
( ~ range_1_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(resolution,[],[f155073,f146273]) ).
fof(f155826,plain,
( $false
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f155824,f151042]) ).
fof(f155827,plain,
( spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(avatar_contradiction_clause,[],[f155826]) ).
fof(f155832,plain,
( v154852(sK54)
| spl55_15
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154405,f151261]) ).
fof(f155843,plain,
( $false
| ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f155832,f154239]) ).
fof(f155844,plain,
( ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(avatar_contradiction_clause,[],[f155843]) ).
fof(f155848,plain,
( ~ range_3_0(bitIndex3)
| v1051(sK54)
| ~ spl55_15
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f154541,f151260]) ).
fof(f155849,plain,
( v1051(sK54)
| ~ spl55_15
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f155848,f151030]) ).
fof(f155850,plain,
( $false
| ~ spl55_15
| spl55_16
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f155849,f151280]) ).
fof(f155851,plain,
( ~ spl55_15
| spl55_16
| spl55_18 ),
inference(avatar_contradiction_clause,[],[f155850]) ).
fof(f155858,plain,
( ~ range_3_0(bitIndex2)
| v1051(sK54)
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154868,f151968]) ).
fof(f155864,plain,
( v1051(sK54)
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155858,f151029]) ).
fof(f155871,plain,
( $false
| spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155864,f151280]) ).
fof(f155872,plain,
( spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f155871]) ).
fof(f155897,plain,
( v154842(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| ~ spl55_15 ),
inference(resolution,[],[f151260,f146087]) ).
fof(f156766,plain,
( ~ range_1_0(bitIndex1)
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(resolution,[],[f154408,f146273]) ).
fof(f156768,plain,
( $false
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f156766,f151043]) ).
fof(f156769,plain,
( spl55_11
| spl55_16
| ~ spl55_45 ),
inference(avatar_contradiction_clause,[],[f156768]) ).
fof(f156780,plain,
( ~ range_3_0(bitIndex2)
| ~ v1051(sK54)
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155754,f152119]) ).
fof(f156786,plain,
( ~ v1051(sK54)
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f156780,f151029]) ).
fof(f156787,plain,
( $false
| ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f156786,f151279]) ).
fof(f156788,plain,
( ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f156787]) ).
fof(f156789,plain,
( $false
| ~ spl55_31
| ~ spl55_72 ),
inference(forward_subsumption_resolution,[],[f154838,f152114]) ).
fof(f156790,plain,
( ~ spl55_31
| ~ spl55_72 ),
inference(avatar_contradiction_clause,[],[f156789]) ).
fof(f156808,plain,
( $false
| ~ spl55_17
| spl55_31 ),
inference(forward_subsumption_resolution,[],[f154093,f151430]) ).
fof(f156809,plain,
( ~ spl55_17
| spl55_31 ),
inference(avatar_contradiction_clause,[],[f156808]) ).
fof(f156822,plain,
( ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| ~ spl55_15
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f155897,f151284]) ).
fof(f156824,plain,
( ~ v1051(sK54)
| ~ spl55_15
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f156822,f151030]) ).
fof(f156825,plain,
( $false
| ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f156824,f151279]) ).
fof(f156826,plain,
( ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(avatar_contradiction_clause,[],[f156825]) ).
cnf(s1,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(sat_conversion,[],[f151157]) ).
cnf(s4,plain,
( spl55_3
| ~ spl55_7
| ~ spl55_8 ),
inference(sat_conversion,[],[f151196]) ).
cnf(s6,plain,
( spl55_1
| spl55_9
| ~ spl55_10 ),
inference(sat_conversion,[],[f151215]) ).
cnf(s7,plain,
( spl55_7
| ~ spl55_11
| ~ spl55_12 ),
inference(sat_conversion,[],[f151225]) ).
cnf(s9,plain,
( spl55_2
| ~ spl55_4 ),
inference(sat_conversion,[],[f151234]) ).
cnf(s10,plain,
( spl55_2
| ~ spl55_6 ),
inference(sat_conversion,[],[f151237]) ).
cnf(s11,plain,
( spl55_9
| spl55_10
| ~ spl55_13 ),
inference(sat_conversion,[],[f151253]) ).
cnf(s12,plain,
( spl55_10
| spl55_14
| ~ spl55_15 ),
inference(sat_conversion,[],[f151262]) ).
cnf(s13,plain,
( spl55_15
| ~ spl55_16
| ~ spl55_17 ),
inference(sat_conversion,[],[f151285]) ).
cnf(s14,plain,
( spl55_15
| spl55_16
| ~ spl55_18 ),
inference(sat_conversion,[],[f151290]) ).
cnf(s19,plain,
( spl55_5
| ~ spl55_8
| spl55_11
| ~ spl55_12 ),
inference(sat_conversion,[],[f151340]) ).
cnf(s26,plain,
( spl55_9
| ~ spl55_14
| spl55_35 ),
inference(sat_conversion,[],[f151472]) ).
cnf(s32,plain,
( spl55_17
| ~ spl55_31 ),
inference(sat_conversion,[],[f151551]) ).
cnf(s33,plain,
( spl55_9
| spl55_14
| spl55_45 ),
inference(sat_conversion,[],[f151565]) ).
cnf(s43,plain,
( ~ spl55_5
| spl55_6
| spl55_13 ),
inference(sat_conversion,[],[f151639]) ).
cnf(s47,plain,
( spl55_8
| ~ spl55_9 ),
inference(sat_conversion,[],[f151653]) ).
cnf(s83,plain,
( ~ spl55_16
| ~ spl55_72
| spl55_73 ),
inference(sat_conversion,[],[f152120]) ).
cnf(s84,plain,
( spl55_8
| ~ spl55_45
| spl55_73 ),
inference(sat_conversion,[],[f152121]) ).
cnf(s88,plain,
( spl55_8
| spl55_9
| ~ spl55_14 ),
inference(sat_conversion,[],[f152129]) ).
cnf(s100,plain,
( spl55_31
| spl55_72 ),
inference(sat_conversion,[],[f152152]) ).
cnf(s197,plain,
( spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(sat_conversion,[],[f153720]) ).
cnf(s219,plain,
( spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(sat_conversion,[],[f153983]) ).
cnf(s220,plain,
( ~ spl55_12
| ~ spl55_295
| spl55_296 ),
inference(sat_conversion,[],[f153992]) ).
cnf(s222,plain,
( spl55_5
| ~ spl55_7
| spl55_8 ),
inference(sat_conversion,[],[f153998]) ).
cnf(s225,plain,
( spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(sat_conversion,[],[f154023]) ).
cnf(s239,plain,
( spl55_9
| ~ spl55_14
| spl55_295 ),
inference(sat_conversion,[],[f154200]) ).
cnf(s240,plain,
( spl55_1
| spl55_9
| ~ spl55_14 ),
inference(sat_conversion,[],[f154203]) ).
cnf(s244,plain,
( ~ spl55_7
| ~ spl55_301
| spl55_302 ),
inference(sat_conversion,[],[f154215]) ).
cnf(s246,plain,
( spl55_2
| ~ spl55_3
| spl55_4 ),
inference(sat_conversion,[],[f154235]) ).
cnf(s247,plain,
( ~ spl55_10
| ~ spl55_14 ),
inference(sat_conversion,[],[f154252]) ).
cnf(s249,plain,
( ~ spl55_9
| spl55_11 ),
inference(sat_conversion,[],[f154253]) ).
cnf(s251,plain,
( ~ spl55_13
| ~ spl55_35 ),
inference(sat_conversion,[],[f154278]) ).
cnf(s252,plain,
( ~ spl55_9
| ~ spl55_13 ),
inference(sat_conversion,[],[f154280]) ).
cnf(s255,plain,
( spl55_1
| ~ spl55_9 ),
inference(sat_conversion,[],[f154373]) ).
cnf(s263,plain,
( spl55_5
| ~ spl55_302 ),
inference(sat_conversion,[],[f154374]) ).
cnf(s267,plain,
( spl55_5
| ~ spl55_8
| ~ spl55_296 ),
inference(sat_conversion,[],[f154378]) ).
cnf(s268,plain,
( spl55_5
| ~ spl55_8
| ~ spl55_11
| spl55_12 ),
inference(sat_conversion,[],[f154379]) ).
cnf(s271,plain,
( spl55_9
| spl55_12
| ~ spl55_14 ),
inference(sat_conversion,[],[f154380]) ).
cnf(s319,plain,
( spl55_16
| spl55_18
| spl55_73 ),
inference(sat_conversion,[],[f154777]) ).
cnf(s321,plain,
( spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(sat_conversion,[],[f154781]) ).
cnf(s431,plain,
( spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(sat_conversion,[],[f155827]) ).
cnf(s436,plain,
( ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(sat_conversion,[],[f155844]) ).
cnf(s438,plain,
( ~ spl55_15
| spl55_16
| spl55_18 ),
inference(sat_conversion,[],[f155851]) ).
cnf(s445,plain,
( spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(sat_conversion,[],[f155872]) ).
cnf(s510,plain,
( spl55_11
| spl55_16
| ~ spl55_45 ),
inference(sat_conversion,[],[f156769]) ).
cnf(s514,plain,
( ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(sat_conversion,[],[f156788]) ).
cnf(s515,plain,
( ~ spl55_31
| ~ spl55_72 ),
inference(sat_conversion,[],[f156790]) ).
cnf(s526,plain,
( ~ spl55_17
| spl55_31 ),
inference(sat_conversion,[],[f156809]) ).
cnf(s529,plain,
( ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(sat_conversion,[],[f156826]) ).
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(f156827,plain,
$false,
inference(avatar_sat_refutation,[],[s585]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV124+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.12 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.46 % Computer : n009.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 27 11:42:30 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.55 Running first-order theorem proving
% 0.24/0.55 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
% 28.58/8.29 % (1892484)Detected formulas, will run a generic FOF schedule.
% 28.58/8.29 % (1892503)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=3699659390:i=141695:sd=1:nm=32:gsp=on:ss=included_2964 on theBenchmark for (2964ds/141695Mi)
% 28.58/8.29 % (1892501)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=546676331:i=141193_2964 on theBenchmark for (2964ds/141193Mi)
% 28.58/8.29 % (1892504)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3535176406:i=109:sd=1:ins=1:gsp=on:ss=axioms_2964 on theBenchmark for (2964ds/109Mi)
% 28.58/8.29 % (1892505)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2797265442:i=119:av=off:ss=axioms_2964 on theBenchmark for (2964ds/119Mi)
% 28.58/8.29 % (1892507)dis-21_1_sil=8000:lcm=predicate:random_seed=2234312244:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2964 on theBenchmark for (2964ds/129Mi)
% 28.58/8.29 % (1892506)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1698752559:s2a=on:i=139:gtg=position_2964 on theBenchmark for (2964ds/139Mi)
% 28.58/8.29 % (1892502)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=2175131226:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2964 on theBenchmark for (2964ds/134677Mi)
% 28.58/8.29 % (1892504)Instruction limit reached!
% 28.58/8.29 % (1892504)------------------------------
% 28.58/8.29 % (1892504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.58/8.29 % (1892504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.58/8.29 % (1892504)CaDiCaL version: 2.1.3
% 28.58/8.29 % (1892504)Termination reason: Instruction limit
% 28.58/8.29 % (1892504)Termination phase: SInE selection
% 28.58/8.29 % (1892504)Time elapsed: 0.104 s
% 28.58/8.29 % (1892504)Peak memory usage: 205 MB
% 28.58/8.29 % (1892504)Instructions burned: 110 (million)
% 28.58/8.29 % (1892505)Instruction limit reached!
% 28.58/8.29 % (1892505)------------------------------
% 28.58/8.29 % (1892505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.58/8.29 % (1892505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.58/8.29 % (1892505)CaDiCaL version: 2.1.3
% 28.58/8.29 % (1892505)Termination reason: Instruction limit
% 28.58/8.29 % (1892505)Termination phase: SInE selection
% 28.58/8.29 % (1892505)Time elapsed: 0.111 s
% 28.58/8.29 % (1892505)Peak memory usage: 205 MB
% 28.58/8.29 % (1892505)Instructions burned: 119 (million)
% 28.58/8.29 % (1892507)Instruction limit reached!
% 28.58/8.29 % (1892507)------------------------------
% 28.58/8.29 % (1892507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.58/8.29 % (1892507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.58/8.29 % (1892507)CaDiCaL version: 2.1.3
% 28.58/8.29 % (1892507)Termination reason: Instruction limit
% 28.58/8.29 % (1892507)Termination phase: SInE selection
% 28.58/8.29 % (1892507)Time elapsed: 0.154 s
% 28.58/8.29 % (1892507)Peak memory usage: 205 MB
% 28.58/8.29 % (1892507)Instructions burned: 134 (million)
% 28.58/8.29 % (1892506)Instruction limit reached!
% 28.58/8.29 % (1892506)------------------------------
% 28.58/8.29 % (1892506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.58/8.29 % (1892506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.58/8.29 % (1892506)CaDiCaL version: 2.1.3
% 28.58/8.29 % (1892506)Termination reason: Instruction limit
% 28.58/8.29 % (1892506)Termination phase: Property scanning
% 28.58/8.29 % (1892506)Time elapsed: 0.181 s
% 28.58/8.29 % (1892506)Peak memory usage: 206 MB
% 28.58/8.29 % (1892506)Instructions burned: 139 (million)
% 28.58/8.29 % (1892515)lrs+10_1_sil=8000:sp=occurrence:random_seed=3265984197:i=285:sd=3:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/285Mi)
% 28.58/8.29 % (1892516)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2138817318:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2960 on theBenchmark for (2960ds/157Mi)
% 28.58/8.29 % (1892518)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=990650231:s2a=on:i=248:s2at=1.23:gtg=position_2959 on theBenchmark for (2959ds/248Mi)
% 28.58/8.29 % (1892517)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1265685590:i=325:sd=1:ss=axioms:sgt=32_2959 on theBenchmark for (2959ds/325Mi)
% 28.58/8.29 % (1892516)Instruction limit reached!
% 39.56/9.81 % (1892516)------------------------------
% 39.56/9.81 % (1892516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892516)CaDiCaL version: 2.1.3
% 39.56/9.81 % (1892516)Termination reason: Instruction limit
% 39.56/9.81 % (1892516)Termination phase: Property scanning
% 39.56/9.81 % (1892516)Time elapsed: 0.192 s
% 39.56/9.81 % (1892516)Peak memory usage: 206 MB
% 39.56/9.81 % (1892516)Instructions burned: 159 (million)
% 39.56/9.81 % (1892515)Instruction limit reached!
% 39.56/9.81 % (1892515)------------------------------
% 39.56/9.81 % (1892515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892515)CaDiCaL version: 2.1.3
% 39.56/9.81 % (1892515)Termination reason: Instruction limit
% 39.56/9.81 % (1892515)Termination phase: SInE selection
% 39.56/9.81 % (1892515)Time elapsed: 0.226 s
% 39.56/9.81 % (1892515)Peak memory usage: 205 MB
% 39.56/9.81 % (1892515)Instructions burned: 286 (million)
% 39.56/9.81 % (1892518)Instruction limit reached!
% 39.56/9.81 % (1892518)------------------------------
% 39.56/9.81 % (1892518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892518)CaDiCaL version: 2.1.3
% 39.56/9.81 % (1892518)Termination reason: Instruction limit
% 39.56/9.81 % (1892518)Termination phase: Property scanning
% 39.56/9.81 % (1892518)Time elapsed: 0.244 s
% 39.56/9.81 % (1892518)Peak memory usage: 206 MB
% 39.56/9.81 % (1892518)Instructions burned: 249 (million)
% 39.56/9.81 % (1892517)Instruction limit reached!
% 39.56/9.81 % (1892517)------------------------------
% 39.56/9.81 % (1892517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892517)CaDiCaL version: 2.1.3
% 39.56/9.81 % (1892517)Termination reason: Instruction limit
% 39.56/9.81 % (1892517)Termination phase: SInE selection
% 39.56/9.81 % (1892517)Time elapsed: 0.263 s
% 39.56/9.81 % (1892517)Peak memory usage: 205 MB
% 39.56/9.81 % (1892517)Instructions burned: 326 (million)
% 39.56/9.81 % (1892524)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2430262185:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2955 on theBenchmark for (2955ds/294Mi)
% 39.56/9.81 % (1892525)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3502066728:i=2350_2955 on theBenchmark for (2955ds/2350Mi)
% 39.56/9.81 % (1892527)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3432562597:cts=off:i=113:fsr=off:ss=included:sgt=4_2954 on theBenchmark for (2954ds/113Mi)
% 39.56/9.81 % (1892524)Instruction limit reached!
% 39.56/9.81 % (1892524)------------------------------
% 39.56/9.81 % (1892524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892524)CaDiCaL version: 2.1.3
% 39.56/9.81 % (1892524)Termination reason: Instruction limit
% 39.56/9.81 % (1892524)Termination phase: SInE selection
% 39.56/9.81 % (1892524)Time elapsed: 0.235 s
% 39.56/9.81 % (1892524)Peak memory usage: 205 MB
% 39.56/9.81 % (1892524)Instructions burned: 295 (million)
% 39.56/9.81 % (1892528)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4103604089:i=127:av=off:fsr=off:sup=off_2954 on theBenchmark for (2954ds/127Mi)
% 39.56/9.81 % (1892527)Instruction limit reached!
% 39.56/9.81 % (1892527)------------------------------
% 39.56/9.81 % (1892527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892527)CaDiCaL version: 2.1.3
% 39.56/9.81 % (1892527)Termination reason: Instruction limit
% 39.56/9.81 % (1892527)Termination phase: SInE selection
% 39.56/9.81 % (1892527)Time elapsed: 0.116 s
% 39.56/9.81 % (1892527)Peak memory usage: 205 MB
% 39.56/9.81 % (1892527)Instructions burned: 114 (million)
% 39.56/9.81 % (1892528)Instruction limit reached!
% 39.56/9.81 % (1892528)------------------------------
% 39.56/9.81 % (1892528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.56/9.81 % (1892528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.56/9.81 % (1892528)CaDiCaL version: 2.1.3
% 41.69/10.11 % (1892528)Termination reason: Instruction limit
% 41.69/10.11 % (1892528)Termination phase: Preprocessing 1
% 41.69/10.11 % (1892528)Time elapsed: 0.180 s
% 41.69/10.11 % (1892528)Peak memory usage: 206 MB
% 41.69/10.11 % (1892528)Instructions burned: 127 (million)
% 41.69/10.11 % (1892533)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=721981355:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2951 on theBenchmark for (2951ds/114Mi)
% 41.69/10.11 % (1892534)lrs+10_1_sil=8000:sp=occurrence:random_seed=81750530:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2950 on theBenchmark for (2950ds/907Mi)
% 41.69/10.11 % (1892533)Instruction limit reached!
% 41.69/10.11 % (1892533)------------------------------
% 41.69/10.11 % (1892533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.69/10.11 % (1892533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.69/10.11 % (1892533)CaDiCaL version: 2.1.3
% 41.69/10.11 % (1892533)Termination reason: Instruction limit
% 41.69/10.11 % (1892533)Termination phase: Property scanning
% 41.69/10.11 % (1892533)Time elapsed: 0.147 s
% 41.69/10.11 % (1892533)Peak memory usage: 206 MB
% 41.69/10.11 % (1892533)Instructions burned: 115 (million)
% 41.69/10.11 % (1892535)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2716918700:i=437:sd=1:aac=none:ss=included_2949 on theBenchmark for (2949ds/437Mi)
% 41.69/10.11 % (1892538)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3299506747:i=5202:ss=axioms:sgt=16_2947 on theBenchmark for (2947ds/5202Mi)
% 41.69/10.11 % (1892535)Instruction limit reached!
% 41.69/10.11 % (1892535)------------------------------
% 41.69/10.11 % (1892535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.69/10.11 % (1892535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.69/10.11 % (1892535)CaDiCaL version: 2.1.3
% 41.69/10.11 % (1892535)Termination reason: Instruction limit
% 41.69/10.11 % (1892535)Termination phase: SInE selection
% 41.69/10.11 % (1892535)Time elapsed: 0.357 s
% 41.69/10.11 % (1892535)Peak memory usage: 212 MB
% 41.69/10.11 % (1892535)Instructions burned: 438 (million)
% 41.69/10.11 % (1892534)Instruction limit reached!
% 41.69/10.11 % (1892534)------------------------------
% 41.69/10.11 % (1892534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.69/10.11 % (1892534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.69/10.11 % (1892534)CaDiCaL version: 2.1.3
% 41.69/10.11 % (1892534)Termination reason: Instruction limit
% 41.69/10.11 % (1892534)Termination phase: Saturation
% 41.69/10.11 % (1892534)Time elapsed: 0.812 s
% 41.69/10.11 % (1892534)Peak memory usage: 260 MB
% 41.69/10.11 % (1892534)Instructions burned: 908 (million)
% 41.69/10.11 % (1892543)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2188881601:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2942 on theBenchmark for (2942ds/134Mi)
% 41.69/10.11 % (1892543)Instruction limit reached!
% 41.69/10.11 % (1892543)------------------------------
% 41.69/10.11 % (1892543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.69/10.11 % (1892543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.69/10.11 % (1892543)CaDiCaL version: 2.1.3
% 41.69/10.11 % (1892543)Termination reason: Instruction limit
% 41.69/10.11 % (1892543)Termination phase: SInE selection
% 41.69/10.11 % (1892543)Time elapsed: 0.137 s
% 41.69/10.11 % (1892543)Peak memory usage: 205 MB
% 41.69/10.11 % (1892543)Instructions burned: 134 (million)
% 41.69/10.11 % (1892545)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1598317386:st=8:i=592:sd=3:ep=RST:ss=axioms_2939 on theBenchmark for (2939ds/592Mi)
% 41.69/10.11 % (1892546)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2983383850:st=3:i=13193:sd=3:ss=axioms_2937 on theBenchmark for (2937ds/13193Mi)
% 41.69/10.11 % (1892545)Instruction limit reached!
% 41.69/10.11 % (1892545)------------------------------
% 41.69/10.11 % (1892545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.69/10.11 % (1892545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.69/10.11 % (1892545)CaDiCaL version: 2.1.3
% 41.69/10.11 % (1892545)Termination reason: Instruction limit
% 41.69/10.11 % (1892545)Termination phase: SInE selection
% 41.69/10.11 % (1892545)Time elapsed: 0.401 s
% 41.69/10.11 % (1892545)Peak memory usage: 207 MB
% 41.69/10.11 % (1892545)Instructions burned: 593 (million)
% 41.69/10.11 % (1892549)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=2815794105:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2932 on theBenchmark for (2932ds/125Mi)
% 74.70/14.72 % (1892525)Instruction limit reached!
% 74.70/14.72 % (1892525)------------------------------
% 74.70/14.72 % (1892525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.70/14.72 % (1892525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.70/14.72 % (1892525)CaDiCaL version: 2.1.3
% 74.70/14.72 % (1892525)Termination reason: Instruction limit
% 74.70/14.72 % (1892525)Termination phase: Preprocessing 3
% 74.70/14.72 % (1892525)Time elapsed: 2.421 s
% 74.70/14.72 % (1892525)Peak memory usage: 283 MB
% 74.70/14.72 % (1892525)Instructions burned: 2350 (million)
% 74.70/14.72 % (1892549)Instruction limit reached!
% 74.70/14.72 % (1892549)------------------------------
% 74.70/14.72 % (1892549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.70/14.72 % (1892549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.70/14.72 % (1892549)CaDiCaL version: 2.1.3
% 74.70/14.72 % (1892549)Termination reason: Instruction limit
% 74.70/14.72 % (1892549)Termination phase: Property scanning
% 74.70/14.72 % (1892549)Time elapsed: 0.162 s
% 74.70/14.72 % (1892549)Peak memory usage: 206 MB
% 74.70/14.72 % (1892549)Instructions burned: 125 (million)
% 74.70/14.72 % (1892551)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=106580040:i=134:gtgl=5:slsql=off:gtg=exists_sym_2927 on theBenchmark for (2927ds/134Mi)
% 74.70/14.72 % (1892552)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1347116678:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2926 on theBenchmark for (2926ds/141Mi)
% 74.70/14.72 % (1892551)Instruction limit reached!
% 74.70/14.72 % (1892551)------------------------------
% 74.70/14.72 % (1892551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.70/14.72 % (1892551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.70/14.72 % (1892551)CaDiCaL version: 2.1.3
% 74.70/14.72 % (1892551)Termination reason: Instruction limit
% 74.70/14.72 % (1892551)Termination phase: Property scanning
% 74.70/14.72 % (1892551)Time elapsed: 0.174 s
% 74.70/14.72 % (1892551)Peak memory usage: 206 MB
% 74.70/14.72 % (1892551)Instructions burned: 134 (million)
% 74.70/14.72 % (1892552)Instruction limit reached!
% 74.70/14.72 % (1892552)------------------------------
% 74.70/14.72 % (1892552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.70/14.72 % (1892552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.70/14.72 % (1892552)CaDiCaL version: 2.1.3
% 74.70/14.72 % (1892552)Termination reason: Instruction limit
% 74.70/14.72 % (1892552)Termination phase: SInE selection
% 74.70/14.72 % (1892552)Time elapsed: 0.134 s
% 74.70/14.72 % (1892552)Peak memory usage: 205 MB
% 74.70/14.72 % (1892552)Instructions burned: 141 (million)
% 74.70/14.72 % (1892555)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=126750483:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2923 on theBenchmark for (2923ds/431Mi)
% 74.70/14.72 % (1892556)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=3540655155:i=6060:aac=none:ins=25_2922 on theBenchmark for (2922ds/6060Mi)
% 74.70/14.72 % (1892555)Instruction limit reached!
% 74.70/14.72 % (1892555)------------------------------
% 74.70/14.72 % (1892555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.70/14.72 % (1892555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.70/14.72 % (1892555)CaDiCaL version: 2.1.3
% 74.70/14.72 % (1892555)Termination reason: Instruction limit
% 74.70/14.72 % (1892555)Termination phase: SInE selection
% 74.70/14.72 % (1892555)Time elapsed: 0.323 s
% 74.70/14.72 % (1892555)Peak memory usage: 207 MB
% 74.70/14.72 % (1892555)Instructions burned: 431 (million)
% 74.70/14.72 % (1892559)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=3224824824:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2917 on theBenchmark for (2917ds/150Mi)
% 74.70/14.72 [W927 11:42:39.540488118 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.
% 74.70/14.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 74.70/14.72 [W927 11:42:39.540622823 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540706620 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540761287 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540817377 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540834918 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540879301 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540896175 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540938832 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540955742 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.540998692 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 [W927 11:42:39.541028452 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.
% 145.68/24.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 145.68/24.75 % (1892559)Instruction limit reached!
% 145.68/24.75 % (1892559)------------------------------
% 145.68/24.75 % (1892559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 145.68/24.75 % (1892559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.68/24.75 % (1892559)CaDiCaL version: 2.1.3
% 145.68/24.75 % (1892559)Termination reason: Instruction limit
% 145.68/24.75 % (1892559)Termination phase: SInE selection
% 145.68/24.75 % (1892559)Time elapsed: 0.139 s
% 145.68/24.75 % (1892559)Peak memory usage: 205 MB
% 145.68/24.75 % (1892559)Instructions burned: 150 (million)
% 145.68/24.75 % (1892561)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3134405485:i=14155:bd=all_2913 on theBenchmark for (2913ds/14155Mi)
% 182.58/29.93 % (1892538)Instruction limit reached!
% 182.58/29.93 % (1892538)------------------------------
% 182.58/29.93 % (1892538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.58/29.93 % (1892538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.58/29.93 % (1892538)CaDiCaL version: 2.1.3
% 182.58/29.93 % (1892538)Termination reason: Instruction limit
% 182.58/29.93 % (1892538)Termination phase: Saturation
% 182.58/29.93 % (1892538)Time elapsed: 4.888 s
% 182.58/29.93 % (1892538)Peak memory usage: 333 MB
% 182.58/29.93 % (1892538)Instructions burned: 5202 (million)
% 182.58/29.93 % (1892569)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1128962023:i=667:av=off:fsr=off_2895 on theBenchmark for (2895ds/667Mi)
% 182.58/29.93 % (1892546)Refutation not found, incomplete strategy
% 182.58/29.93 % (1892546)------------------------------
% 182.58/29.93 % (1892546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.58/29.93 % (1892546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.58/29.93 % (1892546)CaDiCaL version: 2.1.3
% 182.58/29.93 % (1892546)Termination reason: Refutation not found, incomplete strategy
% 182.58/29.93 % (1892546)Time elapsed: 4.772 s
% 182.58/29.93 % (1892546)Peak memory usage: 347 MB
% 182.58/29.93 % (1892546)Instructions burned: 4905 (million)
% 182.58/29.93 % (1892569)Instruction limit reached!
% 182.58/29.93 % (1892569)------------------------------
% 182.58/29.93 % (1892569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.58/29.93 % (1892569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.58/29.93 % (1892569)CaDiCaL version: 2.1.3
% 182.58/29.93 % (1892569)Termination reason: Instruction limit
% 182.58/29.93 % (1892569)Termination phase: Preprocessing 2
% 182.58/29.93 % (1892569)Time elapsed: 0.850 s
% 182.58/29.93 % (1892569)Peak memory usage: 257 MB
% 182.58/29.93 % (1892569)Instructions burned: 667 (million)
% 182.58/29.93 % (1892546)------------------------------
% 182.58/29.93 % (1892546)------------------------------
% 182.58/29.93 % (1892575)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=1700322724:s2a=on:i=185:s2at=1.8:fdi=4_2883 on theBenchmark for (2883ds/185Mi)
% 182.58/29.93 % (1892576)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1110788544:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2882 on theBenchmark for (2882ds/193Mi)
% 182.58/29.93 % (1892575)Instruction limit reached!
% 182.58/29.93 % (1892575)------------------------------
% 182.58/29.93 % (1892575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.58/29.93 % (1892575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.58/29.93 % (1892575)CaDiCaL version: 2.1.3
% 182.58/29.93 % (1892575)Termination reason: Instruction limit
% 182.58/29.93 % (1892575)Termination phase: SInE selection
% 182.58/29.93 % (1892575)Time elapsed: 0.166 s
% 182.58/29.93 % (1892575)Peak memory usage: 205 MB
% 182.58/29.93 % (1892575)Instructions burned: 186 (million)
% 182.58/29.93 % (1892576)Instruction limit reached!
% 182.58/29.93 % (1892576)------------------------------
% 182.58/29.93 % (1892576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.58/29.93 % (1892576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.58/29.93 % (1892576)CaDiCaL version: 2.1.3
% 182.58/29.93 % (1892576)Termination reason: Instruction limit
% 182.58/29.93 % (1892576)Termination phase: SInE selection
% 182.58/29.93 % (1892576)Time elapsed: 0.171 s
% 182.58/29.93 % (1892576)Peak memory usage: 205 MB
% 182.58/29.93 % (1892576)Instructions burned: 193 (million)
% 182.58/29.93 % (1892579)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3294707041:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2878 on theBenchmark for (2878ds/4850Mi)
% 182.58/29.93 % (1892580)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=722150623:i=12111:sd=1:ss=included_2876 on theBenchmark for (2876ds/12111Mi)
% 182.58/29.93 % (1892556)Instruction limit reached!
% 182.58/29.93 % (1892556)------------------------------
% 182.58/29.93 % (1892556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.58/29.93 % (1892556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.58/29.93 % (1892556)CaDiCaL version: 2.1.3
% 182.58/29.93 % (1892556)Termination reason: Instruction limit
% 182.58/29.93 % (1892556)Termination phase: Property scanning
% 199.50/32.31 % (1892556)Time elapsed: 5.553 s
% 199.50/32.31 % (1892556)Peak memory usage: 357 MB
% 199.50/32.31 % (1892556)Instructions burned: 6061 (million)
% 199.50/32.31 % (1892587)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=823804844:i=319:kws=precedence:fsr=off_2863 on theBenchmark for (2863ds/319Mi)
% 199.50/32.31 % (1892587)Instruction limit reached!
% 199.50/32.31 % (1892587)------------------------------
% 199.50/32.31 % (1892587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.50/32.31 % (1892587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.50/32.31 % (1892587)CaDiCaL version: 2.1.3
% 199.50/32.31 % (1892587)Termination reason: Instruction limit
% 199.50/32.31 % (1892587)Termination phase: Preprocessing 1
% 199.50/32.31 % (1892587)Time elapsed: 0.390 s
% 199.50/32.31 % (1892587)Peak memory usage: 206 MB
% 199.50/32.31 % (1892587)Instructions burned: 319 (million)
% 199.50/32.31 % (1892590)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=623998424:i=2064:ep=RST_2856 on theBenchmark for (2856ds/2064Mi)
% 199.50/32.31 % (1892590)Instruction limit reached!
% 199.50/32.31 % (1892590)------------------------------
% 199.50/32.31 % (1892590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.50/32.31 % (1892590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.50/32.31 % (1892590)CaDiCaL version: 2.1.3
% 199.50/32.31 % (1892590)Termination reason: Instruction limit
% 199.50/32.31 % (1892590)Termination phase: Preprocessing 3
% 199.50/32.31 % (1892590)Time elapsed: 2.194 s
% 199.50/32.31 % (1892590)Peak memory usage: 318 MB
% 199.50/32.31 % (1892590)Instructions burned: 2065 (million)
% 199.50/32.31 % (1892579)Instruction limit reached!
% 199.50/32.31 % (1892579)------------------------------
% 199.50/32.31 % (1892579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.50/32.31 % (1892579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.50/32.31 % (1892579)CaDiCaL version: 2.1.3
% 199.50/32.31 % (1892579)Termination reason: Instruction limit
% 199.50/32.31 % (1892579)Termination phase: Property scanning
% 199.50/32.31 % (1892579)Time elapsed: 4.678 s
% 199.50/32.31 % (1892579)Peak memory usage: 392 MB
% 199.50/32.31 % (1892579)Instructions burned: 4851 (million)
% 199.50/32.31 % (1892597)dis-1011_128_sil=32000:random_seed=598599811:i=3706:ep=RST:av=off_2831 on theBenchmark for (2831ds/3706Mi)
% 199.50/32.31 % (1892598)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3043585795:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2828 on theBenchmark for (2828ds/757Mi)
% 199.50/32.31 % (1892598)Refutation not found, incomplete strategy
% 199.50/32.31 % (1892598)------------------------------
% 199.50/32.31 % (1892598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.50/32.31 % (1892598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.50/32.31 % (1892598)CaDiCaL version: 2.1.3
% 199.50/32.31 % (1892598)Termination reason: Refutation not found, incomplete strategy
% 199.50/32.31 % (1892598)Time elapsed: 0.679 s
% 199.50/32.31 % (1892598)Peak memory usage: 260 MB
% 199.50/32.31 % (1892598)Instructions burned: 749 (million)
% 199.50/32.31 % (1892598)------------------------------
% 199.50/32.31 % (1892598)------------------------------
% 199.50/32.31 % (1892601)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3369886069:i=13913:ss=axioms:sgt=8_2813 on theBenchmark for (2813ds/13913Mi)
% 199.50/32.31 % (1892597)Instruction limit reached!
% 199.50/32.31 % (1892597)------------------------------
% 199.50/32.31 % (1892597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.50/32.31 % (1892597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.50/32.31 % (1892597)CaDiCaL version: 2.1.3
% 199.50/32.31 % (1892597)Termination reason: Instruction limit
% 199.50/32.31 % (1892597)Termination phase: Property scanning
% 199.50/32.31 % (1892597)Time elapsed: 3.855 s
% 199.50/32.31 % (1892597)Peak memory usage: 392 MB
% 199.50/32.31 % (1892597)Instructions burned: 3706 (million)
% 199.50/32.31 % (1892605)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2035174341:i=9925:aac=none_2789 on theBenchmark for (2789ds/9925Mi)
% 199.50/32.31 % (1892601)Refutation not found, incomplete strategy
% 199.50/32.31 % (1892601)------------------------------
% 199.50/32.31 % (1892601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 199.50/32.31 % (1892601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 199.50/32.31 % (1892601)CaDiCaL version: 2.1.3
% 223.01/35.67 % (1892601)Termination reason: Refutation not found, incomplete strategy
% 223.01/35.67 % (1892601)Time elapsed: 4.597 s
% 223.01/35.67 % (1892601)Peak memory usage: 545 MB
% 223.01/35.67 % (1892601)Instructions burned: 4467 (million)
% 223.01/35.67 % (1892601)------------------------------
% 223.01/35.67 % (1892601)------------------------------
% 223.01/35.67 % (1892613)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4108222084:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2758 on theBenchmark for (2758ds/2479Mi)
% 223.01/35.67 % (1892613)Refutation not found, incomplete strategy
% 223.01/35.67 % (1892613)------------------------------
% 223.01/35.67 % (1892613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 223.01/35.67 % (1892613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.01/35.67 % (1892613)CaDiCaL version: 2.1.3
% 223.01/35.67 % (1892613)Termination reason: Refutation not found, incomplete strategy
% 223.01/35.67 % (1892613)Time elapsed: 1.289 s
% 223.01/35.67 % (1892613)Peak memory usage: 259 MB
% 223.01/35.67 % (1892613)Instructions burned: 1680 (million)
% 223.01/35.67 % (1892613)------------------------------
% 223.01/35.67 % (1892613)------------------------------
% 223.01/35.67 % (1892619)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=2290890434:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2737 on theBenchmark for (2737ds/440Mi)
% 223.01/35.67 % (1892619)Instruction limit reached!
% 223.01/35.67 % (1892619)------------------------------
% 223.01/35.67 % (1892619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 223.01/35.67 % (1892619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.01/35.67 % (1892619)CaDiCaL version: 2.1.3
% 223.01/35.67 % (1892619)Termination reason: Instruction limit
% 223.01/35.67 % (1892619)Termination phase: Property scanning
% 223.01/35.67 % (1892619)Time elapsed: 0.421 s
% 223.01/35.67 % (1892619)Peak memory usage: 205 MB
% 223.01/35.67 % (1892619)Instructions burned: 440 (million)
% 223.01/35.67 % (1892622)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2436070963:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2729 on theBenchmark for (2729ds/11145Mi)
% 223.01/35.67 [W927 11:42:59.660794744 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.
% 223.01/35.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 223.01/35.67 [W927 11:42:59.660837144 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.
% 223.01/35.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 223.01/35.67 [W927 11:42:59.660891588 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.
% 223.01/35.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 223.01/35.67 [W927 11:42:59.660905361 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.
% 223.01/35.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 223.01/35.67 [W927 11:42:59.660933758 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.
% 223.01/35.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 223.01/35.67 [W927 11:42:59.660945418 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.
% 223.01/35.67 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 223.01/35.67 [W927 11:42:59.660973468 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.
% 163.53/37.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 163.53/37.30 [W927 11:42:59.660985538 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.
% 163.53/37.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 163.53/37.30 [W927 11:42:59.661031212 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.
% 163.53/37.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 163.53/37.30 [W927 11:42:59.661043072 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.
% 163.53/37.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 163.53/37.30 [W927 11:42:59.661071552 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.
% 163.53/37.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 163.53/37.30 [W927 11:42:59.661082336 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.
% 163.53/37.30 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 163.53/37.30 % (1892580)Instruction limit reached!
% 163.53/37.30 % (1892580)------------------------------
% 163.53/37.30 % (1892580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892580)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892580)Termination reason: Instruction limit
% 163.53/37.30 % (1892580)Termination phase: Saturation
% 163.53/37.30 % (1892580)Time elapsed: 16.395 s
% 163.53/37.30 % (1892580)Peak memory usage: 1326 MB
% 163.53/37.30 % (1892580)Instructions burned: 12111 (million)
% 163.53/37.30 % (1892777)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=930138470:cts=off:i=3034:av=off:er=known:fsd=on_2708 on theBenchmark for (2708ds/3034Mi)
% 163.53/37.30 % (1892622)Refutation not found, incomplete strategy
% 163.53/37.30 % (1892622)------------------------------
% 163.53/37.30 % (1892622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892622)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892622)Termination reason: Refutation not found, incomplete strategy
% 163.53/37.30 % (1892622)Time elapsed: 3.347 s
% 163.53/37.30 % (1892622)Peak memory usage: 601 MB
% 163.53/37.30 % (1892622)Instructions burned: 5271 (million)
% 163.53/37.30 % (1892561)Instruction limit reached!
% 163.53/37.30 % (1892561)------------------------------
% 163.53/37.30 % (1892561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892561)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892561)Termination reason: Instruction limit
% 163.53/37.30 % (1892561)Termination phase: Saturation
% 163.53/37.30 % (1892561)Time elapsed: 21.656 s
% 163.53/37.30 % (1892561)Peak memory usage: 1321 MB
% 163.53/37.30 % (1892561)Instructions burned: 14155 (million)
% 163.53/37.30 % (1892622)------------------------------
% 163.53/37.30 % (1892622)------------------------------
% 163.53/37.30 % (1892779)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1699016888:st=2:s2a=on:i=524:s2at=2:ss=axioms_2692 on theBenchmark for (2692ds/524Mi)
% 163.53/37.30 % (1892777)Instruction limit reached!
% 163.53/37.30 % (1892777)------------------------------
% 163.53/37.30 % (1892777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892777)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892777)Termination reason: Instruction limit
% 163.53/37.30 % (1892777)Termination phase: Preprocessing 3
% 163.53/37.30 % (1892777)Time elapsed: 1.797 s
% 163.53/37.30 % (1892777)Peak memory usage: 343 MB
% 163.53/37.30 % (1892777)Instructions burned: 3034 (million)
% 163.53/37.30 % (1892781)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2880850578:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2690 on theBenchmark for (2690ds/1016Mi)
% 163.53/37.30 % (1892779)Instruction limit reached!
% 163.53/37.30 % (1892779)------------------------------
% 163.53/37.30 % (1892779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892779)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892779)Termination reason: Instruction limit
% 163.53/37.30 % (1892779)Termination phase: SInE selection
% 163.53/37.30 % (1892779)Time elapsed: 0.233 s
% 163.53/37.30 % (1892779)Peak memory usage: 207 MB
% 163.53/37.30 % (1892779)Instructions burned: 527 (million)
% 163.53/37.30 % (1892783)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2651499929:i=14123:bd=preordered:ins=4_2688 on theBenchmark for (2688ds/14123Mi)
% 163.53/37.30 % (1892784)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3105742558:i=5781:kws=precedence:bd=all:rawr=on_2688 on theBenchmark for (2688ds/5781Mi)
% 163.53/37.30 % (1892781)Refutation not found, incomplete strategy
% 163.53/37.30 % (1892781)------------------------------
% 163.53/37.30 % (1892781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892781)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892781)Termination reason: Refutation not found, incomplete strategy
% 163.53/37.30 % (1892781)Time elapsed: 0.507 s
% 163.53/37.30 % (1892781)Peak memory usage: 258 MB
% 163.53/37.30 % (1892781)Instructions burned: 906 (million)
% 163.53/37.30 % (1892781)------------------------------
% 163.53/37.30 % (1892781)------------------------------
% 163.53/37.30 % (1892787)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=208448491:i=2448:gtgl=5:bd=preordered:gtg=all_2679 on theBenchmark for (2679ds/2448Mi)
% 163.53/37.30 % (1892605)Instruction limit reached!
% 163.53/37.30 % (1892605)------------------------------
% 163.53/37.30 % (1892605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892605)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892605)Termination reason: Instruction limit
% 163.53/37.30 % (1892605)Termination phase: Saturation
% 163.53/37.30 % (1892605)Time elapsed: 11.099 s
% 163.53/37.30 % (1892605)Peak memory usage: 1210 MB
% 163.53/37.30 % (1892605)Instructions burned: 9926 (million)
% 163.53/37.30 % (1892789)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=921661171:i=3223:kws=precedence:fgj=on:av=off_2673 on theBenchmark for (2673ds/3223Mi)
% 163.53/37.30 % (1892787)Instruction limit reached!
% 163.53/37.30 % (1892787)------------------------------
% 163.53/37.30 % (1892787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892787)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892787)Termination reason: Instruction limit
% 163.53/37.30 % (1892787)Termination phase: Preprocessing 1
% 163.53/37.30 % (1892787)Time elapsed: 1.006 s
% 163.53/37.30 % (1892787)Peak memory usage: 210 MB
% 163.53/37.30 % (1892787)Instructions burned: 2449 (million)
% 163.53/37.30 % (1892791)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=1295003411:st=5.6:i=2033:sd=3:ss=axioms_2668 on theBenchmark for (2668ds/2033Mi)
% 163.53/37.30 % (1892791)Instruction limit reached!
% 163.53/37.30 % (1892791)------------------------------
% 163.53/37.30 % (1892791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892791)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892791)Termination reason: Instruction limit
% 163.53/37.30 % (1892791)Termination phase: Saturation
% 163.53/37.30 % (1892791)Time elapsed: 0.960 s
% 163.53/37.30 % (1892791)Peak memory usage: 263 MB
% 163.53/37.30 % (1892791)Instructions burned: 2033 (million)
% 163.53/37.30 % (1892784)Instruction limit reached!
% 163.53/37.30 % (1892784)------------------------------
% 163.53/37.30 % (1892784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892784)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892784)Termination reason: Instruction limit
% 163.53/37.30 % (1892784)Termination phase: Property scanning
% 163.53/37.30 % (1892784)Time elapsed: 3.134 s
% 163.53/37.30 % (1892784)Peak memory usage: 392 MB
% 163.53/37.30 % (1892784)Instructions burned: 5783 (million)
% 163.53/37.30 % (1892793)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2058372589:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2656 on theBenchmark for (2656ds/2055Mi)
% 163.53/37.30 % (1892795)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=1711748517:i=21611:sd=3:ss=axioms_2654 on theBenchmark for (2654ds/21611Mi)
% 163.53/37.30 % (1892789)Instruction limit reached!
% 163.53/37.30 % (1892789)------------------------------
% 163.53/37.30 % (1892789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892789)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892789)Termination reason: Instruction limit
% 163.53/37.30 % (1892789)Termination phase: Clausification
% 163.53/37.30 % (1892789)Time elapsed: 1.934 s
% 163.53/37.30 % (1892789)Peak memory usage: 366 MB
% 163.53/37.30 % (1892789)Instructions burned: 3223 (million)
% 163.53/37.30 % (1892797)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2757109068:i=4835:sd=13:ss=axioms:sgt=23_2652 on theBenchmark for (2652ds/4835Mi)
% 163.53/37.30 % (1892793)Instruction limit reached!
% 163.53/37.30 % (1892793)------------------------------
% 163.53/37.30 % (1892793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892793)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892793)Termination reason: Instruction limit
% 163.53/37.30 % (1892793)Termination phase: SInE selection
% 163.53/37.30 % (1892793)Time elapsed: 0.832 s
% 163.53/37.30 % (1892793)Peak memory usage: 209 MB
% 163.53/37.30 % (1892793)Instructions burned: 2056 (million)
% 163.53/37.30 % (1892799)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=1376131166:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2646 on theBenchmark for (2646ds/797Mi)
% 163.53/37.30 % (1892797)First to succeed.
% 163.53/37.30 % (1892797)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1892484"
% 163.53/37.30 % (1892799)Instruction limit reached!
% 163.53/37.30 % (1892799)------------------------------
% 163.53/37.30 % (1892799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.53/37.30 % (1892799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.53/37.30 % (1892799)CaDiCaL version: 2.1.3
% 163.53/37.30 % (1892799)Termination reason: Instruction limit
% 163.53/37.30 % (1892799)Termination phase: SInE selection
% 163.53/37.30 % (1892799)Time elapsed: 0.321 s
% 163.53/37.30 % (1892799)Peak memory usage: 208 MB
% 163.53/37.30 % (1892799)Instructions burned: 798 (million)
% 163.53/37.30 % (1892797)Refutation found. Thanks to Tanya!
% 163.53/37.30 % SZS status Theorem for theBenchmark
% 163.53/37.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.32/37.62 % (1892797)------------------------------
% 0.32/37.62 % (1892797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.32/37.62 % (1892797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.32/37.62 % (1892797)CaDiCaL version: 2.1.3
% 0.32/37.62 % (1892797)Termination reason: Refutation
% 0.32/37.62 % (1892797)Time elapsed: 0.642 s
% 0.32/37.62 % (1892797)Peak memory usage: 260 MB
% 0.32/37.62 % (1892797)Instructions burned: 1109 (million)
% 0.32/37.62 % (1892797)------------------------------
% 0.32/37.62 % (1892797)------------------------------
% 0.32/37.62 % (1892484)Success in time 36.136 s
% 0.32/37.62 % Vampire exiting
%------------------------------------------------------------------------------