%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV123+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 : n015.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:46:39 AM UTC 2026
% Result : Theorem 77.40s 21.92s
% Output : Refutation 0.26s
% 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(f35,conjecture,
! [X0] :
( reachableState(X0)
=> v4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssertion) ).
fof(f36,negated_conjecture,
~ ! [X0] :
( reachableState(X0)
=> v4(X0) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,axiom,
! [X0] :
( ~ v4(X0)
<=> v154847(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11893) ).
fof(f38,axiom,
! [X0] :
( ~ v154847(X0)
<=> v154848(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11892) ).
fof(f39,axiom,
! [X0] :
( v154848(X0)
<=> ( v154850(X0)
& v154868(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20766) ).
fof(f40,axiom,
! [X0] :
( v154868(X0)
<=> ( v154869(X0)
| v154853(X0,bitIndex3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7474) ).
fof(f41,axiom,
! [X0] :
( v154869(X0)
<=> ( v154870(X0)
| v154853(X0,bitIndex2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7473) ).
fof(f42,axiom,
! [X0] :
( v154870(X0)
<=> ( v154853(X0,bitIndex0)
| v154853(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7472) ).
fof(f43,axiom,
! [X0] :
( v154850(X0)
<=> ( v154851(X0)
| v154859(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20765) ).
fof(f44,axiom,
! [X0] :
( v154859(X0)
<=> ( v154860(X0)
| v154861(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20764) ).
fof(f45,axiom,
! [X0] :
( v154861(X0)
<=> ( v154852(X0)
& v154862(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20763) ).
fof(f46,axiom,
! [X0] :
( v154862(X0)
<=> ( v154863(X0)
| v154864(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20762) ).
fof(f47,axiom,
! [X0] :
( v154864(X0)
<=> ( v154855(X0)
& v154865(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20761) ).
fof(f48,axiom,
! [X0] :
( v154865(X0)
<=> ( v154866(X0)
| v154867(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20760) ).
fof(f49,axiom,
! [X0] :
( v154867(X0)
<=> ( v154853(X0,bitIndex0)
& v154858(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20759) ).
fof(f50,axiom,
! [X0] :
( v154866(X0)
<=> ( v154857(X0)
& v154853(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7471) ).
fof(f51,axiom,
! [X0] :
( v154863(X0)
<=> ( v154853(X0,bitIndex2)
& v154856(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7470) ).
fof(f52,axiom,
! [X0] :
( v154860(X0)
<=> ( v154853(X0,bitIndex3)
& v154854(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_7469) ).
fof(f53,axiom,
! [X0] :
( v154851(X0)
<=> ( v154852(X0)
& v154854(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20758) ).
fof(f54,axiom,
! [X0] :
( v154854(X0)
<=> ( v154855(X0)
& v154856(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20757) ).
fof(f55,axiom,
! [X0] :
( v154856(X0)
<=> ( v154857(X0)
& v154858(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_20756) ).
fof(f56,axiom,
! [X0] :
( ~ v154858(X0)
<=> v154853(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11891) ).
fof(f57,axiom,
! [X0] :
( ~ v154857(X0)
<=> v154853(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11890) ).
fof(f58,axiom,
! [X0] :
( ~ v154855(X0)
<=> v154853(X0,bitIndex2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11889) ).
fof(f59,axiom,
! [X0] :
( ~ v154852(X0)
<=> v154853(X0,bitIndex3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11888) ).
fof(f60,axiom,
! [X0,X1] :
( range_3_0(X1)
=> ( v154853(X0,X1)
<=> v6(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86259) ).
fof(f61,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(f62,axiom,
! [X0] :
( v154836(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> b0001(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1782) ).
fof(f63,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(f64,axiom,
! [X0] :
( v154839(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v154838(X0,X1)
<=> b0010(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_1781) ).
fof(f65,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(f66,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(f67,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v154844(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86258) ).
fof(f68,axiom,
! [X0] :
( v154844(X0,bitIndex2)
<=> v154845(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86257) ).
fof(f69,axiom,
! [X0] :
( v154844(X0,bitIndex3)
<=> v83122(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86256) ).
fof(f70,axiom,
! [X0] :
( ~ v154845(X0)
<=> v83122(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11887) ).
fof(f71,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v154842(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86255) ).
fof(f72,axiom,
! [X0] :
( v154842(X0,bitIndex2)
<=> v154843(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86254) ).
fof(f73,axiom,
! [X0] :
( v154842(X0,bitIndex3)
<=> v83122(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_86253) ).
fof(f74,axiom,
! [X0] :
( ~ v154843(X0)
<=> v83122(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_11886) ).
fof(f138033,axiom,
~ b0010(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_280) ).
fof(f138034,axiom,
~ b0010(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_279) ).
fof(f138035,axiom,
b0010(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_278) ).
fof(f138036,axiom,
~ b0010(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_277) ).
fof(f138060,axiom,
~ b0001(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_276) ).
fof(f138061,axiom,
~ b0001(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_275) ).
fof(f138062,axiom,
~ b0001(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_274) ).
fof(f138063,axiom,
b0001(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_273) ).
fof(f141390,axiom,
! [X0] :
( range_1_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_axiom_4) ).
fof(f142249,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(f142335,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154842(X0,X1) ),
inference(true_and_false_elimination,[],[f71]) ).
fof(f142336,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154842(X0,X1) ),
inference(flattening,[],[f142335]) ).
fof(f142337,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154844(X0,X1) ),
inference(true_and_false_elimination,[],[f67]) ).
fof(f142338,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v154844(X0,X1) ),
inference(flattening,[],[f142337]) ).
fof(f142431,plain,
! [X0] :
( range_3_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
inference(true_and_false_elimination,[],[f142249]) ).
fof(f142435,plain,
! [X0] :
( range_1_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0 ) ),
inference(true_and_false_elimination,[],[f141390]) ).
fof(f142662,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0 )
=> range_1_0(X0) ),
inference(unused_predicate_definition_removal,[],[f142435]) ).
fof(f142663,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 )
=> range_3_0(X0) ),
inference(unused_predicate_definition_removal,[],[f142431]) ).
fof(f142664,plain,
! [X0] :
( ~ v4(X0)
=> v154847(X0) ),
inference(unused_predicate_definition_removal,[],[f37]) ).
fof(f142665,plain,
! [X0] :
( v154848(X0)
=> ~ v154847(X0) ),
inference(unused_predicate_definition_removal,[],[f38]) ).
fof(f142666,plain,
! [X0] :
( ( v154850(X0)
& v154868(X0) )
=> v154848(X0) ),
inference(unused_predicate_definition_removal,[],[f39]) ).
fof(f142667,plain,
! [X0] :
( ( v154851(X0)
| v154859(X0) )
=> v154850(X0) ),
inference(unused_predicate_definition_removal,[],[f43]) ).
fof(f142668,plain,
! [X0] :
( ( v154852(X0)
& v154854(X0) )
=> v154851(X0) ),
inference(unused_predicate_definition_removal,[],[f53]) ).
fof(f142669,plain,
! [X0] :
( ( v154860(X0)
| v154861(X0) )
=> v154859(X0) ),
inference(unused_predicate_definition_removal,[],[f44]) ).
fof(f142670,plain,
! [X0] :
( ( v154853(X0,bitIndex3)
& v154854(X0) )
=> v154860(X0) ),
inference(unused_predicate_definition_removal,[],[f52]) ).
fof(f142671,plain,
! [X0] :
( ( v154855(X0)
& v154856(X0) )
=> v154854(X0) ),
inference(unused_predicate_definition_removal,[],[f54]) ).
fof(f142672,plain,
! [X0] :
( ( v154852(X0)
& v154862(X0) )
=> v154861(X0) ),
inference(unused_predicate_definition_removal,[],[f45]) ).
fof(f142673,plain,
! [X0] :
( ~ v154852(X0)
=> v154853(X0,bitIndex3) ),
inference(unused_predicate_definition_removal,[],[f59]) ).
fof(f142674,plain,
! [X0] :
( ( v154863(X0)
| v154864(X0) )
=> v154862(X0) ),
inference(unused_predicate_definition_removal,[],[f46]) ).
fof(f142675,plain,
! [X0] :
( ( v154853(X0,bitIndex2)
& v154856(X0) )
=> v154863(X0) ),
inference(unused_predicate_definition_removal,[],[f51]) ).
fof(f142676,plain,
! [X0] :
( ( v154857(X0)
& v154858(X0) )
=> v154856(X0) ),
inference(unused_predicate_definition_removal,[],[f55]) ).
fof(f142677,plain,
! [X0] :
( ( v154855(X0)
& v154865(X0) )
=> v154864(X0) ),
inference(unused_predicate_definition_removal,[],[f47]) ).
fof(f142678,plain,
! [X0] :
( ~ v154855(X0)
=> v154853(X0,bitIndex2) ),
inference(unused_predicate_definition_removal,[],[f58]) ).
fof(f142679,plain,
! [X0] :
( ( v154866(X0)
| v154867(X0) )
=> v154865(X0) ),
inference(unused_predicate_definition_removal,[],[f48]) ).
fof(f142680,plain,
! [X0] :
( ( v154857(X0)
& v154853(X0,bitIndex1) )
=> v154866(X0) ),
inference(unused_predicate_definition_removal,[],[f50]) ).
fof(f142681,plain,
! [X0] :
( ~ v154857(X0)
=> v154853(X0,bitIndex0) ),
inference(unused_predicate_definition_removal,[],[f57]) ).
fof(f142682,plain,
! [X0] :
( ( v154853(X0,bitIndex0)
& v154858(X0) )
=> v154867(X0) ),
inference(unused_predicate_definition_removal,[],[f49]) ).
fof(f142683,plain,
! [X0] :
( ~ v154858(X0)
=> v154853(X0,bitIndex1) ),
inference(unused_predicate_definition_removal,[],[f56]) ).
fof(f142684,plain,
! [X0] :
( ( v154869(X0)
| v154853(X0,bitIndex3) )
=> v154868(X0) ),
inference(unused_predicate_definition_removal,[],[f40]) ).
fof(f142685,plain,
! [X0] :
( ( v154870(X0)
| v154853(X0,bitIndex2) )
=> v154869(X0) ),
inference(unused_predicate_definition_removal,[],[f41]) ).
fof(f142686,plain,
! [X0] :
( ( v154853(X0,bitIndex0)
| v154853(X0,bitIndex1) )
=> v154870(X0) ),
inference(unused_predicate_definition_removal,[],[f42]) ).
fof(f142710,plain,
~ ! [X0] : v4(X0),
inference(pure_predicate_removal,[],[f36]) ).
fof(f142799,plain,
? [X0] : ~ v4(X0),
inference(ennf_transformation,[],[f142710]) ).
fof(f142800,plain,
! [X0] :
( v154847(X0)
| v4(X0) ),
inference(ennf_transformation,[],[f142664]) ).
fof(f142801,plain,
! [X0] :
( ~ v154847(X0)
| ~ v154848(X0) ),
inference(ennf_transformation,[],[f142665]) ).
fof(f142802,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(ennf_transformation,[],[f142666]) ).
fof(f142803,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(flattening,[],[f142802]) ).
fof(f142804,plain,
! [X0] :
( v154850(X0)
| ( ~ v154851(X0)
& ~ v154859(X0) ) ),
inference(ennf_transformation,[],[f142667]) ).
fof(f142805,plain,
! [X0] :
( v154868(X0)
| ( ~ v154869(X0)
& ~ v154853(X0,bitIndex3) ) ),
inference(ennf_transformation,[],[f142684]) ).
fof(f142806,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(ennf_transformation,[],[f142668]) ).
fof(f142807,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(flattening,[],[f142806]) ).
fof(f142808,plain,
! [X0] :
( v154859(X0)
| ( ~ v154860(X0)
& ~ v154861(X0) ) ),
inference(ennf_transformation,[],[f142669]) ).
fof(f142809,plain,
! [X0] :
( v154869(X0)
| ( ~ v154870(X0)
& ~ v154853(X0,bitIndex2) ) ),
inference(ennf_transformation,[],[f142685]) ).
fof(f142810,plain,
! [X0,X1] :
( ( v154853(X0,X1)
<=> v6(X0,X1) )
| ~ range_3_0(X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f142811,plain,
! [X0] :
( v154853(X0,bitIndex3)
| v154852(X0) ),
inference(ennf_transformation,[],[f142673]) ).
fof(f142812,plain,
! [X0] :
( v154853(X0,bitIndex2)
| v154855(X0) ),
inference(ennf_transformation,[],[f142678]) ).
fof(f142813,plain,
! [X0] :
( v154853(X0,bitIndex0)
| v154857(X0) ),
inference(ennf_transformation,[],[f142681]) ).
fof(f142814,plain,
! [X0] :
( v154853(X0,bitIndex1)
| v154858(X0) ),
inference(ennf_transformation,[],[f142683]) ).
fof(f142815,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(ennf_transformation,[],[f142670]) ).
fof(f142816,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(flattening,[],[f142815]) ).
fof(f142817,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(ennf_transformation,[],[f142675]) ).
fof(f142818,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(flattening,[],[f142817]) ).
fof(f142819,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(ennf_transformation,[],[f142680]) ).
fof(f142820,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(flattening,[],[f142819]) ).
fof(f142821,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(ennf_transformation,[],[f142682]) ).
fof(f142822,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(flattening,[],[f142821]) ).
fof(f142823,plain,
! [X0] :
( v154870(X0)
| ( ~ v154853(X0,bitIndex0)
& ~ v154853(X0,bitIndex1) ) ),
inference(ennf_transformation,[],[f142686]) ).
fof(f142824,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(ennf_transformation,[],[f142672]) ).
fof(f142825,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(flattening,[],[f142824]) ).
fof(f142826,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(ennf_transformation,[],[f142671]) ).
fof(f142827,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(flattening,[],[f142826]) ).
fof(f142828,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> b0001(X1) )
| ~ range_3_0(X1) )
| ~ v154836(X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f142829,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> v154838(X0,X1) )
| ~ range_3_0(X1) )
| v154836(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f142830,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(ennf_transformation,[],[f142677]) ).
fof(f142831,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(flattening,[],[f142830]) ).
fof(f142832,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(ennf_transformation,[],[f142676]) ).
fof(f142833,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(flattening,[],[f142832]) ).
fof(f142834,plain,
! [X0] :
( v154862(X0)
| ( ~ v154863(X0)
& ~ v154864(X0) ) ),
inference(ennf_transformation,[],[f142674]) ).
fof(f142835,plain,
! [X0] :
( v154865(X0)
| ( ~ v154866(X0)
& ~ v154867(X0) ) ),
inference(ennf_transformation,[],[f142679]) ).
fof(f142840,plain,
! [X0] :
( ! [X1] :
( ( v154838(X0,X1)
<=> b0010(X1) )
| ~ range_3_0(X1) )
| ~ v154839(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f142841,plain,
! [X0] :
( ! [X1] :
( ( v154838(X0,X1)
<=> v154841(X0,X1) )
| ~ range_3_0(X1) )
| v154839(X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f142856,plain,
! [X0] :
( ! [X1] :
( ( v154841(X0,X1)
<=> v154842(X0,X1) )
| ~ range_3_0(X1) )
| ~ v1051(X0) ),
inference(ennf_transformation,[],[f66]) ).
fof(f142857,plain,
! [X0] :
( ! [X1] :
( ( v154841(X0,X1)
<=> v154844(X0,X1) )
| ~ range_3_0(X1) )
| v1051(X0) ),
inference(ennf_transformation,[],[f65]) ).
fof(f142903,plain,
! [X0,X1] :
( ~ v154842(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f142336]) ).
fof(f142904,plain,
! [X0,X1] :
( ~ v154844(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f142338]) ).
fof(f143130,plain,
! [X0] :
( range_3_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0
& bitIndex2 != X0
& bitIndex3 != X0 ) ),
inference(ennf_transformation,[],[f142663]) ).
fof(f143133,plain,
! [X0] :
( range_1_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0 ) ),
inference(ennf_transformation,[],[f142662]) ).
fof(f143450,plain,
~ v4(sK54),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X0,sK54)],[f142799]) ).
fof(f143451,plain,
! [X0,X1] :
( ( ( v154853(X0,X1)
| ~ v6(X0,X1) )
& ( v6(X0,X1)
| ~ v154853(X0,X1) ) )
| ~ range_3_0(X1) ),
inference(nnf_transformation,[],[f142810]) ).
fof(f143452,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ b0001(X1) )
& ( b0001(X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v154836(X0) ),
inference(nnf_transformation,[],[f142828]) ).
fof(f143453,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ v154838(X0,X1) )
& ( v154838(X0,X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| v154836(X0) ),
inference(nnf_transformation,[],[f142829]) ).
fof(f143460,plain,
! [X0] :
( ! [X1] :
( ( ( v154838(X0,X1)
| ~ b0010(X1) )
& ( b0010(X1)
| ~ v154838(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v154839(X0) ),
inference(nnf_transformation,[],[f142840]) ).
fof(f143461,plain,
! [X0] :
( ! [X1] :
( ( ( v154838(X0,X1)
| ~ v154841(X0,X1) )
& ( v154841(X0,X1)
| ~ v154838(X0,X1) ) )
| ~ range_3_0(X1) )
| v154839(X0) ),
inference(nnf_transformation,[],[f142841]) ).
fof(f143496,plain,
! [X0] :
( ! [X1] :
( ( ( v154841(X0,X1)
| ~ v154842(X0,X1) )
& ( v154842(X0,X1)
| ~ v154841(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v1051(X0) ),
inference(nnf_transformation,[],[f142856]) ).
fof(f143497,plain,
! [X0] :
( ! [X1] :
( ( ( v154841(X0,X1)
| ~ v154844(X0,X1) )
& ( v154844(X0,X1)
| ~ v154841(X0,X1) ) )
| ~ range_3_0(X1) )
| v1051(X0) ),
inference(nnf_transformation,[],[f142857]) ).
fof(f143588,plain,
! [X0] :
( ( v154842(X0,bitIndex3)
| ~ v83122(X0,bitIndex1) )
& ( v83122(X0,bitIndex1)
| ~ v154842(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f73]) ).
fof(f143589,plain,
! [X0] :
( ( v154842(X0,bitIndex2)
| ~ v154843(X0) )
& ( v154843(X0)
| ~ v154842(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f72]) ).
fof(f143590,plain,
! [X0] :
( ( v154844(X0,bitIndex3)
| ~ v83122(X0,bitIndex0) )
& ( v83122(X0,bitIndex0)
| ~ v154844(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f69]) ).
fof(f143591,plain,
! [X0] :
( ( v154844(X0,bitIndex2)
| ~ v154845(X0) )
& ( v154845(X0)
| ~ v154844(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f143856,plain,
! [X0] :
( ( ~ v154843(X0)
| ~ v83122(X0,bitIndex1) )
& ( v83122(X0,bitIndex1)
| v154843(X0) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f143857,plain,
! [X0] :
( ( ~ v154845(X0)
| ~ v83122(X0,bitIndex0) )
& ( v83122(X0,bitIndex0)
| v154845(X0) ) ),
inference(nnf_transformation,[],[f70]) ).
fof(f145895,plain,
~ v4(sK54),
inference(cnf_transformation,[],[f143450]) ).
fof(f145896,plain,
! [X0] :
( v154847(X0)
| v4(X0) ),
inference(cnf_transformation,[],[f142800]) ).
fof(f145897,plain,
! [X0] :
( ~ v154847(X0)
| ~ v154848(X0) ),
inference(cnf_transformation,[],[f142801]) ).
fof(f145898,plain,
! [X0] :
( v154848(X0)
| ~ v154850(X0)
| ~ v154868(X0) ),
inference(cnf_transformation,[],[f142803]) ).
fof(f145899,plain,
! [X0] :
( v154850(X0)
| ~ v154859(X0) ),
inference(cnf_transformation,[],[f142804]) ).
fof(f145900,plain,
! [X0] :
( v154850(X0)
| ~ v154851(X0) ),
inference(cnf_transformation,[],[f142804]) ).
fof(f145901,plain,
! [X0] :
( v154868(X0)
| ~ v154853(X0,bitIndex3) ),
inference(cnf_transformation,[],[f142805]) ).
fof(f145902,plain,
! [X0] :
( v154868(X0)
| ~ v154869(X0) ),
inference(cnf_transformation,[],[f142805]) ).
fof(f145903,plain,
! [X0] :
( v154851(X0)
| ~ v154852(X0)
| ~ v154854(X0) ),
inference(cnf_transformation,[],[f142807]) ).
fof(f145904,plain,
! [X0] :
( v154859(X0)
| ~ v154861(X0) ),
inference(cnf_transformation,[],[f142808]) ).
fof(f145905,plain,
! [X0] :
( v154859(X0)
| ~ v154860(X0) ),
inference(cnf_transformation,[],[f142808]) ).
fof(f145906,plain,
! [X0] :
( v154869(X0)
| ~ v154853(X0,bitIndex2) ),
inference(cnf_transformation,[],[f142809]) ).
fof(f145907,plain,
! [X0] :
( v154869(X0)
| ~ v154870(X0) ),
inference(cnf_transformation,[],[f142809]) ).
fof(f145908,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v154853(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f143451]) ).
fof(f145909,plain,
! [X0,X1] :
( v154853(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f143451]) ).
fof(f145910,plain,
! [X0] :
( v154853(X0,bitIndex3)
| v154852(X0) ),
inference(cnf_transformation,[],[f142811]) ).
fof(f145911,plain,
! [X0] :
( v154853(X0,bitIndex2)
| v154855(X0) ),
inference(cnf_transformation,[],[f142812]) ).
fof(f145912,plain,
! [X0] :
( v154853(X0,bitIndex0)
| v154857(X0) ),
inference(cnf_transformation,[],[f142813]) ).
fof(f145913,plain,
! [X0] :
( v154853(X0,bitIndex1)
| v154858(X0) ),
inference(cnf_transformation,[],[f142814]) ).
fof(f145914,plain,
! [X0] :
( v154860(X0)
| ~ v154853(X0,bitIndex3)
| ~ v154854(X0) ),
inference(cnf_transformation,[],[f142816]) ).
fof(f145915,plain,
! [X0] :
( v154863(X0)
| ~ v154853(X0,bitIndex2)
| ~ v154856(X0) ),
inference(cnf_transformation,[],[f142818]) ).
fof(f145916,plain,
! [X0] :
( v154866(X0)
| ~ v154857(X0)
| ~ v154853(X0,bitIndex1) ),
inference(cnf_transformation,[],[f142820]) ).
fof(f145917,plain,
! [X0] :
( v154867(X0)
| ~ v154853(X0,bitIndex0)
| ~ v154858(X0) ),
inference(cnf_transformation,[],[f142822]) ).
fof(f145918,plain,
! [X0] :
( v154870(X0)
| ~ v154853(X0,bitIndex1) ),
inference(cnf_transformation,[],[f142823]) ).
fof(f145919,plain,
! [X0] :
( v154870(X0)
| ~ v154853(X0,bitIndex0) ),
inference(cnf_transformation,[],[f142823]) ).
fof(f145920,plain,
! [X0] :
( v154861(X0)
| ~ v154852(X0)
| ~ v154862(X0) ),
inference(cnf_transformation,[],[f142825]) ).
fof(f145921,plain,
! [X0] :
( v154854(X0)
| ~ v154855(X0)
| ~ v154856(X0) ),
inference(cnf_transformation,[],[f142827]) ).
fof(f145922,plain,
! [X0,X1] :
( b0001(X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| ~ v154836(X0) ),
inference(cnf_transformation,[],[f143452]) ).
fof(f145923,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ b0001(X1)
| ~ range_3_0(X1)
| ~ v154836(X0) ),
inference(cnf_transformation,[],[f143452]) ).
fof(f145924,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| v154836(X0) ),
inference(cnf_transformation,[],[f143453]) ).
fof(f145925,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| v154836(X0) ),
inference(cnf_transformation,[],[f143453]) ).
fof(f145926,plain,
! [X0] :
( v154864(X0)
| ~ v154855(X0)
| ~ v154865(X0) ),
inference(cnf_transformation,[],[f142831]) ).
fof(f145927,plain,
! [X0] :
( v154856(X0)
| ~ v154857(X0)
| ~ v154858(X0) ),
inference(cnf_transformation,[],[f142833]) ).
fof(f145928,plain,
! [X0] :
( v154862(X0)
| ~ v154864(X0) ),
inference(cnf_transformation,[],[f142834]) ).
fof(f145929,plain,
! [X0] :
( v154862(X0)
| ~ v154863(X0) ),
inference(cnf_transformation,[],[f142834]) ).
fof(f145930,plain,
! [X0] :
( v154865(X0)
| ~ v154867(X0) ),
inference(cnf_transformation,[],[f142835]) ).
fof(f145931,plain,
! [X0] :
( v154865(X0)
| ~ v154866(X0) ),
inference(cnf_transformation,[],[f142835]) ).
fof(f145935,plain,
b0001(bitIndex0),
inference(cnf_transformation,[],[f138063]) ).
fof(f145936,plain,
~ b0001(bitIndex1),
inference(cnf_transformation,[],[f138062]) ).
fof(f145937,plain,
~ b0001(bitIndex2),
inference(cnf_transformation,[],[f138061]) ).
fof(f145938,plain,
~ b0001(bitIndex3),
inference(cnf_transformation,[],[f138060]) ).
fof(f145951,plain,
! [X0,X1] :
( b0010(X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| ~ v154839(X0) ),
inference(cnf_transformation,[],[f143460]) ).
fof(f145952,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ b0010(X1)
| ~ range_3_0(X1)
| ~ v154839(X0) ),
inference(cnf_transformation,[],[f143460]) ).
fof(f145953,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154838(X0,X1)
| ~ range_3_0(X1)
| v154839(X0) ),
inference(cnf_transformation,[],[f143461]) ).
fof(f145954,plain,
! [X0,X1] :
( v154838(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| v154839(X0) ),
inference(cnf_transformation,[],[f143461]) ).
fof(f146019,plain,
~ b0010(bitIndex0),
inference(cnf_transformation,[],[f138036]) ).
fof(f146020,plain,
b0010(bitIndex1),
inference(cnf_transformation,[],[f138035]) ).
fof(f146021,plain,
~ b0010(bitIndex2),
inference(cnf_transformation,[],[f138034]) ).
fof(f146022,plain,
~ b0010(bitIndex3),
inference(cnf_transformation,[],[f138033]) ).
fof(f146027,plain,
! [X0,X1] :
( v154842(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| ~ v1051(X0) ),
inference(cnf_transformation,[],[f143496]) ).
fof(f146028,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154842(X0,X1)
| ~ range_3_0(X1)
| ~ v1051(X0) ),
inference(cnf_transformation,[],[f143496]) ).
fof(f146029,plain,
! [X0,X1] :
( v154844(X0,X1)
| ~ v154841(X0,X1)
| ~ range_3_0(X1)
| v1051(X0) ),
inference(cnf_transformation,[],[f143497]) ).
fof(f146030,plain,
! [X0,X1] :
( v154841(X0,X1)
| ~ v154844(X0,X1)
| ~ range_3_0(X1)
| v1051(X0) ),
inference(cnf_transformation,[],[f143497]) ).
fof(f146204,plain,
! [X0] :
( v83122(X0,bitIndex1)
| ~ v154842(X0,bitIndex3) ),
inference(cnf_transformation,[],[f143588]) ).
fof(f146205,plain,
! [X0] :
( v154842(X0,bitIndex3)
| ~ v83122(X0,bitIndex1) ),
inference(cnf_transformation,[],[f143588]) ).
fof(f146206,plain,
! [X0] :
( v154843(X0)
| ~ v154842(X0,bitIndex2) ),
inference(cnf_transformation,[],[f143589]) ).
fof(f146207,plain,
! [X0] :
( v154842(X0,bitIndex2)
| ~ v154843(X0) ),
inference(cnf_transformation,[],[f143589]) ).
fof(f146208,plain,
! [X0,X1] :
( ~ v154842(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f142903]) ).
fof(f146209,plain,
! [X0] :
( v83122(X0,bitIndex0)
| ~ v154844(X0,bitIndex3) ),
inference(cnf_transformation,[],[f143590]) ).
fof(f146210,plain,
! [X0] :
( v154844(X0,bitIndex3)
| ~ v83122(X0,bitIndex0) ),
inference(cnf_transformation,[],[f143590]) ).
fof(f146211,plain,
! [X0] :
( v154845(X0)
| ~ v154844(X0,bitIndex2) ),
inference(cnf_transformation,[],[f143591]) ).
fof(f146212,plain,
! [X0] :
( v154844(X0,bitIndex2)
| ~ v154845(X0) ),
inference(cnf_transformation,[],[f143591]) ).
fof(f146213,plain,
! [X0,X1] :
( ~ v154844(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f142904]) ).
fof(f146732,plain,
! [X0] :
( v83122(X0,bitIndex1)
| v154843(X0) ),
inference(cnf_transformation,[],[f143856]) ).
fof(f146733,plain,
! [X0] :
( ~ v154843(X0)
| ~ v83122(X0,bitIndex1) ),
inference(cnf_transformation,[],[f143856]) ).
fof(f146734,plain,
! [X0] :
( v83122(X0,bitIndex0)
| v154845(X0) ),
inference(cnf_transformation,[],[f143857]) ).
fof(f146735,plain,
! [X0] :
( ~ v154845(X0)
| ~ v83122(X0,bitIndex0) ),
inference(cnf_transformation,[],[f143857]) ).
fof(f148291,plain,
! [X0] :
( range_3_0(X0)
| bitIndex3 != X0 ),
inference(cnf_transformation,[],[f143130]) ).
fof(f148292,plain,
! [X0] :
( range_3_0(X0)
| bitIndex2 != X0 ),
inference(cnf_transformation,[],[f143130]) ).
fof(f148293,plain,
! [X0] :
( range_3_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f143130]) ).
fof(f148294,plain,
! [X0] :
( range_3_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f143130]) ).
fof(f148306,plain,
! [X0] :
( range_1_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f143133]) ).
fof(f148307,plain,
! [X0] :
( range_1_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f143133]) ).
fof(f150967,plain,
range_3_0(bitIndex0),
inference(equality_resolution,[],[f148294]) ).
fof(f150968,plain,
range_3_0(bitIndex1),
inference(equality_resolution,[],[f148293]) ).
fof(f150969,plain,
range_3_0(bitIndex2),
inference(equality_resolution,[],[f148292]) ).
fof(f150970,plain,
range_3_0(bitIndex3),
inference(equality_resolution,[],[f148291]) ).
fof(f150982,plain,
range_1_0(bitIndex0),
inference(equality_resolution,[],[f148307]) ).
fof(f150983,plain,
range_1_0(bitIndex1),
inference(equality_resolution,[],[f148306]) ).
fof(f151086,plain,
v154847(sK54),
inference(resolution,[],[f145895,f145896]) ).
fof(f151087,plain,
~ v154848(sK54),
inference(resolution,[],[f151086,f145897]) ).
fof(f151088,plain,
( ~ v154850(sK54)
| ~ v154868(sK54) ),
inference(resolution,[],[f151087,f145898]) ).
fof(f151090,definition,
( spl55_1
<=> v154868(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_1])],[avatar_definition]) ).
fof(f151092,plain,
( ~ v154868(sK54)
| spl55_1 ),
inference(avatar_component_clause,[],[f151090]) ).
fof(f151094,definition,
( spl55_2
<=> v154850(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_2])],[avatar_definition]) ).
fof(f151096,plain,
( ~ v154850(sK54)
| spl55_2 ),
inference(avatar_component_clause,[],[f151094]) ).
fof(f151097,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(avatar_split_clause,[],[f151088,f151094,f151090]) ).
fof(f151098,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_1 ),
inference(resolution,[],[f151092,f145901]) ).
fof(f151099,plain,
( ~ v154869(sK54)
| spl55_1 ),
inference(resolution,[],[f151092,f145902]) ).
fof(f151101,plain,
( ~ v154870(sK54)
| spl55_1 ),
inference(resolution,[],[f151099,f145907]) ).
fof(f151103,plain,
( ~ v6(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl55_1 ),
inference(resolution,[],[f151098,f145909]) ).
fof(f151104,plain,
( ~ v6(sK54,bitIndex3)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f151103,f150970]) ).
fof(f151110,definition,
( spl55_3
<=> v154854(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_3])],[avatar_definition]) ).
fof(f151111,plain,
( v154854(sK54)
| ~ spl55_3 ),
inference(avatar_component_clause,[],[f151110]) ).
fof(f151112,plain,
( ~ v154854(sK54)
| spl55_3 ),
inference(avatar_component_clause,[],[f151110]) ).
fof(f151114,definition,
( spl55_4
<=> v154851(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_4])],[avatar_definition]) ).
fof(f151115,plain,
( ~ v154851(sK54)
| spl55_4 ),
inference(avatar_component_clause,[],[f151114]) ).
fof(f151119,definition,
( spl55_5
<=> v154862(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_5])],[avatar_definition]) ).
fof(f151120,plain,
( v154862(sK54)
| ~ spl55_5 ),
inference(avatar_component_clause,[],[f151119]) ).
fof(f151121,plain,
( ~ v154862(sK54)
| spl55_5 ),
inference(avatar_component_clause,[],[f151119]) ).
fof(f151123,definition,
( spl55_6
<=> v154861(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_6])],[avatar_definition]) ).
fof(f151124,plain,
( ~ v154861(sK54)
| spl55_6 ),
inference(avatar_component_clause,[],[f151123]) ).
fof(f151127,plain,
( ~ v154855(sK54)
| ~ v154856(sK54)
| spl55_3 ),
inference(resolution,[],[f151112,f145921]) ).
fof(f151129,definition,
( spl55_7
<=> v154856(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_7])],[avatar_definition]) ).
fof(f151130,plain,
( v154856(sK54)
| ~ spl55_7 ),
inference(avatar_component_clause,[],[f151129]) ).
fof(f151131,plain,
( ~ v154856(sK54)
| spl55_7 ),
inference(avatar_component_clause,[],[f151129]) ).
fof(f151133,definition,
( spl55_8
<=> v154855(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_8])],[avatar_definition]) ).
fof(f151134,plain,
( v154855(sK54)
| ~ spl55_8 ),
inference(avatar_component_clause,[],[f151133]) ).
fof(f151135,plain,
( ~ v154855(sK54)
| spl55_8 ),
inference(avatar_component_clause,[],[f151133]) ).
fof(f151136,plain,
( ~ spl55_7
| ~ spl55_8
| spl55_3 ),
inference(avatar_split_clause,[],[f151127,f151110,f151133,f151129]) ).
fof(f151141,plain,
( ~ v154864(sK54)
| spl55_5 ),
inference(resolution,[],[f151121,f145928]) ).
fof(f151142,plain,
( ~ v154863(sK54)
| spl55_5 ),
inference(resolution,[],[f151121,f145929]) ).
fof(f151143,plain,
( ~ v154838(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154836(sK54)
| spl55_1 ),
inference(resolution,[],[f151104,f145925]) ).
fof(f151146,plain,
( ~ v154838(sK54,bitIndex3)
| v154836(sK54)
| spl55_1 ),
inference(forward_subsumption_resolution,[],[f151143,f150970]) ).
fof(f151148,definition,
( spl55_9
<=> v154836(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_9])],[avatar_definition]) ).
fof(f151149,plain,
( ~ v154836(sK54)
| spl55_9 ),
inference(avatar_component_clause,[],[f151148]) ).
fof(f151150,plain,
( v154836(sK54)
| ~ spl55_9 ),
inference(avatar_component_clause,[],[f151148]) ).
fof(f151152,definition,
( spl55_10
<=> v154838(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_10])],[avatar_definition]) ).
fof(f151153,plain,
( v154838(sK54,bitIndex3)
| ~ spl55_10 ),
inference(avatar_component_clause,[],[f151152]) ).
fof(f151154,plain,
( ~ v154838(sK54,bitIndex3)
| spl55_10 ),
inference(avatar_component_clause,[],[f151152]) ).
fof(f151155,plain,
( spl55_9
| ~ spl55_10
| spl55_1 ),
inference(avatar_split_clause,[],[f151146,f151090,f151152,f151148]) ).
fof(f151156,plain,
( ~ v154857(sK54)
| ~ v154858(sK54)
| spl55_7 ),
inference(resolution,[],[f151131,f145927]) ).
fof(f151158,definition,
( spl55_11
<=> v154858(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_11])],[avatar_definition]) ).
fof(f151160,plain,
( ~ v154858(sK54)
| spl55_11 ),
inference(avatar_component_clause,[],[f151158]) ).
fof(f151162,definition,
( spl55_12
<=> v154857(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_12])],[avatar_definition]) ).
fof(f151163,plain,
( v154857(sK54)
| ~ spl55_12 ),
inference(avatar_component_clause,[],[f151162]) ).
fof(f151164,plain,
( ~ v154857(sK54)
| spl55_12 ),
inference(avatar_component_clause,[],[f151162]) ).
fof(f151165,plain,
( ~ spl55_11
| ~ spl55_12
| spl55_7 ),
inference(avatar_split_clause,[],[f151156,f151129,f151162,f151158]) ).
fof(f151172,plain,
( ~ v154859(sK54)
| spl55_2 ),
inference(resolution,[],[f151096,f145899]) ).
fof(f151173,plain,
( ~ v154851(sK54)
| spl55_2 ),
inference(resolution,[],[f151096,f145900]) ).
fof(f151174,plain,
( ~ spl55_4
| spl55_2 ),
inference(avatar_split_clause,[],[f151173,f151094,f151114]) ).
fof(f151175,plain,
( ~ v154861(sK54)
| spl55_2 ),
inference(resolution,[],[f151172,f145904]) ).
fof(f151176,plain,
( ~ v154860(sK54)
| spl55_2 ),
inference(resolution,[],[f151172,f145905]) ).
fof(f151177,plain,
( ~ spl55_6
| spl55_2 ),
inference(avatar_split_clause,[],[f151175,f151094,f151123]) ).
fof(f151181,plain,
( v154864(sK54)
| ~ v154865(sK54)
| ~ spl55_8 ),
inference(resolution,[],[f151134,f145926]) ).
fof(f151183,plain,
( ~ v154865(sK54)
| spl55_5
| ~ spl55_8 ),
inference(forward_subsumption_resolution,[],[f151181,f151141]) ).
fof(f151184,plain,
( ~ v154841(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154839(sK54)
| spl55_10 ),
inference(resolution,[],[f151154,f145954]) ).
fof(f151186,plain,
( ~ v6(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v154836(sK54)
| spl55_10 ),
inference(resolution,[],[f151154,f145924]) ).
fof(f151187,plain,
( ~ v6(sK54,bitIndex3)
| v154836(sK54)
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f151186,f150970]) ).
fof(f151188,plain,
( ~ v154841(sK54,bitIndex3)
| v154839(sK54)
| spl55_10 ),
inference(forward_subsumption_resolution,[],[f151184,f150970]) ).
fof(f151190,definition,
( spl55_13
<=> v6(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_13])],[avatar_definition]) ).
fof(f151191,plain,
( v6(sK54,bitIndex3)
| ~ spl55_13 ),
inference(avatar_component_clause,[],[f151190]) ).
fof(f151192,plain,
( ~ v6(sK54,bitIndex3)
| spl55_13 ),
inference(avatar_component_clause,[],[f151190]) ).
fof(f151193,plain,
( spl55_9
| ~ spl55_13
| spl55_10 ),
inference(avatar_split_clause,[],[f151187,f151152,f151190,f151148]) ).
fof(f151195,definition,
( spl55_14
<=> v154839(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_14])],[avatar_definition]) ).
fof(f151196,plain,
( ~ v154839(sK54)
| spl55_14 ),
inference(avatar_component_clause,[],[f151195]) ).
fof(f151197,plain,
( v154839(sK54)
| ~ spl55_14 ),
inference(avatar_component_clause,[],[f151195]) ).
fof(f151199,definition,
( spl55_15
<=> v154841(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_15])],[avatar_definition]) ).
fof(f151200,plain,
( v154841(sK54,bitIndex3)
| ~ spl55_15 ),
inference(avatar_component_clause,[],[f151199]) ).
fof(f151201,plain,
( ~ v154841(sK54,bitIndex3)
| spl55_15 ),
inference(avatar_component_clause,[],[f151199]) ).
fof(f151202,plain,
( spl55_14
| ~ spl55_15
| spl55_10 ),
inference(avatar_split_clause,[],[f151188,f151152,f151199,f151195]) ).
fof(f151205,plain,
( v154853(sK54,bitIndex1)
| spl55_11 ),
inference(resolution,[],[f151160,f145913]) ).
fof(f151208,plain,
( ~ v154853(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl55_13 ),
inference(resolution,[],[f151192,f145908]) ).
fof(f151209,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151208,f150970]) ).
fof(f151210,plain,
( ~ v154867(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151183,f145930]) ).
fof(f151211,plain,
( ~ v154866(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151183,f145931]) ).
fof(f151212,plain,
( ~ v154844(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v1051(sK54)
| spl55_15 ),
inference(resolution,[],[f151201,f146030]) ).
fof(f151213,plain,
( ~ v154842(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| spl55_15 ),
inference(resolution,[],[f151201,f146028]) ).
fof(f151215,plain,
( ~ v154842(sK54,bitIndex3)
| ~ v1051(sK54)
| spl55_15 ),
inference(forward_subsumption_resolution,[],[f151213,f150970]) ).
fof(f151216,plain,
( ~ v154844(sK54,bitIndex3)
| v1051(sK54)
| spl55_15 ),
inference(forward_subsumption_resolution,[],[f151212,f150970]) ).
fof(f151218,definition,
( spl55_16
<=> v1051(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_16])],[avatar_definition]) ).
fof(f151219,plain,
( v1051(sK54)
| ~ spl55_16 ),
inference(avatar_component_clause,[],[f151218]) ).
fof(f151220,plain,
( ~ v1051(sK54)
| spl55_16 ),
inference(avatar_component_clause,[],[f151218]) ).
fof(f151222,definition,
( spl55_17
<=> v154842(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_17])],[avatar_definition]) ).
fof(f151223,plain,
( v154842(sK54,bitIndex3)
| ~ spl55_17 ),
inference(avatar_component_clause,[],[f151222]) ).
fof(f151224,plain,
( ~ v154842(sK54,bitIndex3)
| spl55_17 ),
inference(avatar_component_clause,[],[f151222]) ).
fof(f151225,plain,
( ~ spl55_16
| ~ spl55_17
| spl55_15 ),
inference(avatar_split_clause,[],[f151215,f151199,f151222,f151218]) ).
fof(f151227,definition,
( spl55_18
<=> v154844(sK54,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl55_18])],[avatar_definition]) ).
fof(f151228,plain,
( v154844(sK54,bitIndex3)
| ~ spl55_18 ),
inference(avatar_component_clause,[],[f151227]) ).
fof(f151229,plain,
( ~ v154844(sK54,bitIndex3)
| spl55_18 ),
inference(avatar_component_clause,[],[f151227]) ).
fof(f151230,plain,
( spl55_16
| ~ spl55_18
| spl55_15 ),
inference(avatar_split_clause,[],[f151216,f151199,f151227,f151218]) ).
fof(f151273,plain,
( v154852(sK54)
| spl55_13 ),
inference(resolution,[],[f151209,f145910]) ).
fof(f151275,plain,
( ~ v154853(sK54,bitIndex0)
| ~ v154858(sK54)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151210,f145917]) ).
fof(f151276,plain,
( ~ v83122(sK54,bitIndex0)
| spl55_18 ),
inference(resolution,[],[f151229,f146210]) ).
fof(f151278,plain,
( ~ v154857(sK54)
| ~ v154853(sK54,bitIndex1)
| spl55_5
| ~ spl55_8 ),
inference(resolution,[],[f151211,f145916]) ).
fof(f151279,plain,
( ~ v154857(sK54)
| spl55_5
| ~ spl55_8
| spl55_11 ),
inference(forward_subsumption_resolution,[],[f151278,f151205]) ).
fof(f151280,plain,
( ~ spl55_12
| spl55_5
| ~ spl55_8
| spl55_11 ),
inference(avatar_split_clause,[],[f151279,f151158,f151133,f151119,f151162]) ).
fof(f151281,plain,
( v154853(sK54,bitIndex0)
| spl55_12 ),
inference(resolution,[],[f151164,f145912]) ).
fof(f151325,plain,
( v154861(sK54)
| ~ v154862(sK54)
| spl55_13 ),
inference(resolution,[],[f151273,f145920]) ).
fof(f151365,plain,
( v154845(sK54)
| spl55_18 ),
inference(resolution,[],[f151276,f146734]) ).
fof(f151369,definition,
( spl55_31
<=> v83122(sK54,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl55_31])],[avatar_definition]) ).
fof(f151370,plain,
( ~ v83122(sK54,bitIndex1)
| spl55_31 ),
inference(avatar_component_clause,[],[f151369]) ).
fof(f151371,plain,
( v83122(sK54,bitIndex1)
| ~ spl55_31 ),
inference(avatar_component_clause,[],[f151369]) ).
fof(f151388,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| b0010(X0)
| ~ range_3_0(X0) )
| ~ spl55_14 ),
inference(resolution,[],[f151197,f145951]) ).
fof(f151400,plain,
( v83122(sK54,bitIndex0)
| ~ spl55_18 ),
inference(resolution,[],[f151228,f146209]) ).
fof(f151405,plain,
( ! [X0] :
( b0010(X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0)
| v154836(sK54) )
| ~ spl55_14 ),
inference(resolution,[],[f151388,f145924]) ).
fof(f151406,plain,
( ! [X0] :
( b0010(X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| v154836(sK54) )
| ~ spl55_14 ),
inference(duplicate_literal_removal,[],[f151405]) ).
fof(f151410,definition,
( spl55_35
<=> ! [X0] :
( b0010(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_35])],[avatar_definition]) ).
fof(f151411,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| b0010(X0)
| ~ range_3_0(X0) )
| ~ spl55_35 ),
inference(avatar_component_clause,[],[f151410]) ).
fof(f151412,plain,
( spl55_9
| spl55_35
| ~ spl55_14 ),
inference(avatar_split_clause,[],[f151406,f151195,f151410,f151148]) ).
fof(f151416,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| spl55_14 ),
inference(resolution,[],[f151196,f145953]) ).
fof(f151431,plain,
( ! [X0] :
( ~ v154842(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_16 ),
inference(resolution,[],[f151219,f146028]) ).
fof(f151489,plain,
( ~ v83122(sK54,bitIndex1)
| spl55_17 ),
inference(resolution,[],[f151224,f146205]) ).
fof(f151491,plain,
( ~ spl55_31
| spl55_17 ),
inference(avatar_split_clause,[],[f151489,f151222,f151369]) ).
fof(f151498,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0)
| v154836(sK54) )
| spl55_14 ),
inference(resolution,[],[f151416,f145924]) ).
fof(f151499,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v6(sK54,X0)
| v154836(sK54) )
| spl55_14 ),
inference(duplicate_literal_removal,[],[f151498]) ).
fof(f151503,definition,
( spl55_45
<=> ! [X0] :
( v154841(sK54,X0)
| ~ v6(sK54,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl55_45])],[avatar_definition]) ).
fof(f151504,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_45 ),
inference(avatar_component_clause,[],[f151503]) ).
fof(f151505,plain,
( spl55_9
| spl55_45
| spl55_14 ),
inference(avatar_split_clause,[],[f151499,f151195,f151503,f151148]) ).
fof(f151508,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151150,f145922]) ).
fof(f151518,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151508,f145908]) ).
fof(f151519,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl55_9 ),
inference(duplicate_literal_removal,[],[f151518]) ).
fof(f151551,plain,
( ~ range_3_0(bitIndex2)
| b0001(bitIndex2)
| v154855(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f151519,f145911]) ).
fof(f151553,plain,
( ~ range_3_0(bitIndex1)
| b0001(bitIndex1)
| v154858(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f151519,f145913]) ).
fof(f151555,plain,
( b0001(bitIndex1)
| v154858(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151553,f150968]) ).
fof(f151557,plain,
( v154858(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151555,f145936]) ).
fof(f151562,plain,
( ~ v154858(sK54)
| spl55_5
| ~ spl55_8
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151275,f151281]) ).
fof(f151575,plain,
( ~ v154862(sK54)
| spl55_6
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151325,f151124]) ).
fof(f151578,plain,
( $false
| ~ spl55_5
| spl55_6
| spl55_13 ),
inference(forward_subsumption_resolution,[],[f151575,f151120]) ).
fof(f151579,plain,
( ~ spl55_5
| spl55_6
| spl55_13 ),
inference(avatar_contradiction_clause,[],[f151578]) ).
fof(f151590,plain,
( b0001(bitIndex2)
| v154855(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151551,f150969]) ).
fof(f151591,plain,
( v154855(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151590,f145937]) ).
fof(f151592,plain,
( $false
| spl55_8
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f151591,f151135]) ).
fof(f151593,plain,
( spl55_8
| ~ spl55_9 ),
inference(avatar_contradiction_clause,[],[f151592]) ).
fof(f151604,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151149,f145924]) ).
fof(f151605,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| v6(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151149,f145925]) ).
fof(f151607,plain,
( v154853(sK54,bitIndex2)
| spl55_8 ),
inference(resolution,[],[f151135,f145911]) ).
fof(f151618,plain,
( ! [X0] :
( v154838(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151604,f145908]) ).
fof(f151619,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154838(sK54,X0) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151618]) ).
fof(f151624,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ v154841(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| spl55_9 ),
inference(resolution,[],[f151605,f145954]) ).
fof(f151625,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ range_3_0(X0)
| ~ v154839(sK54) )
| spl55_9 ),
inference(resolution,[],[f151605,f145952]) ).
fof(f151628,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ v154839(sK54) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151625]) ).
fof(f151629,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ v154841(sK54,X0)
| v154839(sK54) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f151624]) ).
fof(f151637,plain,
( v154863(sK54)
| ~ v154856(sK54)
| spl55_8 ),
inference(resolution,[],[f151607,f145915]) ).
fof(f151639,plain,
( v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_8 ),
inference(resolution,[],[f151607,f145908]) ).
fof(f151640,plain,
( v6(sK54,bitIndex2)
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f151639,f150969]) ).
fof(f151656,plain,
( ~ range_3_0(bitIndex2)
| v154838(sK54,bitIndex2)
| spl55_8
| spl55_9 ),
inference(resolution,[],[f151619,f151607]) ).
fof(f151660,plain,
( ~ range_3_0(bitIndex0)
| v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(resolution,[],[f151619,f145912]) ).
fof(f151661,plain,
( ~ range_3_0(bitIndex1)
| v154838(sK54,bitIndex1)
| v154858(sK54)
| spl55_9 ),
inference(resolution,[],[f151619,f145913]) ).
fof(f151663,plain,
( v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151660,f150967]) ).
fof(f151665,plain,
( v154838(sK54,bitIndex2)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151656,f150969]) ).
fof(f151666,plain,
( v154838(sK54,bitIndex0)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151663,f151164]) ).
fof(f151691,plain,
( ~ v154845(sK54)
| ~ spl55_18 ),
inference(resolution,[],[f151400,f146735]) ).
fof(f151753,plain,
( b0010(bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(resolution,[],[f151665,f145951]) ).
fof(f151761,plain,
( v154841(sK54,bitIndex0)
| ~ range_3_0(bitIndex0)
| v154839(sK54)
| spl55_9
| spl55_12 ),
inference(resolution,[],[f151666,f145953]) ).
fof(f151762,plain,
( b0010(bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(resolution,[],[f151666,f145951]) ).
fof(f151764,plain,
( v154841(sK54,bitIndex0)
| v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151761,f150967]) ).
fof(f151908,plain,
( ~ v154844(sK54,bitIndex2)
| ~ spl55_18 ),
inference(resolution,[],[f151691,f146211]) ).
fof(f151911,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154843(sK54)
| ~ spl55_16 ),
inference(resolution,[],[f151431,f146207]) ).
fof(f151915,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_8
| ~ spl55_45 ),
inference(resolution,[],[f151504,f151640]) ).
fof(f151918,plain,
( ! [X0] :
( v154841(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_45 ),
inference(resolution,[],[f151504,f145908]) ).
fof(f151919,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154841(sK54,X0) )
| ~ spl55_45 ),
inference(duplicate_literal_removal,[],[f151918]) ).
fof(f151992,plain,
( v154843(sK54)
| spl55_31 ),
inference(resolution,[],[f151370,f146732]) ).
fof(f152041,plain,
( ~ range_3_0(bitIndex2)
| ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151753,f146021]) ).
fof(f152042,plain,
( ~ range_3_0(bitIndex0)
| ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f151762,f146019]) ).
fof(f152043,plain,
( v154841(sK54,bitIndex2)
| ~ v154843(sK54)
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f151911,f150969]) ).
fof(f152045,plain,
( v154841(sK54,bitIndex2)
| spl55_8
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f151915,f150969]) ).
fof(f152050,plain,
( ~ v154839(sK54)
| spl55_8
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f152041,f150969]) ).
fof(f152051,plain,
( ~ v154839(sK54)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f152042,f150967]) ).
fof(f152053,definition,
( spl55_72
<=> v154843(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_72])],[avatar_definition]) ).
fof(f152054,plain,
( v154843(sK54)
| ~ spl55_72 ),
inference(avatar_component_clause,[],[f152053]) ).
fof(f152055,plain,
( ~ v154843(sK54)
| spl55_72 ),
inference(avatar_component_clause,[],[f152053]) ).
fof(f152057,definition,
( spl55_73
<=> v154841(sK54,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl55_73])],[avatar_definition]) ).
fof(f152059,plain,
( v154841(sK54,bitIndex2)
| ~ spl55_73 ),
inference(avatar_component_clause,[],[f152057]) ).
fof(f152060,plain,
( ~ spl55_72
| spl55_73
| ~ spl55_16 ),
inference(avatar_split_clause,[],[f152043,f151218,f152057,f152053]) ).
fof(f152061,plain,
( spl55_73
| spl55_8
| ~ spl55_45 ),
inference(avatar_split_clause,[],[f152045,f151503,f151133,f152057]) ).
fof(f152068,plain,
( $false
| spl55_8
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f152050,f151197]) ).
fof(f152069,plain,
( spl55_8
| spl55_9
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f152068]) ).
fof(f152072,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| ~ range_3_0(X0)
| v6(sK54,X0) )
| spl55_9
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f151629,f151196]) ).
fof(f152073,plain,
( v154841(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14 ),
inference(forward_subsumption_resolution,[],[f151764,f151196]) ).
fof(f152092,plain,
( spl55_72
| spl55_31 ),
inference(avatar_split_clause,[],[f151992,f151369,f152053]) ).
fof(f152099,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_14 ),
inference(resolution,[],[f151196,f145954]) ).
fof(f152103,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154842(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_16 ),
inference(resolution,[],[f151219,f146027]) ).
fof(f152262,plain,
( ! [X0] :
( v154842(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| ~ spl55_16 ),
inference(resolution,[],[f152103,f145953]) ).
fof(f152263,plain,
( ! [X0] :
( v154842(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| v154839(sK54) )
| ~ spl55_16 ),
inference(duplicate_literal_removal,[],[f152262]) ).
fof(f152266,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154842(sK54,X0) )
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152263,f151196]) ).
fof(f152388,plain,
( v154838(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_14
| ~ spl55_73 ),
inference(resolution,[],[f152059,f152099]) ).
fof(f152389,plain,
( ~ range_3_0(bitIndex2)
| v6(sK54,bitIndex2)
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(resolution,[],[f152059,f152072]) ).
fof(f152395,plain,
( v154842(sK54,bitIndex0)
| ~ range_3_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f152073,f152103]) ).
fof(f152402,plain,
( v154842(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f152395,f150967]) ).
fof(f152542,plain,
( ~ range_3_0(bitIndex3)
| v154841(sK54,bitIndex3)
| v154852(sK54)
| ~ spl55_45 ),
inference(resolution,[],[f151919,f145910]) ).
fof(f152545,plain,
( ~ range_3_0(bitIndex1)
| v154841(sK54,bitIndex1)
| v154858(sK54)
| ~ spl55_45 ),
inference(resolution,[],[f151919,f145913]) ).
fof(f153657,plain,
( ~ range_1_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f152402,f146208]) ).
fof(f153659,plain,
( $false
| spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153657,f150982]) ).
fof(f153660,plain,
( spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f153659]) ).
fof(f153661,plain,
( v154838(sK54,bitIndex1)
| v154858(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f151661,f150968]) ).
fof(f153662,plain,
( v154841(sK54,bitIndex1)
| v154858(sK54)
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152545,f150968]) ).
fof(f153663,plain,
( v154838(sK54,bitIndex1)
| spl55_9
| spl55_11 ),
inference(forward_subsumption_resolution,[],[f153661,f151160]) ).
fof(f153664,plain,
( v154841(sK54,bitIndex1)
| spl55_11
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f153662,f151160]) ).
fof(f153667,plain,
( v154866(sK54)
| ~ v154853(sK54,bitIndex1)
| ~ spl55_12 ),
inference(resolution,[],[f151163,f145916]) ).
fof(f153670,plain,
( ~ range_3_0(bitIndex1)
| v154842(sK54,bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f153663,f152266]) ).
fof(f153678,plain,
( v154842(sK54,bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153670,f150968]) ).
fof(f153912,plain,
( v154844(sK54,bitIndex1)
| ~ range_3_0(bitIndex1)
| v1051(sK54)
| spl55_11
| ~ spl55_45 ),
inference(resolution,[],[f153664,f146029]) ).
fof(f153920,plain,
( ~ range_1_0(bitIndex1)
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(resolution,[],[f153678,f146208]) ).
fof(f153922,plain,
( $false
| spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(forward_subsumption_resolution,[],[f153920,f150983]) ).
fof(f153923,plain,
( spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(avatar_contradiction_clause,[],[f153922]) ).
fof(f153925,definition,
( spl55_295
<=> v154853(sK54,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl55_295])],[avatar_definition]) ).
fof(f153927,plain,
( ~ v154853(sK54,bitIndex1)
| spl55_295 ),
inference(avatar_component_clause,[],[f153925]) ).
fof(f153929,definition,
( spl55_296
<=> v154866(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_296])],[avatar_definition]) ).
fof(f153932,plain,
( ~ spl55_295
| spl55_296
| ~ spl55_12 ),
inference(avatar_split_clause,[],[f153667,f151162,f153929,f153925]) ).
fof(f153934,plain,
( ~ v154856(sK54)
| spl55_5
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f151637,f151142]) ).
fof(f153937,plain,
( $false
| spl55_5
| ~ spl55_7
| spl55_8 ),
inference(forward_subsumption_resolution,[],[f153934,f151130]) ).
fof(f153938,plain,
( spl55_5
| ~ spl55_7
| spl55_8 ),
inference(avatar_contradiction_clause,[],[f153937]) ).
fof(f153943,plain,
( v6(sK54,bitIndex2)
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f152389,f150969]) ).
fof(f153944,plain,
( v154838(sK54,bitIndex2)
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f152388,f150969]) ).
fof(f153953,plain,
( ~ v154853(sK54,bitIndex2)
| spl55_1 ),
inference(resolution,[],[f151099,f145906]) ).
fof(f153957,plain,
( v154860(sK54)
| ~ v154853(sK54,bitIndex3)
| ~ spl55_3 ),
inference(resolution,[],[f151111,f145914]) ).
fof(f153958,plain,
( v154851(sK54)
| ~ v154852(sK54)
| ~ spl55_3 ),
inference(resolution,[],[f151111,f145903]) ).
fof(f153960,plain,
( ~ v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_1 ),
inference(resolution,[],[f153953,f145909]) ).
fof(f153961,plain,
( ~ range_3_0(bitIndex2)
| spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f153960,f153943]) ).
fof(f153962,plain,
( $false
| spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f153961,f150969]) ).
fof(f153963,plain,
( spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f153962]) ).
fof(f153965,plain,
( ~ v154852(sK54)
| ~ spl55_3
| spl55_4 ),
inference(forward_subsumption_resolution,[],[f153958,f151115]) ).
fof(f153977,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ range_3_0(X0)
| ~ b0010(X0) )
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f151628,f151197]) ).
fof(f153993,plain,
( ~ v154852(sK54)
| ~ v154862(sK54)
| spl55_6 ),
inference(resolution,[],[f151124,f145920]) ).
fof(f153995,plain,
( v154863(sK54)
| ~ v154853(sK54,bitIndex2)
| ~ spl55_7 ),
inference(resolution,[],[f151130,f145915]) ).
fof(f154033,plain,
( v83122(sK54,bitIndex1)
| ~ spl55_17 ),
inference(resolution,[],[f151223,f146204]) ).
fof(f154049,plain,
( ! [X0] :
( ~ range_3_0(X0)
| ~ b0010(X0)
| v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9
| ~ spl55_14 ),
inference(resolution,[],[f153977,f145909]) ).
fof(f154050,plain,
( ! [X0] :
( v154853(sK54,X0)
| ~ b0010(X0)
| ~ range_3_0(X0) )
| spl55_9
| ~ spl55_14 ),
inference(duplicate_literal_removal,[],[f154049]) ).
fof(f154081,plain,
( ~ v154842(sK54,bitIndex2)
| spl55_72 ),
inference(resolution,[],[f152055,f146206]) ).
fof(f154121,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(resolution,[],[f154050,f153927]) ).
fof(f154129,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(resolution,[],[f154050,f145918]) ).
fof(f154135,plain,
( ~ range_3_0(bitIndex1)
| v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154129,f146020]) ).
fof(f154136,plain,
( ~ range_3_0(bitIndex1)
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(forward_subsumption_resolution,[],[f154121,f146020]) ).
fof(f154138,plain,
( v154870(sK54)
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154135,f150968]) ).
fof(f154139,plain,
( $false
| spl55_9
| ~ spl55_14
| spl55_295 ),
inference(forward_subsumption_resolution,[],[f154136,f150968]) ).
fof(f154140,plain,
( spl55_9
| ~ spl55_14
| spl55_295 ),
inference(avatar_contradiction_clause,[],[f154139]) ).
fof(f154142,plain,
( $false
| spl55_1
| spl55_9
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154138,f151101]) ).
fof(f154143,plain,
( spl55_1
| spl55_9
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f154142]) ).
fof(f154146,plain,
( ~ v154853(sK54,bitIndex3)
| spl55_2
| ~ spl55_3 ),
inference(forward_subsumption_resolution,[],[f153957,f151176]) ).
fof(f154148,definition,
( spl55_301
<=> v154853(sK54,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl55_301])],[avatar_definition]) ).
fof(f154150,plain,
( ~ v154853(sK54,bitIndex2)
| spl55_301 ),
inference(avatar_component_clause,[],[f154148]) ).
fof(f154152,definition,
( spl55_302
<=> v154863(sK54) ),
introduced(definition,[new_symbols(definition,[spl55_302])],[avatar_definition]) ).
fof(f154155,plain,
( ~ spl55_301
| spl55_302
| ~ spl55_7 ),
inference(avatar_split_clause,[],[f153995,f151129,f154152,f154148]) ).
fof(f154173,plain,
( v154853(sK54,bitIndex3)
| ~ spl55_3
| spl55_4 ),
inference(resolution,[],[f153965,f145910]) ).
fof(f154174,plain,
( $false
| spl55_2
| ~ spl55_3
| spl55_4 ),
inference(forward_subsumption_resolution,[],[f154173,f154146]) ).
fof(f154175,plain,
( spl55_2
| ~ spl55_3
| spl55_4 ),
inference(avatar_contradiction_clause,[],[f154174]) ).
fof(f154179,plain,
( ~ v154852(sK54)
| ~ spl55_5
| spl55_6 ),
inference(forward_subsumption_resolution,[],[f153993,f151120]) ).
fof(f154187,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v154839(sK54)
| ~ spl55_10 ),
inference(resolution,[],[f151153,f145951]) ).
fof(f154189,plain,
( ~ range_3_0(bitIndex3)
| ~ v154839(sK54)
| ~ spl55_10 ),
inference(forward_subsumption_resolution,[],[f154187,f146022]) ).
fof(f154190,plain,
( ~ v154839(sK54)
| ~ spl55_10 ),
inference(forward_subsumption_resolution,[],[f154189,f150970]) ).
fof(f154191,plain,
( $false
| ~ spl55_10
| ~ spl55_14 ),
inference(forward_subsumption_resolution,[],[f154190,f151197]) ).
fof(f154192,plain,
( ~ spl55_10
| ~ spl55_14 ),
inference(avatar_contradiction_clause,[],[f154191]) ).
fof(f154193,plain,
( spl55_11
| ~ spl55_9 ),
inference(avatar_split_clause,[],[f151557,f151148,f151158]) ).
fof(f154203,plain,
( ! [X0] :
( v6(sK54,X0)
| ~ b0001(X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f151150,f145923]) ).
fof(f154209,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ spl55_13
| ~ spl55_35 ),
inference(resolution,[],[f151191,f151411]) ).
fof(f154212,plain,
( b0001(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v154836(sK54)
| ~ spl55_13 ),
inference(resolution,[],[f151191,f145922]) ).
fof(f154214,plain,
( ~ range_3_0(bitIndex3)
| ~ v154836(sK54)
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154212,f145938]) ).
fof(f154215,plain,
( ~ range_3_0(bitIndex3)
| ~ spl55_13
| ~ spl55_35 ),
inference(forward_subsumption_resolution,[],[f154209,f146022]) ).
fof(f154216,plain,
( ~ v154836(sK54)
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154214,f150970]) ).
fof(f154217,plain,
( $false
| ~ spl55_13
| ~ spl55_35 ),
inference(forward_subsumption_resolution,[],[f154215,f150970]) ).
fof(f154218,plain,
( ~ spl55_13
| ~ spl55_35 ),
inference(avatar_contradiction_clause,[],[f154217]) ).
fof(f154219,plain,
( $false
| ~ spl55_9
| ~ spl55_13 ),
inference(forward_subsumption_resolution,[],[f154216,f151150]) ).
fof(f154220,plain,
( ~ spl55_9
| ~ spl55_13 ),
inference(avatar_contradiction_clause,[],[f154219]) ).
fof(f154260,plain,
( ! [X0] :
( ~ b0001(X0)
| ~ range_3_0(X0)
| v154853(sK54,X0)
| ~ range_3_0(X0) )
| ~ spl55_9 ),
inference(resolution,[],[f154203,f145909]) ).
fof(f154261,plain,
( ! [X0] :
( v154853(sK54,X0)
| ~ range_3_0(X0)
| ~ b0001(X0) )
| ~ spl55_9 ),
inference(duplicate_literal_removal,[],[f154260]) ).
fof(f154274,plain,
( ~ v6(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl55_301 ),
inference(resolution,[],[f154150,f145909]) ).
fof(f154275,plain,
( ~ v6(sK54,bitIndex2)
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154274,f150969]) ).
fof(f154303,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v154870(sK54)
| ~ spl55_9 ),
inference(resolution,[],[f154261,f145919]) ).
fof(f154310,plain,
( ~ b0001(bitIndex0)
| v154870(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154303,f150967]) ).
fof(f154311,plain,
( v154870(sK54)
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154310,f145935]) ).
fof(f154312,plain,
( $false
| spl55_1
| ~ spl55_9 ),
inference(forward_subsumption_resolution,[],[f154311,f151101]) ).
fof(f154313,plain,
( spl55_1
| ~ spl55_9 ),
inference(avatar_contradiction_clause,[],[f154312]) ).
fof(f154314,plain,
( ~ spl55_302
| spl55_5 ),
inference(avatar_split_clause,[],[f151142,f151119,f154152]) ).
fof(f154318,plain,
( ~ spl55_296
| spl55_5
| ~ spl55_8 ),
inference(avatar_split_clause,[],[f151211,f151133,f151119,f153929]) ).
fof(f154319,plain,
( ~ spl55_11
| spl55_5
| ~ spl55_8
| spl55_12 ),
inference(avatar_split_clause,[],[f151562,f151162,f151133,f151119,f151158]) ).
fof(f154320,plain,
( ~ spl55_14
| spl55_9
| spl55_12 ),
inference(avatar_split_clause,[],[f152051,f151162,f151148,f151195]) ).
fof(f154322,plain,
( v154844(sK54,bitIndex1)
| v1051(sK54)
| spl55_11
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f153912,f150968]) ).
fof(f154345,plain,
( v154841(sK54,bitIndex3)
| v154852(sK54)
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f152542,f150970]) ).
fof(f154348,plain,
( v154844(sK54,bitIndex1)
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154322,f151220]) ).
fof(f154421,plain,
( ! [X0] :
( ~ v6(sK54,X0)
| v154838(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f151149,f145924]) ).
fof(f154438,plain,
( ! [X0] :
( v154838(sK54,X0)
| ~ range_3_0(X0)
| ~ v154853(sK54,X0)
| ~ range_3_0(X0) )
| spl55_9 ),
inference(resolution,[],[f154421,f145908]) ).
fof(f154439,plain,
( ! [X0] :
( ~ v154853(sK54,X0)
| ~ range_3_0(X0)
| v154838(sK54,X0) )
| spl55_9 ),
inference(duplicate_literal_removal,[],[f154438]) ).
fof(f154442,plain,
( ! [X0] :
( ~ v154841(sK54,X0)
| v154844(sK54,X0)
| ~ range_3_0(X0) )
| spl55_16 ),
inference(resolution,[],[f151220,f146029]) ).
fof(f154443,plain,
( ! [X0] :
( ~ v154844(sK54,X0)
| v154841(sK54,X0)
| ~ range_3_0(X0) )
| spl55_16 ),
inference(resolution,[],[f151220,f146030]) ).
fof(f154481,plain,
( ~ v154841(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| v1051(sK54)
| spl55_18 ),
inference(resolution,[],[f151229,f146029]) ).
fof(f154504,plain,
( ~ range_3_0(bitIndex0)
| v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(resolution,[],[f154439,f145912]) ).
fof(f154507,plain,
( v154838(sK54,bitIndex0)
| v154857(sK54)
| spl55_9 ),
inference(forward_subsumption_resolution,[],[f154504,f150967]) ).
fof(f154508,plain,
( v154838(sK54,bitIndex0)
| spl55_9
| spl55_12 ),
inference(forward_subsumption_resolution,[],[f154507,f151164]) ).
fof(f154574,plain,
( ~ v154838(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| v154836(sK54)
| spl55_301 ),
inference(resolution,[],[f154275,f145925]) ).
fof(f154577,plain,
( ~ v154838(sK54,bitIndex2)
| v154836(sK54)
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154574,f150969]) ).
fof(f154578,plain,
( ~ v154838(sK54,bitIndex2)
| spl55_9
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f154577,f151149]) ).
fof(f154702,plain,
( ! [X0] :
( v154844(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154839(sK54) )
| spl55_16 ),
inference(resolution,[],[f154442,f145953]) ).
fof(f154703,plain,
( ! [X0] :
( v154844(sK54,X0)
| ~ range_3_0(X0)
| ~ v154838(sK54,X0)
| v154839(sK54) )
| spl55_16 ),
inference(duplicate_literal_removal,[],[f154702]) ).
fof(f154706,plain,
( ! [X0] :
( ~ v154838(sK54,X0)
| ~ range_3_0(X0)
| v154844(sK54,X0) )
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f154703,f151196]) ).
fof(f154713,plain,
( v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v154845(sK54)
| spl55_16 ),
inference(resolution,[],[f154443,f146212]) ).
fof(f154715,plain,
( v154841(sK54,bitIndex2)
| ~ v154845(sK54)
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f154713,f150969]) ).
fof(f154716,plain,
( v154841(sK54,bitIndex2)
| spl55_16
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f154715,f151365]) ).
fof(f154717,plain,
( spl55_73
| spl55_16
| spl55_18 ),
inference(avatar_split_clause,[],[f154716,f151227,f151218,f152057]) ).
fof(f154720,plain,
( $false
| spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(forward_subsumption_resolution,[],[f153944,f154578]) ).
fof(f154721,plain,
( spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(avatar_contradiction_clause,[],[f154720]) ).
fof(f154778,plain,
( ~ v154843(sK54)
| ~ spl55_31 ),
inference(resolution,[],[f151371,f146733]) ).
fof(f154808,plain,
( v154844(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| v1051(sK54)
| ~ spl55_73 ),
inference(resolution,[],[f152059,f146029]) ).
fof(f155005,plain,
( ~ range_3_0(bitIndex0)
| v154844(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(resolution,[],[f154706,f154508]) ).
fof(f155013,plain,
( v154844(sK54,bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f155005,f150967]) ).
fof(f155694,plain,
( ~ v154841(sK54,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v1051(sK54)
| spl55_72 ),
inference(resolution,[],[f154081,f146027]) ).
fof(f155764,plain,
( ~ range_1_0(bitIndex0)
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(resolution,[],[f155013,f146213]) ).
fof(f155766,plain,
( $false
| spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(forward_subsumption_resolution,[],[f155764,f150982]) ).
fof(f155767,plain,
( spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(avatar_contradiction_clause,[],[f155766]) ).
fof(f155772,plain,
( v154852(sK54)
| spl55_15
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f154345,f151201]) ).
fof(f155783,plain,
( $false
| ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f155772,f154179]) ).
fof(f155784,plain,
( ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(avatar_contradiction_clause,[],[f155783]) ).
fof(f155788,plain,
( ~ range_3_0(bitIndex3)
| v1051(sK54)
| ~ spl55_15
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f154481,f151200]) ).
fof(f155789,plain,
( v1051(sK54)
| ~ spl55_15
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f155788,f150970]) ).
fof(f155790,plain,
( $false
| ~ spl55_15
| spl55_16
| spl55_18 ),
inference(forward_subsumption_resolution,[],[f155789,f151220]) ).
fof(f155791,plain,
( ~ spl55_15
| spl55_16
| spl55_18 ),
inference(avatar_contradiction_clause,[],[f155790]) ).
fof(f155798,plain,
( ~ range_3_0(bitIndex2)
| v1051(sK54)
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f154808,f151908]) ).
fof(f155804,plain,
( v1051(sK54)
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155798,f150969]) ).
fof(f155811,plain,
( $false
| spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155804,f151220]) ).
fof(f155812,plain,
( spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f155811]) ).
fof(f155837,plain,
( v154842(sK54,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| ~ spl55_15 ),
inference(resolution,[],[f151200,f146027]) ).
fof(f156706,plain,
( ~ range_1_0(bitIndex1)
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(resolution,[],[f154348,f146213]) ).
fof(f156708,plain,
( $false
| spl55_11
| spl55_16
| ~ spl55_45 ),
inference(forward_subsumption_resolution,[],[f156706,f150983]) ).
fof(f156709,plain,
( spl55_11
| spl55_16
| ~ spl55_45 ),
inference(avatar_contradiction_clause,[],[f156708]) ).
fof(f156720,plain,
( ~ range_3_0(bitIndex2)
| ~ v1051(sK54)
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f155694,f152059]) ).
fof(f156726,plain,
( ~ v1051(sK54)
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f156720,f150969]) ).
fof(f156727,plain,
( $false
| ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(forward_subsumption_resolution,[],[f156726,f151219]) ).
fof(f156728,plain,
( ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(avatar_contradiction_clause,[],[f156727]) ).
fof(f156729,plain,
( $false
| ~ spl55_31
| ~ spl55_72 ),
inference(forward_subsumption_resolution,[],[f154778,f152054]) ).
fof(f156730,plain,
( ~ spl55_31
| ~ spl55_72 ),
inference(avatar_contradiction_clause,[],[f156729]) ).
fof(f156748,plain,
( $false
| ~ spl55_17
| spl55_31 ),
inference(forward_subsumption_resolution,[],[f154033,f151370]) ).
fof(f156749,plain,
( ~ spl55_17
| spl55_31 ),
inference(avatar_contradiction_clause,[],[f156748]) ).
fof(f156762,plain,
( ~ range_3_0(bitIndex3)
| ~ v1051(sK54)
| ~ spl55_15
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f155837,f151224]) ).
fof(f156764,plain,
( ~ v1051(sK54)
| ~ spl55_15
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f156762,f150970]) ).
fof(f156765,plain,
( $false
| ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(forward_subsumption_resolution,[],[f156764,f151219]) ).
fof(f156766,plain,
( ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(avatar_contradiction_clause,[],[f156765]) ).
cnf(s1,plain,
( ~ spl55_1
| ~ spl55_2 ),
inference(sat_conversion,[],[f151097]) ).
cnf(s4,plain,
( spl55_3
| ~ spl55_7
| ~ spl55_8 ),
inference(sat_conversion,[],[f151136]) ).
cnf(s6,plain,
( spl55_1
| spl55_9
| ~ spl55_10 ),
inference(sat_conversion,[],[f151155]) ).
cnf(s7,plain,
( spl55_7
| ~ spl55_11
| ~ spl55_12 ),
inference(sat_conversion,[],[f151165]) ).
cnf(s9,plain,
( spl55_2
| ~ spl55_4 ),
inference(sat_conversion,[],[f151174]) ).
cnf(s10,plain,
( spl55_2
| ~ spl55_6 ),
inference(sat_conversion,[],[f151177]) ).
cnf(s11,plain,
( spl55_9
| spl55_10
| ~ spl55_13 ),
inference(sat_conversion,[],[f151193]) ).
cnf(s12,plain,
( spl55_10
| spl55_14
| ~ spl55_15 ),
inference(sat_conversion,[],[f151202]) ).
cnf(s13,plain,
( spl55_15
| ~ spl55_16
| ~ spl55_17 ),
inference(sat_conversion,[],[f151225]) ).
cnf(s14,plain,
( spl55_15
| spl55_16
| ~ spl55_18 ),
inference(sat_conversion,[],[f151230]) ).
cnf(s19,plain,
( spl55_5
| ~ spl55_8
| spl55_11
| ~ spl55_12 ),
inference(sat_conversion,[],[f151280]) ).
cnf(s26,plain,
( spl55_9
| ~ spl55_14
| spl55_35 ),
inference(sat_conversion,[],[f151412]) ).
cnf(s32,plain,
( spl55_17
| ~ spl55_31 ),
inference(sat_conversion,[],[f151491]) ).
cnf(s33,plain,
( spl55_9
| spl55_14
| spl55_45 ),
inference(sat_conversion,[],[f151505]) ).
cnf(s43,plain,
( ~ spl55_5
| spl55_6
| spl55_13 ),
inference(sat_conversion,[],[f151579]) ).
cnf(s47,plain,
( spl55_8
| ~ spl55_9 ),
inference(sat_conversion,[],[f151593]) ).
cnf(s83,plain,
( ~ spl55_16
| ~ spl55_72
| spl55_73 ),
inference(sat_conversion,[],[f152060]) ).
cnf(s84,plain,
( spl55_8
| ~ spl55_45
| spl55_73 ),
inference(sat_conversion,[],[f152061]) ).
cnf(s88,plain,
( spl55_8
| spl55_9
| ~ spl55_14 ),
inference(sat_conversion,[],[f152069]) ).
cnf(s100,plain,
( spl55_31
| spl55_72 ),
inference(sat_conversion,[],[f152092]) ).
cnf(s197,plain,
( spl55_9
| spl55_12
| spl55_14
| ~ spl55_16 ),
inference(sat_conversion,[],[f153660]) ).
cnf(s219,plain,
( spl55_9
| spl55_11
| spl55_14
| ~ spl55_16 ),
inference(sat_conversion,[],[f153923]) ).
cnf(s220,plain,
( ~ spl55_12
| ~ spl55_295
| spl55_296 ),
inference(sat_conversion,[],[f153932]) ).
cnf(s222,plain,
( spl55_5
| ~ spl55_7
| spl55_8 ),
inference(sat_conversion,[],[f153938]) ).
cnf(s225,plain,
( spl55_1
| spl55_9
| spl55_14
| ~ spl55_73 ),
inference(sat_conversion,[],[f153963]) ).
cnf(s239,plain,
( spl55_9
| ~ spl55_14
| spl55_295 ),
inference(sat_conversion,[],[f154140]) ).
cnf(s240,plain,
( spl55_1
| spl55_9
| ~ spl55_14 ),
inference(sat_conversion,[],[f154143]) ).
cnf(s244,plain,
( ~ spl55_7
| ~ spl55_301
| spl55_302 ),
inference(sat_conversion,[],[f154155]) ).
cnf(s246,plain,
( spl55_2
| ~ spl55_3
| spl55_4 ),
inference(sat_conversion,[],[f154175]) ).
cnf(s247,plain,
( ~ spl55_10
| ~ spl55_14 ),
inference(sat_conversion,[],[f154192]) ).
cnf(s249,plain,
( ~ spl55_9
| spl55_11 ),
inference(sat_conversion,[],[f154193]) ).
cnf(s251,plain,
( ~ spl55_13
| ~ spl55_35 ),
inference(sat_conversion,[],[f154218]) ).
cnf(s252,plain,
( ~ spl55_9
| ~ spl55_13 ),
inference(sat_conversion,[],[f154220]) ).
cnf(s255,plain,
( spl55_1
| ~ spl55_9 ),
inference(sat_conversion,[],[f154313]) ).
cnf(s263,plain,
( spl55_5
| ~ spl55_302 ),
inference(sat_conversion,[],[f154314]) ).
cnf(s267,plain,
( spl55_5
| ~ spl55_8
| ~ spl55_296 ),
inference(sat_conversion,[],[f154318]) ).
cnf(s268,plain,
( spl55_5
| ~ spl55_8
| ~ spl55_11
| spl55_12 ),
inference(sat_conversion,[],[f154319]) ).
cnf(s271,plain,
( spl55_9
| spl55_12
| ~ spl55_14 ),
inference(sat_conversion,[],[f154320]) ).
cnf(s319,plain,
( spl55_16
| spl55_18
| spl55_73 ),
inference(sat_conversion,[],[f154717]) ).
cnf(s321,plain,
( spl55_9
| spl55_14
| ~ spl55_73
| spl55_301 ),
inference(sat_conversion,[],[f154721]) ).
cnf(s431,plain,
( spl55_9
| spl55_12
| spl55_14
| spl55_16 ),
inference(sat_conversion,[],[f155767]) ).
cnf(s436,plain,
( ~ spl55_5
| spl55_6
| spl55_15
| ~ spl55_45 ),
inference(sat_conversion,[],[f155784]) ).
cnf(s438,plain,
( ~ spl55_15
| spl55_16
| spl55_18 ),
inference(sat_conversion,[],[f155791]) ).
cnf(s445,plain,
( spl55_16
| ~ spl55_18
| ~ spl55_73 ),
inference(sat_conversion,[],[f155812]) ).
cnf(s510,plain,
( spl55_11
| spl55_16
| ~ spl55_45 ),
inference(sat_conversion,[],[f156709]) ).
cnf(s514,plain,
( ~ spl55_16
| spl55_72
| ~ spl55_73 ),
inference(sat_conversion,[],[f156728]) ).
cnf(s515,plain,
( ~ spl55_31
| ~ spl55_72 ),
inference(sat_conversion,[],[f156730]) ).
cnf(s526,plain,
( ~ spl55_17
| spl55_31 ),
inference(sat_conversion,[],[f156749]) ).
cnf(s529,plain,
( ~ spl55_15
| ~ spl55_16
| spl55_17 ),
inference(sat_conversion,[],[f156766]) ).
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(f156767,plain,
$false,
inference(avatar_sat_refutation,[],[s585]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV123+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.43 % Computer : n015.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 27 11:45:32 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.51 Running first-order theorem proving
% 0.20/0.51 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
% 12.30/3.45 % (1522461)Detected formulas, will run a generic FOF schedule.
% 12.30/3.45 % (1522471)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1527613877:s2a=on:i=139:gtg=position_2988 on theBenchmark for (2988ds/139Mi)
% 12.30/3.45 % (1522466)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=2523454390:i=141193_2988 on theBenchmark for (2988ds/141193Mi)
% 12.30/3.45 % (1522468)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=1629644693:i=141695:sd=1:nm=32:gsp=on:ss=included_2988 on theBenchmark for (2988ds/141695Mi)
% 12.30/3.45 % (1522470)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=808118552:i=119:av=off:ss=axioms_2988 on theBenchmark for (2988ds/119Mi)
% 12.30/3.45 % (1522469)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=98064680:i=109:sd=1:ins=1:gsp=on:ss=axioms_2988 on theBenchmark for (2988ds/109Mi)
% 12.30/3.45 % (1522467)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=2870128850:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2988 on theBenchmark for (2988ds/134677Mi)
% 12.30/3.45 % (1522472)dis-21_1_sil=8000:lcm=predicate:random_seed=552289896:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2988 on theBenchmark for (2988ds/129Mi)
% 12.30/3.45 % (1522471)Instruction limit reached!
% 12.30/3.45 % (1522471)------------------------------
% 12.30/3.45 % (1522471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/3.45 % (1522471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/3.45 % (1522471)CaDiCaL version: 2.1.3
% 12.30/3.45 % (1522471)Termination reason: Instruction limit
% 12.30/3.45 % (1522471)Termination phase: Property scanning
% 12.30/3.45 % (1522471)Time elapsed: 0.052 s
% 12.30/3.45 % (1522471)Peak memory usage: 205 MB
% 12.30/3.45 % (1522471)Instructions burned: 143 (million)
% 12.30/3.45 % (1522469)Instruction limit reached!
% 12.30/3.45 % (1522469)------------------------------
% 12.30/3.45 % (1522469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/3.45 % (1522469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/3.45 % (1522469)CaDiCaL version: 2.1.3
% 12.30/3.45 % (1522469)Termination reason: Instruction limit
% 12.30/3.45 % (1522469)Termination phase: SInE selection
% 12.30/3.45 % (1522469)Time elapsed: 0.061 s
% 12.30/3.45 % (1522469)Peak memory usage: 205 MB
% 12.30/3.45 % (1522469)Instructions burned: 111 (million)
% 12.30/3.45 % (1522470)Instruction limit reached!
% 12.30/3.45 % (1522470)------------------------------
% 12.30/3.45 % (1522470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/3.45 % (1522470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/3.45 % (1522470)CaDiCaL version: 2.1.3
% 12.30/3.45 % (1522470)Termination reason: Instruction limit
% 12.30/3.45 % (1522470)Termination phase: SInE selection
% 12.30/3.45 % (1522470)Time elapsed: 0.064 s
% 12.30/3.45 % (1522470)Peak memory usage: 205 MB
% 12.30/3.45 % (1522470)Instructions burned: 121 (million)
% 12.30/3.45 % (1522472)Instruction limit reached!
% 12.30/3.45 % (1522472)------------------------------
% 12.30/3.45 % (1522472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/3.46 % (1522472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/3.46 % (1522472)CaDiCaL version: 2.1.3
% 12.30/3.46 % (1522472)Termination reason: Instruction limit
% 12.30/3.46 % (1522472)Termination phase: SInE selection
% 12.30/3.46 % (1522472)Time elapsed: 0.067 s
% 12.30/3.46 % (1522472)Peak memory usage: 205 MB
% 12.30/3.46 % (1522472)Instructions burned: 129 (million)
% 12.30/3.46 % (1522480)lrs+10_1_sil=8000:sp=occurrence:random_seed=2396741773:i=285:sd=3:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/285Mi)
% 12.30/3.46 % (1522483)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=522996394:s2a=on:i=248:s2at=1.23:gtg=position_2986 on theBenchmark for (2986ds/248Mi)
% 12.30/3.46 % (1522482)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1055248922:i=325:sd=1:ss=axioms:sgt=32_2986 on theBenchmark for (2986ds/325Mi)
% 12.30/3.46 % (1522481)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3504583258:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2986 on theBenchmark for (2986ds/157Mi)
% 12.30/3.46 % (1522480)Instruction limit reached!
% 19.35/4.45 % (1522480)------------------------------
% 19.35/4.45 % (1522480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/4.45 % (1522480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/4.45 % (1522480)CaDiCaL version: 2.1.3
% 19.35/4.45 % (1522480)Termination reason: Instruction limit
% 19.35/4.45 % (1522480)Termination phase: SInE selection
% 19.35/4.45 % (1522480)Time elapsed: 0.071 s
% 19.35/4.45 % (1522480)Peak memory usage: 205 MB
% 19.35/4.45 % (1522480)Instructions burned: 286 (million)
% 19.35/4.45 % (1522481)Instruction limit reached!
% 19.35/4.45 % (1522481)------------------------------
% 19.35/4.45 % (1522481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/4.45 % (1522481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/4.45 % (1522481)CaDiCaL version: 2.1.3
% 19.35/4.45 % (1522481)Termination reason: Instruction limit
% 19.35/4.45 % (1522481)Termination phase: Property scanning
% 19.35/4.45 % (1522481)Time elapsed: 0.099 s
% 19.35/4.45 % (1522481)Peak memory usage: 205 MB
% 19.35/4.45 % (1522481)Instructions burned: 158 (million)
% 19.35/4.45 % (1522483)Instruction limit reached!
% 19.35/4.45 % (1522483)------------------------------
% 19.35/4.45 % (1522483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/4.45 % (1522483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/4.45 % (1522483)CaDiCaL version: 2.1.3
% 19.35/4.45 % (1522483)Termination reason: Instruction limit
% 19.35/4.45 % (1522483)Termination phase: Property scanning
% 19.35/4.45 % (1522483)Time elapsed: 0.139 s
% 19.35/4.45 % (1522483)Peak memory usage: 205 MB
% 19.35/4.45 % (1522483)Instructions burned: 250 (million)
% 19.35/4.45 % (1522488)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4164413252:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2984 on theBenchmark for (2984ds/294Mi)
% 19.35/4.45 % (1522482)Instruction limit reached!
% 19.35/4.45 % (1522482)------------------------------
% 19.35/4.45 % (1522482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/4.45 % (1522482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/4.45 % (1522482)CaDiCaL version: 2.1.3
% 19.35/4.45 % (1522482)Termination reason: Instruction limit
% 19.35/4.45 % (1522482)Termination phase: SInE selection
% 19.35/4.45 % (1522482)Time elapsed: 0.146 s
% 19.35/4.45 % (1522482)Peak memory usage: 205 MB
% 19.35/4.45 % (1522482)Instructions burned: 326 (million)
% 19.35/4.45 % (1522488)Instruction limit reached!
% 19.35/4.45 % (1522488)------------------------------
% 19.35/4.45 % (1522488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/4.45 % (1522488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/4.45 % (1522488)CaDiCaL version: 2.1.3
% 19.35/4.45 % (1522488)Termination reason: Instruction limit
% 19.35/4.45 % (1522488)Termination phase: SInE selection
% 19.35/4.45 % (1522488)Time elapsed: 0.073 s
% 19.35/4.45 % (1522488)Peak memory usage: 205 MB
% 19.35/4.45 % (1522488)Instructions burned: 297 (million)
% 19.35/4.45 % (1522489)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2698441222:i=2350_2983 on theBenchmark for (2983ds/2350Mi)
% 19.35/4.45 % (1522492)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1315415566:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 19.35/4.45 % (1522491)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2095233692:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 19.35/4.45 % (1522493)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2918728658:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2982 on theBenchmark for (2982ds/114Mi)
% 19.35/4.45 % (1522491)Instruction limit reached!
% 19.35/4.45 % (1522491)------------------------------
% 19.35/4.45 % (1522491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.35/4.45 % (1522491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.35/4.45 % (1522491)CaDiCaL version: 2.1.3
% 19.35/4.45 % (1522491)Termination reason: Instruction limit
% 19.35/4.45 % (1522491)Termination phase: SInE selection
% 19.35/4.45 % (1522491)Time elapsed: 0.064 s
% 19.35/4.45 % (1522491)Peak memory usage: 205 MB
% 19.35/4.45 % (1522491)Instructions burned: 113 (million)
% 19.35/4.45 % (1522493)Instruction limit reached!
% 19.35/4.45 % (1522493)------------------------------
% 19.35/4.45 % (1522493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.75 % (1522493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.75 % (1522493)CaDiCaL version: 2.1.3
% 21.46/4.75 % (1522493)Termination reason: Instruction limit
% 21.46/4.75 % (1522493)Termination phase: Property scanning
% 21.46/4.75 % (1522493)Time elapsed: 0.047 s
% 21.46/4.75 % (1522493)Peak memory usage: 205 MB
% 21.46/4.75 % (1522493)Instructions burned: 115 (million)
% 21.46/4.75 % (1522492)Instruction limit reached!
% 21.46/4.75 % (1522492)------------------------------
% 21.46/4.75 % (1522492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.75 % (1522492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.75 % (1522492)CaDiCaL version: 2.1.3
% 21.46/4.75 % (1522492)Termination reason: Instruction limit
% 21.46/4.75 % (1522492)Termination phase: Preprocessing 1
% 21.46/4.75 % (1522492)Time elapsed: 0.098 s
% 21.46/4.75 % (1522492)Peak memory usage: 205 MB
% 21.46/4.75 % (1522492)Instructions burned: 128 (million)
% 21.46/4.75 % (1522499)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3438376897:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 21.46/4.75 % (1522498)lrs+10_1_sil=8000:sp=occurrence:random_seed=613752550:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2981 on theBenchmark for (2981ds/907Mi)
% 21.46/4.75 % (1522500)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2487524169:i=5202:ss=axioms:sgt=16_2980 on theBenchmark for (2980ds/5202Mi)
% 21.46/4.75 % (1522499)Instruction limit reached!
% 21.46/4.75 % (1522499)------------------------------
% 21.46/4.75 % (1522499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.75 % (1522499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.75 % (1522499)CaDiCaL version: 2.1.3
% 21.46/4.75 % (1522499)Termination reason: Instruction limit
% 21.46/4.75 % (1522499)Termination phase: SInE selection
% 21.46/4.75 % (1522499)Time elapsed: 0.119 s
% 21.46/4.75 % (1522499)Peak memory usage: 212 MB
% 21.46/4.75 % (1522499)Instructions burned: 438 (million)
% 21.46/4.75 % (1522505)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2718131770:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 21.46/4.75 % (1522505)Instruction limit reached!
% 21.46/4.75 % (1522505)------------------------------
% 21.46/4.75 % (1522505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.75 % (1522505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.75 % (1522505)CaDiCaL version: 2.1.3
% 21.46/4.75 % (1522505)Termination reason: Instruction limit
% 21.46/4.75 % (1522505)Termination phase: SInE selection
% 21.46/4.75 % (1522505)Time elapsed: 0.040 s
% 21.46/4.75 % (1522505)Peak memory usage: 205 MB
% 21.46/4.75 % (1522505)Instructions burned: 138 (million)
% 21.46/4.75 % (1522507)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=388824128:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 21.46/4.75 % (1522498)Instruction limit reached!
% 21.46/4.75 % (1522498)------------------------------
% 21.46/4.75 % (1522498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.75 % (1522498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.75 % (1522498)CaDiCaL version: 2.1.3
% 21.46/4.75 % (1522498)Termination reason: Instruction limit
% 21.46/4.75 % (1522498)Termination phase: Saturation
% 21.46/4.75 % (1522498)Time elapsed: 0.500 s
% 21.46/4.75 % (1522498)Peak memory usage: 259 MB
% 21.46/4.75 % (1522498)Instructions burned: 907 (million)
% 21.46/4.75 % (1522507)Instruction limit reached!
% 21.46/4.75 % (1522507)------------------------------
% 21.46/4.75 % (1522507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.46/4.75 % (1522507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.46/4.75 % (1522507)CaDiCaL version: 2.1.3
% 21.46/4.75 % (1522507)Termination reason: Instruction limit
% 21.46/4.75 % (1522507)Termination phase: SInE selection
% 21.46/4.75 % (1522507)Time elapsed: 0.130 s
% 21.46/4.75 % (1522507)Peak memory usage: 207 MB
% 21.46/4.75 % (1522507)Instructions burned: 594 (million)
% 21.46/4.75 % (1522509)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3295984528:st=3:i=13193:sd=3:ss=axioms_2974 on theBenchmark for (2974ds/13193Mi)
% 21.46/4.75 % (1522510)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=755224082:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 35.38/6.73 % (1522510)Instruction limit reached!
% 35.38/6.73 % (1522510)------------------------------
% 35.38/6.73 % (1522510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.38/6.73 % (1522510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.38/6.73 % (1522510)CaDiCaL version: 2.1.3
% 35.38/6.73 % (1522510)Termination reason: Instruction limit
% 35.38/6.73 % (1522510)Termination phase: Property scanning
% 35.38/6.73 % (1522510)Time elapsed: 0.050 s
% 35.38/6.73 % (1522510)Peak memory usage: 205 MB
% 35.38/6.73 % (1522510)Instructions burned: 129 (million)
% 35.38/6.73 % (1522513)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3228045570:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 35.38/6.73 % (1522513)Instruction limit reached!
% 35.38/6.73 % (1522513)------------------------------
% 35.38/6.73 % (1522513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.38/6.73 % (1522513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.38/6.73 % (1522513)CaDiCaL version: 2.1.3
% 35.38/6.73 % (1522513)Termination reason: Instruction limit
% 35.38/6.73 % (1522513)Termination phase: Property scanning
% 35.38/6.73 % (1522513)Time elapsed: 0.052 s
% 35.38/6.73 % (1522513)Peak memory usage: 205 MB
% 35.38/6.73 % (1522513)Instructions burned: 136 (million)
% 35.38/6.73 % (1522489)Instruction limit reached!
% 35.38/6.73 % (1522489)------------------------------
% 35.38/6.73 % (1522489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.38/6.73 % (1522489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.38/6.73 % (1522489)CaDiCaL version: 2.1.3
% 35.38/6.73 % (1522489)Termination reason: Instruction limit
% 35.38/6.73 % (1522489)Termination phase: Preprocessing 3
% 35.38/6.73 % (1522489)Time elapsed: 1.311 s
% 35.38/6.73 % (1522489)Peak memory usage: 285 MB
% 35.38/6.73 % (1522489)Instructions burned: 2350 (million)
% 35.38/6.73 % (1522515)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3700355631:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/141Mi)
% 35.38/6.73 % (1522515)Instruction limit reached!
% 35.38/6.73 % (1522515)------------------------------
% 35.38/6.73 % (1522515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.38/6.73 % (1522515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.38/6.73 % (1522515)CaDiCaL version: 2.1.3
% 35.38/6.73 % (1522515)Termination reason: Instruction limit
% 35.38/6.73 % (1522515)Termination phase: SInE selection
% 35.38/6.73 % (1522515)Time elapsed: 0.042 s
% 35.38/6.73 % (1522515)Peak memory usage: 205 MB
% 35.38/6.73 % (1522515)Instructions burned: 146 (million)
% 35.38/6.73 % (1522517)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=316863114:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2968 on theBenchmark for (2968ds/431Mi)
% 35.38/6.73 % (1522518)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=1405285859:i=6060:aac=none:ins=25_2968 on theBenchmark for (2968ds/6060Mi)
% 35.38/6.73 % (1522517)Instruction limit reached!
% 35.38/6.73 % (1522517)------------------------------
% 35.38/6.73 % (1522517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.38/6.73 % (1522517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.38/6.73 % (1522517)CaDiCaL version: 2.1.3
% 35.38/6.73 % (1522517)Termination reason: Instruction limit
% 35.38/6.73 % (1522517)Termination phase: SInE selection
% 35.38/6.73 % (1522517)Time elapsed: 0.181 s
% 35.38/6.73 % (1522517)Peak memory usage: 207 MB
% 35.38/6.73 % (1522517)Instructions burned: 433 (million)
% 35.38/6.73 % (1522521)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=2778845070:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2965 on theBenchmark for (2965ds/150Mi)
% 35.38/6.73 % (1522521)Instruction limit reached!
% 35.38/6.73 % (1522521)------------------------------
% 35.38/6.73 % (1522521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.38/6.73 % (1522521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.38/6.73 % (1522521)CaDiCaL version: 2.1.3
% 35.38/6.73 % (1522521)Termination reason: Instruction limit
% 78.40/12.75 % (1522521)Termination phase: SInE selection
% 78.40/12.75 % (1522521)Time elapsed: 0.079 s
% 78.40/12.75 % (1522521)Peak memory usage: 205 MB
% 78.40/12.75 % (1522521)Instructions burned: 151 (million)
% 78.40/12.75 % (1522523)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2186258287:i=14155:bd=all_2962 on theBenchmark for (2962ds/14155Mi)
% 78.40/12.75 [W927 11:45:36.544288037 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.
% 78.40/12.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.75 [W927 11:45:36.544335568 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.
% 78.40/12.75 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.75 [W927 11:45:36.544380774 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544394431 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544420888 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544432645 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544460218 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544471978 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544499235 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544510712 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544538072 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 78.40/12.76 [W927 11:45:36.544549256 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.
% 78.40/12.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 91.97/16.36 % (1522500)Instruction limit reached!
% 91.97/16.36 % (1522500)------------------------------
% 91.97/16.36 % (1522500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.97/16.36 % (1522500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.97/16.36 % (1522500)CaDiCaL version: 2.1.3
% 91.97/16.36 % (1522500)Termination reason: Instruction limit
% 91.97/16.36 % (1522500)Termination phase: Saturation
% 91.97/16.36 % (1522500)Time elapsed: 2.976 s
% 91.97/16.36 % (1522500)Peak memory usage: 333 MB
% 91.97/16.36 % (1522500)Instructions burned: 5202 (million)
% 91.97/16.36 % (1522518)Instruction limit reached!
% 91.97/16.36 % (1522518)------------------------------
% 91.97/16.36 % (1522518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.97/16.36 % (1522518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.97/16.36 % (1522518)CaDiCaL version: 2.1.3
% 91.97/16.36 % (1522518)Termination reason: Instruction limit
% 91.97/16.36 % (1522518)Termination phase: Property scanning
% 91.97/16.36 % (1522518)Time elapsed: 1.908 s
% 91.97/16.36 % (1522518)Peak memory usage: 357 MB
% 91.97/16.36 % (1522518)Instructions burned: 6063 (million)
% 91.97/16.36 % (1522525)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=4246097644:i=667:av=off:fsr=off_2948 on theBenchmark for (2948ds/667Mi)
% 91.97/16.36 % (1522526)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=2888327186:s2a=on:i=185:s2at=1.8:fdi=4_2947 on theBenchmark for (2947ds/185Mi)
% 91.97/16.36 % (1522526)Instruction limit reached!
% 91.97/16.36 % (1522526)------------------------------
% 91.97/16.36 % (1522526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.97/16.36 % (1522526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.97/16.36 % (1522526)CaDiCaL version: 2.1.3
% 91.97/16.36 % (1522526)Termination reason: Instruction limit
% 91.97/16.36 % (1522526)Termination phase: SInE selection
% 91.97/16.36 % (1522526)Time elapsed: 0.051 s
% 91.97/16.36 % (1522526)Peak memory usage: 205 MB
% 91.97/16.36 % (1522526)Instructions burned: 189 (million)
% 91.97/16.36 % (1522529)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1519464567:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2945 on theBenchmark for (2945ds/193Mi)
% 91.97/16.36 % (1522529)Instruction limit reached!
% 91.97/16.36 % (1522529)------------------------------
% 91.97/16.36 % (1522529)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.97/16.36 % (1522529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.97/16.36 % (1522529)CaDiCaL version: 2.1.3
% 91.97/16.36 % (1522529)Termination reason: Instruction limit
% 91.97/16.36 % (1522529)Termination phase: SInE selection
% 91.97/16.36 % (1522529)Time elapsed: 0.053 s
% 91.97/16.36 % (1522529)Peak memory usage: 205 MB
% 91.97/16.36 % (1522529)Instructions burned: 196 (million)
% 91.97/16.36 % (1522531)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=5902886:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2943 on theBenchmark for (2943ds/4850Mi)
% 91.97/16.36 % (1522525)Instruction limit reached!
% 91.97/16.36 % (1522525)------------------------------
% 91.97/16.36 % (1522525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.97/16.36 % (1522525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.97/16.36 % (1522525)CaDiCaL version: 2.1.3
% 91.97/16.36 % (1522525)Termination reason: Instruction limit
% 91.97/16.36 % (1522525)Termination phase: Preprocessing 2
% 91.97/16.36 % (1522525)Time elapsed: 0.523 s
% 91.97/16.36 % (1522525)Peak memory usage: 257 MB
% 91.97/16.36 % (1522525)Instructions burned: 668 (million)
% 91.97/16.36 % (1522509)Refutation not found, incomplete strategy
% 91.97/16.36 % (1522509)------------------------------
% 91.97/16.36 % (1522509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 91.97/16.36 % (1522509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.97/16.36 % (1522509)CaDiCaL version: 2.1.3
% 91.97/16.36 % (1522509)Termination reason: Refutation not found, incomplete strategy
% 91.97/16.36 % (1522509)Time elapsed: 3.190 s
% 91.97/16.36 % (1522509)Peak memory usage: 635 MB
% 91.97/16.36 % (1522509)Instructions burned: 4881 (million)
% 91.97/16.36 % (1522533)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3253949737:i=12111:sd=1:ss=included_2941 on theBenchmark for (2941ds/12111Mi)
% 115.25/17.97 % (1522509)------------------------------
% 115.25/17.97 % (1522509)------------------------------
% 115.25/17.97 % (1522535)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4046199840:i=319:kws=precedence:fsr=off_2937 on theBenchmark for (2937ds/319Mi)
% 115.25/17.97 % (1522535)Instruction limit reached!
% 115.25/17.97 % (1522535)------------------------------
% 115.25/17.97 % (1522535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.25/17.97 % (1522535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.25/17.97 % (1522535)CaDiCaL version: 2.1.3
% 115.25/17.97 % (1522535)Termination reason: Instruction limit
% 115.25/17.97 % (1522535)Termination phase: Preprocessing 1
% 115.25/17.97 % (1522535)Time elapsed: 0.233 s
% 115.25/17.97 % (1522535)Peak memory usage: 206 MB
% 115.25/17.97 % (1522535)Instructions burned: 320 (million)
% 115.25/17.97 % (1522537)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3183692233:i=2064:ep=RST_2932 on theBenchmark for (2932ds/2064Mi)
% 115.25/17.97 % (1522531)Instruction limit reached!
% 115.25/17.97 % (1522531)------------------------------
% 115.25/17.97 % (1522531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.25/17.97 % (1522531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.25/17.97 % (1522531)CaDiCaL version: 2.1.3
% 115.25/17.97 % (1522531)Termination reason: Instruction limit
% 115.25/17.97 % (1522531)Termination phase: Property scanning
% 115.25/17.97 % (1522531)Time elapsed: 1.626 s
% 115.25/17.97 % (1522531)Peak memory usage: 392 MB
% 115.25/17.97 % (1522531)Instructions burned: 4855 (million)
% 115.25/17.97 % (1522539)dis-1011_128_sil=32000:random_seed=3450747876:i=3706:ep=RST:av=off_2925 on theBenchmark for (2925ds/3706Mi)
% 115.25/17.97 % (1522537)Instruction limit reached!
% 115.25/17.97 % (1522537)------------------------------
% 115.25/17.97 % (1522537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.25/17.97 % (1522537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.25/17.97 % (1522537)CaDiCaL version: 2.1.3
% 115.25/17.97 % (1522537)Termination reason: Instruction limit
% 115.25/17.97 % (1522537)Termination phase: Preprocessing 3
% 115.25/17.97 % (1522537)Time elapsed: 1.306 s
% 115.25/17.97 % (1522537)Peak memory usage: 317 MB
% 115.25/17.97 % (1522537)Instructions burned: 2065 (million)
% 115.25/17.97 % (1522541)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1817883577:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2917 on theBenchmark for (2917ds/757Mi)
% 115.25/17.97 % (1522539)Instruction limit reached!
% 115.25/17.97 % (1522539)------------------------------
% 115.25/17.97 % (1522539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.25/17.97 % (1522539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.25/17.97 % (1522539)CaDiCaL version: 2.1.3
% 115.25/17.97 % (1522539)Termination reason: Instruction limit
% 115.25/17.97 % (1522539)Termination phase: Property scanning
% 115.25/17.97 % (1522539)Time elapsed: 1.226 s
% 115.25/17.97 % (1522539)Peak memory usage: 392 MB
% 115.25/17.97 % (1522539)Instructions burned: 3711 (million)
% 115.25/17.97 % (1522541)Refutation not found, incomplete strategy
% 115.25/17.97 % (1522541)------------------------------
% 115.25/17.97 % (1522541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.25/17.97 % (1522541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.25/17.97 % (1522541)CaDiCaL version: 2.1.3
% 115.25/17.97 % (1522541)Termination reason: Refutation not found, incomplete strategy
% 115.25/17.97 % (1522541)Time elapsed: 0.422 s
% 115.25/17.97 % (1522541)Peak memory usage: 259 MB
% 115.25/17.97 % (1522541)Instructions burned: 724 (million)
% 115.25/17.97 % (1522543)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1328762331:i=13913:ss=axioms:sgt=8_2912 on theBenchmark for (2912ds/13913Mi)
% 115.25/17.97 % (1522541)------------------------------
% 115.25/17.97 % (1522541)------------------------------
% 115.25/17.97 % (1522545)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=971338855:i=9925:aac=none_2908 on theBenchmark for (2908ds/9925Mi)
% 115.25/17.97 % (1522543)Refutation not found, incomplete strategy
% 115.25/17.97 % (1522543)------------------------------
% 115.25/17.97 % (1522543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 115.25/17.97 % (1522543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.25/17.97 % (1522543)CaDiCaL version: 2.1.3
% 133.73/20.56 % (1522543)Termination reason: Refutation not found, incomplete strategy
% 133.73/20.56 % (1522543)Time elapsed: 3.078 s
% 133.73/20.56 % (1522543)Peak memory usage: 580 MB
% 133.73/20.56 % (1522543)Instructions burned: 4438 (million)
% 133.73/20.56 % (1522543)------------------------------
% 133.73/20.56 % (1522543)------------------------------
% 133.73/20.56 % (1522547)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4112096032:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2875 on theBenchmark for (2875ds/2479Mi)
% 133.73/20.56 % (1522547)Refutation not found, incomplete strategy
% 133.73/20.56 % (1522547)------------------------------
% 133.73/20.56 % (1522547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.73/20.56 % (1522547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.73/20.56 % (1522547)CaDiCaL version: 2.1.3
% 133.73/20.56 % (1522547)Termination reason: Refutation not found, incomplete strategy
% 133.73/20.56 % (1522547)Time elapsed: 0.736 s
% 133.73/20.56 % (1522547)Peak memory usage: 258 MB
% 133.73/20.56 % (1522547)Instructions burned: 1651 (million)
% 133.73/20.56 % (1522547)------------------------------
% 133.73/20.56 % (1522547)------------------------------
% 133.73/20.56 % (1522549)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4233350010:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2863 on theBenchmark for (2863ds/440Mi)
% 133.73/20.56 % (1522549)Instruction limit reached!
% 133.73/20.56 % (1522549)------------------------------
% 133.73/20.56 % (1522549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.73/20.56 % (1522549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.73/20.56 % (1522549)CaDiCaL version: 2.1.3
% 133.73/20.56 % (1522549)Termination reason: Instruction limit
% 133.73/20.56 % (1522549)Termination phase: Property scanning
% 133.73/20.56 % (1522549)Time elapsed: 0.217 s
% 133.73/20.56 % (1522549)Peak memory usage: 205 MB
% 133.73/20.56 % (1522549)Instructions burned: 443 (million)
% 133.73/20.56 % (1522551)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2679048745:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2859 on theBenchmark for (2859ds/11145Mi)
% 133.73/20.56 % (1522523)Instruction limit reached!
% 133.73/20.56 % (1522523)------------------------------
% 133.73/20.56 % (1522523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.73/20.56 % (1522523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.73/20.56 % (1522523)CaDiCaL version: 2.1.3
% 133.73/20.56 % (1522523)Termination reason: Instruction limit
% 133.73/20.56 % (1522523)Termination phase: Saturation
% 133.73/20.56 % (1522523)Time elapsed: 11.603 s
% 133.73/20.56 % (1522523)Peak memory usage: 1221 MB
% 133.73/20.56 % (1522523)Instructions burned: 14156 (million)
% 133.73/20.56 [W927 11:45:48.156702068 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.
% 133.73/20.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.73/20.56 [W927 11:45:48.156749698 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.
% 133.73/20.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.73/20.56 [W927 11:45:48.156800209 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.
% 133.73/20.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.73/20.56 [W927 11:45:48.156814132 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.
% 133.73/20.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.73/20.56 [W927 11:45:48.156841096 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.
% 133.73/20.56 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.73/20.56 [W927 11:45:48.156853489 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 [W927 11:45:48.156879206 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 [W927 11:45:48.156890283 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 [W927 11:45:48.156975097 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 [W927 11:45:48.156992503 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 [W927 11:45:48.157032130 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 [W927 11:45:48.157043217 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.
% 77.40/21.92 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 77.40/21.92 % (1522553)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=1519091470:cts=off:i=3034:av=off:er=known:fsd=on_2843 on theBenchmark for (2843ds/3034Mi)
% 77.40/21.92 % (1522553)Instruction limit reached!
% 77.40/21.92 % (1522553)------------------------------
% 77.40/21.92 % (1522553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522553)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522553)Termination reason: Instruction limit
% 77.40/21.92 % (1522553)Termination phase: Preprocessing 3
% 77.40/21.92 % (1522553)Time elapsed: 1.036 s
% 77.40/21.92 % (1522553)Peak memory usage: 345 MB
% 77.40/21.92 % (1522553)Instructions burned: 3037 (million)
% 77.40/21.92 % (1522555)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=572841843:st=2:s2a=on:i=524:s2at=2:ss=axioms_2831 on theBenchmark for (2831ds/524Mi)
% 77.40/21.92 % (1522555)Instruction limit reached!
% 77.40/21.92 % (1522555)------------------------------
% 77.40/21.92 % (1522555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522555)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522555)Termination reason: Instruction limit
% 77.40/21.92 % (1522555)Termination phase: SInE selection
% 77.40/21.92 % (1522555)Time elapsed: 0.121 s
% 77.40/21.92 % (1522555)Peak memory usage: 206 MB
% 77.40/21.92 % (1522555)Instructions burned: 525 (million)
% 77.40/21.92 % (1522557)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2176451455:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2829 on theBenchmark for (2829ds/1016Mi)
% 77.40/21.92 % (1522533)Instruction limit reached!
% 77.40/21.92 % (1522533)------------------------------
% 77.40/21.92 % (1522533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522533)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522533)Termination reason: Instruction limit
% 77.40/21.92 % (1522533)Termination phase: Saturation
% 77.40/21.92 % (1522533)Time elapsed: 11.239 s
% 77.40/21.92 % (1522533)Peak memory usage: 1219 MB
% 77.40/21.92 % (1522533)Instructions burned: 12111 (million)
% 77.40/21.92 % (1522557)Refutation not found, incomplete strategy
% 77.40/21.92 % (1522557)------------------------------
% 77.40/21.92 % (1522557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522557)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522557)Termination reason: Refutation not found, incomplete strategy
% 77.40/21.92 % (1522557)Time elapsed: 0.276 s
% 77.40/21.92 % (1522557)Peak memory usage: 258 MB
% 77.40/21.92 % (1522557)Instructions burned: 882 (million)
% 77.40/21.92 % (1522551)Refutation not found, incomplete strategy
% 77.40/21.92 % (1522551)------------------------------
% 77.40/21.92 % (1522551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522551)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522551)Termination reason: Refutation not found, incomplete strategy
% 77.40/21.92 % (1522551)Time elapsed: 3.327 s
% 77.40/21.92 % (1522551)Peak memory usage: 601 MB
% 77.40/21.92 % (1522551)Instructions burned: 5244 (million)
% 77.40/21.92 % (1522559)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1194524822:i=14123:bd=preordered:ins=4_2826 on theBenchmark for (2826ds/14123Mi)
% 77.40/21.92 % (1522557)------------------------------
% 77.40/21.92 % (1522557)------------------------------
% 77.40/21.92 % (1522561)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=32538146:i=5781:kws=precedence:bd=all:rawr=on_2822 on theBenchmark for (2822ds/5781Mi)
% 77.40/21.92 % (1522551)------------------------------
% 77.40/21.92 % (1522551)------------------------------
% 77.40/21.92 % (1522563)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=1872081049:i=2448:gtgl=5:bd=preordered:gtg=all_2820 on theBenchmark for (2820ds/2448Mi)
% 77.40/21.92 % (1522545)Instruction limit reached!
% 77.40/21.92 % (1522545)------------------------------
% 77.40/21.92 % (1522545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522545)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522545)Termination reason: Instruction limit
% 77.40/21.92 % (1522545)Termination phase: Saturation
% 77.40/21.92 % (1522545)Time elapsed: 8.884 s
% 77.40/21.92 % (1522545)Peak memory usage: 1149 MB
% 77.40/21.92 % (1522545)Instructions burned: 9927 (million)
% 77.40/21.92 % (1522565)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2128647949:i=3223:kws=precedence:fgj=on:av=off_2816 on theBenchmark for (2816ds/3223Mi)
% 77.40/21.92 % (1522563)Instruction limit reached!
% 77.40/21.92 % (1522563)------------------------------
% 77.40/21.92 % (1522563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522563)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522563)Termination reason: Instruction limit
% 77.40/21.92 % (1522563)Termination phase: Preprocessing 1
% 77.40/21.92 % (1522563)Time elapsed: 1.014 s
% 77.40/21.92 % (1522563)Peak memory usage: 210 MB
% 77.40/21.92 % (1522563)Instructions burned: 2448 (million)
% 77.40/21.92 % (1522567)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=230192550:st=5.6:i=2033:sd=3:ss=axioms_2808 on theBenchmark for (2808ds/2033Mi)
% 77.40/21.92 % (1522561)Instruction limit reached!
% 77.40/21.92 % (1522561)------------------------------
% 77.40/21.92 % (1522561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522561)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522561)Termination reason: Instruction limit
% 77.40/21.92 % (1522561)Termination phase: Saturation
% 77.40/21.92 % (1522561)Time elapsed: 1.794 s
% 77.40/21.92 % (1522561)Peak memory usage: 394 MB
% 77.40/21.92 % (1522561)Instructions burned: 5786 (million)
% 77.40/21.92 % (1522569)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=595176292:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2802 on theBenchmark for (2802ds/2055Mi)
% 77.40/21.92 % (1522567)Instruction limit reached!
% 77.40/21.92 % (1522567)------------------------------
% 77.40/21.92 % (1522567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522567)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522567)Termination reason: Instruction limit
% 77.40/21.92 % (1522567)Termination phase: Saturation
% 77.40/21.92 % (1522567)Time elapsed: 0.965 s
% 77.40/21.92 % (1522567)Peak memory usage: 263 MB
% 77.40/21.92 % (1522567)Instructions burned: 2033 (million)
% 77.40/21.92 % (1522569)Instruction limit reached!
% 77.40/21.92 % (1522569)------------------------------
% 77.40/21.92 % (1522569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522569)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522569)Termination reason: Instruction limit
% 77.40/21.92 % (1522569)Termination phase: SInE selection
% 77.40/21.92 % (1522569)Time elapsed: 0.458 s
% 77.40/21.92 % (1522569)Peak memory usage: 209 MB
% 77.40/21.92 % (1522569)Instructions burned: 2056 (million)
% 77.40/21.92 % (1522572)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3606822287:i=4835:sd=13:ss=axioms:sgt=23_2796 on theBenchmark for (2796ds/4835Mi)
% 77.40/21.92 % (1522571)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=3873990848:i=21611:sd=3:ss=axioms_2796 on theBenchmark for (2796ds/21611Mi)
% 77.40/21.92 % (1522565)Instruction limit reached!
% 77.40/21.92 % (1522565)------------------------------
% 77.40/21.92 % (1522565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.40/21.92 % (1522565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.40/21.92 % (1522565)CaDiCaL version: 2.1.3
% 77.40/21.92 % (1522565)Termination reason: Instruction limit
% 77.40/21.92 % (1522565)Termination phase: Clausification
% 77.40/21.92 % (1522565)Time elapsed: 2.020 s
% 77.40/21.92 % (1522565)Peak memory usage: 370 MB
% 77.40/21.92 % (1522565)Instructions burned: 3223 (million)
% 77.40/21.92 % (1522572)First to succeed.
% 77.40/21.92 % (1522572)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1522461"
% 77.40/21.92 % (1522575)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=3832395851:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2793 on theBenchmark for (2793ds/797Mi)
% 77.40/21.92 % (1522572)Refutation found. Thanks to Tanya!
% 77.40/21.92 % SZS status Theorem for theBenchmark
% 77.40/21.92 % SZS output start Proof for theBenchmark
% See solution above
% 0.26/22.20 % (1522572)------------------------------
% 0.26/22.20 % (1522572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.26/22.20 % (1522572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.26/22.20 % (1522572)CaDiCaL version: 2.1.3
% 0.26/22.20 % (1522572)Termination reason: Refutation
% 0.26/22.20 % (1522572)Time elapsed: 0.356 s
% 0.26/22.20 % (1522572)Peak memory usage: 260 MB
% 0.26/22.20 % (1522572)Instructions burned: 1082 (million)
% 0.26/22.20 % (1522572)------------------------------
% 0.26/22.20 % (1522572)------------------------------
% 0.26/22.20 % (1522461)Success in time 21.205 s
% 0.26/22.20 % Vampire exiting
%------------------------------------------------------------------------------