%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV126+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:52:44 AM UTC 2026
% Result : Theorem 187.89s 37.20s
% Output : Refutation 231.70s
% 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(f35,conjecture,
! [X0] :
( reachableState(X0)
=> v4(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssertion) ).
fof(f36,negated_conjecture,
~ ! [X0] :
( reachableState(X0)
=> v4(X0) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,axiom,
! [X0] :
( ~ v4(X0)
<=> v231505(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18766) ).
fof(f38,axiom,
! [X0] :
( ~ v231505(X0)
<=> v231506(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18765) ).
fof(f39,axiom,
! [X0] :
( v231506(X0)
<=> ( v231508(X0)
& v231526(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32503) ).
fof(f40,axiom,
! [X0] :
( v231526(X0)
<=> ( v231527(X0)
| v231511(X0,bitIndex3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8391) ).
fof(f41,axiom,
! [X0] :
( v231527(X0)
<=> ( v231528(X0)
| v231511(X0,bitIndex2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8390) ).
fof(f42,axiom,
! [X0] :
( v231528(X0)
<=> ( v231511(X0,bitIndex0)
| v231511(X0,bitIndex1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8389) ).
fof(f43,axiom,
! [X0] :
( v231508(X0)
<=> ( v231509(X0)
| v231517(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32502) ).
fof(f44,axiom,
! [X0] :
( v231517(X0)
<=> ( v231518(X0)
| v231519(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32501) ).
fof(f45,axiom,
! [X0] :
( v231519(X0)
<=> ( v231510(X0)
& v231520(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32500) ).
fof(f46,axiom,
! [X0] :
( v231520(X0)
<=> ( v231521(X0)
| v231522(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32499) ).
fof(f47,axiom,
! [X0] :
( v231522(X0)
<=> ( v231513(X0)
& v231523(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32498) ).
fof(f48,axiom,
! [X0] :
( v231523(X0)
<=> ( v231524(X0)
| v231525(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32497) ).
fof(f49,axiom,
! [X0] :
( v231525(X0)
<=> ( v231511(X0,bitIndex0)
& v231516(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32496) ).
fof(f50,axiom,
! [X0] :
( v231524(X0)
<=> ( v231515(X0)
& v231511(X0,bitIndex1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8388) ).
fof(f51,axiom,
! [X0] :
( v231521(X0)
<=> ( v231511(X0,bitIndex2)
& v231514(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8387) ).
fof(f52,axiom,
! [X0] :
( v231518(X0)
<=> ( v231511(X0,bitIndex3)
& v231512(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorShiftedRanges_8386) ).
fof(f53,axiom,
! [X0] :
( v231509(X0)
<=> ( v231510(X0)
& v231512(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32495) ).
fof(f54,axiom,
! [X0] :
( v231512(X0)
<=> ( v231513(X0)
& v231514(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32494) ).
fof(f55,axiom,
! [X0] :
( v231514(X0)
<=> ( v231515(X0)
& v231516(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_32493) ).
fof(f56,axiom,
! [X0] :
( ~ v231516(X0)
<=> v231511(X0,bitIndex1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18764) ).
fof(f57,axiom,
! [X0] :
( ~ v231515(X0)
<=> v231511(X0,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18763) ).
fof(f58,axiom,
! [X0] :
( ~ v231513(X0)
<=> v231511(X0,bitIndex2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18762) ).
fof(f59,axiom,
! [X0] :
( ~ v231510(X0)
<=> v231511(X0,bitIndex3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18761) ).
fof(f60,axiom,
! [X0,X1] :
( range_3_0(X1)
=> ( v231511(X0,X1)
<=> v6(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118543) ).
fof(f61,axiom,
! [X0] :
( ~ v231494(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> v231496(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_3223) ).
fof(f62,axiom,
! [X0] :
( v231494(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v6(X0,X1)
<=> b0001(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_3183) ).
fof(f63,axiom,
! [X0] :
( ~ v231497(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231496(X0,X1)
<=> v231499(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_3222) ).
fof(f64,axiom,
! [X0] :
( v231497(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231496(X0,X1)
<=> b0010(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_3182) ).
fof(f65,axiom,
! [X0] :
( ~ v2311(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231499(X0,X1)
<=> v231502(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aaddConditionBooleanCondEqualRangesElseBranch_3221) ).
fof(f66,axiom,
! [X0] :
( v2311(X0)
=> ! [X1] :
( range_3_0(X1)
=> ( v231499(X0,X1)
<=> v231500(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addConditionBooleanCondEqualRangesThenBranch_3181) ).
fof(f67,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v231502(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118542) ).
fof(f68,axiom,
! [X0] :
( v231502(X0,bitIndex2)
<=> v231503(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118541) ).
fof(f69,axiom,
! [X0] :
( v231502(X0,bitIndex3)
<=> v126476(X0,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118540) ).
fof(f70,axiom,
! [X0] :
( ~ v231503(X0)
<=> v126476(X0,bitIndex0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18760) ).
fof(f71,axiom,
! [X0,X1] :
( range_1_0(X1)
=> ( v231500(X0,X1)
<=> $false ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118539) ).
fof(f72,axiom,
! [X0] :
( v231500(X0,bitIndex2)
<=> v231501(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118538) ).
fof(f73,axiom,
! [X0] :
( v231500(X0,bitIndex3)
<=> v126476(X0,bitIndex1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',addAssignment_118537) ).
fof(f74,axiom,
! [X0] :
( ~ v231501(X0)
<=> v126476(X0,bitIndex1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',writeUnaryOperator_18759) ).
fof(f119393,axiom,
~ b0010(bitIndex3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_1021) ).
fof(f119394,axiom,
~ b0010(bitIndex2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_1020) ).
fof(f119395,axiom,
b0010(bitIndex1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_1019) ).
fof(f119396,axiom,
~ b0010(bitIndex0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_1018) ).
fof(f197680,axiom,
~ b0001(bitIndex3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_290) ).
fof(f197681,axiom,
~ b0001(bitIndex2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_289) ).
fof(f197682,axiom,
~ b0001(bitIndex1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_288) ).
fof(f197683,axiom,
b0001(bitIndex0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bitBlastConstant_287) ).
fof(f202414,axiom,
! [X0] :
( range_3_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_axiom_22) ).
fof(f202956,axiom,
! [X0] :
( range_1_0(X0)
<=> ( $false
| bitIndex0 = X0
| bitIndex1 = X0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_axiom_7) ).
fof(f204721,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231500(X0,X1) ),
inference(true_and_false_elimination,[],[f71]) ).
fof(f204722,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231500(X0,X1) ),
inference(flattening,[],[f204721]) ).
fof(f204723,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231502(X0,X1) ),
inference(true_and_false_elimination,[],[f67]) ).
fof(f204724,plain,
! [X0,X1] :
( range_1_0(X1)
=> ~ v231502(X0,X1) ),
inference(flattening,[],[f204723]) ).
fof(f204825,plain,
! [X0] :
( range_1_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0 ) ),
inference(true_and_false_elimination,[],[f202956]) ).
fof(f204827,plain,
! [X0] :
( range_3_0(X0)
<=> ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 ) ),
inference(true_and_false_elimination,[],[f202414]) ).
fof(f205098,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0 )
=> range_1_0(X0) ),
inference(unused_predicate_definition_removal,[],[f204825]) ).
fof(f205099,plain,
! [X0] :
( ( bitIndex0 = X0
| bitIndex1 = X0
| bitIndex2 = X0
| bitIndex3 = X0 )
=> range_3_0(X0) ),
inference(unused_predicate_definition_removal,[],[f204827]) ).
fof(f205100,plain,
! [X0] :
( ~ v4(X0)
=> v231505(X0) ),
inference(unused_predicate_definition_removal,[],[f37]) ).
fof(f205101,plain,
! [X0] :
( v231506(X0)
=> ~ v231505(X0) ),
inference(unused_predicate_definition_removal,[],[f38]) ).
fof(f205102,plain,
! [X0] :
( ( v231508(X0)
& v231526(X0) )
=> v231506(X0) ),
inference(unused_predicate_definition_removal,[],[f39]) ).
fof(f205103,plain,
! [X0] :
( ( v231509(X0)
| v231517(X0) )
=> v231508(X0) ),
inference(unused_predicate_definition_removal,[],[f43]) ).
fof(f205104,plain,
! [X0] :
( ( v231510(X0)
& v231512(X0) )
=> v231509(X0) ),
inference(unused_predicate_definition_removal,[],[f53]) ).
fof(f205105,plain,
! [X0] :
( ( v231518(X0)
| v231519(X0) )
=> v231517(X0) ),
inference(unused_predicate_definition_removal,[],[f44]) ).
fof(f205106,plain,
! [X0] :
( ( v231511(X0,bitIndex3)
& v231512(X0) )
=> v231518(X0) ),
inference(unused_predicate_definition_removal,[],[f52]) ).
fof(f205107,plain,
! [X0] :
( ( v231513(X0)
& v231514(X0) )
=> v231512(X0) ),
inference(unused_predicate_definition_removal,[],[f54]) ).
fof(f205108,plain,
! [X0] :
( ( v231510(X0)
& v231520(X0) )
=> v231519(X0) ),
inference(unused_predicate_definition_removal,[],[f45]) ).
fof(f205109,plain,
! [X0] :
( ~ v231510(X0)
=> v231511(X0,bitIndex3) ),
inference(unused_predicate_definition_removal,[],[f59]) ).
fof(f205110,plain,
! [X0] :
( ( v231521(X0)
| v231522(X0) )
=> v231520(X0) ),
inference(unused_predicate_definition_removal,[],[f46]) ).
fof(f205111,plain,
! [X0] :
( ( v231511(X0,bitIndex2)
& v231514(X0) )
=> v231521(X0) ),
inference(unused_predicate_definition_removal,[],[f51]) ).
fof(f205112,plain,
! [X0] :
( ( v231515(X0)
& v231516(X0) )
=> v231514(X0) ),
inference(unused_predicate_definition_removal,[],[f55]) ).
fof(f205113,plain,
! [X0] :
( ( v231513(X0)
& v231523(X0) )
=> v231522(X0) ),
inference(unused_predicate_definition_removal,[],[f47]) ).
fof(f205114,plain,
! [X0] :
( ~ v231513(X0)
=> v231511(X0,bitIndex2) ),
inference(unused_predicate_definition_removal,[],[f58]) ).
fof(f205115,plain,
! [X0] :
( ( v231524(X0)
| v231525(X0) )
=> v231523(X0) ),
inference(unused_predicate_definition_removal,[],[f48]) ).
fof(f205116,plain,
! [X0] :
( ( v231515(X0)
& v231511(X0,bitIndex1) )
=> v231524(X0) ),
inference(unused_predicate_definition_removal,[],[f50]) ).
fof(f205117,plain,
! [X0] :
( ~ v231515(X0)
=> v231511(X0,bitIndex0) ),
inference(unused_predicate_definition_removal,[],[f57]) ).
fof(f205118,plain,
! [X0] :
( ( v231511(X0,bitIndex0)
& v231516(X0) )
=> v231525(X0) ),
inference(unused_predicate_definition_removal,[],[f49]) ).
fof(f205119,plain,
! [X0] :
( ~ v231516(X0)
=> v231511(X0,bitIndex1) ),
inference(unused_predicate_definition_removal,[],[f56]) ).
fof(f205120,plain,
! [X0] :
( ( v231527(X0)
| v231511(X0,bitIndex3) )
=> v231526(X0) ),
inference(unused_predicate_definition_removal,[],[f40]) ).
fof(f205121,plain,
! [X0] :
( ( v231528(X0)
| v231511(X0,bitIndex2) )
=> v231527(X0) ),
inference(unused_predicate_definition_removal,[],[f41]) ).
fof(f205122,plain,
! [X0] :
( ( v231511(X0,bitIndex0)
| v231511(X0,bitIndex1) )
=> v231528(X0) ),
inference(unused_predicate_definition_removal,[],[f42]) ).
fof(f205175,plain,
~ ! [X0] : v4(X0),
inference(pure_predicate_removal,[],[f36]) ).
fof(f205252,plain,
? [X0] : ~ v4(X0),
inference(ennf_transformation,[],[f205175]) ).
fof(f205253,plain,
! [X0] :
( v231505(X0)
| v4(X0) ),
inference(ennf_transformation,[],[f205100]) ).
fof(f205254,plain,
! [X0] :
( ~ v231505(X0)
| ~ v231506(X0) ),
inference(ennf_transformation,[],[f205101]) ).
fof(f205255,plain,
! [X0] :
( v231506(X0)
| ~ v231508(X0)
| ~ v231526(X0) ),
inference(ennf_transformation,[],[f205102]) ).
fof(f205256,plain,
! [X0] :
( v231506(X0)
| ~ v231508(X0)
| ~ v231526(X0) ),
inference(flattening,[],[f205255]) ).
fof(f205257,plain,
! [X0] :
( v231508(X0)
| ( ~ v231509(X0)
& ~ v231517(X0) ) ),
inference(ennf_transformation,[],[f205103]) ).
fof(f205258,plain,
! [X0] :
( v231526(X0)
| ( ~ v231527(X0)
& ~ v231511(X0,bitIndex3) ) ),
inference(ennf_transformation,[],[f205120]) ).
fof(f205259,plain,
! [X0] :
( v231509(X0)
| ~ v231510(X0)
| ~ v231512(X0) ),
inference(ennf_transformation,[],[f205104]) ).
fof(f205260,plain,
! [X0] :
( v231509(X0)
| ~ v231510(X0)
| ~ v231512(X0) ),
inference(flattening,[],[f205259]) ).
fof(f205261,plain,
! [X0] :
( v231517(X0)
| ( ~ v231518(X0)
& ~ v231519(X0) ) ),
inference(ennf_transformation,[],[f205105]) ).
fof(f205262,plain,
! [X0] :
( v231527(X0)
| ( ~ v231528(X0)
& ~ v231511(X0,bitIndex2) ) ),
inference(ennf_transformation,[],[f205121]) ).
fof(f205263,plain,
! [X0,X1] :
( ( v231511(X0,X1)
<=> v6(X0,X1) )
| ~ range_3_0(X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f205264,plain,
! [X0] :
( v231511(X0,bitIndex3)
| v231510(X0) ),
inference(ennf_transformation,[],[f205109]) ).
fof(f205265,plain,
! [X0] :
( v231511(X0,bitIndex2)
| v231513(X0) ),
inference(ennf_transformation,[],[f205114]) ).
fof(f205266,plain,
! [X0] :
( v231511(X0,bitIndex0)
| v231515(X0) ),
inference(ennf_transformation,[],[f205117]) ).
fof(f205267,plain,
! [X0] :
( v231511(X0,bitIndex1)
| v231516(X0) ),
inference(ennf_transformation,[],[f205119]) ).
fof(f205268,plain,
! [X0] :
( v231518(X0)
| ~ v231511(X0,bitIndex3)
| ~ v231512(X0) ),
inference(ennf_transformation,[],[f205106]) ).
fof(f205269,plain,
! [X0] :
( v231518(X0)
| ~ v231511(X0,bitIndex3)
| ~ v231512(X0) ),
inference(flattening,[],[f205268]) ).
fof(f205270,plain,
! [X0] :
( v231521(X0)
| ~ v231511(X0,bitIndex2)
| ~ v231514(X0) ),
inference(ennf_transformation,[],[f205111]) ).
fof(f205271,plain,
! [X0] :
( v231521(X0)
| ~ v231511(X0,bitIndex2)
| ~ v231514(X0) ),
inference(flattening,[],[f205270]) ).
fof(f205272,plain,
! [X0] :
( v231524(X0)
| ~ v231515(X0)
| ~ v231511(X0,bitIndex1) ),
inference(ennf_transformation,[],[f205116]) ).
fof(f205273,plain,
! [X0] :
( v231524(X0)
| ~ v231515(X0)
| ~ v231511(X0,bitIndex1) ),
inference(flattening,[],[f205272]) ).
fof(f205274,plain,
! [X0] :
( v231525(X0)
| ~ v231511(X0,bitIndex0)
| ~ v231516(X0) ),
inference(ennf_transformation,[],[f205118]) ).
fof(f205275,plain,
! [X0] :
( v231525(X0)
| ~ v231511(X0,bitIndex0)
| ~ v231516(X0) ),
inference(flattening,[],[f205274]) ).
fof(f205276,plain,
! [X0] :
( v231528(X0)
| ( ~ v231511(X0,bitIndex0)
& ~ v231511(X0,bitIndex1) ) ),
inference(ennf_transformation,[],[f205122]) ).
fof(f205277,plain,
! [X0] :
( v231519(X0)
| ~ v231510(X0)
| ~ v231520(X0) ),
inference(ennf_transformation,[],[f205108]) ).
fof(f205278,plain,
! [X0] :
( v231519(X0)
| ~ v231510(X0)
| ~ v231520(X0) ),
inference(flattening,[],[f205277]) ).
fof(f205279,plain,
! [X0] :
( v231512(X0)
| ~ v231513(X0)
| ~ v231514(X0) ),
inference(ennf_transformation,[],[f205107]) ).
fof(f205280,plain,
! [X0] :
( v231512(X0)
| ~ v231513(X0)
| ~ v231514(X0) ),
inference(flattening,[],[f205279]) ).
fof(f205281,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> b0001(X1) )
| ~ range_3_0(X1) )
| ~ v231494(X0) ),
inference(ennf_transformation,[],[f62]) ).
fof(f205282,plain,
! [X0] :
( ! [X1] :
( ( v6(X0,X1)
<=> v231496(X0,X1) )
| ~ range_3_0(X1) )
| v231494(X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f205283,plain,
! [X0] :
( v231522(X0)
| ~ v231513(X0)
| ~ v231523(X0) ),
inference(ennf_transformation,[],[f205113]) ).
fof(f205284,plain,
! [X0] :
( v231522(X0)
| ~ v231513(X0)
| ~ v231523(X0) ),
inference(flattening,[],[f205283]) ).
fof(f205285,plain,
! [X0] :
( v231514(X0)
| ~ v231515(X0)
| ~ v231516(X0) ),
inference(ennf_transformation,[],[f205112]) ).
fof(f205286,plain,
! [X0] :
( v231514(X0)
| ~ v231515(X0)
| ~ v231516(X0) ),
inference(flattening,[],[f205285]) ).
fof(f205287,plain,
! [X0] :
( v231520(X0)
| ( ~ v231521(X0)
& ~ v231522(X0) ) ),
inference(ennf_transformation,[],[f205110]) ).
fof(f205288,plain,
! [X0] :
( v231523(X0)
| ( ~ v231524(X0)
& ~ v231525(X0) ) ),
inference(ennf_transformation,[],[f205115]) ).
fof(f205293,plain,
! [X0] :
( ! [X1] :
( ( v231496(X0,X1)
<=> b0010(X1) )
| ~ range_3_0(X1) )
| ~ v231497(X0) ),
inference(ennf_transformation,[],[f64]) ).
fof(f205294,plain,
! [X0] :
( ! [X1] :
( ( v231496(X0,X1)
<=> v231499(X0,X1) )
| ~ range_3_0(X1) )
| v231497(X0) ),
inference(ennf_transformation,[],[f63]) ).
fof(f205309,plain,
! [X0] :
( ! [X1] :
( ( v231499(X0,X1)
<=> v231500(X0,X1) )
| ~ range_3_0(X1) )
| ~ v2311(X0) ),
inference(ennf_transformation,[],[f66]) ).
fof(f205310,plain,
! [X0] :
( ! [X1] :
( ( v231499(X0,X1)
<=> v231502(X0,X1) )
| ~ range_3_0(X1) )
| v2311(X0) ),
inference(ennf_transformation,[],[f65]) ).
fof(f205356,plain,
! [X0,X1] :
( ~ v231500(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f204722]) ).
fof(f205357,plain,
! [X0,X1] :
( ~ v231502(X0,X1)
| ~ range_1_0(X1) ),
inference(ennf_transformation,[],[f204724]) ).
fof(f205612,plain,
! [X0] :
( range_1_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0 ) ),
inference(ennf_transformation,[],[f205098]) ).
fof(f205613,plain,
! [X0] :
( range_3_0(X0)
| ( bitIndex0 != X0
& bitIndex1 != X0
& bitIndex2 != X0
& bitIndex3 != X0 ) ),
inference(ennf_transformation,[],[f205099]) ).
fof(f206109,plain,
~ v4(sK115),
inference(skolemize,[status(esa),new_symbols(skolem,[sK115]),skolemize(X0,sK115)],[f205252]) ).
fof(f206110,plain,
! [X0,X1] :
( ( ( v231511(X0,X1)
| ~ v6(X0,X1) )
& ( v6(X0,X1)
| ~ v231511(X0,X1) ) )
| ~ range_3_0(X1) ),
inference(nnf_transformation,[],[f205263]) ).
fof(f206111,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ b0001(X1) )
& ( b0001(X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v231494(X0) ),
inference(nnf_transformation,[],[f205281]) ).
fof(f206112,plain,
! [X0] :
( ! [X1] :
( ( ( v6(X0,X1)
| ~ v231496(X0,X1) )
& ( v231496(X0,X1)
| ~ v6(X0,X1) ) )
| ~ range_3_0(X1) )
| v231494(X0) ),
inference(nnf_transformation,[],[f205282]) ).
fof(f206119,plain,
! [X0] :
( ! [X1] :
( ( ( v231496(X0,X1)
| ~ b0010(X1) )
& ( b0010(X1)
| ~ v231496(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v231497(X0) ),
inference(nnf_transformation,[],[f205293]) ).
fof(f206120,plain,
! [X0] :
( ! [X1] :
( ( ( v231496(X0,X1)
| ~ v231499(X0,X1) )
& ( v231499(X0,X1)
| ~ v231496(X0,X1) ) )
| ~ range_3_0(X1) )
| v231497(X0) ),
inference(nnf_transformation,[],[f205294]) ).
fof(f206155,plain,
! [X0] :
( ! [X1] :
( ( ( v231499(X0,X1)
| ~ v231500(X0,X1) )
& ( v231500(X0,X1)
| ~ v231499(X0,X1) ) )
| ~ range_3_0(X1) )
| ~ v2311(X0) ),
inference(nnf_transformation,[],[f205309]) ).
fof(f206156,plain,
! [X0] :
( ! [X1] :
( ( ( v231499(X0,X1)
| ~ v231502(X0,X1) )
& ( v231502(X0,X1)
| ~ v231499(X0,X1) ) )
| ~ range_3_0(X1) )
| v2311(X0) ),
inference(nnf_transformation,[],[f205310]) ).
fof(f206247,plain,
! [X0] :
( ( v231500(X0,bitIndex3)
| ~ v126476(X0,bitIndex1) )
& ( v126476(X0,bitIndex1)
| ~ v231500(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f73]) ).
fof(f206248,plain,
! [X0] :
( ( v231500(X0,bitIndex2)
| ~ v231501(X0) )
& ( v231501(X0)
| ~ v231500(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f72]) ).
fof(f206249,plain,
! [X0] :
( ( v231502(X0,bitIndex3)
| ~ v126476(X0,bitIndex0) )
& ( v126476(X0,bitIndex0)
| ~ v231502(X0,bitIndex3) ) ),
inference(nnf_transformation,[],[f69]) ).
fof(f206250,plain,
! [X0] :
( ( v231502(X0,bitIndex2)
| ~ v231503(X0) )
& ( v231503(X0)
| ~ v231502(X0,bitIndex2) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f206448,plain,
! [X0] :
( ( ~ v231501(X0)
| ~ v126476(X0,bitIndex1) )
& ( v126476(X0,bitIndex1)
| v231501(X0) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f206449,plain,
! [X0] :
( ( ~ v231503(X0)
| ~ v126476(X0,bitIndex0) )
& ( v126476(X0,bitIndex0)
| v231503(X0) ) ),
inference(nnf_transformation,[],[f70]) ).
fof(f209171,plain,
~ v4(sK115),
inference(cnf_transformation,[],[f206109]) ).
fof(f209172,plain,
! [X0] :
( v231505(X0)
| v4(X0) ),
inference(cnf_transformation,[],[f205253]) ).
fof(f209173,plain,
! [X0] :
( ~ v231505(X0)
| ~ v231506(X0) ),
inference(cnf_transformation,[],[f205254]) ).
fof(f209174,plain,
! [X0] :
( v231506(X0)
| ~ v231508(X0)
| ~ v231526(X0) ),
inference(cnf_transformation,[],[f205256]) ).
fof(f209175,plain,
! [X0] :
( v231508(X0)
| ~ v231517(X0) ),
inference(cnf_transformation,[],[f205257]) ).
fof(f209176,plain,
! [X0] :
( v231508(X0)
| ~ v231509(X0) ),
inference(cnf_transformation,[],[f205257]) ).
fof(f209177,plain,
! [X0] :
( v231526(X0)
| ~ v231511(X0,bitIndex3) ),
inference(cnf_transformation,[],[f205258]) ).
fof(f209178,plain,
! [X0] :
( v231526(X0)
| ~ v231527(X0) ),
inference(cnf_transformation,[],[f205258]) ).
fof(f209179,plain,
! [X0] :
( v231509(X0)
| ~ v231510(X0)
| ~ v231512(X0) ),
inference(cnf_transformation,[],[f205260]) ).
fof(f209180,plain,
! [X0] :
( v231517(X0)
| ~ v231519(X0) ),
inference(cnf_transformation,[],[f205261]) ).
fof(f209181,plain,
! [X0] :
( v231517(X0)
| ~ v231518(X0) ),
inference(cnf_transformation,[],[f205261]) ).
fof(f209182,plain,
! [X0] :
( v231527(X0)
| ~ v231511(X0,bitIndex2) ),
inference(cnf_transformation,[],[f205262]) ).
fof(f209183,plain,
! [X0] :
( v231527(X0)
| ~ v231528(X0) ),
inference(cnf_transformation,[],[f205262]) ).
fof(f209184,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v231511(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f206110]) ).
fof(f209185,plain,
! [X0,X1] :
( v231511(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1) ),
inference(cnf_transformation,[],[f206110]) ).
fof(f209186,plain,
! [X0] :
( v231511(X0,bitIndex3)
| v231510(X0) ),
inference(cnf_transformation,[],[f205264]) ).
fof(f209187,plain,
! [X0] :
( v231511(X0,bitIndex2)
| v231513(X0) ),
inference(cnf_transformation,[],[f205265]) ).
fof(f209188,plain,
! [X0] :
( v231511(X0,bitIndex0)
| v231515(X0) ),
inference(cnf_transformation,[],[f205266]) ).
fof(f209189,plain,
! [X0] :
( v231511(X0,bitIndex1)
| v231516(X0) ),
inference(cnf_transformation,[],[f205267]) ).
fof(f209190,plain,
! [X0] :
( v231518(X0)
| ~ v231511(X0,bitIndex3)
| ~ v231512(X0) ),
inference(cnf_transformation,[],[f205269]) ).
fof(f209191,plain,
! [X0] :
( v231521(X0)
| ~ v231511(X0,bitIndex2)
| ~ v231514(X0) ),
inference(cnf_transformation,[],[f205271]) ).
fof(f209192,plain,
! [X0] :
( v231524(X0)
| ~ v231515(X0)
| ~ v231511(X0,bitIndex1) ),
inference(cnf_transformation,[],[f205273]) ).
fof(f209193,plain,
! [X0] :
( v231525(X0)
| ~ v231511(X0,bitIndex0)
| ~ v231516(X0) ),
inference(cnf_transformation,[],[f205275]) ).
fof(f209194,plain,
! [X0] :
( v231528(X0)
| ~ v231511(X0,bitIndex1) ),
inference(cnf_transformation,[],[f205276]) ).
fof(f209195,plain,
! [X0] :
( v231528(X0)
| ~ v231511(X0,bitIndex0) ),
inference(cnf_transformation,[],[f205276]) ).
fof(f209196,plain,
! [X0] :
( v231519(X0)
| ~ v231510(X0)
| ~ v231520(X0) ),
inference(cnf_transformation,[],[f205278]) ).
fof(f209197,plain,
! [X0] :
( v231512(X0)
| ~ v231513(X0)
| ~ v231514(X0) ),
inference(cnf_transformation,[],[f205280]) ).
fof(f209198,plain,
! [X0,X1] :
( b0001(X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| ~ v231494(X0) ),
inference(cnf_transformation,[],[f206111]) ).
fof(f209199,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ b0001(X1)
| ~ range_3_0(X1)
| ~ v231494(X0) ),
inference(cnf_transformation,[],[f206111]) ).
fof(f209200,plain,
! [X0,X1] :
( v231496(X0,X1)
| ~ v6(X0,X1)
| ~ range_3_0(X1)
| v231494(X0) ),
inference(cnf_transformation,[],[f206112]) ).
fof(f209201,plain,
! [X0,X1] :
( v6(X0,X1)
| ~ v231496(X0,X1)
| ~ range_3_0(X1)
| v231494(X0) ),
inference(cnf_transformation,[],[f206112]) ).
fof(f209202,plain,
! [X0] :
( v231522(X0)
| ~ v231513(X0)
| ~ v231523(X0) ),
inference(cnf_transformation,[],[f205284]) ).
fof(f209203,plain,
! [X0] :
( v231514(X0)
| ~ v231515(X0)
| ~ v231516(X0) ),
inference(cnf_transformation,[],[f205286]) ).
fof(f209204,plain,
! [X0] :
( v231520(X0)
| ~ v231522(X0) ),
inference(cnf_transformation,[],[f205287]) ).
fof(f209205,plain,
! [X0] :
( v231520(X0)
| ~ v231521(X0) ),
inference(cnf_transformation,[],[f205287]) ).
fof(f209206,plain,
! [X0] :
( v231523(X0)
| ~ v231525(X0) ),
inference(cnf_transformation,[],[f205288]) ).
fof(f209207,plain,
! [X0] :
( v231523(X0)
| ~ v231524(X0) ),
inference(cnf_transformation,[],[f205288]) ).
fof(f209211,plain,
b0001(bitIndex0),
inference(cnf_transformation,[],[f197683]) ).
fof(f209212,plain,
~ b0001(bitIndex1),
inference(cnf_transformation,[],[f197682]) ).
fof(f209213,plain,
~ b0001(bitIndex2),
inference(cnf_transformation,[],[f197681]) ).
fof(f209214,plain,
~ b0001(bitIndex3),
inference(cnf_transformation,[],[f197680]) ).
fof(f209227,plain,
! [X0,X1] :
( b0010(X1)
| ~ v231496(X0,X1)
| ~ range_3_0(X1)
| ~ v231497(X0) ),
inference(cnf_transformation,[],[f206119]) ).
fof(f209228,plain,
! [X0,X1] :
( v231496(X0,X1)
| ~ b0010(X1)
| ~ range_3_0(X1)
| ~ v231497(X0) ),
inference(cnf_transformation,[],[f206119]) ).
fof(f209229,plain,
! [X0,X1] :
( v231499(X0,X1)
| ~ v231496(X0,X1)
| ~ range_3_0(X1)
| v231497(X0) ),
inference(cnf_transformation,[],[f206120]) ).
fof(f209230,plain,
! [X0,X1] :
( v231496(X0,X1)
| ~ v231499(X0,X1)
| ~ range_3_0(X1)
| v231497(X0) ),
inference(cnf_transformation,[],[f206120]) ).
fof(f209295,plain,
~ b0010(bitIndex0),
inference(cnf_transformation,[],[f119396]) ).
fof(f209296,plain,
b0010(bitIndex1),
inference(cnf_transformation,[],[f119395]) ).
fof(f209297,plain,
~ b0010(bitIndex2),
inference(cnf_transformation,[],[f119394]) ).
fof(f209298,plain,
~ b0010(bitIndex3),
inference(cnf_transformation,[],[f119393]) ).
fof(f209303,plain,
! [X0,X1] :
( v231500(X0,X1)
| ~ v231499(X0,X1)
| ~ range_3_0(X1)
| ~ v2311(X0) ),
inference(cnf_transformation,[],[f206155]) ).
fof(f209304,plain,
! [X0,X1] :
( v231499(X0,X1)
| ~ v231500(X0,X1)
| ~ range_3_0(X1)
| ~ v2311(X0) ),
inference(cnf_transformation,[],[f206155]) ).
fof(f209305,plain,
! [X0,X1] :
( v231502(X0,X1)
| ~ v231499(X0,X1)
| ~ range_3_0(X1)
| v2311(X0) ),
inference(cnf_transformation,[],[f206156]) ).
fof(f209306,plain,
! [X0,X1] :
( v231499(X0,X1)
| ~ v231502(X0,X1)
| ~ range_3_0(X1)
| v2311(X0) ),
inference(cnf_transformation,[],[f206156]) ).
fof(f209480,plain,
! [X0] :
( v126476(X0,bitIndex1)
| ~ v231500(X0,bitIndex3) ),
inference(cnf_transformation,[],[f206247]) ).
fof(f209481,plain,
! [X0] :
( v231500(X0,bitIndex3)
| ~ v126476(X0,bitIndex1) ),
inference(cnf_transformation,[],[f206247]) ).
fof(f209482,plain,
! [X0] :
( v231501(X0)
| ~ v231500(X0,bitIndex2) ),
inference(cnf_transformation,[],[f206248]) ).
fof(f209483,plain,
! [X0] :
( v231500(X0,bitIndex2)
| ~ v231501(X0) ),
inference(cnf_transformation,[],[f206248]) ).
fof(f209484,plain,
! [X0,X1] :
( ~ v231500(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f205356]) ).
fof(f209485,plain,
! [X0] :
( v126476(X0,bitIndex0)
| ~ v231502(X0,bitIndex3) ),
inference(cnf_transformation,[],[f206249]) ).
fof(f209486,plain,
! [X0] :
( v231502(X0,bitIndex3)
| ~ v126476(X0,bitIndex0) ),
inference(cnf_transformation,[],[f206249]) ).
fof(f209487,plain,
! [X0] :
( v231503(X0)
| ~ v231502(X0,bitIndex2) ),
inference(cnf_transformation,[],[f206250]) ).
fof(f209488,plain,
! [X0] :
( v231502(X0,bitIndex2)
| ~ v231503(X0) ),
inference(cnf_transformation,[],[f206250]) ).
fof(f209489,plain,
! [X0,X1] :
( ~ v231502(X0,X1)
| ~ range_1_0(X1) ),
inference(cnf_transformation,[],[f205357]) ).
fof(f209834,plain,
! [X0] :
( v126476(X0,bitIndex1)
| v231501(X0) ),
inference(cnf_transformation,[],[f206448]) ).
fof(f209835,plain,
! [X0] :
( ~ v231501(X0)
| ~ v126476(X0,bitIndex1) ),
inference(cnf_transformation,[],[f206448]) ).
fof(f209836,plain,
! [X0] :
( v126476(X0,bitIndex0)
| v231503(X0) ),
inference(cnf_transformation,[],[f206449]) ).
fof(f209837,plain,
! [X0] :
( ~ v231503(X0)
| ~ v126476(X0,bitIndex0) ),
inference(cnf_transformation,[],[f206449]) ).
fof(f211901,plain,
! [X0] :
( range_1_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f205612]) ).
fof(f211902,plain,
! [X0] :
( range_1_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f205612]) ).
fof(f211903,plain,
! [X0] :
( range_3_0(X0)
| bitIndex3 != X0 ),
inference(cnf_transformation,[],[f205613]) ).
fof(f211904,plain,
! [X0] :
( range_3_0(X0)
| bitIndex2 != X0 ),
inference(cnf_transformation,[],[f205613]) ).
fof(f211905,plain,
! [X0] :
( range_3_0(X0)
| bitIndex1 != X0 ),
inference(cnf_transformation,[],[f205613]) ).
fof(f211906,plain,
! [X0] :
( range_3_0(X0)
| bitIndex0 != X0 ),
inference(cnf_transformation,[],[f205613]) ).
fof(f215463,plain,
range_1_0(bitIndex0),
inference(equality_resolution,[],[f211902]) ).
fof(f215464,plain,
range_1_0(bitIndex1),
inference(equality_resolution,[],[f211901]) ).
fof(f215465,plain,
range_3_0(bitIndex0),
inference(equality_resolution,[],[f211906]) ).
fof(f215466,plain,
range_3_0(bitIndex1),
inference(equality_resolution,[],[f211905]) ).
fof(f215467,plain,
range_3_0(bitIndex2),
inference(equality_resolution,[],[f211904]) ).
fof(f215468,plain,
range_3_0(bitIndex3),
inference(equality_resolution,[],[f211903]) ).
fof(f215536,plain,
v231505(sK115),
inference(resolution,[],[f209171,f209172]) ).
fof(f215537,plain,
~ v231506(sK115),
inference(resolution,[],[f215536,f209173]) ).
fof(f215538,plain,
( ~ v231508(sK115)
| ~ v231526(sK115) ),
inference(resolution,[],[f215537,f209174]) ).
fof(f215540,definition,
( spl116_1
<=> v231526(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_1])],[avatar_definition]) ).
fof(f215542,plain,
( ~ v231526(sK115)
| spl116_1 ),
inference(avatar_component_clause,[],[f215540]) ).
fof(f215544,definition,
( spl116_2
<=> v231508(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_2])],[avatar_definition]) ).
fof(f215546,plain,
( ~ v231508(sK115)
| spl116_2 ),
inference(avatar_component_clause,[],[f215544]) ).
fof(f215547,plain,
( ~ spl116_1
| ~ spl116_2 ),
inference(avatar_split_clause,[],[f215538,f215544,f215540]) ).
fof(f215548,plain,
( ~ v231511(sK115,bitIndex3)
| spl116_1 ),
inference(resolution,[],[f215542,f209177]) ).
fof(f215549,plain,
( ~ v231527(sK115)
| spl116_1 ),
inference(resolution,[],[f215542,f209178]) ).
fof(f215551,plain,
( ~ v231528(sK115)
| spl116_1 ),
inference(resolution,[],[f215549,f209183]) ).
fof(f215553,plain,
( ~ v6(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl116_1 ),
inference(resolution,[],[f215548,f209185]) ).
fof(f215554,plain,
( ~ v6(sK115,bitIndex3)
| spl116_1 ),
inference(forward_subsumption_resolution,[],[f215553,f215468]) ).
fof(f215560,definition,
( spl116_3
<=> v231512(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_3])],[avatar_definition]) ).
fof(f215561,plain,
( v231512(sK115)
| ~ spl116_3 ),
inference(avatar_component_clause,[],[f215560]) ).
fof(f215562,plain,
( ~ v231512(sK115)
| spl116_3 ),
inference(avatar_component_clause,[],[f215560]) ).
fof(f215564,definition,
( spl116_4
<=> v231509(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_4])],[avatar_definition]) ).
fof(f215565,plain,
( ~ v231509(sK115)
| spl116_4 ),
inference(avatar_component_clause,[],[f215564]) ).
fof(f215569,definition,
( spl116_5
<=> v231520(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_5])],[avatar_definition]) ).
fof(f215570,plain,
( v231520(sK115)
| ~ spl116_5 ),
inference(avatar_component_clause,[],[f215569]) ).
fof(f215571,plain,
( ~ v231520(sK115)
| spl116_5 ),
inference(avatar_component_clause,[],[f215569]) ).
fof(f215573,definition,
( spl116_6
<=> v231519(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_6])],[avatar_definition]) ).
fof(f215574,plain,
( ~ v231519(sK115)
| spl116_6 ),
inference(avatar_component_clause,[],[f215573]) ).
fof(f215577,plain,
( ~ v231513(sK115)
| ~ v231514(sK115)
| spl116_3 ),
inference(resolution,[],[f215562,f209197]) ).
fof(f215579,definition,
( spl116_7
<=> v231514(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_7])],[avatar_definition]) ).
fof(f215580,plain,
( v231514(sK115)
| ~ spl116_7 ),
inference(avatar_component_clause,[],[f215579]) ).
fof(f215581,plain,
( ~ v231514(sK115)
| spl116_7 ),
inference(avatar_component_clause,[],[f215579]) ).
fof(f215583,definition,
( spl116_8
<=> v231513(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_8])],[avatar_definition]) ).
fof(f215584,plain,
( v231513(sK115)
| ~ spl116_8 ),
inference(avatar_component_clause,[],[f215583]) ).
fof(f215585,plain,
( ~ v231513(sK115)
| spl116_8 ),
inference(avatar_component_clause,[],[f215583]) ).
fof(f215586,plain,
( ~ spl116_7
| ~ spl116_8
| spl116_3 ),
inference(avatar_split_clause,[],[f215577,f215560,f215583,f215579]) ).
fof(f215591,plain,
( ~ v231522(sK115)
| spl116_5 ),
inference(resolution,[],[f215571,f209204]) ).
fof(f215592,plain,
( ~ v231521(sK115)
| spl116_5 ),
inference(resolution,[],[f215571,f209205]) ).
fof(f215593,plain,
( ~ v231496(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v231494(sK115)
| spl116_1 ),
inference(resolution,[],[f215554,f209201]) ).
fof(f215596,plain,
( ~ v231496(sK115,bitIndex3)
| v231494(sK115)
| spl116_1 ),
inference(forward_subsumption_resolution,[],[f215593,f215468]) ).
fof(f215598,definition,
( spl116_9
<=> v231494(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_9])],[avatar_definition]) ).
fof(f215599,plain,
( ~ v231494(sK115)
| spl116_9 ),
inference(avatar_component_clause,[],[f215598]) ).
fof(f215600,plain,
( v231494(sK115)
| ~ spl116_9 ),
inference(avatar_component_clause,[],[f215598]) ).
fof(f215602,definition,
( spl116_10
<=> v231496(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_10])],[avatar_definition]) ).
fof(f215603,plain,
( v231496(sK115,bitIndex3)
| ~ spl116_10 ),
inference(avatar_component_clause,[],[f215602]) ).
fof(f215604,plain,
( ~ v231496(sK115,bitIndex3)
| spl116_10 ),
inference(avatar_component_clause,[],[f215602]) ).
fof(f215605,plain,
( spl116_9
| ~ spl116_10
| spl116_1 ),
inference(avatar_split_clause,[],[f215596,f215540,f215602,f215598]) ).
fof(f215606,plain,
( ~ v231515(sK115)
| ~ v231516(sK115)
| spl116_7 ),
inference(resolution,[],[f215581,f209203]) ).
fof(f215608,definition,
( spl116_11
<=> v231516(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_11])],[avatar_definition]) ).
fof(f215609,plain,
( v231516(sK115)
| ~ spl116_11 ),
inference(avatar_component_clause,[],[f215608]) ).
fof(f215610,plain,
( ~ v231516(sK115)
| spl116_11 ),
inference(avatar_component_clause,[],[f215608]) ).
fof(f215612,definition,
( spl116_12
<=> v231515(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_12])],[avatar_definition]) ).
fof(f215613,plain,
( v231515(sK115)
| ~ spl116_12 ),
inference(avatar_component_clause,[],[f215612]) ).
fof(f215614,plain,
( ~ v231515(sK115)
| spl116_12 ),
inference(avatar_component_clause,[],[f215612]) ).
fof(f215615,plain,
( ~ spl116_11
| ~ spl116_12
| spl116_7 ),
inference(avatar_split_clause,[],[f215606,f215579,f215612,f215608]) ).
fof(f215622,plain,
( ~ v231517(sK115)
| spl116_2 ),
inference(resolution,[],[f215546,f209175]) ).
fof(f215623,plain,
( ~ v231509(sK115)
| spl116_2 ),
inference(resolution,[],[f215546,f209176]) ).
fof(f215624,plain,
( ~ spl116_4
| spl116_2 ),
inference(avatar_split_clause,[],[f215623,f215544,f215564]) ).
fof(f215625,plain,
( ~ v231519(sK115)
| spl116_2 ),
inference(resolution,[],[f215622,f209180]) ).
fof(f215626,plain,
( ~ v231518(sK115)
| spl116_2 ),
inference(resolution,[],[f215622,f209181]) ).
fof(f215627,plain,
( ~ spl116_6
| spl116_2 ),
inference(avatar_split_clause,[],[f215625,f215544,f215573]) ).
fof(f215629,plain,
( ~ v231510(sK115)
| ~ v231512(sK115)
| spl116_4 ),
inference(resolution,[],[f215565,f209179]) ).
fof(f215631,plain,
( v231522(sK115)
| ~ v231523(sK115)
| ~ spl116_8 ),
inference(resolution,[],[f215584,f209202]) ).
fof(f215633,plain,
( ~ v231523(sK115)
| spl116_5
| ~ spl116_8 ),
inference(forward_subsumption_resolution,[],[f215631,f215591]) ).
fof(f215634,plain,
( ~ v231499(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v231497(sK115)
| spl116_10 ),
inference(resolution,[],[f215604,f209230]) ).
fof(f215636,plain,
( ~ v6(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v231494(sK115)
| spl116_10 ),
inference(resolution,[],[f215604,f209200]) ).
fof(f215637,plain,
( ~ v6(sK115,bitIndex3)
| v231494(sK115)
| spl116_10 ),
inference(forward_subsumption_resolution,[],[f215636,f215468]) ).
fof(f215638,plain,
( ~ v231499(sK115,bitIndex3)
| v231497(sK115)
| spl116_10 ),
inference(forward_subsumption_resolution,[],[f215634,f215468]) ).
fof(f215640,definition,
( spl116_13
<=> v6(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_13])],[avatar_definition]) ).
fof(f215642,plain,
( ~ v6(sK115,bitIndex3)
| spl116_13 ),
inference(avatar_component_clause,[],[f215640]) ).
fof(f215643,plain,
( spl116_9
| ~ spl116_13
| spl116_10 ),
inference(avatar_split_clause,[],[f215637,f215602,f215640,f215598]) ).
fof(f215645,definition,
( spl116_14
<=> v231497(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_14])],[avatar_definition]) ).
fof(f215646,plain,
( ~ v231497(sK115)
| spl116_14 ),
inference(avatar_component_clause,[],[f215645]) ).
fof(f215647,plain,
( v231497(sK115)
| ~ spl116_14 ),
inference(avatar_component_clause,[],[f215645]) ).
fof(f215649,definition,
( spl116_15
<=> v231499(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_15])],[avatar_definition]) ).
fof(f215650,plain,
( v231499(sK115,bitIndex3)
| ~ spl116_15 ),
inference(avatar_component_clause,[],[f215649]) ).
fof(f215651,plain,
( ~ v231499(sK115,bitIndex3)
| spl116_15 ),
inference(avatar_component_clause,[],[f215649]) ).
fof(f215652,plain,
( spl116_14
| ~ spl116_15
| spl116_10 ),
inference(avatar_split_clause,[],[f215638,f215602,f215649,f215645]) ).
fof(f215658,plain,
( ~ v231511(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| spl116_13 ),
inference(resolution,[],[f215642,f209184]) ).
fof(f215659,plain,
( ~ v231511(sK115,bitIndex3)
| spl116_13 ),
inference(forward_subsumption_resolution,[],[f215658,f215468]) ).
fof(f215661,plain,
( ~ v231524(sK115)
| spl116_5
| ~ spl116_8 ),
inference(resolution,[],[f215633,f209207]) ).
fof(f215662,plain,
( ~ v231502(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v2311(sK115)
| spl116_15 ),
inference(resolution,[],[f215651,f209306]) ).
fof(f215663,plain,
( ~ v231500(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v2311(sK115)
| spl116_15 ),
inference(resolution,[],[f215651,f209304]) ).
fof(f215665,plain,
( ~ v231500(sK115,bitIndex3)
| ~ v2311(sK115)
| spl116_15 ),
inference(forward_subsumption_resolution,[],[f215663,f215468]) ).
fof(f215666,plain,
( ~ v231502(sK115,bitIndex3)
| v2311(sK115)
| spl116_15 ),
inference(forward_subsumption_resolution,[],[f215662,f215468]) ).
fof(f215668,definition,
( spl116_16
<=> v2311(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_16])],[avatar_definition]) ).
fof(f215669,plain,
( v2311(sK115)
| ~ spl116_16 ),
inference(avatar_component_clause,[],[f215668]) ).
fof(f215670,plain,
( ~ v2311(sK115)
| spl116_16 ),
inference(avatar_component_clause,[],[f215668]) ).
fof(f215672,definition,
( spl116_17
<=> v231500(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_17])],[avatar_definition]) ).
fof(f215673,plain,
( v231500(sK115,bitIndex3)
| ~ spl116_17 ),
inference(avatar_component_clause,[],[f215672]) ).
fof(f215674,plain,
( ~ v231500(sK115,bitIndex3)
| spl116_17 ),
inference(avatar_component_clause,[],[f215672]) ).
fof(f215675,plain,
( ~ spl116_16
| ~ spl116_17
| spl116_15 ),
inference(avatar_split_clause,[],[f215665,f215649,f215672,f215668]) ).
fof(f215677,definition,
( spl116_18
<=> v231502(sK115,bitIndex3) ),
introduced(definition,[new_symbols(definition,[spl116_18])],[avatar_definition]) ).
fof(f215678,plain,
( v231502(sK115,bitIndex3)
| ~ spl116_18 ),
inference(avatar_component_clause,[],[f215677]) ).
fof(f215679,plain,
( ~ v231502(sK115,bitIndex3)
| spl116_18 ),
inference(avatar_component_clause,[],[f215677]) ).
fof(f215680,plain,
( spl116_16
| ~ spl116_18
| spl116_15 ),
inference(avatar_split_clause,[],[f215666,f215649,f215677,f215668]) ).
fof(f215723,plain,
( v231510(sK115)
| spl116_13 ),
inference(resolution,[],[f215659,f209186]) ).
fof(f215726,plain,
( ~ v126476(sK115,bitIndex0)
| spl116_18 ),
inference(resolution,[],[f215679,f209486]) ).
fof(f215777,plain,
( v231519(sK115)
| ~ v231520(sK115)
| spl116_13 ),
inference(resolution,[],[f215723,f209196]) ).
fof(f215817,plain,
( v231503(sK115)
| spl116_18 ),
inference(resolution,[],[f215726,f209836]) ).
fof(f215821,definition,
( spl116_31
<=> v126476(sK115,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl116_31])],[avatar_definition]) ).
fof(f215822,plain,
( ~ v126476(sK115,bitIndex1)
| spl116_31 ),
inference(avatar_component_clause,[],[f215821]) ).
fof(f215823,plain,
( v126476(sK115,bitIndex1)
| ~ spl116_31 ),
inference(avatar_component_clause,[],[f215821]) ).
fof(f215852,plain,
( v126476(sK115,bitIndex0)
| ~ spl116_18 ),
inference(resolution,[],[f215678,f209485]) ).
fof(f215868,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| v231499(sK115,X0)
| ~ range_3_0(X0) )
| spl116_14 ),
inference(resolution,[],[f215646,f209229]) ).
fof(f215941,plain,
( ~ v126476(sK115,bitIndex1)
| spl116_17 ),
inference(resolution,[],[f215674,f209481]) ).
fof(f215942,plain,
( ~ v231499(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v2311(sK115)
| spl116_17 ),
inference(resolution,[],[f215674,f209303]) ).
fof(f215943,plain,
( ~ spl116_31
| spl116_17 ),
inference(avatar_split_clause,[],[f215941,f215672,f215821]) ).
fof(f215952,plain,
( ! [X0] :
( v231499(sK115,X0)
| ~ range_3_0(X0)
| ~ v6(sK115,X0)
| ~ range_3_0(X0)
| v231494(sK115) )
| spl116_14 ),
inference(resolution,[],[f215868,f209200]) ).
fof(f215953,plain,
( ! [X0] :
( v231499(sK115,X0)
| ~ range_3_0(X0)
| ~ v6(sK115,X0)
| v231494(sK115) )
| spl116_14 ),
inference(duplicate_literal_removal,[],[f215952]) ).
fof(f215957,definition,
( spl116_45
<=> ! [X0] :
( v231499(sK115,X0)
| ~ v6(sK115,X0)
| ~ range_3_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl116_45])],[avatar_definition]) ).
fof(f215958,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| v231499(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_45 ),
inference(avatar_component_clause,[],[f215957]) ).
fof(f215959,plain,
( spl116_9
| spl116_45
| spl116_14 ),
inference(avatar_split_clause,[],[f215953,f215645,f215957,f215598]) ).
fof(f215962,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215600,f209198]) ).
fof(f215972,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215962,f209184]) ).
fof(f215973,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl116_9 ),
inference(duplicate_literal_removal,[],[f215972]) ).
fof(f216005,plain,
( ~ range_3_0(bitIndex2)
| b0001(bitIndex2)
| v231513(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f215973,f209187]) ).
fof(f216007,plain,
( ~ range_3_0(bitIndex1)
| b0001(bitIndex1)
| v231516(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f215973,f209189]) ).
fof(f216009,plain,
( b0001(bitIndex1)
| v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216007,f215466]) ).
fof(f216011,plain,
( v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216009,f209212]) ).
fof(f216014,plain,
( $false
| ~ spl116_9
| spl116_11 ),
inference(forward_subsumption_resolution,[],[f216011,f215610]) ).
fof(f216015,plain,
( ~ spl116_9
| spl116_11 ),
inference(avatar_contradiction_clause,[],[f216014]) ).
fof(f216021,definition,
( spl116_47
<=> v231523(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_47])],[avatar_definition]) ).
fof(f216023,plain,
( ~ v231523(sK115)
| spl116_47 ),
inference(avatar_component_clause,[],[f216021]) ).
fof(f216029,plain,
( ~ v231520(sK115)
| spl116_6
| spl116_13 ),
inference(forward_subsumption_resolution,[],[f215777,f215574]) ).
fof(f216032,plain,
( $false
| ~ spl116_5
| spl116_6
| spl116_13 ),
inference(forward_subsumption_resolution,[],[f216029,f215570]) ).
fof(f216033,plain,
( ~ spl116_5
| spl116_6
| spl116_13 ),
inference(avatar_contradiction_clause,[],[f216032]) ).
fof(f216044,plain,
( b0001(bitIndex2)
| v231513(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216005,f215467]) ).
fof(f216045,plain,
( v231513(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216044,f209213]) ).
fof(f216046,plain,
( $false
| spl116_8
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f216045,f215585]) ).
fof(f216047,plain,
( spl116_8
| ~ spl116_9 ),
inference(avatar_contradiction_clause,[],[f216046]) ).
fof(f216053,plain,
( ~ v231511(sK115,bitIndex3)
| ~ v231512(sK115)
| spl116_2 ),
inference(resolution,[],[f215626,f209190]) ).
fof(f216056,plain,
( ~ v231510(sK115)
| ~ v231520(sK115)
| spl116_6 ),
inference(resolution,[],[f215574,f209196]) ).
fof(f216058,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| v231496(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f215599,f209200]) ).
fof(f216059,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f215599,f209201]) ).
fof(f216061,plain,
( v231511(sK115,bitIndex2)
| spl116_8 ),
inference(resolution,[],[f215585,f209187]) ).
fof(f216072,plain,
( ! [X0] :
( v231496(sK115,X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f216058,f209184]) ).
fof(f216073,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| v231496(sK115,X0) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f216072]) ).
fof(f216078,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| spl116_9 ),
inference(resolution,[],[f216059,f209230]) ).
fof(f216083,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| v231497(sK115) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f216078]) ).
fof(f216085,plain,
( ~ v231525(sK115)
| spl116_47 ),
inference(resolution,[],[f216023,f209206]) ).
fof(f216091,plain,
( v231521(sK115)
| ~ v231514(sK115)
| spl116_8 ),
inference(resolution,[],[f216061,f209191]) ).
fof(f216093,plain,
( v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_8 ),
inference(resolution,[],[f216061,f209184]) ).
fof(f216094,plain,
( v6(sK115,bitIndex2)
| spl116_8 ),
inference(forward_subsumption_resolution,[],[f216093,f215467]) ).
fof(f216110,plain,
( ~ range_3_0(bitIndex2)
| v231496(sK115,bitIndex2)
| spl116_8
| spl116_9 ),
inference(resolution,[],[f216073,f216061]) ).
fof(f216114,plain,
( ~ range_3_0(bitIndex0)
| v231496(sK115,bitIndex0)
| v231515(sK115)
| spl116_9 ),
inference(resolution,[],[f216073,f209188]) ).
fof(f216115,plain,
( ~ range_3_0(bitIndex1)
| v231496(sK115,bitIndex1)
| v231516(sK115)
| spl116_9 ),
inference(resolution,[],[f216073,f209189]) ).
fof(f216117,plain,
( v231496(sK115,bitIndex0)
| v231515(sK115)
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216114,f215465]) ).
fof(f216119,plain,
( v231496(sK115,bitIndex2)
| spl116_8
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216110,f215467]) ).
fof(f216120,plain,
( v231496(sK115,bitIndex0)
| spl116_9
| spl116_12 ),
inference(forward_subsumption_resolution,[],[f216117,f215614]) ).
fof(f216145,plain,
( ~ v231503(sK115)
| ~ spl116_18 ),
inference(resolution,[],[f215852,f209837]) ).
fof(f216207,plain,
( b0010(bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v231497(sK115)
| spl116_8
| spl116_9 ),
inference(resolution,[],[f216119,f209227]) ).
fof(f216214,plain,
( v231499(sK115,bitIndex0)
| ~ range_3_0(bitIndex0)
| spl116_9
| spl116_12
| spl116_14 ),
inference(resolution,[],[f216120,f215868]) ).
fof(f216216,plain,
( b0010(bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v231497(sK115)
| spl116_9
| spl116_12 ),
inference(resolution,[],[f216120,f209227]) ).
fof(f216219,plain,
( v231499(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f216214,f215465]) ).
fof(f216371,plain,
( v231499(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_8
| ~ spl116_45 ),
inference(resolution,[],[f215958,f216094]) ).
fof(f216374,plain,
( ! [X0] :
( v231499(sK115,X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_45 ),
inference(resolution,[],[f215958,f209184]) ).
fof(f216375,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| v231499(sK115,X0) )
| ~ spl116_45 ),
inference(duplicate_literal_removal,[],[f216374]) ).
fof(f216379,plain,
( ~ v231502(sK115,bitIndex2)
| ~ spl116_18 ),
inference(resolution,[],[f216145,f209487]) ).
fof(f216452,plain,
( ~ v231500(sK115,bitIndex3)
| spl116_31 ),
inference(resolution,[],[f215822,f209480]) ).
fof(f216458,plain,
( v231501(sK115)
| spl116_31 ),
inference(resolution,[],[f215822,f209834]) ).
fof(f216564,plain,
( v231500(sK115,bitIndex0)
| ~ range_3_0(bitIndex0)
| ~ v2311(sK115)
| spl116_9
| spl116_12
| spl116_14 ),
inference(resolution,[],[f216219,f209303]) ).
fof(f216566,plain,
( v231500(sK115,bitIndex0)
| ~ v2311(sK115)
| spl116_9
| spl116_12
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f216564,f215465]) ).
fof(f217269,plain,
( ~ range_3_0(bitIndex1)
| v231499(sK115,bitIndex1)
| v231516(sK115)
| ~ spl116_45 ),
inference(resolution,[],[f216375,f209189]) ).
fof(f217569,plain,
( v231500(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f216566,f215669]) ).
fof(f218157,plain,
( ~ range_1_0(bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f217569,f209484]) ).
fof(f218159,plain,
( $false
| spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f218157,f215463]) ).
fof(f218160,plain,
( spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(avatar_contradiction_clause,[],[f218159]) ).
fof(f218174,plain,
( ~ range_3_0(bitIndex2)
| ~ v231497(sK115)
| spl116_8
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216207,f209297]) ).
fof(f218175,plain,
( ~ range_3_0(bitIndex0)
| ~ v231497(sK115)
| spl116_9
| spl116_12 ),
inference(forward_subsumption_resolution,[],[f216216,f209295]) ).
fof(f218177,plain,
( v231499(sK115,bitIndex2)
| spl116_8
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f216371,f215467]) ).
fof(f218184,plain,
( ~ v231497(sK115)
| spl116_8
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f218174,f215467]) ).
fof(f218185,plain,
( ~ v231497(sK115)
| spl116_9
| spl116_12 ),
inference(forward_subsumption_resolution,[],[f218175,f215465]) ).
fof(f218186,plain,
( $false
| spl116_8
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f218184,f215647]) ).
fof(f218187,plain,
( spl116_8
| spl116_9
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f218186]) ).
fof(f218188,plain,
( $false
| spl116_9
| spl116_12
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f218185,f215647]) ).
fof(f218189,plain,
( spl116_9
| spl116_12
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f218188]) ).
fof(f218252,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v6(sK115,X0) )
| spl116_9
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f216083,f215646]) ).
fof(f218258,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| v231502(sK115,X0)
| ~ range_3_0(X0) )
| spl116_16 ),
inference(resolution,[],[f215670,f209305]) ).
fof(f218292,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231500(sK115,X0)
| ~ range_3_0(X0)
| ~ v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(resolution,[],[f218252,f209304]) ).
fof(f218295,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231500(sK115,X0)
| ~ v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(duplicate_literal_removal,[],[f218292]) ).
fof(f218484,plain,
( ! [X0] :
( v231502(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| spl116_16 ),
inference(resolution,[],[f218258,f209229]) ).
fof(f218485,plain,
( ! [X0] :
( v231502(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| v231497(sK115) )
| spl116_16 ),
inference(duplicate_literal_removal,[],[f218484]) ).
fof(f218488,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231502(sK115,X0) )
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f218485,f215646]) ).
fof(f218687,plain,
( ~ range_3_0(bitIndex0)
| v231502(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(resolution,[],[f218488,f216120]) ).
fof(f218695,plain,
( v231502(sK115,bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f218687,f215465]) ).
fof(f219472,plain,
( ~ range_1_0(bitIndex0)
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(resolution,[],[f218695,f209489]) ).
fof(f219474,plain,
( $false
| spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f219472,f215463]) ).
fof(f219475,plain,
( spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(avatar_contradiction_clause,[],[f219474]) ).
fof(f219481,plain,
( ! [X0] :
( ~ v231500(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f218295,f215669]) ).
fof(f219485,plain,
( v231496(sK115,bitIndex1)
| v231516(sK115)
| spl116_9 ),
inference(forward_subsumption_resolution,[],[f216115,f215466]) ).
fof(f219486,plain,
( v231499(sK115,bitIndex1)
| v231516(sK115)
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f217269,f215466]) ).
fof(f219487,plain,
( v231496(sK115,bitIndex1)
| spl116_9
| spl116_11 ),
inference(forward_subsumption_resolution,[],[f219485,f215610]) ).
fof(f219488,plain,
( v231499(sK115,bitIndex1)
| spl116_11
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f219486,f215610]) ).
fof(f219493,plain,
( v231524(sK115)
| ~ v231511(sK115,bitIndex1)
| ~ spl116_12 ),
inference(resolution,[],[f215613,f209192]) ).
fof(f219495,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| v231500(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_16 ),
inference(resolution,[],[f215669,f209303]) ).
fof(f219637,plain,
( v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v231501(sK115)
| spl116_9
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f219481,f209483]) ).
fof(f219647,plain,
( v231500(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_8
| ~ spl116_16
| ~ spl116_45 ),
inference(resolution,[],[f219495,f218177]) ).
fof(f219650,plain,
( ! [X0] :
( v231500(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| ~ spl116_16 ),
inference(resolution,[],[f219495,f209229]) ).
fof(f219651,plain,
( ! [X0] :
( v231500(sK115,X0)
| ~ range_3_0(X0)
| ~ v231496(sK115,X0)
| v231497(sK115) )
| ~ spl116_16 ),
inference(duplicate_literal_removal,[],[f219650]) ).
fof(f219654,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| ~ range_3_0(X0)
| v231500(sK115,X0) )
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219651,f215646]) ).
fof(f219806,plain,
( ~ range_3_0(bitIndex1)
| v231500(sK115,bitIndex1)
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f219654,f219487]) ).
fof(f219814,plain,
( v231500(sK115,bitIndex1)
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219806,f215466]) ).
fof(f219820,plain,
( v231502(sK115,bitIndex1)
| ~ range_3_0(bitIndex1)
| v2311(sK115)
| spl116_11
| ~ spl116_45 ),
inference(resolution,[],[f219488,f209305]) ).
fof(f219863,plain,
( ~ range_1_0(bitIndex1)
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(resolution,[],[f219814,f209484]) ).
fof(f219865,plain,
( $false
| spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219863,f215464]) ).
fof(f219866,plain,
( spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(avatar_contradiction_clause,[],[f219865]) ).
fof(f219868,definition,
( spl116_363
<=> v231511(sK115,bitIndex1) ),
introduced(definition,[new_symbols(definition,[spl116_363])],[avatar_definition]) ).
fof(f219870,plain,
( ~ v231511(sK115,bitIndex1)
| spl116_363 ),
inference(avatar_component_clause,[],[f219868]) ).
fof(f219872,definition,
( spl116_364
<=> v231524(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_364])],[avatar_definition]) ).
fof(f219875,plain,
( ~ spl116_363
| spl116_364
| ~ spl116_12 ),
inference(avatar_split_clause,[],[f219493,f215612,f219872,f219868]) ).
fof(f219877,plain,
( ~ v231514(sK115)
| spl116_5
| spl116_8 ),
inference(forward_subsumption_resolution,[],[f216091,f215592]) ).
fof(f219880,plain,
( $false
| spl116_5
| ~ spl116_7
| spl116_8 ),
inference(forward_subsumption_resolution,[],[f219877,f215580]) ).
fof(f219881,plain,
( spl116_5
| ~ spl116_7
| spl116_8 ),
inference(avatar_contradiction_clause,[],[f219880]) ).
fof(f219882,plain,
( ~ spl116_47
| spl116_5
| ~ spl116_8 ),
inference(avatar_split_clause,[],[f215633,f215583,f215569,f216021]) ).
fof(f219883,plain,
( ~ spl116_364
| spl116_5
| ~ spl116_8 ),
inference(avatar_split_clause,[],[f215661,f215583,f215569,f219872]) ).
fof(f219885,plain,
( v6(sK115,bitIndex2)
| ~ v231501(sK115)
| spl116_9
| spl116_14
| ~ spl116_16 ),
inference(forward_subsumption_resolution,[],[f219637,f215467]) ).
fof(f219891,plain,
( v6(sK115,bitIndex2)
| spl116_9
| spl116_14
| ~ spl116_16
| spl116_31 ),
inference(forward_subsumption_resolution,[],[f219885,f216458]) ).
fof(f219898,plain,
( ~ v231511(sK115,bitIndex3)
| spl116_2
| ~ spl116_3 ),
inference(forward_subsumption_resolution,[],[f216053,f215561]) ).
fof(f219900,plain,
( ~ v231510(sK115)
| ~ spl116_3
| spl116_4 ),
inference(forward_subsumption_resolution,[],[f215629,f215561]) ).
fof(f219908,plain,
( ~ range_3_0(bitIndex3)
| ~ v2311(sK115)
| ~ spl116_15
| spl116_17 ),
inference(forward_subsumption_resolution,[],[f215942,f215650]) ).
fof(f219909,plain,
( ~ v2311(sK115)
| ~ spl116_15
| spl116_17 ),
inference(forward_subsumption_resolution,[],[f219908,f215468]) ).
fof(f219910,plain,
( $false
| ~ spl116_15
| ~ spl116_16
| spl116_17 ),
inference(forward_subsumption_resolution,[],[f219909,f215669]) ).
fof(f219911,plain,
( ~ spl116_15
| ~ spl116_16
| spl116_17 ),
inference(avatar_contradiction_clause,[],[f219910]) ).
fof(f219912,plain,
( $false
| ~ spl116_17
| spl116_31 ),
inference(forward_subsumption_resolution,[],[f216452,f215673]) ).
fof(f219913,plain,
( ~ spl116_17
| spl116_31 ),
inference(avatar_contradiction_clause,[],[f219912]) ).
fof(f219933,definition,
( spl116_368
<=> v231501(sK115) ),
introduced(definition,[new_symbols(definition,[spl116_368])],[avatar_definition]) ).
fof(f219934,plain,
( v231501(sK115)
| ~ spl116_368 ),
inference(avatar_component_clause,[],[f219933]) ).
fof(f219935,plain,
( ~ v231501(sK115)
| spl116_368 ),
inference(avatar_component_clause,[],[f219933]) ).
fof(f219937,definition,
( spl116_369
<=> v6(sK115,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl116_369])],[avatar_definition]) ).
fof(f219938,plain,
( ~ v6(sK115,bitIndex2)
| spl116_369 ),
inference(avatar_component_clause,[],[f219937]) ).
fof(f219939,plain,
( v6(sK115,bitIndex2)
| ~ spl116_369 ),
inference(avatar_component_clause,[],[f219937]) ).
fof(f219947,definition,
( spl116_371
<=> v231499(sK115,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl116_371])],[avatar_definition]) ).
fof(f219949,plain,
( v231499(sK115,bitIndex2)
| ~ spl116_371 ),
inference(avatar_component_clause,[],[f219947]) ).
fof(f219961,plain,
( v231510(sK115)
| spl116_2
| ~ spl116_3 ),
inference(resolution,[],[f219898,f209186]) ).
fof(f219964,plain,
( $false
| spl116_2
| ~ spl116_3
| spl116_4 ),
inference(forward_subsumption_resolution,[],[f219961,f219900]) ).
fof(f219965,plain,
( spl116_2
| ~ spl116_3
| spl116_4 ),
inference(avatar_contradiction_clause,[],[f219964]) ).
fof(f219970,plain,
( spl116_371
| spl116_8
| ~ spl116_45 ),
inference(avatar_split_clause,[],[f218177,f215957,f215583,f219947]) ).
fof(f219971,plain,
( v231500(sK115,bitIndex2)
| spl116_8
| ~ spl116_16
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f219647,f215467]) ).
fof(f219975,plain,
( ~ v231510(sK115)
| ~ spl116_5
| spl116_6 ),
inference(forward_subsumption_resolution,[],[f216056,f215570]) ).
fof(f219977,definition,
( spl116_372
<=> v231511(sK115,bitIndex2) ),
introduced(definition,[new_symbols(definition,[spl116_372])],[avatar_definition]) ).
fof(f219978,plain,
( v231511(sK115,bitIndex2)
| ~ spl116_372 ),
inference(avatar_component_clause,[],[f219977]) ).
fof(f219979,plain,
( ~ v231511(sK115,bitIndex2)
| spl116_372 ),
inference(avatar_component_clause,[],[f219977]) ).
fof(f219994,plain,
( v231511(sK115,bitIndex3)
| ~ spl116_5
| spl116_6 ),
inference(resolution,[],[f219975,f209186]) ).
fof(f220022,plain,
( v231527(sK115)
| ~ spl116_372 ),
inference(resolution,[],[f219978,f209182]) ).
fof(f220027,plain,
( ~ range_3_0(bitIndex3)
| v231499(sK115,bitIndex3)
| ~ spl116_5
| spl116_6
| ~ spl116_45 ),
inference(resolution,[],[f219994,f216375]) ).
fof(f220048,plain,
( ~ v231500(sK115,bitIndex2)
| spl116_368 ),
inference(resolution,[],[f219935,f209482]) ).
fof(f220049,plain,
( $false
| spl116_8
| ~ spl116_16
| ~ spl116_45
| spl116_368 ),
inference(forward_subsumption_resolution,[],[f220048,f219971]) ).
fof(f220050,plain,
( spl116_8
| ~ spl116_16
| ~ spl116_45
| spl116_368 ),
inference(avatar_contradiction_clause,[],[f220049]) ).
fof(f220051,plain,
( ~ v126476(sK115,bitIndex1)
| ~ spl116_368 ),
inference(resolution,[],[f219934,f209835]) ).
fof(f220053,plain,
( $false
| ~ spl116_31
| ~ spl116_368 ),
inference(forward_subsumption_resolution,[],[f220051,f215823]) ).
fof(f220054,plain,
( ~ spl116_31
| ~ spl116_368 ),
inference(avatar_contradiction_clause,[],[f220053]) ).
fof(f220058,plain,
( $false
| spl116_1
| ~ spl116_372 ),
inference(forward_subsumption_resolution,[],[f220022,f215549]) ).
fof(f220059,plain,
( spl116_1
| ~ spl116_372 ),
inference(avatar_contradiction_clause,[],[f220058]) ).
fof(f220114,plain,
( ~ v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| spl116_372 ),
inference(resolution,[],[f219979,f209185]) ).
fof(f220115,plain,
( ~ range_3_0(bitIndex2)
| ~ spl116_369
| spl116_372 ),
inference(forward_subsumption_resolution,[],[f220114,f219939]) ).
fof(f220116,plain,
( $false
| ~ spl116_369
| spl116_372 ),
inference(forward_subsumption_resolution,[],[f220115,f215467]) ).
fof(f220117,plain,
( ~ spl116_369
| spl116_372 ),
inference(avatar_contradiction_clause,[],[f220116]) ).
fof(f220118,plain,
( $false
| spl116_9
| spl116_14
| ~ spl116_16
| spl116_31
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f219891,f219938]) ).
fof(f220119,plain,
( spl116_9
| spl116_14
| ~ spl116_16
| spl116_31
| spl116_369 ),
inference(avatar_contradiction_clause,[],[f220118]) ).
fof(f220125,plain,
( ! [X0] :
( ~ v6(sK115,X0)
| b0001(X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215600,f209198]) ).
fof(f220126,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ b0001(X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f215600,f209199]) ).
fof(f220133,plain,
( ! [X0] :
( b0001(X0)
| ~ range_3_0(X0)
| ~ v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f220125,f209184]) ).
fof(f220134,plain,
( ! [X0] :
( ~ v231511(sK115,X0)
| ~ range_3_0(X0)
| b0001(X0) )
| ~ spl116_9 ),
inference(duplicate_literal_removal,[],[f220133]) ).
fof(f220144,plain,
( ! [X0] :
( ~ b0001(X0)
| ~ range_3_0(X0)
| v231511(sK115,X0)
| ~ range_3_0(X0) )
| ~ spl116_9 ),
inference(resolution,[],[f220126,f209185]) ).
fof(f220145,plain,
( ! [X0] :
( v231511(sK115,X0)
| ~ range_3_0(X0)
| ~ b0001(X0) )
| ~ spl116_9 ),
inference(duplicate_literal_removal,[],[f220144]) ).
fof(f220169,plain,
( ~ range_3_0(bitIndex3)
| b0001(bitIndex3)
| v231510(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f220134,f209186]) ).
fof(f220196,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v231528(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f220145,f209195]) ).
fof(f220197,plain,
( ~ range_3_0(bitIndex0)
| ~ b0001(bitIndex0)
| v231525(sK115)
| ~ v231516(sK115)
| ~ spl116_9 ),
inference(resolution,[],[f220145,f209193]) ).
fof(f220203,plain,
( ~ b0001(bitIndex0)
| v231525(sK115)
| ~ v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220197,f215465]) ).
fof(f220204,plain,
( ~ b0001(bitIndex0)
| v231528(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220196,f215465]) ).
fof(f220206,plain,
( v231525(sK115)
| ~ v231516(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220203,f209211]) ).
fof(f220207,plain,
( v231528(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220204,f209211]) ).
fof(f220210,plain,
( ~ v231516(sK115)
| ~ spl116_9
| spl116_47 ),
inference(forward_subsumption_resolution,[],[f220206,f216085]) ).
fof(f220211,plain,
( $false
| spl116_1
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220207,f215551]) ).
fof(f220212,plain,
( spl116_1
| ~ spl116_9 ),
inference(avatar_contradiction_clause,[],[f220211]) ).
fof(f220213,plain,
( $false
| ~ spl116_9
| ~ spl116_11
| spl116_47 ),
inference(forward_subsumption_resolution,[],[f220210,f215609]) ).
fof(f220214,plain,
( ~ spl116_9
| ~ spl116_11
| spl116_47 ),
inference(avatar_contradiction_clause,[],[f220213]) ).
fof(f220215,plain,
( v231499(sK115,bitIndex3)
| ~ spl116_5
| spl116_6
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f220027,f215468]) ).
fof(f220224,plain,
( b0001(bitIndex3)
| v231510(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220169,f215468]) ).
fof(f220232,plain,
( v231510(sK115)
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220224,f209214]) ).
fof(f220233,plain,
( $false
| ~ spl116_5
| spl116_6
| ~ spl116_9 ),
inference(forward_subsumption_resolution,[],[f220232,f219975]) ).
fof(f220234,plain,
( ~ spl116_5
| spl116_6
| ~ spl116_9 ),
inference(avatar_contradiction_clause,[],[f220233]) ).
fof(f220252,plain,
( ! [X0] :
( ~ v231496(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9 ),
inference(resolution,[],[f215599,f209201]) ).
fof(f220255,plain,
( b0010(bitIndex3)
| ~ range_3_0(bitIndex3)
| ~ v231497(sK115)
| ~ spl116_10 ),
inference(resolution,[],[f215603,f209227]) ).
fof(f220257,plain,
( ~ range_3_0(bitIndex3)
| ~ v231497(sK115)
| ~ spl116_10 ),
inference(forward_subsumption_resolution,[],[f220255,f209298]) ).
fof(f220258,plain,
( ~ v231497(sK115)
| ~ spl116_10 ),
inference(forward_subsumption_resolution,[],[f220257,f215468]) ).
fof(f220259,plain,
( $false
| ~ spl116_10
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220258,f215647]) ).
fof(f220260,plain,
( ~ spl116_10
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f220259]) ).
fof(f220315,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v231497(sK115) )
| spl116_9 ),
inference(resolution,[],[f220252,f209230]) ).
fof(f220316,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ range_3_0(X0)
| ~ v231497(sK115) )
| spl116_9 ),
inference(resolution,[],[f220252,f209228]) ).
fof(f220319,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ b0010(X0)
| ~ v231497(sK115) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f220316]) ).
fof(f220320,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ v231499(sK115,X0)
| v231497(sK115) )
| spl116_9 ),
inference(duplicate_literal_removal,[],[f220315]) ).
fof(f220321,plain,
( ! [X0] :
( v6(sK115,X0)
| ~ range_3_0(X0)
| ~ b0010(X0) )
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220319,f215647]) ).
fof(f220351,plain,
( ! [X0] :
( ~ range_3_0(X0)
| ~ b0010(X0)
| v231511(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9
| ~ spl116_14 ),
inference(resolution,[],[f220321,f209185]) ).
fof(f220352,plain,
( ! [X0] :
( v231511(sK115,X0)
| ~ b0010(X0)
| ~ range_3_0(X0) )
| spl116_9
| ~ spl116_14 ),
inference(duplicate_literal_removal,[],[f220351]) ).
fof(f220407,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| spl116_9
| ~ spl116_14
| spl116_363 ),
inference(resolution,[],[f220352,f219870]) ).
fof(f220415,plain,
( ~ b0010(bitIndex1)
| ~ range_3_0(bitIndex1)
| v231528(sK115)
| spl116_9
| ~ spl116_14 ),
inference(resolution,[],[f220352,f209194]) ).
fof(f220420,plain,
( ~ range_3_0(bitIndex1)
| v231528(sK115)
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220415,f209296]) ).
fof(f220421,plain,
( ~ range_3_0(bitIndex1)
| spl116_9
| ~ spl116_14
| spl116_363 ),
inference(forward_subsumption_resolution,[],[f220407,f209296]) ).
fof(f220423,plain,
( v231528(sK115)
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220420,f215466]) ).
fof(f220424,plain,
( $false
| spl116_9
| ~ spl116_14
| spl116_363 ),
inference(forward_subsumption_resolution,[],[f220421,f215466]) ).
fof(f220425,plain,
( spl116_9
| ~ spl116_14
| spl116_363 ),
inference(avatar_contradiction_clause,[],[f220424]) ).
fof(f220427,plain,
( $false
| spl116_1
| spl116_9
| ~ spl116_14 ),
inference(forward_subsumption_resolution,[],[f220423,f215551]) ).
fof(f220428,plain,
( spl116_1
| spl116_9
| ~ spl116_14 ),
inference(avatar_contradiction_clause,[],[f220427]) ).
fof(f220432,plain,
( ! [X0] :
( ~ v231499(sK115,X0)
| ~ range_3_0(X0)
| v6(sK115,X0) )
| spl116_9
| spl116_14 ),
inference(forward_subsumption_resolution,[],[f220320,f215646]) ).
fof(f220463,plain,
( ~ v231499(sK115,bitIndex3)
| ~ range_3_0(bitIndex3)
| v2311(sK115)
| spl116_18 ),
inference(resolution,[],[f215679,f209305]) ).
fof(f220467,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231502(sK115,X0)
| ~ range_3_0(X0)
| v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(resolution,[],[f220432,f209306]) ).
fof(f220472,plain,
( ! [X0] :
( ~ range_3_0(X0)
| v6(sK115,X0)
| ~ v231502(sK115,X0)
| v2311(sK115) )
| spl116_9
| spl116_14 ),
inference(duplicate_literal_removal,[],[f220467]) ).
fof(f220473,plain,
( ! [X0] :
( ~ v231502(sK115,X0)
| v6(sK115,X0)
| ~ range_3_0(X0) )
| spl116_9
| spl116_14
| spl116_16 ),
inference(forward_subsumption_resolution,[],[f220472,f215670]) ).
fof(f220663,plain,
( v6(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| ~ v231503(sK115)
| spl116_9
| spl116_14
| spl116_16 ),
inference(resolution,[],[f220473,f209488]) ).
fof(f220665,plain,
( ~ range_3_0(bitIndex2)
| ~ v231503(sK115)
| spl116_9
| spl116_14
| spl116_16
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f220663,f219938]) ).
fof(f220666,plain,
( ~ v231503(sK115)
| spl116_9
| spl116_14
| spl116_16
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f220665,f215467]) ).
fof(f220667,plain,
( $false
| spl116_9
| spl116_14
| spl116_16
| spl116_18
| spl116_369 ),
inference(forward_subsumption_resolution,[],[f220666,f215817]) ).
fof(f220668,plain,
( spl116_9
| spl116_14
| spl116_16
| spl116_18
| spl116_369 ),
inference(avatar_contradiction_clause,[],[f220667]) ).
fof(f220669,plain,
( spl116_15
| ~ spl116_5
| spl116_6
| ~ spl116_45 ),
inference(avatar_split_clause,[],[f220215,f215957,f215573,f215569,f215649]) ).
fof(f220672,plain,
( ~ range_3_0(bitIndex3)
| v2311(sK115)
| ~ spl116_15
| spl116_18 ),
inference(forward_subsumption_resolution,[],[f220463,f215650]) ).
fof(f220674,plain,
( v2311(sK115)
| ~ spl116_15
| spl116_18 ),
inference(forward_subsumption_resolution,[],[f220672,f215468]) ).
fof(f220675,plain,
( $false
| ~ spl116_15
| spl116_16
| spl116_18 ),
inference(forward_subsumption_resolution,[],[f220674,f215670]) ).
fof(f220676,plain,
( ~ spl116_15
| spl116_16
| spl116_18 ),
inference(avatar_contradiction_clause,[],[f220675]) ).
fof(f220677,plain,
( v231502(sK115,bitIndex1)
| v2311(sK115)
| spl116_11
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f219820,f215466]) ).
fof(f220683,plain,
( v231502(sK115,bitIndex1)
| spl116_11
| spl116_16
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f220677,f215670]) ).
fof(f220820,plain,
( v231502(sK115,bitIndex2)
| ~ range_3_0(bitIndex2)
| v2311(sK115)
| ~ spl116_371 ),
inference(resolution,[],[f219949,f209305]) ).
fof(f220823,plain,
( ~ range_3_0(bitIndex2)
| v2311(sK115)
| ~ spl116_18
| ~ spl116_371 ),
inference(forward_subsumption_resolution,[],[f220820,f216379]) ).
fof(f220825,plain,
( v2311(sK115)
| ~ spl116_18
| ~ spl116_371 ),
inference(forward_subsumption_resolution,[],[f220823,f215467]) ).
fof(f220828,plain,
( $false
| spl116_16
| ~ spl116_18
| ~ spl116_371 ),
inference(forward_subsumption_resolution,[],[f220825,f215670]) ).
fof(f220829,plain,
( spl116_16
| ~ spl116_18
| ~ spl116_371 ),
inference(avatar_contradiction_clause,[],[f220828]) ).
fof(f222518,plain,
( ~ range_1_0(bitIndex1)
| spl116_11
| spl116_16
| ~ spl116_45 ),
inference(resolution,[],[f220683,f209489]) ).
fof(f222520,plain,
( $false
| spl116_11
| spl116_16
| ~ spl116_45 ),
inference(forward_subsumption_resolution,[],[f222518,f215464]) ).
fof(f222521,plain,
( spl116_11
| spl116_16
| ~ spl116_45 ),
inference(avatar_contradiction_clause,[],[f222520]) ).
cnf(s1,plain,
( ~ spl116_1
| ~ spl116_2 ),
inference(sat_conversion,[],[f215547]) ).
cnf(s4,plain,
( spl116_3
| ~ spl116_7
| ~ spl116_8 ),
inference(sat_conversion,[],[f215586]) ).
cnf(s6,plain,
( spl116_1
| spl116_9
| ~ spl116_10 ),
inference(sat_conversion,[],[f215605]) ).
cnf(s7,plain,
( spl116_7
| ~ spl116_11
| ~ spl116_12 ),
inference(sat_conversion,[],[f215615]) ).
cnf(s9,plain,
( spl116_2
| ~ spl116_4 ),
inference(sat_conversion,[],[f215624]) ).
cnf(s10,plain,
( spl116_2
| ~ spl116_6 ),
inference(sat_conversion,[],[f215627]) ).
cnf(s11,plain,
( spl116_9
| spl116_10
| ~ spl116_13 ),
inference(sat_conversion,[],[f215643]) ).
cnf(s12,plain,
( spl116_10
| spl116_14
| ~ spl116_15 ),
inference(sat_conversion,[],[f215652]) ).
cnf(s13,plain,
( spl116_15
| ~ spl116_16
| ~ spl116_17 ),
inference(sat_conversion,[],[f215675]) ).
cnf(s14,plain,
( spl116_15
| spl116_16
| ~ spl116_18 ),
inference(sat_conversion,[],[f215680]) ).
cnf(s32,plain,
( spl116_17
| ~ spl116_31 ),
inference(sat_conversion,[],[f215943]) ).
cnf(s33,plain,
( spl116_9
| spl116_14
| spl116_45 ),
inference(sat_conversion,[],[f215959]) ).
cnf(s39,plain,
( ~ spl116_9
| spl116_11 ),
inference(sat_conversion,[],[f216015]) ).
cnf(s43,plain,
( ~ spl116_5
| spl116_6
| spl116_13 ),
inference(sat_conversion,[],[f216033]) ).
cnf(s47,plain,
( spl116_8
| ~ spl116_9 ),
inference(sat_conversion,[],[f216047]) ).
cnf(s186,plain,
( spl116_9
| spl116_12
| spl116_14
| ~ spl116_16 ),
inference(sat_conversion,[],[f218160]) ).
cnf(s193,plain,
( spl116_8
| spl116_9
| ~ spl116_14 ),
inference(sat_conversion,[],[f218187]) ).
cnf(s194,plain,
( spl116_9
| spl116_12
| ~ spl116_14 ),
inference(sat_conversion,[],[f218189]) ).
cnf(s344,plain,
( spl116_9
| spl116_12
| spl116_14
| spl116_16 ),
inference(sat_conversion,[],[f219475]) ).
cnf(s353,plain,
( spl116_9
| spl116_11
| spl116_14
| ~ spl116_16 ),
inference(sat_conversion,[],[f219866]) ).
cnf(s354,plain,
( ~ spl116_12
| ~ spl116_363
| spl116_364 ),
inference(sat_conversion,[],[f219875]) ).
cnf(s356,plain,
( spl116_5
| ~ spl116_7
| spl116_8 ),
inference(sat_conversion,[],[f219881]) ).
cnf(s357,plain,
( spl116_5
| ~ spl116_8
| ~ spl116_47 ),
inference(sat_conversion,[],[f219882]) ).
cnf(s358,plain,
( spl116_5
| ~ spl116_8
| ~ spl116_364 ),
inference(sat_conversion,[],[f219883]) ).
cnf(s364,plain,
( ~ spl116_15
| ~ spl116_16
| spl116_17 ),
inference(sat_conversion,[],[f219911]) ).
cnf(s365,plain,
( ~ spl116_17
| spl116_31 ),
inference(sat_conversion,[],[f219913]) ).
cnf(s372,plain,
( spl116_2
| ~ spl116_3
| spl116_4 ),
inference(sat_conversion,[],[f219965]) ).
cnf(s374,plain,
( spl116_8
| ~ spl116_45
| spl116_371 ),
inference(sat_conversion,[],[f219970]) ).
cnf(s383,plain,
( spl116_8
| ~ spl116_16
| ~ spl116_45
| spl116_368 ),
inference(sat_conversion,[],[f220050]) ).
cnf(s384,plain,
( ~ spl116_31
| ~ spl116_368 ),
inference(sat_conversion,[],[f220054]) ).
cnf(s389,plain,
( spl116_1
| ~ spl116_372 ),
inference(sat_conversion,[],[f220059]) ).
cnf(s394,plain,
( ~ spl116_369
| spl116_372 ),
inference(sat_conversion,[],[f220117]) ).
cnf(s395,plain,
( spl116_9
| spl116_14
| ~ spl116_16
| spl116_31
| spl116_369 ),
inference(sat_conversion,[],[f220119]) ).
cnf(s402,plain,
( spl116_1
| ~ spl116_9 ),
inference(sat_conversion,[],[f220212]) ).
cnf(s403,plain,
( ~ spl116_9
| ~ spl116_11
| spl116_47 ),
inference(sat_conversion,[],[f220214]) ).
cnf(s413,plain,
( ~ spl116_5
| spl116_6
| ~ spl116_9 ),
inference(sat_conversion,[],[f220234]) ).
cnf(s418,plain,
( ~ spl116_10
| ~ spl116_14 ),
inference(sat_conversion,[],[f220260]) ).
cnf(s430,plain,
( spl116_9
| ~ spl116_14
| spl116_363 ),
inference(sat_conversion,[],[f220425]) ).
cnf(s431,plain,
( spl116_1
| spl116_9
| ~ spl116_14 ),
inference(sat_conversion,[],[f220428]) ).
cnf(s437,plain,
( spl116_9
| spl116_14
| spl116_16
| spl116_18
| spl116_369 ),
inference(sat_conversion,[],[f220668]) ).
cnf(s441,plain,
( ~ spl116_5
| spl116_6
| spl116_15
| ~ spl116_45 ),
inference(sat_conversion,[],[f220669]) ).
cnf(s442,plain,
( ~ spl116_15
| spl116_16
| spl116_18 ),
inference(sat_conversion,[],[f220676]) ).
cnf(s450,plain,
( spl116_16
| ~ spl116_18
| ~ spl116_371 ),
inference(sat_conversion,[],[f220829]) ).
cnf(s586,plain,
( spl116_11
| spl116_16
| ~ spl116_45 ),
inference(sat_conversion,[],[f222521]) ).
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(f222522,plain,
$false,
inference(avatar_sat_refutation,[],[s630]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV126+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.11 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.44 % Computer : n004.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 27 11:43:24 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.54 Running first-order theorem proving
% 0.21/0.54 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.57/6.84 % (3373659)Detected formulas, will run a generic FOF schedule.
% 15.57/6.84 % (3373783)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4034534205:i=119:av=off:ss=axioms_2958 on theBenchmark for (2958ds/119Mi)
% 15.57/6.84 % (3373779)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=382328083:i=141193_2958 on theBenchmark for (2958ds/141193Mi)
% 15.57/6.84 % (3373781)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=3716200964:i=141695:sd=1:nm=32:gsp=on:ss=included_2958 on theBenchmark for (2958ds/141695Mi)
% 15.57/6.84 % (3373780)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=824896789:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2958 on theBenchmark for (2958ds/134677Mi)
% 15.57/6.84 % (3373782)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2525525480:i=109:sd=1:ins=1:gsp=on:ss=axioms_2958 on theBenchmark for (2958ds/109Mi)
% 15.57/6.84 % (3373783)Instruction limit reached!
% 15.57/6.84 % (3373783)------------------------------
% 15.57/6.84 % (3373783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/6.84 % (3373783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/6.84 % (3373783)CaDiCaL version: 2.1.3
% 15.57/6.84 % (3373783)Termination reason: Instruction limit
% 15.57/6.84 % (3373783)Termination phase: SInE selection
% 15.57/6.84 % (3373783)Time elapsed: 0.036 s
% 15.57/6.84 % (3373783)Peak memory usage: 270 MB
% 15.57/6.84 % (3373783)Instructions burned: 120 (million)
% 15.57/6.84 % (3373784)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1133362092:s2a=on:i=139:gtg=position_2958 on theBenchmark for (2958ds/139Mi)
% 15.57/6.84 % (3373785)dis-21_1_sil=8000:lcm=predicate:random_seed=1743321407: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)
% 15.57/6.84 % (3373782)Instruction limit reached!
% 15.57/6.84 % (3373782)------------------------------
% 15.57/6.84 % (3373782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/6.84 % (3373782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/6.84 % (3373782)CaDiCaL version: 2.1.3
% 15.57/6.84 % (3373782)Termination reason: Instruction limit
% 15.57/6.84 % (3373782)Termination phase: SInE selection
% 15.57/6.84 % (3373782)Time elapsed: 0.055 s
% 15.57/6.84 % (3373782)Peak memory usage: 270 MB
% 15.57/6.84 % (3373782)Instructions burned: 111 (million)
% 15.57/6.84 % (3373785)Instruction limit reached!
% 15.57/6.84 % (3373785)------------------------------
% 15.57/6.84 % (3373785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/6.84 % (3373785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/6.84 % (3373785)CaDiCaL version: 2.1.3
% 15.57/6.84 % (3373785)Termination reason: Instruction limit
% 15.57/6.84 % (3373785)Termination phase: SInE selection
% 15.57/6.84 % (3373785)Time elapsed: 0.065 s
% 15.57/6.84 % (3373785)Peak memory usage: 270 MB
% 15.57/6.84 % (3373785)Instructions burned: 132 (million)
% 15.57/6.84 % (3373784)Instruction limit reached!
% 15.57/6.84 % (3373784)------------------------------
% 15.57/6.84 % (3373784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/6.84 % (3373784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/6.84 % (3373784)CaDiCaL version: 2.1.3
% 15.57/6.84 % (3373784)Termination reason: Instruction limit
% 15.57/6.84 % (3373784)Termination phase: Property scanning
% 15.57/6.84 % (3373784)Time elapsed: 0.111 s
% 15.57/6.84 % (3373784)Peak memory usage: 270 MB
% 15.57/6.84 % (3373784)Instructions burned: 140 (million)
% 15.57/6.84 % (3373793)lrs+10_1_sil=8000:sp=occurrence:random_seed=812398566:i=285:sd=3:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/285Mi)
% 15.57/6.84 % (3373794)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3316419178:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2956 on theBenchmark for (2956ds/157Mi)
% 15.57/6.84 % (3373793)Instruction limit reached!
% 15.57/6.84 % (3373793)------------------------------
% 15.57/6.84 % (3373793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.57/6.84 % (3373793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.57/6.84 % (3373793)CaDiCaL version: 2.1.3
% 15.57/6.84 % (3373793)Termination reason: Instruction limit
% 23.79/7.92 % (3373793)Termination phase: SInE selection
% 23.79/7.92 % (3373793)Time elapsed: 0.070 s
% 23.79/7.92 % (3373793)Peak memory usage: 270 MB
% 23.79/7.92 % (3373793)Instructions burned: 289 (million)
% 23.79/7.92 % (3373797)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=2490942511:s2a=on:i=248:s2at=1.23:gtg=position_2955 on theBenchmark for (2955ds/248Mi)
% 23.79/7.92 % (3373795)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4123341490:i=325:sd=1:ss=axioms:sgt=32_2956 on theBenchmark for (2956ds/325Mi)
% 23.79/7.92 % (3373794)Instruction limit reached!
% 23.79/7.92 % (3373794)------------------------------
% 23.79/7.92 % (3373794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/7.92 % (3373794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/7.92 % (3373794)CaDiCaL version: 2.1.3
% 23.79/7.92 % (3373794)Termination reason: Instruction limit
% 23.79/7.92 % (3373794)Termination phase: Property scanning
% 23.79/7.92 % (3373794)Time elapsed: 0.120 s
% 23.79/7.92 % (3373794)Peak memory usage: 270 MB
% 23.79/7.92 % (3373794)Instructions burned: 160 (million)
% 23.79/7.92 % (3373799)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1400552592:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2954 on theBenchmark for (2954ds/294Mi)
% 23.79/7.92 % (3373799)Instruction limit reached!
% 23.79/7.92 % (3373799)------------------------------
% 23.79/7.92 % (3373799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/7.92 % (3373799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/7.92 % (3373799)CaDiCaL version: 2.1.3
% 23.79/7.92 % (3373799)Termination reason: Instruction limit
% 23.79/7.92 % (3373799)Termination phase: SInE selection
% 23.79/7.92 % (3373799)Time elapsed: 0.072 s
% 23.79/7.92 % (3373799)Peak memory usage: 270 MB
% 23.79/7.92 % (3373799)Instructions burned: 300 (million)
% 23.79/7.92 % (3373797)Instruction limit reached!
% 23.79/7.92 % (3373797)------------------------------
% 23.79/7.92 % (3373797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/7.92 % (3373797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/7.92 % (3373797)CaDiCaL version: 2.1.3
% 23.79/7.92 % (3373797)Termination reason: Instruction limit
% 23.79/7.92 % (3373797)Termination phase: Property scanning
% 23.79/7.92 % (3373797)Time elapsed: 0.154 s
% 23.79/7.92 % (3373797)Peak memory usage: 270 MB
% 23.79/7.92 % (3373797)Instructions burned: 248 (million)
% 23.79/7.92 % (3373795)Instruction limit reached!
% 23.79/7.92 % (3373795)------------------------------
% 23.79/7.92 % (3373795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/7.92 % (3373795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/7.92 % (3373795)CaDiCaL version: 2.1.3
% 23.79/7.92 % (3373795)Termination reason: Instruction limit
% 23.79/7.92 % (3373795)Termination phase: SInE selection
% 23.79/7.92 % (3373795)Time elapsed: 0.172 s
% 23.79/7.92 % (3373795)Peak memory usage: 270 MB
% 23.79/7.92 % (3373795)Instructions burned: 325 (million)
% 23.79/7.92 % (3373803)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2951568564:i=2350_2953 on theBenchmark for (2953ds/2350Mi)
% 23.79/7.92 % (3373804)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3088954041:cts=off:i=113:fsr=off:ss=included:sgt=4_2952 on theBenchmark for (2952ds/113Mi)
% 23.79/7.92 % (3373804)Instruction limit reached!
% 23.79/7.92 % (3373804)------------------------------
% 23.79/7.92 % (3373804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.79/7.92 % (3373804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.79/7.92 % (3373804)CaDiCaL version: 2.1.3
% 23.79/7.92 % (3373804)Termination reason: Instruction limit
% 23.79/7.92 % (3373804)Termination phase: SInE selection
% 23.79/7.92 % (3373804)Time elapsed: 0.034 s
% 23.79/7.92 % (3373804)Peak memory usage: 270 MB
% 23.79/7.92 % (3373804)Instructions burned: 114 (million)
% 23.79/7.92 % (3373807)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=620533047:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2952 on theBenchmark for (2952ds/114Mi)
% 23.79/7.92 % (3373805)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2044366485:i=127:av=off:fsr=off:sup=off_2952 on theBenchmark for (2952ds/127Mi)
% 23.79/7.92 % (3373809)lrs+10_1_sil=8000:sp=occurrence:random_seed=52461177:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2951 on theBenchmark for (2951ds/907Mi)
% 27.27/8.34 % (3373807)Instruction limit reached!
% 27.27/8.34 % (3373807)------------------------------
% 27.27/8.34 % (3373807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/8.34 % (3373807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/8.34 % (3373807)CaDiCaL version: 2.1.3
% 27.27/8.34 % (3373807)Termination reason: Instruction limit
% 27.27/8.34 % (3373807)Termination phase: Property scanning
% 27.27/8.34 % (3373807)Time elapsed: 0.100 s
% 27.27/8.34 % (3373807)Peak memory usage: 270 MB
% 27.27/8.34 % (3373807)Instructions burned: 116 (million)
% 27.27/8.34 % (3373805)Instruction limit reached!
% 27.27/8.34 % (3373805)------------------------------
% 27.27/8.34 % (3373805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/8.34 % (3373805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/8.34 % (3373805)CaDiCaL version: 2.1.3
% 27.27/8.34 % (3373805)Termination reason: Instruction limit
% 27.27/8.34 % (3373805)Termination phase: Preprocessing 1
% 27.27/8.34 % (3373805)Time elapsed: 0.149 s
% 27.27/8.34 % (3373805)Peak memory usage: 271 MB
% 27.27/8.34 % (3373805)Instructions burned: 127 (million)
% 27.27/8.34 % (3373809)Instruction limit reached!
% 27.27/8.34 % (3373809)------------------------------
% 27.27/8.34 % (3373809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/8.34 % (3373809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/8.34 % (3373809)CaDiCaL version: 2.1.3
% 27.27/8.34 % (3373809)Termination reason: Instruction limit
% 27.27/8.34 % (3373809)Termination phase: SInE selection
% 27.27/8.34 % (3373809)Time elapsed: 0.211 s
% 27.27/8.34 % (3373809)Peak memory usage: 276 MB
% 27.27/8.34 % (3373809)Instructions burned: 909 (million)
% 27.27/8.34 % (3373813)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1512641700:i=437:sd=1:aac=none:ss=included_2949 on theBenchmark for (2949ds/437Mi)
% 27.27/8.34 % (3373814)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=995021076:i=5202:ss=axioms:sgt=16_2948 on theBenchmark for (2948ds/5202Mi)
% 27.27/8.34 % (3373816)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1340484314:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2947 on theBenchmark for (2947ds/134Mi)
% 27.27/8.34 % (3373813)Instruction limit reached!
% 27.27/8.34 % (3373813)------------------------------
% 27.27/8.34 % (3373813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/8.34 % (3373813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/8.34 % (3373813)CaDiCaL version: 2.1.3
% 27.27/8.34 % (3373813)Termination reason: Instruction limit
% 27.27/8.34 % (3373813)Termination phase: SInE selection
% 27.27/8.34 % (3373813)Time elapsed: 0.183 s
% 27.27/8.34 % (3373813)Peak memory usage: 270 MB
% 27.27/8.34 % (3373813)Instructions burned: 439 (million)
% 27.27/8.34 % (3373816)Instruction limit reached!
% 27.27/8.34 % (3373816)------------------------------
% 27.27/8.34 % (3373816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/8.34 % (3373816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/8.34 % (3373816)CaDiCaL version: 2.1.3
% 27.27/8.34 % (3373816)Termination reason: Instruction limit
% 27.27/8.34 % (3373816)Termination phase: SInE selection
% 27.27/8.34 % (3373816)Time elapsed: 0.039 s
% 27.27/8.34 % (3373816)Peak memory usage: 270 MB
% 27.27/8.34 % (3373816)Instructions burned: 136 (million)
% 27.27/8.34 % (3373819)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2297684566:st=8:i=592:sd=3:ep=RST:ss=axioms_2945 on theBenchmark for (2945ds/592Mi)
% 27.27/8.34 % (3373820)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1151047979:st=3:i=13193:sd=3:ss=axioms_2945 on theBenchmark for (2945ds/13193Mi)
% 27.27/8.34 % (3373819)Instruction limit reached!
% 27.27/8.34 % (3373819)------------------------------
% 27.27/8.34 % (3373819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.27/8.34 % (3373819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.27/8.34 % (3373819)CaDiCaL version: 2.1.3
% 27.27/8.34 % (3373819)Termination reason: Instruction limit
% 27.27/8.34 % (3373819)Termination phase: SInE selection
% 27.27/8.34 % (3373819)Time elapsed: 0.130 s
% 27.27/8.34 % (3373819)Peak memory usage: 272 MB
% 27.27/8.34 % (3373819)Instructions burned: 595 (million)
% 27.27/8.34 % (3373823)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=1269924955:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/125Mi)
% 59.02/12.87 % (3373823)Instruction limit reached!
% 59.02/12.87 % (3373823)------------------------------
% 59.02/12.87 % (3373823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.02/12.87 % (3373823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.02/12.87 % (3373823)CaDiCaL version: 2.1.3
% 59.02/12.87 % (3373823)Termination reason: Instruction limit
% 59.02/12.87 % (3373823)Termination phase: Property scanning
% 59.02/12.87 % (3373823)Time elapsed: 0.061 s
% 59.02/12.87 % (3373823)Peak memory usage: 270 MB
% 59.02/12.87 % (3373823)Instructions burned: 127 (million)
% 59.02/12.87 % (3373825)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2120603457:i=134:gtgl=5:slsql=off:gtg=exists_sym_2940 on theBenchmark for (2940ds/134Mi)
% 59.02/12.87 % (3373803)Instruction limit reached!
% 59.02/12.87 % (3373803)------------------------------
% 59.02/12.87 % (3373803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.02/12.87 % (3373803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.02/12.87 % (3373803)CaDiCaL version: 2.1.3
% 59.02/12.87 % (3373803)Termination reason: Instruction limit
% 59.02/12.87 % (3373803)Termination phase: Naming
% 59.02/12.87 % (3373803)Time elapsed: 1.402 s
% 59.02/12.87 % (3373803)Peak memory usage: 355 MB
% 59.02/12.87 % (3373803)Instructions burned: 2351 (million)
% 59.02/12.87 % (3373825)Instruction limit reached!
% 59.02/12.87 % (3373825)------------------------------
% 59.02/12.87 % (3373825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.02/12.87 % (3373825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.02/12.87 % (3373825)CaDiCaL version: 2.1.3
% 59.02/12.87 % (3373825)Termination reason: Instruction limit
% 59.02/12.87 % (3373825)Termination phase: Property scanning
% 59.02/12.87 % (3373825)Time elapsed: 0.109 s
% 59.02/12.87 % (3373825)Peak memory usage: 270 MB
% 59.02/12.87 % (3373825)Instructions burned: 135 (million)
% 59.02/12.87 % (3373827)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=865133272:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2937 on theBenchmark for (2937ds/141Mi)
% 59.02/12.87 % (3373828)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4122542972:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2937 on theBenchmark for (2937ds/431Mi)
% 59.02/12.87 % (3373827)Instruction limit reached!
% 59.02/12.87 % (3373827)------------------------------
% 59.02/12.87 % (3373827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.02/12.87 % (3373827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.02/12.87 % (3373827)CaDiCaL version: 2.1.3
% 59.02/12.87 % (3373827)Termination reason: Instruction limit
% 59.02/12.87 % (3373827)Termination phase: SInE selection
% 59.02/12.87 % (3373827)Time elapsed: 0.070 s
% 59.02/12.87 % (3373827)Peak memory usage: 270 MB
% 59.02/12.87 % (3373827)Instructions burned: 143 (million)
% 59.02/12.87 % (3373828)Instruction limit reached!
% 59.02/12.87 % (3373828)------------------------------
% 59.02/12.87 % (3373828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.02/12.87 % (3373828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.02/12.87 % (3373828)CaDiCaL version: 2.1.3
% 59.02/12.87 % (3373828)Termination reason: Instruction limit
% 59.02/12.87 % (3373828)Termination phase: SInE selection
% 59.02/12.87 % (3373828)Time elapsed: 0.180 s
% 59.02/12.87 % (3373828)Peak memory usage: 270 MB
% 59.02/12.87 % (3373828)Instructions burned: 433 (million)
% 59.02/12.87 % (3373831)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=2966163832:i=6060:aac=none:ins=25_2935 on theBenchmark for (2935ds/6060Mi)
% 59.02/12.87 % (3373833)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=4238248817:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2933 on theBenchmark for (2933ds/150Mi)
% 59.02/12.87 % (3373833)Instruction limit reached!
% 59.02/12.87 % (3373833)------------------------------
% 59.02/12.87 % (3373833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.02/12.87 % (3373833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.02/12.87 % (3373833)CaDiCaL version: 2.1.3
% 59.02/12.87 % (3373833)Termination reason: Instruction limit
% 128.74/22.61 % (3373833)Termination phase: SInE selection
% 128.74/22.61 % (3373833)Time elapsed: 0.092 s
% 128.74/22.61 % (3373833)Peak memory usage: 270 MB
% 128.74/22.61 % (3373833)Instructions burned: 150 (million)
% 128.74/22.61 % (3373835)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1170300449:i=14155:bd=all_2930 on theBenchmark for (2930ds/14155Mi)
% 128.74/22.61 [W927 11:43:32.594087853 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594127937 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594173893 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594186174 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594211777 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594223704 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594250851 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594262761 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594287481 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594299241 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594325405 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.74/22.61 [W927 11:43:32.594337198 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.
% 128.74/22.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.12/28.18 % (3373814)Instruction limit reached!
% 157.12/28.18 % (3373814)------------------------------
% 157.12/28.18 % (3373814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.12/28.18 % (3373814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.12/28.18 % (3373814)CaDiCaL version: 2.1.3
% 157.12/28.18 % (3373814)Termination reason: Instruction limit
% 157.12/28.18 % (3373814)Termination phase: Property scanning
% 157.12/28.18 % (3373814)Time elapsed: 2.244 s
% 157.12/28.18 % (3373814)Peak memory usage: 422 MB
% 157.12/28.18 % (3373814)Instructions burned: 5208 (million)
% 157.12/28.18 % (3373837)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1608205528:i=667:av=off:fsr=off_2924 on theBenchmark for (2924ds/667Mi)
% 157.12/28.18 % (3373837)Instruction limit reached!
% 157.12/28.18 % (3373837)------------------------------
% 157.12/28.18 % (3373837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.12/28.18 % (3373837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.12/28.18 % (3373837)CaDiCaL version: 2.1.3
% 157.12/28.18 % (3373837)Termination reason: Instruction limit
% 157.12/28.18 % (3373837)Termination phase: Unused predicate definition removal
% 157.12/28.18 % (3373837)Time elapsed: 0.424 s
% 157.12/28.18 % (3373837)Peak memory usage: 346 MB
% 157.12/28.18 % (3373837)Instructions burned: 668 (million)
% 157.12/28.18 % (3373859)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=2527455882:s2a=on:i=185:s2at=1.8:fdi=4_2917 on theBenchmark for (2917ds/185Mi)
% 157.12/28.18 % (3373859)Instruction limit reached!
% 157.12/28.18 % (3373859)------------------------------
% 157.12/28.18 % (3373859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.12/28.18 % (3373859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.12/28.18 % (3373859)CaDiCaL version: 2.1.3
% 157.12/28.18 % (3373859)Termination reason: Instruction limit
% 157.12/28.18 % (3373859)Termination phase: SInE selection
% 157.12/28.18 % (3373859)Time elapsed: 0.071 s
% 157.12/28.18 % (3373859)Peak memory usage: 270 MB
% 157.12/28.18 % (3373859)Instructions burned: 188 (million)
% 157.12/28.18 % (3373872)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2797783502:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/193Mi)
% 157.12/28.18 % (3373872)Instruction limit reached!
% 157.12/28.18 % (3373872)------------------------------
% 157.12/28.18 % (3373872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.12/28.18 % (3373872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.12/28.18 % (3373872)CaDiCaL version: 2.1.3
% 157.12/28.18 % (3373872)Termination reason: Instruction limit
% 157.12/28.18 % (3373872)Termination phase: SInE selection
% 157.12/28.18 % (3373872)Time elapsed: 0.068 s
% 157.12/28.18 % (3373872)Peak memory usage: 270 MB
% 157.12/28.18 % (3373872)Instructions burned: 193 (million)
% 157.12/28.18 % (3373882)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=900756207:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2911 on theBenchmark for (2911ds/4850Mi)
% 157.12/28.18 % (3373820)Refutation not found, incomplete strategy
% 157.12/28.18 % (3373820)------------------------------
% 157.12/28.18 % (3373820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.12/28.18 % (3373820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.12/28.18 % (3373820)CaDiCaL version: 2.1.3
% 157.12/28.18 % (3373820)Termination reason: Refutation not found, incomplete strategy
% 157.12/28.18 % (3373820)Time elapsed: 5.355 s
% 157.12/28.18 % (3373820)Peak memory usage: 840 MB
% 157.12/28.18 % (3373820)Instructions burned: 6754 (million)
% 157.12/28.18 % (3373820)------------------------------
% 157.12/28.18 % (3373820)------------------------------
% 157.12/28.18 % (3373882)Instruction limit reached!
% 157.12/28.18 % (3373882)------------------------------
% 157.12/28.18 % (3373882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.12/28.18 % (3373882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.12/28.18 % (3373882)CaDiCaL version: 2.1.3
% 157.12/28.18 % (3373882)Termination reason: Instruction limit
% 157.12/28.18 % (3373882)Termination phase: Clausification
% 157.12/28.18 % (3373882)Time elapsed: 2.601 s
% 157.12/28.18 % (3373882)Peak memory usage: 530 MB
% 157.12/28.18 % (3373882)Instructions burned: 4852 (million)
% 157.12/28.18 % (3373831)Instruction limit reached!
% 157.12/28.18 % (3373831)------------------------------
% 175.03/29.17 % (3373831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.03/29.17 % (3373831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/29.17 % (3373831)CaDiCaL version: 2.1.3
% 175.03/29.17 % (3373831)Termination reason: Instruction limit
% 175.03/29.17 % (3373831)Termination phase: Property scanning
% 175.03/29.17 % (3373831)Time elapsed: 5.233 s
% 175.03/29.17 % (3373831)Peak memory usage: 470 MB
% 175.03/29.17 % (3373831)Instructions burned: 6060 (million)
% 175.03/29.17 % (3373946)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1185481781:i=12111:sd=1:ss=included_2883 on theBenchmark for (2883ds/12111Mi)
% 175.03/29.17 % (3373950)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=85041720:i=319:kws=precedence:fsr=off_2882 on theBenchmark for (2882ds/319Mi)
% 175.03/29.17 % (3373950)Instruction limit reached!
% 175.03/29.17 % (3373950)------------------------------
% 175.03/29.17 % (3373950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.03/29.17 % (3373950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/29.17 % (3373950)CaDiCaL version: 2.1.3
% 175.03/29.17 % (3373950)Termination reason: Instruction limit
% 175.03/29.17 % (3373950)Termination phase: Preprocessing 1
% 175.03/29.17 % (3373950)Time elapsed: 0.244 s
% 175.03/29.17 % (3373950)Peak memory usage: 271 MB
% 175.03/29.17 % (3373950)Instructions burned: 320 (million)
% 175.03/29.17 % (3373956)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=912415393:i=2064:ep=RST_2880 on theBenchmark for (2880ds/2064Mi)
% 175.03/29.17 % (3373961)dis-1011_128_sil=32000:random_seed=687259759:i=3706:ep=RST:av=off_2877 on theBenchmark for (2877ds/3706Mi)
% 175.03/29.17 % (3373956)Instruction limit reached!
% 175.03/29.17 % (3373956)------------------------------
% 175.03/29.17 % (3373956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.03/29.17 % (3373956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/29.17 % (3373956)CaDiCaL version: 2.1.3
% 175.03/29.17 % (3373956)Termination reason: Instruction limit
% 175.03/29.17 % (3373956)Termination phase: Preprocessing 3
% 175.03/29.17 % (3373956)Time elapsed: 2.241 s
% 175.03/29.17 % (3373956)Peak memory usage: 351 MB
% 175.03/29.17 % (3373956)Instructions burned: 2064 (million)
% 175.03/29.17 % (3373996)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3988289736:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2854 on theBenchmark for (2854ds/757Mi)
% 175.03/29.17 % (3373996)Instruction limit reached!
% 175.03/29.17 % (3373996)------------------------------
% 175.03/29.17 % (3373996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.03/29.17 % (3373996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/29.17 % (3373996)CaDiCaL version: 2.1.3
% 175.03/29.17 % (3373996)Termination reason: Instruction limit
% 175.03/29.17 % (3373996)Termination phase: SInE selection
% 175.03/29.17 % (3373996)Time elapsed: 0.526 s
% 175.03/29.17 % (3373996)Peak memory usage: 275 MB
% 175.03/29.17 % (3373996)Instructions burned: 757 (million)
% 175.03/29.17 % (3374011)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4287201637:i=13913:ss=axioms:sgt=8_2845 on theBenchmark for (2845ds/13913Mi)
% 175.03/29.17 % (3373961)Instruction limit reached!
% 175.03/29.17 % (3373961)------------------------------
% 175.03/29.17 % (3373961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.03/29.17 % (3373961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/29.17 % (3373961)CaDiCaL version: 2.1.3
% 175.03/29.17 % (3373961)Termination reason: Instruction limit
% 175.03/29.17 % (3373961)Termination phase: Clausification
% 175.03/29.17 % (3373961)Time elapsed: 3.901 s
% 175.03/29.17 % (3373961)Peak memory usage: 514 MB
% 175.03/29.17 % (3373961)Instructions burned: 3706 (million)
% 175.03/29.17 % (3374024)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1244063512:i=9925:aac=none_2835 on theBenchmark for (2835ds/9925Mi)
% 175.03/29.17 % (3374011)Refutation not found, incomplete strategy
% 175.03/29.17 % (3374011)------------------------------
% 175.03/29.17 % (3374011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 175.03/29.17 % (3374011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 175.03/29.17 % (3374011)CaDiCaL version: 2.1.3
% 175.03/29.17 % (3374011)Termination reason: Refutation not found, incomplete strategy
% 215.56/34.95 % (3374011)Time elapsed: 5.867 s
% 215.56/34.95 % (3374011)Peak memory usage: 791 MB
% 215.56/34.95 % (3374011)Instructions burned: 6067 (million)
% 215.56/34.95 % (3374011)------------------------------
% 215.56/34.95 % (3374011)------------------------------
% 215.56/34.95 % (3374067)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1709331524:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2777 on theBenchmark for (2777ds/2479Mi)
% 215.56/34.95 % (3373946)Instruction limit reached!
% 215.56/34.95 % (3373946)------------------------------
% 215.56/34.95 % (3373946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.56/34.95 % (3373946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.56/34.95 % (3373946)CaDiCaL version: 2.1.3
% 215.56/34.95 % (3373946)Termination reason: Instruction limit
% 215.56/34.95 % (3373946)Termination phase: Saturation
% 215.56/34.95 % (3373946)Time elapsed: 12.144 s
% 215.56/34.95 % (3373946)Peak memory usage: 1262 MB
% 215.56/34.95 % (3373946)Instructions burned: 12111 (million)
% 215.56/34.95 % (3374067)Refutation not found, incomplete strategy
% 215.56/34.95 % (3374067)------------------------------
% 215.56/34.95 % (3374067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.56/34.95 % (3374067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.56/34.95 % (3374067)CaDiCaL version: 2.1.3
% 215.56/34.95 % (3374067)Termination reason: Refutation not found, incomplete strategy
% 215.56/34.95 % (3374067)Time elapsed: 1.691 s
% 215.56/34.95 % (3374067)Peak memory usage: 351 MB
% 215.56/34.95 % (3374067)Instructions burned: 2423 (million)
% 215.56/34.95 % (3374075)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=4083589849:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2756 on theBenchmark for (2756ds/440Mi)
% 215.56/34.95 % (3374067)------------------------------
% 215.56/34.95 % (3374067)------------------------------
% 215.56/34.95 % (3374075)Instruction limit reached!
% 215.56/34.95 % (3374075)------------------------------
% 215.56/34.95 % (3374075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.56/34.95 % (3374075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.56/34.95 % (3374075)CaDiCaL version: 2.1.3
% 215.56/34.95 % (3374075)Termination reason: Instruction limit
% 215.56/34.95 % (3374075)Termination phase: Property scanning
% 215.56/34.95 % (3374075)Time elapsed: 0.419 s
% 215.56/34.95 % (3374075)Peak memory usage: 270 MB
% 215.56/34.95 % (3374075)Instructions burned: 441 (million)
% 215.56/34.95 % (3374079)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=4007425444:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2752 on theBenchmark for (2752ds/11145Mi)
% 215.56/34.95 % (3374081)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=3117629937:cts=off:i=3034:av=off:er=known:fsd=on_2749 on theBenchmark for (2749ds/3034Mi)
% 215.56/34.95 % (3373835)Instruction limit reached!
% 215.56/34.95 % (3373835)------------------------------
% 215.56/34.95 % (3373835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.56/34.95 % (3373835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.56/34.95 % (3373835)CaDiCaL version: 2.1.3
% 215.56/34.95 % (3373835)Termination reason: Instruction limit
% 215.56/34.95 % (3373835)Termination phase: Saturation
% 215.56/34.95 % (3373835)Time elapsed: 19.016 s
% 215.56/34.95 % (3373835)Peak memory usage: 1710 MB
% 215.56/34.95 % (3373835)Instructions burned: 14156 (million)
% 215.56/34.95 % (3374085)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=1913779682:st=2:s2a=on:i=524:s2at=2:ss=axioms_2734 on theBenchmark for (2734ds/524Mi)
% 215.56/34.95 % (3374024)Instruction limit reached!
% 215.56/34.95 % (3374024)------------------------------
% 215.56/34.95 % (3374024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.56/34.95 % (3374024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.56/34.95 % (3374024)CaDiCaL version: 2.1.3
% 215.56/34.95 % (3374024)Termination reason: Instruction limit
% 215.56/34.95 % (3374024)Termination phase: Saturation
% 215.56/34.95 % (3374024)Time elapsed: 10.270 s
% 215.56/34.95 % (3374024)Peak memory usage: 890 MB
% 215.56/34.95 % (3374024)Instructions burned: 9927 (million)
% 215.56/34.95 % (3374085)Instruction limit reached!
% 215.56/34.95 % (3374085)------------------------------
% 215.56/34.95 % (3374085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.56/34.95 % (3374085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.47/36.84 % (3374085)CaDiCaL version: 2.1.3
% 229.47/36.84 % (3374085)Termination reason: Instruction limit
% 229.47/36.84 % (3374085)Termination phase: SInE selection
% 229.47/36.84 % (3374085)Time elapsed: 0.357 s
% 229.47/36.84 % (3374085)Peak memory usage: 272 MB
% 229.47/36.84 % (3374085)Instructions burned: 524 (million)
% 229.47/36.84 % (3374087)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1936727153:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2727 on theBenchmark for (2727ds/1016Mi)
% 229.47/36.84 % (3374088)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=4091106217:i=14123:bd=preordered:ins=4_2727 on theBenchmark for (2727ds/14123Mi)
% 229.47/36.84 % (3374087)Instruction limit reached!
% 229.47/36.84 % (3374087)------------------------------
% 229.47/36.84 % (3374087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 229.47/36.84 % (3374087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 229.47/36.84 % (3374087)CaDiCaL version: 2.1.3
% 229.47/36.84 % (3374087)Termination reason: Instruction limit
% 229.47/36.84 % (3374087)Termination phase: Unused predicate definition removal
% 229.47/36.84 % (3374087)Time elapsed: 0.690 s
% 229.47/36.84 % (3374087)Peak memory usage: 309 MB
% 229.47/36.84 % (3374087)Instructions burned: 1016 (million)
% 229.47/36.84 [W927 11:43:52.420219412 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420270715 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420342489 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420362126 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420404600 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420422750 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420466787 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420484630 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420526107 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.
% 229.47/36.84 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 229.47/36.84 [W927 11:43:52.420543837 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:43:52.420585678 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:43:52.420602441 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 % (3374081)Instruction limit reached!
% 187.89/37.20 % (3374081)------------------------------
% 187.89/37.20 % (3374081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374081)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374081)Termination reason: Instruction limit
% 187.89/37.20 % (3374081)Termination phase: Preprocessing 3
% 187.89/37.20 % (3374081)Time elapsed: 3.0000 s
% 187.89/37.20 % (3374081)Peak memory usage: 355 MB
% 187.89/37.20 % (3374081)Instructions burned: 3035 (million)
% 187.89/37.20 % (3374096)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3882560808:i=5781:kws=precedence:bd=all:rawr=on_2718 on theBenchmark for (2718ds/5781Mi)
% 187.89/37.20 % (3374099)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=3250582815:i=2448:gtgl=5:bd=preordered:gtg=all_2715 on theBenchmark for (2715ds/2448Mi)
% 187.89/37.20 % (3374099)Instruction limit reached!
% 187.89/37.20 % (3374099)------------------------------
% 187.89/37.20 % (3374099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374099)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374099)Termination reason: Instruction limit
% 187.89/37.20 % (3374099)Termination phase: Property scanning
% 187.89/37.20 % (3374099)Time elapsed: 1.643 s
% 187.89/37.20 % (3374099)Peak memory usage: 270 MB
% 187.89/37.20 % (3374099)Instructions burned: 2449 (million)
% 187.89/37.20 % (3374109)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3730249710:i=3223:kws=precedence:fgj=on:av=off_2695 on theBenchmark for (2695ds/3223Mi)
% 187.89/37.20 % (3374079)Refutation not found, incomplete strategy
% 187.89/37.20 % (3374079)------------------------------
% 187.89/37.20 % (3374079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374079)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374079)Termination reason: Refutation not found, incomplete strategy
% 187.89/37.20 % (3374079)Time elapsed: 7.226 s
% 187.89/37.20 % (3374079)Peak memory usage: 475 MB
% 187.89/37.20 % (3374079)Instructions burned: 7263 (million)
% 187.89/37.20 % (3374079)------------------------------
% 187.89/37.20 % (3374079)------------------------------
% 187.89/37.20 % (3374116)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=4080323959:st=5.6:i=2033:sd=3:ss=axioms_2671 on theBenchmark for (2671ds/2033Mi)
% 187.89/37.20 % (3374109)Instruction limit reached!
% 187.89/37.20 % (3374109)------------------------------
% 187.89/37.20 % (3374109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374109)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374109)Termination reason: Instruction limit
% 187.89/37.20 % (3374109)Termination phase: Preprocessing 3
% 187.89/37.20 % (3374109)Time elapsed: 2.790 s
% 187.89/37.20 % (3374109)Peak memory usage: 366 MB
% 187.89/37.20 % (3374109)Instructions burned: 3224 (million)
% 187.89/37.20 % (3374118)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=1227767928:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2665 on theBenchmark for (2665ds/2055Mi)
% 187.89/37.20 % (3374116)Instruction limit reached!
% 187.89/37.20 % (3374116)------------------------------
% 187.89/37.20 % (3374116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374116)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374116)Termination reason: Instruction limit
% 187.89/37.20 % (3374116)Termination phase: SInE selection
% 187.89/37.20 % (3374116)Time elapsed: 0.777 s
% 187.89/37.20 % (3374116)Peak memory usage: 276 MB
% 187.89/37.20 % (3374116)Instructions burned: 2036 (million)
% 187.89/37.20 % (3374120)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=536361171:i=21611:sd=3:ss=axioms_2660 on theBenchmark for (2660ds/21611Mi)
% 187.89/37.20 % (3374096)Instruction limit reached!
% 187.89/37.20 % (3374096)------------------------------
% 187.89/37.20 % (3374096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374096)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374096)Termination reason: Instruction limit
% 187.89/37.20 % (3374096)Termination phase: Property scanning
% 187.89/37.20 % (3374096)Time elapsed: 5.928 s
% 187.89/37.20 % (3374096)Peak memory usage: 536 MB
% 187.89/37.20 % (3374096)Instructions burned: 5782 (million)
% 187.89/37.20 % (3374118)Instruction limit reached!
% 187.89/37.20 % (3374118)------------------------------
% 187.89/37.20 % (3374118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374118)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374118)Termination reason: Instruction limit
% 187.89/37.20 % (3374118)Termination phase: SInE selection
% 187.89/37.20 % (3374118)Time elapsed: 0.838 s
% 187.89/37.20 % (3374118)Peak memory usage: 277 MB
% 187.89/37.20 % (3374118)Instructions burned: 2055 (million)
% 187.89/37.20 % (3374122)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3863850789:i=4835:sd=13:ss=axioms:sgt=23_2655 on theBenchmark for (2655ds/4835Mi)
% 187.89/37.20 % (3374123)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=4152351743:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2655 on theBenchmark for (2655ds/797Mi)
% 187.89/37.20 % (3374123)Instruction limit reached!
% 187.89/37.20 % (3374123)------------------------------
% 187.89/37.20 % (3374123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.89/37.20 % (3374123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.89/37.20 % (3374123)CaDiCaL version: 2.1.3
% 187.89/37.20 % (3374123)Termination reason: Instruction limit
% 187.89/37.20 % (3374123)Termination phase: SInE selection
% 187.89/37.20 % (3374123)Time elapsed: 0.314 s
% 187.89/37.20 % (3374123)Peak memory usage: 274 MB
% 187.89/37.20 % (3374123)Instructions burned: 799 (million)
% 187.89/37.20 % (3374172)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=265203668:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2650 on theBenchmark for (2650ds/2326Mi)
% 187.89/37.20 % (3374122)First to succeed.
% 187.89/37.20 % (3374122)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3373659"
% 187.89/37.20 [W927 11:44:00.097450852 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097489293 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097544290 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097557520 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097587500 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097598747 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097627767 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097638041 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097663014 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097673147 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097699091 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 [W927 11:44:00.097709574 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.
% 187.89/37.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 187.89/37.20 % (3374122)Refutation found. Thanks to Tanya!
% 187.89/37.20 % SZS status Theorem for theBenchmark
% 187.89/37.20 % SZS output start Proof for theBenchmark
% See solution above
% 231.70/37.57 % (3374122)------------------------------
% 231.70/37.57 % (3374122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 231.70/37.57 % (3374122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 231.70/37.57 % (3374122)CaDiCaL version: 2.1.3
% 231.70/37.57 % (3374122)Termination reason: Refutation
% 231.70/37.57 % (3374122)Time elapsed: 0.884 s
% 231.70/37.57 % (3374122)Peak memory usage: 355 MB
% 231.70/37.57 % (3374122)Instructions burned: 1544 (million)
% 231.70/37.57 % (3374122)------------------------------
% 231.70/37.57 % (3374122)------------------------------
% 231.70/37.57 % (3373659)Success in time 36.215 s
% 231.70/37.57 % Vampire exiting
%------------------------------------------------------------------------------