%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ050-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 12:31:23 PM UTC 2026
% Result : Unsatisfiable 209.01s 32.00s
% Output : Refutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 272
% Number of leaves : 48
% Syntax : Number of formulae : 467 ( 307 unt; 16 def)
% Number of atoms : 627 ( 32 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 322 ( 162 ~; 160 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-12 aty)
% Number of functors : 30 ( 30 usr; 17 con; 0-2 aty)
% Number of variables : 1697 (1697 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,X7),X8,X9,X10,e1(X6,s(X7)),X11)
| state(X0,X1,X2,X3,X4,X5,s1(X6,s(X7)),X8,X9,X10,e1(X6,X7),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_right) ).
fof(f2,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,s(X7)),X8,X9,X10,e1(X6,X7),X11)
| state(X0,X1,X2,X3,X4,X5,s1(X6,X7),X8,X9,X10,e1(X6,s(X7)),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_left) ).
fof(f3,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,X7),X8,X9,X10,e1(s(X6),X7),X11)
| state(X0,X1,X2,X3,X4,X5,s1(s(X6),X7),X8,X9,X10,e1(X6,X7),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_down) ).
fof(f4,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(s(X6),X7),X8,X9,X10,e1(X6,X7),X11)
| state(X0,X1,X2,X3,X4,X5,s1(X6,X7),X8,X9,X10,e1(s(X6),X7),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_up) ).
fof(f5,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_right) ).
fof(f6,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,s(X8)),X9,X10,e1(X7,X8),X11)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(X7,s(X8)),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_left) ).
fof(f7,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11)
| state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_down) ).
fof(f8,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(s(X7),X8),X9,X10,e1(X7,X8),X11)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,X8),X9,X10,e1(s(X7),X8),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s2_up) ).
fof(f9,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s3_right) ).
fof(f10,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,s(X9)),X10,e1(X8,X9),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(X8,s(X9)),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s3_left) ).
fof(f11,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(s(X8),X9),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(s(X8),X9),X10,e1(X8,X9),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s3_down) ).
fof(f12,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(s(X8),X9),X10,e1(X8,X9),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,X9),X10,e1(s(X8),X9),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s3_up) ).
fof(f13,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s4_right) ).
fof(f14,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,s(X10)),e1(X9,X10),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(X9,s(X10)),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s4_left) ).
fof(f15,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s4_down) ).
fof(f16,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(s(X9),X10),e1(X9,X10),X11)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,X10),e1(s(X9),X10),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s4_up) ).
fof(f19,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,v1(X1,X2),X3,X4,X5,X6,X7,X8,X9,X10,e1(s(s(X1)),X2),X11)
| state(X0,v1(s(X1),X2),X3,X4,X5,X6,X7,X8,X9,X10,e1(X1,X2),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v1_down) ).
fof(f25,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(X3,s(X4)),e2(s(X3),s(X4)))
| state(X0,X1,X2,v3(X3,s(X4)),X5,X6,X7,X8,X9,X10,e1(X3,X4),e2(s(X3),X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3_right) ).
fof(f26,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,s(X4)),X5,X6,X7,X8,X9,X10,e1(X3,X4),e2(s(X3),X4))
| state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(X3,s(X4)),e2(s(X3),s(X4))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3_left) ).
fof(f27,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11)
| state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3_down) ).
fof(f28,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(s(X3),X4),X5,X6,X7,X8,X9,X10,e1(X3,X4),X11)
| state(X0,X1,X2,v3(X3,X4),X5,X6,X7,X8,X9,X10,e1(s(s(X3)),X4),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v3_up) ).
fof(f29,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5)))
| state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4_right) ).
fof(f30,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,s(X5)),X6,X7,X8,X9,X10,e1(X4,X5),e2(s(X4),X5))
| state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(X4,s(X5)),e2(s(X4),s(X5))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4_left) ).
fof(f31,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(s(s(X4)),X5),X11)
| state(X0,X1,X2,X3,v4(s(X4),X5),X6,X7,X8,X9,X10,e1(X4,X5),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4_down) ).
fof(f32,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(s(X4),X5),X6,X7,X8,X9,X10,e1(X4,X5),X11)
| state(X0,X1,X2,X3,v4(X4,X5),X6,X7,X8,X9,X10,e1(s(s(X4)),X5),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',v4_up) ).
fof(f33,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11)
| state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_right) ).
fof(f34,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,s(X6)),X7,X8,X9,X10,e1(X5,X6),X11)
| state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(X5,s(s(X6))),X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_left) ).
fof(f35,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,X6),X7,X8,X9,X10,e1(s(X5),X6),e2(s(X5),s(X6)))
| state(X0,X1,X2,X3,X4,h(s(X5),X6),X7,X8,X9,X10,e1(X5,X6),e2(X5,s(X6))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h_down) ).
fof(f38,axiom,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(bb(X0,s(X1)),X2,X3,X4,X5,X6,X7,X8,X9,X10,e1(X0,X1),e2(s(X0),X1))
| state(bb(X0,X1),X2,X3,X4,X5,X6,X7,X8,X9,X10,e1(X0,s(s(X1))),e2(s(X0),s(s(X1)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_left) ).
fof(f41,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(X12,X13))
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X12,X13),e2(X10,X11)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',swap_blanks) ).
fof(f42,axiom,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',initial_state) ).
fof(f43,negated_conjecture,
~ state(bb(o,o),v1(s(s(o)),o),v2(o,s(s(s(o)))),v3(o,s(s(o))),v4(s(s(s(o))),s(s(o))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(o)),s2(s(s(o)),s(s(o))),s3(s(s(o)),s(s(s(o)))),s4(s(s(s(o))),s(o)),e1(s(s(s(o))),s(s(s(o)))),e2(s(s(s(s(o)))),s(s(s(o))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intermediate_state) ).
fof(f44,definition,
sF0 = bb(o,o),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f45,plain,
bb(o,o) = sF0,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF1 = s(o),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f47,plain,
s(o) = sF1,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF2 = s(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f49,plain,
s(sF1) = sF2,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF3 = v1(sF2,o),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f51,plain,
v1(sF2,o) = sF3,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF4 = s(sF2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f53,plain,
s(sF2) = sF4,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF5 = v2(o,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f55,plain,
v2(o,sF4) = sF5,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF6 = v3(o,sF2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f57,plain,
v3(o,sF2) = sF6,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF7 = v4(sF4,sF2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f59,plain,
v4(sF4,sF2) = sF7,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF8 = s(sF4),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f61,plain,
s(sF4) = sF8,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF9 = h(sF8,o),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f63,plain,
h(sF8,o) = sF9,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF10 = s1(sF2,sF1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f65,plain,
s1(sF2,sF1) = sF10,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF11 = s2(sF2,sF2),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f67,plain,
s2(sF2,sF2) = sF11,
inference(reorient_equations,[],[f66]) ).
fof(f68,definition,
sF12 = s3(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f69,plain,
s3(sF2,sF4) = sF12,
inference(reorient_equations,[],[f68]) ).
fof(f70,definition,
sF13 = s4(sF4,sF1),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f71,plain,
s4(sF4,sF1) = sF13,
inference(reorient_equations,[],[f70]) ).
fof(f72,definition,
sF14 = e1(sF4,sF4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f73,plain,
e1(sF4,sF4) = sF14,
inference(reorient_equations,[],[f72]) ).
fof(f74,definition,
sF15 = e2(sF8,sF4),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f75,plain,
e2(sF8,sF4) = sF15,
inference(reorient_equations,[],[f74]) ).
fof(f76,plain,
~ state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,sF12,sF13,sF14,sF15),
inference(definition_folding,[],[f43,f75,f53,f49,f47,f61,f53,f49,f47,f73,f53,f49,f47,f53,f49,f47,f71,f47,f53,f49,f47,f69,f53,f49,f47,f49,f47,f67,f49,f47,f49,f47,f65,f47,f49,f47,f63,f61,f53,f49,f47,f59,f49,f47,f53,f49,f47,f57,f49,f47,f55,f53,f49,f47,f51,f49,f47,f45]) ).
fof(f78,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,sF2),X5,X6,X7,X8,X9,e1(X4,sF1),e2(s(X4),sF1))
| state(X0,X1,X2,X3,v4(X4,sF1),X5,X6,X7,X8,X9,e1(X4,sF2),e2(s(X4),sF2)) ),
inference(superposition,[],[f30,f49]) ).
fof(f79,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,sF4),X5,X6,X7,X8,X9,e1(X4,sF2),e2(s(X4),sF2))
| state(X0,X1,X2,X3,v4(X4,sF2),X5,X6,X7,X8,X9,e1(X4,sF4),e2(s(X4),sF4)) ),
inference(superposition,[],[f30,f53]) ).
fof(f89,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,sF1),X4,X5,X6,X7,X8,X9,e1(X3,o),e2(s(X3),o))
| state(X0,X1,X2,v3(X3,o),X4,X5,X6,X7,X8,X9,e1(X3,sF1),e2(s(X3),sF1)) ),
inference(superposition,[],[f26,f47]) ).
fof(f90,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,sF2),X4,X5,X6,X7,X8,X9,e1(X3,sF1),e2(s(X3),sF1))
| state(X0,X1,X2,v3(X3,sF1),X4,X5,X6,X7,X8,X9,e1(X3,sF2),e2(s(X3),sF2)) ),
inference(superposition,[],[f26,f49]) ).
fof(f136,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF4,s(sF2)),e2(s(sF4),s(sF2)))
| state(X0,X1,X2,X3,v4(sF4,s(sF2)),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(s(sF4),sF2)) ),
inference(superposition,[],[f29,f59]) ).
fof(f142,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,sF1),X5,X6,X7,X8,X9,e1(X4,sF2),e2(s(X4),sF2))
| state(X0,X1,X2,X3,v4(X4,sF2),X5,X6,X7,X8,X9,e1(X4,sF1),e2(s(X4),sF1)) ),
inference(superposition,[],[f29,f49]) ).
fof(f143,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(X4,sF2),X5,X6,X7,X8,X9,e1(X4,sF4),e2(s(X4),sF4))
| state(X0,X1,X2,X3,v4(X4,sF4),X5,X6,X7,X8,X9,e1(X4,sF2),e2(s(X4),sF2)) ),
inference(superposition,[],[f29,f53]) ).
fof(f145,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF4,sF4),e2(s(sF4),sF4))
| state(X0,X1,X2,X3,v4(sF4,s(sF2)),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(s(sF4),sF2)) ),
inference(forward_demodulation,[],[f136,f53]) ).
fof(f146,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF4,sF4),e2(sF8,sF4))
| state(X0,X1,X2,X3,v4(sF4,s(sF2)),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(s(sF4),sF2)) ),
inference(forward_demodulation,[],[f145,f61]) ).
fof(f147,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF4,sF4),sF15)
| state(X0,X1,X2,X3,v4(sF4,s(sF2)),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(s(sF4),sF2)) ),
inference(forward_demodulation,[],[f146,f75]) ).
fof(f148,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,sF14,sF15)
| state(X0,X1,X2,X3,v4(sF4,s(sF2)),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(s(sF4),sF2)) ),
inference(forward_demodulation,[],[f147,f73]) ).
fof(f149,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( state(X0,X1,X2,X3,v4(sF4,s(sF2)),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2))
| ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,sF14,sF15) ),
inference(forward_demodulation,[],[f148,f61]) ).
fof(f150,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,sF14,sF15)
| state(X0,X1,X2,X3,v4(sF4,sF4),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2)) ),
inference(forward_demodulation,[],[f149,f53]) ).
fof(f156,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,o),X4,X5,X6,X7,X8,X9,e1(X3,sF1),e2(s(X3),sF1))
| state(X0,X1,X2,v3(X3,sF1),X4,X5,X6,X7,X8,X9,e1(X3,o),e2(s(X3),o)) ),
inference(superposition,[],[f25,f47]) ).
fof(f157,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(X3,sF1),X4,X5,X6,X7,X8,X9,e1(X3,sF2),e2(s(X3),sF2))
| state(X0,X1,X2,v3(X3,sF2),X4,X5,X6,X7,X8,X9,e1(X3,sF1),e2(s(X3),sF1)) ),
inference(superposition,[],[f25,f49]) ).
fof(f195,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(s(X5),o),e2(s(X5),sF1))
| state(X0,X1,X2,X3,X4,h(s(X5),o),X6,X7,X8,X9,e1(X5,o),e2(X5,sF1)) ),
inference(superposition,[],[f35,f47]) ).
fof(f202,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(X5,s(sF1)),X10)
| state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,o),X10) ),
inference(superposition,[],[f33,f47]) ).
fof(f203,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,s(sF2)),X10)
| state(X0,X1,X2,X3,X4,h(X5,sF2),X6,X7,X8,X9,e1(X5,sF1),X10) ),
inference(superposition,[],[f33,f49]) ).
fof(f207,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,sF4),X10)
| state(X0,X1,X2,X3,X4,h(X5,sF2),X6,X7,X8,X9,e1(X5,sF1),X10) ),
inference(forward_demodulation,[],[f203,f53]) ).
fof(f208,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(X5,sF2),X10)
| state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,o),X10) ),
inference(forward_demodulation,[],[f202,f49]) ).
fof(f212,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,sF14,e2(X10,X11))
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),e2(sF4,sF4)) ),
inference(superposition,[],[f41,f73]) ).
fof(f213,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(X10,X11),sF15)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(sF8,sF4),e2(X10,X11)) ),
inference(superposition,[],[f41,f75]) ).
fof(f214,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,o),X10)
| state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(X5,s(sF1)),X10) ),
inference(superposition,[],[f34,f47]) ).
fof(f215,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,sF2),X6,X7,X8,X9,e1(X5,sF1),X10)
| state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,s(sF2)),X10) ),
inference(superposition,[],[f34,f49]) ).
fof(f221,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,sF2),X6,X7,X8,X9,e1(X5,sF1),X10)
| state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,sF4),X10) ),
inference(forward_demodulation,[],[f215,f53]) ).
fof(f222,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(X5,sF1),X6,X7,X8,X9,e1(X5,o),X10)
| state(X0,X1,X2,X3,X4,h(X5,o),X6,X7,X8,X9,e1(X5,sF2),X10) ),
inference(forward_demodulation,[],[f214,f49]) ).
fof(f226,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,X4),X5,X6,X7,X8,X9,e1(sF2,X4),X10)
| state(X0,X1,X2,X3,v4(sF2,X4),X5,X6,X7,X8,X9,e1(s(sF4),X4),X10) ),
inference(superposition,[],[f32,f53]) ).
fof(f230,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,X4),X5,X6,X7,X8,X9,e1(sF2,X4),X10)
| state(X0,X1,X2,X3,v4(sF2,X4),X5,X6,X7,X8,X9,e1(sF8,X4),X10) ),
inference(forward_demodulation,[],[f226,f61]) ).
fof(f234,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF1,X3),X4,X5,X6,X7,X8,X9,e1(o,X3),X10)
| state(X0,X1,X2,v3(o,X3),X4,X5,X6,X7,X8,X9,e1(s(sF1),X3),X10) ),
inference(superposition,[],[f28,f47]) ).
fof(f235,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF2,X3),X4,X5,X6,X7,X8,X9,e1(sF1,X3),X10)
| state(X0,X1,X2,v3(sF1,X3),X4,X5,X6,X7,X8,X9,e1(s(sF2),X3),X10) ),
inference(superposition,[],[f28,f49]) ).
fof(f236,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF4,X3),X4,X5,X6,X7,X8,X9,e1(sF2,X3),X10)
| state(X0,X1,X2,v3(sF2,X3),X4,X5,X6,X7,X8,X9,e1(s(sF4),X3),X10) ),
inference(superposition,[],[f28,f53]) ).
fof(f240,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF4,X3),X4,X5,X6,X7,X8,X9,e1(sF2,X3),X10)
| state(X0,X1,X2,v3(sF2,X3),X4,X5,X6,X7,X8,X9,e1(sF8,X3),X10) ),
inference(forward_demodulation,[],[f236,f61]) ).
fof(f241,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF2,X3),X4,X5,X6,X7,X8,X9,e1(sF1,X3),X10)
| state(X0,X1,X2,v3(sF1,X3),X4,X5,X6,X7,X8,X9,e1(sF4,X3),X10) ),
inference(forward_demodulation,[],[f235,f53]) ).
fof(f242,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF1,X3),X4,X5,X6,X7,X8,X9,e1(o,X3),X10)
| state(X0,X1,X2,v3(o,X3),X4,X5,X6,X7,X8,X9,e1(sF2,X3),X10) ),
inference(forward_demodulation,[],[f234,f49]) ).
fof(f247,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF2,X4),X5,X6,X7,X8,X9,e1(s(sF4),X4),X10)
| state(X0,X1,X2,X3,v4(sF4,X4),X5,X6,X7,X8,X9,e1(sF2,X4),X10) ),
inference(superposition,[],[f31,f53]) ).
fof(f249,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF2,X4),X5,X6,X7,X8,X9,e1(sF8,X4),X10)
| state(X0,X1,X2,X3,v4(sF4,X4),X5,X6,X7,X8,X9,e1(sF2,X4),X10) ),
inference(forward_demodulation,[],[f247,f61]) ).
fof(f266,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF4,X6),X7,X8,X9,e1(sF2,X6),X10)
| state(X0,X1,X2,X3,X4,X5,s1(sF2,X6),X7,X8,X9,e1(sF4,X6),X10) ),
inference(superposition,[],[f4,f53]) ).
fof(f267,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF8,X6),X7,X8,X9,e1(sF4,X6),X10)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,X6),X7,X8,X9,e1(sF8,X6),X10) ),
inference(superposition,[],[f4,f61]) ).
fof(f268,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(s(sF4),sF4),X6,X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,sF4),X6,X7,X8,e1(s(sF4),sF4),X9) ),
inference(superposition,[],[f4,f73]) ).
fof(f269,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF8,sF4),X6,X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,sF4),X6,X7,X8,e1(s(sF4),sF4),X9) ),
inference(forward_demodulation,[],[f268,f61]) ).
fof(f270,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF8,sF4),X6,X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,sF4),X6,X7,X8,e1(sF8,sF4),X9) ),
inference(forward_demodulation,[],[f269,f61]) ).
fof(f274,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF2,X3),X4,X5,X6,X7,X8,X9,e1(s(sF4),X3),X10)
| state(X0,X1,X2,v3(sF4,X3),X4,X5,X6,X7,X8,X9,e1(sF2,X3),X10) ),
inference(superposition,[],[f27,f53]) ).
fof(f276,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF2,X3),X4,X5,X6,X7,X8,X9,e1(sF8,X3),X10)
| state(X0,X1,X2,v3(sF4,X3),X4,X5,X6,X7,X8,X9,e1(sF2,X3),X10) ),
inference(forward_demodulation,[],[f274,f61]) ).
fof(f304,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,v1(o,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(s(sF1),X1),X10)
| state(X0,v1(sF1,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(o,X1),X10) ),
inference(superposition,[],[f19,f47]) ).
fof(f305,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,v1(sF1,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(s(sF2),X1),X10)
| state(X0,v1(sF2,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(sF1,X1),X10) ),
inference(superposition,[],[f19,f49]) ).
fof(f309,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,v1(sF1,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(sF4,X1),X10)
| state(X0,v1(sF2,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(sF1,X1),X10) ),
inference(forward_demodulation,[],[f305,f53]) ).
fof(f310,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,v1(o,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(sF2,X1),X10)
| state(X0,v1(sF1,X1),X2,X3,X4,X5,X6,X7,X8,X9,e1(o,X1),X10) ),
inference(forward_demodulation,[],[f304,f49]) ).
fof(f314,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,sF1),X7,X8,X9,e1(X6,o),X10)
| state(X0,X1,X2,X3,X4,X5,s1(X6,o),X7,X8,X9,e1(X6,sF1),X10) ),
inference(superposition,[],[f2,f47]) ).
fof(f315,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,sF2),X7,X8,X9,e1(X6,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,s1(X6,sF1),X7,X8,X9,e1(X6,sF2),X10) ),
inference(superposition,[],[f2,f49]) ).
fof(f316,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,sF4),X7,X8,X9,e1(X6,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,s1(X6,sF2),X7,X8,X9,e1(X6,sF4),X10) ),
inference(superposition,[],[f2,f53]) ).
fof(f323,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,X7),X8,X9,e1(sF2,X7),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,X7),X8,X9,e1(sF4,X7),X10) ),
inference(superposition,[],[f8,f53]) ).
fof(f324,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF8,X7),X8,X9,e1(sF4,X7),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,X7),X8,X9,e1(sF8,X7),X10) ),
inference(superposition,[],[f8,f61]) ).
fof(f325,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(s(sF4),sF4),X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,sF4),X7,X8,e1(s(sF4),sF4),X9) ),
inference(superposition,[],[f8,f73]) ).
fof(f326,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF8,sF4),X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,sF4),X7,X8,e1(s(sF4),sF4),X9) ),
inference(forward_demodulation,[],[f325,f61]) ).
fof(f327,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF8,sF4),X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,sF4),X7,X8,e1(sF8,sF4),X9) ),
inference(forward_demodulation,[],[f326,f61]) ).
fof(f328,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,sF10,X6,X7,X8,e1(sF2,s(sF1)),X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF2,s(sF1)),X6,X7,X8,e1(sF2,sF1),X9) ),
inference(superposition,[],[f1,f65]) ).
fof(f329,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,o),X7,X8,X9,e1(X6,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,s1(X6,sF1),X7,X8,X9,e1(X6,o),X10) ),
inference(superposition,[],[f1,f47]) ).
fof(f330,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,sF1),X7,X8,X9,e1(X6,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,s1(X6,sF2),X7,X8,X9,e1(X6,sF1),X10) ),
inference(superposition,[],[f1,f49]) ).
fof(f331,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(X6,sF2),X7,X8,X9,e1(X6,sF4),X10)
| state(X0,X1,X2,X3,X4,X5,s1(X6,sF4),X7,X8,X9,e1(X6,sF2),X10) ),
inference(superposition,[],[f1,f53]) ).
fof(f333,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,sF10,X6,X7,X8,e1(sF2,sF2),X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF2,s(sF1)),X6,X7,X8,e1(sF2,sF1),X9) ),
inference(forward_demodulation,[],[f328,f49]) ).
fof(f334,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,sF10,X6,X7,X8,e1(sF2,sF2),X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF2,sF2),X6,X7,X8,e1(sF2,sF1),X9) ),
inference(forward_demodulation,[],[f333,f49]) ).
fof(f335,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF1),X8,X9,e1(X7,o),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,o),X8,X9,e1(X7,sF1),X10) ),
inference(superposition,[],[f6,f47]) ).
fof(f336,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF2),X8,X9,e1(X7,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF1),X8,X9,e1(X7,sF2),X10) ),
inference(superposition,[],[f6,f49]) ).
fof(f337,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF4),X8,X9,e1(X7,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF2),X8,X9,e1(X7,sF4),X10) ),
inference(superposition,[],[f6,f53]) ).
fof(f344,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,X8),X9,e1(sF2,X8),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF2,X8),X9,e1(sF4,X8),X10) ),
inference(superposition,[],[f12,f53]) ).
fof(f345,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF8,X8),X9,e1(sF4,X8),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,X8),X9,e1(sF8,X8),X10) ),
inference(superposition,[],[f12,f61]) ).
fof(f346,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(s(sF4),sF4),X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,sF4),X8,e1(s(sF4),sF4),X9) ),
inference(superposition,[],[f12,f73]) ).
fof(f347,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF8,sF4),X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,sF4),X8,e1(s(sF4),sF4),X9) ),
inference(forward_demodulation,[],[f346,f61]) ).
fof(f348,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF8,sF4),X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,sF4),X8,e1(sF8,sF4),X9) ),
inference(forward_demodulation,[],[f347,f61]) ).
fof(f349,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF1),X9,e1(X8,o),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,o),X9,e1(X8,sF1),X10) ),
inference(superposition,[],[f10,f47]) ).
fof(f350,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF2),X9,e1(X8,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF1),X9,e1(X8,sF2),X10) ),
inference(superposition,[],[f10,f49]) ).
fof(f351,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF4),X9,e1(X8,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF2),X9,e1(X8,sF4),X10) ),
inference(superposition,[],[f10,f53]) ).
fof(f356,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF1),e1(X9,o),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,o),e1(X9,sF1),X10) ),
inference(superposition,[],[f14,f47]) ).
fof(f357,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF2),e1(X9,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF1),e1(X9,sF2),X10) ),
inference(superposition,[],[f14,f49]) ).
fof(f358,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF4),e1(X9,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF2),e1(X9,sF4),X10) ),
inference(superposition,[],[f14,f53]) ).
fof(f363,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,sF11,X7,X8,e1(sF2,s(sF2)),X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,s(sF2)),X7,X8,e1(sF2,sF2),X9) ),
inference(superposition,[],[f5,f67]) ).
fof(f364,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,o),X8,X9,e1(X7,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF1),X8,X9,e1(X7,o),X10) ),
inference(superposition,[],[f5,f47]) ).
fof(f365,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF1),X8,X9,e1(X7,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF2),X8,X9,e1(X7,sF1),X10) ),
inference(superposition,[],[f5,f49]) ).
fof(f366,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF2),X8,X9,e1(X7,sF4),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(X7,sF4),X8,X9,e1(X7,sF2),X10) ),
inference(superposition,[],[f5,f53]) ).
fof(f368,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,sF11,X7,X8,e1(sF2,sF4),X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,s(sF2)),X7,X8,e1(sF2,sF2),X9) ),
inference(forward_demodulation,[],[f363,f53]) ).
fof(f369,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,sF11,X7,X8,e1(sF2,sF4),X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,sF4),X7,X8,e1(sF2,sF2),X9) ),
inference(forward_demodulation,[],[f368,f53]) ).
fof(f372,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF4,X9),e1(sF2,X9),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF2,X9),e1(sF4,X9),X10) ),
inference(superposition,[],[f16,f53]) ).
fof(f373,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF8,X9),e1(sF4,X9),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF4,X9),e1(sF8,X9),X10) ),
inference(superposition,[],[f16,f61]) ).
fof(f380,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF2,X6),X7,X8,X9,e1(sF4,X6),X10)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,X6),X7,X8,X9,e1(sF2,X6),X10) ),
inference(superposition,[],[f3,f53]) ).
fof(f381,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF4,X6),X7,X8,X9,e1(sF8,X6),X10)
| state(X0,X1,X2,X3,X4,X5,s1(sF8,X6),X7,X8,X9,e1(sF4,X6),X10) ),
inference(superposition,[],[f3,f61]) ).
fof(f385,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,o),X9,e1(X8,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF1),X9,e1(X8,o),X10) ),
inference(superposition,[],[f9,f47]) ).
fof(f386,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF1),X9,e1(X8,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF2),X9,e1(X8,sF1),X10) ),
inference(superposition,[],[f9,f49]) ).
fof(f387,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF2),X9,e1(X8,sF4),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(X8,sF4),X9,e1(X8,sF2),X10) ),
inference(superposition,[],[f9,f53]) ).
fof(f392,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,o),e1(X9,sF1),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF1),e1(X9,o),X10) ),
inference(superposition,[],[f13,f47]) ).
fof(f393,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF1),e1(X9,sF2),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF2),e1(X9,sF1),X10) ),
inference(superposition,[],[f13,f49]) ).
fof(f394,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF2),e1(X9,sF4),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(X9,sF4),e1(X9,sF2),X10) ),
inference(superposition,[],[f13,f53]) ).
fof(f401,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,X7),X8,X9,e1(sF4,X7),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,X7),X8,X9,e1(sF2,X7),X10) ),
inference(superposition,[],[f7,f53]) ).
fof(f402,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,X7),X8,X9,e1(sF8,X7),X10)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF8,X7),X8,X9,e1(sF4,X7),X10) ),
inference(superposition,[],[f7,f61]) ).
fof(f408,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF2,X8),X9,e1(sF4,X8),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,X8),X9,e1(sF2,X8),X10) ),
inference(superposition,[],[f11,f53]) ).
fof(f409,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF4,X8),X9,e1(sF8,X8),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF8,X8),X9,e1(sF4,X8),X10) ),
inference(superposition,[],[f11,f61]) ).
fof(f416,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF2,X9),e1(sF4,X9),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF4,X9),e1(sF2,X9),X10) ),
inference(superposition,[],[f15,f53]) ).
fof(f417,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF4,X9),e1(sF8,X9),X10)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF8,X9),e1(sF4,X9),X10) ),
inference(superposition,[],[f15,f61]) ).
fof(f425,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(bb(o,s(X0)),X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(o,X0),e2(sF1,X0))
| state(bb(o,X0),X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(o,s(s(X0))),e2(sF1,s(s(X0)))) ),
inference(superposition,[],[f38,f47]) ).
fof(f442,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF4,o),X3,X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1))
| state(X0,X1,X2,v3(sF4,sF1),X3,X4,X5,X6,X7,X8,e1(sF4,o),e2(sF8,o)) ),
inference(superposition,[],[f156,f61]) ).
fof(f455,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,sF10,X6,X7,X8,e1(sF2,o),X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF2,o),X6,X7,X8,e1(sF2,sF1),X9) ),
inference(superposition,[],[f314,f65]) ).
fof(f459,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(sF2,o),X5,X6,X7,X8,e1(sF4,o),e2(sF4,sF1))
| state(X0,X1,X2,X3,X4,h(sF4,o),X5,X6,X7,X8,e1(sF2,o),e2(sF2,sF1)) ),
inference(superposition,[],[f195,f53]) ).
fof(f460,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(sF4,o),X5,X6,X7,X8,e1(sF8,o),e2(sF8,sF1))
| state(X0,X1,X2,X3,X4,h(sF8,o),X5,X6,X7,X8,e1(sF4,o),e2(sF4,sF1)) ),
inference(superposition,[],[f195,f61]) ).
fof(f461,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,h(sF4,o),X5,X6,X7,X8,e1(sF8,o),e2(sF8,sF1))
| state(X0,X1,X2,X3,X4,sF9,X5,X6,X7,X8,e1(sF4,o),e2(sF4,sF1)) ),
inference(forward_demodulation,[],[f460,f63]) ).
fof(f462,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,sF13,e1(sF4,o),X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF4,o),e1(sF4,sF1),X9) ),
inference(superposition,[],[f356,f71]) ).
fof(f470,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF4,sF1),X3,X4,X5,X6,X7,X8,e1(sF4,o),e2(sF8,o))
| state(X0,X1,X2,v3(sF4,o),X3,X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1)) ),
inference(superposition,[],[f89,f61]) ).
fof(f490,plain,
state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(o)),e2(s(s(s(s(o)))),s(s(s(o))))),
inference(resolution,[],[f42,f10]) ).
fof(f495,plain,
state(bb(o,sF1),v1(o,o),v2(o,s(s(sF1))),v3(s(sF1),o),v4(s(sF1),s(s(sF1))),h(s(sF1),sF1),s1(s(s(sF1)),sF1),s2(s(s(sF1)),s(sF1)),s3(s(s(s(sF1))),o),s4(s(s(s(sF1))),s(sF1)),e1(s(s(s(sF1))),sF1),e2(s(s(s(sF1))),s(s(sF1)))),
inference(forward_demodulation,[],[f490,f47]) ).
fof(f499,plain,
state(bb(o,sF1),v1(o,o),v2(o,s(sF2)),v3(sF2,o),v4(sF2,s(sF2)),h(sF2,sF1),s1(s(sF2),sF1),s2(s(sF2),sF2),s3(s(s(sF2)),o),s4(s(s(sF2)),sF2),e1(s(s(sF2)),sF1),e2(s(s(sF2)),s(sF2))),
inference(forward_demodulation,[],[f495,f49]) ).
fof(f503,plain,
state(bb(o,sF1),v1(o,o),v2(o,sF4),v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF1),s2(sF4,sF2),s3(s(sF4),o),s4(s(sF4),sF2),e1(s(sF4),sF1),e2(s(sF4),sF4)),
inference(forward_demodulation,[],[f499,f53]) ).
fof(f507,plain,
state(bb(o,sF1),v1(o,o),v2(o,sF4),v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF1),s2(sF4,sF2),s3(sF8,o),s4(sF8,sF2),e1(sF8,sF1),e2(sF8,sF4)),
inference(forward_demodulation,[],[f503,f61]) ).
fof(f511,plain,
state(bb(o,sF1),v1(o,o),v2(o,sF4),v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF1),s2(sF4,sF2),s3(sF8,o),s4(sF8,sF2),e1(sF8,sF1),sF15),
inference(forward_demodulation,[],[f507,f75]) ).
fof(f513,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF1),s2(sF4,sF2),s3(sF8,o),s4(sF8,sF2),e1(sF8,sF1),sF15),
inference(forward_demodulation,[],[f511,f55]) ).
fof(f583,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,sF1),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2))
| state(X0,X1,X2,X3,v4(sF4,sF2),X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1)) ),
inference(superposition,[],[f142,f61]) ).
fof(f584,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,sF1),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2))
| state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1)) ),
inference(forward_demodulation,[],[f583,f59]) ).
fof(f592,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF4,sF1),X3,X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2))
| state(X0,X1,X2,v3(sF4,sF2),X3,X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1)) ),
inference(superposition,[],[f157,f61]) ).
fof(f599,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,sF11,X7,X8,e1(sF2,sF1),X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,sF1),X7,X8,e1(sF2,sF2),X9) ),
inference(superposition,[],[f336,f67]) ).
fof(f604,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF2,sF2),X4,X5,X6,X7,X8,e1(sF2,sF4),e2(sF4,sF4))
| state(X0,X1,X2,X3,v4(sF2,sF4),X4,X5,X6,X7,X8,e1(sF2,sF2),e2(sF4,sF2)) ),
inference(superposition,[],[f143,f53]) ).
fof(f622,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF4,sF2),X6,X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,sF4),X6,X7,X8,e1(sF4,sF2),X9) ),
inference(superposition,[],[f331,f73]) ).
fof(f623,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF1),s2(sF4,sF2),s3(sF8,o),s4(sF8,sF1),e1(sF8,sF2),sF15),
inference(resolution,[],[f357,f513]) ).
fof(f625,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,sF2),X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,sF4),X7,X8,e1(sF4,sF2),X9) ),
inference(superposition,[],[f366,f73]) ).
fof(f626,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,sF12,X8,e1(sF2,sF2),X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,s3(sF2,sF2),X8,e1(sF2,sF4),X9) ),
inference(superposition,[],[f351,f69]) ).
fof(f628,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,s1(sF2,sF4),X6,X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,s1(sF4,sF4),X6,X7,X8,e1(sF2,sF4),X9) ),
inference(superposition,[],[f380,f73]) ).
fof(f676,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF2,sF2),X9)
| state(X0,X1,X2,X3,v4(sF2,sF2),X4,X5,X6,X7,X8,e1(sF8,sF2),X9) ),
inference(superposition,[],[f230,f59]) ).
fof(f680,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,s2(sF2,sF4),X7,X8,sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,s2(sF4,sF4),X7,X8,e1(sF2,sF4),X9) ),
inference(superposition,[],[f401,f73]) ).
fof(f710,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF2,sF4),sF14,X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF4,sF4),e1(sF2,sF4),X9) ),
inference(superposition,[],[f416,f73]) ).
fof(f711,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,sF13,e1(sF2,sF1),X9)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,s4(sF2,sF1),e1(sF4,sF1),X9) ),
inference(superposition,[],[f372,f71]) ).
fof(f715,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF2,sF4),X4,X5,X6,X7,X8,e1(sF2,sF2),e2(sF4,sF2))
| state(X0,X1,X2,X3,v4(sF2,sF2),X4,X5,X6,X7,X8,e1(sF2,sF4),e2(sF4,sF4)) ),
inference(superposition,[],[f79,f53]) ).
fof(f716,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,sF4),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2))
| state(X0,X1,X2,X3,v4(sF4,sF2),X4,X5,X6,X7,X8,e1(sF4,sF4),e2(sF8,sF4)) ),
inference(superposition,[],[f79,f61]) ).
fof(f717,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( state(X0,X1,X2,X3,v4(sF4,sF2),X4,X5,X6,X7,X8,e1(sF4,sF4),sF15)
| ~ state(X0,X1,X2,X3,v4(sF4,sF4),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2)) ),
inference(forward_demodulation,[],[f716,f75]) ).
fof(f718,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( state(X0,X1,X2,X3,v4(sF4,sF2),X4,X5,X6,X7,X8,sF14,sF15)
| ~ state(X0,X1,X2,X3,v4(sF4,sF4),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2)) ),
inference(forward_demodulation,[],[f717,f73]) ).
fof(f719,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,sF4),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2))
| state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,sF14,sF15) ),
inference(forward_demodulation,[],[f718,f59]) ).
fof(f725,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,v4(sF4,sF2),X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1))
| state(X0,X1,X2,X3,v4(sF4,sF1),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2)) ),
inference(superposition,[],[f78,f61]) ).
fof(f726,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,sF7,X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1))
| state(X0,X1,X2,X3,v4(sF4,sF1),X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2)) ),
inference(forward_demodulation,[],[f725,f59]) ).
fof(f768,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(X0,X1,X2,v3(sF4,sF2),X3,X4,X5,X6,X7,X8,e1(sF4,sF1),e2(sF8,sF1))
| state(X0,X1,X2,v3(sF4,sF1),X3,X4,X5,X6,X7,X8,e1(sF4,sF2),e2(sF8,sF2)) ),
inference(superposition,[],[f90,f61]) ).
fof(f1117,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,sF14,sF15)
| state(X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,e1(sF8,sF4),e2(sF4,sF4)) ),
inference(superposition,[],[f212,f75]) ).
fof(f1122,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF1),s2(sF8,sF2),s3(sF8,o),s4(sF8,sF1),e1(sF4,sF2),sF15),
inference(resolution,[],[f623,f402]) ).
fof(f1150,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(bb(o,sF1),X0,X1,X2,X3,X4,X5,X6,X7,X8,e1(o,o),e2(sF1,o))
| state(bb(o,o),X0,X1,X2,X3,X4,X5,X6,X7,X8,e1(o,s(sF1)),e2(sF1,s(sF1))) ),
inference(superposition,[],[f425,f47]) ).
fof(f1156,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( state(bb(o,o),X0,X1,X2,X3,X4,X5,X6,X7,X8,e1(o,sF2),e2(sF1,sF2))
| ~ state(bb(o,sF1),X0,X1,X2,X3,X4,X5,X6,X7,X8,e1(o,o),e2(sF1,o)) ),
inference(forward_demodulation,[],[f1150,f49]) ).
fof(f1157,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ state(bb(o,sF1),X0,X1,X2,X3,X4,X5,X6,X7,X8,e1(o,o),e2(sF1,o))
| state(sF0,X0,X1,X2,X3,X4,X5,X6,X7,X8,e1(o,sF2),e2(sF1,sF2)) ),
inference(forward_demodulation,[],[f1156,f45]) ).
fof(f1219,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF2),s3(sF8,o),s4(sF8,sF1),e1(sF4,sF1),sF15),
inference(resolution,[],[f1122,f330]) ).
fof(f1377,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF2),s3(sF8,o),s4(sF4,sF1),e1(sF8,sF1),sF15),
inference(resolution,[],[f1219,f373]) ).
fof(f1379,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF2),s3(sF8,o),sF13,e1(sF8,sF1),sF15),
inference(forward_demodulation,[],[f1377,f71]) ).
fof(f1381,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF2),s3(sF8,sF1),sF13,e1(sF8,o),sF15),
inference(resolution,[],[f1379,f385]) ).
fof(f1426,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF2),s3(sF8,sF1),sF13,e1(sF8,sF4),e2(sF8,o)),
inference(resolution,[],[f1381,f213]) ).
fof(f2077,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF8,sF2),e2(sF8,o)),
inference(resolution,[],[f1426,f366]) ).
fof(f2083,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF8,o),e2(sF8,sF2)),
inference(resolution,[],[f2077,f41]) ).
fof(f2090,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF4),h(sF2,sF1),s1(sF4,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF2,o),e2(sF8,sF2)),
inference(resolution,[],[f2083,f276]) ).
fof(f2743,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF4),h(sF2,o),s1(sF4,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF2,sF2),e2(sF8,sF2)),
inference(resolution,[],[f2090,f222]) ).
fof(f2749,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF4),h(sF2,o),s1(sF4,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF8,sF2),e2(sF2,sF2)),
inference(resolution,[],[f2743,f41]) ).
fof(f2756,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF4),h(sF2,o),s1(sF8,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF4,sF2),e2(sF2,sF2)),
inference(resolution,[],[f2749,f381]) ).
fof(f2765,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF4),h(sF2,o),s1(sF8,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF2,sF2),e2(sF4,sF2)),
inference(resolution,[],[f2756,f41]) ).
fof(f2766,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF2,sF4),e2(sF4,sF4)),
inference(resolution,[],[f2765,f715]) ).
fof(f3078,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,e1(sF4,sF4),e2(sF2,sF4)),
inference(resolution,[],[f2766,f41]) ).
fof(f3079,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF8,sF4),s3(sF8,sF1),sF13,sF14,e2(sF2,sF4)),
inference(forward_demodulation,[],[f3078,f73]) ).
fof(f3080,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF4,sF4),s3(sF8,sF1),sF13,e1(sF8,sF4),e2(sF2,sF4)),
inference(resolution,[],[f3079,f327]) ).
fof(f3501,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF4,sF4),s3(sF8,sF1),sF13,e1(sF2,sF4),e2(sF8,sF4)),
inference(resolution,[],[f3080,f41]) ).
fof(f3502,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF4,sF4),s3(sF8,sF1),sF13,e1(sF2,sF4),sF15),
inference(forward_demodulation,[],[f3501,f75]) ).
fof(f3505,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF4,sF4),sF15),
inference(resolution,[],[f3502,f323]) ).
fof(f3507,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF2,sF4),s3(sF8,sF1),sF13,sF14,sF15),
inference(forward_demodulation,[],[f3505,f73]) ).
fof(f3509,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF2),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF8,sF4),e2(sF4,sF4)),
inference(resolution,[],[f3507,f1117]) ).
fof(f3510,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF2,sF2),h(sF2,o),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF8,sF2),e2(sF4,sF4)),
inference(resolution,[],[f3509,f331]) ).
fof(f3515,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF2),h(sF2,o),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF2,sF2),e2(sF4,sF4)),
inference(resolution,[],[f3510,f249]) ).
fof(f3519,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,o),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF2,sF2),e2(sF4,sF4)),
inference(forward_demodulation,[],[f3515,f59]) ).
fof(f3521,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF2,o),e2(sF4,sF4)),
inference(resolution,[],[f3519,f208]) ).
fof(f3594,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF4,sF4),e2(sF2,o)),
inference(resolution,[],[f3521,f41]) ).
fof(f3595,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,sF1),sF13,sF14,e2(sF2,o)),
inference(forward_demodulation,[],[f3594,f73]) ).
fof(f3597,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF4,sF4),s3(sF8,sF1),sF13,e1(sF2,sF4),e2(sF2,o)),
inference(resolution,[],[f3595,f680]) ).
fof(f3600,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF8,sF1),sF13,e1(sF2,sF1),e2(sF2,o)),
inference(resolution,[],[f3597,f207]) ).
fof(f3605,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF8,sF1),s4(sF2,sF1),e1(sF4,sF1),e2(sF2,o)),
inference(resolution,[],[f3600,f711]) ).
fof(f3612,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF8,sF1),s4(sF2,sF1),e1(sF2,o),e2(sF4,sF1)),
inference(resolution,[],[f3605,f41]) ).
fof(f3656,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF8,sF1),s4(sF2,o),e1(sF2,sF1),e2(sF4,sF1)),
inference(resolution,[],[f3612,f356]) ).
fof(f3660,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF8,sF1),s4(sF2,o),e1(sF4,sF1),e2(sF2,sF1)),
inference(resolution,[],[f3656,f41]) ).
fof(f3684,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF4,sF1),s4(sF2,o),e1(sF8,sF1),e2(sF2,sF1)),
inference(resolution,[],[f3660,f345]) ).
fof(f3728,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF4,sF1),s4(sF2,o),e1(sF2,sF1),e2(sF8,sF1)),
inference(resolution,[],[f3684,f41]) ).
fof(f3734,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f3728,f344]) ).
fof(f3777,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f3734,f726]) ).
fof(f4569,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF4),e2(sF8,sF2)),
inference(resolution,[],[f3777,f337]) ).
fof(f4571,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),sF14,e2(sF8,sF2)),
inference(forward_demodulation,[],[f4569,f73]) ).
fof(f4574,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),e1(sF8,sF2),e2(sF4,sF4)),
inference(resolution,[],[f4571,f212]) ).
fof(f4575,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),e1(sF8,sF4),e2(sF4,sF4)),
inference(resolution,[],[f4574,f316]) ).
fof(f4580,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF4),e2(sF8,sF4)),
inference(resolution,[],[f4575,f41]) ).
fof(f4581,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF4),sF15),
inference(forward_demodulation,[],[f4580,f75]) ).
fof(f4582,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF4,sF2),s3(sF2,sF1),s4(sF2,o),sF14,sF15),
inference(forward_demodulation,[],[f4581,f73]) ).
fof(f4583,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF4,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF2),sF15),
inference(resolution,[],[f4582,f625]) ).
fof(f4587,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF4,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF8,sF4),e2(sF4,sF2)),
inference(resolution,[],[f4583,f213]) ).
fof(f4592,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF4),e2(sF4,sF2)),
inference(resolution,[],[f4587,f402]) ).
fof(f4595,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),sF14,e2(sF4,sF2)),
inference(forward_demodulation,[],[f4592,f73]) ).
fof(f4597,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF2),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF2),e2(sF4,sF4)),
inference(resolution,[],[f4595,f212]) ).
fof(f4598,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF8,sF2),e2(sF4,sF4)),
inference(resolution,[],[f4597,f267]) ).
fof(f4611,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF4),e2(sF8,sF2)),
inference(resolution,[],[f4598,f41]) ).
fof(f4612,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),sF14,e2(sF8,sF2)),
inference(forward_demodulation,[],[f4611,f73]) ).
fof(f4613,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f4612,f622]) ).
fof(f4617,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f4613,f584]) ).
fof(f4620,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,sF1),s4(sF2,o),e1(sF4,o),e2(sF8,o)),
inference(resolution,[],[f4617,f442]) ).
fof(f4625,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,sF1),s4(sF4,o),e1(sF2,o),e2(sF8,o)),
inference(resolution,[],[f4620,f416]) ).
fof(f4628,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF4,o),e1(sF2,sF1),e2(sF8,o)),
inference(resolution,[],[f4625,f349]) ).
fof(f4641,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF4,o),e1(sF2,sF4),e2(sF8,o)),
inference(resolution,[],[f4628,f221]) ).
fof(f4666,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF4,o),e1(sF4,sF4),e2(sF8,o)),
inference(resolution,[],[f4641,f266]) ).
fof(f4670,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF4,o),sF14,e2(sF8,o)),
inference(forward_demodulation,[],[f4666,f73]) ).
fof(f4673,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF4,o),e1(sF8,o),e2(sF4,sF4)),
inference(resolution,[],[f4670,f212]) ).
fof(f4692,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF8,o),e1(sF4,o),e2(sF4,sF4)),
inference(resolution,[],[f4673,f417]) ).
fof(f4695,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF8,o),e1(sF2,o),e2(sF4,sF4)),
inference(resolution,[],[f4692,f408]) ).
fof(f4702,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF8,o),e1(sF2,sF2),e2(sF4,sF4)),
inference(resolution,[],[f4695,f222]) ).
fof(f5280,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF8,o),e1(sF4,sF4),e2(sF2,sF2)),
inference(resolution,[],[f4702,f41]) ).
fof(f5281,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF8,o),sF14,e2(sF2,sF2)),
inference(forward_demodulation,[],[f5280,f73]) ).
fof(f5283,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF4,sF4),s3(sF4,o),s4(sF8,o),e1(sF8,sF4),e2(sF2,sF2)),
inference(resolution,[],[f5281,f327]) ).
fof(f5296,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF4,sF4),s3(sF4,o),s4(sF8,o),e1(sF2,sF2),e2(sF8,sF4)),
inference(resolution,[],[f5283,f41]) ).
fof(f5297,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF4,sF4),s3(sF4,o),s4(sF8,o),e1(sF2,sF2),sF15),
inference(forward_demodulation,[],[f5296,f75]) ).
fof(f5299,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF2),s2(sF4,sF4),s3(sF4,o),s4(sF8,o),e1(sF2,sF4),sF15),
inference(resolution,[],[f5297,f316]) ).
fof(f5305,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF4,o),s4(sF8,o),e1(sF4,sF4),sF15),
inference(resolution,[],[f5299,f323]) ).
fof(f5307,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF4,o),s4(sF8,o),sF14,sF15),
inference(forward_demodulation,[],[f5305,f73]) ).
fof(f5308,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF4,o),s4(sF8,o),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f5307,f150]) ).
fof(f5721,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF4,o),s4(sF8,o),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f5308,f592]) ).
fof(f5726,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF4,o),s4(sF8,o),e1(sF8,sF1),e2(sF4,sF1)),
inference(resolution,[],[f5721,f41]) ).
fof(f5730,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF4,o),s4(sF8,sF1),e1(sF8,o),e2(sF4,sF1)),
inference(resolution,[],[f5726,f392]) ).
fof(f5732,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF8,sF1),e1(sF4,o),e2(sF4,sF1)),
inference(resolution,[],[f5730,f409]) ).
fof(f5738,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF8,sF1),e1(sF4,sF1),e2(sF4,o)),
inference(resolution,[],[f5732,f41]) ).
fof(f5918,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF4,sF1),e1(sF8,sF1),e2(sF4,o)),
inference(resolution,[],[f5738,f373]) ).
fof(f5920,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),sF13,e1(sF8,sF1),e2(sF4,o)),
inference(forward_demodulation,[],[f5918,f71]) ).
fof(f5921,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF8,o),e2(sF4,o)),
inference(resolution,[],[f5920,f385]) ).
fof(f5925,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,sF1),sF13,e1(sF4,o),e2(sF8,o)),
inference(resolution,[],[f5921,f41]) ).
fof(f5926,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,sF1),s4(sF4,o),e1(sF4,sF1),e2(sF8,o)),
inference(resolution,[],[f5925,f462]) ).
fof(f5942,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,sF1),s4(sF4,o),e1(sF8,o),e2(sF4,sF1)),
inference(resolution,[],[f5926,f41]) ).
fof(f5944,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF4,o),e1(sF8,sF1),e2(sF4,sF1)),
inference(resolution,[],[f5942,f349]) ).
fof(f5948,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF4,o),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f5944,f41]) ).
fof(f6130,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),v4(sF4,sF4),h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF4,o),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f5948,f768]) ).
fof(f6136,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF2),s2(sF2,sF4),s3(sF8,o),s4(sF4,o),sF14,sF15),
inference(resolution,[],[f6130,f719]) ).
fof(f6139,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF2),s2(sF4,sF4),s3(sF8,o),s4(sF4,o),e1(sF2,sF4),sF15),
inference(resolution,[],[f6136,f680]) ).
fof(f6141,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF4,sF4),s3(sF8,o),s4(sF4,o),e1(sF2,sF2),sF15),
inference(resolution,[],[f6139,f331]) ).
fof(f6149,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF4,sF4),s3(sF8,o),s4(sF4,o),e1(sF8,sF4),e2(sF2,sF2)),
inference(resolution,[],[f6141,f213]) ).
fof(f6150,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF8,sF4),s3(sF8,o),s4(sF4,o),e1(sF4,sF4),e2(sF2,sF2)),
inference(resolution,[],[f6149,f402]) ).
fof(f6153,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF8,sF4),s3(sF8,o),s4(sF4,o),sF14,e2(sF2,sF2)),
inference(forward_demodulation,[],[f6150,f73]) ).
fof(f6156,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),s2(sF8,sF4),s3(sF8,o),s4(sF4,o),e1(sF2,sF2),e2(sF4,sF4)),
inference(resolution,[],[f6153,f212]) ).
fof(f6166,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF8,o),s4(sF4,o),e1(sF2,o),e2(sF4,sF4)),
inference(resolution,[],[f6156,f208]) ).
fof(f6262,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF8,o),s4(sF2,o),e1(sF4,o),e2(sF4,sF4)),
inference(resolution,[],[f6166,f372]) ).
fof(f6265,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF2,o),e1(sF8,o),e2(sF4,sF4)),
inference(resolution,[],[f6262,f345]) ).
fof(f6273,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF2,o),e1(sF4,sF4),e2(sF8,o)),
inference(resolution,[],[f6265,f41]) ).
fof(f6274,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF2,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF2,o),sF14,e2(sF8,o)),
inference(forward_demodulation,[],[f6273,f73]) ).
fof(f6275,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF4,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF2,o),e1(sF2,sF4),e2(sF8,o)),
inference(resolution,[],[f6274,f628]) ).
fof(f6280,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF2,o),e1(sF2,sF1),e2(sF8,o)),
inference(resolution,[],[f6275,f207]) ).
fof(f6285,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF4,o),s4(sF2,sF1),e1(sF2,o),e2(sF8,o)),
inference(resolution,[],[f6280,f392]) ).
fof(f6288,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,o),e2(sF8,o)),
inference(resolution,[],[f6285,f344]) ).
fof(f6296,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f6288,f470]) ).
fof(f6300,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f6296,f726]) ).
fof(f6342,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF4),e2(sF8,sF2)),
inference(resolution,[],[f6300,f316]) ).
fof(f6345,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF4),s3(sF2,o),s4(sF2,sF1),sF14,e2(sF8,sF2)),
inference(forward_demodulation,[],[f6342,f73]) ).
fof(f6348,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF8,sF2),e2(sF4,sF4)),
inference(resolution,[],[f6345,f212]) ).
fof(f6350,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF8,sF4),e2(sF4,sF4)),
inference(resolution,[],[f6348,f337]) ).
fof(f6354,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF4),e2(sF8,sF4)),
inference(resolution,[],[f6350,f41]) ).
fof(f6355,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF4),sF15),
inference(forward_demodulation,[],[f6354,f75]) ).
fof(f6356,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF2),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),sF14,sF15),
inference(forward_demodulation,[],[f6355,f73]) ).
fof(f6357,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF2),sF15),
inference(resolution,[],[f6356,f622]) ).
fof(f6361,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF4,sF4),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF8,sF4),e2(sF4,sF2)),
inference(resolution,[],[f6357,f213]) ).
fof(f6365,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF4),e2(sF4,sF2)),
inference(resolution,[],[f6361,f381]) ).
fof(f6369,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),sF14,e2(sF4,sF2)),
inference(forward_demodulation,[],[f6365,f73]) ).
fof(f6371,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF8,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF2),e2(sF4,sF4)),
inference(resolution,[],[f6369,f212]) ).
fof(f6373,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF8,sF2),e2(sF4,sF4)),
inference(resolution,[],[f6371,f324]) ).
fof(f6385,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF2),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF4),e2(sF8,sF2)),
inference(resolution,[],[f6373,f41]) ).
fof(f6386,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF2),s3(sF2,o),s4(sF2,sF1),sF14,e2(sF8,sF2)),
inference(forward_demodulation,[],[f6385,f73]) ).
fof(f6388,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),v4(sF4,sF1),h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f6386,f625]) ).
fof(f6390,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,o),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f6388,f584]) ).
fof(f6394,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF2,o),s4(sF2,sF1),e1(sF4,o),e2(sF8,o)),
inference(resolution,[],[f6390,f442]) ).
fof(f6419,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF4,o),s4(sF2,sF1),e1(sF2,o),e2(sF8,o)),
inference(resolution,[],[f6394,f408]) ).
fof(f6423,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF2),s1(sF8,sF4),s2(sF4,sF4),s3(sF4,o),s4(sF2,o),e1(sF2,sF1),e2(sF8,o)),
inference(resolution,[],[f6419,f356]) ).
fof(f6427,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF4,sF4),s3(sF4,o),s4(sF2,o),e1(sF2,sF4),e2(sF8,o)),
inference(resolution,[],[f6423,f221]) ).
fof(f6497,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF4,o),s4(sF2,o),e1(sF4,sF4),e2(sF8,o)),
inference(resolution,[],[f6427,f323]) ).
fof(f6499,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF4,o),s4(sF2,o),sF14,e2(sF8,o)),
inference(forward_demodulation,[],[f6497,f73]) ).
fof(f6502,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF4,o),s4(sF2,o),e1(sF8,o),e2(sF4,sF4)),
inference(resolution,[],[f6499,f212]) ).
fof(f6503,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,o),s4(sF2,o),e1(sF4,o),e2(sF4,sF4)),
inference(resolution,[],[f6502,f409]) ).
fof(f6507,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,sF1),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,o),s4(sF4,o),e1(sF2,o),e2(sF4,sF4)),
inference(resolution,[],[f6503,f416]) ).
fof(f6525,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF8,sF4),s2(sF2,sF4),s3(sF8,o),s4(sF4,o),e1(sF2,sF2),e2(sF4,sF4)),
inference(resolution,[],[f6507,f222]) ).
fof(f6629,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF8,sF4),s2(sF2,sF2),s3(sF8,o),s4(sF4,o),e1(sF2,sF4),e2(sF4,sF4)),
inference(resolution,[],[f6525,f337]) ).
fof(f6632,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF8,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF2,sF4),e2(sF4,sF4)),
inference(forward_demodulation,[],[f6629,f67]) ).
fof(f6635,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF8,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF4,sF4),e2(sF2,sF4)),
inference(resolution,[],[f6632,f41]) ).
fof(f6636,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF8,sF4),sF11,s3(sF8,o),s4(sF4,o),sF14,e2(sF2,sF4)),
inference(forward_demodulation,[],[f6635,f73]) ).
fof(f6637,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF4,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF8,sF4),e2(sF2,sF4)),
inference(resolution,[],[f6636,f270]) ).
fof(f6640,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF4,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF2,sF4),e2(sF8,sF4)),
inference(resolution,[],[f6637,f41]) ).
fof(f6641,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF4,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF2,sF4),sF15),
inference(forward_demodulation,[],[f6640,f75]) ).
fof(f6643,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF4,sF4),sF15),
inference(resolution,[],[f6641,f266]) ).
fof(f6647,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),sF7,h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,o),s4(sF4,o),sF14,sF15),
inference(forward_demodulation,[],[f6643,f73]) ).
fof(f6649,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF1),v4(sF4,sF4),h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f6647,f150]) ).
fof(f6654,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF4,sF1),e2(sF8,sF1)),
inference(resolution,[],[f6649,f592]) ).
fof(f6660,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,o),s4(sF4,o),e1(sF8,sF1),e2(sF4,sF1)),
inference(resolution,[],[f6654,f41]) ).
fof(f6672,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,sF1),s4(sF4,o),e1(sF8,o),e2(sF4,sF1)),
inference(resolution,[],[f6660,f385]) ).
fof(f6675,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF2,o),s1(sF2,sF4),sF11,s3(sF8,sF1),s4(sF8,o),e1(sF4,o),e2(sF4,sF1)),
inference(resolution,[],[f6672,f417]) ).
fof(f6679,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF4,o),s1(sF2,sF4),sF11,s3(sF8,sF1),s4(sF8,o),e1(sF2,o),e2(sF2,sF1)),
inference(resolution,[],[f6675,f459]) ).
fof(f6684,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF4,o),s1(sF2,sF4),sF11,s3(sF8,sF1),s4(sF8,o),e1(sF2,sF1),e2(sF2,o)),
inference(resolution,[],[f6679,f41]) ).
fof(f6693,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF4,o),s1(sF2,sF4),s2(sF2,sF1),s3(sF8,sF1),s4(sF8,o),e1(sF2,sF2),e2(sF2,o)),
inference(resolution,[],[f6684,f599]) ).
fof(f6705,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF4,sF4),h(sF4,o),s1(sF2,sF2),s2(sF2,sF1),s3(sF8,sF1),s4(sF8,o),e1(sF2,sF4),e2(sF2,o)),
inference(resolution,[],[f6693,f316]) ).
fof(f6712,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF2,sF4),h(sF4,o),s1(sF2,sF2),s2(sF2,sF1),s3(sF8,sF1),s4(sF8,o),e1(sF8,sF4),e2(sF2,o)),
inference(resolution,[],[f6705,f230]) ).
fof(f7000,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF2,sF4),h(sF4,o),s1(sF2,sF2),s2(sF2,sF1),s3(sF8,sF1),s4(sF8,o),e1(sF2,o),e2(sF8,sF4)),
inference(resolution,[],[f6712,f41]) ).
fof(f7001,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF2,sF4),h(sF4,o),s1(sF2,sF2),s2(sF2,sF1),s3(sF8,sF1),s4(sF8,o),e1(sF2,o),sF15),
inference(forward_demodulation,[],[f7000,f75]) ).
fof(f7003,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF2,sF4),h(sF4,o),s1(sF2,sF2),s2(sF2,o),s3(sF8,sF1),s4(sF8,o),e1(sF2,sF1),sF15),
inference(resolution,[],[f7001,f335]) ).
fof(f7005,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF2,sF4),h(sF4,o),s1(sF2,sF1),s2(sF2,o),s3(sF8,sF1),s4(sF8,o),e1(sF2,sF2),sF15),
inference(resolution,[],[f7003,f315]) ).
fof(f7008,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF4,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF1),s4(sF8,o),e1(sF2,sF2),sF15),
inference(forward_demodulation,[],[f7005,f65]) ).
fof(f7010,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF1),s4(sF8,o),e1(sF8,sF2),sF15),
inference(resolution,[],[f7008,f240]) ).
fof(f7013,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF2),s4(sF8,o),e1(sF8,sF1),sF15),
inference(resolution,[],[f7010,f386]) ).
fof(f7016,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF2),s4(sF8,sF1),e1(sF8,o),sF15),
inference(resolution,[],[f7013,f392]) ).
fof(f7024,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF2),s4(sF8,sF1),e1(sF8,sF4),e2(sF8,o)),
inference(resolution,[],[f7016,f213]) ).
fof(f7928,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF4),s4(sF8,sF1),e1(sF8,sF2),e2(sF8,o)),
inference(resolution,[],[f7024,f387]) ).
fof(f7933,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF4),s4(sF8,sF2),e1(sF8,sF1),e2(sF8,o)),
inference(resolution,[],[f7928,f393]) ).
fof(f7936,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),h(sF4,o),sF10,s2(sF2,o),s3(sF8,sF4),s4(sF8,sF2),e1(sF8,o),e2(sF8,sF1)),
inference(resolution,[],[f7933,f41]) ).
fof(f7937,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF2,o),s3(sF8,sF4),s4(sF8,sF2),e1(sF4,o),e2(sF4,sF1)),
inference(resolution,[],[f7936,f461]) ).
fof(f7940,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,o),s3(sF8,sF4),s4(sF8,sF2),e1(sF2,o),e2(sF4,sF1)),
inference(resolution,[],[f7937,f401]) ).
fof(f7942,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,s1(sF2,o),s2(sF4,o),s3(sF8,sF4),s4(sF8,sF2),e1(sF2,sF1),e2(sF4,sF1)),
inference(resolution,[],[f7940,f455]) ).
fof(f7948,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,s1(sF2,o),s2(sF4,o),s3(sF8,sF4),s4(sF8,sF2),e1(sF4,sF1),e2(sF2,sF1)),
inference(resolution,[],[f7942,f41]) ).
fof(f8062,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,s1(sF2,o),s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF4,o),e2(sF2,sF1)),
inference(resolution,[],[f7948,f364]) ).
fof(f8066,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,s1(sF2,o),s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF2,sF1),e2(sF4,o)),
inference(resolution,[],[f8062,f41]) ).
fof(f8099,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,s1(sF2,sF1),s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF2,o),e2(sF4,o)),
inference(resolution,[],[f8066,f329]) ).
fof(f8102,plain,
state(bb(o,sF1),v1(o,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF2,o),e2(sF4,o)),
inference(forward_demodulation,[],[f8099,f65]) ).
fof(f8104,plain,
state(bb(o,sF1),v1(sF1,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(o,o),e2(sF4,o)),
inference(resolution,[],[f8102,f310]) ).
fof(f8107,plain,
state(bb(o,sF1),v1(sF1,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF4,o),e2(o,o)),
inference(resolution,[],[f8104,f41]) ).
fof(f8108,plain,
state(bb(o,sF1),v1(sF2,o),sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF1,o),e2(o,o)),
inference(resolution,[],[f8107,f309]) ).
fof(f8111,plain,
state(bb(o,sF1),sF3,sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF1,o),e2(o,o)),
inference(forward_demodulation,[],[f8108,f51]) ).
fof(f8113,plain,
state(bb(o,sF1),sF3,sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(o,o),e2(sF1,o)),
inference(resolution,[],[f8111,f41]) ).
fof(f8117,plain,
state(sF0,sF3,sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(o,sF2),e2(sF1,sF2)),
inference(resolution,[],[f8113,f1157]) ).
fof(f8121,plain,
state(sF0,sF3,sF5,v3(sF2,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF1,sF2),e2(o,sF2)),
inference(resolution,[],[f8117,f41]) ).
fof(f8122,plain,
state(sF0,sF3,sF5,v3(sF1,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF8,sF2),e1(sF4,sF2),e2(o,sF2)),
inference(resolution,[],[f8121,f241]) ).
fof(f8126,plain,
state(sF0,sF3,sF5,v3(sF1,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF4),s4(sF4,sF2),e1(sF8,sF2),e2(o,sF2)),
inference(resolution,[],[f8122,f373]) ).
fof(f8129,plain,
state(sF0,sF3,sF5,v3(sF1,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF2),s4(sF4,sF2),e1(sF8,sF4),e2(o,sF2)),
inference(resolution,[],[f8126,f351]) ).
fof(f8137,plain,
state(sF0,sF3,sF5,v3(sF1,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF2),s4(sF4,sF2),e1(o,sF2),e2(sF8,sF4)),
inference(resolution,[],[f8129,f41]) ).
fof(f8138,plain,
state(sF0,sF3,sF5,v3(sF1,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF2),s4(sF4,sF2),e1(o,sF2),sF15),
inference(forward_demodulation,[],[f8137,f75]) ).
fof(f8139,plain,
state(sF0,sF3,sF5,v3(o,sF2),v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF2),s4(sF4,sF2),e1(sF2,sF2),sF15),
inference(resolution,[],[f8138,f242]) ).
fof(f8141,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF2),s4(sF4,sF2),e1(sF2,sF2),sF15),
inference(forward_demodulation,[],[f8139,f57]) ).
fof(f8144,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF4,sF1),s3(sF8,sF2),s4(sF2,sF2),e1(sF4,sF2),sF15),
inference(resolution,[],[f8141,f372]) ).
fof(f8146,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF4,sF2),s3(sF8,sF2),s4(sF2,sF2),e1(sF4,sF1),sF15),
inference(resolution,[],[f8144,f365]) ).
fof(f8155,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF4,sF2),s3(sF8,sF2),s4(sF2,sF2),e1(sF8,sF4),e2(sF4,sF1)),
inference(resolution,[],[f8146,f213]) ).
fof(f8180,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,s2(sF4,sF2),s3(sF8,sF2),s4(sF2,sF2),e1(sF2,sF4),e2(sF4,sF1)),
inference(resolution,[],[f8155,f249]) ).
fof(f8786,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,s2(sF4,sF2),s3(sF8,sF2),s4(sF2,sF4),e1(sF2,sF2),e2(sF4,sF1)),
inference(resolution,[],[f8180,f394]) ).
fof(f8790,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,s2(sF2,sF2),s3(sF8,sF2),s4(sF2,sF4),e1(sF4,sF2),e2(sF4,sF1)),
inference(resolution,[],[f8786,f323]) ).
fof(f8793,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,sF11,s3(sF8,sF2),s4(sF2,sF4),e1(sF4,sF2),e2(sF4,sF1)),
inference(forward_demodulation,[],[f8790,f67]) ).
fof(f8795,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,sF11,s3(sF4,sF2),s4(sF2,sF4),e1(sF8,sF2),e2(sF4,sF1)),
inference(resolution,[],[f8793,f345]) ).
fof(f8799,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,sF11,s3(sF4,sF2),s4(sF2,sF4),e1(sF4,sF1),e2(sF8,sF2)),
inference(resolution,[],[f8795,f41]) ).
fof(f8801,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,sF11,s3(sF4,sF1),s4(sF2,sF4),e1(sF4,sF2),e2(sF8,sF2)),
inference(resolution,[],[f8799,f350]) ).
fof(f8803,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF1),s4(sF2,sF4),sF14,sF15),
inference(resolution,[],[f8801,f719]) ).
fof(f8808,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF1),s4(sF4,sF4),e1(sF2,sF4),sF15),
inference(resolution,[],[f8803,f710]) ).
fof(f8813,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF1),s4(sF4,sF4),e1(sF8,sF4),e2(sF2,sF4)),
inference(resolution,[],[f8808,f213]) ).
fof(f8815,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF1),s4(sF8,sF4),e1(sF4,sF4),e2(sF2,sF4)),
inference(resolution,[],[f8813,f417]) ).
fof(f8818,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF1),s4(sF8,sF4),sF14,e2(sF2,sF4)),
inference(forward_demodulation,[],[f8815,f73]) ).
fof(f8820,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF1),s4(sF8,sF4),e1(sF2,sF4),e2(sF4,sF4)),
inference(resolution,[],[f8818,f212]) ).
fof(f8822,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF2,sF4),s3(sF4,sF1),s4(sF8,sF4),e1(sF2,sF2),e2(sF4,sF4)),
inference(resolution,[],[f8820,f369]) ).
fof(f8841,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF2,sF4),s3(sF4,sF1),s4(sF8,sF4),e1(sF4,sF4),e2(sF2,sF2)),
inference(resolution,[],[f8822,f41]) ).
fof(f8842,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF2,sF4),s3(sF4,sF1),s4(sF8,sF4),sF14,e2(sF2,sF2)),
inference(forward_demodulation,[],[f8841,f73]) ).
fof(f8844,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF4,sF4),s3(sF4,sF1),s4(sF8,sF4),e1(sF2,sF4),e2(sF2,sF2)),
inference(resolution,[],[f8842,f680]) ).
fof(f8849,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF4,sF4),s3(sF4,sF1),s4(sF8,sF4),e1(sF2,sF2),e2(sF2,sF4)),
inference(resolution,[],[f8844,f41]) ).
fof(f8852,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF4,sF4),s3(sF4,sF1),s4(sF8,sF4),e1(sF8,sF2),e2(sF2,sF4)),
inference(resolution,[],[f8849,f676]) ).
fof(f8880,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF4,sF4),s3(sF4,sF1),s4(sF8,sF2),e1(sF8,sF4),e2(sF2,sF4)),
inference(resolution,[],[f8852,f358]) ).
fof(f8883,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF8,sF4),s3(sF4,sF1),s4(sF8,sF2),e1(sF4,sF4),e2(sF2,sF4)),
inference(resolution,[],[f8880,f402]) ).
fof(f8887,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF8,sF4),s3(sF4,sF1),s4(sF8,sF2),sF14,e2(sF2,sF4)),
inference(forward_demodulation,[],[f8883,f73]) ).
fof(f8889,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF8,sF4),s3(sF4,sF1),s4(sF8,sF2),e1(sF2,sF4),e2(sF4,sF4)),
inference(resolution,[],[f8887,f212]) ).
fof(f8900,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF4),s3(sF4,sF1),s4(sF8,sF2),e1(sF2,sF2),e2(sF4,sF2)),
inference(resolution,[],[f8889,f604]) ).
fof(f8907,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF4),s3(sF4,sF1),s4(sF8,sF2),e1(sF4,sF2),e2(sF2,sF2)),
inference(resolution,[],[f8900,f41]) ).
fof(f8909,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF4),s3(sF4,sF1),s4(sF4,sF2),e1(sF8,sF2),e2(sF2,sF2)),
inference(resolution,[],[f8907,f373]) ).
fof(f8912,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF4,sF1),s4(sF4,sF2),e1(sF8,sF4),e2(sF2,sF2)),
inference(resolution,[],[f8909,f337]) ).
fof(f8920,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF4,sF1),s4(sF4,sF2),e1(sF2,sF2),e2(sF8,sF4)),
inference(resolution,[],[f8912,f41]) ).
fof(f8921,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF4,sF1),s4(sF4,sF2),e1(sF2,sF2),sF15),
inference(forward_demodulation,[],[f8920,f75]) ).
fof(f8922,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF2,sF2),s2(sF8,sF2),s3(sF4,sF1),s4(sF4,sF2),e1(sF2,sF1),sF15),
inference(resolution,[],[f8921,f334]) ).
fof(f8944,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF2,sF2),s2(sF8,sF2),s3(sF2,sF1),s4(sF4,sF2),e1(sF4,sF1),sF15),
inference(resolution,[],[f8922,f344]) ).
fof(f8957,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF2,sF2),s2(sF8,sF2),s3(sF2,sF1),s4(sF4,sF1),e1(sF4,sF2),sF15),
inference(resolution,[],[f8944,f357]) ).
fof(f8959,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF2,sF2),s2(sF8,sF2),s3(sF2,sF1),sF13,e1(sF4,sF2),sF15),
inference(forward_demodulation,[],[f8957,f71]) ).
fof(f8960,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF4,sF2),s2(sF8,sF2),s3(sF2,sF1),sF13,e1(sF2,sF2),sF15),
inference(resolution,[],[f8959,f380]) ).
fof(f8969,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF4,sF2),s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF2,sF1),sF15),
inference(resolution,[],[f8960,f386]) ).
fof(f8973,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,s1(sF4,sF2),s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF8,sF4),e2(sF2,sF1)),
inference(resolution,[],[f8969,f213]) ).
fof(f9021,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,s1(sF4,sF2),s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF2,sF4),e2(sF2,sF1)),
inference(resolution,[],[f8973,f249]) ).
fof(f11712,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,s1(sF4,sF2),s2(sF8,sF2),s3(sF2,sF4),sF13,e1(sF2,sF2),e2(sF2,sF1)),
inference(resolution,[],[f9021,f387]) ).
fof(f11714,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,s1(sF4,sF2),s2(sF8,sF2),sF12,sF13,e1(sF2,sF2),e2(sF2,sF1)),
inference(forward_demodulation,[],[f11712,f69]) ).
fof(f11715,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,s1(sF2,sF2),s2(sF8,sF2),sF12,sF13,e1(sF4,sF2),e2(sF2,sF1)),
inference(resolution,[],[f11714,f266]) ).
fof(f11722,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,s1(sF2,sF2),s2(sF8,sF2),sF12,sF13,e1(sF2,sF1),e2(sF4,sF2)),
inference(resolution,[],[f11715,f41]) ).
fof(f11726,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,s1(sF2,sF1),s2(sF8,sF2),sF12,sF13,e1(sF2,sF2),e2(sF4,sF2)),
inference(resolution,[],[f11722,f315]) ).
fof(f11729,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,s2(sF8,sF2),sF12,sF13,e1(sF2,sF2),e2(sF4,sF2)),
inference(forward_demodulation,[],[f11726,f65]) ).
fof(f11732,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF4),sF9,sF10,s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF2,sF4),e2(sF4,sF2)),
inference(resolution,[],[f11729,f626]) ).
fof(f11735,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF8,sF4),e2(sF4,sF2)),
inference(resolution,[],[f11732,f230]) ).
fof(f11741,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF4,sF2),e2(sF8,sF4)),
inference(resolution,[],[f11735,f41]) ).
fof(f11742,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF2,sF2),sF13,e1(sF4,sF2),sF15),
inference(forward_demodulation,[],[f11741,f75]) ).
fof(f11744,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF4,sF2),sF13,e1(sF2,sF2),sF15),
inference(resolution,[],[f11742,f408]) ).
fof(f11753,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF2),s3(sF4,sF2),sF13,e1(sF8,sF4),e2(sF2,sF2)),
inference(resolution,[],[f11744,f213]) ).
fof(f11758,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF4),s3(sF4,sF2),sF13,e1(sF8,sF2),e2(sF2,sF2)),
inference(resolution,[],[f11753,f366]) ).
fof(f11763,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF4),s3(sF8,sF2),sF13,e1(sF4,sF2),e2(sF2,sF2)),
inference(resolution,[],[f11758,f409]) ).
fof(f11767,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF4),sF9,sF10,s2(sF8,sF4),s3(sF8,sF2),sF13,e1(sF2,sF2),e2(sF4,sF2)),
inference(resolution,[],[f11763,f41]) ).
fof(f11870,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF8,sF4),s3(sF8,sF2),sF13,e1(sF2,sF4),e2(sF4,sF4)),
inference(resolution,[],[f11767,f715]) ).
fof(f11875,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF8,sF4),s3(sF8,sF2),sF13,e1(sF4,sF4),e2(sF2,sF4)),
inference(resolution,[],[f11870,f41]) ).
fof(f11876,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF8,sF4),s3(sF8,sF2),sF13,sF14,e2(sF2,sF4)),
inference(forward_demodulation,[],[f11875,f73]) ).
fof(f11877,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF4,sF4),s3(sF8,sF2),sF13,e1(sF8,sF4),e2(sF2,sF4)),
inference(resolution,[],[f11876,f327]) ).
fof(f11881,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF4,sF4),s3(sF8,sF2),sF13,e1(sF2,sF4),e2(sF8,sF4)),
inference(resolution,[],[f11877,f41]) ).
fof(f11882,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF4,sF4),s3(sF8,sF2),sF13,e1(sF2,sF4),sF15),
inference(forward_demodulation,[],[f11881,f75]) ).
fof(f11885,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF2,sF4),s3(sF8,sF2),sF13,e1(sF4,sF4),sF15),
inference(resolution,[],[f11882,f323]) ).
fof(f11887,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF2,sF4),s3(sF8,sF2),sF13,sF14,sF15),
inference(forward_demodulation,[],[f11885,f73]) ).
fof(f11889,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF2,sF4),s3(sF8,sF2),sF13,e1(sF8,sF4),e2(sF4,sF4)),
inference(resolution,[],[f11887,f1117]) ).
fof(f11890,plain,
state(sF0,sF3,sF5,sF6,v4(sF2,sF2),sF9,sF10,s2(sF2,sF4),s3(sF8,sF4),sF13,e1(sF8,sF2),e2(sF4,sF4)),
inference(resolution,[],[f11889,f387]) ).
fof(f11895,plain,
state(sF0,sF3,sF5,sF6,v4(sF4,sF2),sF9,sF10,s2(sF2,sF4),s3(sF8,sF4),sF13,e1(sF2,sF2),e2(sF4,sF4)),
inference(resolution,[],[f11890,f249]) ).
fof(f11899,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF2,sF4),s3(sF8,sF4),sF13,e1(sF2,sF2),e2(sF4,sF4)),
inference(forward_demodulation,[],[f11895,f59]) ).
fof(f11903,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,s2(sF2,sF2),s3(sF8,sF4),sF13,e1(sF2,sF4),e2(sF4,sF4)),
inference(resolution,[],[f11899,f337]) ).
fof(f11906,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF8,sF4),sF13,e1(sF2,sF4),e2(sF4,sF4)),
inference(forward_demodulation,[],[f11903,f67]) ).
fof(f11909,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF8,sF4),sF13,e1(sF4,sF4),e2(sF2,sF4)),
inference(resolution,[],[f11906,f41]) ).
fof(f11910,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF8,sF4),sF13,sF14,e2(sF2,sF4)),
inference(forward_demodulation,[],[f11909,f73]) ).
fof(f11911,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF4),sF13,e1(sF8,sF4),e2(sF2,sF4)),
inference(resolution,[],[f11910,f348]) ).
fof(f11928,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF4),sF13,e1(sF2,sF4),e2(sF8,sF4)),
inference(resolution,[],[f11911,f41]) ).
fof(f11929,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF4,sF4),sF13,e1(sF2,sF4),sF15),
inference(forward_demodulation,[],[f11928,f75]) ).
fof(f11933,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF2,sF4),sF13,e1(sF4,sF4),sF15),
inference(resolution,[],[f11929,f344]) ).
fof(f11935,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,s3(sF2,sF4),sF13,sF14,sF15),
inference(forward_demodulation,[],[f11933,f73]) ).
fof(f11936,plain,
state(sF0,sF3,sF5,sF6,sF7,sF9,sF10,sF11,sF12,sF13,sF14,sF15),
inference(forward_demodulation,[],[f11935,f69]) ).
fof(f11937,plain,
$false,
inference(forward_subsumption_resolution,[],[f11936,f76]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ050-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.43 % Computer : n019.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Sun Sep 27 22:36:04 UTC 2026
% 0.15/0.44 % CPUTime :
% 0.15/0.44 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.49 Running first-order theorem proving
% 0.15/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.00/3.23 % (3481894)Input is clausal, will run a generic CNF schedule.
% 16.00/3.23 % (3481914)lrs+10_1_sil=8000:sp=occurrence:random_seed=1220034028:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.00/3.23 % (3481917)dis-21_1_sil=8000:lcm=predicate:random_seed=704014427: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)
% 16.00/3.23 % (3481914)Instruction limit reached!
% 16.00/3.23 % (3481914)------------------------------
% 16.00/3.23 % (3481914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.23 % (3481914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.23 % (3481914)CaDiCaL version: 2.1.3
% 16.00/3.23 % (3481914)Termination reason: Instruction limit
% 16.00/3.23 % (3481914)Termination phase: Saturation
% 16.00/3.23 % (3481914)Time elapsed: 0.052 s
% 16.00/3.23 % (3481914)Peak memory usage: 89 MB
% 16.00/3.23 % (3481914)Instructions burned: 108 (million)
% 16.00/3.23 % (3481913)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3437160234:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.00/3.23 % (3481916)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3357502990:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.00/3.23 % (3481911)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=2319308719:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.00/3.23 % (3481915)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=13564279:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.00/3.23 % (3481912)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2620648366:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.00/3.23 % (3481917)Instruction limit reached!
% 16.00/3.23 % (3481917)------------------------------
% 16.00/3.23 % (3481917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.23 % (3481917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.23 % (3481917)CaDiCaL version: 2.1.3
% 16.00/3.23 % (3481917)Termination reason: Instruction limit
% 16.00/3.23 % (3481917)Termination phase: Saturation
% 16.00/3.23 % (3481917)Time elapsed: 0.109 s
% 16.00/3.23 % (3481917)Peak memory usage: 88 MB
% 16.00/3.23 % (3481917)Instructions burned: 117 (million)
% 16.00/3.23 % (3481915)Instruction limit reached!
% 16.00/3.23 % (3481915)------------------------------
% 16.00/3.23 % (3481915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.23 % (3481915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.23 % (3481915)CaDiCaL version: 2.1.3
% 16.00/3.23 % (3481915)Termination reason: Instruction limit
% 16.00/3.23 % (3481915)Termination phase: Saturation
% 16.00/3.23 % (3481915)Time elapsed: 0.105 s
% 16.00/3.23 % (3481915)Peak memory usage: 88 MB
% 16.00/3.23 % (3481915)Instructions burned: 114 (million)
% 16.00/3.23 % (3481920)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=2050847885:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 16.00/3.23 % (3481916)Instruction limit reached!
% 16.00/3.23 % (3481916)------------------------------
% 16.00/3.23 % (3481916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.23 % (3481916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.23 % (3481916)CaDiCaL version: 2.1.3
% 16.00/3.23 % (3481916)Termination reason: Instruction limit
% 16.00/3.23 % (3481916)Termination phase: Saturation
% 16.00/3.23 % (3481916)Time elapsed: 0.152 s
% 16.00/3.23 % (3481916)Peak memory usage: 88 MB
% 16.00/3.23 % (3481916)Instructions burned: 180 (million)
% 16.00/3.23 % (3481920)Instruction limit reached!
% 16.00/3.23 % (3481920)------------------------------
% 16.00/3.23 % (3481920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/3.23 % (3481920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/3.23 % (3481920)CaDiCaL version: 2.1.3
% 16.00/3.23 % (3481920)Termination reason: Instruction limit
% 16.00/3.23 % (3481920)Termination phase: Saturation
% 16.00/3.23 % (3481920)Time elapsed: 0.064 s
% 16.00/3.23 % (3481920)Peak memory usage: 88 MB
% 16.00/3.23 % (3481920)Instructions burned: 145 (million)
% 16.00/3.23 % (3481926)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2856905225:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 27.06/4.94 % (3481928)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=33709673:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 27.06/4.94 % (3481932)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1815698662:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 27.06/4.94 % (3481930)lrs+10_64_to=lpo:sil=8000:random_seed=1135801484:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 27.06/4.94 % (3481926)Instruction limit reached!
% 27.06/4.94 % (3481926)------------------------------
% 27.06/4.94 % (3481926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.06/4.94 % (3481926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.06/4.94 % (3481926)CaDiCaL version: 2.1.3
% 27.06/4.94 % (3481926)Termination reason: Instruction limit
% 27.06/4.94 % (3481926)Termination phase: Saturation
% 27.06/4.94 % (3481926)Time elapsed: 0.141 s
% 27.06/4.94 % (3481926)Peak memory usage: 88 MB
% 27.06/4.94 % (3481926)Instructions burned: 189 (million)
% 27.06/4.94 % (3481932)Instruction limit reached!
% 27.06/4.94 % (3481932)------------------------------
% 27.06/4.94 % (3481932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.06/4.94 % (3481932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.06/4.94 % (3481932)CaDiCaL version: 2.1.3
% 27.06/4.94 % (3481932)Termination reason: Instruction limit
% 27.06/4.94 % (3481932)Termination phase: Saturation
% 27.06/4.94 % (3481932)Time elapsed: 0.086 s
% 27.06/4.94 % (3481932)Peak memory usage: 87 MB
% 27.06/4.94 % (3481932)Instructions burned: 195 (million)
% 27.06/4.94 % (3481930)Instruction limit reached!
% 27.06/4.94 % (3481930)------------------------------
% 27.06/4.94 % (3481930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.06/4.94 % (3481930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.06/4.94 % (3481930)CaDiCaL version: 2.1.3
% 27.06/4.94 % (3481930)Termination reason: Instruction limit
% 27.06/4.94 % (3481930)Termination phase: Saturation
% 27.06/4.94 % (3481930)Time elapsed: 0.106 s
% 27.06/4.94 % (3481930)Peak memory usage: 87 MB
% 27.06/4.94 % (3481930)Instructions burned: 126 (million)
% 27.06/4.94 % (3481928)Instruction limit reached!
% 27.06/4.94 % (3481928)------------------------------
% 27.06/4.94 % (3481928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.06/4.94 % (3481928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.06/4.94 % (3481928)CaDiCaL version: 2.1.3
% 27.06/4.94 % (3481928)Termination reason: Instruction limit
% 27.06/4.94 % (3481928)Termination phase: Saturation
% 27.06/4.94 % (3481928)Time elapsed: 0.184 s
% 27.06/4.94 % (3481928)Peak memory usage: 88 MB
% 27.06/4.94 % (3481928)Instructions burned: 219 (million)
% 27.06/4.94 % (3481937)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1730106464:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 27.06/4.94 % (3481938)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1205682215:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 27.06/4.94 % (3481939)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=4077770652:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 27.06/4.94 % (3481940)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3725730293:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 27.06/4.94 % (3481937)Instruction limit reached!
% 27.06/4.94 % (3481937)------------------------------
% 27.06/4.94 % (3481937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.06/4.94 % (3481937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.06/4.94 % (3481937)CaDiCaL version: 2.1.3
% 27.06/4.94 % (3481937)Termination reason: Instruction limit
% 27.06/4.94 % (3481937)Termination phase: Saturation
% 27.06/4.94 % (3481937)Time elapsed: 0.152 s
% 27.06/4.94 % (3481937)Peak memory usage: 90 MB
% 27.06/4.94 % (3481937)Instructions burned: 158 (million)
% 27.06/4.94 % (3481939)Instruction limit reached!
% 27.06/4.94 % (3481939)------------------------------
% 27.06/4.94 % (3481939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.91/8.66 % (3481939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.91/8.66 % (3481939)CaDiCaL version: 2.1.3
% 53.91/8.66 % (3481939)Termination reason: Instruction limit
% 53.91/8.66 % (3481939)Termination phase: Saturation
% 53.91/8.66 % (3481939)Time elapsed: 0.093 s
% 53.91/8.66 % (3481939)Peak memory usage: 88 MB
% 53.91/8.66 % (3481939)Instructions burned: 106 (million)
% 53.91/8.66 % (3481940)Refutation not found, incomplete strategy
% 53.91/8.66 % (3481940)------------------------------
% 53.91/8.66 % (3481940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.91/8.66 % (3481940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.91/8.66 % (3481940)CaDiCaL version: 2.1.3
% 53.91/8.66 % (3481940)Termination reason: Refutation not found, incomplete strategy
% 53.91/8.66 % (3481940)Time elapsed: 0.038 s
% 53.91/8.66 % (3481940)Peak memory usage: 87 MB
% 53.91/8.66 % (3481940)Instructions burned: 44 (million)
% 53.91/8.66 % (3481945)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1638490744:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 53.91/8.66 % (3481946)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1562071560:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 53.91/8.66 % (3481940)------------------------------
% 53.91/8.66 % (3481940)------------------------------
% 53.91/8.66 % (3481945)Instruction limit reached!
% 53.91/8.66 % (3481945)------------------------------
% 53.91/8.66 % (3481945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.91/8.66 % (3481945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.91/8.66 % (3481945)CaDiCaL version: 2.1.3
% 53.91/8.66 % (3481945)Termination reason: Instruction limit
% 53.91/8.66 % (3481945)Termination phase: Saturation
% 53.91/8.66 % (3481945)Time elapsed: 0.243 s
% 53.91/8.66 % (3481945)Peak memory usage: 90 MB
% 53.91/8.66 % (3481945)Instructions burned: 242 (million)
% 53.91/8.66 % (3481954)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1885442707:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 53.91/8.66 % (3481953)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1593498120:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 53.91/8.66 % (3481953)Instruction limit reached!
% 53.91/8.66 % (3481953)------------------------------
% 53.91/8.66 % (3481953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.91/8.66 % (3481953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.91/8.66 % (3481953)CaDiCaL version: 2.1.3
% 53.91/8.66 % (3481953)Termination reason: Instruction limit
% 53.91/8.66 % (3481953)Termination phase: Saturation
% 53.91/8.66 % (3481953)Time elapsed: 0.113 s
% 53.91/8.66 % (3481953)Peak memory usage: 88 MB
% 53.91/8.66 % (3481953)Instructions burned: 135 (million)
% 53.91/8.66 % (3481957)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3275087649:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 53.91/8.66 % (3481957)Refutation not found, incomplete strategy
% 53.91/8.66 % (3481957)------------------------------
% 53.91/8.66 % (3481957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.91/8.66 % (3481957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.91/8.66 % (3481957)CaDiCaL version: 2.1.3
% 53.91/8.66 % (3481957)Termination reason: Refutation not found, incomplete strategy
% 53.91/8.66 % (3481957)Time elapsed: 0.006 s
% 53.91/8.66 % (3481957)Peak memory usage: 87 MB
% 53.91/8.66 % (3481957)Instructions burned: 5 (million)
% 53.91/8.66 % (3481954)Instruction limit reached!
% 53.91/8.66 % (3481954)------------------------------
% 53.91/8.66 % (3481954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.91/8.66 % (3481954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.91/8.66 % (3481954)CaDiCaL version: 2.1.3
% 53.91/8.66 % (3481954)Termination reason: Instruction limit
% 53.91/8.66 % (3481954)Termination phase: Saturation
% 53.91/8.66 % (3481954)Time elapsed: 0.442 s
% 53.91/8.66 % (3481954)Peak memory usage: 90 MB
% 53.91/8.66 % (3481954)Instructions burned: 500 (million)
% 53.91/8.66 % (3481959)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1721223254:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 79.00/12.11 % (3481957)------------------------------
% 79.00/12.11 % (3481957)------------------------------
% 79.00/12.11 % (3481959)Instruction limit reached!
% 79.00/12.11 % (3481959)------------------------------
% 79.00/12.11 % (3481959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.00/12.11 % (3481959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.00/12.11 % (3481959)CaDiCaL version: 2.1.3
% 79.00/12.11 % (3481959)Termination reason: Instruction limit
% 79.00/12.11 % (3481959)Termination phase: Saturation
% 79.00/12.11 % (3481959)Time elapsed: 0.223 s
% 79.00/12.11 % (3481959)Peak memory usage: 89 MB
% 79.00/12.11 % (3481959)Instructions burned: 265 (million)
% 79.00/12.11 % (3481961)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=683889720:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 79.00/12.11 % (3481961)Refutation not found, incomplete strategy
% 79.00/12.11 % (3481961)------------------------------
% 79.00/12.11 % (3481961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.00/12.11 % (3481961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.00/12.11 % (3481961)CaDiCaL version: 2.1.3
% 79.00/12.11 % (3481961)Termination reason: Refutation not found, incomplete strategy
% 79.00/12.11 % (3481961)Time elapsed: 0.011 s
% 79.00/12.11 % (3481961)Peak memory usage: 88 MB
% 79.00/12.11 % (3481961)Instructions burned: 10 (million)
% 79.00/12.11 % (3481962)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=2218016139:i=3256:kws=precedence:bd=preordered:av=off_2975 on theBenchmark for (2975ds/3256Mi)
% 79.00/12.11 % (3481938)Instruction limit reached!
% 79.00/12.11 % (3481938)------------------------------
% 79.00/12.11 % (3481938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.00/12.11 % (3481938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.00/12.11 % (3481938)CaDiCaL version: 2.1.3
% 79.00/12.11 % (3481938)Termination reason: Instruction limit
% 79.00/12.11 % (3481938)Termination phase: Saturation
% 79.00/12.11 % (3481938)Time elapsed: 2.070 s
% 79.00/12.11 % (3481938)Peak memory usage: 141 MB
% 79.00/12.11 % (3481938)Instructions burned: 3394 (million)
% 79.00/12.11 % (3481961)------------------------------
% 79.00/12.11 % (3481961)------------------------------
% 79.00/12.11 % (3481965)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1926564971:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi)
% 79.00/12.11 % (3481966)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3914185126:i=180:bd=preordered:av=off_2970 on theBenchmark for (2970ds/180Mi)
% 79.00/12.11 % (3481965)Instruction limit reached!
% 79.00/12.11 % (3481965)------------------------------
% 79.00/12.11 % (3481965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.00/12.11 % (3481965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.00/12.11 % (3481965)CaDiCaL version: 2.1.3
% 79.00/12.11 % (3481965)Termination reason: Instruction limit
% 79.00/12.11 % (3481965)Termination phase: Saturation
% 79.00/12.11 % (3481965)Time elapsed: 0.262 s
% 79.00/12.11 % (3481965)Peak memory usage: 90 MB
% 79.00/12.11 % (3481965)Instructions burned: 537 (million)
% 79.00/12.11 % (3481966)Instruction limit reached!
% 79.00/12.11 % (3481966)------------------------------
% 79.00/12.11 % (3481966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.00/12.11 % (3481966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.00/12.11 % (3481966)CaDiCaL version: 2.1.3
% 79.00/12.11 % (3481966)Termination reason: Instruction limit
% 79.00/12.11 % (3481966)Termination phase: Saturation
% 79.00/12.11 % (3481966)Time elapsed: 0.160 s
% 79.00/12.11 % (3481966)Peak memory usage: 87 MB
% 79.00/12.11 % (3481966)Instructions burned: 180 (million)
% 79.00/12.11 % (3481969)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=1782926578:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2967 on theBenchmark for (2967ds/10307Mi)
% 79.00/12.11 % (3481970)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=533366931:i=412:gtgl=4:gtg=exists_all_2966 on theBenchmark for (2966ds/412Mi)
% 79.00/12.11 % (3481970)Instruction limit reached!
% 79.00/12.11 % (3481970)------------------------------
% 79.00/12.11 % (3481970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.23/16.91 % (3481970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.23/16.91 % (3481970)CaDiCaL version: 2.1.3
% 109.23/16.91 % (3481970)Termination reason: Instruction limit
% 109.23/16.91 % (3481970)Termination phase: Saturation
% 109.23/16.91 % (3481970)Time elapsed: 0.392 s
% 109.23/16.91 % (3481970)Peak memory usage: 94 MB
% 109.23/16.91 % (3481970)Instructions burned: 413 (million)
% 109.23/16.91 % (3481973)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=2693213879:s2pl=no:i=8478:s2at=4:nm=6_2960 on theBenchmark for (2960ds/8478Mi)
% 109.23/16.91 % (3481962)Instruction limit reached!
% 109.23/16.91 % (3481962)------------------------------
% 109.23/16.91 % (3481962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.23/16.91 % (3481962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.23/16.91 % (3481962)CaDiCaL version: 2.1.3
% 109.23/16.91 % (3481962)Termination reason: Instruction limit
% 109.23/16.91 % (3481962)Termination phase: Saturation
% 109.23/16.91 % (3481962)Time elapsed: 3.437 s
% 109.23/16.91 % (3481962)Peak memory usage: 137 MB
% 109.23/16.91 % (3481962)Instructions burned: 3256 (million)
% 109.23/16.91 % (3481946)Instruction limit reached!
% 109.23/16.91 % (3481946)------------------------------
% 109.23/16.91 % (3481946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.23/16.91 % (3481946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.23/16.91 % (3481946)CaDiCaL version: 2.1.3
% 109.23/16.91 % (3481946)Termination reason: Instruction limit
% 109.23/16.91 % (3481946)Termination phase: Saturation
% 109.23/16.91 % (3481946)Time elapsed: 5.087 s
% 109.23/16.91 % (3481946)Peak memory usage: 165 MB
% 109.23/16.91 % (3481946)Instructions burned: 5208 (million)
% 109.23/16.91 % (3481979)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=2942947866:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2938 on theBenchmark for (2938ds/303Mi)
% 109.23/16.91 % (3481980)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1939815926:st=4:i=720:sd=3:fsr=off:ss=axioms_2937 on theBenchmark for (2937ds/720Mi)
% 109.23/16.91 % (3481979)Instruction limit reached!
% 109.23/16.91 % (3481979)------------------------------
% 109.23/16.91 % (3481979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.23/16.91 % (3481979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.23/16.91 % (3481979)CaDiCaL version: 2.1.3
% 109.23/16.91 % (3481979)Termination reason: Instruction limit
% 109.23/16.91 % (3481979)Termination phase: Saturation
% 109.23/16.91 % (3481979)Time elapsed: 0.265 s
% 109.23/16.91 % (3481979)Peak memory usage: 89 MB
% 109.23/16.91 % (3481979)Instructions burned: 303 (million)
% 109.23/16.91 % (3481983)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3140113222:i=598:bs=on:bd=preordered:av=off:ss=axioms_2933 on theBenchmark for (2933ds/598Mi)
% 109.23/16.91 % (3481980)Instruction limit reached!
% 109.23/16.91 % (3481980)------------------------------
% 109.23/16.91 % (3481980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.23/16.91 % (3481980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.23/16.91 % (3481980)CaDiCaL version: 2.1.3
% 109.23/16.91 % (3481980)Termination reason: Instruction limit
% 109.23/16.91 % (3481980)Termination phase: Saturation
% 109.23/16.91 % (3481980)Time elapsed: 0.604 s
% 109.23/16.91 % (3481980)Peak memory usage: 90 MB
% 109.23/16.91 % (3481980)Instructions burned: 720 (million)
% 109.23/16.91 % (3481985)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=546250219:i=2989:sd=3:ss=axioms:sgt=60_2928 on theBenchmark for (2928ds/2989Mi)
% 109.23/16.91 % (3481983)Instruction limit reached!
% 109.23/16.91 % (3481983)------------------------------
% 109.23/16.91 % (3481983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.23/16.91 % (3481983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.23/16.91 % (3481983)CaDiCaL version: 2.1.3
% 109.23/16.91 % (3481983)Termination reason: Instruction limit
% 109.23/16.91 % (3481983)Termination phase: Saturation
% 109.23/16.91 % (3481983)Time elapsed: 0.592 s
% 109.23/16.91 % (3481983)Peak memory usage: 95 MB
% 109.23/16.91 % (3481983)Instructions burned: 598 (million)
% 109.23/16.91 % (3481989)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=3441651145:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2925 on theBenchmark for (2925ds/1997Mi)
% 166.69/24.48 % (3481969)Instruction limit reached!
% 166.69/24.48 % (3481969)------------------------------
% 166.69/24.48 % (3481969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.69/24.48 % (3481969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.69/24.48 % (3481969)CaDiCaL version: 2.1.3
% 166.69/24.48 % (3481969)Termination reason: Instruction limit
% 166.69/24.48 % (3481969)Termination phase: Saturation
% 166.69/24.48 % (3481969)Time elapsed: 5.395 s
% 166.69/24.48 % (3481969)Peak memory usage: 201 MB
% 166.69/24.48 % (3481969)Instructions burned: 10308 (million)
% 166.69/24.48 % (3481991)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=3322255512:i=2088:bd=preordered:av=off_2911 on theBenchmark for (2911ds/2088Mi)
% 166.69/24.48 % (3481989)Instruction limit reached!
% 166.69/24.48 % (3481989)------------------------------
% 166.69/24.48 % (3481989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.69/24.48 % (3481989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.69/24.48 % (3481989)CaDiCaL version: 2.1.3
% 166.69/24.48 % (3481989)Termination reason: Instruction limit
% 166.69/24.48 % (3481989)Termination phase: Saturation
% 166.69/24.48 % (3481989)Time elapsed: 2.213 s
% 166.69/24.48 % (3481989)Peak memory usage: 135 MB
% 166.69/24.48 % (3481989)Instructions burned: 1997 (million)
% 166.69/24.48 % (3481991)Instruction limit reached!
% 166.69/24.48 % (3481991)------------------------------
% 166.69/24.48 % (3481991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.69/24.48 % (3481991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.69/24.48 % (3481991)CaDiCaL version: 2.1.3
% 166.69/24.48 % (3481991)Termination reason: Instruction limit
% 166.69/24.48 % (3481991)Termination phase: Saturation
% 166.69/24.48 % (3481991)Time elapsed: 1.098 s
% 166.69/24.48 % (3481991)Peak memory usage: 138 MB
% 166.69/24.48 % (3481991)Instructions burned: 2090 (million)
% 166.69/24.48 % (3481999)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3389600105:i=1098:nicw=on_2901 on theBenchmark for (2901ds/1098Mi)
% 166.69/24.48 % (3482000)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2405737152:i=433:bd=preordered_2899 on theBenchmark for (2899ds/433Mi)
% 166.69/24.48 % (3482000)Refutation not found, incomplete strategy
% 166.69/24.48 % (3482000)------------------------------
% 166.69/24.48 % (3482000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.69/24.48 % (3482000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.69/24.48 % (3482000)CaDiCaL version: 2.1.3
% 166.69/24.48 % (3482000)Termination reason: Refutation not found, incomplete strategy
% 166.69/24.48 % (3482000)Time elapsed: 0.006 s
% 166.69/24.48 % (3482000)Peak memory usage: 88 MB
% 166.69/24.48 % (3482000)Instructions burned: 12 (million)
% 166.69/24.48 % (3481985)Instruction limit reached!
% 166.69/24.48 % (3481985)------------------------------
% 166.69/24.48 % (3481985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.69/24.48 % (3481985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.69/24.48 % (3481985)CaDiCaL version: 2.1.3
% 166.69/24.48 % (3481985)Termination reason: Instruction limit
% 166.69/24.48 % (3481985)Termination phase: Saturation
% 166.69/24.48 % (3481985)Time elapsed: 2.952 s
% 166.69/24.48 % (3481985)Peak memory usage: 142 MB
% 166.69/24.48 % (3481985)Instructions burned: 2989 (million)
% 166.69/24.48 % (3482000)------------------------------
% 166.69/24.48 % (3482000)------------------------------
% 166.69/24.48 % (3482003)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1472191265:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2896 on theBenchmark for (2896ds/2942Mi)
% 166.69/24.48 % (3482004)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2226513949:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2895 on theBenchmark for (2895ds/6922Mi)
% 166.69/24.48 % (3481999)Instruction limit reached!
% 166.69/24.48 % (3481999)------------------------------
% 166.69/24.48 % (3481999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.93/26.95 % (3481999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.93/26.95 % (3481999)CaDiCaL version: 2.1.3
% 183.93/26.95 % (3481999)Termination reason: Instruction limit
% 183.93/26.95 % (3481999)Termination phase: Saturation
% 183.93/26.95 % (3481999)Time elapsed: 1.019 s
% 183.93/26.95 % (3481999)Peak memory usage: 105 MB
% 183.93/26.95 % (3481999)Instructions burned: 1098 (million)
% 183.93/26.95 % (3482007)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2070211348:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2888 on theBenchmark for (2888ds/596Mi)
% 183.93/26.95 % (3482007)Refutation not found, incomplete strategy
% 183.93/26.95 % (3482007)------------------------------
% 183.93/26.95 % (3482007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.93/26.95 % (3482007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.93/26.95 % (3482007)CaDiCaL version: 2.1.3
% 183.93/26.95 % (3482007)Termination reason: Refutation not found, incomplete strategy
% 183.93/26.95 % (3482007)Time elapsed: 0.008 s
% 183.93/26.95 % (3482007)Peak memory usage: 88 MB
% 183.93/26.95 % (3482007)Instructions burned: 11 (million)
% 183.93/26.95 % (3482007)------------------------------
% 183.93/26.95 % (3482007)------------------------------
% 183.93/26.95 % (3482009)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3122369279:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2883 on theBenchmark for (2883ds/4123Mi)
% 183.93/26.95 % (3482003)Instruction limit reached!
% 183.93/26.95 % (3482003)------------------------------
% 183.93/26.95 % (3482003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.93/26.95 % (3482003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.93/26.95 % (3482003)CaDiCaL version: 2.1.3
% 183.93/26.95 % (3482003)Termination reason: Instruction limit
% 183.93/26.95 % (3482003)Termination phase: Saturation
% 183.93/26.95 % (3482003)Time elapsed: 3.033 s
% 183.93/26.95 % (3482003)Peak memory usage: 144 MB
% 183.93/26.95 % (3482003)Instructions burned: 2942 (million)
% 183.93/26.95 % (3482013)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1874756649:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2864 on theBenchmark for (2864ds/16411Mi)
% 183.93/26.95 % (3481973)Instruction limit reached!
% 183.93/26.95 % (3481973)------------------------------
% 183.93/26.95 % (3481973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.93/26.95 % (3481973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.93/26.95 % (3481973)CaDiCaL version: 2.1.3
% 183.93/26.95 % (3481973)Termination reason: Instruction limit
% 183.93/26.95 % (3481973)Termination phase: Saturation
% 183.93/26.95 % (3481973)Time elapsed: 10.211 s
% 183.93/26.95 % (3481973)Peak memory usage: 173 MB
% 183.93/26.95 % (3481973)Instructions burned: 8478 (million)
% 183.93/26.95 % (3482015)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=65570613:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2856 on theBenchmark for (2856ds/1670Mi)
% 183.93/26.95 % (3482004)Instruction limit reached!
% 183.93/26.95 % (3482004)------------------------------
% 183.93/26.95 % (3482004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.93/26.95 % (3482004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.93/26.95 % (3482004)CaDiCaL version: 2.1.3
% 183.93/26.95 % (3482004)Termination reason: Instruction limit
% 183.93/26.95 % (3482004)Termination phase: Saturation
% 183.93/26.95 % (3482004)Time elapsed: 4.073 s
% 183.93/26.95 % (3482004)Peak memory usage: 156 MB
% 183.93/26.95 % (3482004)Instructions burned: 6922 (million)
% 183.93/26.95 % (3482017)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2593141256:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2853 on theBenchmark for (2853ds/1722Mi)
% 183.93/26.95 % (3482009)Instruction limit reached!
% 183.93/26.95 % (3482009)------------------------------
% 183.93/26.95 % (3482009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 183.93/26.95 % (3482009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.93/26.95 % (3482009)CaDiCaL version: 2.1.3
% 183.93/26.95 % (3482009)Termination reason: Instruction limit
% 183.93/26.95 % (3482009)Termination phase: Saturation
% 183.93/26.95 % (3482009)Time elapsed: 4.015 s
% 183.93/26.95 % (3482009)Peak memory usage: 155 MB
% 209.01/32.00 % (3482009)Instructions burned: 4126 (million)
% 209.01/32.00 % (3482027)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1003572313:cts=off:cond=on:i=9530:bs=on:fsd=on_2840 on theBenchmark for (2840ds/9530Mi)
% 209.01/32.00 % (3482015)Instruction limit reached!
% 209.01/32.00 % (3482015)------------------------------
% 209.01/32.00 % (3482015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482015)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482015)Termination reason: Instruction limit
% 209.01/32.00 % (3482015)Termination phase: Saturation
% 209.01/32.00 % (3482015)Time elapsed: 1.686 s
% 209.01/32.00 % (3482015)Peak memory usage: 136 MB
% 209.01/32.00 % (3482015)Instructions burned: 1671 (million)
% 209.01/32.00 % (3482029)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1782238392:st=2:i=4495:sd=10:ss=included_2837 on theBenchmark for (2837ds/4495Mi)
% 209.01/32.00 % (3482017)Instruction limit reached!
% 209.01/32.00 % (3482017)------------------------------
% 209.01/32.00 % (3482017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482017)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482017)Termination reason: Instruction limit
% 209.01/32.00 % (3482017)Termination phase: Saturation
% 209.01/32.00 % (3482017)Time elapsed: 1.793 s
% 209.01/32.00 % (3482017)Peak memory usage: 132 MB
% 209.01/32.00 % (3482017)Instructions burned: 1723 (million)
% 209.01/32.00 % (3482033)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2097002021:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2832 on theBenchmark for (2832ds/4920Mi)
% 209.01/32.00 % (3482029)Instruction limit reached!
% 209.01/32.00 % (3482029)------------------------------
% 209.01/32.00 % (3482029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482029)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482029)Termination reason: Instruction limit
% 209.01/32.00 % (3482029)Termination phase: Saturation
% 209.01/32.00 % (3482029)Time elapsed: 5.113 s
% 209.01/32.00 % (3482029)Peak memory usage: 145 MB
% 209.01/32.00 % (3482029)Instructions burned: 4495 (million)
% 209.01/32.00 % (3482033)Instruction limit reached!
% 209.01/32.00 % (3482033)------------------------------
% 209.01/32.00 % (3482033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482033)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482033)Termination reason: Instruction limit
% 209.01/32.00 % (3482033)Termination phase: Saturation
% 209.01/32.00 % (3482033)Time elapsed: 4.849 s
% 209.01/32.00 % (3482033)Peak memory usage: 162 MB
% 209.01/32.00 % (3482033)Instructions burned: 4920 (million)
% 209.01/32.00 % (3482035)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2879778979:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2784 on theBenchmark for (2784ds/2083Mi)
% 209.01/32.00 % (3482036)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2425325798:i=4629:av=off:gsp=on_2782 on theBenchmark for (2782ds/4629Mi)
% 209.01/32.00 % (3482036)Refutation not found, incomplete strategy
% 209.01/32.00 % (3482036)------------------------------
% 209.01/32.00 % (3482036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482036)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482036)Termination reason: Refutation not found, incomplete strategy
% 209.01/32.00 % (3482036)Time elapsed: 0.957 s
% 209.01/32.00 % (3482036)Peak memory usage: 129 MB
% 209.01/32.00 % (3482036)Instructions burned: 915 (million)
% 209.01/32.00 % (3482036)------------------------------
% 209.01/32.00 % (3482036)------------------------------
% 209.01/32.00 % (3482041)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=456173294:i=1258:av=off_2766 on theBenchmark for (2766ds/1258Mi)
% 209.01/32.00 % (3482035)Instruction limit reached!
% 209.01/32.00 % (3482035)------------------------------
% 209.01/32.00 % (3482035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482035)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482035)Termination reason: Instruction limit
% 209.01/32.00 % (3482035)Termination phase: Saturation
% 209.01/32.00 % (3482035)Time elapsed: 2.051 s
% 209.01/32.00 % (3482035)Peak memory usage: 135 MB
% 209.01/32.00 % (3482035)Instructions burned: 2084 (million)
% 209.01/32.00 % (3482013)Instruction limit reached!
% 209.01/32.00 % (3482013)------------------------------
% 209.01/32.00 % (3482013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482013)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482013)Termination reason: Instruction limit
% 209.01/32.00 % (3482013)Termination phase: Saturation
% 209.01/32.00 % (3482013)Time elapsed: 10.221 s
% 209.01/32.00 % (3482013)Peak memory usage: 199 MB
% 209.01/32.00 % (3482013)Instructions burned: 16412 (million)
% 209.01/32.00 % (3482043)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1816922476:i=7343:av=off:ss=included_2761 on theBenchmark for (2761ds/7343Mi)
% 209.01/32.00 % (3482045)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3853990233:i=1325:sd=2:ss=axioms:sgt=16_2759 on theBenchmark for (2759ds/1325Mi)
% 209.01/32.00 % (3482041)Instruction limit reached!
% 209.01/32.00 % (3482041)------------------------------
% 209.01/32.00 % (3482041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482041)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482041)Termination reason: Instruction limit
% 209.01/32.00 % (3482041)Termination phase: Saturation
% 209.01/32.00 % (3482041)Time elapsed: 1.118 s
% 209.01/32.00 % (3482041)Peak memory usage: 99 MB
% 209.01/32.00 % (3482041)Instructions burned: 1258 (million)
% 209.01/32.00 % (3482045)Refutation not found, incomplete strategy
% 209.01/32.00 % (3482045)------------------------------
% 209.01/32.00 % (3482045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482045)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482045)Termination reason: Refutation not found, incomplete strategy
% 209.01/32.00 % (3482045)Time elapsed: 0.556 s
% 209.01/32.00 % (3482045)Peak memory usage: 92 MB
% 209.01/32.00 % (3482045)Instructions burned: 1257 (million)
% 209.01/32.00 % (3482047)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=1571242173:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2753 on theBenchmark for (2753ds/2646Mi)
% 209.01/32.00 % (3482045)------------------------------
% 209.01/32.00 % (3482045)------------------------------
% 209.01/32.00 % (3482049)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1248122676:i=1489:sd=2:ep=R:ss=axioms_2750 on theBenchmark for (2750ds/1489Mi)
% 209.01/32.00 % (3482027)Instruction limit reached!
% 209.01/32.00 % (3482027)------------------------------
% 209.01/32.00 % (3482027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482027)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482027)Termination reason: Instruction limit
% 209.01/32.00 % (3482027)Termination phase: Saturation
% 209.01/32.00 % (3482027)Time elapsed: 9.209 s
% 209.01/32.00 % (3482027)Peak memory usage: 183 MB
% 209.01/32.00 % (3482027)Instructions burned: 9530 (million)
% 209.01/32.00 % (3482051)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2955272362:i=1503_2746 on theBenchmark for (2746ds/1503Mi)
% 209.01/32.00 % (3482049)Instruction limit reached!
% 209.01/32.00 % (3482049)------------------------------
% 209.01/32.00 % (3482049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482049)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482049)Termination reason: Instruction limit
% 209.01/32.00 % (3482049)Termination phase: Saturation
% 209.01/32.00 % (3482049)Time elapsed: 0.824 s
% 209.01/32.00 % (3482049)Peak memory usage: 130 MB
% 209.01/32.00 % (3482049)Instructions burned: 1491 (million)
% 209.01/32.00 % (3482053)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2075550940:i=13942:kws=frequency_2740 on theBenchmark for (2740ds/13942Mi)
% 209.01/32.00 % (3482051)Instruction limit reached!
% 209.01/32.00 % (3482051)------------------------------
% 209.01/32.00 % (3482051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482051)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482051)Termination reason: Instruction limit
% 209.01/32.00 % (3482051)Termination phase: Saturation
% 209.01/32.00 % (3482051)Time elapsed: 1.552 s
% 209.01/32.00 % (3482051)Peak memory usage: 130 MB
% 209.01/32.00 % (3482051)Instructions burned: 1503 (million)
% 209.01/32.00 % (3482057)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=1096997041:i=3604:fsr=off:er=filter_2728 on theBenchmark for (2728ds/3604Mi)
% 209.01/32.00 % (3482047)Instruction limit reached!
% 209.01/32.00 % (3482047)------------------------------
% 209.01/32.00 % (3482047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482047)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482047)Termination reason: Instruction limit
% 209.01/32.00 % (3482047)Termination phase: Saturation
% 209.01/32.00 % (3482047)Time elapsed: 2.857 s
% 209.01/32.00 % (3482047)Peak memory usage: 136 MB
% 209.01/32.00 % (3482047)Instructions burned: 2647 (million)
% 209.01/32.00 % (3482059)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=254031660:i=1876:sd=1:ss=included:sgt=32_2722 on theBenchmark for (2722ds/1876Mi)
% 209.01/32.00 % (3482059)Instruction limit reached!
% 209.01/32.00 % (3482059)------------------------------
% 209.01/32.00 % (3482059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482059)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482059)Termination reason: Instruction limit
% 209.01/32.00 % (3482059)Termination phase: Saturation
% 209.01/32.00 % (3482059)Time elapsed: 1.992 s
% 209.01/32.00 % (3482059)Peak memory usage: 133 MB
% 209.01/32.00 % (3482059)Instructions burned: 1876 (million)
% 209.01/32.00 % (3482061)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2092178108:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2701 on theBenchmark for (2701ds/1932Mi)
% 209.01/32.00 % (3482043)First to succeed.
% 209.01/32.00 % (3482043)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3481894"
% 209.01/32.00 % (3482057)Instruction limit reached!
% 209.01/32.00 % (3482057)------------------------------
% 209.01/32.00 % (3482057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.01/32.00 % (3482057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.01/32.00 % (3482057)CaDiCaL version: 2.1.3
% 209.01/32.00 % (3482057)Termination reason: Instruction limit
% 209.01/32.00 % (3482057)Termination phase: Saturation
% 209.01/32.00 % (3482057)Time elapsed: 3.608 s
% 209.01/32.00 % (3482057)Peak memory usage: 147 MB
% 209.01/32.00 % (3482057)Instructions burned: 3604 (million)
% 209.01/32.00 % (3482043)Refutation found. Thanks to Tanya!
% 209.01/32.00 % SZS status Unsatisfiable for theBenchmark
% 209.01/32.00 % SZS output start Proof for theBenchmark
% See solution above
% 0.23/32.30 % (3482043)------------------------------
% 0.23/32.30 % (3482043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.23/32.30 % (3482043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/32.30 % (3482043)CaDiCaL version: 2.1.3
% 0.23/32.30 % (3482043)Termination reason: Refutation
% 0.23/32.30 % (3482043)Time elapsed: 6.543 s
% 0.23/32.30 % (3482043)Peak memory usage: 154 MB
% 0.23/32.30 % (3482043)Instructions burned: 5624 (million)
% 0.23/32.30 % (3482043)------------------------------
% 0.23/32.30 % (3482043)------------------------------
% 0.23/32.30 % (3481894)Success in time 31.008 s
% 0.23/32.30 % Vampire exiting
%------------------------------------------------------------------------------