%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV127+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 : n002.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:54:46 AM UTC 2026
% Result : Theorem 169.92s 28.60s
% Output : Refutation 170.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 76
% Syntax : Number of formulae : 608 ( 40 unt; 27 def)
% Number of atoms : 1829 ( 30 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 2000 ( 779 ~;1055 |; 44 &)
% ( 76 <=>; 46 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 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 : 287 ( 0 sgn 286 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f95,conjecture,
! [X0] :
( reachableState(X0)
=> v4(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssertion) ).
fof(f96,negated_conjecture,
~ ! [X0] :
( reachableState(X0)
=> v4(X0) ),
inference(negated_conjecture,[status(cth)],[f95]) ).
fof(f97,axiom,
! [X0] :
( ~ v4(X0)
<=> v231505(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18766) ).
fof(f98,axiom,
! [X0] :
( ~ v231505(X0)
<=> v231506(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18765) ).
fof(f99,axiom,
! [X0] :
( v231506(X0)
<=> ( v231508(X0)
& v231526(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32503) ).
fof(f100,axiom,
! [X0] :
( v231526(X0)
<=> ( v231527(X0)
| v231511(X0,bitIndex3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8391) ).
fof(f101,axiom,
! [X0] :
( v231527(X0)
<=> ( v231528(X0)
| v231511(X0,bitIndex2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8390) ).
fof(f102,axiom,
! [X0] :
( v231528(X0)
<=> ( v231511(X0,bitIndex0)
| v231511(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8389) ).
fof(f103,axiom,
! [X0] :
( v231508(X0)
<=> ( v231509(X0)
| v231517(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32502) ).
fof(f104,axiom,
! [X0] :
( v231517(X0)
<=> ( v231518(X0)
| v231519(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32501) ).
fof(f105,axiom,
! [X0] :
( v231519(X0)
<=> ( v231510(X0)
& v231520(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32500) ).
fof(f106,axiom,
! [X0] :
( v231520(X0)
<=> ( v231521(X0)
| v231522(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32499) ).
fof(f107,axiom,
! [X0] :
( v231522(X0)
<=> ( v231513(X0)
& v231523(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32498) ).
fof(f108,axiom,
! [X0] :
( v231523(X0)
<=> ( v231524(X0)
| v231525(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32497) ).
fof(f109,axiom,
! [X0] :
( v231525(X0)
<=> ( v231511(X0,bitIndex0)
& v231516(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32496) ).
fof(f110,axiom,
! [X0] :
( v231524(X0)
<=> ( v231515(X0)
& v231511(X0,bitIndex1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8388) ).
fof(f111,axiom,
! [X0] :
( v231521(X0)
<=> ( v231511(X0,bitIndex2)
& v231514(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8387) ).
fof(f112,axiom,
! [X0] :
( v231518(X0)
<=> ( v231511(X0,bitIndex3)
& v231512(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8386) ).
fof(f113,axiom,
! [X0] :
( v231509(X0)
<=> ( v231510(X0)
& v231512(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32495) ).
fof(f114,axiom,
! [X0] :
( v231512(X0)
<=> ( v231513(X0)
& v231514(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32494) ).
fof(f115,axiom,
! [X0] :
( v231514(X0)
<=> ( v231515(X0)
& v231516(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32493) ).
fof(f116,axiom,
! [X0] :
( ~ v231516(X0)
<=> v231511(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18764) ).
fof(f117,axiom,
! [X0] :
( ~ v231515(X0)
<=> v231511(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18763) ).
fof(f118,axiom,
! [X0] :
( ~ v231513(X0)
<=> v231511(X0,bitIndex2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18762) ).
fof(f119,axiom,
! [X0] :
( ~ v231510(X0)
<=> v231511(X0,bitIndex3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18761) ).
fof(f120,axiom,
! [X0,X1] :
( range_3_0(X1)
=> ( v231511(X0,X1)
<=> v6(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118543) ).
fof(f121,axiom,
! [X0] :
( ~ v231494(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> v231496(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_3223) ).
fof(f122,axiom,
! [X0] :
( v231494(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> b0001(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_3183) ).
fof(f123,axiom,
! [X0] :
( ~ v231497(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231496(X0,X1)
<=> v231499(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_3222) ).
fof(f124,axiom,
! [X0] :
( v231497(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231496(X0,X1)
<=> b0010(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_3182) ).
fof(f125,axiom,
! [X0] :
( ~ v2311(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231499(X0,X1)
<=> v231502(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_3221) ).
fof(f126,axiom,
! [X0] :
( v2311(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231499(X0,X1)
<=> v231500(X0,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_3181) ).
fof(f127,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v231502(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118542) ).
fof(f128,axiom,
! [X0] :
( v231502(X0,bitIndex2)
<=> v231503(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118541) ).
fof(f129,axiom,
! [X0] :
( v231502(X0,bitIndex3)
<=> v126476(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118540) ).
fof(f130,axiom,
! [X0] :
( ~ v231503(X0)
<=> v126476(X0,bitIndex0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18760) ).
fof(f131,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v231500(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118539) ).
fof(f132,axiom,
! [X0] :
( v231500(X0,bitIndex2)
<=> v231501(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118538) ).
fof(f133,axiom,
! [X0] :
( v231500(X0,bitIndex3)
<=> v126476(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addAssignment_118537) ).
fof(f134,axiom,
! [X0] :
( ~ v231501(X0)
<=> v126476(X0,bitIndex1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',writeUnaryOperator_18759) ).
fof(f119453,axiom,
~ b0010(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_1021) ).
fof(f119454,axiom,
~ b0010(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_1020) ).
fof(f119455,axiom,
b0010(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_1019) ).
fof(f119456,axiom,
~ b0010(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_1018) ).
fof(f197740,axiom,
~ b0001(bitIndex3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_290) ).
fof(f197741,axiom,
~ b0001(bitIndex2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_289) ).
fof(f197742,axiom,
~ b0001(bitIndex1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_288) ).
fof(f197743,axiom,
b0001(bitIndex0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bitBlastConstant_287) ).
fof(f202474,axiom,
! [X0] :
( range_3_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_axiom_22) ).
fof(f203016,axiom,
! [X0] :
( range_1_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',range_axiom_7) ).
fof(f204781,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231500(X0,X1) ),
inference(true_and_false_elimination,[],[f131]) ).
fof(f204782,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231500(X0,X1) ),
inference(flattening,[],[f204781]) ).
fof(f204783,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231502(X0,X1) ),
inference(true_and_false_elimination,[],[f127]) ).
fof(f204784,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231502(X0,X1) ),
inference(flattening,[],[f204783]) ).
fof(f204885,plain,
! [X0] :
( range_1_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0 ) ),
inference(true_and_false_elimination,[],[f203016]) ).
fof(f204887,plain,
! [X0] :
( range_3_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
inference(true_and_false_elimination,[],[f202474]) ).
fof(f205158,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0 )
=> range_1_0(X0) ),
inference(unused_predicate_definition_removal,[],[f204885]) ).
fof(f205159,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 )
=> range_3_0(X0) ),
inference(unused_predicate_definition_removal,[],[f204887]) ).
fof(f205160,plain,
! [X0] :
( ~ v4(X0)
=> v231505(X0) ),
inference(unused_predicate_definition_removal,[],[f97]) ).
fof(f205161,plain,
! [X0] :
( v231506(X0)
=> ~ v231505(X0) ),
inference(unused_predicate_definition_removal,[],[f98]) ).
fof(f205162,plain,
! [X0] :
( ( v231508(X0)
& v231526(X0) )
=> v231506(X0) ),
inference(unused_predicate_definition_removal,[],[f99]) ).
fof(f205163,plain,
! [X0] :
( ( v231509(X0)
| v231517(X0) )
=> v231508(X0) ),
inference(unused_predicate_definition_removal,[],[f103]) ).
fof(f205164,plain,
! [X0] :
( ( v231510(X0)
& v231512(X0) )
=> v231509(X0) ),
inference(unused_predicate_definition_removal,[],[f113]) ).
fof(f205165,plain,
! [X0] :
( ( v231518(X0)
| v231519(X0) )
=> v231517(X0) ),
inference(unused_predicate_definition_removal,[],[f104]) ).
fof(f205166,plain,
! [X0] :
( ( v231511(X0,bitIndex3)
& v231512(X0) )
=> v231518(X0) ),
inference(unused_predicate_definition_removal,[],[f112]) ).
fof(f205167,plain,
! [X0] :
( ( v231513(X0)
& v231514(X0) )
=> v231512(X0) ),
inference(unused_predicate_definition_removal,[],[f114]) ).
fof(f205168,plain,
! [X0] :
( ( v231510(X0)
& v231520(X0) )
=> v231519(X0) ),
inference(unused_predicate_definition_removal,[],[f105]) ).
fof(f205169,plain,
! [X0] :
( ~ v231510(X0)
=> v231511(X0,bitIndex3) ),
inference(unused_predicate_definition_removal,[],[f119]) ).
fof(f205170,plain,
! [X0] :
( ( v231521(X0)
| v231522(X0) )
=> v231520(X0) ),
inference(unused_predicate_definition_removal,[],[f106]) ).
fof(f205171,plain,
! [X0] :
( ( v231511(X0,bitIndex2)
& v231514(X0) )
=> v231521(X0) ),
inference(unused_predicate_definition_removal,[],[f111]) ).
fof(f205172,plain,
! [X0] :
( ( v231515(X0)
& v231516(X0) )
=> v231514(X0) ),
inference(unused_predicate_definition_removal,[],[f115]) ).
fof(f205173,plain,
! [X0] :
( ( v231513(X0)
& v231523(X0) )
=> v231522(X0) ),
inference(unused_predicate_definition_removal,[],[f107]) ).
fof(f205174,plain,
! [X0] :
( ~ v231513(X0)
=> v231511(X0,bitIndex2) ),
inference(unused_predicate_definition_removal,[],[f118]) ).
fof(f205175,plain,
! [X0] :
( ( v231524(X0)
| v231525(X0) )
=> v231523(X0) ),
inference(unused_predicate_definition_removal,[],[f108]) ).
fof(f205176,plain,
! [X0] :
( ( v231515(X0)
& v231511(X0,bitIndex1) )
=> v231524(X0) ),
inference(unused_predicate_definition_removal,[],[f110]) ).
fof(f205177,plain,
! [X0] :
( ~ v231515(X0)
=> v231511(X0,bitIndex0) ),
inference(unused_predicate_definition_removal,[],[f117]) ).
fof(f205178,plain,
! [X0] :
( ( v231511(X0,bitIndex0)
& v231516(X0) )
=> v231525(X0) ),
inference(unused_predicate_definition_removal,[],[f109]) ).
fof(f205179,plain,
! [X0] :
( ~ v231516(X0)
=> v231511(X0,bitIndex1) ),
inference(unused_predicate_definition_removal,[],[f116]) ).
fof(f205180,plain,
! [X0] :
( ( v231527(X0)
| v231511(X0,bitIndex3) )
=> v231526(X0) ),
inference(unused_predicate_definition_removal,[],[f100]) ).
fof(f205181,plain,
! [X0] :
( ( v231528(X0)
| v231511(X0,bitIndex2) )
=> v231527(X0) ),
inference(unused_predicate_definition_removal,[],[f101]) ).
fof(f205182,plain,
! [X0] :
( ( v231511(X0,bitIndex0)
| v231511(X0,bitIndex1) )
=> v231528(X0) ),
inference(unused_predicate_definition_removal,[],[f102]) ).
fof(f205236,plain,
~ ! [X0] : v4(X0),
inference(pure_predicate_removal,[],[f96]) ).
fof(f205312,plain,
? [X0] : ~ v4(X0),
inference(ennf_transformation,[],[f205236]) ).
fof(f205313,plain,
! [X0] :
( v231505(X0)
| v4(X0) ),
inference(ennf_transformation,[],[f205160]) ).
fof(f205314,plain,
! [X0] :
( ~ v231505(X0)
| ~ v231506(X0) ),
inference(ennf_transformation,[],[f205161]) ).
fof(f205315,plain,
! [X0] :
( v231506(X0)
| ~ v231508(X0)
| ~ v231526(X0) ),
inference(ennf_transformation,[],[f205162]) ).
fof(f205316,plain,
! [X0] :
( v231506(X0)
| ~ v231508(X0)
| ~ v231526(X0) ),
inference(flattening,[],[f205315]) ).
fof(f205317,plain,
! [X0] :
( v231508(X0)
| ( ~ v231509(X0)
& ~ v231517(X0) ) ),
inference(ennf_transformation,[],[f205163]) ).
fof(f205318,plain,
! [X0] :
( v231526(X0)
| ( ~ v231527(X0)
& ~ v231511(X0,bitIndex3) ) ),
inference(ennf_transformation,[],[f205180]) ).
fof(f205319,plain,
! [X0] :
( v231509(X0)
| ~ v231510(X0)
| ~ v231512(X0) ),
inference(ennf_transformation,[],[f205164]) ).
fof(f205320,plain,
! [X0] :
( v231509(X0)
| ~ v231510(X0)
| ~ v231512(X0) ),
inference(flattening,[],[f205319]) ).
fof(f205321,plain,
! [X0] :
( v231517(X0)
| ( ~ v231518(X0)
& ~ v231519(X0) ) ),
inference(ennf_transformation,[],[f205165]) ).
fof(f205322,plain,
! [X0] :
( v231527(X0)
| ( ~ v231528(X0)
& ~ v231511(X0,bitIndex2) ) ),
inference(ennf_transformation,[],[f205181]) ).
fof(f205323,plain,
! [X0,X1] :
( ( v231511(X0,X1)
<=> v6(X0,X1) )
| ~ range_3_0(X1) ),
inference(ennf_transformation,[],[f120]) ).
fof(f205324,plain,
! [X0] :
( v231511(X0,bitIndex3)
| v231510(X0) ),
inference(ennf_transformation,[],[f205169]) ).
fof(f205325,plain,
! [X0] :
( v231511(X0,bitIndex2)
| v231513(X0) ),
inference(ennf_transformation,[],[f205174]) ).
fof(f205326,plain,
! [X0] :
( v231511(X0,bitIndex0)
| v231515(X0) ),
inference(ennf_transformation,[],[f205177]) ).
fof(f205327,plain,
! [X0] :
( v231511(X0,bitIndex1)
| v231516(X0) ),
inference(ennf_transformation,[],[f205179]) ).
fof(f205328,plain,
! [X0] :
( v231518(X0)
| ~ v231511(X0,bitIndex3)
| ~ v231512(X0) ),
inference(ennf_transformation,[],[f205166]) ).
fof(f205329,plain,
! [X0] :
( v231518(X0)
| ~ v231511(X0,bitIndex3)
| ~ v231512(X0) ),
inference(flattening,[],[f205328]) ).
fof(f205330,plain,
! [X0] :
( v231521(X0)
| ~ v231511(X0,bitIndex2)
| ~ v231514(X0) ),
inference(ennf_transformation,[],[f205171]) ).
fof(f205331,plain,
! [X0] :
( v231521(X0)
| ~ v231511(X0,bitIndex2)
| ~ v231514(X0) ),
inference(flattening,[],[f205330]) ).
fof(f205332,plain,
! [X0] :
( v231524(X0)
| ~ v231515(X0)
| ~ v231511(X0,bitIndex1) ),
inference(ennf_transformation,[],[f205176]) ).
fof(f205333,plain,
! [X0] :
( v231524(X0)
| ~ v231515(X0)
| ~ v231511(X0,bitIndex1) ),
inference(flattening,[],[f205332]) ).
fof(f205334,plain,
! [X0] :
( v231525(X0)
| ~ v231511(X0,bitIndex0)
| ~ v231516(X0) ),
inference(ennf_transformation,[],[f205178]) ).
fof(f205335,plain,
! [X0] :
( v231525(X0)
| ~ v231511(X0,bitIndex0)
| ~ v231516(X0) ),
inference(flattening,[],[f205334]) ).
fof(f205336,plain,
! [X0] :
( v231528(X0)
| ( ~ v231511(X0,bitIndex0)
& ~ v231511(X0,bitIndex1) ) ),
inference(ennf_transformation,[],[f205182]) ).
fof(f205337,plain,
! [X0] :
( v231519(X0)
| ~ v231510(X0)
| ~ v231520(X0) ),
inference(ennf_transformation,[],[f205168]) ).
fof(f205338,plain,
! [X0] :
( v231519(X0)
| ~ v231510(X0)
| ~ v231520(X0) ),
inference(flattening,[],[f205337]) ).
fof(f205339,plain,
! [X0] :
( v231512(X0)
| ~ v231513(X0)
| ~ v231514(X0) ),
inference(ennf_transformation,[],[f205167]) ).
fof(f205340,plain,
! [X0] :
( v231512(X0)
| ~ v231513(X0)
| ~ v231514(X0) ),
inference(flattening,[],[f205339]) ).
fof(f205341,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> b0001(X1) )
| ~ range_3_0(X1) )
| ~ v231494(X0) ),
inference(ennf_transformation,[],[f122]) ).
fof(f205342,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> v231496(X0,X1) )
| ~ range_3_0(X1) )
| v231494(X0) ),
inference(ennf_transformation,[],[f121]) ).
fof(f205343,plain,
! [X0] :
( v231522(X0)
| ~ v231513(X0)
| ~ v231523(X0) ),
inference(ennf_transformation,[],[f205173]) ).
fof(f205344,plain,
! [X0] :
( v231522(X0)
| ~ v231513(X0)
| ~ v231523(X0) ),
inference(flattening,[],[f205343]) ).
fof(f205345,plain,
! [X0] :
( v231514(X0)
| ~ v231515(X0)
| ~ v231516(X0) ),
inference(ennf_transformation,[],[f205172]) ).
fof(f205346,plain,
! [X0] :
( v231514(X0)
| ~ v231515(X0)
| ~ v231516(X0) ),
inference(flattening,[],[f205345]) ).
fof(f205347,plain,
! [X0] :
( v231520(X0)
| ( ~ v231521(X0)
& ~ v231522(X0) ) ),
inference(ennf_transformation,[],[f205170]) ).
fof(f205348,plain,
! [X0] :
( v231523(X0)
| ( ~ v231524(X0)
& ~ v231525(X0) ) ),
inference(ennf_transformation,[],[f205175]) ).
fof(f205353,plain,
! [X0] :
( ! [X1] :
( ( v231496(X0,X1)
<=> b0010(X1) )
| ~ range_3_0(X1) )
| ~ v231497(X0) ),
inference(ennf_transformation,[],[f124]) ).
fof(f205354,plain,
! [X0] :
( ! [X1] :
( ( v231496(X0,X1)
<=> v231499(X0,X1) )
| ~ range_3_0(X1) )
| v231497(X0) ),
inference(ennf_transformation,[],[f123]) ).
fof(f205369,plain,
! [X0] :
( ! [X1] :
( ( v231499(X0,X1)
<=> v231500(X0,X1) )
| ~ range_3_0(X1) )
| ~ v2311(X0) ),
inference(ennf_transformation,[],[f126]) ).
fof(f205370,plain,
! [X0] :
( ! [X1] :
( ( v231499(X0,X1)
<=> v231502(X0,X1) )
| ~ range_3_0(X1) )
| v2311(X0) ),
inference(ennf_transformation,[],[f125]) ).
fof(f205416,plain,
! [X0,X1] :
( ~ v231500(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f204782]) ).
fof(f205417,plain,
! [X0,X1] :
( ~ v231502(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f204784]) ).
fof(f205672,plain,
! [X0] :
( range_1_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0 ) ),
inference(ennf_transformation,[],[f205158]) ).
fof(f205673,plain,
! [X0] :
( range_3_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0
& bitIndex2 != X0
& bitIndex3 != X0 ) ),
inference(ennf_transformation,[],[f205159]) ).
fof(f206169,plain,
~ v4(sK115),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115]),skolemize(X0,sK115)],[f205312]) ).
fof(f206170,plain,
! [X0,X1] :
( ( ( v231511(X0,X1)
| ~ v6(X0,X1) )
& ( v6(X0,X1)
| ~ v231511(X0,X1) ) )
| ~ range_3_0(X1) ),
inference(nnf_transformation,[],[f205323]) ).
fof(f206171,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ b0001(X1) )
& ( b0001(X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v231494(X0) ),
inference(nnf_transformation,[],[f205341]) ).
fof(f206172,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ v231496(X0,X1) )
& ( v231496(X0,X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| v231494(X0) ),
inference(nnf_transformation,[],[f205342]) ).
fof(f206179,plain,
! [X0] :
( ! [X1] :
( ( ( v231496(X0,X1)
| ~ b0010(X1) )
& ( b0010(X1)
| ~ v231496(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v231497(X0) ),
inference(nnf_transformation,[],[f205353]) ).
fof(f206180,plain,
! [X0] :
( ! [X1] :
( ( ( v231496(X0,X1)
| ~ v231499(X0,X1) )
& ( v231499(X0,X1)
| ~ v231496(X0,X1) ) )
| ~ range_3_0(X1) )
| v231497(X0) ),
inference(nnf_transformation,[],[f205354]) ).
fof(f206215,plain,
! [X0] :
( ! [X1] :
( ( ( v231499(X0,X1)
| ~ v231500(X0,X1) )
& ( v231500(X0,X1)
| ~ v231499(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v2311(X0) ),
inference(nnf_transformation,[],[f205369]) ).
fof(f206216,plain,
! [X0] :
( ! [X1] :
( ( ( v231499(X0,X1)
| ~ v231502(X0,X1) )
& ( v231502(X0,X1)
| ~ v231499(X0,X1) ) )
| ~ range_3_0(X1) )
| v2311(X0) ),
inference(nnf_transformation,[],[f205370]) ).
fof(f206307,plain,
! [X0] :
( ( v231500(X0,bitIndex3)
| ~ v126476(X0,bitIndex1) )
& ( v126476(X0,bitIndex1)
| ~ v231500(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f133]) ).
fof(f206308,plain,
! [X0] :
( ( v231500(X0,bitIndex2)
| ~ v231501(X0) )
& ( v231501(X0)
| ~ v231500(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f132]) ).
fof(f206309,plain,
! [X0] :
( ( v231502(X0,bitIndex3)
| ~ v126476(X0,bitIndex0) )
& ( v126476(X0,bitIndex0)
| ~ v231502(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f129]) ).
fof(f206310,plain,
! [X0] :
( ( v231502(X0,bitIndex2)
| ~ v231503(X0) )
& ( v231503(X0)
| ~ v231502(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f128]) ).
fof(f206508,plain,
! [X0] :
( ( ~ v231501(X0)
| ~ v126476(X0,bitIndex1) )
& ( v126476(X0,bitIndex1)
| v231501(X0) ) ),
inference(nnf_transformation,[],[f134]) ).
fof(f206509,plain,
! [X0] :
( ( ~ v231503(X0)
| ~ v126476(X0,bitIndex0) )
& ( v126476(X0,bitIndex0)
| v231503(X0) ) ),
inference(nnf_transformation,[],[f130]) ).
fof(f209231,plain,
~ v4(sK115),
inference(cnf_transformation,[],[f206169]) ).
fof(f209232,plain,
! [X0] :
( v231505(X0)
| v4(X0) ),
inference(cnf_transformation,[],[f205313]) ).
fof(f209233,plain,
! [X0] :
( ~ v231505(X0)
| ~ v231506(X0) ),
inference(cnf_transformation,[],[f205314]) ).
fof(f209234,plain,
! [X0] :
( v231506(X0)
| ~ v231508(X0)
| ~ v231526(X0) ),
inference(cnf_transformation,[],[f205316]) ).
fof(f209235,plain,
! [X0] :
( v231508(X0)
| ~ v231517(X0) ),
inference(cnf_transformation,[],[f205317]) ).
fof(f209236,plain,
! [X0] :
( v231508(X0)
| ~ v231509(X0) ),
inference(cnf_transformation,[],[f205317]) ).
fof(f209237,plain,
! [X0] :
( v231526(X0)
| ~ v231511(X0,bitIndex3) ),
inference(cnf_transformation,[],[f205318]) ).
fof(f209238,plain,
! [X0] :
( v231526(X0)
| ~ v231527(X0) ),
inference(cnf_transformation,[],[f205318]) ).
fof(f209239,plain,
! [X0] :
( v231509(X0)
| ~ v231510(X0)
| ~ v231512(X0) ),
inference(cnf_transformation,[],[f205320]) ).
fof(f209240,plain,
! [X0] :
( v231517(X0)
| ~ v231519(X0) ),
inference(cnf_transformation,[],[f205321]) ).
fof(f209241,plain,
! [X0] :
( v231517(X0)
| ~ v231518(X0) ),
inference(cnf_transformation,[],[f205321]) ).
fof(f209242,plain,
! [X0] :
( v231527(X0)
| ~ v231511(X0,bitIndex2) ),
inference(cnf_transformation,[],[f205322]) ).
fof(f209243,plain,
! [X0] :
( v231527(X0)
| ~ v231528(X0) ),
inference(cnf_transformation,[],[f205322]) ).
fof(f209244,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v231511(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f206170]) ).
fof(f209245,plain,
! [X0,X1] :
( v231511(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f206170]) ).
fof(f209246,plain,
! [X0] :
( v231511(X0,bitIndex3)
| v231510(X0) ),
inference(cnf_transformation,[],[f205324]) ).
fof(f209247,plain,
! [X0] :
( v231511(X0,bitIndex2)
| v231513(X0) ),
inference(cnf_transformation,[],[f205325]) ).
fof(f209248,plain,
! [X0] :
( v231511(X0,bitIndex0)
| v231515(X0) ),
inference(cnf_transformation,[],[f205326]) ).
fof(f209249,plain,
! [X0] :
( v231511(X0,bitIndex1)
| v231516(X0) ),
inference(cnf_transformation,[],[f205327]) ).
fof(f209250,plain,
! [X0] :
( v231518(X0)
| ~ v231511(X0,bitIndex3)
| ~ v231512(X0) ),
inference(cnf_transformation,[],[f205329]) ).
fof(f209251,plain,
! [X0] :
( v231521(X0)
| ~ v231511(X0,bitIndex2)
| ~ v231514(X0) ),
inference(cnf_transformation,[],[f205331]) ).
fof(f209252,plain,
! [X0] :
( v231524(X0)
| ~ v231515(X0)
| ~ v231511(X0,bitIndex1) ),
inference(cnf_transformation,[],[f205333]) ).
fof(f209253,plain,
! [X0] :
( v231525(X0)
| ~ v231511(X0,bitIndex0)
| ~ v231516(X0) ),
inference(cnf_transformation,[],[f205335]) ).
fof(f209254,plain,
! [X0] :
( v231528(X0)
| ~ v231511(X0,bitIndex1) ),
inference(cnf_transformation,[],[f205336]) ).
fof(f209255,plain,
! [X0] :
( v231528(X0)
| ~ v231511(X0,bitIndex0) ),
inference(cnf_transformation,[],[f205336]) ).
fof(f209256,plain,
! [X0] :
( v231519(X0)
| ~ v231510(X0)
| ~ v231520(X0) ),
inference(cnf_transformation,[],[f205338]) ).
fof(f209257,plain,
! [X0] :
( v231512(X0)
| ~ v231513(X0)
| ~ v231514(X0) ),
inference(cnf_transformation,[],[f205340]) ).
fof(f209258,plain,
! [X0,X1] :
( b0001(X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| ~ v231494(X0) ),
inference(cnf_transformation,[],[f206171]) ).
fof(f209259,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ b0001(X1)
| ~ range_3_0(X1)
| ~ v231494(X0) ),
inference(cnf_transformation,[],[f206171]) ).
fof(f209260,plain,
! [X0,X1] :
( v231496(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| v231494(X0) ),
inference(cnf_transformation,[],[f206172]) ).
fof(f209261,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v231496(X0,X1)
| ~ range_3_0(X1)
| v231494(X0) ),
inference(cnf_transformation,[],[f206172]) ).
fof(f209262,plain,
! [X0] :
( v231522(X0)
| ~ v231513(X0)
| ~ v231523(X0) ),
inference(cnf_transformation,[],[f205344]) ).
fof(f209263,plain,
! [X0] :
( v231514(X0)
| ~ v231515(X0)
| ~ v231516(X0) ),
inference(cnf_transformation,[],[f205346]) ).
fof(f209264,plain,
! [X0] :
( v231520(X0)
| ~ v231522(X0) ),
inference(cnf_transformation,[],[f205347]) ).
fof(f209265,plain,
! [X0] :
( v231520(X0)
| ~ v231521(X0) ),
inference(cnf_transformation,[],[f205347]) ).
fof(f209266,plain,
! [X0] :
( v231523(X0)
| ~ v231525(X0) ),
inference(cnf_transformation,[],[f205348]) ).
fof(f209267,plain,
! [X0] :
( v231523(X0)
| ~ v231524(X0) ),
inference(cnf_transformation,[],[f205348]) ).
fof(f209271,plain,
b0001(bitIndex0),
inference(cnf_transformation,[],[f197743]) ).
fof(f209272,plain,
~ b0001(bitIndex1),
inference(cnf_transformation,[],[f197742]) ).
fof(f209273,plain,
~ b0001(bitIndex2),
inference(cnf_transformation,[],[f197741]) ).
fof(f209274,plain,
~ b0001(bitIndex3),
inference(cnf_transformation,[],[f197740]) ).
fof(f209287,plain,
! [X0,X1] :
( b0010(X1)
| ~ v231496(X0,X1)
| ~ range_3_0(X1)
| ~ v231497(X0) ),
inference(cnf_transformation,[],[f206179]) ).
fof(f209288,plain,
! [X0,X1] :
( v231496(X0,X1)
| ~ b0010(X1)
| ~ range_3_0(X1)
| ~ v231497(X0) ),
inference(cnf_transformation,[],[f206179]) ).
fof(f209289,plain,
! [X0,X1] :
( v231499(X0,X1)
| ~ v231496(X0,X1)
| ~ range_3_0(X1)
| v231497(X0) ),
inference(cnf_transformation,[],[f206180]) ).
fof(f209290,plain,
! [X0,X1] :
( v231496(X0,X1)
| ~ v231499(X0,X1)
| ~ range_3_0(X1)
| v231497(X0) ),
inference(cnf_transformation,[],[f206180]) ).
fof(f209355,plain,
~ b0010(bitIndex0),
inference(cnf_transformation,[],[f119456]) ).
fof(f209356,plain,
b0010(bitIndex1),
inference(cnf_transformation,[],[f119455]) ).
fof(f209357,plain,
~ b0010(bitIndex2),
inference(cnf_transformation,[],[f119454]) ).
fof(f209358,plain,
~ b0010(bitIndex3),
inference(cnf_transformation,[],[f119453]) ).
fof(f209363,plain,
! [X0,X1] :
( v231500(X0,X1)
| ~ v231499(X0,X1)
| ~ range_3_0(X1)
| ~ v2311(X0) ),
inference(cnf_transformation,[],[f206215]) ).
fof(f209364,plain,
! [X0,X1] :
( v231499(X0,X1)
| ~ v231500(X0,X1)
| ~ range_3_0(X1)
| ~ v2311(X0) ),
inference(cnf_transformation,[],[f206215]) ).
fof(f209365,plain,
! [X0,X1] :
( v231502(X0,X1)
| ~ v231499(X0,X1)
| ~ range_3_0(X1)
| v2311(X0) ),
inference(cnf_transformation,[],[f206216]) ).
fof(f209366,plain,
! [X0,X1] :
( v231499(X0,X1)
| ~ v231502(X0,X1)
| ~ range_3_0(X1)
| v2311(X0) ),
inference(cnf_transformation,[],[f206216]) ).
fof(f209540,plain,
! [X0] :
( v126476(X0,bitIndex1)
| ~ v231500(X0,bitIndex3) ),
inference(cnf_transformation,[],[f206307]) ).
fof(f209541,plain,
! [X0] :
( v231500(X0,bitIndex3)
| ~ v126476(X0,bitIndex1) ),
inference(cnf_transformation,[],[f206307]) ).
fof(f209542,plain,
! [X0] :
( v231501(X0)
| ~ v231500(X0,bitIndex2) ),
inference(cnf_transformation,[],[f206308]) ).
fof(f209543,plain,
! [X0] :
( v231500(X0,bitIndex2)
| ~ v231501(X0) ),
inference(cnf_transformation,[],[f206308]) ).
fof(f209544,plain,
! [X0,X1] :
( ~ v231500(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f205416]) ).
fof(f209545,plain,
! [X0] :
( v126476(X0,bitIndex0)
| ~ v231502(X0,bitIndex3) ),
inference(cnf_transformation,[],[f206309]) ).
fof(f209546,plain,
! [X0] :
( v231502(X0,bitIndex3)
| ~ v126476(X0,bitIndex0) ),
inference(cnf_transformation,[],[f206309]) ).
fof(f209547,plain,
! [X0] :
( v231503(X0)
| ~ v231502(X0,bitIndex2) ),
inference(cnf_transformation,[],[f206310]) ).
fof(f209548,plain,
! [X0] :
( v231502(X0,bitIndex2)
| ~ v231503(X0) ),
inference(cnf_transformation,[],[f206310]) ).
fof(f209549,plain,
! [X0,X1] :
( ~ v231502(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f205417]) ).
fof(f209894,plain,
! [X0] :
( v126476(X0,bitIndex1)
| v231501(X0) ),
inference(cnf_transformation,[],[f206508]) ).
fof(f209895,plain,
! [X0] :
( ~ v231501(X0)
| ~ v126476(X0,bitIndex1) ),
inference(cnf_transformation,[],[f206508]) ).
fof(f209896,plain,
! [X0] :
( v126476(X0,bitIndex0)
| v231503(X0) ),
inference(cnf_transformation,[],[f206509]) ).
fof(f209897,plain,
! [X0] :
( ~ v231503(X0)
| ~ v126476(X0,bitIndex0) ),
inference(cnf_transformation,[],[f206509]) ).
fof(f211961,plain,
! [X0] :
( range_1_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f205672]) ).
fof(f211962,plain,
! [X0] :
( range_1_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f205672]) ).
fof(f211963,plain,
! [X0] :
( range_3_0(X0)
| bitIndex3 != X0 ),
inference(cnf_transformation,[],[f205673]) ).
fof(f211964,plain,
! [X0] :
( range_3_0(X0)
| bitIndex2 != X0 ),
inference(cnf_transformation,[],[f205673]) ).
fof(f211965,plain,
! [X0] :
( range_3_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f205673]) ).
fof(f211966,plain,
! [X0] :
( range_3_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f205673]) ).
fof(f215523,plain,
range_1_0(bitIndex0),
inference(equality_resolution,[],[f211962]) ).
fof(f215524,plain,
range_1_0(bitIndex1),
inference(equality_resolution,[],[f211961]) ).
fof(f215525,plain,
range_3_0(bitIndex0),
inference(equality_resolution,[],[f211966]) ).
fof(f215526,plain,
range_3_0(bitIndex1),
inference(equality_resolution,[],[f211965]) ).
fof(f215527,plain,
range_3_0(bitIndex2),
inference(equality_resolution,[],[f211964]) ).
fof(f215528,plain,
range_3_0(bitIndex3),
inference(equality_resolution,[],[f211963]) ).
fof(f215596,plain,
v231505(sK115),
inference(resolution,[],[f209231,f209232]) ).
fof(f215597,plain,
~ v231506(sK115),
inference(resolution,[],[f215596,f209233]) ).
fof(f215598,plain,
( ~ v231508(sK115)
| ~ v231526(sK115) ),
inference(resolution,[],[f215597,f209234]) ).
fof(f215600,definition,
( spl116_1
<=> v231526(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_1])],[avatar_definition]) ).
fof(f215602,plain,
( ~ v231526(sK115)
| spl116_1 ),
inference(avatar_component_clause,[],[f215600]) ).
fof(f215604,definition,
( spl116_2
<=> v231508(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_2])],[avatar_definition]) ).
fof(f215606,plain,
( ~ v231508(sK115)
| spl116_2 ),
inference(avatar_component_clause,[],[f215604]) ).
fof(f215607,plain,
( ~ spl116_1
| ~ spl116_2 ),
inference(avatar_split_clause,[],[f215598,f215604,f215600]) ).
fof(f215608,plain,
( ~ v231511(sK115,bitIndex3)
| spl116_1 ),
inference(resolution,[],[f215602,f209237]) ).
fof(f215609,plain,
( ~ v231527(sK115)
| spl116_1 ),
inference(resolution,[],[f215602,f209238]) ).
fof(f215611,plain,
( ~ v231528(sK115)
| spl116_1 ),
inference(resolution,[],[f215609,f209243]) ).
fof(f215613,plain,
( ~ v6(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl116_1 ),
inference(resolution,[],[f215608,f209245]) ).
fof(f215614,plain,
( ~ v6(sK115,bitIndex3)
| spl116_1 ),
inference(forward_subsumption_resolution,[],[f215613,f215528]) ).
fof(f215620,definition,
( spl116_3
<=> v231512(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_3])],[avatar_definition]) ).
fof(f215621,plain,
( v231512(sK115)
| ~ spl116_3 ),
inference(avatar_component_clause,[],[f215620]) ).
fof(f215622,plain,
( ~ v231512(sK115)
| spl116_3 ),
inference(avatar_component_clause,[],[f215620]) ).
fof(f215624,definition,
( spl116_4
<=> v231509(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_4])],[avatar_definition]) ).
fof(f215625,plain,
( ~ v231509(sK115)
| spl116_4 ),
inference(avatar_component_clause,[],[f215624]) ).
fof(f215629,definition,
( spl116_5
<=> v231520(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_5])],[avatar_definition]) ).
fof(f215630,plain,
( v231520(sK115)
| ~ spl116_5 ),
inference(avatar_component_clause,[],[f215629]) ).
fof(f215631,plain,
( ~ v231520(sK115)
| spl116_5 ),
inference(avatar_component_clause,[],[f215629]) ).
fof(f215633,definition,
( spl116_6
<=> v231519(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_6])],[avatar_definition]) ).
fof(f215634,plain,
( ~ v231519(sK115)
| spl116_6 ),
inference(avatar_component_clause,[],[f215633]) ).
fof(f215637,plain,
( ~ v231513(sK115)
| ~ v231514(sK115)
| spl116_3 ),
inference(resolution,[],[f215622,f209257]) ).
fof(f215639,definition,
( spl116_7
<=> v231514(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_7])],[avatar_definition]) ).
fof(f215640,plain,
( v231514(sK115)
| ~ spl116_7 ),
inference(avatar_component_clause,[],[f215639]) ).
fof(f215641,plain,
( ~ v231514(sK115)
| spl116_7 ),
inference(avatar_component_clause,[],[f215639]) ).
fof(f215643,definition,
( spl116_8
<=> v231513(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_8])],[avatar_definition]) ).
fof(f215644,plain,
( v231513(sK115)
| ~ spl116_8 ),
inference(avatar_component_clause,[],[f215643]) ).
fof(f215645,plain,
( ~ v231513(sK115)
| spl116_8 ),
inference(avatar_component_clause,[],[f215643]) ).
fof(f215646,plain,
( ~ spl116_7
| ~ spl116_8
| spl116_3 ),
inference(avatar_split_clause,[],[f215637,f215620,f215643,f215639]) ).
fof(f215651,plain,
( ~ v231522(sK115)
| spl116_5 ),
inference(resolution,[],[f215631,f209264]) ).
fof(f215652,plain,
( ~ v231521(sK115)
| spl116_5 ),
inference(resolution,[],[f215631,f209265]) ).
fof(f215653,plain,
( ~ v231496(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v231494(sK115)
| spl116_1 ),
inference(resolution,[],[f215614,f209261]) ).
fof(f215656,plain,
( ~ v231496(sK115,bitIndex3)
| v231494(sK115)
| spl116_1 ),
inference(forward_subsumption_resolution,[],[f215653,f215528]) ).
fof(f215658,definition,
( spl116_9
<=> v231494(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_9])],[avatar_definition]) ).
fof(f215659,plain,
( ~ v231494(sK115)
| spl116_9 ),
inference(avatar_component_clause,[],[f215658]) ).
fof(f215660,plain,
( v231494(sK115)
| ~ spl116_9 ),
inference(avatar_component_clause,[],[f215658]) ).
fof(f215662,definition,
( spl116_10
<=> v231496(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_10])],[avatar_definition]) ).
fof(f215663,plain,
( v231496(sK115,bitIndex3)
| ~ spl116_10 ),
inference(avatar_component_clause,[],[f215662]) ).
fof(f215664,plain,
( ~ v231496(sK115,bitIndex3)
| spl116_10 ),
inference(avatar_component_clause,[],[f215662]) ).
fof(f215665,plain,
( spl116_9
| ~ spl116_10
| spl116_1 ),
inference(avatar_split_clause,[],[f215656,f215600,f215662,f215658]) ).
fof(f215666,plain,
( ~ v231515(sK115)
| ~ v231516(sK115)
| spl116_7 ),
inference(resolution,[],[f215641,f209263]) ).
fof(f215668,definition,
( spl116_11
<=> v231516(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_11])],[avatar_definition]) ).
fof(f215669,plain,
( v231516(sK115)
| ~ spl116_11 ),
inference(avatar_component_clause,[],[f215668]) ).
fof(f215670,plain,
( ~ v231516(sK115)
| spl116_11 ),
inference(avatar_component_clause,[],[f215668]) ).
fof(f215672,definition,
( spl116_12
<=> v231515(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_12])],[avatar_definition]) ).
fof(f215673,plain,
( v231515(sK115)
| ~ spl116_12 ),
inference(avatar_component_clause,[],[f215672]) ).
fof(f215674,plain,
( ~ v231515(sK115)
| spl116_12 ),
inference(avatar_component_clause,[],[f215672]) ).
fof(f215675,plain,
( ~ spl116_11
| ~ spl116_12
| spl116_7 ),
inference(avatar_split_clause,[],[f215666,f215639,f215672,f215668]) ).
fof(f215682,plain,
( ~ v231517(sK115)
| spl116_2 ),
inference(resolution,[],[f215606,f209235]) ).
fof(f215683,plain,
( ~ v231509(sK115)
| spl116_2 ),
inference(resolution,[],[f215606,f209236]) ).
fof(f215684,plain,
( ~ spl116_4
| spl116_2 ),
inference(avatar_split_clause,[],[f215683,f215604,f215624]) ).
fof(f215685,plain,
( ~ v231519(sK115)
| spl116_2 ),
inference(resolution,[],[f215682,f209240]) ).
fof(f215686,plain,
( ~ v231518(sK115)
| spl116_2 ),
inference(resolution,[],[f215682,f209241]) ).
fof(f215687,plain,
( ~ spl116_6
| spl116_2 ),
inference(avatar_split_clause,[],[f215685,f215604,f215633]) ).
fof(f215689,plain,
( ~ v231510(sK115)
| ~ v231512(sK115)
| spl116_4 ),
inference(resolution,[],[f215625,f209239]) ).
fof(f215691,plain,
( v231522(sK115)
| ~ v231523(sK115)
| ~ spl116_8 ),
inference(resolution,[],[f215644,f209262]) ).
fof(f215693,plain,
( ~ v231523(sK115)
| spl116_5
| ~ spl116_8 ),
inference(forward_subsumption_resolution,[],[f215691,f215651]) ).
fof(f215694,plain,
( ~ v231499(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v231497(sK115)
| spl116_10 ),
inference(resolution,[],[f215664,f209290]) ).
fof(f215696,plain,
( ~ v6(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v231494(sK115)
| spl116_10 ),
inference(resolution,[],[f215664,f209260]) ).
fof(f215697,plain,
( ~ v6(sK115,bitIndex3)
| v231494(sK115)
| spl116_10 ),
inference(forward_subsumption_resolution,[],[f215696,f215528]) ).
fof(f215698,plain,
( ~ v231499(sK115,bitIndex3)
| v231497(sK115)
| spl116_10 ),
inference(forward_subsumption_resolution,[],[f215694,f215528]) ).
fof(f215700,definition,
( spl116_13
<=> v6(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_13])],[avatar_definition]) ).
fof(f215702,plain,
( ~ v6(sK115,bitIndex3)
| spl116_13 ),
inference(avatar_component_clause,[],[f215700]) ).
fof(f215703,plain,
( spl116_9
| ~ spl116_13
| spl116_10 ),
inference(avatar_split_clause,[],[f215697,f215662,f215700,f215658]) ).
fof(f215705,definition,
( spl116_14
<=> v231497(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_14])],[avatar_definition]) ).
fof(f215706,plain,
( ~ v231497(sK115)
| spl116_14 ),
inference(avatar_component_clause,[],[f215705]) ).
fof(f215707,plain,
( v231497(sK115)
| ~ spl116_14 ),
inference(avatar_component_clause,[],[f215705]) ).
fof(f215709,definition,
( spl116_15
<=> v231499(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_15])],[avatar_definition]) ).
fof(f215710,plain,
( v231499(sK115,bitIndex3)
| ~ spl116_15 ),
inference(avatar_component_clause,[],[f215709]) ).
fof(f215711,plain,
( ~ v231499(sK115,bitIndex3)
| spl116_15 ),
inference(avatar_component_clause,[],[f215709]) ).
fof(f215712,plain,
( spl116_14
| ~ spl116_15
| spl116_10 ),
inference(avatar_split_clause,[],[f215698,f215662,f215709,f215705]) ).
fof(f215718,plain,
( ~ v231511(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl116_13 ),
inference(resolution,[],[f215702,f209244]) ).
fof(f215719,plain,
( ~ v231511(sK115,bitIndex3)
| spl116_13 ),
inference(forward_subsumption_resolution,[],[f215718,f215528]) ).
fof(f215721,plain,
( ~ v231524(sK115)
| spl116_5
| ~ spl116_8 ),
inference(resolution,[],[f215693,f209267]) ).
fof(f215722,plain,
( ~ v231502(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v2311(sK115)
| spl116_15 ),
inference(resolution,[],[f215711,f209366]) ).
fof(f215723,plain,
( ~ v231500(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v2311(sK115)
| spl116_15 ),
inference(resolution,[],[f215711,f209364]) ).
fof(f215725,plain,
( ~ v231500(sK115,bitIndex3)
| ~ v2311(sK115)
| spl116_15 ),
inference(forward_subsumption_resolution,[],[f215723,f215528]) ).
fof(f215726,plain,
( ~ v231502(sK115,bitIndex3)
| v2311(sK115)
| spl116_15 ),
inference(forward_subsumption_resolution,[],[f215722,f215528]) ).
fof(f215728,definition,
( spl116_16
<=> v2311(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_16])],[avatar_definition]) ).
fof(f215729,plain,
( v2311(sK115)
| ~ spl116_16 ),
inference(avatar_component_clause,[],[f215728]) ).
fof(f215730,plain,
( ~ v2311(sK115)
| spl116_16 ),
inference(avatar_component_clause,[],[f215728]) ).
fof(f215732,definition,
( spl116_17
<=> v231500(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_17])],[avatar_definition]) ).
fof(f215733,plain,
( v231500(sK115,bitIndex3)
| ~ spl116_17 ),
inference(avatar_component_clause,[],[f215732]) ).
fof(f215734,plain,
( ~ v231500(sK115,bitIndex3)
| spl116_17 ),
inference(avatar_component_clause,[],[f215732]) ).
fof(f215735,plain,
( ~ spl116_16
| ~ spl116_17
| spl116_15 ),
inference(avatar_split_clause,[],[f215725,f215709,f215732,f215728]) ).
fof(f215737,definition,
( spl116_18
<=> v231502(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_18])],[avatar_definition]) ).
fof(f215738,plain,
( v231502(sK115,bitIndex3)
| ~ spl116_18 ),
inference(avatar_component_clause,[],[f215737]) ).
fof(f215739,plain,
( ~ v231502(sK115,bitIndex3)
| spl116_18 ),
inference(avatar_component_clause,[],[f215737]) ).
fof(f215740,plain,
( spl116_16
| ~ spl116_18
| spl116_15 ),
inference(avatar_split_clause,[],[f215726,f215709,f215737,f215728]) ).
fof(f215783,plain,
( v231510(sK115)
| spl116_13 ),
inference(resolution,[],[f215719,f209246]) ).
fof(f215786,plain,
( ~ v126476(sK115,bitIndex0)
| spl116_18 ),
inference(resolution,[],[f215739,f209546]) ).
fof(f215837,plain,
( v231519(sK115)
| ~ v231520(sK115)
| spl116_13 ),
inference(resolution,[],[f215783,f209256]) ).
fof(f215877,plain,
( v231503(sK115)
| spl116_18 ),
inference(resolution,[],[f215786,f209896]) ).
fof(f215881,definition,
( spl116_31
<=> v126476(sK115,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl116_31])],[avatar_definition]) ).
fof(f215882,plain,
( ~ v126476(sK115,bitIndex1)
| spl116_31 ),
inference(avatar_component_clause,[],[f215881]) ).
fof(f215883,plain,
( v126476(sK115,bitIndex1)
| ~ spl116_31 ),
inference(avatar_component_clause,[],[f215881]) ).
fof(f215912,plain,
( v126476(sK115,bitIndex0)
| ~ spl116_18 ),
inference(resolution,[],[f215738,f209545]) ).
fof(f215928,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| v231499(sK115,X0)
| ~ range_3_0(X0) )
| spl116_14 ),
inference(resolution,[],[f215706,f209289]) ).
fof(f216001,plain,
( ~ v126476(sK115,bitIndex1)
| spl116_17 ),
inference(resolution,[],[f215734,f209541]) ).
fof(f216002,plain,
( ~ v231499(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v2311(sK115)
| spl116_17 ),
inference(resolution,[],[f215734,f209363]) ).
fof(f216003,plain,
( ~ spl116_31
| spl116_17 ),
inference(avatar_split_clause,[],[f216001,f215732,f215881]) ).
fof(f216012,plain,
( ! [X0] :
( v231499(sK115,X0)
| ~ range_3_0(X0)
| ~ v6(sK115,X0)
| ~ range_3_0(X0)
| v231494(sK115) )
| spl116_14 ),
inference(resolution,[],[f215928,f209260]) ).
fof(f216013,plain,
( ! [X0] :
( v231499(sK115,X0)
| ~ range_3_0(X0)
| ~ v6(sK115,X0)
| v231494(sK115) )
| spl116_14 ),
inference(duplicate_literal_removal,[],[f216012]) ).
fof(f216017,definition,
( spl116_45
<=> ! [X0] :
( v231499(sK115,X0)
| ~ v6(sK115,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl116_45])],[avatar_definition]) ).
fof(f216018,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| v231499(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_45 ),
inference(avatar_component_clause,[],[f216017]) ).
fof(f216019,plain,
( spl116_9
| spl116_45
| spl116_14 ),
inference(avatar_split_clause,[],[f216013,f215705,f216017,f215658]) ).
fof(f216022,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215660,f209258]) ).
fof(f216032,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f216022,f209244]) ).
fof(f216033,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl116_9 ),
inference(duplicate_literal_removal,[],[f216032]) ).
fof(f216065,plain,
( ~ range_3_0(bitIndex2)
| b0001(bitIndex2)
| v231513(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f216033,f209247]) ).
fof(f216067,plain,
( ~ range_3_0(bitIndex1)
| b0001(bitIndex1)
| v231516(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f216033,f209249]) ).
fof(f216069,plain,
( b0001(bitIndex1)
| v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216067,f215526]) ).
fof(f216071,plain,
( v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216069,f209272]) ).
fof(f216074,plain,
( $false
| ~ spl116_9
| spl116_11 ),
inference(forward_subsumption_resolution,[],[f216071,f215670]) ).
fof(f216075,plain,
( ~ spl116_9
| spl116_11 ),
inference(avatar_contradiction_clause,[],[f216074]) ).
fof(f216081,definition,
( spl116_47
<=> v231523(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_47])],[avatar_definition]) ).
fof(f216083,plain,
( ~ v231523(sK115)
| spl116_47 ),
inference(avatar_component_clause,[],[f216081]) ).
fof(f216089,plain,
( ~ v231520(sK115)
| spl116_6
| spl116_13 ),
inference(forward_subsumption_resolution,[],[f215837,f215634]) ).
fof(f216092,plain,
( $false
| ~ spl116_5
| spl116_6
| spl116_13 ),
inference(forward_subsumption_resolution,[],[f216089,f215630]) ).
fof(f216093,plain,
( ~ spl116_5
| spl116_6
| spl116_13 ),
inference(avatar_contradiction_clause,[],[f216092]) ).
fof(f216104,plain,
( b0001(bitIndex2)
| v231513(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216065,f215527]) ).
fof(f216105,plain,
( v231513(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216104,f209273]) ).
fof(f216106,plain,
( $false
| spl116_8
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216105,f215645]) ).
fof(f216107,plain,
( spl116_8
| ~ spl116_9 ),
inference(avatar_contradiction_clause,[],[f216106]) ).
fof(f216113,plain,
( ~ v231511(sK115,bitIndex3)
| ~ v231512(sK115)
| spl116_2 ),
inference(resolution,[],[f215686,f209250]) ).
fof(f216116,plain,
( ~ v231510(sK115)
| ~ v231520(sK115)
| spl116_6 ),
inference(resolution,[],[f215634,f209256]) ).
fof(f216118,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| v231496(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f215659,f209260]) ).
fof(f216119,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f215659,f209261]) ).
fof(f216121,plain,
( v231511(sK115,bitIndex2)
| spl116_8 ),
inference(resolution,[],[f215645,f209247]) ).
fof(f216132,plain,
( ! [X0] :
( v231496(sK115,X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f216118,f209244]) ).
fof(f216133,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| v231496(sK115,X0) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f216132]) ).
fof(f216138,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| spl116_9 ),
inference(resolution,[],[f216119,f209290]) ).
fof(f216143,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| v231497(sK115) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f216138]) ).
fof(f216145,plain,
( ~ v231525(sK115)
| spl116_47 ),
inference(resolution,[],[f216083,f209266]) ).
fof(f216151,plain,
( v231521(sK115)
| ~ v231514(sK115)
| spl116_8 ),
inference(resolution,[],[f216121,f209251]) ).
fof(f216153,plain,
( v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_8 ),
inference(resolution,[],[f216121,f209244]) ).
fof(f216154,plain,
( v6(sK115,bitIndex2)
| spl116_8 ),
inference(forward_subsumption_resolution,[],[f216153,f215527]) ).
fof(f216170,plain,
( ~ range_3_0(bitIndex2)
| v231496(sK115,bitIndex2)
| spl116_8
| spl116_9 ),
inference(resolution,[],[f216133,f216121]) ).
fof(f216174,plain,
( ~ range_3_0(bitIndex0)
| v231496(sK115,bitIndex0)
| v231515(sK115)
| spl116_9 ),
inference(resolution,[],[f216133,f209248]) ).
fof(f216175,plain,
( ~ range_3_0(bitIndex1)
| v231496(sK115,bitIndex1)
| v231516(sK115)
| spl116_9 ),
inference(resolution,[],[f216133,f209249]) ).
fof(f216177,plain,
( v231496(sK115,bitIndex0)
| v231515(sK115)
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216174,f215525]) ).
fof(f216179,plain,
( v231496(sK115,bitIndex2)
| spl116_8
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216170,f215527]) ).
fof(f216180,plain,
( v231496(sK115,bitIndex0)
| spl116_9
| spl116_12 ),
inference(forward_subsumption_resolution,[],[f216177,f215674]) ).
fof(f216205,plain,
( ~ v231503(sK115)
| ~ spl116_18 ),
inference(resolution,[],[f215912,f209897]) ).
fof(f216267,plain,
( b0010(bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v231497(sK115)
| spl116_8
| spl116_9 ),
inference(resolution,[],[f216179,f209287]) ).
fof(f216274,plain,
( v231499(sK115,bitIndex0)
| ~ range_3_0(bitIndex0)
| spl116_9
| spl116_12
| spl116_14 ),
inference(resolution,[],[f216180,f215928]) ).
fof(f216276,plain,
( b0010(bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v231497(sK115)
| spl116_9
| spl116_12 ),
inference(resolution,[],[f216180,f209287]) ).
fof(f216279,plain,
( v231499(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f216274,f215525]) ).
fof(f216431,plain,
( v231499(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_8
| ~ spl116_45 ),
inference(resolution,[],[f216018,f216154]) ).
fof(f216434,plain,
( ! [X0] :
( v231499(sK115,X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_45 ),
inference(resolution,[],[f216018,f209244]) ).
fof(f216435,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| v231499(sK115,X0) )
| ~ spl116_45 ),
inference(duplicate_literal_removal,[],[f216434]) ).
fof(f216439,plain,
( ~ v231502(sK115,bitIndex2)
| ~ spl116_18 ),
inference(resolution,[],[f216205,f209547]) ).
fof(f216512,plain,
( ~ v231500(sK115,bitIndex3)
| spl116_31 ),
inference(resolution,[],[f215882,f209540]) ).
fof(f216518,plain,
( v231501(sK115)
| spl116_31 ),
inference(resolution,[],[f215882,f209894]) ).
fof(f216624,plain,
( v231500(sK115,bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v2311(sK115)
| spl116_9
| spl116_12
| spl116_14 ),
inference(resolution,[],[f216279,f209363]) ).
fof(f216626,plain,
( v231500(sK115,bitIndex0)
| ~ v2311(sK115)
| spl116_9
| spl116_12
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f216624,f215525]) ).
fof(f217329,plain,
( ~ range_3_0(bitIndex1)
| v231499(sK115,bitIndex1)
| v231516(sK115)
| ~ spl116_45 ),
inference(resolution,[],[f216435,f209249]) ).
fof(f217629,plain,
( v231500(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f216626,f215729]) ).
fof(f218217,plain,
( ~ range_1_0(bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f217629,f209544]) ).
fof(f218219,plain,
( $false
| spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f218217,f215523]) ).
fof(f218220,plain,
( spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(avatar_contradiction_clause,[],[f218219]) ).
fof(f218234,plain,
( ~ range_3_0(bitIndex2)
| ~ v231497(sK115)
| spl116_8
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216267,f209357]) ).
fof(f218235,plain,
( ~ range_3_0(bitIndex0)
| ~ v231497(sK115)
| spl116_9
| spl116_12 ),
inference(forward_subsumption_resolution,[],[f216276,f209355]) ).
fof(f218237,plain,
( v231499(sK115,bitIndex2)
| spl116_8
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f216431,f215527]) ).
fof(f218244,plain,
( ~ v231497(sK115)
| spl116_8
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f218234,f215527]) ).
fof(f218245,plain,
( ~ v231497(sK115)
| spl116_9
| spl116_12 ),
inference(forward_subsumption_resolution,[],[f218235,f215525]) ).
fof(f218246,plain,
( $false
| spl116_8
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f218244,f215707]) ).
fof(f218247,plain,
( spl116_8
| spl116_9
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f218246]) ).
fof(f218248,plain,
( $false
| spl116_9
| spl116_12
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f218245,f215707]) ).
fof(f218249,plain,
( spl116_9
| spl116_12
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f218248]) ).
fof(f218312,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v6(sK115,X0) )
| spl116_9
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f216143,f215706]) ).
fof(f218318,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| v231502(sK115,X0)
| ~ range_3_0(X0) )
| spl116_16 ),
inference(resolution,[],[f215730,f209365]) ).
fof(f218352,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231500(sK115,X0)
| ~ range_3_0(X0)
| ~ v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(resolution,[],[f218312,f209364]) ).
fof(f218355,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231500(sK115,X0)
| ~ v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(duplicate_literal_removal,[],[f218352]) ).
fof(f218544,plain,
( ! [X0] :
( v231502(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| spl116_16 ),
inference(resolution,[],[f218318,f209289]) ).
fof(f218545,plain,
( ! [X0] :
( v231502(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| v231497(sK115) )
| spl116_16 ),
inference(duplicate_literal_removal,[],[f218544]) ).
fof(f218548,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231502(sK115,X0) )
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f218545,f215706]) ).
fof(f218747,plain,
( ~ range_3_0(bitIndex0)
| v231502(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(resolution,[],[f218548,f216180]) ).
fof(f218755,plain,
( v231502(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f218747,f215525]) ).
fof(f219532,plain,
( ~ range_1_0(bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(resolution,[],[f218755,f209549]) ).
fof(f219534,plain,
( $false
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f219532,f215523]) ).
fof(f219535,plain,
( spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(avatar_contradiction_clause,[],[f219534]) ).
fof(f219541,plain,
( ! [X0] :
( ~ v231500(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f218355,f215729]) ).
fof(f219545,plain,
( v231496(sK115,bitIndex1)
| v231516(sK115)
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216175,f215526]) ).
fof(f219546,plain,
( v231499(sK115,bitIndex1)
| v231516(sK115)
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f217329,f215526]) ).
fof(f219547,plain,
( v231496(sK115,bitIndex1)
| spl116_9
| spl116_11 ),
inference(forward_subsumption_resolution,[],[f219545,f215670]) ).
fof(f219548,plain,
( v231499(sK115,bitIndex1)
| spl116_11
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f219546,f215670]) ).
fof(f219553,plain,
( v231524(sK115)
| ~ v231511(sK115,bitIndex1)
| ~ spl116_12 ),
inference(resolution,[],[f215673,f209252]) ).
fof(f219555,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| v231500(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_16 ),
inference(resolution,[],[f215729,f209363]) ).
fof(f219697,plain,
( v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v231501(sK115)
| spl116_9
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f219541,f209543]) ).
fof(f219707,plain,
( v231500(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_8
| ~ spl116_16
| ~ spl116_45 ),
inference(resolution,[],[f219555,f218237]) ).
fof(f219710,plain,
( ! [X0] :
( v231500(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| ~ spl116_16 ),
inference(resolution,[],[f219555,f209289]) ).
fof(f219711,plain,
( ! [X0] :
( v231500(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| v231497(sK115) )
| ~ spl116_16 ),
inference(duplicate_literal_removal,[],[f219710]) ).
fof(f219714,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231500(sK115,X0) )
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219711,f215706]) ).
fof(f219866,plain,
( ~ range_3_0(bitIndex1)
| v231500(sK115,bitIndex1)
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f219714,f219547]) ).
fof(f219874,plain,
( v231500(sK115,bitIndex1)
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219866,f215526]) ).
fof(f219880,plain,
( v231502(sK115,bitIndex1)
| ~ range_3_0(bitIndex1)
| v2311(sK115)
| spl116_11
| ~ spl116_45 ),
inference(resolution,[],[f219548,f209365]) ).
fof(f219923,plain,
( ~ range_1_0(bitIndex1)
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f219874,f209544]) ).
fof(f219925,plain,
( $false
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219923,f215524]) ).
fof(f219926,plain,
( spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(avatar_contradiction_clause,[],[f219925]) ).
fof(f219928,definition,
( spl116_363
<=> v231511(sK115,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl116_363])],[avatar_definition]) ).
fof(f219930,plain,
( ~ v231511(sK115,bitIndex1)
| spl116_363 ),
inference(avatar_component_clause,[],[f219928]) ).
fof(f219932,definition,
( spl116_364
<=> v231524(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_364])],[avatar_definition]) ).
fof(f219935,plain,
( ~ spl116_363
| spl116_364
| ~ spl116_12 ),
inference(avatar_split_clause,[],[f219553,f215672,f219932,f219928]) ).
fof(f219937,plain,
( ~ v231514(sK115)
| spl116_5
| spl116_8 ),
inference(forward_subsumption_resolution,[],[f216151,f215652]) ).
fof(f219940,plain,
( $false
| spl116_5
| ~ spl116_7
| spl116_8 ),
inference(forward_subsumption_resolution,[],[f219937,f215640]) ).
fof(f219941,plain,
( spl116_5
| ~ spl116_7
| spl116_8 ),
inference(avatar_contradiction_clause,[],[f219940]) ).
fof(f219942,plain,
( ~ spl116_47
| spl116_5
| ~ spl116_8 ),
inference(avatar_split_clause,[],[f215693,f215643,f215629,f216081]) ).
fof(f219943,plain,
( ~ spl116_364
| spl116_5
| ~ spl116_8 ),
inference(avatar_split_clause,[],[f215721,f215643,f215629,f219932]) ).
fof(f219945,plain,
( v6(sK115,bitIndex2)
| ~ v231501(sK115)
| spl116_9
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219697,f215527]) ).
fof(f219951,plain,
( v6(sK115,bitIndex2)
| spl116_9
| spl116_14
| ~ spl116_16
| spl116_31 ),
inference(forward_subsumption_resolution,[],[f219945,f216518]) ).
fof(f219958,plain,
( ~ v231511(sK115,bitIndex3)
| spl116_2
| ~ spl116_3 ),
inference(forward_subsumption_resolution,[],[f216113,f215621]) ).
fof(f219960,plain,
( ~ v231510(sK115)
| ~ spl116_3
| spl116_4 ),
inference(forward_subsumption_resolution,[],[f215689,f215621]) ).
fof(f219968,plain,
( ~ range_3_0(bitIndex3)
| ~ v2311(sK115)
| ~ spl116_15
| spl116_17 ),
inference(forward_subsumption_resolution,[],[f216002,f215710]) ).
fof(f219969,plain,
( ~ v2311(sK115)
| ~ spl116_15
| spl116_17 ),
inference(forward_subsumption_resolution,[],[f219968,f215528]) ).
fof(f219970,plain,
( $false
| ~ spl116_15
| ~ spl116_16
| spl116_17 ),
inference(forward_subsumption_resolution,[],[f219969,f215729]) ).
fof(f219971,plain,
( ~ spl116_15
| ~ spl116_16
| spl116_17 ),
inference(avatar_contradiction_clause,[],[f219970]) ).
fof(f219972,plain,
( $false
| ~ spl116_17
| spl116_31 ),
inference(forward_subsumption_resolution,[],[f216512,f215733]) ).
fof(f219973,plain,
( ~ spl116_17
| spl116_31 ),
inference(avatar_contradiction_clause,[],[f219972]) ).
fof(f219993,definition,
( spl116_368
<=> v231501(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_368])],[avatar_definition]) ).
fof(f219994,plain,
( v231501(sK115)
| ~ spl116_368 ),
inference(avatar_component_clause,[],[f219993]) ).
fof(f219995,plain,
( ~ v231501(sK115)
| spl116_368 ),
inference(avatar_component_clause,[],[f219993]) ).
fof(f219997,definition,
( spl116_369
<=> v6(sK115,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl116_369])],[avatar_definition]) ).
fof(f219998,plain,
( ~ v6(sK115,bitIndex2)
| spl116_369 ),
inference(avatar_component_clause,[],[f219997]) ).
fof(f219999,plain,
( v6(sK115,bitIndex2)
| ~ spl116_369 ),
inference(avatar_component_clause,[],[f219997]) ).
fof(f220007,definition,
( spl116_371
<=> v231499(sK115,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl116_371])],[avatar_definition]) ).
fof(f220009,plain,
( v231499(sK115,bitIndex2)
| ~ spl116_371 ),
inference(avatar_component_clause,[],[f220007]) ).
fof(f220021,plain,
( v231510(sK115)
| spl116_2
| ~ spl116_3 ),
inference(resolution,[],[f219958,f209246]) ).
fof(f220024,plain,
( $false
| spl116_2
| ~ spl116_3
| spl116_4 ),
inference(forward_subsumption_resolution,[],[f220021,f219960]) ).
fof(f220025,plain,
( spl116_2
| ~ spl116_3
| spl116_4 ),
inference(avatar_contradiction_clause,[],[f220024]) ).
fof(f220030,plain,
( spl116_371
| spl116_8
| ~ spl116_45 ),
inference(avatar_split_clause,[],[f218237,f216017,f215643,f220007]) ).
fof(f220031,plain,
( v231500(sK115,bitIndex2)
| spl116_8
| ~ spl116_16
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f219707,f215527]) ).
fof(f220035,plain,
( ~ v231510(sK115)
| ~ spl116_5
| spl116_6 ),
inference(forward_subsumption_resolution,[],[f216116,f215630]) ).
fof(f220037,definition,
( spl116_372
<=> v231511(sK115,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl116_372])],[avatar_definition]) ).
fof(f220038,plain,
( v231511(sK115,bitIndex2)
| ~ spl116_372 ),
inference(avatar_component_clause,[],[f220037]) ).
fof(f220039,plain,
( ~ v231511(sK115,bitIndex2)
| spl116_372 ),
inference(avatar_component_clause,[],[f220037]) ).
fof(f220054,plain,
( v231511(sK115,bitIndex3)
| ~ spl116_5
| spl116_6 ),
inference(resolution,[],[f220035,f209246]) ).
fof(f220082,plain,
( v231527(sK115)
| ~ spl116_372 ),
inference(resolution,[],[f220038,f209242]) ).
fof(f220087,plain,
( ~ range_3_0(bitIndex3)
| v231499(sK115,bitIndex3)
| ~ spl116_5
| spl116_6
| ~ spl116_45 ),
inference(resolution,[],[f220054,f216435]) ).
fof(f220108,plain,
( ~ v231500(sK115,bitIndex2)
| spl116_368 ),
inference(resolution,[],[f219995,f209542]) ).
fof(f220109,plain,
( $false
| spl116_8
| ~ spl116_16
| ~ spl116_45
| spl116_368 ),
inference(forward_subsumption_resolution,[],[f220108,f220031]) ).
fof(f220110,plain,
( spl116_8
| ~ spl116_16
| ~ spl116_45
| spl116_368 ),
inference(avatar_contradiction_clause,[],[f220109]) ).
fof(f220111,plain,
( ~ v126476(sK115,bitIndex1)
| ~ spl116_368 ),
inference(resolution,[],[f219994,f209895]) ).
fof(f220113,plain,
( $false
| ~ spl116_31
| ~ spl116_368 ),
inference(forward_subsumption_resolution,[],[f220111,f215883]) ).
fof(f220114,plain,
( ~ spl116_31
| ~ spl116_368 ),
inference(avatar_contradiction_clause,[],[f220113]) ).
fof(f220118,plain,
( $false
| spl116_1
| ~ spl116_372 ),
inference(forward_subsumption_resolution,[],[f220082,f215609]) ).
fof(f220119,plain,
( spl116_1
| ~ spl116_372 ),
inference(avatar_contradiction_clause,[],[f220118]) ).
fof(f220174,plain,
( ~ v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_372 ),
inference(resolution,[],[f220039,f209245]) ).
fof(f220175,plain,
( ~ range_3_0(bitIndex2)
| ~ spl116_369
| spl116_372 ),
inference(forward_subsumption_resolution,[],[f220174,f219999]) ).
fof(f220176,plain,
( $false
| ~ spl116_369
| spl116_372 ),
inference(forward_subsumption_resolution,[],[f220175,f215527]) ).
fof(f220177,plain,
( ~ spl116_369
| spl116_372 ),
inference(avatar_contradiction_clause,[],[f220176]) ).
fof(f220178,plain,
( $false
| spl116_9
| spl116_14
| ~ spl116_16
| spl116_31
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f219951,f219998]) ).
fof(f220179,plain,
( spl116_9
| spl116_14
| ~ spl116_16
| spl116_31
| spl116_369 ),
inference(avatar_contradiction_clause,[],[f220178]) ).
fof(f220185,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215660,f209258]) ).
fof(f220186,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ b0001(X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215660,f209259]) ).
fof(f220193,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f220185,f209244]) ).
fof(f220194,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl116_9 ),
inference(duplicate_literal_removal,[],[f220193]) ).
fof(f220204,plain,
( ! [X0] :
( ~ b0001(X0)
| ~ range_3_0(X0)
| v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f220186,f209245]) ).
fof(f220205,plain,
( ! [X0] :
( v231511(sK115,X0)
| ~ range_3_0(X0)
| ~ b0001(X0) )
| ~ spl116_9 ),
inference(duplicate_literal_removal,[],[f220204]) ).
fof(f220229,plain,
( ~ range_3_0(bitIndex3)
| b0001(bitIndex3)
| v231510(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f220194,f209246]) ).
fof(f220256,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v231528(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f220205,f209255]) ).
fof(f220257,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v231525(sK115)
| ~ v231516(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f220205,f209253]) ).
fof(f220263,plain,
( ~ b0001(bitIndex0)
| v231525(sK115)
| ~ v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220257,f215525]) ).
fof(f220264,plain,
( ~ b0001(bitIndex0)
| v231528(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220256,f215525]) ).
fof(f220266,plain,
( v231525(sK115)
| ~ v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220263,f209271]) ).
fof(f220267,plain,
( v231528(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220264,f209271]) ).
fof(f220270,plain,
( ~ v231516(sK115)
| ~ spl116_9
| spl116_47 ),
inference(forward_subsumption_resolution,[],[f220266,f216145]) ).
fof(f220271,plain,
( $false
| spl116_1
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220267,f215611]) ).
fof(f220272,plain,
( spl116_1
| ~ spl116_9 ),
inference(avatar_contradiction_clause,[],[f220271]) ).
fof(f220273,plain,
( $false
| ~ spl116_9
| ~ spl116_11
| spl116_47 ),
inference(forward_subsumption_resolution,[],[f220270,f215669]) ).
fof(f220274,plain,
( ~ spl116_9
| ~ spl116_11
| spl116_47 ),
inference(avatar_contradiction_clause,[],[f220273]) ).
fof(f220275,plain,
( v231499(sK115,bitIndex3)
| ~ spl116_5
| spl116_6
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f220087,f215528]) ).
fof(f220284,plain,
( b0001(bitIndex3)
| v231510(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220229,f215528]) ).
fof(f220292,plain,
( v231510(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220284,f209274]) ).
fof(f220293,plain,
( $false
| ~ spl116_5
| spl116_6
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220292,f220035]) ).
fof(f220294,plain,
( ~ spl116_5
| spl116_6
| ~ spl116_9 ),
inference(avatar_contradiction_clause,[],[f220293]) ).
fof(f220312,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f215659,f209261]) ).
fof(f220315,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v231497(sK115)
| ~ spl116_10 ),
inference(resolution,[],[f215663,f209287]) ).
fof(f220317,plain,
( ~ range_3_0(bitIndex3)
| ~ v231497(sK115)
| ~ spl116_10 ),
inference(forward_subsumption_resolution,[],[f220315,f209358]) ).
fof(f220318,plain,
( ~ v231497(sK115)
| ~ spl116_10 ),
inference(forward_subsumption_resolution,[],[f220317,f215528]) ).
fof(f220319,plain,
( $false
| ~ spl116_10
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220318,f215707]) ).
fof(f220320,plain,
( ~ spl116_10
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f220319]) ).
fof(f220375,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| spl116_9 ),
inference(resolution,[],[f220312,f209290]) ).
fof(f220376,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ range_3_0(X0)
| ~ v231497(sK115) )
| spl116_9 ),
inference(resolution,[],[f220312,f209288]) ).
fof(f220379,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ v231497(sK115) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f220376]) ).
fof(f220380,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| v231497(sK115) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f220375]) ).
fof(f220381,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ b0010(X0) )
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220379,f215707]) ).
fof(f220411,plain,
( ! [X0] :
( ~ range_3_0(X0)
| ~ b0010(X0)
| v231511(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9
| ~ spl116_14 ),
inference(resolution,[],[f220381,f209245]) ).
fof(f220412,plain,
( ! [X0] :
( v231511(sK115,X0)
| ~ b0010(X0)
| ~ range_3_0(X0) )
| spl116_9
| ~ spl116_14 ),
inference(duplicate_literal_removal,[],[f220411]) ).
fof(f220467,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| spl116_9
| ~ spl116_14
| spl116_363 ),
inference(resolution,[],[f220412,f219930]) ).
fof(f220475,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| v231528(sK115)
| spl116_9
| ~ spl116_14 ),
inference(resolution,[],[f220412,f209254]) ).
fof(f220480,plain,
( ~ range_3_0(bitIndex1)
| v231528(sK115)
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220475,f209356]) ).
fof(f220481,plain,
( ~ range_3_0(bitIndex1)
| spl116_9
| ~ spl116_14
| spl116_363 ),
inference(forward_subsumption_resolution,[],[f220467,f209356]) ).
fof(f220483,plain,
( v231528(sK115)
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220480,f215526]) ).
fof(f220484,plain,
( $false
| spl116_9
| ~ spl116_14
| spl116_363 ),
inference(forward_subsumption_resolution,[],[f220481,f215526]) ).
fof(f220485,plain,
( spl116_9
| ~ spl116_14
| spl116_363 ),
inference(avatar_contradiction_clause,[],[f220484]) ).
fof(f220487,plain,
( $false
| spl116_1
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220483,f215611]) ).
fof(f220488,plain,
( spl116_1
| spl116_9
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f220487]) ).
fof(f220492,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v6(sK115,X0) )
| spl116_9
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f220380,f215706]) ).
fof(f220523,plain,
( ~ v231499(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v2311(sK115)
| spl116_18 ),
inference(resolution,[],[f215739,f209365]) ).
fof(f220527,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231502(sK115,X0)
| ~ range_3_0(X0)
| v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(resolution,[],[f220492,f209366]) ).
fof(f220532,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231502(sK115,X0)
| v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(duplicate_literal_removal,[],[f220527]) ).
fof(f220533,plain,
( ! [X0] :
( ~ v231502(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f220532,f215730]) ).
fof(f220723,plain,
( v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v231503(sK115)
| spl116_9
| spl116_14
| spl116_16 ),
inference(resolution,[],[f220533,f209548]) ).
fof(f220725,plain,
( ~ range_3_0(bitIndex2)
| ~ v231503(sK115)
| spl116_9
| spl116_14
| spl116_16
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f220723,f219998]) ).
fof(f220726,plain,
( ~ v231503(sK115)
| spl116_9
| spl116_14
| spl116_16
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f220725,f215527]) ).
fof(f220727,plain,
( $false
| spl116_9
| spl116_14
| spl116_16
| spl116_18
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f220726,f215877]) ).
fof(f220728,plain,
( spl116_9
| spl116_14
| spl116_16
| spl116_18
| spl116_369 ),
inference(avatar_contradiction_clause,[],[f220727]) ).
fof(f220729,plain,
( spl116_15
| ~ spl116_5
| spl116_6
| ~ spl116_45 ),
inference(avatar_split_clause,[],[f220275,f216017,f215633,f215629,f215709]) ).
fof(f220732,plain,
( ~ range_3_0(bitIndex3)
| v2311(sK115)
| ~ spl116_15
| spl116_18 ),
inference(forward_subsumption_resolution,[],[f220523,f215710]) ).
fof(f220734,plain,
( v2311(sK115)
| ~ spl116_15
| spl116_18 ),
inference(forward_subsumption_resolution,[],[f220732,f215528]) ).
fof(f220735,plain,
( $false
| ~ spl116_15
| spl116_16
| spl116_18 ),
inference(forward_subsumption_resolution,[],[f220734,f215730]) ).
fof(f220736,plain,
( ~ spl116_15
| spl116_16
| spl116_18 ),
inference(avatar_contradiction_clause,[],[f220735]) ).
fof(f220737,plain,
( v231502(sK115,bitIndex1)
| v2311(sK115)
| spl116_11
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f219880,f215526]) ).
fof(f220743,plain,
( v231502(sK115,bitIndex1)
| spl116_11
| spl116_16
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f220737,f215730]) ).
fof(f220880,plain,
( v231502(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| v2311(sK115)
| ~ spl116_371 ),
inference(resolution,[],[f220009,f209365]) ).
fof(f220883,plain,
( ~ range_3_0(bitIndex2)
| v2311(sK115)
| ~ spl116_18
| ~ spl116_371 ),
inference(forward_subsumption_resolution,[],[f220880,f216439]) ).
fof(f220885,plain,
( v2311(sK115)
| ~ spl116_18
| ~ spl116_371 ),
inference(forward_subsumption_resolution,[],[f220883,f215527]) ).
fof(f220888,plain,
( $false
| spl116_16
| ~ spl116_18
| ~ spl116_371 ),
inference(forward_subsumption_resolution,[],[f220885,f215730]) ).
fof(f220889,plain,
( spl116_16
| ~ spl116_18
| ~ spl116_371 ),
inference(avatar_contradiction_clause,[],[f220888]) ).
fof(f222578,plain,
( ~ range_1_0(bitIndex1)
| spl116_11
| spl116_16
| ~ spl116_45 ),
inference(resolution,[],[f220743,f209549]) ).
fof(f222580,plain,
( $false
| spl116_11
| spl116_16
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f222578,f215524]) ).
fof(f222581,plain,
( spl116_11
| spl116_16
| ~ spl116_45 ),
inference(avatar_contradiction_clause,[],[f222580]) ).
cnf(s1,plain,
( ~ spl116_1
| ~ spl116_2 ),
inference(sat_conversion,[],[f215607]) ).
cnf(s4,plain,
( spl116_3
| ~ spl116_7
| ~ spl116_8 ),
inference(sat_conversion,[],[f215646]) ).
cnf(s6,plain,
( spl116_1
| spl116_9
| ~ spl116_10 ),
inference(sat_conversion,[],[f215665]) ).
cnf(s7,plain,
( spl116_7
| ~ spl116_11
| ~ spl116_12 ),
inference(sat_conversion,[],[f215675]) ).
cnf(s9,plain,
( spl116_2
| ~ spl116_4 ),
inference(sat_conversion,[],[f215684]) ).
cnf(s10,plain,
( spl116_2
| ~ spl116_6 ),
inference(sat_conversion,[],[f215687]) ).
cnf(s11,plain,
( spl116_9
| spl116_10
| ~ spl116_13 ),
inference(sat_conversion,[],[f215703]) ).
cnf(s12,plain,
( spl116_10
| spl116_14
| ~ spl116_15 ),
inference(sat_conversion,[],[f215712]) ).
cnf(s13,plain,
( spl116_15
| ~ spl116_16
| ~ spl116_17 ),
inference(sat_conversion,[],[f215735]) ).
cnf(s14,plain,
( spl116_15
| spl116_16
| ~ spl116_18 ),
inference(sat_conversion,[],[f215740]) ).
cnf(s32,plain,
( spl116_17
| ~ spl116_31 ),
inference(sat_conversion,[],[f216003]) ).
cnf(s33,plain,
( spl116_9
| spl116_14
| spl116_45 ),
inference(sat_conversion,[],[f216019]) ).
cnf(s39,plain,
( ~ spl116_9
| spl116_11 ),
inference(sat_conversion,[],[f216075]) ).
cnf(s43,plain,
( ~ spl116_5
| spl116_6
| spl116_13 ),
inference(sat_conversion,[],[f216093]) ).
cnf(s47,plain,
( spl116_8
| ~ spl116_9 ),
inference(sat_conversion,[],[f216107]) ).
cnf(s186,plain,
( spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(sat_conversion,[],[f218220]) ).
cnf(s193,plain,
( spl116_8
| spl116_9
| ~ spl116_14 ),
inference(sat_conversion,[],[f218247]) ).
cnf(s194,plain,
( spl116_9
| spl116_12
| ~ spl116_14 ),
inference(sat_conversion,[],[f218249]) ).
cnf(s344,plain,
( spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(sat_conversion,[],[f219535]) ).
cnf(s353,plain,
( spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(sat_conversion,[],[f219926]) ).
cnf(s354,plain,
( ~ spl116_12
| ~ spl116_363
| spl116_364 ),
inference(sat_conversion,[],[f219935]) ).
cnf(s356,plain,
( spl116_5
| ~ spl116_7
| spl116_8 ),
inference(sat_conversion,[],[f219941]) ).
cnf(s357,plain,
( spl116_5
| ~ spl116_8
| ~ spl116_47 ),
inference(sat_conversion,[],[f219942]) ).
cnf(s358,plain,
( spl116_5
| ~ spl116_8
| ~ spl116_364 ),
inference(sat_conversion,[],[f219943]) ).
cnf(s364,plain,
( ~ spl116_15
| ~ spl116_16
| spl116_17 ),
inference(sat_conversion,[],[f219971]) ).
cnf(s365,plain,
( ~ spl116_17
| spl116_31 ),
inference(sat_conversion,[],[f219973]) ).
cnf(s372,plain,
( spl116_2
| ~ spl116_3
| spl116_4 ),
inference(sat_conversion,[],[f220025]) ).
cnf(s374,plain,
( spl116_8
| ~ spl116_45
| spl116_371 ),
inference(sat_conversion,[],[f220030]) ).
cnf(s383,plain,
( spl116_8
| ~ spl116_16
| ~ spl116_45
| spl116_368 ),
inference(sat_conversion,[],[f220110]) ).
cnf(s384,plain,
( ~ spl116_31
| ~ spl116_368 ),
inference(sat_conversion,[],[f220114]) ).
cnf(s389,plain,
( spl116_1
| ~ spl116_372 ),
inference(sat_conversion,[],[f220119]) ).
cnf(s394,plain,
( ~ spl116_369
| spl116_372 ),
inference(sat_conversion,[],[f220177]) ).
cnf(s395,plain,
( spl116_9
| spl116_14
| ~ spl116_16
| spl116_31
| spl116_369 ),
inference(sat_conversion,[],[f220179]) ).
cnf(s402,plain,
( spl116_1
| ~ spl116_9 ),
inference(sat_conversion,[],[f220272]) ).
cnf(s403,plain,
( ~ spl116_9
| ~ spl116_11
| spl116_47 ),
inference(sat_conversion,[],[f220274]) ).
cnf(s413,plain,
( ~ spl116_5
| spl116_6
| ~ spl116_9 ),
inference(sat_conversion,[],[f220294]) ).
cnf(s418,plain,
( ~ spl116_10
| ~ spl116_14 ),
inference(sat_conversion,[],[f220320]) ).
cnf(s430,plain,
( spl116_9
| ~ spl116_14
| spl116_363 ),
inference(sat_conversion,[],[f220485]) ).
cnf(s431,plain,
( spl116_1
| spl116_9
| ~ spl116_14 ),
inference(sat_conversion,[],[f220488]) ).
cnf(s437,plain,
( spl116_9
| spl116_14
| spl116_16
| spl116_18
| spl116_369 ),
inference(sat_conversion,[],[f220728]) ).
cnf(s441,plain,
( ~ spl116_5
| spl116_6
| spl116_15
| ~ spl116_45 ),
inference(sat_conversion,[],[f220729]) ).
cnf(s442,plain,
( ~ spl116_15
| spl116_16
| spl116_18 ),
inference(sat_conversion,[],[f220736]) ).
cnf(s450,plain,
( spl116_16
| ~ spl116_18
| ~ spl116_371 ),
inference(sat_conversion,[],[f220889]) ).
cnf(s586,plain,
( spl116_11
| spl116_16
| ~ spl116_45 ),
inference(sat_conversion,[],[f222581]) ).
cnf(s605,plain,
( spl116_16
| spl116_1 ),
inference(rat,[],[s437,s14,s394,s389,s12,s431,s6,s402]) ).
cnf(s606,plain,
spl116_1,
inference(rat,[],[s32,s13,s395,s605,s12,s394,s431,s6,s389,s402]) ).
cnf(s607,plain,
~ spl116_2,
inference(rat,[],[s1,s606]) ).
cnf(s608,plain,
~ spl116_6,
inference(rat,[],[s10,s607]) ).
cnf(s609,plain,
~ spl116_4,
inference(rat,[],[s9,s607]) ).
cnf(s610,plain,
~ spl116_3,
inference(rat,[],[s372,s607,s609]) ).
cnf(s611,plain,
( ~ spl116_7
| spl116_5 ),
inference(rat,[],[s4,s356,s610]) ).
cnf(s612,plain,
( spl116_16
| spl116_7
| spl116_14
| spl116_9 ),
inference(rat,[],[s7,s344,s586,s33]) ).
cnf(s613,plain,
( spl116_7
| spl116_14
| spl116_9 ),
inference(rat,[],[s7,s186,s353,s612]) ).
cnf(s614,plain,
( spl116_16
| ~ spl116_371
| ~ spl116_15 ),
inference(rat,[],[s450,s442]) ).
cnf(s615,plain,
( spl116_14
| spl116_9 ),
inference(rat,[],[s384,s365,s383,s364,s614,s374,s441,s4,s611,s613,s33,s610,s608]) ).
cnf(s616,plain,
( ~ spl116_14
| spl116_9 ),
inference(rat,[],[s43,s358,s11,s354,s193,s194,s418,s430,s608]) ).
cnf(s617,plain,
spl116_9,
inference(rat,[],[s616,s615]) ).
cnf(s618,plain,
spl116_8,
inference(rat,[],[s47,s617]) ).
cnf(s619,plain,
spl116_11,
inference(rat,[],[s39,s617]) ).
cnf(s622,plain,
~ spl116_5,
inference(rat,[],[s413,s608,s617]) ).
cnf(s625,plain,
spl116_47,
inference(rat,[],[s403,s617,s619]) ).
cnf(s630,plain,
$false,
inference(rat,[],[s357,s618,s622,s625]) ).
fof(f222582,plain,
$false,
inference(avatar_sat_refutation,[],[s630]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV127+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.11 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 % Computer : n002.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Sun Sep 27 11:46:40 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.19/0.53 Running first-order theorem proving
% 0.19/0.53 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
% 18.74/7.17 % (3391919)Detected formulas, will run a generic FOF schedule.
% 18.74/7.17 % (3391924)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=2193041287:i=141193_2958 on theBenchmark for (2958ds/141193Mi)
% 18.74/7.17 % (3391925)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=2779992090:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2958 on theBenchmark for (2958ds/134677Mi)
% 18.74/7.17 % (3391926)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=2112243039:i=141695:sd=1:nm=32:gsp=on:ss=included_2958 on theBenchmark for (2958ds/141695Mi)
% 18.74/7.17 % (3391927)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2177245653:i=109:sd=1:ins=1:gsp=on:ss=axioms_2958 on theBenchmark for (2958ds/109Mi)
% 18.74/7.17 % (3391928)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3249362733:i=119:av=off:ss=axioms_2958 on theBenchmark for (2958ds/119Mi)
% 18.74/7.17 % (3391929)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4130096815:s2a=on:i=139:gtg=position_2958 on theBenchmark for (2958ds/139Mi)
% 18.74/7.17 % (3391930)dis-21_1_sil=8000:lcm=predicate:random_seed=1644716498:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2958 on theBenchmark for (2958ds/129Mi)
% 18.74/7.17 % (3391927)Instruction limit reached!
% 18.74/7.17 % (3391927)------------------------------
% 18.74/7.17 % (3391927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/7.17 % (3391927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/7.17 % (3391927)CaDiCaL version: 2.1.3
% 18.74/7.17 % (3391927)Termination reason: Instruction limit
% 18.74/7.17 % (3391927)Termination phase: SInE selection
% 18.74/7.17 % (3391927)Time elapsed: 0.056 s
% 18.74/7.17 % (3391927)Peak memory usage: 270 MB
% 18.74/7.17 % (3391927)Instructions burned: 109 (million)
% 18.74/7.17 % (3391928)Instruction limit reached!
% 18.74/7.17 % (3391928)------------------------------
% 18.74/7.17 % (3391928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/7.17 % (3391928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/7.17 % (3391928)CaDiCaL version: 2.1.3
% 18.74/7.17 % (3391928)Termination reason: Instruction limit
% 18.74/7.17 % (3391928)Termination phase: SInE selection
% 18.74/7.17 % (3391928)Time elapsed: 0.061 s
% 18.74/7.17 % (3391928)Peak memory usage: 270 MB
% 18.74/7.17 % (3391928)Instructions burned: 121 (million)
% 18.74/7.17 % (3391930)Instruction limit reached!
% 18.74/7.17 % (3391930)------------------------------
% 18.74/7.17 % (3391930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/7.17 % (3391930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/7.17 % (3391930)CaDiCaL version: 2.1.3
% 18.74/7.17 % (3391930)Termination reason: Instruction limit
% 18.74/7.17 % (3391930)Termination phase: SInE selection
% 18.74/7.17 % (3391930)Time elapsed: 0.064 s
% 18.74/7.17 % (3391930)Peak memory usage: 270 MB
% 18.74/7.17 % (3391930)Instructions burned: 129 (million)
% 18.74/7.17 % (3391929)Instruction limit reached!
% 18.74/7.17 % (3391929)------------------------------
% 18.74/7.17 % (3391929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.74/7.17 % (3391929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.74/7.17 % (3391929)CaDiCaL version: 2.1.3
% 18.74/7.17 % (3391929)Termination reason: Instruction limit
% 18.74/7.17 % (3391929)Termination phase: Property scanning
% 18.74/7.17 % (3391929)Time elapsed: 0.111 s
% 18.74/7.17 % (3391929)Peak memory usage: 270 MB
% 18.74/7.17 % (3391929)Instructions burned: 140 (million)
% 18.74/7.17 % (3391939)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1193666685:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/157Mi)
% 18.74/7.17 % (3391938)lrs+10_1_sil=8000:sp=occurrence:random_seed=214553354:i=285:sd=3:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/285Mi)
% 18.74/7.17 % (3391940)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4787659:i=325:sd=1:ss=axioms:sgt=32_2955 on theBenchmark for (2955ds/325Mi)
% 18.74/7.17 % (3391941)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=29586875:s2a=on:i=248:s2at=1.23:gtg=position_2954 on theBenchmark for (2954ds/248Mi)
% 18.74/7.17 % (3391939)Instruction limit reached!
% 25.83/8.18 % (3391939)------------------------------
% 25.83/8.18 % (3391939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391939)CaDiCaL version: 2.1.3
% 25.83/8.18 % (3391939)Termination reason: Instruction limit
% 25.83/8.18 % (3391939)Termination phase: Property scanning
% 25.83/8.18 % (3391939)Time elapsed: 0.117 s
% 25.83/8.18 % (3391939)Peak memory usage: 270 MB
% 25.83/8.18 % (3391939)Instructions burned: 159 (million)
% 25.83/8.18 % (3391938)Instruction limit reached!
% 25.83/8.18 % (3391938)------------------------------
% 25.83/8.18 % (3391938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391938)CaDiCaL version: 2.1.3
% 25.83/8.18 % (3391938)Termination reason: Instruction limit
% 25.83/8.18 % (3391938)Termination phase: SInE selection
% 25.83/8.18 % (3391938)Time elapsed: 0.126 s
% 25.83/8.18 % (3391938)Peak memory usage: 270 MB
% 25.83/8.18 % (3391938)Instructions burned: 285 (million)
% 25.83/8.18 % (3391940)Instruction limit reached!
% 25.83/8.18 % (3391940)------------------------------
% 25.83/8.18 % (3391940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391940)CaDiCaL version: 2.1.3
% 25.83/8.18 % (3391940)Termination reason: Instruction limit
% 25.83/8.18 % (3391940)Termination phase: SInE selection
% 25.83/8.18 % (3391940)Time elapsed: 0.142 s
% 25.83/8.18 % (3391940)Peak memory usage: 270 MB
% 25.83/8.18 % (3391940)Instructions burned: 327 (million)
% 25.83/8.18 % (3391941)Instruction limit reached!
% 25.83/8.18 % (3391941)------------------------------
% 25.83/8.18 % (3391941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391941)CaDiCaL version: 2.1.3
% 25.83/8.18 % (3391941)Termination reason: Instruction limit
% 25.83/8.18 % (3391941)Termination phase: Property scanning
% 25.83/8.18 % (3391941)Time elapsed: 0.154 s
% 25.83/8.18 % (3391941)Peak memory usage: 270 MB
% 25.83/8.18 % (3391941)Instructions burned: 250 (million)
% 25.83/8.18 % (3391946)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=110318134:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2952 on theBenchmark for (2952ds/294Mi)
% 25.83/8.18 % (3391947)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=594099922:i=2350_2952 on theBenchmark for (2952ds/2350Mi)
% 25.83/8.18 % (3391948)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1493436681:cts=off:i=113:fsr=off:ss=included:sgt=4_2951 on theBenchmark for (2951ds/113Mi)
% 25.83/8.18 % (3391949)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=980324233:i=127:av=off:fsr=off:sup=off_2951 on theBenchmark for (2951ds/127Mi)
% 25.83/8.18 % (3391948)Instruction limit reached!
% 25.83/8.18 % (3391948)------------------------------
% 25.83/8.18 % (3391948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391948)CaDiCaL version: 2.1.3
% 25.83/8.18 % (3391948)Termination reason: Instruction limit
% 25.83/8.18 % (3391948)Termination phase: SInE selection
% 25.83/8.18 % (3391948)Time elapsed: 0.057 s
% 25.83/8.18 % (3391948)Peak memory usage: 270 MB
% 25.83/8.18 % (3391948)Instructions burned: 114 (million)
% 25.83/8.18 % (3391946)Instruction limit reached!
% 25.83/8.18 % (3391946)------------------------------
% 25.83/8.18 % (3391946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391946)CaDiCaL version: 2.1.3
% 25.83/8.18 % (3391946)Termination reason: Instruction limit
% 25.83/8.18 % (3391946)Termination phase: SInE selection
% 25.83/8.18 % (3391946)Time elapsed: 0.127 s
% 25.83/8.18 % (3391946)Peak memory usage: 270 MB
% 25.83/8.18 % (3391946)Instructions burned: 294 (million)
% 25.83/8.18 % (3391949)Instruction limit reached!
% 25.83/8.18 % (3391949)------------------------------
% 25.83/8.18 % (3391949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.83/8.18 % (3391949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.83/8.18 % (3391949)CaDiCaL version: 2.1.3
% 28.71/8.66 % (3391949)Termination reason: Instruction limit
% 28.71/8.66 % (3391949)Termination phase: Preprocessing 1
% 28.71/8.66 % (3391949)Time elapsed: 0.099 s
% 28.71/8.66 % (3391949)Peak memory usage: 270 MB
% 28.71/8.66 % (3391949)Instructions burned: 127 (million)
% 28.71/8.66 % (3391955)lrs+10_1_sil=8000:sp=occurrence:random_seed=1900102341:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2949 on theBenchmark for (2949ds/907Mi)
% 28.71/8.66 % (3391954)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1953217194:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2949 on theBenchmark for (2949ds/114Mi)
% 28.71/8.66 % (3391956)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=440018282:i=437:sd=1:aac=none:ss=included_2948 on theBenchmark for (2948ds/437Mi)
% 28.71/8.66 % (3391954)Instruction limit reached!
% 28.71/8.66 % (3391954)------------------------------
% 28.71/8.66 % (3391954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/8.66 % (3391954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/8.66 % (3391954)CaDiCaL version: 2.1.3
% 28.71/8.66 % (3391954)Termination reason: Instruction limit
% 28.71/8.66 % (3391954)Termination phase: Property scanning
% 28.71/8.66 % (3391954)Time elapsed: 0.100 s
% 28.71/8.66 % (3391954)Peak memory usage: 270 MB
% 28.71/8.66 % (3391954)Instructions burned: 116 (million)
% 28.71/8.66 % (3391956)Instruction limit reached!
% 28.71/8.66 % (3391956)------------------------------
% 28.71/8.66 % (3391956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/8.66 % (3391956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/8.66 % (3391956)CaDiCaL version: 2.1.3
% 28.71/8.66 % (3391956)Termination reason: Instruction limit
% 28.71/8.66 % (3391956)Termination phase: SInE selection
% 28.71/8.66 % (3391956)Time elapsed: 0.179 s
% 28.71/8.66 % (3391956)Peak memory usage: 270 MB
% 28.71/8.66 % (3391956)Instructions burned: 438 (million)
% 28.71/8.66 % (3391960)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3608314021:i=5202:ss=axioms:sgt=16_2946 on theBenchmark for (2946ds/5202Mi)
% 28.71/8.66 % (3391955)Instruction limit reached!
% 28.71/8.66 % (3391955)------------------------------
% 28.71/8.66 % (3391955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/8.66 % (3391955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/8.66 % (3391955)CaDiCaL version: 2.1.3
% 28.71/8.66 % (3391955)Termination reason: Instruction limit
% 28.71/8.66 % (3391955)Termination phase: SInE selection
% 28.71/8.66 % (3391955)Time elapsed: 0.356 s
% 28.71/8.66 % (3391955)Peak memory usage: 275 MB
% 28.71/8.66 % (3391955)Instructions burned: 910 (million)
% 28.71/8.66 % (3391961)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=785274266:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2945 on theBenchmark for (2945ds/134Mi)
% 28.71/8.66 % (3391961)Instruction limit reached!
% 28.71/8.66 % (3391961)------------------------------
% 28.71/8.66 % (3391961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/8.66 % (3391961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/8.66 % (3391961)CaDiCaL version: 2.1.3
% 28.71/8.66 % (3391961)Termination reason: Instruction limit
% 28.71/8.66 % (3391961)Termination phase: SInE selection
% 28.71/8.66 % (3391961)Time elapsed: 0.068 s
% 28.71/8.66 % (3391961)Peak memory usage: 270 MB
% 28.71/8.66 % (3391961)Instructions burned: 135 (million)
% 28.71/8.66 % (3391963)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3561599678:st=8:i=592:sd=3:ep=RST:ss=axioms_2944 on theBenchmark for (2944ds/592Mi)
% 28.71/8.66 % (3391965)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3432947132:st=3:i=13193:sd=3:ss=axioms_2942 on theBenchmark for (2942ds/13193Mi)
% 28.71/8.66 % (3391963)Instruction limit reached!
% 28.71/8.66 % (3391963)------------------------------
% 28.71/8.66 % (3391963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.71/8.66 % (3391963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.71/8.66 % (3391963)CaDiCaL version: 2.1.3
% 28.71/8.66 % (3391963)Termination reason: Instruction limit
% 28.71/8.66 % (3391963)Termination phase: SInE selection
% 28.71/8.66 % (3391963)Time elapsed: 0.246 s
% 28.71/8.66 % (3391963)Peak memory usage: 272 MB
% 28.71/8.66 % (3391963)Instructions burned: 592 (million)
% 28.71/8.66 % (3391968)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=1142871243:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2939 on theBenchmark for (2939ds/125Mi)
% 50.32/11.70 % (3391968)Instruction limit reached!
% 50.32/11.70 % (3391968)------------------------------
% 50.32/11.70 % (3391968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.32/11.70 % (3391968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.32/11.70 % (3391968)CaDiCaL version: 2.1.3
% 50.32/11.70 % (3391968)Termination reason: Instruction limit
% 50.32/11.70 % (3391968)Termination phase: Property scanning
% 50.32/11.70 % (3391968)Time elapsed: 0.105 s
% 50.32/11.70 % (3391968)Peak memory usage: 270 MB
% 50.32/11.70 % (3391968)Instructions burned: 127 (million)
% 50.32/11.70 % (3391947)Instruction limit reached!
% 50.32/11.70 % (3391947)------------------------------
% 50.32/11.70 % (3391947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.32/11.70 % (3391947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.32/11.70 % (3391947)CaDiCaL version: 2.1.3
% 50.32/11.70 % (3391947)Termination reason: Instruction limit
% 50.32/11.70 % (3391947)Termination phase: Naming
% 50.32/11.70 % (3391947)Time elapsed: 1.411 s
% 50.32/11.70 % (3391947)Peak memory usage: 355 MB
% 50.32/11.70 % (3391947)Instructions burned: 2350 (million)
% 50.32/11.70 % (3391970)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=258192462:i=134:gtgl=5:slsql=off:gtg=exists_sym_2936 on theBenchmark for (2936ds/134Mi)
% 50.32/11.70 % (3391971)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1571921452:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2936 on theBenchmark for (2936ds/141Mi)
% 50.32/11.70 % (3391970)Instruction limit reached!
% 50.32/11.70 % (3391970)------------------------------
% 50.32/11.70 % (3391970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.32/11.70 % (3391970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.32/11.70 % (3391970)CaDiCaL version: 2.1.3
% 50.32/11.70 % (3391970)Termination reason: Instruction limit
% 50.32/11.70 % (3391970)Termination phase: Property scanning
% 50.32/11.70 % (3391970)Time elapsed: 0.107 s
% 50.32/11.70 % (3391970)Peak memory usage: 270 MB
% 50.32/11.70 % (3391970)Instructions burned: 134 (million)
% 50.32/11.70 % (3391971)Instruction limit reached!
% 50.32/11.70 % (3391971)------------------------------
% 50.32/11.70 % (3391971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.32/11.70 % (3391971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.32/11.70 % (3391971)CaDiCaL version: 2.1.3
% 50.32/11.70 % (3391971)Termination reason: Instruction limit
% 50.32/11.70 % (3391971)Termination phase: SInE selection
% 50.32/11.70 % (3391971)Time elapsed: 0.070 s
% 50.32/11.70 % (3391971)Peak memory usage: 270 MB
% 50.32/11.70 % (3391971)Instructions burned: 141 (million)
% 50.32/11.70 % (3391974)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2012823505:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2933 on theBenchmark for (2933ds/431Mi)
% 50.32/11.70 % (3391975)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=3018347131:i=6060:aac=none:ins=25_2933 on theBenchmark for (2933ds/6060Mi)
% 50.32/11.70 % (3391974)Instruction limit reached!
% 50.32/11.70 % (3391974)------------------------------
% 50.32/11.70 % (3391974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.32/11.70 % (3391974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.32/11.70 % (3391974)CaDiCaL version: 2.1.3
% 50.32/11.70 % (3391974)Termination reason: Instruction limit
% 50.32/11.70 % (3391974)Termination phase: SInE selection
% 50.32/11.70 % (3391974)Time elapsed: 0.182 s
% 50.32/11.70 % (3391974)Peak memory usage: 270 MB
% 50.32/11.70 % (3391974)Instructions burned: 432 (million)
% 50.32/11.70 % (3391978)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=2745557083:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2930 on theBenchmark for (2930ds/150Mi)
% 50.32/11.70 % (3391978)Instruction limit reached!
% 50.32/11.70 % (3391978)------------------------------
% 50.32/11.70 % (3391978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.32/11.70 % (3391978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.32/11.70 % (3391978)CaDiCaL version: 2.1.3
% 50.32/11.70 % (3391978)Termination reason: Instruction limit
% 105.77/19.47 % (3391978)Termination phase: SInE selection
% 105.77/19.47 % (3391978)Time elapsed: 0.074 s
% 105.77/19.47 % (3391978)Peak memory usage: 270 MB
% 105.77/19.47 % (3391978)Instructions burned: 151 (million)
% 105.77/19.47 % (3391980)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3034452700:i=14155:bd=all_2927 on theBenchmark for (2927ds/14155Mi)
% 105.77/19.47 [W927 11:46:48.412899753 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.412947509 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.412998883 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413020760 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413047710 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413068420 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413096866 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413110390 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413136320 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413146990 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413174700 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 105.77/19.47 [W927 11:46:48.413186156 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.
% 105.77/19.47 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 127.05/22.40 % (3391960)Instruction limit reached!
% 127.05/22.40 % (3391960)------------------------------
% 127.05/22.40 % (3391960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.40 % (3391960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.40 % (3391960)CaDiCaL version: 2.1.3
% 127.05/22.40 % (3391960)Termination reason: Instruction limit
% 127.05/22.40 % (3391960)Termination phase: Property scanning
% 127.05/22.40 % (3391960)Time elapsed: 3.211 s
% 127.05/22.40 % (3391960)Peak memory usage: 422 MB
% 127.05/22.40 % (3391960)Instructions burned: 5203 (million)
% 127.05/22.40 % (3391982)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2202421469:i=667:av=off:fsr=off_2912 on theBenchmark for (2912ds/667Mi)
% 127.05/22.40 % (3391982)Instruction limit reached!
% 127.05/22.40 % (3391982)------------------------------
% 127.05/22.40 % (3391982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.40 % (3391982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.40 % (3391982)CaDiCaL version: 2.1.3
% 127.05/22.40 % (3391982)Termination reason: Instruction limit
% 127.05/22.40 % (3391982)Termination phase: Unused predicate definition removal
% 127.05/22.40 % (3391982)Time elapsed: 0.555 s
% 127.05/22.40 % (3391982)Peak memory usage: 346 MB
% 127.05/22.40 % (3391982)Instructions burned: 667 (million)
% 127.05/22.40 % (3391984)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=1172842062:s2a=on:i=185:s2at=1.8:fdi=4_2904 on theBenchmark for (2904ds/185Mi)
% 127.05/22.40 % (3391984)Instruction limit reached!
% 127.05/22.40 % (3391984)------------------------------
% 127.05/22.40 % (3391984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.40 % (3391984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.40 % (3391984)CaDiCaL version: 2.1.3
% 127.05/22.40 % (3391984)Termination reason: Instruction limit
% 127.05/22.40 % (3391984)Termination phase: SInE selection
% 127.05/22.40 % (3391984)Time elapsed: 0.088 s
% 127.05/22.40 % (3391984)Peak memory usage: 270 MB
% 127.05/22.40 % (3391984)Instructions burned: 185 (million)
% 127.05/22.40 % (3391986)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2315179492:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2901 on theBenchmark for (2901ds/193Mi)
% 127.05/22.40 % (3391986)Instruction limit reached!
% 127.05/22.40 % (3391986)------------------------------
% 127.05/22.40 % (3391986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.40 % (3391986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.40 % (3391986)CaDiCaL version: 2.1.3
% 127.05/22.40 % (3391986)Termination reason: Instruction limit
% 127.05/22.40 % (3391986)Termination phase: SInE selection
% 127.05/22.40 % (3391986)Time elapsed: 0.089 s
% 127.05/22.40 % (3391986)Peak memory usage: 270 MB
% 127.05/22.40 % (3391986)Instructions burned: 195 (million)
% 127.05/22.40 % (3391988)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3043623202:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2899 on theBenchmark for (2899ds/4850Mi)
% 127.05/22.40 % (3391965)Refutation not found, incomplete strategy
% 127.05/22.40 % (3391965)------------------------------
% 127.05/22.40 % (3391965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.40 % (3391965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.40 % (3391965)CaDiCaL version: 2.1.3
% 127.05/22.40 % (3391965)Termination reason: Refutation not found, incomplete strategy
% 127.05/22.40 % (3391965)Time elapsed: 4.441 s
% 127.05/22.40 % (3391965)Peak memory usage: 774 MB
% 127.05/22.40 % (3391965)Instructions burned: 6762 (million)
% 127.05/22.40 % (3391975)Instruction limit reached!
% 127.05/22.40 % (3391975)------------------------------
% 127.05/22.40 % (3391975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.40 % (3391975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.40 % (3391975)CaDiCaL version: 2.1.3
% 127.05/22.40 % (3391975)Termination reason: Instruction limit
% 127.05/22.40 % (3391975)Termination phase: Property scanning
% 127.05/22.40 % (3391975)Time elapsed: 3.722 s
% 127.05/22.40 % (3391975)Peak memory usage: 470 MB
% 127.05/22.40 % (3391975)Instructions burned: 6061 (million)
% 127.05/22.40 % (3391990)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1442457281:i=12111:sd=1:ss=included_2894 on theBenchmark for (2894ds/12111Mi)
% 127.05/22.45 % (3391965)------------------------------
% 127.05/22.45 % (3391965)------------------------------
% 127.05/22.45 % (3391992)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1540321756:i=319:kws=precedence:fsr=off_2891 on theBenchmark for (2891ds/319Mi)
% 127.05/22.45 % (3391992)Instruction limit reached!
% 127.05/22.45 % (3391992)------------------------------
% 127.05/22.45 % (3391992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.45 % (3391992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.45 % (3391992)CaDiCaL version: 2.1.3
% 127.05/22.45 % (3391992)Termination reason: Instruction limit
% 127.05/22.45 % (3391992)Termination phase: Preprocessing 1
% 127.05/22.45 % (3391992)Time elapsed: 0.238 s
% 127.05/22.45 % (3391992)Peak memory usage: 270 MB
% 127.05/22.45 % (3391992)Instructions burned: 319 (million)
% 127.05/22.45 % (3391994)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3348130357:i=2064:ep=RST_2887 on theBenchmark for (2887ds/2064Mi)
% 127.05/22.45 % (3391994)Instruction limit reached!
% 127.05/22.45 % (3391994)------------------------------
% 127.05/22.45 % (3391994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.45 % (3391994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.45 % (3391994)CaDiCaL version: 2.1.3
% 127.05/22.45 % (3391994)Termination reason: Instruction limit
% 127.05/22.45 % (3391994)Termination phase: Preprocessing 3
% 127.05/22.45 % (3391994)Time elapsed: 1.305 s
% 127.05/22.45 % (3391994)Peak memory usage: 351 MB
% 127.05/22.45 % (3391994)Instructions burned: 2066 (million)
% 127.05/22.45 % (3391996)dis-1011_128_sil=32000:random_seed=4008482099:i=3706:ep=RST:av=off_2872 on theBenchmark for (2872ds/3706Mi)
% 127.05/22.45 % (3391988)Instruction limit reached!
% 127.05/22.45 % (3391988)------------------------------
% 127.05/22.45 % (3391988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.45 % (3391988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.45 % (3391988)CaDiCaL version: 2.1.3
% 127.05/22.45 % (3391988)Termination reason: Instruction limit
% 127.05/22.45 % (3391988)Termination phase: Clausification
% 127.05/22.45 % (3391988)Time elapsed: 3.047 s
% 127.05/22.45 % (3391988)Peak memory usage: 528 MB
% 127.05/22.45 % (3391988)Instructions burned: 4851 (million)
% 127.05/22.45 % (3391998)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=424180233:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2866 on theBenchmark for (2866ds/757Mi)
% 127.05/22.45 % (3391998)Instruction limit reached!
% 127.05/22.45 % (3391998)------------------------------
% 127.05/22.45 % (3391998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.45 % (3391998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.45 % (3391998)CaDiCaL version: 2.1.3
% 127.05/22.45 % (3391998)Termination reason: Instruction limit
% 127.05/22.45 % (3391998)Termination phase: SInE selection
% 127.05/22.45 % (3391998)Time elapsed: 0.308 s
% 127.05/22.45 % (3391998)Peak memory usage: 275 MB
% 127.05/22.45 % (3391998)Instructions burned: 758 (million)
% 127.05/22.45 % (3392000)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2456680302:i=13913:ss=axioms:sgt=8_2861 on theBenchmark for (2861ds/13913Mi)
% 127.05/22.45 % (3391996)Instruction limit reached!
% 127.05/22.45 % (3391996)------------------------------
% 127.05/22.45 % (3391996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.45 % (3391996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.45 % (3391996)CaDiCaL version: 2.1.3
% 127.05/22.45 % (3391996)Termination reason: Instruction limit
% 127.05/22.45 % (3391996)Termination phase: Clausification
% 127.05/22.45 % (3391996)Time elapsed: 2.503 s
% 127.05/22.45 % (3391996)Peak memory usage: 515 MB
% 127.05/22.45 % (3391996)Instructions burned: 3706 (million)
% 127.05/22.45 % (3392002)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4142886380:i=9925:aac=none_2844 on theBenchmark for (2844ds/9925Mi)
% 127.05/22.45 % (3392000)Refutation not found, incomplete strategy
% 127.05/22.45 % (3392000)------------------------------
% 127.05/22.45 % (3392000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.05/22.45 % (3392000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.05/22.45 % (3392000)CaDiCaL version: 2.1.3
% 127.05/22.45 % (3392000)Termination reason: Refutation not found, incomplete strategy
% 156.13/26.50 % (3392000)Time elapsed: 4.459 s
% 156.13/26.50 % (3392000)Peak memory usage: 743 MB
% 156.13/26.50 % (3392000)Instructions burned: 6087 (million)
% 156.13/26.50 % (3391990)Instruction limit reached!
% 156.13/26.50 % (3391990)------------------------------
% 156.13/26.50 % (3391990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.13/26.50 % (3391990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.13/26.50 % (3391990)CaDiCaL version: 2.1.3
% 156.13/26.50 % (3391990)Termination reason: Instruction limit
% 156.13/26.50 % (3391990)Termination phase: Saturation
% 156.13/26.50 % (3391990)Time elapsed: 7.875 s
% 156.13/26.50 % (3391990)Peak memory usage: 1098 MB
% 156.13/26.50 % (3391990)Instructions burned: 12113 (million)
% 156.13/26.50 % (3392000)------------------------------
% 156.13/26.50 % (3392000)------------------------------
% 156.13/26.50 % (3392004)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=4250380104:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2812 on theBenchmark for (2812ds/2479Mi)
% 156.13/26.50 % (3392006)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4151273845:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2810 on theBenchmark for (2810ds/440Mi)
% 156.13/26.50 % (3392006)Instruction limit reached!
% 156.13/26.50 % (3392006)------------------------------
% 156.13/26.50 % (3392006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.13/26.50 % (3392006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.13/26.50 % (3392006)CaDiCaL version: 2.1.3
% 156.13/26.50 % (3392006)Termination reason: Instruction limit
% 156.13/26.50 % (3392006)Termination phase: Property scanning
% 156.13/26.50 % (3392006)Time elapsed: 0.230 s
% 156.13/26.50 % (3392006)Peak memory usage: 270 MB
% 156.13/26.50 % (3392006)Instructions burned: 441 (million)
% 156.13/26.50 % (3392008)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=375604046:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2806 on theBenchmark for (2806ds/11145Mi)
% 156.13/26.50 % (3392004)Refutation not found, incomplete strategy
% 156.13/26.50 % (3392004)------------------------------
% 156.13/26.50 % (3392004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.13/26.50 % (3392004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.13/26.50 % (3392004)CaDiCaL version: 2.1.3
% 156.13/26.50 % (3392004)Termination reason: Refutation not found, incomplete strategy
% 156.13/26.50 % (3392004)Time elapsed: 1.079 s
% 156.13/26.50 % (3392004)Peak memory usage: 351 MB
% 156.13/26.50 % (3392004)Instructions burned: 2442 (million)
% 156.13/26.50 % (3391980)Instruction limit reached!
% 156.13/26.50 % (3391980)------------------------------
% 156.13/26.50 % (3391980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.13/26.50 % (3391980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.13/26.50 % (3391980)CaDiCaL version: 2.1.3
% 156.13/26.50 % (3391980)Termination reason: Instruction limit
% 156.13/26.50 % (3391980)Termination phase: Saturation
% 156.13/26.50 % (3391980)Time elapsed: 12.602 s
% 156.13/26.50 % (3391980)Peak memory usage: 1733 MB
% 156.13/26.50 % (3391980)Instructions burned: 14157 (million)
% 156.13/26.50 % (3392010)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=2002268629:cts=off:i=3034:av=off:er=known:fsd=on_2797 on theBenchmark for (2797ds/3034Mi)
% 156.13/26.50 % (3392004)------------------------------
% 156.13/26.50 % (3392004)------------------------------
% 156.13/26.50 % (3392012)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2651099574:st=2:s2a=on:i=524:s2at=2:ss=axioms_2795 on theBenchmark for (2795ds/524Mi)
% 156.13/26.50 % (3392012)Instruction limit reached!
% 156.13/26.50 % (3392012)------------------------------
% 156.13/26.50 % (3392012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.13/26.50 % (3392012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.13/26.50 % (3392012)CaDiCaL version: 2.1.3
% 156.13/26.50 % (3392012)Termination reason: Instruction limit
% 156.13/26.50 % (3392012)Termination phase: SInE selection
% 156.13/26.50 % (3392012)Time elapsed: 0.219 s
% 156.13/26.50 % (3392012)Peak memory usage: 272 MB
% 156.13/26.50 % (3392012)Instructions burned: 524 (million)
% 156.13/26.50 % (3392014)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3144035955:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2791 on theBenchmark for (2791ds/1016Mi)
% 156.13/26.50 [W927 11:47:02.154182630 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154220767 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154278100 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154290010 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154316977 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154328427 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154355684 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154367284 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154393097 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154404887 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154432594 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 [W927 11:47:02.154443407 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.
% 169.92/28.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 169.92/28.60 % (3392014)Instruction limit reached!
% 169.92/28.60 % (3392014)------------------------------
% 169.92/28.60 % (3392014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392014)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392014)Termination reason: Instruction limit
% 169.92/28.60 % (3392014)Termination phase: Unused predicate definition removal
% 169.92/28.60 % (3392014)Time elapsed: 0.445 s
% 169.92/28.60 % (3392014)Peak memory usage: 293 MB
% 169.92/28.60 % (3392014)Instructions burned: 1016 (million)
% 169.92/28.60 % (3392016)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=2183472550:i=14123:bd=preordered:ins=4_2785 on theBenchmark for (2785ds/14123Mi)
% 169.92/28.60 % (3392002)Instruction limit reached!
% 169.92/28.60 % (3392002)------------------------------
% 169.92/28.60 % (3392002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392002)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392002)Termination reason: Instruction limit
% 169.92/28.60 % (3392002)Termination phase: Saturation
% 169.92/28.60 % (3392002)Time elapsed: 6.011 s
% 169.92/28.60 % (3392002)Peak memory usage: 690 MB
% 169.92/28.60 % (3392002)Instructions burned: 9925 (million)
% 169.92/28.60 % (3392018)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1586440441:i=5781:kws=precedence:bd=all:rawr=on_2782 on theBenchmark for (2782ds/5781Mi)
% 169.92/28.60 % (3392010)Instruction limit reached!
% 169.92/28.60 % (3392010)------------------------------
% 169.92/28.60 % (3392010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392010)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392010)Termination reason: Instruction limit
% 169.92/28.60 % (3392010)Termination phase: Preprocessing 3
% 169.92/28.60 % (3392010)Time elapsed: 1.782 s
% 169.92/28.60 % (3392010)Peak memory usage: 355 MB
% 169.92/28.60 % (3392010)Instructions burned: 3035 (million)
% 169.92/28.60 % (3392020)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=2647425424:i=2448:gtgl=5:bd=preordered:gtg=all_2778 on theBenchmark for (2778ds/2448Mi)
% 169.92/28.60 % (3392020)Instruction limit reached!
% 169.92/28.60 % (3392020)------------------------------
% 169.92/28.60 % (3392020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392020)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392020)Termination reason: Instruction limit
% 169.92/28.60 % (3392020)Termination phase: Property scanning
% 169.92/28.60 % (3392020)Time elapsed: 0.975 s
% 169.92/28.60 % (3392020)Peak memory usage: 270 MB
% 169.92/28.60 % (3392020)Instructions burned: 2449 (million)
% 169.92/28.60 % (3392022)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2461921748:i=3223:kws=precedence:fgj=on:av=off_2766 on theBenchmark for (2766ds/3223Mi)
% 169.92/28.60 % (3392008)Refutation not found, incomplete strategy
% 169.92/28.60 % (3392008)------------------------------
% 169.92/28.60 % (3392008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392008)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392008)Termination reason: Refutation not found, incomplete strategy
% 169.92/28.60 % (3392008)Time elapsed: 4.950 s
% 169.92/28.60 % (3392008)Peak memory usage: 475 MB
% 169.92/28.60 % (3392008)Instructions burned: 7279 (million)
% 169.92/28.60 % (3392008)------------------------------
% 169.92/28.60 % (3392008)------------------------------
% 169.92/28.60 % (3392024)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3195677252:st=5.6:i=2033:sd=3:ss=axioms_2750 on theBenchmark for (2750ds/2033Mi)
% 169.92/28.60 % (3392022)Instruction limit reached!
% 169.92/28.60 % (3392022)------------------------------
% 169.92/28.60 % (3392022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392022)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392022)Termination reason: Instruction limit
% 169.92/28.60 % (3392022)Termination phase: Preprocessing 3
% 169.92/28.60 % (3392022)Time elapsed: 1.900 s
% 169.92/28.60 % (3392022)Peak memory usage: 364 MB
% 169.92/28.60 % (3392022)Instructions burned: 3223 (million)
% 169.92/28.60 % (3392018)Instruction limit reached!
% 169.92/28.60 % (3392018)------------------------------
% 169.92/28.60 % (3392018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392018)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392018)Termination reason: Instruction limit
% 169.92/28.60 % (3392018)Termination phase: Property scanning
% 169.92/28.60 % (3392018)Time elapsed: 3.556 s
% 169.92/28.60 % (3392018)Peak memory usage: 536 MB
% 169.92/28.60 % (3392018)Instructions burned: 5784 (million)
% 169.92/28.60 % (3392026)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2114371184:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2745 on theBenchmark for (2745ds/2055Mi)
% 169.92/28.60 % (3392027)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=3167632215:i=21611:sd=3:ss=axioms_2744 on theBenchmark for (2744ds/21611Mi)
% 169.92/28.60 % (3392024)Instruction limit reached!
% 169.92/28.60 % (3392024)------------------------------
% 169.92/28.60 % (3392024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392024)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392024)Termination reason: Instruction limit
% 169.92/28.60 % (3392024)Termination phase: SInE selection
% 169.92/28.60 % (3392024)Time elapsed: 0.755 s
% 169.92/28.60 % (3392024)Peak memory usage: 276 MB
% 169.92/28.60 % (3392024)Instructions burned: 2034 (million)
% 169.92/28.60 % (3392030)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=4082646044:i=4835:sd=13:ss=axioms:sgt=23_2741 on theBenchmark for (2741ds/4835Mi)
% 169.92/28.60 % (3392026)Instruction limit reached!
% 169.92/28.60 % (3392026)------------------------------
% 169.92/28.60 % (3392026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392026)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392026)Termination reason: Instruction limit
% 169.92/28.60 % (3392026)Termination phase: SInE selection
% 169.92/28.60 % (3392026)Time elapsed: 0.873 s
% 169.92/28.60 % (3392026)Peak memory usage: 277 MB
% 169.92/28.60 % (3392026)Instructions burned: 2058 (million)
% 169.92/28.60 % (3392032)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=3644090238:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2734 on theBenchmark for (2734ds/797Mi)
% 169.92/28.60 % (3392030)First to succeed.
% 169.92/28.60 % (3392030)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3391919"
% 169.92/28.60 % (3392032)Instruction limit reached!
% 169.92/28.60 % (3392032)------------------------------
% 169.92/28.60 % (3392032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 169.92/28.60 % (3392032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 169.92/28.60 % (3392032)CaDiCaL version: 2.1.3
% 169.92/28.60 % (3392032)Termination reason: Instruction limit
% 169.92/28.60 % (3392032)Termination phase: SInE selection
% 169.92/28.60 % (3392032)Time elapsed: 0.322 s
% 169.92/28.60 % (3392032)Peak memory usage: 273 MB
% 169.92/28.60 % (3392032)Instructions burned: 797 (million)
% 169.92/28.60 % (3392034)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3598242666:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2729 on theBenchmark for (2729ds/2326Mi)
% 169.92/28.60 % (3392030)Refutation found. Thanks to Tanya!
% 169.92/28.60 % SZS status Theorem for theBenchmark
% 169.92/28.60 % SZS output start Proof for theBenchmark
% See solution above
% 170.22/28.98 % (3392030)------------------------------
% 170.22/28.98 % (3392030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 170.22/28.98 % (3392030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.22/28.98 % (3392030)CaDiCaL version: 2.1.3
% 170.22/28.98 % (3392030)Termination reason: Refutation
% 170.22/28.98 % (3392030)Time elapsed: 0.850 s
% 170.22/28.98 % (3392030)Peak memory usage: 355 MB
% 170.22/28.98 % (3392030)Instructions burned: 1557 (million)
% 170.22/28.98 % (3392030)------------------------------
% 170.22/28.98 % (3392030)------------------------------
% 170.22/28.98 % (3391919)Success in time 27.627 s
% 170.22/28.98 % Vampire exiting
%------------------------------------------------------------------------------