%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HWV052-1.002.002 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n010.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:35:08 AM UTC 2026
% Result : Unsatisfiable 65.13s 10.08s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 44
% Syntax : Number of formulae : 460 ( 33 unt; 32 def)
% Number of atoms : 1481 ( 561 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 1518 ( 497 ~; 989 |; 0 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 33 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-4 aty)
% Number of variables : 217 ( 0 sgn 217 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( X0 = o
| X0 = i ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bit_domain) ).
fof(f2,plain,
! [X0] :
( i = X0
| o = X0 ),
inference(reorient_equations,[],[f1]) ).
fof(f3,axiom,
! [X0] : inv(X0) != X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bit_inverse) ).
fof(f4,axiom,
! [X0,X1] : unpack1(X0,X1,pack1(X0,X1),pack2(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack1) ).
fof(f5,axiom,
! [X0,X1] : unpack1(inv(X0),X1,pack1(X0,X1),pack2(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack1_01) ).
fof(f6,axiom,
! [X0,X1] : unpack1(X0,inv(X1),pack1(X0,X1),pack2(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack1_02) ).
fof(f7,axiom,
! [X0,X1] : unpack1(X0,X1,inv(pack1(X0,X1)),pack2(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack1_03) ).
fof(f8,axiom,
! [X0,X1] : unpack1(X0,X1,pack1(X0,X1),inv(pack2(X0,X1))) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack1_04) ).
fof(f9,axiom,
! [X0,X1] : unpack2(X0,X1,pack1(X0,X1),pack2(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack2) ).
fof(f10,axiom,
! [X0,X1] : unpack2(inv(X0),X1,pack1(X0,X1),pack2(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack2_05) ).
fof(f11,axiom,
! [X0,X1] : unpack2(X0,inv(X1),pack1(X0,X1),pack2(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack2_06) ).
fof(f12,axiom,
! [X0,X1] : unpack2(X0,X1,inv(pack1(X0,X1)),pack2(X0,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack2_07) ).
fof(f13,axiom,
! [X0,X1] : unpack2(X0,X1,pack1(X0,X1),inv(pack2(X0,X1))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unpack2_08) ).
fof(f14,plain,
! [X0,X1] :
( X0 = X1
| o = X1
| o = X0 ),
inference(superposition,[],[f2,f2]) ).
fof(f15,plain,
! [X0] :
( i != X0
| o = inv(X0) ),
inference(superposition,[],[f3,f2]) ).
fof(f16,plain,
! [X0,X1] :
( unpack2(X0,i,pack1(X0,X1),pack2(X0,X1)) = X1
| o = inv(X1) ),
inference(superposition,[],[f11,f2]) ).
fof(f18,plain,
! [X0,X1] :
( unpack2(X0,X1,i,pack2(X0,X1)) = X1
| o = inv(pack1(X0,X1)) ),
inference(superposition,[],[f12,f2]) ).
fof(f19,plain,
! [X0,X1] :
( unpack2(X0,X1,inv(i),pack2(X0,X1)) = X1
| o = pack1(X0,X1) ),
inference(superposition,[],[f12,f2]) ).
fof(f20,plain,
! [X0,X1] :
( unpack2(X0,X1,i,inv(pack2(X0,X1))) = X1
| o = pack1(X0,X1) ),
inference(superposition,[],[f13,f2]) ).
fof(f22,plain,
! [X0,X1] :
( unpack2(X0,X1,i,pack2(X0,X1)) = X1
| o = pack1(X0,X1) ),
inference(superposition,[],[f9,f2]) ).
fof(f24,plain,
! [X0,X1] :
( unpack2(X0,X1,inv(pack1(X0,X1)),i) = X1
| o = pack2(X0,X1) ),
inference(superposition,[],[f12,f2]) ).
fof(f26,plain,
! [X0,X1] :
( unpack1(X0,X1,pack1(X0,X1),i) = X0
| o = pack2(X0,X1) ),
inference(superposition,[],[f4,f2]) ).
fof(f27,plain,
! [X0,X1] :
( unpack2(X0,X1,pack1(X0,X1),i) = X1
| o = pack2(X0,X1) ),
inference(superposition,[],[f9,f2]) ).
fof(f28,plain,
! [X0,X1] :
( unpack2(X0,inv(X1),pack1(X0,X1),i) = X1
| o = pack2(X0,X1) ),
inference(superposition,[],[f11,f2]) ).
fof(f34,plain,
! [X0] :
( o != i
| o = X0 ),
inference(equality_factoring,[],[f2]) ).
fof(f36,definition,
( spl0_1
<=> ! [X0] : o = X0 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f37,plain,
( ! [X0] : o = X0
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f36]) ).
fof(f39,definition,
( spl0_2
<=> o = i ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f41,plain,
( o != i
| spl0_2 ),
inference(avatar_component_clause,[],[f39]) ).
fof(f42,plain,
( spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f34,f39,f36]) ).
fof(f48,plain,
! [X0,X1] :
( unpack1(X0,X1,i,inv(pack2(X0,X1))) = X0
| o = pack1(X0,X1) ),
inference(superposition,[],[f8,f2]) ).
fof(f49,plain,
! [X0,X1] :
( unpack1(X0,X1,pack1(X0,X1),inv(i)) = X0
| o = pack2(X0,X1) ),
inference(superposition,[],[f8,f2]) ).
fof(f50,plain,
! [X0,X1] :
( unpack1(X0,X1,pack1(X0,X1),i) = X0
| o = inv(pack2(X0,X1)) ),
inference(superposition,[],[f8,f2]) ).
fof(f53,plain,
! [X0,X1] :
( unpack1(X0,X1,inv(i),pack2(X0,X1)) = X0
| o = pack1(X0,X1) ),
inference(superposition,[],[f7,f2]) ).
fof(f55,plain,
! [X0,X1] :
( unpack1(X0,X1,inv(pack1(X0,X1)),i) = X0
| o = pack2(X0,X1) ),
inference(superposition,[],[f7,f2]) ).
fof(f59,plain,
! [X0,X1] :
( unpack1(X0,inv(X1),i,pack2(X0,X1)) = X0
| o = pack1(X0,X1) ),
inference(superposition,[],[f6,f2]) ).
fof(f60,plain,
! [X0,X1] :
( unpack1(X0,inv(X1),pack1(X0,X1),i) = X0
| o = pack2(X0,X1) ),
inference(superposition,[],[f6,f2]) ).
fof(f63,plain,
! [X0,X1] :
( unpack1(i,X1,pack1(X0,X1),pack2(X0,X1)) = X0
| o = inv(X0) ),
inference(superposition,[],[f5,f2]) ).
fof(f64,plain,
! [X0,X1] :
( unpack1(inv(X0),X1,i,pack2(X0,X1)) = X0
| o = pack1(X0,X1) ),
inference(superposition,[],[f5,f2]) ).
fof(f65,plain,
! [X0,X1] :
( unpack1(inv(X0),X1,pack1(X0,X1),i) = X0
| o = pack2(X0,X1) ),
inference(superposition,[],[f5,f2]) ).
fof(f70,plain,
! [X0,X1] :
( unpack2(X0,i,pack1(X0,X1),i) = X1
| o = inv(X1)
| o = pack2(X0,X1) ),
inference(superposition,[],[f16,f2]) ).
fof(f71,plain,
! [X0,X1] :
( i = X1
| o = inv(X1)
| o = unpack2(X0,i,pack1(X0,X1),pack2(X0,X1)) ),
inference(superposition,[],[f16,f2]) ).
fof(f72,plain,
! [X0,X1] :
( o = unpack2(X0,i,pack1(X0,X1),pack2(X0,X1))
| o = inv(X1) ),
inference(forward_subsumption_resolution,[],[f71,f15]) ).
fof(f76,plain,
! [X0,X1] :
( o = unpack2(X0,X1,inv(pack1(X0,X1)),i)
| o = pack2(X0,X1)
| i = X1 ),
inference(superposition,[],[f24,f2]) ).
fof(f78,plain,
! [X0,X1] :
( unpack2(X0,inv(X1),i,i) = X1
| o = pack2(X0,X1)
| o = pack1(X0,X1) ),
inference(superposition,[],[f28,f2]) ).
fof(f85,plain,
! [X0,X1] :
( o = unpack2(X0,X1,i,inv(pack2(X0,X1)))
| o = pack1(X0,X1)
| i = X1 ),
inference(superposition,[],[f20,f2]) ).
fof(f90,plain,
! [X0,X1] :
( unpack2(X0,X1,i,i) = X1
| o = pack2(X0,X1)
| o = pack1(X0,X1) ),
inference(superposition,[],[f27,f2]) ).
fof(f94,plain,
! [X0,X1] :
( unpack1(X0,X1,i,i) = X0
| o = pack2(X0,X1)
| o = inv(pack1(X0,X1)) ),
inference(superposition,[],[f55,f2]) ).
fof(f102,plain,
! [X0,X1] :
( unpack1(X0,X1,i,i) = X0
| o = pack1(X0,X1)
| o = inv(pack2(X0,X1)) ),
inference(superposition,[],[f48,f2]) ).
fof(f105,plain,
! [X0,X1] :
( o = unpack2(X0,i,i,pack2(X0,X1))
| o = inv(X1)
| o = pack1(X0,X1) ),
inference(superposition,[],[f72,f2]) ).
fof(f111,plain,
( o = i
| o = inv(i) ),
inference(superposition,[],[f9,f72]) ).
fof(f114,plain,
( o = inv(i)
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f111,f41]) ).
fof(f119,plain,
( ! [X0] : i = unpack1(o,X0,pack1(i,X0),pack2(i,X0))
| spl0_2 ),
inference(superposition,[],[f5,f114]) ).
fof(f122,plain,
( ! [X0] : i = unpack2(X0,o,pack1(X0,i),pack2(X0,i))
| spl0_2 ),
inference(superposition,[],[f11,f114]) ).
fof(f138,plain,
! [X0,X1] :
( unpack1(X0,X1,i,i) = X0
| o = pack2(X0,X1)
| o = pack1(X0,X1) ),
inference(superposition,[],[f26,f2]) ).
fof(f148,plain,
! [X0,X1] :
( unpack2(inv(X0),X1,pack1(X0,X1),i) = X1
| o = pack2(X0,X1) ),
inference(superposition,[],[f10,f2]) ).
fof(f153,plain,
! [X0,X1] :
( unpack1(i,X1,i,pack2(X0,X1)) = X0
| o = pack1(X0,X1)
| o = inv(X0) ),
inference(superposition,[],[f64,f2]) ).
fof(f155,plain,
! [X0,X1] :
( unpack1(inv(X0),X1,i,i) = X0
| o = pack1(X0,X1)
| o = pack2(X0,X1) ),
inference(superposition,[],[f64,f2]) ).
fof(f162,plain,
! [X0,X1] :
( o = unpack1(inv(X0),X1,pack1(X0,X1),i)
| o = pack2(X0,X1)
| i = X0 ),
inference(superposition,[],[f65,f2]) ).
fof(f187,plain,
! [X0,X1] :
( i = X1
| o = inv(X1)
| o = unpack1(i,X0,pack1(X1,X0),pack2(X1,X0)) ),
inference(superposition,[],[f63,f2]) ).
fof(f188,plain,
! [X0,X1] :
( o = unpack1(i,X0,pack1(X1,X0),pack2(X1,X0))
| o = inv(X1) ),
inference(forward_subsumption_resolution,[],[f187,f15]) ).
fof(f190,plain,
! [X0,X1] :
( o = unpack1(i,X0,i,pack2(X1,X0))
| o = inv(X1)
| o = pack1(X1,X0) ),
inference(superposition,[],[f188,f2]) ).
fof(f229,plain,
! [X0,X1] :
( unpack1(X0,inv(X1),i,i) = X0
| o = pack2(X0,X1)
| o = pack1(X0,X1) ),
inference(superposition,[],[f60,f2]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( X0 = X1
| X1 = X2
| X0 = X2
| X0 = X3
| o = X3 ),
inference(superposition,[],[f14,f14]) ).
fof(f416,plain,
! [X0,X1] :
( X0 != X1
| o = inv(X1)
| o = X0 ),
inference(superposition,[],[f3,f14]) ).
fof(f936,plain,
! [X0,X1] :
( unpack2(i,X1,pack1(X0,X1),i) = X1
| o = pack2(X0,X1)
| o = inv(X0) ),
inference(superposition,[],[f148,f2]) ).
fof(f991,plain,
! [X0,X1] :
( o = unpack2(X0,X1,i,i)
| o = pack2(X0,X1)
| o = pack1(X0,X1)
| i = X1 ),
inference(superposition,[],[f90,f2]) ).
fof(f1000,plain,
! [X0,X1] :
( unpack2(X0,i,i,i) = X1
| o = pack2(X0,X1)
| o = pack1(X0,X1)
| o = inv(X1) ),
inference(superposition,[],[f78,f2]) ).
fof(f1023,plain,
! [X0,X1] :
( unpack1(i,X1,i,i) = X0
| o = pack2(X0,X1)
| o = pack1(X0,X1)
| o = inv(X0) ),
inference(superposition,[],[f155,f2]) ).
fof(f1058,plain,
! [X0,X1] :
( unpack1(X0,i,i,i) = X0
| o = pack2(X0,X1)
| o = pack1(X0,X1)
| o = inv(X1) ),
inference(superposition,[],[f229,f2]) ).
fof(f1131,plain,
! [X0,X1] :
( o = unpack2(X0,X1,i,i)
| o = pack2(X0,X1)
| i = X1
| o = inv(pack1(X0,X1)) ),
inference(superposition,[],[f76,f2]) ).
fof(f2800,definition,
( spl0_3
<=> i = unpack1(i,i,i,i) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f2801,plain,
( i != unpack1(i,i,i,i)
| spl0_3 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f2802,plain,
( i = unpack1(i,i,i,i)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f2800]) ).
fof(f4726,plain,
( ! [X2,X0,X1] :
( o = inv(X0)
| i = X1
| X0 = X1
| X0 = X2
| o = X2 )
| spl0_2 ),
inference(superposition,[],[f114,f241]) ).
fof(f8247,plain,
! [X2,X0,X1] :
( X1 != X1
| X1 = X2
| X0 = X2
| X0 = X1
| o = X0 ),
inference(equality_factoring,[],[f241]) ).
fof(f8261,plain,
! [X2,X0,X1] :
( o != X1
| X1 = X2
| X0 = X2
| X0 = X1
| X0 = X1 ),
inference(equality_factoring,[],[f241]) ).
fof(f8263,plain,
! [X2,X0,X1] :
( o != X1
| X1 = X2
| X0 = X2
| X0 = X1 ),
inference(duplicate_literal_removal,[],[f8261]) ).
fof(f8268,plain,
! [X2,X0,X1] :
( X1 = X2
| X0 = X2
| X0 = X1
| o = X0 ),
inference(trivial_inequality_removal,[],[f8247]) ).
fof(f8369,plain,
! [X2,X0,X1] :
( X1 = X2
| X0 = X2
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f8268,f8263]) ).
fof(f9484,plain,
( ! [X2,X0,X1] :
( o = inv(X0)
| i = X1
| X0 = X1
| o = X2 )
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f4726,f416]) ).
fof(f9566,definition,
( spl0_165
<=> ! [X0,X1] :
( o = inv(X0)
| i = X1
| X0 = X1 ) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f9567,plain,
( ! [X0,X1] :
( o = inv(X0)
| i = X1
| X0 = X1 )
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f9566]) ).
fof(f9603,plain,
( spl0_1
| spl0_165
| spl0_2 ),
inference(avatar_split_clause,[],[f9484,f39,f9566,f36]) ).
fof(f12047,plain,
! [X2,X0,X1] :
( X0 != X1
| inv(X1) = X2
| X0 = X2 ),
inference(superposition,[],[f3,f8369]) ).
fof(f13781,plain,
( ! [X0] : o != X0
| ~ spl0_1 ),
inference(superposition,[],[f3,f37]) ).
fof(f14063,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f13781,f37]) ).
fof(f14064,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f14063]) ).
fof(f15100,plain,
! [X0,X1] :
( inv(X0) = X1
| X0 = X1 ),
inference(equality_resolution,[],[f12047]) ).
fof(f15200,plain,
! [X0,X1] :
( inv(X0) != X1
| inv(X1) = X0 ),
inference(superposition,[],[f3,f15100]) ).
fof(f15609,plain,
! [X0] : inv(inv(X0)) = X0,
inference(equality_resolution,[],[f15200]) ).
fof(f15610,plain,
( i = inv(o)
| spl0_2 ),
inference(superposition,[],[f15609,f114]) ).
fof(f22080,plain,
( ! [X0] :
( i = X0
| o = pack2(X0,i)
| o = pack1(X0,i)
| o = inv(X0) )
| ~ spl0_3 ),
inference(superposition,[],[f2802,f1023]) ).
fof(f22229,plain,
( ! [X0] :
( o = pack2(X0,i)
| o = pack1(X0,i)
| o = inv(X0) )
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f22080,f15]) ).
fof(f22255,definition,
( spl0_179
<=> ! [X0] :
( o = pack2(X0,i)
| o = inv(X0)
| o = pack1(X0,i) ) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f22256,plain,
( ! [X0] :
( o = pack2(X0,i)
| o = inv(X0)
| o = pack1(X0,i) )
| ~ spl0_179 ),
inference(avatar_component_clause,[],[f22255]) ).
fof(f22258,definition,
( spl0_180
<=> ! [X1] :
( o = pack2(i,X1)
| o = inv(X1)
| o = pack1(i,X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f22259,plain,
( ! [X1] :
( o = pack2(i,X1)
| o = inv(X1)
| o = pack1(i,X1) )
| ~ spl0_180 ),
inference(avatar_component_clause,[],[f22258]) ).
fof(f22261,plain,
( spl0_179
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f22229,f2800,f22255]) ).
fof(f22363,plain,
( ! [X0] :
( o = unpack1(i,i,i,o)
| o = inv(X0)
| o = pack1(X0,i)
| o = inv(X0)
| o = pack1(X0,i) )
| ~ spl0_179 ),
inference(superposition,[],[f190,f22256]) ).
fof(f22389,plain,
( ! [X0] :
( o = unpack1(i,i,i,o)
| o = inv(X0)
| o = pack1(X0,i) )
| ~ spl0_179 ),
inference(duplicate_literal_removal,[],[f22363]) ).
fof(f22425,definition,
( spl0_182
<=> ! [X0] :
( o = pack1(X0,i)
| o = inv(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f22426,plain,
( ! [X0] :
( o = pack1(X0,i)
| o = inv(X0) )
| ~ spl0_182 ),
inference(avatar_component_clause,[],[f22425]) ).
fof(f22428,definition,
( spl0_183
<=> i = unpack2(i,i,i,o) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f22429,plain,
( i != unpack2(i,i,i,o)
| spl0_183 ),
inference(avatar_component_clause,[],[f22428]) ).
fof(f22430,plain,
( i = unpack2(i,i,i,o)
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f22428]) ).
fof(f22434,definition,
( spl0_184
<=> o = unpack1(i,i,i,o) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f22436,plain,
( o = unpack1(i,i,i,o)
| ~ spl0_184 ),
inference(avatar_component_clause,[],[f22434]) ).
fof(f22437,plain,
( spl0_182
| spl0_184
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f22389,f22255,f22434,f22425]) ).
fof(f22551,plain,
( ! [X0] :
( o = unpack2(i,i,i,o)
| o = inv(X0)
| o = pack1(i,X0)
| o = inv(X0)
| o = pack1(i,X0) )
| ~ spl0_180 ),
inference(superposition,[],[f105,f22259]) ).
fof(f22592,plain,
( ! [X0] :
( o = unpack2(i,i,i,o)
| o = inv(X0)
| o = pack1(i,X0) )
| ~ spl0_180 ),
inference(duplicate_literal_removal,[],[f22551]) ).
fof(f22624,definition,
( spl0_185
<=> ! [X0] :
( o = inv(X0)
| o = pack1(i,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_185])],[avatar_definition]) ).
fof(f22625,plain,
( ! [X0] :
( o = pack1(i,X0)
| o = inv(X0) )
| ~ spl0_185 ),
inference(avatar_component_clause,[],[f22624]) ).
fof(f22627,definition,
( spl0_186
<=> i = unpack1(i,i,i,o) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f22628,plain,
( i != unpack1(i,i,i,o)
| spl0_186 ),
inference(avatar_component_clause,[],[f22627]) ).
fof(f22629,plain,
( i = unpack1(i,i,i,o)
| ~ spl0_186 ),
inference(avatar_component_clause,[],[f22627]) ).
fof(f22634,definition,
( spl0_187
<=> o = unpack2(i,i,i,o) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f22636,plain,
( o = unpack2(i,i,i,o)
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f22634]) ).
fof(f22637,plain,
( spl0_185
| spl0_187
| ~ spl0_180 ),
inference(avatar_split_clause,[],[f22592,f22258,f22634,f22624]) ).
fof(f22763,plain,
( ! [X0] :
( i = unpack2(i,i,o,i)
| o = pack2(X0,i)
| o = inv(X0)
| o = inv(X0) )
| ~ spl0_182 ),
inference(superposition,[],[f936,f22426]) ).
fof(f22772,plain,
( ! [X0] :
( i = unpack2(i,i,o,i)
| o = pack2(X0,i)
| o = inv(X0) )
| ~ spl0_182 ),
inference(duplicate_literal_removal,[],[f22763]) ).
fof(f22788,definition,
( spl0_188
<=> ! [X0] :
( o = pack2(X0,i)
| o = inv(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f22789,plain,
( ! [X0] :
( o = pack2(X0,i)
| o = inv(X0) )
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f22788]) ).
fof(f22791,definition,
( spl0_189
<=> i = unpack2(i,i,o,i) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f22793,plain,
( i = unpack2(i,i,o,i)
| ~ spl0_189 ),
inference(avatar_component_clause,[],[f22791]) ).
fof(f22794,plain,
( spl0_188
| spl0_189
| ~ spl0_182 ),
inference(avatar_split_clause,[],[f22772,f22425,f22791,f22788]) ).
fof(f22798,definition,
( spl0_190
<=> o = unpack1(i,i,o,i) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f22799,plain,
( o != unpack1(i,i,o,i)
| spl0_190 ),
inference(avatar_component_clause,[],[f22798]) ).
fof(f22800,plain,
( o = unpack1(i,i,o,i)
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f22798]) ).
fof(f23243,plain,
( ! [X0] :
( i != i
| o = pack2(i,X0)
| o = pack1(i,X0)
| o = inv(X0) )
| spl0_3 ),
inference(superposition,[],[f2801,f1058]) ).
fof(f23246,plain,
( i != i
| o = pack2(i,i)
| o = pack1(i,i)
| spl0_3 ),
inference(superposition,[],[f2801,f138]) ).
fof(f23247,plain,
( i != i
| o = unpack1(i,i,i,i)
| spl0_3 ),
inference(superposition,[],[f2801,f2]) ).
fof(f23281,plain,
( o = unpack1(i,i,i,i)
| spl0_3 ),
inference(trivial_inequality_removal,[],[f23247]) ).
fof(f23282,plain,
( o = pack2(i,i)
| o = pack1(i,i)
| spl0_3 ),
inference(trivial_inequality_removal,[],[f23246]) ).
fof(f23285,plain,
( ! [X0] :
( o = pack2(i,X0)
| o = pack1(i,X0)
| o = inv(X0) )
| spl0_3 ),
inference(trivial_inequality_removal,[],[f23243]) ).
fof(f23292,definition,
( spl0_191
<=> o = pack1(i,i) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f23293,plain,
( o != pack1(i,i)
| spl0_191 ),
inference(avatar_component_clause,[],[f23292]) ).
fof(f23294,plain,
( o = pack1(i,i)
| ~ spl0_191 ),
inference(avatar_component_clause,[],[f23292]) ).
fof(f23296,definition,
( spl0_192
<=> o = pack2(i,i) ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f23297,plain,
( o != pack2(i,i)
| spl0_192 ),
inference(avatar_component_clause,[],[f23296]) ).
fof(f23298,plain,
( o = pack2(i,i)
| ~ spl0_192 ),
inference(avatar_component_clause,[],[f23296]) ).
fof(f23299,plain,
( spl0_191
| spl0_192
| spl0_3 ),
inference(avatar_split_clause,[],[f23282,f2800,f23296,f23292]) ).
fof(f23306,definition,
( spl0_194
<=> o = inv(pack2(i,i)) ),
introduced(definition,[new_symbols(definition,[spl0_194])],[avatar_definition]) ).
fof(f23308,plain,
( o = inv(pack2(i,i))
| ~ spl0_194 ),
inference(avatar_component_clause,[],[f23306]) ).
fof(f23310,plain,
( spl0_180
| spl0_3 ),
inference(avatar_split_clause,[],[f23285,f2800,f22258]) ).
fof(f23484,definition,
( spl0_195
<=> ! [X0] : o = inv(X0) ),
introduced(definition,[new_symbols(definition,[spl0_195])],[avatar_definition]) ).
fof(f23485,plain,
( ! [X0] : o = inv(X0)
| ~ spl0_195 ),
inference(avatar_component_clause,[],[f23484]) ).
fof(f23547,plain,
( i = unpack1(i,i,inv(pack1(i,i)),o)
| ~ spl0_192 ),
inference(superposition,[],[f7,f23298]) ).
fof(f23553,plain,
( i = unpack2(i,i,pack1(i,i),inv(o))
| ~ spl0_192 ),
inference(superposition,[],[f13,f23298]) ).
fof(f23555,plain,
( i = unpack2(i,i,i,o)
| o = inv(pack1(i,i))
| ~ spl0_192 ),
inference(superposition,[],[f18,f23298]) ).
fof(f23597,plain,
( i = unpack2(i,i,pack1(i,i),i)
| spl0_2
| ~ spl0_192 ),
inference(forward_demodulation,[],[f23553,f15610]) ).
fof(f23603,plain,
( i = unpack1(i,i,inv(o),o)
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f23547,f23294]) ).
fof(f23631,plain,
( i = unpack2(i,i,o,i)
| spl0_2
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f23597,f23294]) ).
fof(f23636,plain,
( i = unpack1(i,i,i,o)
| spl0_2
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f23603,f15610]) ).
fof(f23643,plain,
( spl0_189
| spl0_2
| ~ spl0_191
| ~ spl0_192 ),
inference(avatar_split_clause,[],[f23631,f23296,f23292,f39,f22791]) ).
fof(f23644,plain,
( o = i
| spl0_2
| ~ spl0_184
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f23636,f22436]) ).
fof(f23647,plain,
( $false
| spl0_2
| ~ spl0_184
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f23644,f41]) ).
fof(f23648,plain,
( spl0_2
| ~ spl0_184
| ~ spl0_191
| ~ spl0_192 ),
inference(avatar_contradiction_clause,[],[f23647]) ).
fof(f23725,plain,
( i = unpack1(i,i,o,i)
| o = inv(pack2(i,i))
| ~ spl0_191 ),
inference(superposition,[],[f50,f23294]) ).
fof(f23932,plain,
( o = i
| o = pack1(i,i)
| o = inv(pack2(i,i))
| spl0_3 ),
inference(superposition,[],[f23281,f102]) ).
fof(f23933,plain,
( o = i
| o = pack2(i,i)
| o = inv(pack1(i,i))
| spl0_3 ),
inference(superposition,[],[f23281,f94]) ).
fof(f24180,plain,
( ! [X0] :
( unpack2(i,i,o,i) = X0
| o = inv(X0)
| o = pack2(i,X0)
| o = inv(X0) )
| ~ spl0_185 ),
inference(superposition,[],[f70,f22625]) ).
fof(f24217,plain,
( ! [X0] :
( unpack2(i,i,o,i) = X0
| o = inv(X0)
| o = pack2(i,X0) )
| ~ spl0_185 ),
inference(duplicate_literal_removal,[],[f24180]) ).
fof(f24239,plain,
( ! [X0] :
( i = X0
| o = inv(X0)
| o = pack2(i,X0) )
| ~ spl0_185
| ~ spl0_189 ),
inference(forward_demodulation,[],[f24217,f22793]) ).
fof(f24261,plain,
( ! [X0] :
( o = pack2(i,X0)
| o = inv(X0) )
| ~ spl0_185
| ~ spl0_189 ),
inference(forward_subsumption_resolution,[],[f24239,f15]) ).
fof(f25170,plain,
( o = i
| ~ spl0_183
| ~ spl0_187 ),
inference(forward_demodulation,[],[f22636,f22430]) ).
fof(f25171,plain,
( $false
| spl0_2
| ~ spl0_183
| ~ spl0_187 ),
inference(forward_subsumption_resolution,[],[f25170,f41]) ).
fof(f25172,plain,
( spl0_2
| ~ spl0_183
| ~ spl0_187 ),
inference(avatar_contradiction_clause,[],[f25171]) ).
fof(f25173,plain,
( o = inv(pack1(i,i))
| spl0_183
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f23555,f22429]) ).
fof(f25178,plain,
( o = inv(o)
| spl0_183
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f25173,f23294]) ).
fof(f25179,plain,
( $false
| spl0_183
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25178,f3]) ).
fof(f25180,plain,
( spl0_183
| ~ spl0_191
| ~ spl0_192 ),
inference(avatar_contradiction_clause,[],[f25179]) ).
fof(f25194,definition,
( spl0_201
<=> i = unpack1(i,i,o,i) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f25196,plain,
( i = unpack1(i,i,o,i)
| ~ spl0_201 ),
inference(avatar_component_clause,[],[f25194]) ).
fof(f25197,plain,
( spl0_194
| spl0_201
| ~ spl0_191 ),
inference(avatar_split_clause,[],[f23725,f23292,f25194,f23306]) ).
fof(f25210,plain,
( o = pack2(i,i)
| o = inv(pack1(i,i))
| spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f23933,f41]) ).
fof(f25232,plain,
( o = inv(pack1(i,i))
| spl0_2
| spl0_3
| spl0_192 ),
inference(forward_subsumption_resolution,[],[f25210,f23297]) ).
fof(f25236,plain,
( o = inv(o)
| spl0_2
| spl0_3
| ~ spl0_191
| spl0_192 ),
inference(forward_demodulation,[],[f25232,f23294]) ).
fof(f25239,plain,
( $false
| spl0_2
| spl0_3
| ~ spl0_191
| spl0_192 ),
inference(forward_subsumption_resolution,[],[f25236,f3]) ).
fof(f25240,plain,
( spl0_2
| spl0_3
| ~ spl0_191
| spl0_192 ),
inference(avatar_contradiction_clause,[],[f25239]) ).
fof(f25242,plain,
( o = inv(o)
| ~ spl0_192
| ~ spl0_194 ),
inference(forward_demodulation,[],[f23308,f23298]) ).
fof(f25244,plain,
( o = pack1(i,i)
| o = inv(pack2(i,i))
| spl0_2
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f23932,f41]) ).
fof(f25245,plain,
( $false
| ~ spl0_192
| ~ spl0_194 ),
inference(forward_subsumption_resolution,[],[f25242,f3]) ).
fof(f25246,plain,
( ~ spl0_192
| ~ spl0_194 ),
inference(avatar_contradiction_clause,[],[f25245]) ).
fof(f25248,plain,
( o = inv(pack2(i,i))
| spl0_2
| spl0_3
| spl0_191 ),
inference(forward_subsumption_resolution,[],[f25244,f23293]) ).
fof(f25250,plain,
( o = inv(o)
| spl0_2
| spl0_3
| spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f25248,f23298]) ).
fof(f25253,plain,
( $false
| spl0_2
| spl0_3
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25250,f3]) ).
fof(f25254,plain,
( spl0_2
| spl0_3
| spl0_191
| ~ spl0_192 ),
inference(avatar_contradiction_clause,[],[f25253]) ).
fof(f25265,plain,
( ! [X0] : o = X0
| ~ spl0_195 ),
inference(superposition,[],[f23485,f15609]) ).
fof(f25295,plain,
( ! [X0] : o != X0
| ~ spl0_195 ),
inference(superposition,[],[f3,f23485]) ).
fof(f25398,plain,
( $false
| ~ spl0_195 ),
inference(forward_subsumption_resolution,[],[f25265,f25295]) ).
fof(f25399,plain,
~ spl0_195,
inference(avatar_contradiction_clause,[],[f25398]) ).
fof(f25463,plain,
( i = unpack1(i,i,pack1(i,i),o)
| ~ spl0_192 ),
inference(superposition,[],[f4,f23298]) ).
fof(f25475,plain,
( i = unpack2(i,i,inv(i),o)
| o = pack1(i,i)
| ~ spl0_192 ),
inference(superposition,[],[f19,f23298]) ).
fof(f25476,plain,
( i = unpack2(i,i,i,inv(o))
| o = pack1(i,i)
| ~ spl0_192 ),
inference(superposition,[],[f20,f23298]) ).
fof(f25478,plain,
( i = unpack2(i,i,i,o)
| o = pack1(i,i)
| ~ spl0_192 ),
inference(superposition,[],[f22,f23298]) ).
fof(f25481,plain,
( i = unpack1(i,i,inv(i),o)
| o = pack1(i,i)
| ~ spl0_192 ),
inference(superposition,[],[f53,f23298]) ).
fof(f25524,plain,
( i = unpack1(i,i,inv(i),o)
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25481,f23293]) ).
fof(f25527,plain,
( o = pack1(i,i)
| spl0_183
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25478,f22429]) ).
fof(f25528,plain,
( i = unpack2(i,i,i,inv(o))
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25476,f23293]) ).
fof(f25529,plain,
( i = unpack2(i,i,inv(i),o)
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25475,f23293]) ).
fof(f25565,plain,
( i = unpack1(i,i,o,o)
| spl0_2
| spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f25524,f114]) ).
fof(f25568,plain,
( $false
| spl0_183
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f25527,f23293]) ).
fof(f25569,plain,
( spl0_183
| spl0_191
| ~ spl0_192 ),
inference(avatar_contradiction_clause,[],[f25568]) ).
fof(f25570,plain,
( i = unpack2(i,i,i,i)
| spl0_2
| spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f25528,f15610]) ).
fof(f25571,plain,
( i = unpack2(i,i,o,o)
| spl0_2
| spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f25529,f114]) ).
fof(f26016,plain,
( ! [X0] :
( o = unpack1(i,i,o,pack2(X0,i))
| o = inv(X0)
| o = inv(X0) )
| ~ spl0_182 ),
inference(superposition,[],[f188,f22426]) ).
fof(f26033,plain,
( ! [X0] :
( o = unpack1(i,i,o,pack2(X0,i))
| o = inv(X0) )
| ~ spl0_182 ),
inference(duplicate_literal_removal,[],[f26016]) ).
fof(f26426,definition,
( spl0_202
<=> i = pack1(i,i) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f26428,plain,
( i = pack1(i,i)
| ~ spl0_202 ),
inference(avatar_component_clause,[],[f26426]) ).
fof(f26860,plain,
( ! [X0] :
( i = X0
| o = pack2(i,X0)
| o = pack1(i,X0)
| o = inv(X0) )
| spl0_2
| spl0_191
| ~ spl0_192 ),
inference(superposition,[],[f1000,f25570]) ).
fof(f26861,plain,
( ! [X0] :
( o = pack2(i,X0)
| o = pack1(i,X0)
| o = inv(X0) )
| spl0_2
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f26860,f15]) ).
fof(f26888,plain,
( spl0_180
| spl0_2
| spl0_191
| ~ spl0_192 ),
inference(avatar_split_clause,[],[f26861,f23296,f23292,f39,f22258]) ).
fof(f26942,plain,
( ! [X0] :
( o != X0
| o = inv(X0)
| i = pack1(i,i) )
| ~ spl0_165
| spl0_191 ),
inference(superposition,[],[f23293,f9567]) ).
fof(f26960,plain,
( ! [X0] :
( o = inv(X0)
| i = pack1(i,i) )
| ~ spl0_165
| spl0_191 ),
inference(forward_subsumption_resolution,[],[f26942,f15100]) ).
fof(f26965,plain,
( spl0_202
| spl0_195
| ~ spl0_165
| spl0_191 ),
inference(avatar_split_clause,[],[f26960,f23292,f9566,f23484,f26426]) ).
fof(f27041,plain,
( i = unpack2(i,inv(i),i,i)
| o = pack2(i,i)
| ~ spl0_202 ),
inference(superposition,[],[f28,f26428]) ).
fof(f27042,plain,
( i = unpack1(i,i,i,inv(i))
| o = pack2(i,i)
| ~ spl0_202 ),
inference(superposition,[],[f49,f26428]) ).
fof(f27044,plain,
( i = unpack1(i,i,inv(i),i)
| o = pack2(i,i)
| ~ spl0_202 ),
inference(superposition,[],[f55,f26428]) ).
fof(f27195,plain,
( ! [X0] :
( o = unpack2(i,i,o,pack2(i,X0))
| o = inv(X0)
| o = inv(X0) )
| ~ spl0_185 ),
inference(superposition,[],[f72,f22625]) ).
fof(f27230,plain,
( ! [X0] :
( o = unpack2(i,i,o,pack2(i,X0))
| o = inv(X0) )
| ~ spl0_185 ),
inference(duplicate_literal_removal,[],[f27195]) ).
fof(f28001,plain,
( ! [X0] :
( unpack1(i,i,i,o) = X0
| o = pack1(X0,i)
| o = inv(X0)
| o = inv(X0)
| o = pack1(X0,i) )
| ~ spl0_179 ),
inference(superposition,[],[f153,f22256]) ).
fof(f28037,plain,
( ! [X0] :
( unpack1(i,i,i,o) = X0
| o = pack1(X0,i)
| o = inv(X0) )
| ~ spl0_179 ),
inference(duplicate_literal_removal,[],[f28001]) ).
fof(f29165,plain,
( i = unpack1(i,i,i,o)
| ~ spl0_192
| ~ spl0_202 ),
inference(superposition,[],[f25463,f26428]) ).
fof(f32127,plain,
( ! [X0] :
( o = unpack1(i,i,o,o)
| o = inv(X0)
| o = inv(X0) )
| ~ spl0_182
| ~ spl0_188 ),
inference(superposition,[],[f26033,f22789]) ).
fof(f32205,plain,
( ! [X0] :
( o = unpack1(i,i,o,o)
| o = inv(X0) )
| ~ spl0_182
| ~ spl0_188 ),
inference(duplicate_literal_removal,[],[f32127]) ).
fof(f32217,plain,
( ! [X0] :
( o = i
| o = inv(X0) )
| spl0_2
| ~ spl0_182
| ~ spl0_188
| spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f32205,f25565]) ).
fof(f32225,plain,
( ! [X0] : o = inv(X0)
| spl0_2
| ~ spl0_182
| ~ spl0_188
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f32217,f41]) ).
fof(f32226,plain,
( spl0_195
| spl0_2
| ~ spl0_182
| ~ spl0_188
| spl0_191
| ~ spl0_192 ),
inference(avatar_split_clause,[],[f32225,f23296,f23292,f22788,f22425,f39,f23484]) ).
fof(f33324,plain,
( ! [X0] :
( o = unpack2(i,i,o,o)
| o = inv(X0)
| o = inv(X0) )
| ~ spl0_185
| ~ spl0_189 ),
inference(superposition,[],[f27230,f24261]) ).
fof(f33326,plain,
( ! [X0] :
( o = unpack2(i,i,o,i)
| o = inv(X0)
| o = pack2(i,X0) )
| ~ spl0_185 ),
inference(superposition,[],[f27230,f2]) ).
fof(f33398,plain,
( ! [X0] :
( o = unpack2(i,i,o,o)
| o = inv(X0) )
| ~ spl0_185
| ~ spl0_189 ),
inference(duplicate_literal_removal,[],[f33324]) ).
fof(f33415,plain,
( ! [X0] :
( o = i
| o = inv(X0) )
| spl0_2
| ~ spl0_185
| ~ spl0_189
| spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f33398,f25571]) ).
fof(f33423,plain,
( ! [X0] : o = inv(X0)
| spl0_2
| ~ spl0_185
| ~ spl0_189
| spl0_191
| ~ spl0_192 ),
inference(forward_subsumption_resolution,[],[f33415,f41]) ).
fof(f33424,plain,
( spl0_195
| spl0_2
| ~ spl0_185
| ~ spl0_189
| spl0_191
| ~ spl0_192 ),
inference(avatar_split_clause,[],[f33423,f23296,f23292,f22791,f22624,f39,f23484]) ).
fof(f33433,definition,
( spl0_231
<=> ! [X0] :
( o = inv(X0)
| o = pack2(i,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f33434,plain,
( ! [X0] :
( o = pack2(i,X0)
| o = inv(X0) )
| ~ spl0_231 ),
inference(avatar_component_clause,[],[f33433]) ).
fof(f33436,definition,
( spl0_232
<=> o = unpack2(i,i,o,i) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f33438,plain,
( o = unpack2(i,i,o,i)
| ~ spl0_232 ),
inference(avatar_component_clause,[],[f33436]) ).
fof(f33480,plain,
( spl0_231
| spl0_232
| ~ spl0_185 ),
inference(avatar_split_clause,[],[f33326,f22624,f33436,f33433]) ).
fof(f33486,plain,
( ! [X0] :
( i = X0
| o = pack1(X0,i)
| o = inv(X0) )
| ~ spl0_179
| ~ spl0_186 ),
inference(forward_demodulation,[],[f28037,f22629]) ).
fof(f33541,plain,
( ! [X0] :
( o = pack1(X0,i)
| o = inv(X0) )
| ~ spl0_179
| ~ spl0_186 ),
inference(forward_subsumption_resolution,[],[f33486,f15]) ).
fof(f33555,plain,
( spl0_182
| ~ spl0_179
| ~ spl0_186 ),
inference(avatar_split_clause,[],[f33541,f22627,f22255,f22425]) ).
fof(f33567,plain,
( $false
| spl0_186
| ~ spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f29165,f22628]) ).
fof(f33568,plain,
( spl0_186
| ~ spl0_192
| ~ spl0_202 ),
inference(avatar_contradiction_clause,[],[f33567]) ).
fof(f33593,plain,
( i = unpack1(i,i,inv(i),i)
| spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f27044,f23297]) ).
fof(f33594,plain,
( i = unpack1(i,i,i,inv(i))
| spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f27042,f23297]) ).
fof(f33595,plain,
( i = unpack2(i,inv(i),i,i)
| spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f27041,f23297]) ).
fof(f33610,definition,
( spl0_239
<=> i = unpack1(i,i,o,o) ),
introduced(definition,[new_symbols(definition,[spl0_239])],[avatar_definition]) ).
fof(f33611,plain,
( i != unpack1(i,i,o,o)
| spl0_239 ),
inference(avatar_component_clause,[],[f33610]) ).
fof(f33612,plain,
( i = unpack1(i,i,o,o)
| ~ spl0_239 ),
inference(avatar_component_clause,[],[f33610]) ).
fof(f33646,definition,
( spl0_240
<=> o = unpack2(i,i,o,o) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f33647,plain,
( o != unpack2(i,i,o,o)
| spl0_240 ),
inference(avatar_component_clause,[],[f33646]) ).
fof(f33648,plain,
( o = unpack2(i,i,o,o)
| ~ spl0_240 ),
inference(avatar_component_clause,[],[f33646]) ).
fof(f33656,plain,
( i = unpack1(i,i,o,i)
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(forward_demodulation,[],[f33593,f114]) ).
fof(f33657,plain,
( i = unpack1(i,i,i,o)
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(forward_demodulation,[],[f33594,f114]) ).
fof(f33658,plain,
( i = unpack2(i,o,i,i)
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(forward_demodulation,[],[f33595,f114]) ).
fof(f33670,plain,
( o = i
| spl0_2
| ~ spl0_190
| spl0_192
| ~ spl0_202 ),
inference(forward_demodulation,[],[f33656,f22800]) ).
fof(f33671,plain,
( spl0_186
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f33657,f26426,f23296,f39,f22627]) ).
fof(f33672,plain,
( $false
| spl0_2
| ~ spl0_190
| spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f33670,f41]) ).
fof(f33673,plain,
( spl0_2
| ~ spl0_190
| spl0_192
| ~ spl0_202 ),
inference(avatar_contradiction_clause,[],[f33672]) ).
fof(f34417,plain,
( ! [X0] :
( o != X0
| o = inv(X0)
| i = pack2(i,i) )
| ~ spl0_165
| spl0_192 ),
inference(superposition,[],[f23297,f9567]) ).
fof(f34438,plain,
( ! [X0] :
( o = inv(X0)
| i = pack2(i,i) )
| ~ spl0_165
| spl0_192 ),
inference(forward_subsumption_resolution,[],[f34417,f15100]) ).
fof(f34444,definition,
( spl0_241
<=> i = pack2(i,i) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f34446,plain,
( i = pack2(i,i)
| ~ spl0_241 ),
inference(avatar_component_clause,[],[f34444]) ).
fof(f34447,plain,
( spl0_241
| spl0_195
| ~ spl0_165
| spl0_192 ),
inference(avatar_split_clause,[],[f34438,f23296,f9566,f23484,f34444]) ).
fof(f34510,plain,
( i = unpack1(o,i,pack1(i,i),i)
| spl0_2
| ~ spl0_241 ),
inference(superposition,[],[f119,f34446]) ).
fof(f34513,plain,
( i = unpack2(i,o,pack1(i,i),i)
| spl0_2
| ~ spl0_241 ),
inference(superposition,[],[f122,f34446]) ).
fof(f34518,plain,
( i = unpack1(i,i,pack1(i,i),inv(i))
| ~ spl0_241 ),
inference(superposition,[],[f8,f34446]) ).
fof(f34523,plain,
( i = unpack2(i,i,pack1(i,i),inv(i))
| ~ spl0_241 ),
inference(superposition,[],[f13,f34446]) ).
fof(f34573,plain,
( i = unpack2(i,i,pack1(i,i),o)
| spl0_2
| ~ spl0_241 ),
inference(forward_demodulation,[],[f34523,f114]) ).
fof(f34578,plain,
( i = unpack1(i,i,pack1(i,i),o)
| spl0_2
| ~ spl0_241 ),
inference(forward_demodulation,[],[f34518,f114]) ).
fof(f34667,plain,
( o = i
| o = pack2(i,o)
| o = i
| o = inv(pack1(i,o))
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(superposition,[],[f33658,f1131]) ).
fof(f34668,plain,
( o = i
| o = pack2(i,o)
| o = pack1(i,o)
| o = i
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(superposition,[],[f33658,f991]) ).
fof(f34721,plain,
( o = i
| o = pack2(i,o)
| o = pack1(i,o)
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(duplicate_literal_removal,[],[f34668]) ).
fof(f34722,plain,
( o = i
| o = pack2(i,o)
| o = inv(pack1(i,o))
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(duplicate_literal_removal,[],[f34667]) ).
fof(f34760,plain,
( o = pack2(i,o)
| o = pack1(i,o)
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f34721,f41]) ).
fof(f34761,plain,
( o = pack2(i,o)
| o = inv(pack1(i,o))
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(forward_subsumption_resolution,[],[f34722,f41]) ).
fof(f34768,definition,
( spl0_242
<=> o = pack1(i,o) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f34769,plain,
( o != pack1(i,o)
| spl0_242 ),
inference(avatar_component_clause,[],[f34768]) ).
fof(f34770,plain,
( o = pack1(i,o)
| ~ spl0_242 ),
inference(avatar_component_clause,[],[f34768]) ).
fof(f34772,definition,
( spl0_243
<=> o = pack2(i,o) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f34773,plain,
( o != pack2(i,o)
| spl0_243 ),
inference(avatar_component_clause,[],[f34772]) ).
fof(f34774,plain,
( o = pack2(i,o)
| ~ spl0_243 ),
inference(avatar_component_clause,[],[f34772]) ).
fof(f34779,definition,
( spl0_244
<=> o = inv(pack1(i,o)) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f34781,plain,
( o = inv(pack1(i,o))
| ~ spl0_244 ),
inference(avatar_component_clause,[],[f34779]) ).
fof(f34804,plain,
( spl0_242
| spl0_243
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f34760,f26426,f23296,f39,f34772,f34768]) ).
fof(f34805,plain,
( spl0_244
| spl0_243
| spl0_2
| spl0_192
| ~ spl0_202 ),
inference(avatar_split_clause,[],[f34761,f26426,f23296,f39,f34772,f34779]) ).
fof(f34886,plain,
( o = unpack2(i,inv(o),pack1(i,o),o)
| ~ spl0_243 ),
inference(superposition,[],[f11,f34774]) ).
fof(f34954,plain,
( o = unpack2(i,inv(o),o,o)
| ~ spl0_242
| ~ spl0_243 ),
inference(forward_demodulation,[],[f34886,f34770]) ).
fof(f34993,plain,
( o = unpack2(i,i,o,o)
| spl0_2
| ~ spl0_242
| ~ spl0_243 ),
inference(forward_demodulation,[],[f34954,f15610]) ).
fof(f35005,plain,
( spl0_240
| spl0_2
| ~ spl0_242
| ~ spl0_243 ),
inference(avatar_split_clause,[],[f34993,f34772,f34768,f39,f33646]) ).
fof(f35007,plain,
( o = inv(o)
| ~ spl0_242
| ~ spl0_244 ),
inference(forward_demodulation,[],[f34781,f34770]) ).
fof(f35008,plain,
( $false
| ~ spl0_242
| ~ spl0_244 ),
inference(forward_subsumption_resolution,[],[f35007,f3]) ).
fof(f35009,plain,
( ~ spl0_242
| ~ spl0_244 ),
inference(avatar_contradiction_clause,[],[f35008]) ).
fof(f35111,plain,
( o = unpack2(i,o,i,inv(o))
| o = pack1(i,o)
| o = i
| ~ spl0_243 ),
inference(superposition,[],[f85,f34774]) ).
fof(f35525,definition,
( spl0_246
<=> o = pack1(o,i) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f35526,plain,
( o != pack1(o,i)
| spl0_246 ),
inference(avatar_component_clause,[],[f35525]) ).
fof(f35527,plain,
( o = pack1(o,i)
| ~ spl0_246 ),
inference(avatar_component_clause,[],[f35525]) ).
fof(f35529,definition,
( spl0_247
<=> o = pack2(o,i) ),
introduced(definition,[new_symbols(definition,[spl0_247])],[avatar_definition]) ).
fof(f35530,plain,
( o != pack2(o,i)
| spl0_247 ),
inference(avatar_component_clause,[],[f35529]) ).
fof(f35531,plain,
( o = pack2(o,i)
| ~ spl0_247 ),
inference(avatar_component_clause,[],[f35529]) ).
fof(f35637,plain,
( o = unpack1(inv(o),i,pack1(o,i),o)
| ~ spl0_247 ),
inference(superposition,[],[f5,f35531]) ).
fof(f35642,plain,
( i = unpack2(inv(o),i,pack1(o,i),o)
| ~ spl0_247 ),
inference(superposition,[],[f10,f35531]) ).
fof(f35707,plain,
( i = unpack2(inv(o),i,o,o)
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_demodulation,[],[f35642,f35527]) ).
fof(f35712,plain,
( o = unpack1(inv(o),i,o,o)
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_demodulation,[],[f35637,f35527]) ).
fof(f35742,plain,
( i = unpack2(i,i,o,o)
| spl0_2
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_demodulation,[],[f35707,f15610]) ).
fof(f35746,plain,
( o = unpack1(i,i,o,o)
| spl0_2
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_demodulation,[],[f35712,f15610]) ).
fof(f35753,plain,
( o = i
| spl0_2
| ~ spl0_240
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_demodulation,[],[f35742,f33648]) ).
fof(f35755,plain,
( o = i
| spl0_2
| ~ spl0_239
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_demodulation,[],[f35746,f33612]) ).
fof(f35760,plain,
( $false
| spl0_2
| ~ spl0_240
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_subsumption_resolution,[],[f35753,f41]) ).
fof(f35761,plain,
( spl0_2
| ~ spl0_240
| ~ spl0_246
| ~ spl0_247 ),
inference(avatar_contradiction_clause,[],[f35760]) ).
fof(f35764,plain,
( $false
| spl0_2
| ~ spl0_239
| ~ spl0_246
| ~ spl0_247 ),
inference(forward_subsumption_resolution,[],[f35755,f41]) ).
fof(f35765,plain,
( spl0_2
| ~ spl0_239
| ~ spl0_246
| ~ spl0_247 ),
inference(avatar_contradiction_clause,[],[f35764]) ).
fof(f35781,plain,
( o = unpack2(i,o,i,inv(o))
| o = i
| spl0_242
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f35111,f34769]) ).
fof(f35811,plain,
( o = unpack2(i,o,i,inv(o))
| spl0_2
| spl0_242
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f35781,f41]) ).
fof(f35823,plain,
( o = unpack2(i,o,i,i)
| spl0_2
| spl0_242
| ~ spl0_243 ),
inference(forward_demodulation,[],[f35811,f15610]) ).
fof(f35827,plain,
( o = i
| spl0_2
| spl0_192
| ~ spl0_202
| spl0_242
| ~ spl0_243 ),
inference(forward_demodulation,[],[f35823,f33658]) ).
fof(f35834,plain,
( $false
| spl0_2
| spl0_192
| ~ spl0_202
| spl0_242
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f35827,f41]) ).
fof(f35835,plain,
( spl0_2
| spl0_192
| ~ spl0_202
| spl0_242
| ~ spl0_243 ),
inference(avatar_contradiction_clause,[],[f35834]) ).
fof(f35883,plain,
( i = unpack2(i,o,o,i)
| spl0_2
| ~ spl0_191
| ~ spl0_241 ),
inference(forward_demodulation,[],[f34513,f23294]) ).
fof(f35884,plain,
( i = unpack1(o,i,o,i)
| spl0_2
| ~ spl0_191
| ~ spl0_241 ),
inference(forward_demodulation,[],[f34510,f23294]) ).
fof(f35885,plain,
( i = unpack2(i,i,o,o)
| spl0_2
| ~ spl0_191
| ~ spl0_241 ),
inference(forward_demodulation,[],[f34573,f23294]) ).
fof(f35886,plain,
( i = unpack1(i,i,o,o)
| spl0_2
| ~ spl0_191
| ~ spl0_241 ),
inference(forward_demodulation,[],[f34578,f23294]) ).
fof(f35915,plain,
( $false
| spl0_2
| ~ spl0_191
| spl0_239
| ~ spl0_241 ),
inference(forward_subsumption_resolution,[],[f35886,f33611]) ).
fof(f35916,plain,
( spl0_2
| ~ spl0_191
| spl0_239
| ~ spl0_241 ),
inference(avatar_contradiction_clause,[],[f35915]) ).
fof(f35985,plain,
( i = unpack1(i,i,o,pack2(i,i))
| ~ spl0_191 ),
inference(superposition,[],[f4,f23294]) ).
fof(f35990,plain,
( i = unpack2(i,i,o,pack2(i,i))
| ~ spl0_191 ),
inference(superposition,[],[f9,f23294]) ).
fof(f37081,plain,
( ! [X0] :
( o = unpack2(i,i,o,o)
| o = inv(X0)
| o = inv(X0) )
| ~ spl0_185
| ~ spl0_231 ),
inference(superposition,[],[f27230,f33434]) ).
fof(f37153,plain,
( ! [X0] :
( o = unpack2(i,i,o,o)
| o = inv(X0) )
| ~ spl0_185
| ~ spl0_231 ),
inference(duplicate_literal_removal,[],[f37081]) ).
fof(f37166,plain,
( ! [X0] : o = inv(X0)
| ~ spl0_185
| ~ spl0_231
| spl0_240 ),
inference(forward_subsumption_resolution,[],[f37153,f33647]) ).
fof(f37172,plain,
( spl0_195
| ~ spl0_185
| ~ spl0_231
| spl0_240 ),
inference(avatar_split_clause,[],[f37166,f33646,f33433,f22624,f23484]) ).
fof(f37173,plain,
( o = i
| spl0_2
| ~ spl0_191
| ~ spl0_240
| ~ spl0_241 ),
inference(forward_demodulation,[],[f33648,f35885]) ).
fof(f37175,plain,
( $false
| spl0_2
| ~ spl0_191
| ~ spl0_240
| ~ spl0_241 ),
inference(forward_subsumption_resolution,[],[f37173,f41]) ).
fof(f37176,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_240
| ~ spl0_241 ),
inference(avatar_contradiction_clause,[],[f37175]) ).
fof(f37179,plain,
( o = i
| ~ spl0_189
| ~ spl0_232 ),
inference(forward_demodulation,[],[f33438,f22793]) ).
fof(f37182,plain,
( $false
| spl0_2
| ~ spl0_189
| ~ spl0_232 ),
inference(forward_subsumption_resolution,[],[f37179,f41]) ).
fof(f37183,plain,
( spl0_2
| ~ spl0_189
| ~ spl0_232 ),
inference(avatar_contradiction_clause,[],[f37182]) ).
fof(f37270,plain,
( ! [X0] :
( o != X0
| o = inv(X0)
| i = pack1(i,o) )
| ~ spl0_165
| spl0_242 ),
inference(superposition,[],[f34769,f9567]) ).
fof(f37289,plain,
( ! [X0] :
( o = inv(X0)
| i = pack1(i,o) )
| ~ spl0_165
| spl0_242 ),
inference(forward_subsumption_resolution,[],[f37270,f15100]) ).
fof(f37297,definition,
( spl0_251
<=> i = pack1(i,o) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f37299,plain,
( i = pack1(i,o)
| ~ spl0_251 ),
inference(avatar_component_clause,[],[f37297]) ).
fof(f37401,plain,
( o = unpack2(i,o,inv(i),i)
| o = pack2(i,o)
| o = i
| ~ spl0_251 ),
inference(superposition,[],[f76,f37299]) ).
fof(f37523,plain,
( o != o
| o = inv(o)
| ~ spl0_182
| spl0_246 ),
inference(superposition,[],[f35526,f22426]) ).
fof(f37561,plain,
( o = inv(o)
| ~ spl0_182
| spl0_246 ),
inference(trivial_inequality_removal,[],[f37523]) ).
fof(f37566,plain,
( $false
| ~ spl0_182
| spl0_246 ),
inference(forward_subsumption_resolution,[],[f37561,f3]) ).
fof(f37567,plain,
( ~ spl0_182
| spl0_246 ),
inference(avatar_contradiction_clause,[],[f37566]) ).
fof(f37598,plain,
( o = unpack2(i,o,inv(i),i)
| o = i
| spl0_243
| ~ spl0_251 ),
inference(forward_subsumption_resolution,[],[f37401,f34773]) ).
fof(f37643,plain,
( o = unpack2(i,o,inv(i),i)
| spl0_2
| spl0_243
| ~ spl0_251 ),
inference(forward_subsumption_resolution,[],[f37598,f41]) ).
fof(f37660,plain,
( o = unpack2(i,o,o,i)
| spl0_2
| spl0_243
| ~ spl0_251 ),
inference(forward_demodulation,[],[f37643,f114]) ).
fof(f37667,plain,
( o = i
| spl0_2
| ~ spl0_191
| ~ spl0_241
| spl0_243
| ~ spl0_251 ),
inference(forward_demodulation,[],[f37660,f35883]) ).
fof(f37676,plain,
( $false
| spl0_2
| ~ spl0_191
| ~ spl0_241
| spl0_243
| ~ spl0_251 ),
inference(forward_subsumption_resolution,[],[f37667,f41]) ).
fof(f37677,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_241
| spl0_243
| ~ spl0_251 ),
inference(avatar_contradiction_clause,[],[f37676]) ).
fof(f37772,plain,
( i = unpack1(i,inv(o),i,o)
| o = pack1(i,o)
| ~ spl0_243 ),
inference(superposition,[],[f59,f34774]) ).
fof(f37839,plain,
( i = unpack1(i,inv(o),i,o)
| spl0_242
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f37772,f34769]) ).
fof(f37898,plain,
( i = unpack1(i,i,i,o)
| spl0_2
| spl0_242
| ~ spl0_243 ),
inference(forward_demodulation,[],[f37839,f15610]) ).
fof(f37922,plain,
( o = i
| spl0_2
| ~ spl0_184
| spl0_242
| ~ spl0_243 ),
inference(forward_demodulation,[],[f37898,f22436]) ).
fof(f37927,plain,
( $false
| spl0_2
| ~ spl0_184
| spl0_242
| ~ spl0_243 ),
inference(forward_subsumption_resolution,[],[f37922,f41]) ).
fof(f37928,plain,
( spl0_2
| ~ spl0_184
| spl0_242
| ~ spl0_243 ),
inference(avatar_contradiction_clause,[],[f37927]) ).
fof(f38024,plain,
( o = unpack1(o,i,o,i)
| o = pack2(o,i)
| ~ spl0_246 ),
inference(superposition,[],[f26,f35527]) ).
fof(f38048,plain,
( o = unpack1(inv(o),i,o,i)
| o = pack2(o,i)
| o = i
| ~ spl0_246 ),
inference(superposition,[],[f162,f35527]) ).
fof(f38087,plain,
( o = unpack1(inv(o),i,o,i)
| o = i
| ~ spl0_246
| spl0_247 ),
inference(forward_subsumption_resolution,[],[f38048,f35530]) ).
fof(f38104,plain,
( o = unpack1(o,i,o,i)
| ~ spl0_246
| spl0_247 ),
inference(forward_subsumption_resolution,[],[f38024,f35530]) ).
fof(f38141,plain,
( o = unpack1(inv(o),i,o,i)
| spl0_2
| ~ spl0_246
| spl0_247 ),
inference(forward_subsumption_resolution,[],[f38087,f41]) ).
fof(f38153,plain,
( o = i
| spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_246
| spl0_247 ),
inference(forward_demodulation,[],[f38104,f35884]) ).
fof(f38162,plain,
( o = unpack1(i,i,o,i)
| spl0_2
| ~ spl0_246
| spl0_247 ),
inference(forward_demodulation,[],[f38141,f15610]) ).
fof(f38168,plain,
( $false
| spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_246
| spl0_247 ),
inference(forward_subsumption_resolution,[],[f38153,f41]) ).
fof(f38169,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_246
| spl0_247 ),
inference(avatar_contradiction_clause,[],[f38168]) ).
fof(f38170,plain,
( $false
| spl0_2
| spl0_190
| ~ spl0_246
| spl0_247 ),
inference(forward_subsumption_resolution,[],[f38162,f22799]) ).
fof(f38171,plain,
( spl0_2
| spl0_190
| ~ spl0_246
| spl0_247 ),
inference(avatar_contradiction_clause,[],[f38170]) ).
fof(f38262,plain,
( o = unpack2(i,o,o,i)
| o = pack2(i,o)
| ~ spl0_242 ),
inference(superposition,[],[f27,f34770]) ).
fof(f38342,plain,
( o = unpack2(i,o,o,i)
| ~ spl0_242
| spl0_243 ),
inference(forward_subsumption_resolution,[],[f38262,f34773]) ).
fof(f38392,plain,
( o = i
| spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_242
| spl0_243 ),
inference(forward_demodulation,[],[f38342,f35883]) ).
fof(f38407,plain,
( $false
| spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_242
| spl0_243 ),
inference(forward_subsumption_resolution,[],[f38392,f41]) ).
fof(f38408,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_242
| spl0_243 ),
inference(avatar_contradiction_clause,[],[f38407]) ).
fof(f38421,plain,
( spl0_251
| spl0_195
| ~ spl0_165
| spl0_242 ),
inference(avatar_split_clause,[],[f37289,f34768,f9566,f23484,f37297]) ).
fof(f38426,plain,
( i = unpack2(i,i,o,o)
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f35990,f23298]) ).
fof(f38431,plain,
( i = unpack1(i,i,o,o)
| ~ spl0_191
| ~ spl0_192 ),
inference(forward_demodulation,[],[f35985,f23298]) ).
fof(f38443,plain,
( o = i
| ~ spl0_191
| ~ spl0_192
| ~ spl0_240 ),
inference(forward_demodulation,[],[f38426,f33648]) ).
fof(f38450,plain,
( $false
| spl0_2
| ~ spl0_191
| ~ spl0_192
| ~ spl0_240 ),
inference(forward_subsumption_resolution,[],[f38443,f41]) ).
fof(f38451,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_192
| ~ spl0_240 ),
inference(avatar_contradiction_clause,[],[f38450]) ).
fof(f38454,plain,
( o = i
| ~ spl0_190
| ~ spl0_201 ),
inference(forward_demodulation,[],[f22800,f25196]) ).
fof(f38456,plain,
( $false
| spl0_2
| ~ spl0_190
| ~ spl0_201 ),
inference(forward_subsumption_resolution,[],[f38454,f41]) ).
fof(f38457,plain,
( spl0_2
| ~ spl0_190
| ~ spl0_201 ),
inference(avatar_contradiction_clause,[],[f38456]) ).
fof(f38460,plain,
( $false
| ~ spl0_191
| ~ spl0_192
| spl0_239 ),
inference(forward_subsumption_resolution,[],[f38431,f33611]) ).
fof(f38461,plain,
( ~ spl0_191
| ~ spl0_192
| spl0_239 ),
inference(avatar_contradiction_clause,[],[f38460]) ).
cnf(s1,plain,
( spl0_1
| ~ spl0_2 ),
inference(sat_conversion,[],[f42]) ).
cnf(s168,plain,
( spl0_1
| spl0_2
| spl0_165 ),
inference(sat_conversion,[],[f9603]) ).
cnf(s190,plain,
~ spl0_1,
inference(sat_conversion,[],[f14064]) ).
cnf(s196,plain,
( ~ spl0_3
| spl0_179 ),
inference(sat_conversion,[],[f22261]) ).
cnf(s202,plain,
( ~ spl0_179
| spl0_182
| spl0_184 ),
inference(sat_conversion,[],[f22437]) ).
cnf(s204,plain,
( ~ spl0_180
| spl0_185
| spl0_187 ),
inference(sat_conversion,[],[f22637]) ).
cnf(s205,plain,
( ~ spl0_182
| spl0_188
| spl0_189 ),
inference(sat_conversion,[],[f22794]) ).
cnf(s207,plain,
( spl0_3
| spl0_191
| spl0_192 ),
inference(sat_conversion,[],[f23299]) ).
cnf(s210,plain,
( spl0_3
| spl0_180 ),
inference(sat_conversion,[],[f23310]) ).
cnf(s212,plain,
( spl0_2
| spl0_189
| ~ spl0_191
| ~ spl0_192 ),
inference(sat_conversion,[],[f23643]) ).
cnf(s214,plain,
( spl0_2
| ~ spl0_184
| ~ spl0_191
| ~ spl0_192 ),
inference(sat_conversion,[],[f23648]) ).
cnf(s220,plain,
( spl0_2
| ~ spl0_183
| ~ spl0_187 ),
inference(sat_conversion,[],[f25172]) ).
cnf(s223,plain,
( spl0_183
| ~ spl0_191
| ~ spl0_192 ),
inference(sat_conversion,[],[f25180]) ).
cnf(s224,plain,
( ~ spl0_191
| spl0_194
| spl0_201 ),
inference(sat_conversion,[],[f25197]) ).
cnf(s229,plain,
( spl0_2
| spl0_3
| ~ spl0_191
| spl0_192 ),
inference(sat_conversion,[],[f25240]) ).
cnf(s231,plain,
( ~ spl0_192
| ~ spl0_194 ),
inference(sat_conversion,[],[f25246]) ).
cnf(s233,plain,
( spl0_2
| spl0_3
| spl0_191
| ~ spl0_192 ),
inference(sat_conversion,[],[f25254]) ).
cnf(s236,plain,
~ spl0_195,
inference(sat_conversion,[],[f25399]) ).
cnf(s238,plain,
( spl0_183
| spl0_191
| ~ spl0_192 ),
inference(sat_conversion,[],[f25569]) ).
cnf(s247,plain,
( spl0_2
| spl0_180
| spl0_191
| ~ spl0_192 ),
inference(sat_conversion,[],[f26888]) ).
cnf(s251,plain,
( ~ spl0_165
| spl0_191
| spl0_195
| spl0_202 ),
inference(sat_conversion,[],[f26965]) ).
cnf(s278,plain,
( spl0_2
| ~ spl0_182
| ~ spl0_188
| spl0_191
| ~ spl0_192
| spl0_195 ),
inference(sat_conversion,[],[f32226]) ).
cnf(s288,plain,
( spl0_2
| ~ spl0_185
| ~ spl0_189
| spl0_191
| ~ spl0_192
| spl0_195 ),
inference(sat_conversion,[],[f33424]) ).
cnf(s295,plain,
( ~ spl0_185
| spl0_231
| spl0_232 ),
inference(sat_conversion,[],[f33480]) ).
cnf(s304,plain,
( ~ spl0_179
| spl0_182
| ~ spl0_186 ),
inference(sat_conversion,[],[f33555]) ).
cnf(s311,plain,
( spl0_186
| ~ spl0_192
| ~ spl0_202 ),
inference(sat_conversion,[],[f33568]) ).
cnf(s318,plain,
( spl0_2
| spl0_186
| spl0_192
| ~ spl0_202 ),
inference(sat_conversion,[],[f33671]) ).
cnf(s319,plain,
( spl0_2
| ~ spl0_190
| spl0_192
| ~ spl0_202 ),
inference(sat_conversion,[],[f33673]) ).
cnf(s321,plain,
( ~ spl0_165
| spl0_192
| spl0_195
| spl0_241 ),
inference(sat_conversion,[],[f34447]) ).
cnf(s335,plain,
( spl0_2
| spl0_192
| ~ spl0_202
| spl0_242
| spl0_243 ),
inference(sat_conversion,[],[f34804]) ).
cnf(s336,plain,
( spl0_2
| spl0_192
| ~ spl0_202
| spl0_243
| spl0_244 ),
inference(sat_conversion,[],[f34805]) ).
cnf(s341,plain,
( spl0_2
| spl0_240
| ~ spl0_242
| ~ spl0_243 ),
inference(sat_conversion,[],[f35005]) ).
cnf(s343,plain,
( ~ spl0_242
| ~ spl0_244 ),
inference(sat_conversion,[],[f35009]) ).
cnf(s361,plain,
( spl0_2
| ~ spl0_240
| ~ spl0_246
| ~ spl0_247 ),
inference(sat_conversion,[],[f35761]) ).
cnf(s363,plain,
( spl0_2
| ~ spl0_239
| ~ spl0_246
| ~ spl0_247 ),
inference(sat_conversion,[],[f35765]) ).
cnf(s369,plain,
( spl0_2
| spl0_192
| ~ spl0_202
| spl0_242
| ~ spl0_243 ),
inference(sat_conversion,[],[f35835]) ).
cnf(s372,plain,
( spl0_2
| ~ spl0_191
| spl0_239
| ~ spl0_241 ),
inference(sat_conversion,[],[f35916]) ).
cnf(s377,plain,
( ~ spl0_185
| spl0_195
| ~ spl0_231
| spl0_240 ),
inference(sat_conversion,[],[f37172]) ).
cnf(s378,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_240
| ~ spl0_241 ),
inference(sat_conversion,[],[f37176]) ).
cnf(s381,plain,
( spl0_2
| ~ spl0_189
| ~ spl0_232 ),
inference(sat_conversion,[],[f37183]) ).
cnf(s383,plain,
( ~ spl0_182
| spl0_246 ),
inference(sat_conversion,[],[f37567]) ).
cnf(s390,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_241
| spl0_243
| ~ spl0_251 ),
inference(sat_conversion,[],[f37677]) ).
cnf(s393,plain,
( spl0_2
| ~ spl0_184
| spl0_242
| ~ spl0_243 ),
inference(sat_conversion,[],[f37928]) ).
cnf(s403,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_246
| spl0_247 ),
inference(sat_conversion,[],[f38169]) ).
cnf(s404,plain,
( spl0_2
| spl0_190
| ~ spl0_246
| spl0_247 ),
inference(sat_conversion,[],[f38171]) ).
cnf(s408,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_241
| ~ spl0_242
| spl0_243 ),
inference(sat_conversion,[],[f38408]) ).
cnf(s415,plain,
( ~ spl0_165
| spl0_195
| spl0_242
| spl0_251 ),
inference(sat_conversion,[],[f38421]) ).
cnf(s417,plain,
( spl0_2
| ~ spl0_191
| ~ spl0_192
| ~ spl0_240 ),
inference(sat_conversion,[],[f38451]) ).
cnf(s421,plain,
( spl0_2
| ~ spl0_190
| ~ spl0_201 ),
inference(sat_conversion,[],[f38457]) ).
cnf(s422,plain,
( ~ spl0_191
| ~ spl0_192
| spl0_239 ),
inference(sat_conversion,[],[f38461]) ).
cnf(s441,plain,
( spl0_2
| spl0_165 ),
inference(rat,[],[s168,s190]) ).
cnf(s511,plain,
~ spl0_2,
inference(rat,[],[s1,s190]) ).
cnf(s520,plain,
spl0_165,
inference(rat,[],[s441,s511]) ).
cnf(s530,plain,
( spl0_191
| spl0_3 ),
inference(rat,[],[s233,s207,s511]) ).
cnf(s531,plain,
spl0_3,
inference(rat,[],[s377,s295,s204,s381,s220,s212,s417,s223,s229,s530,s210,s236,s511]) ).
cnf(s532,plain,
spl0_179,
inference(rat,[],[s196,s531]) ).
cnf(s534,plain,
( ~ spl0_192
| spl0_191 ),
inference(rat,[],[s288,s205,s204,s278,s220,s304,s247,s238,s311,s251,s511,s236,s532,s520]) ).
cnf(s535,plain,
( spl0_242
| spl0_192
| ~ spl0_202 ),
inference(rat,[],[s369,s335,s511]) ).
cnf(s536,plain,
( spl0_192
| ~ spl0_202 ),
inference(rat,[],[s336,s341,s343,s535,s361,s404,s383,s304,s319,s318,s532,s511]) ).
cnf(s537,plain,
spl0_191,
inference(rat,[],[s536,s534,s251,s236,s520]) ).
cnf(s540,plain,
( ~ spl0_246
| ~ spl0_241 ),
inference(rat,[],[s363,s403,s372,s511,s537]) ).
cnf(s541,plain,
( spl0_242
| ~ spl0_241 ),
inference(rat,[],[s390,s393,s415,s202,s383,s540,s511,s537,s236,s520,s532]) ).
cnf(s542,plain,
~ spl0_241,
inference(rat,[],[s341,s408,s541,s378,s511,s537]) ).
cnf(s543,plain,
spl0_192,
inference(rat,[],[s321,s520,s236,s542]) ).
cnf(s544,plain,
spl0_239,
inference(rat,[],[s422,s537,s543]) ).
cnf(s545,plain,
~ spl0_194,
inference(rat,[],[s231,s543]) ).
cnf(s548,plain,
~ spl0_184,
inference(rat,[],[s214,s537,s511,s543]) ).
cnf(s551,plain,
spl0_201,
inference(rat,[],[s224,s537,s545]) ).
cnf(s553,plain,
spl0_182,
inference(rat,[],[s202,s532,s548]) ).
cnf(s555,plain,
~ spl0_190,
inference(rat,[],[s421,s511,s551]) ).
cnf(s556,plain,
spl0_246,
inference(rat,[],[s383,s553]) ).
cnf(s561,plain,
spl0_247,
inference(rat,[],[s404,s555,s511,s556]) ).
cnf(s562,plain,
$false,
inference(rat,[],[s363,s544,s511,s556,s561]) ).
fof(f38462,plain,
$false,
inference(avatar_sat_refutation,[],[s562]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV052-1.002.002 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n010.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 11:17:01 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 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
% 17.94/3.40 % (802245)Input is clausal, will run a generic CNF schedule.
% 17.94/3.40 % (802353)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1502722323:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.94/3.40 % (802354)lrs+10_1_sil=8000:sp=occurrence:random_seed=1298608838:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.94/3.40 % (802351)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=2606100817:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.94/3.40 % (802355)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1418660303:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.94/3.40 % (802352)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=8902440:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.94/3.40 % (802356)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2104392613:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.94/3.40 % (802354)Refutation not found, incomplete strategy
% 17.94/3.40 % (802354)------------------------------
% 17.94/3.40 % (802354)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.94/3.40 % (802354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/3.40 % (802355)Refutation not found, incomplete strategy
% 17.94/3.40 % (802355)------------------------------
% 17.94/3.40 % (802355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.94/3.40 % (802354)CaDiCaL version: 2.1.3
% 17.94/3.40 % (802354)Termination reason: Refutation not found, incomplete strategy
% 17.94/3.40 % (802354)Time elapsed: 0.001 s
% 17.94/3.40 % (802354)Peak memory usage: 86 MB
% 17.94/3.40 % (802355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/3.40 % (802355)CaDiCaL version: 2.1.3
% 17.94/3.40 % (802355)Termination reason: Refutation not found, incomplete strategy
% 17.94/3.40 % (802355)Time elapsed: 0.001 s
% 17.94/3.40 % (802355)Peak memory usage: 86 MB
% 17.94/3.40 % (802357)dis-21_1_sil=8000:lcm=predicate:random_seed=3128658700:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 17.94/3.40 % (802357)Refutation not found, incomplete strategy
% 17.94/3.40 % (802357)------------------------------
% 17.94/3.40 % (802357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.94/3.40 % (802357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/3.40 % (802357)CaDiCaL version: 2.1.3
% 17.94/3.40 % (802357)Termination reason: Refutation not found, incomplete strategy
% 17.94/3.40 % (802357)Time elapsed: 0.001 s
% 17.94/3.40 % (802357)Peak memory usage: 88 MB
% 17.94/3.40 % (802356)Instruction limit reached!
% 17.94/3.40 % (802356)------------------------------
% 17.94/3.40 % (802356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.94/3.40 % (802356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/3.40 % (802356)CaDiCaL version: 2.1.3
% 17.94/3.40 % (802356)Termination reason: Instruction limit
% 17.94/3.40 % (802356)Termination phase: Saturation
% 17.94/3.40 % (802356)Time elapsed: 0.114 s
% 17.94/3.40 % (802356)Peak memory usage: 89 MB
% 17.94/3.40 % (802356)Instructions burned: 181 (million)
% 17.94/3.40 % (802355)------------------------------
% 17.94/3.40 % (802355)------------------------------
% 17.94/3.40 % (802357)------------------------------
% 17.94/3.40 % (802357)------------------------------
% 17.94/3.40 % (802378)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1202939616:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 17.94/3.40 % (802378)Refutation not found, incomplete strategy
% 17.94/3.40 % (802378)------------------------------
% 17.94/3.40 % (802378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.94/3.40 % (802378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.94/3.40 % (802378)CaDiCaL version: 2.1.3
% 17.94/3.40 % (802378)Termination reason: Refutation not found, incomplete strategy
% 17.94/3.40 % (802378)Time elapsed: 0.001 s
% 17.94/3.40 % (802378)Peak memory usage: 86 MB
% 17.94/3.40 % (802354)------------------------------
% 17.94/3.40 % (802354)------------------------------
% 17.94/3.40 % (802379)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2995675912:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 30.82/5.31 % (802379)Refutation not found, incomplete strategy
% 30.82/5.31 % (802379)------------------------------
% 30.82/5.31 % (802379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.82/5.31 % (802379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.82/5.31 % (802379)CaDiCaL version: 2.1.3
% 30.82/5.31 % (802379)Termination reason: Refutation not found, incomplete strategy
% 30.82/5.31 % (802379)Time elapsed: 0.0000 s
% 30.82/5.31 % (802379)Peak memory usage: 86 MB
% 30.82/5.31 % (802380)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4069710114:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 30.82/5.31 % (802380)Refutation not found, incomplete strategy
% 30.82/5.31 % (802380)------------------------------
% 30.82/5.31 % (802380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.82/5.31 % (802380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.82/5.31 % (802380)CaDiCaL version: 2.1.3
% 30.82/5.31 % (802380)Termination reason: Refutation not found, incomplete strategy
% 30.82/5.31 % (802380)Time elapsed: 0.001 s
% 30.82/5.31 % (802380)Peak memory usage: 86 MB
% 30.82/5.31 % (802378)------------------------------
% 30.82/5.31 % (802378)------------------------------
% 30.82/5.31 % (802379)------------------------------
% 30.82/5.31 % (802379)------------------------------
% 30.82/5.31 % (802382)lrs+10_64_to=lpo:sil=8000:random_seed=3522127762:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 30.82/5.31 % (802382)Instruction limit reached!
% 30.82/5.31 % (802382)------------------------------
% 30.82/5.31 % (802382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.82/5.31 % (802382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.82/5.31 % (802382)CaDiCaL version: 2.1.3
% 30.82/5.31 % (802382)Termination reason: Instruction limit
% 30.82/5.31 % (802382)Termination phase: Saturation
% 30.82/5.31 % (802382)Time elapsed: 0.064 s
% 30.82/5.31 % (802382)Peak memory usage: 88 MB
% 30.82/5.31 % (802382)Instructions burned: 128 (million)
% 30.82/5.31 % (802387)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1404232761:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 30.82/5.31 % (802380)------------------------------
% 30.82/5.31 % (802380)------------------------------
% 30.82/5.31 % (802385)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3375053010:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 30.82/5.31 % (802387)Instruction limit reached!
% 30.82/5.31 % (802387)------------------------------
% 30.82/5.31 % (802387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.82/5.31 % (802387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.82/5.31 % (802387)CaDiCaL version: 2.1.3
% 30.82/5.31 % (802387)Termination reason: Instruction limit
% 30.82/5.31 % (802387)Termination phase: Saturation
% 30.82/5.31 % (802387)Time elapsed: 0.062 s
% 30.82/5.31 % (802387)Peak memory usage: 89 MB
% 30.82/5.31 % (802387)Instructions burned: 160 (million)
% 30.82/5.31 % (802385)Instruction limit reached!
% 30.82/5.31 % (802385)------------------------------
% 30.82/5.31 % (802385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.82/5.31 % (802385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.82/5.31 % (802385)CaDiCaL version: 2.1.3
% 30.82/5.31 % (802385)Termination reason: Instruction limit
% 30.82/5.31 % (802385)Termination phase: Saturation
% 30.82/5.31 % (802385)Time elapsed: 0.158 s
% 30.82/5.31 % (802385)Peak memory usage: 88 MB
% 30.82/5.31 % (802385)Instructions burned: 194 (million)
% 30.82/5.31 % (802388)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1235686111:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 30.82/5.31 % (802400)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1823309001:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 30.82/5.31 % (802400)Refutation not found, incomplete strategy
% 30.82/5.31 % (802400)------------------------------
% 30.82/5.31 % (802400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.82/5.31 % (802400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.82/5.31 % (802400)CaDiCaL version: 2.1.3
% 44.04/7.12 % (802400)Termination reason: Refutation not found, incomplete strategy
% 44.04/7.12 % (802400)Time elapsed: 0.001 s
% 44.04/7.12 % (802400)Peak memory usage: 87 MB
% 44.04/7.12 % (802398)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1695522957:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 44.04/7.12 % (802398)Refutation not found, incomplete strategy
% 44.04/7.12 % (802398)------------------------------
% 44.04/7.12 % (802398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/7.12 % (802398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/7.12 % (802398)CaDiCaL version: 2.1.3
% 44.04/7.12 % (802398)Termination reason: Refutation not found, incomplete strategy
% 44.04/7.12 % (802398)Time elapsed: 0.001 s
% 44.04/7.12 % (802398)Peak memory usage: 86 MB
% 44.04/7.12 % (802408)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3969243301:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 44.04/7.12 % (802400)------------------------------
% 44.04/7.12 % (802400)------------------------------
% 44.04/7.12 % (802408)Instruction limit reached!
% 44.04/7.12 % (802408)------------------------------
% 44.04/7.12 % (802408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/7.12 % (802408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/7.12 % (802408)CaDiCaL version: 2.1.3
% 44.04/7.12 % (802408)Termination reason: Instruction limit
% 44.04/7.12 % (802408)Termination phase: Saturation
% 44.04/7.12 % (802408)Time elapsed: 0.158 s
% 44.04/7.12 % (802408)Peak memory usage: 88 MB
% 44.04/7.12 % (802408)Instructions burned: 242 (million)
% 44.04/7.12 % (802398)------------------------------
% 44.04/7.12 % (802398)------------------------------
% 44.04/7.12 % (802417)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4025911564:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 44.04/7.12 % (802420)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1402345012:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 44.04/7.12 % (802420)Refutation not found, incomplete strategy
% 44.04/7.12 % (802420)------------------------------
% 44.04/7.12 % (802420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/7.12 % (802420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/7.12 % (802420)CaDiCaL version: 2.1.3
% 44.04/7.12 % (802420)Termination reason: Refutation not found, incomplete strategy
% 44.04/7.12 % (802420)Time elapsed: 0.001 s
% 44.04/7.12 % (802420)Peak memory usage: 86 MB
% 44.04/7.12 % (802422)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2679468078:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 44.04/7.12 % (802420)------------------------------
% 44.04/7.12 % (802420)------------------------------
% 44.04/7.12 % (802422)Instruction limit reached!
% 44.04/7.12 % (802422)------------------------------
% 44.04/7.12 % (802422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/7.12 % (802422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/7.12 % (802422)CaDiCaL version: 2.1.3
% 44.04/7.12 % (802422)Termination reason: Instruction limit
% 44.04/7.12 % (802422)Termination phase: Saturation
% 44.04/7.12 % (802422)Time elapsed: 0.400 s
% 44.04/7.12 % (802422)Peak memory usage: 90 MB
% 44.04/7.12 % (802422)Instructions burned: 500 (million)
% 44.04/7.12 % (802438)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3214086596:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 44.04/7.12 % (802441)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1135288749:i=264:kws=precedence:fsr=off_2977 on theBenchmark for (2977ds/264Mi)
% 44.04/7.12 % (802438)Instruction limit reached!
% 44.04/7.12 % (802438)------------------------------
% 44.04/7.12 % (802438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.04/7.12 % (802438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/7.12 % (802438)CaDiCaL version: 2.1.3
% 44.04/7.12 % (802438)Termination reason: Instruction limit
% 44.04/7.12 % (802438)Termination phase: Saturation
% 44.04/7.12 % (802438)Time elapsed: 0.118 s
% 44.04/7.12 % (802438)Peak memory usage: 88 MB
% 44.34/7.26 % (802438)Instructions burned: 193 (million)
% 44.34/7.26 % (802441)Instruction limit reached!
% 44.34/7.26 % (802441)------------------------------
% 44.34/7.26 % (802441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.26 % (802441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.26 % (802441)CaDiCaL version: 2.1.3
% 44.34/7.26 % (802441)Termination reason: Instruction limit
% 44.34/7.26 % (802441)Termination phase: Saturation
% 44.34/7.26 % (802441)Time elapsed: 0.216 s
% 44.34/7.26 % (802441)Peak memory usage: 89 MB
% 44.34/7.26 % (802441)Instructions burned: 265 (million)
% 44.34/7.26 % (802447)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2132099172:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 44.34/7.26 % (802447)Instruction limit reached!
% 44.34/7.26 % (802447)------------------------------
% 44.34/7.26 % (802447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.26 % (802447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.26 % (802447)CaDiCaL version: 2.1.3
% 44.34/7.26 % (802447)Termination reason: Instruction limit
% 44.34/7.26 % (802447)Termination phase: Saturation
% 44.34/7.26 % (802447)Time elapsed: 0.138 s
% 44.34/7.26 % (802447)Peak memory usage: 88 MB
% 44.34/7.26 % (802447)Instructions burned: 156 (million)
% 44.34/7.26 % (802450)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2194405725:i=3256:kws=precedence:bd=preordered:av=off_2972 on theBenchmark for (2972ds/3256Mi)
% 44.34/7.26 % (802454)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3390622985:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 44.34/7.26 % (802454)Instruction limit reached!
% 44.34/7.26 % (802454)------------------------------
% 44.34/7.26 % (802454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.26 % (802454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.26 % (802454)CaDiCaL version: 2.1.3
% 44.34/7.26 % (802454)Termination reason: Instruction limit
% 44.34/7.26 % (802454)Termination phase: Saturation
% 44.34/7.26 % (802454)Time elapsed: 0.602 s
% 44.34/7.26 % (802454)Peak memory usage: 87 MB
% 44.34/7.26 % (802454)Instructions burned: 537 (million)
% 44.34/7.26 % (802388)Instruction limit reached!
% 44.34/7.26 % (802388)------------------------------
% 44.34/7.26 % (802388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.26 % (802388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.26 % (802388)CaDiCaL version: 2.1.3
% 44.34/7.26 % (802388)Termination reason: Instruction limit
% 44.34/7.26 % (802388)Termination phase: Saturation
% 44.34/7.26 % (802388)Time elapsed: 3.083 s
% 44.34/7.26 % (802388)Peak memory usage: 138 MB
% 44.34/7.26 % (802388)Instructions burned: 3394 (million)
% 44.34/7.26 % (802465)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2279441978:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 44.34/7.26 % (802417)Instruction limit reached!
% 44.34/7.26 % (802417)------------------------------
% 44.34/7.26 % (802417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.26 % (802417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.26 % (802417)CaDiCaL version: 2.1.3
% 44.34/7.26 % (802417)Termination reason: Instruction limit
% 44.34/7.26 % (802417)Termination phase: Saturation
% 44.34/7.26 % (802417)Time elapsed: 2.585 s
% 44.34/7.26 % (802417)Peak memory usage: 148 MB
% 44.34/7.26 % (802417)Instructions burned: 5209 (million)
% 44.34/7.26 % (802465)Instruction limit reached!
% 44.34/7.26 % (802465)------------------------------
% 44.34/7.26 % (802465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.34/7.26 % (802465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.34/7.26 % (802465)CaDiCaL version: 2.1.3
% 44.34/7.26 % (802465)Termination reason: Instruction limit
% 44.34/7.26 % (802465)Termination phase: Saturation
% 44.34/7.26 % (802465)Time elapsed: 0.124 s
% 44.34/7.26 % (802465)Peak memory usage: 87 MB
% 44.34/7.26 % (802465)Instructions burned: 181 (million)
% 44.34/7.26 % (802467)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2207371799:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2958 on theBenchmark for (2958ds/10307Mi)
% 44.34/7.26 % (802468)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2817201175:i=412:gtgl=4:gtg=exists_all_2958 on theBenchmark for (2958ds/412Mi)
% 65.13/10.08 % (802470)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1860142151:s2pl=no:i=8478:s2at=4:nm=6_2957 on theBenchmark for (2957ds/8478Mi)
% 65.13/10.08 % (802468)Instruction limit reached!
% 65.13/10.08 % (802468)------------------------------
% 65.13/10.08 % (802468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802468)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802468)Termination reason: Instruction limit
% 65.13/10.08 % (802468)Termination phase: Saturation
% 65.13/10.08 % (802468)Time elapsed: 0.302 s
% 65.13/10.08 % (802468)Peak memory usage: 89 MB
% 65.13/10.08 % (802468)Instructions burned: 412 (million)
% 65.13/10.08 % (802476)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=993762779:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2952 on theBenchmark for (2952ds/303Mi)
% 65.13/10.08 % (802476)Refutation not found, incomplete strategy
% 65.13/10.08 % (802476)------------------------------
% 65.13/10.08 % (802476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802476)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802476)Termination reason: Refutation not found, incomplete strategy
% 65.13/10.08 % (802476)Time elapsed: 0.002 s
% 65.13/10.08 % (802476)Peak memory usage: 88 MB
% 65.13/10.08 % (802476)Instructions burned: 1 (million)
% 65.13/10.08 % (802476)------------------------------
% 65.13/10.08 % (802476)------------------------------
% 65.13/10.08 % (802485)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2121227055:st=4:i=720:sd=3:fsr=off:ss=axioms_2948 on theBenchmark for (2948ds/720Mi)
% 65.13/10.08 % (802485)Refutation not found, incomplete strategy
% 65.13/10.08 % (802485)------------------------------
% 65.13/10.08 % (802485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802485)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802485)Termination reason: Refutation not found, incomplete strategy
% 65.13/10.08 % (802485)Time elapsed: 0.0000 s
% 65.13/10.08 % (802485)Peak memory usage: 86 MB
% 65.13/10.08 % (802485)------------------------------
% 65.13/10.08 % (802485)------------------------------
% 65.13/10.08 % (802450)Instruction limit reached!
% 65.13/10.08 % (802450)------------------------------
% 65.13/10.08 % (802450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802450)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802450)Termination reason: Instruction limit
% 65.13/10.08 % (802450)Termination phase: Saturation
% 65.13/10.08 % (802450)Time elapsed: 2.774 s
% 65.13/10.08 % (802450)Peak memory usage: 137 MB
% 65.13/10.08 % (802450)Instructions burned: 3257 (million)
% 65.13/10.08 % (802489)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1546208813:i=598:bs=on:bd=preordered:av=off:ss=axioms_2943 on theBenchmark for (2943ds/598Mi)
% 65.13/10.08 % (802489)Refutation not found, incomplete strategy
% 65.13/10.08 % (802489)------------------------------
% 65.13/10.08 % (802489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802489)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802489)Termination reason: Refutation not found, incomplete strategy
% 65.13/10.08 % (802489)Time elapsed: 0.001 s
% 65.13/10.08 % (802489)Peak memory usage: 86 MB
% 65.13/10.08 % (802491)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1495459647:i=2989:sd=3:ss=axioms:sgt=60_2942 on theBenchmark for (2942ds/2989Mi)
% 65.13/10.08 [W927 11:17:08.895216245 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895241746 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895264240 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895270812 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895284301 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895289701 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895303522 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895308952 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895322295 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895327815 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895341071 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 [W927 11:17:08.895346601 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.
% 65.13/10.08 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 65.13/10.08 % (802489)------------------------------
% 65.13/10.08 % (802489)------------------------------
% 65.13/10.08 % (802491)Refutation not found, incomplete strategy
% 65.13/10.08 % (802491)------------------------------
% 65.13/10.08 % (802491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802491)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802491)Termination reason: Refutation not found, incomplete strategy
% 65.13/10.08 % (802491)Time elapsed: 0.388 s
% 65.13/10.08 % (802491)Peak memory usage: 125 MB
% 65.13/10.08 % (802491)Instructions burned: 821 (million)
% 65.13/10.08 % (802498)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=49979381:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2936 on theBenchmark for (2936ds/1997Mi)
% 65.13/10.08 % (802491)------------------------------
% 65.13/10.08 % (802491)------------------------------
% 65.13/10.08 % (802501)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=785384853:i=2088:bd=preordered:av=off_2933 on theBenchmark for (2933ds/2088Mi)
% 65.13/10.08 % (802501)Instruction limit reached!
% 65.13/10.08 % (802501)------------------------------
% 65.13/10.08 % (802501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802501)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802501)Termination reason: Instruction limit
% 65.13/10.08 % (802501)Termination phase: Saturation
% 65.13/10.08 % (802501)Time elapsed: 1.093 s
% 65.13/10.08 % (802501)Peak memory usage: 133 MB
% 65.13/10.08 % (802501)Instructions burned: 2090 (million)
% 65.13/10.08 % (802505)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1688508576:i=1098:nicw=on_2920 on theBenchmark for (2920ds/1098Mi)
% 65.13/10.08 % (802498)Instruction limit reached!
% 65.13/10.08 % (802498)------------------------------
% 65.13/10.08 % (802498)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802498)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802498)Termination reason: Instruction limit
% 65.13/10.08 % (802498)Termination phase: Saturation
% 65.13/10.08 % (802498)Time elapsed: 1.968 s
% 65.13/10.08 % (802498)Peak memory usage: 135 MB
% 65.13/10.08 % (802498)Instructions burned: 1997 (million)
% 65.13/10.08 % (802505)Instruction limit reached!
% 65.13/10.08 % (802505)------------------------------
% 65.13/10.08 % (802505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802505)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802505)Termination reason: Instruction limit
% 65.13/10.08 % (802505)Termination phase: Saturation
% 65.13/10.08 % (802505)Time elapsed: 0.473 s
% 65.13/10.08 % (802505)Peak memory usage: 92 MB
% 65.13/10.08 % (802505)Instructions burned: 1101 (million)
% 65.13/10.08 % (802509)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=668072467:i=433:bd=preordered_2914 on theBenchmark for (2914ds/433Mi)
% 65.13/10.08 % (802509)Refutation not found, incomplete strategy
% 65.13/10.08 % (802509)------------------------------
% 65.13/10.08 % (802509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.13/10.08 % (802509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.13/10.08 % (802509)CaDiCaL version: 2.1.3
% 65.13/10.08 % (802509)Termination reason: Refutation not found, incomplete strategy
% 65.13/10.08 % (802509)Time elapsed: 0.002 s
% 65.13/10.08 % (802509)Peak memory usage: 87 MB
% 65.13/10.08 % (802510)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1714175318:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2913 on theBenchmark for (2913ds/2942Mi)
% 65.13/10.08 % (802351)First to succeed.
% 65.13/10.08 % (802351)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-802245"
% 65.13/10.08 % (802351)Refutation found. Thanks to Tanya!
% 65.13/10.08 % SZS status Unsatisfiable for theBenchmark
% 65.13/10.08 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/10.32 % (802351)------------------------------
% 0.18/10.32 % (802351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/10.32 % (802351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/10.32 % (802351)CaDiCaL version: 2.1.3
% 0.18/10.32 % (802351)Termination reason: Refutation
% 0.18/10.32 % (802351)Time elapsed: 8.774 s
% 0.18/10.32 % (802351)Peak memory usage: 155 MB
% 0.18/10.32 % (802351)Instructions burned: 11325 (million)
% 0.18/10.32 % (802351)------------------------------
% 0.18/10.32 % (802351)------------------------------
% 0.18/10.32 % (802245)Success in time 9.205 s
% 0.18/10.32 % Vampire exiting
%------------------------------------------------------------------------------