%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL511+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 11:52:39 AM UTC 2026
% Result : Theorem 128.42s 30.94s
% Output : Refutation 213.69s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modus_ponens) ).
fof(f2,axiom,
( substitution_of_equivalents
<=> ! [X0,X1] :
( is_a_theorem(equiv(X0,X1))
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',substitution_of_equivalents) ).
fof(f12,axiom,
( or_3
<=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',or_3) ).
fof(f16,axiom,
( kn1
<=> ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kn1) ).
fof(f17,axiom,
( kn2
<=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kn2) ).
fof(f18,axiom,
( kn3
<=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kn3) ).
fof(f27,axiom,
( op_or
=> ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_or) ).
fof(f29,axiom,
( op_implies_and
=> ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_implies_and) ).
fof(f31,axiom,
( op_equiv
=> ! [X0,X1] : equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_equiv) ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rosser_modus_ponens) ).
fof(f36,axiom,
kn1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rosser_kn1) ).
fof(f37,axiom,
kn2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rosser_kn2) ).
fof(f38,axiom,
kn3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rosser_kn3) ).
fof(f39,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',use_substitution_of_equivalents) ).
fof(f40,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_or) ).
fof(f41,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_implies_and) ).
fof(f42,axiom,
op_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_equiv) ).
fof(f43,conjecture,
or_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_or_3) ).
fof(f44,negated_conjecture,
~ or_3,
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f45,plain,
~ or_3,
inference(flattening,[],[f44]) ).
fof(f46,plain,
( kn3
=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))) ),
inference(unused_predicate_definition_removal,[],[f18]) ).
fof(f47,plain,
( kn2
=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)) ),
inference(unused_predicate_definition_removal,[],[f17]) ).
fof(f48,plain,
( kn1
=> ! [X0] : is_a_theorem(implies(X0,and(X0,X0))) ),
inference(unused_predicate_definition_removal,[],[f16]) ).
fof(f49,plain,
( ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2))))
=> or_3 ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f50,plain,
( substitution_of_equivalents
=> ! [X0,X1] :
( is_a_theorem(equiv(X0,X1))
=> X0 = X1 ) ),
inference(unused_predicate_definition_removal,[],[f2]) ).
fof(f51,plain,
( modus_ponens
=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f54,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) )
| ~ modus_ponens ),
inference(ennf_transformation,[],[f51]) ).
fof(f55,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) )
| ~ modus_ponens ),
inference(flattening,[],[f54]) ).
fof(f56,plain,
( ! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) )
| ~ substitution_of_equivalents ),
inference(ennf_transformation,[],[f50]) ).
fof(f57,plain,
( or_3
| ? [X0,X1,X2] : ~ is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
inference(ennf_transformation,[],[f49]) ).
fof(f58,plain,
( ! [X0] : is_a_theorem(implies(X0,and(X0,X0)))
| ~ kn1 ),
inference(ennf_transformation,[],[f48]) ).
fof(f59,plain,
( ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(ennf_transformation,[],[f47]) ).
fof(f60,plain,
( ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
| ~ kn3 ),
inference(ennf_transformation,[],[f46]) ).
fof(f61,plain,
( ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(ennf_transformation,[],[f27]) ).
fof(f62,plain,
( ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(ennf_transformation,[],[f29]) ).
fof(f63,plain,
( ! [X0,X1] : equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(ennf_transformation,[],[f31]) ).
fof(f64,plain,
( or_3
| ~ is_a_theorem(implies(implies(sK0,sK2),implies(implies(sK1,sK2),implies(or(sK0,sK1),sK2)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f57]) ).
fof(f65,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1))
| ~ modus_ponens ),
inference(cnf_transformation,[],[f55]) ).
fof(f66,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[],[f56]) ).
fof(f67,plain,
( or_3
| ~ is_a_theorem(implies(implies(sK0,sK2),implies(implies(sK1,sK2),implies(or(sK0,sK1),sK2)))) ),
inference(cnf_transformation,[],[f64]) ).
fof(f68,plain,
! [X0] :
( is_a_theorem(implies(X0,and(X0,X0)))
| ~ kn1 ),
inference(cnf_transformation,[],[f58]) ).
fof(f69,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(cnf_transformation,[],[f59]) ).
fof(f70,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0)))))
| ~ kn3 ),
inference(cnf_transformation,[],[f60]) ).
fof(f71,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[],[f61]) ).
fof(f72,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[],[f62]) ).
fof(f73,plain,
! [X0,X1] :
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[],[f63]) ).
fof(f77,plain,
modus_ponens,
inference(cnf_transformation,[],[f35]) ).
fof(f78,plain,
kn1,
inference(cnf_transformation,[],[f36]) ).
fof(f79,plain,
kn2,
inference(cnf_transformation,[],[f37]) ).
fof(f80,plain,
kn3,
inference(cnf_transformation,[],[f38]) ).
fof(f81,plain,
substitution_of_equivalents,
inference(cnf_transformation,[],[f39]) ).
fof(f82,plain,
op_or,
inference(cnf_transformation,[],[f40]) ).
fof(f83,plain,
op_implies_and,
inference(cnf_transformation,[],[f41]) ).
fof(f84,plain,
op_equiv,
inference(cnf_transformation,[],[f42]) ).
fof(f85,plain,
~ or_3,
inference(cnf_transformation,[],[f45]) ).
fof(f86,plain,
! [X0,X1] : equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
inference(forward_subsumption_resolution,[],[f73,f84]) ).
fof(f87,plain,
! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))),
inference(forward_subsumption_resolution,[],[f72,f83]) ).
fof(f88,plain,
! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))),
inference(forward_subsumption_resolution,[],[f71,f82]) ).
fof(f89,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(and(X1,X2)),not(and(X2,X0))))),
inference(forward_subsumption_resolution,[],[f70,f80]) ).
fof(f90,plain,
! [X0,X1] : is_a_theorem(implies(and(X0,X1),X0)),
inference(forward_subsumption_resolution,[],[f69,f79]) ).
fof(f91,plain,
! [X0] : is_a_theorem(implies(X0,and(X0,X0))),
inference(forward_subsumption_resolution,[],[f68,f78]) ).
fof(f92,plain,
~ is_a_theorem(implies(implies(sK0,sK2),implies(implies(sK1,sK2),implies(or(sK0,sK1),sK2)))),
inference(forward_subsumption_resolution,[],[f67,f85]) ).
fof(f93,plain,
! [X0,X1] :
( ~ is_a_theorem(equiv(X0,X1))
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f66,f81]) ).
fof(f94,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
inference(forward_subsumption_resolution,[],[f65,f77]) ).
fof(f95,plain,
! [X0,X1] : or(X0,X1) = implies(not(X0),X1),
inference(forward_demodulation,[],[f88,f87]) ).
fof(f97,plain,
! [X2,X0,X1] : or(and(X0,not(X1)),X2) = implies(implies(X0,X1),X2),
inference(superposition,[],[f95,f87]) ).
fof(f98,plain,
! [X0] : is_a_theorem(or(X0,and(not(X0),not(X0)))),
inference(superposition,[],[f91,f95]) ).
fof(f99,plain,
! [X0] :
( is_a_theorem(and(X0,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f94,f91]) ).
fof(f101,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,X1))
| ~ is_a_theorem(not(X0))
| is_a_theorem(X1) ),
inference(superposition,[],[f94,f95]) ).
fof(f102,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(not(and(X1,X2)),not(and(X2,X0)))) ),
inference(resolution,[],[f89,f94]) ).
fof(f104,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X2,X0),implies(implies(X0,X1),not(and(not(X1),X2))))),
inference(superposition,[],[f89,f87]) ).
fof(f105,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(X1),X2),implies(not(and(X2,X0)),implies(X0,X1)))),
inference(superposition,[],[f89,f87]) ).
fof(f106,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X2,X0),or(and(X0,X1),not(and(X1,X2))))),
inference(superposition,[],[f89,f95]) ).
fof(f107,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(X1),X2),or(and(X2,X0),implies(X0,X1)))),
inference(forward_demodulation,[],[f105,f95]) ).
fof(f109,plain,
! [X2,X0,X1] :
( is_a_theorem(or(and(X1,X2),not(and(X2,X0))))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[],[f102,f95]) ).
fof(f110,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(X1,X2),or(and(X2,X0),implies(X0,X1)))),
inference(forward_demodulation,[],[f107,f95]) ).
fof(f113,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(X1,X2),or(and(X2,not(X0)),or(X0,X1)))),
inference(superposition,[],[f110,f95]) ).
fof(f114,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(X1,X2),implies(implies(X2,X0),or(X0,X1)))),
inference(forward_demodulation,[],[f113,f97]) ).
fof(f115,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),or(X2,X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f114,f94]) ).
fof(f117,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(X0,X1))
| ~ is_a_theorem(implies(X1,X2))
| is_a_theorem(or(X2,X0)) ),
inference(resolution,[],[f115,f94]) ).
fof(f128,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(not(and(X1,X2)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(not(and(X2,X0))) ),
inference(resolution,[],[f109,f101]) ).
fof(f135,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),not(and(not(X1),X2))))
| ~ is_a_theorem(implies(X2,X0)) ),
inference(superposition,[],[f109,f97]) ).
fof(f183,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(not(and(not(X2),X0))) ),
inference(resolution,[],[f135,f94]) ).
fof(f197,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,and(X1,X2)))
| is_a_theorem(not(and(not(X1),X0))) ),
inference(resolution,[],[f183,f90]) ).
fof(f202,plain,
! [X0] : is_a_theorem(not(and(not(X0),X0))),
inference(resolution,[],[f197,f91]) ).
fof(f209,plain,
! [X0] : is_a_theorem(implies(not(not(X0)),X0)),
inference(superposition,[],[f202,f87]) ).
fof(f210,plain,
! [X0] : is_a_theorem(or(not(X0),X0)),
inference(forward_demodulation,[],[f209,f95]) ).
fof(f211,plain,
! [X0,X1] :
( is_a_theorem(or(X1,not(X0)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f210,f117]) ).
fof(f213,plain,
! [X0,X1] : is_a_theorem(or(implies(X0,X1),and(X0,not(X1)))),
inference(superposition,[],[f210,f87]) ).
fof(f214,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(not(X0),X2))
| is_a_theorem(or(X2,X1)) ),
inference(resolution,[],[f211,f117]) ).
fof(f215,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(not(X1))
| is_a_theorem(not(X0)) ),
inference(resolution,[],[f211,f101]) ).
fof(f218,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(X0,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(or(X2,X1)) ),
inference(forward_demodulation,[],[f214,f95]) ).
fof(f221,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(or(and(not(X0),not(X0)),X1)) ),
inference(resolution,[],[f218,f98]) ).
fof(f226,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),X0),X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[],[f221,f97]) ).
fof(f227,plain,
! [X0,X1] :
( is_a_theorem(implies(or(X0,X0),X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[],[f226,f95]) ).
fof(f229,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f227,f94]) ).
fof(f262,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,not(X1)))
| is_a_theorem(not(and(X1,X0))) ),
inference(resolution,[],[f128,f202]) ).
fof(f270,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,not(X1)))
| is_a_theorem(not(and(X1,not(X0)))) ),
inference(superposition,[],[f262,f95]) ).
fof(f271,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,not(X1)))
| is_a_theorem(implies(X1,X0)) ),
inference(forward_demodulation,[],[f270,f87]) ).
fof(f274,plain,
! [X0] : is_a_theorem(implies(X0,not(not(X0)))),
inference(resolution,[],[f271,f210]) ).
fof(f275,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(and(X0,X1),and(X2,X0)))
| ~ is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f271,f109]) ).
fof(f280,plain,
! [X0] :
( is_a_theorem(not(not(X0)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f274,f94]) ).
fof(f286,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(and(X2,X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(and(X1,X2)) ),
inference(resolution,[],[f275,f94]) ).
fof(f291,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(and(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f286,f99]) ).
fof(f322,plain,
! [X0,X1] :
( is_a_theorem(not(and(X0,X1)))
| ~ is_a_theorem(not(X0)) ),
inference(resolution,[],[f215,f90]) ).
fof(f332,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(not(X0)) ),
inference(superposition,[],[f322,f87]) ).
fof(f339,plain,
! [X0,X1] :
( is_a_theorem(not(and(X1,X0)))
| ~ is_a_theorem(not(X0)) ),
inference(resolution,[],[f332,f262]) ).
fof(f358,plain,
! [X0,X1] :
( ~ is_a_theorem(not(not(X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(superposition,[],[f339,f87]) ).
fof(f359,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X1) ),
inference(resolution,[],[f358,f280]) ).
fof(f364,plain,
! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(X1) ),
inference(resolution,[],[f359,f291]) ).
fof(f379,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(equiv(X0,X1)) ),
inference(superposition,[],[f364,f86]) ).
fof(f381,plain,
! [X0] :
( ~ is_a_theorem(implies(and(X0,X0),X0))
| is_a_theorem(equiv(and(X0,X0),X0)) ),
inference(resolution,[],[f379,f91]) ).
fof(f382,plain,
! [X0] :
( ~ is_a_theorem(implies(not(not(X0)),X0))
| is_a_theorem(equiv(not(not(X0)),X0)) ),
inference(resolution,[],[f379,f274]) ).
fof(f400,plain,
! [X0] :
( ~ is_a_theorem(or(not(X0),X0))
| is_a_theorem(equiv(not(not(X0)),X0)) ),
inference(forward_demodulation,[],[f382,f95]) ).
fof(f401,plain,
! [X0] : is_a_theorem(equiv(and(X0,X0),X0)),
inference(forward_subsumption_resolution,[],[f381,f90]) ).
fof(f403,plain,
! [X0] : is_a_theorem(equiv(not(not(X0)),X0)),
inference(forward_subsumption_resolution,[],[f400,f210]) ).
fof(f404,plain,
! [X0] : and(X0,X0) = X0,
inference(resolution,[],[f401,f93]) ).
fof(f409,plain,
! [X0] : implies(not(X0),X0) = not(not(X0)),
inference(superposition,[],[f87,f404]) ).
fof(f416,plain,
! [X0] : is_a_theorem(implies(X0,X0)),
inference(superposition,[],[f90,f404]) ).
fof(f433,plain,
! [X0] : is_a_theorem(or(X0,not(X0))),
inference(superposition,[],[f98,f404]) ).
fof(f442,plain,
! [X0] : or(X0,X0) = not(not(X0)),
inference(forward_demodulation,[],[f409,f95]) ).
fof(f481,plain,
! [X0] : not(not(X0)) = X0,
inference(resolution,[],[f403,f93]) ).
fof(f483,plain,
! [X0,X1] : and(X0,not(X1)) = not(implies(X0,X1)),
inference(superposition,[],[f481,f87]) ).
fof(f489,plain,
! [X0,X1] : implies(X1,not(X0)) = not(and(X1,X0)),
inference(superposition,[],[f87,f481]) ).
fof(f490,plain,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
inference(superposition,[],[f95,f481]) ).
fof(f491,plain,
! [X2,X0,X1] : implies(implies(X1,not(X0)),X2) = or(and(X1,X0),X2),
inference(superposition,[],[f97,f481]) ).
fof(f516,plain,
! [X0] : not(X0) = implies(X0,not(X0)),
inference(superposition,[],[f489,f404]) ).
fof(f548,plain,
! [X0,X1] : and(X0,X1) = not(implies(X0,not(X1))),
inference(superposition,[],[f481,f489]) ).
fof(f581,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),implies(not(X0),not(and(not(not(X0)),X1))))),
inference(superposition,[],[f104,f516]) ).
fof(f606,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),or(X0,not(and(not(not(X0)),X1))))),
inference(forward_demodulation,[],[f581,f95]) ).
fof(f622,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),or(X0,implies(not(not(X0)),not(X1))))),
inference(forward_demodulation,[],[f606,f489]) ).
fof(f635,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),or(X0,or(not(X0),not(X1))))),
inference(forward_demodulation,[],[f622,f95]) ).
fof(f644,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),or(X0,implies(X0,not(X1))))),
inference(forward_demodulation,[],[f635,f490]) ).
fof(f651,plain,
! [X2,X0,X1] : implies(and(X0,X1),X2) = or(implies(X0,not(X1)),X2),
inference(superposition,[],[f490,f489]) ).
fof(f693,plain,
! [X0] : is_a_theorem(implies(implies(X0,X0),or(X0,not(X0)))),
inference(superposition,[],[f644,f516]) ).
fof(f717,plain,
! [X0] : is_a_theorem(implies(or(X0,not(X0)),or(not(X0),not(not(X0))))),
inference(superposition,[],[f693,f95]) ).
fof(f727,plain,
! [X0] : is_a_theorem(implies(or(X0,not(X0)),implies(X0,not(not(X0))))),
inference(forward_demodulation,[],[f717,f490]) ).
fof(f734,plain,
! [X0] : is_a_theorem(implies(or(X0,not(X0)),implies(X0,X0))),
inference(forward_demodulation,[],[f727,f481]) ).
fof(f738,plain,
! [X0] :
( ~ is_a_theorem(implies(implies(X0,X0),or(X0,not(X0))))
| is_a_theorem(equiv(implies(X0,X0),or(X0,not(X0)))) ),
inference(resolution,[],[f734,f379]) ).
fof(f756,plain,
! [X0] : is_a_theorem(equiv(implies(X0,X0),or(X0,not(X0)))),
inference(forward_subsumption_resolution,[],[f738,f693]) ).
fof(f768,plain,
! [X0] : implies(X0,X0) = or(X0,not(X0)),
inference(resolution,[],[f756,f93]) ).
fof(f810,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X0),implies(implies(not(X0),X1),or(X1,X0)))),
inference(superposition,[],[f114,f768]) ).
fof(f826,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X0),implies(or(X0,X1),or(X1,X0)))),
inference(forward_demodulation,[],[f810,f95]) ).
fof(f851,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X0))
| is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(resolution,[],[f826,f94]) ).
fof(f869,plain,
! [X0,X1] : is_a_theorem(implies(or(X0,X1),or(X1,X0))),
inference(forward_subsumption_resolution,[],[f851,f416]) ).
fof(f881,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(or(X0,X1),or(X1,X0)))
| is_a_theorem(equiv(or(X0,X1),or(X1,X0))) ),
inference(resolution,[],[f869,f379]) ).
fof(f899,plain,
! [X0,X1] : is_a_theorem(equiv(or(X0,X1),or(X1,X0))),
inference(forward_subsumption_resolution,[],[f881,f869]) ).
fof(f958,plain,
! [X0,X1] : or(X0,X1) = or(X1,X0),
inference(resolution,[],[f899,f93]) ).
fof(f1008,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(X0,X1),implies(implies(X0,X2),or(X2,X1)))),
inference(superposition,[],[f114,f958]) ).
fof(f1024,plain,
! [X0,X1] : implies(X1,X0) = or(X0,not(X1)),
inference(superposition,[],[f490,f958]) ).
fof(f1027,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X1,X2),or(not(and(X0,X1)),and(X2,X0)))),
inference(superposition,[],[f106,f958]) ).
fof(f1032,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X1,X2),implies(and(X0,X1),and(X2,X0)))),
inference(forward_demodulation,[],[f1027,f490]) ).
fof(f1047,plain,
! [X2,X0,X1] : implies(and(X0,X1),X2) = or(X2,implies(X0,not(X1))),
inference(superposition,[],[f1024,f489]) ).
fof(f1066,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X2),or(X2,X1)))),
inference(superposition,[],[f114,f1024]) ).
fof(f1081,plain,
! [X0,X1] : implies(X1,not(X0)) = implies(X0,not(X1)),
inference(superposition,[],[f490,f1024]) ).
fof(f1095,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(or(X0,X2),or(X2,X1)))),
inference(forward_demodulation,[],[f1066,f95]) ).
fof(f1125,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X1,X2),implies(or(X0,X1),or(X0,X2)))),
inference(superposition,[],[f1095,f958]) ).
fof(f1128,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),implies(or(X1,X0),not(not(X0))))),
inference(superposition,[],[f1095,f442]) ).
fof(f1133,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X2,X1),implies(or(X2,not(X0)),implies(X0,X1)))),
inference(superposition,[],[f1095,f490]) ).
fof(f1134,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X2,X1),implies(implies(X0,X2),implies(X0,X1)))),
inference(forward_demodulation,[],[f1133,f1024]) ).
fof(f1137,plain,
! [X0,X1] : is_a_theorem(implies(implies(X1,X0),implies(or(X1,X0),X0))),
inference(forward_demodulation,[],[f1128,f481]) ).
fof(f1196,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(implies(X0,X1),X1))),
inference(superposition,[],[f1137,f490]) ).
fof(f1197,plain,
! [X0,X1] : is_a_theorem(implies(or(X0,X1),implies(implies(X0,X1),X1))),
inference(forward_demodulation,[],[f1196,f95]) ).
fof(f1438,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(not(and(not(implies(or(X3,X1),or(X3,X2))),X0))) ),
inference(resolution,[],[f1125,f183]) ).
fof(f1468,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(not(implies(or(X3,X1),or(X3,X2))),not(X0)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(forward_demodulation,[],[f1438,f489]) ).
fof(f1471,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(or(implies(or(X3,X1),or(X3,X2)),not(X0)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(forward_demodulation,[],[f1468,f95]) ).
fof(f1472,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(or(X3,X1),or(X3,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(forward_demodulation,[],[f1471,f1024]) ).
fof(f1576,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,and(X1,X0)))),
inference(superposition,[],[f1032,f404]) ).
fof(f1685,plain,
! [X0,X1] : is_a_theorem(implies(X0,not(and(not(X0),X1)))),
inference(superposition,[],[f90,f1081]) ).
fof(f1709,plain,
! [X0,X1] : is_a_theorem(or(implies(X0,not(X1)),and(X1,not(not(X0))))),
inference(superposition,[],[f213,f1081]) ).
fof(f1772,plain,
! [X0,X1] : is_a_theorem(implies(and(X0,X1),and(X1,not(not(X0))))),
inference(forward_demodulation,[],[f1709,f651]) ).
fof(f1794,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),not(X1)))),
inference(forward_demodulation,[],[f1685,f489]) ).
fof(f1882,plain,
! [X0,X1] : is_a_theorem(implies(and(X0,X1),not(implies(X1,not(X0))))),
inference(forward_demodulation,[],[f1772,f483]) ).
fof(f1901,plain,
! [X0,X1] : is_a_theorem(implies(X0,or(X0,not(X1)))),
inference(forward_demodulation,[],[f1794,f95]) ).
fof(f1951,plain,
! [X0,X1] : is_a_theorem(implies(and(X0,X1),and(X1,X0))),
inference(forward_demodulation,[],[f1882,f548]) ).
fof(f1962,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(forward_demodulation,[],[f1901,f1024]) ).
fof(f2002,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(not(and(not(implies(X2,X1)),X0))) ),
inference(resolution,[],[f1962,f183]) ).
fof(f2004,plain,
! [X0,X1] : is_a_theorem(implies(X1,or(X0,X1))),
inference(superposition,[],[f1962,f95]) ).
fof(f2008,plain,
! [X0,X1] : is_a_theorem(or(X0,implies(X1,not(X0)))),
inference(superposition,[],[f1962,f95]) ).
fof(f2009,plain,
! [X0,X1] : is_a_theorem(implies(and(X1,X0),X0)),
inference(forward_demodulation,[],[f2008,f1047]) ).
fof(f2012,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(not(implies(X2,X1)),not(X0)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[],[f2002,f489]) ).
fof(f2015,plain,
! [X2,X0,X1] :
( is_a_theorem(or(implies(X2,X1),not(X0)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[],[f2012,f95]) ).
fof(f2016,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(forward_demodulation,[],[f2015,f1024]) ).
fof(f2069,plain,
! [X0,X1] : is_a_theorem(or(X0,or(X1,not(X0)))),
inference(superposition,[],[f2004,f95]) ).
fof(f2070,plain,
! [X0,X1] : is_a_theorem(or(X0,implies(X0,X1))),
inference(forward_demodulation,[],[f2069,f1024]) ).
fof(f2082,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f2016,f94]) ).
fof(f2096,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(and(X0,X1),and(X1,X0)))
| is_a_theorem(equiv(and(X0,X1),and(X1,X0))) ),
inference(resolution,[],[f1951,f379]) ).
fof(f2113,plain,
! [X0,X1] : is_a_theorem(equiv(and(X0,X1),and(X1,X0))),
inference(forward_subsumption_resolution,[],[f2096,f1951]) ).
fof(f2473,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,not(and(not(X1),X3))))
| ~ is_a_theorem(implies(X3,X0)) ),
inference(resolution,[],[f2082,f135]) ).
fof(f2494,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,not(X0)))
| is_a_theorem(implies(X1,implies(X0,X0))) ),
inference(resolution,[],[f2082,f734]) ).
fof(f2499,plain,
! [X0,X1] : is_a_theorem(implies(X1,implies(X0,X0))),
inference(forward_subsumption_resolution,[],[f2494,f433]) ).
fof(f2507,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X2,implies(not(X1),not(X3))))
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X3,X0)) ),
inference(forward_demodulation,[],[f2473,f489]) ).
fof(f2518,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X2,or(X1,not(X3))))
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X3,X0)) ),
inference(forward_demodulation,[],[f2507,f95]) ).
fof(f2521,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,implies(X3,X1))) ),
inference(forward_demodulation,[],[f2518,f1024]) ).
fof(f2634,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),or(X0,and(X1,not(X0))))),
inference(superposition,[],[f1576,f95]) ).
fof(f2635,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),or(X0,not(implies(X1,X0))))),
inference(forward_demodulation,[],[f2634,f483]) ).
fof(f2642,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))),
inference(forward_demodulation,[],[f2635,f1024]) ).
fof(f2646,plain,
! [X0,X1] : is_a_theorem(implies(or(X0,X1),implies(implies(X1,X0),X0))),
inference(forward_demodulation,[],[f2642,f95]) ).
fof(f2949,plain,
! [X0,X1] : and(X0,X1) = and(X1,X0),
inference(resolution,[],[f2113,f93]) ).
fof(f3053,plain,
! [X2,X0,X1] : implies(implies(X1,X0),X2) = or(and(not(X0),X1),X2),
inference(superposition,[],[f97,f2949]) ).
fof(f3125,plain,
! [X2,X0,X1] : implies(implies(not(X0),X1),X2) = implies(implies(not(X1),X0),X2),
inference(superposition,[],[f97,f3053]) ).
fof(f3145,plain,
! [X2,X0,X1] : implies(implies(X0,X1),X2) = or(X2,and(not(X1),X0)),
inference(superposition,[],[f958,f3053]) ).
fof(f3208,plain,
! [X2,X0,X1] : implies(implies(not(X0),X1),X2) = implies(or(X1,X0),X2),
inference(forward_demodulation,[],[f3125,f95]) ).
fof(f3226,plain,
! [X2,X0,X1] : implies(or(X0,X1),X2) = implies(or(X1,X0),X2),
inference(forward_demodulation,[],[f3208,f95]) ).
fof(f3406,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(or(X0,X1),X2),not(and(not(X2),X3))))
| ~ is_a_theorem(implies(X3,or(X1,X0))) ),
inference(superposition,[],[f135,f3226]) ).
fof(f3511,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(or(X0,X1),X2),implies(not(X2),not(X3))))
| ~ is_a_theorem(implies(X3,or(X1,X0))) ),
inference(forward_demodulation,[],[f3406,f489]) ).
fof(f3543,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(or(X0,X1),X2),or(X2,not(X3))))
| ~ is_a_theorem(implies(X3,or(X1,X0))) ),
inference(forward_demodulation,[],[f3511,f95]) ).
fof(f3558,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(or(X0,X1),X2),implies(X3,X2)))
| ~ is_a_theorem(implies(X3,or(X1,X0))) ),
inference(forward_demodulation,[],[f3543,f1024]) ).
fof(f4543,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X3,implies(X1,X2))) ),
inference(resolution,[],[f2521,f1962]) ).
fof(f4661,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(or(X2,X0)) ),
inference(resolution,[],[f2070,f117]) ).
fof(f4732,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[],[f4543,f416]) ).
fof(f5088,plain,
! [X0,X1] : and(not(X1),X0) = not(implies(X0,X1)),
inference(superposition,[],[f2949,f483]) ).
fof(f6189,plain,
! [X0,X1] : is_a_theorem(or(implies(X0,X0),X1)),
inference(resolution,[],[f4661,f2499]) ).
fof(f6227,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(or(X0,X1),X2))
| is_a_theorem(or(X2,not(X0))) ),
inference(superposition,[],[f4661,f95]) ).
fof(f6241,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(or(X0,X1),X2))
| is_a_theorem(implies(X0,X2)) ),
inference(forward_demodulation,[],[f6227,f1024]) ).
fof(f6258,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f6189,f229]) ).
fof(f6393,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),or(X1,X2)))),
inference(resolution,[],[f6241,f1008]) ).
fof(f6396,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(resolution,[],[f6241,f1197]) ).
fof(f6473,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),X1)),
inference(resolution,[],[f6396,f6258]) ).
fof(f6474,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f6396,f94]) ).
fof(f6514,plain,
! [X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X1,implies(X0,X1)))
| is_a_theorem(equiv(X1,implies(X0,X1))) ),
inference(resolution,[],[f6474,f379]) ).
fof(f6541,plain,
! [X0,X1] :
( is_a_theorem(equiv(X1,implies(X0,X1)))
| ~ is_a_theorem(X0) ),
inference(forward_subsumption_resolution,[],[f6514,f1962]) ).
fof(f6772,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X1),X0)))
| is_a_theorem(equiv(X0,implies(implies(X1,X1),X0))) ),
inference(resolution,[],[f6473,f379]) ).
fof(f6804,plain,
! [X0,X1] : is_a_theorem(equiv(X0,implies(implies(X1,X1),X0))),
inference(forward_subsumption_resolution,[],[f6772,f1962]) ).
fof(f6817,plain,
! [X0,X1] : implies(implies(X1,X1),X0) = X0,
inference(resolution,[],[f6804,f93]) ).
fof(f7046,plain,
! [X0,X1] : not(X0) = implies(X0,not(implies(X1,X1))),
inference(superposition,[],[f1081,f6817]) ).
fof(f7766,plain,
! [X0,X1] : not(implies(X0,X0)) = not(implies(X1,X1)),
inference(superposition,[],[f6817,f7046]) ).
fof(f7784,plain,
! [X2,X0,X1] : not(or(X0,X1)) = implies(or(X1,X0),not(implies(X2,X2))),
inference(superposition,[],[f3226,f7046]) ).
fof(f7802,plain,
! [X0,X1] : not(or(X0,X1)) = not(or(X1,X0)),
inference(forward_demodulation,[],[f7784,f7046]) ).
fof(f8092,plain,
! [X2,X0,X1] : implies(X2,or(X1,X0)) = not(and(X2,not(or(X0,X1)))),
inference(superposition,[],[f87,f7802]) ).
fof(f8093,plain,
! [X2,X0,X1] : or(or(X1,X0),X2) = implies(not(or(X0,X1)),X2),
inference(superposition,[],[f95,f7802]) ).
fof(f8160,plain,
! [X2,X0,X1] : or(or(X1,X0),X2) = or(or(X0,X1),X2),
inference(forward_demodulation,[],[f8093,f95]) ).
fof(f8161,plain,
! [X2,X0,X1] : implies(X2,or(X0,X1)) = implies(X2,or(X1,X0)),
inference(forward_demodulation,[],[f8092,f87]) ).
fof(f8629,plain,
! [X2,X0,X1] : implies(not(X0),or(X1,X2)) = or(X0,or(X2,X1)),
inference(superposition,[],[f95,f8161]) ).
fof(f8656,plain,
! [X2,X0,X1] : or(X0,or(X1,X2)) = or(X0,or(X2,X1)),
inference(forward_demodulation,[],[f8629,f95]) ).
fof(f8845,plain,
! [X0,X1] : implies(X1,X1) = not(not(implies(X0,X0))),
inference(superposition,[],[f481,f7766]) ).
fof(f8877,plain,
! [X0,X1] : implies(X0,X0) = implies(X1,X1),
inference(forward_demodulation,[],[f8845,f481]) ).
fof(f10316,plain,
! [X0,X1] : not(not(or(X1,X0))) = or(or(X0,X1),or(X1,X0)),
inference(superposition,[],[f442,f8160]) ).
fof(f10435,plain,
! [X0,X1] : or(X1,X0) = or(or(X0,X1),or(X1,X0)),
inference(forward_demodulation,[],[f10316,f481]) ).
fof(f11716,plain,
! [X0,X1] :
( ~ is_a_theorem(X0)
| implies(X0,X1) = X1 ),
inference(resolution,[],[f6541,f93]) ).
fof(f11743,plain,
! [X2,X0,X1] : implies(implies(X0,implies(X1,X0)),X2) = X2,
inference(resolution,[],[f11716,f1962]) ).
fof(f11781,plain,
! [X2,X0,X1] : implies(implies(X0,or(X1,X0)),X2) = X2,
inference(resolution,[],[f11716,f2004]) ).
fof(f11834,plain,
! [X2,X0,X1] : implies(implies(and(X0,X1),X1),X2) = X2,
inference(resolution,[],[f11716,f2009]) ).
fof(f12013,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X0)) = implies(X2,X2),
inference(superposition,[],[f8877,f11743]) ).
fof(f13169,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,and(X1,X2)),implies(X0,X2))),
inference(superposition,[],[f1134,f11834]) ).
fof(f13255,plain,
! [X2,X0,X1] : is_a_theorem(implies(and(X2,X0),or(X0,X1))),
inference(superposition,[],[f6393,f11834]) ).
fof(f13418,plain,
! [X2,X0,X1] : is_a_theorem(implies(and(X2,not(X0)),implies(X0,X1))),
inference(superposition,[],[f13255,f490]) ).
fof(f13427,plain,
! [X2,X0,X1] : is_a_theorem(implies(not(implies(X2,X0)),implies(X0,X1))),
inference(forward_demodulation,[],[f13418,f483]) ).
fof(f13435,plain,
! [X2,X0,X1] : is_a_theorem(or(implies(X2,X0),implies(X0,X1))),
inference(forward_demodulation,[],[f13427,f95]) ).
fof(f13868,plain,
! [X2,X0,X1] : implies(X2,X2) = implies(X0,or(X1,X0)),
inference(superposition,[],[f8877,f11781]) ).
fof(f14573,plain,
! [X2,X0,X1] : implies(X0,X0) = implies(X1,or(X1,X2)),
inference(superposition,[],[f8161,f13868]) ).
fof(f14704,plain,
! [X2,X0,X1] : implies(X0,X0) = or(X1,or(X2,not(X1))),
inference(superposition,[],[f95,f13868]) ).
fof(f14730,plain,
! [X2,X0,X1] : implies(X0,X0) = or(X1,implies(X1,X2)),
inference(forward_demodulation,[],[f14704,f1024]) ).
fof(f15266,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X0),implies(implies(implies(X1,X2),X1),X1))),
inference(superposition,[],[f2646,f14730]) ).
fof(f15311,plain,
! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1)),
inference(forward_demodulation,[],[f15266,f6817]) ).
fof(f15443,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X0,X1),X0)))
| is_a_theorem(equiv(X0,implies(implies(X0,X1),X0))) ),
inference(resolution,[],[f15311,f379]) ).
fof(f15488,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,not(implies(not(X0),X1))),not(X0))),
inference(superposition,[],[f15311,f1081]) ).
fof(f15504,plain,
! [X0,X1] : is_a_theorem(or(and(X0,implies(not(X0),X1)),not(X0))),
inference(forward_demodulation,[],[f15488,f491]) ).
fof(f15515,plain,
! [X0,X1] : is_a_theorem(equiv(X0,implies(implies(X0,X1),X0))),
inference(forward_subsumption_resolution,[],[f15443,f1962]) ).
fof(f15520,plain,
! [X0,X1] : is_a_theorem(implies(X0,and(X0,implies(not(X0),X1)))),
inference(forward_demodulation,[],[f15504,f1024]) ).
fof(f15528,plain,
! [X0,X1] : is_a_theorem(implies(X0,and(X0,or(X0,X1)))),
inference(forward_demodulation,[],[f15520,f95]) ).
fof(f15537,plain,
! [X0,X1] : implies(implies(X0,X1),X0) = X0,
inference(resolution,[],[f15515,f93]) ).
fof(f15627,plain,
! [X0,X1] : implies(X0,X1) = implies(X0,implies(X0,X1)),
inference(superposition,[],[f15537,f15537]) ).
fof(f15628,plain,
! [X0,X1] : not(X0) = implies(or(X0,X1),not(X0)),
inference(superposition,[],[f15537,f95]) ).
fof(f15816,plain,
! [X0,X1] : not(X0) = implies(X0,not(implies(not(X0),X1))),
inference(superposition,[],[f1081,f15537]) ).
fof(f15856,plain,
! [X0,X1] : not(X0) = implies(X0,not(or(X0,X1))),
inference(forward_demodulation,[],[f15816,f95]) ).
fof(f16112,plain,
! [X0,X1] : implies(not(X0),X1) = or(X0,implies(not(X0),X1)),
inference(superposition,[],[f95,f15627]) ).
fof(f16130,plain,
! [X0,X1] : or(X0,X1) = or(X0,or(X0,X1)),
inference(forward_demodulation,[],[f16112,f95]) ).
fof(f16172,plain,
! [X0,X1] : implies(X0,X1) = or(X1,implies(X0,X1)),
inference(superposition,[],[f16130,f1024]) ).
fof(f16193,plain,
! [X0,X1] : or(X0,X1) = or(X0,or(X1,X0)),
inference(superposition,[],[f8656,f16130]) ).
fof(f17663,plain,
! [X0,X1] : not(X1) = implies(X1,not(implies(X0,X1))),
inference(superposition,[],[f15856,f1024]) ).
fof(f18958,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(and(X0,or(X0,X1)),X0))
| is_a_theorem(equiv(and(X0,or(X0,X1)),X0)) ),
inference(resolution,[],[f15528,f379]) ).
fof(f19000,plain,
! [X0,X1] : is_a_theorem(equiv(and(X0,or(X0,X1)),X0)),
inference(forward_subsumption_resolution,[],[f18958,f90]) ).
fof(f20064,plain,
! [X0,X1] : not(X0) = implies(or(X1,X0),not(X0)),
inference(superposition,[],[f3226,f15628]) ).
fof(f20220,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(not(X0),X1),or(and(X1,or(X2,X0)),not(X0)))),
inference(superposition,[],[f110,f20064]) ).
fof(f20377,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(not(X0),X1),implies(X0,and(X1,or(X2,X0))))),
inference(forward_demodulation,[],[f20220,f1024]) ).
fof(f20409,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,and(X1,or(X2,X0))))),
inference(forward_demodulation,[],[f20377,f490]) ).
fof(f20513,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X1,X2),implies(X1,and(or(X0,X1),X2)))),
inference(superposition,[],[f20409,f2949]) ).
fof(f21200,plain,
! [X0,X1] : or(or(X1,X0),or(X0,X1)) = or(or(X1,X0),X0),
inference(superposition,[],[f16193,f16193]) ).
fof(f21351,plain,
! [X0,X1] : or(X0,X1) = or(or(X1,X0),X0),
inference(forward_demodulation,[],[f21200,f10435]) ).
fof(f24467,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,and(or(X1,X0),X2)),implies(X0,X2)))
| is_a_theorem(equiv(implies(X0,and(or(X1,X0),X2)),implies(X0,X2))) ),
inference(resolution,[],[f20513,f379]) ).
fof(f24589,plain,
! [X2,X0,X1] : is_a_theorem(equiv(implies(X0,and(or(X1,X0),X2)),implies(X0,X2))),
inference(forward_subsumption_resolution,[],[f24467,f13169]) ).
fof(f26338,plain,
! [X0,X1] : and(X0,or(X0,X1)) = X0,
inference(resolution,[],[f19000,f93]) ).
fof(f26384,plain,
! [X0,X1] : and(X1,implies(X0,X1)) = X1,
inference(superposition,[],[f26338,f1024]) ).
fof(f26614,plain,
! [X2,X0,X1] : and(X2,implies(X0,implies(X1,X0))) = X2,
inference(superposition,[],[f26384,f12013]) ).
fof(f26616,plain,
! [X2,X0,X1] : and(X2,implies(X0,or(X1,X0))) = X2,
inference(superposition,[],[f26384,f13868]) ).
fof(f26617,plain,
! [X2,X0,X1] : and(X2,implies(X0,or(X0,X1))) = X2,
inference(superposition,[],[f26384,f14573]) ).
fof(f28587,plain,
! [X2,X0,X1] : implies(X0,X2) = implies(X0,and(or(X1,X0),X2)),
inference(resolution,[],[f24589,f93]) ).
fof(f28756,plain,
! [X0,X1] : implies(X0,X1) = implies(X0,and(not(not(X0)),X1)),
inference(superposition,[],[f28587,f442]) ).
fof(f28772,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(X1,and(implies(X0,X1),X2)),
inference(superposition,[],[f28587,f490]) ).
fof(f29058,plain,
! [X0,X1] : implies(X0,X1) = implies(X0,not(implies(X1,not(X0)))),
inference(forward_demodulation,[],[f28756,f5088]) ).
fof(f29083,plain,
! [X0,X1] : implies(X0,X1) = implies(X0,and(X1,X0)),
inference(forward_demodulation,[],[f29058,f548]) ).
fof(f29284,plain,
! [X0,X1] : implies(not(X0),X1) = or(X0,and(X1,not(X0))),
inference(superposition,[],[f95,f29083]) ).
fof(f29328,plain,
! [X0,X1] : implies(not(X0),X1) = or(X0,not(implies(X1,X0))),
inference(forward_demodulation,[],[f29284,f483]) ).
fof(f29379,plain,
! [X0,X1] : implies(not(X0),X1) = implies(implies(X1,X0),X0),
inference(forward_demodulation,[],[f29328,f1024]) ).
fof(f29392,plain,
! [X0,X1] : or(X0,X1) = implies(implies(X1,X0),X0),
inference(forward_demodulation,[],[f29379,f95]) ).
fof(f29428,plain,
! [X0,X1] : implies(or(X0,X1),X0) = or(X0,implies(X1,X0)),
inference(superposition,[],[f29392,f29392]) ).
fof(f29436,plain,
! [X0,X1] : or(X1,not(X0)) = implies(or(X0,X1),X1),
inference(superposition,[],[f29392,f95]) ).
fof(f29478,plain,
! [X0,X1] : equiv(implies(X1,X0),X0) = and(or(X0,X1),implies(X0,implies(X1,X0))),
inference(superposition,[],[f86,f29392]) ).
fof(f29757,plain,
! [X0,X1] : or(X0,X1) = equiv(implies(X1,X0),X0),
inference(forward_demodulation,[],[f29478,f26614]) ).
fof(f29777,plain,
! [X0,X1] : implies(X0,X1) = implies(or(X0,X1),X1),
inference(forward_demodulation,[],[f29436,f1024]) ).
fof(f29779,plain,
! [X0,X1] : implies(X1,X0) = implies(or(X0,X1),X0),
inference(forward_demodulation,[],[f29428,f16172]) ).
fof(f29868,plain,
! [X0,X1] : implies(X1,not(X0)) = implies(implies(X0,X1),not(X0)),
inference(superposition,[],[f29777,f1024]) ).
fof(f29905,plain,
! [X0,X1] : equiv(or(X0,X1),X1) = and(implies(X0,X1),implies(X1,or(X0,X1))),
inference(superposition,[],[f86,f29777]) ).
fof(f30060,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(X2,or(X1,X0))) ),
inference(superposition,[],[f3558,f29777]) ).
fof(f30178,plain,
! [X0,X1] : implies(X0,X1) = equiv(or(X0,X1),X1),
inference(forward_demodulation,[],[f29905,f26616]) ).
fof(f30276,plain,
! [X0,X1] : equiv(or(X1,X0),X1) = and(implies(X0,X1),implies(X1,or(X1,X0))),
inference(superposition,[],[f86,f29779]) ).
fof(f30556,plain,
! [X0,X1] : implies(X0,X1) = equiv(or(X1,X0),X1),
inference(forward_demodulation,[],[f30276,f26617]) ).
fof(f30884,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| or(X0,X1) = X1 ),
inference(superposition,[],[f93,f30178]) ).
fof(f31109,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,X1))
| or(not(X0),X1) = X1 ),
inference(superposition,[],[f30884,f95]) ).
fof(f31111,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| or(or(X0,X1),X1) = X1 ),
inference(superposition,[],[f30884,f29777]) ).
fof(f31120,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| or(X1,X0) = X1 ),
inference(forward_demodulation,[],[f31111,f21351]) ).
fof(f31122,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,X1))
| implies(X0,X1) = X1 ),
inference(forward_demodulation,[],[f31109,f490]) ).
fof(f32017,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(not(X0),implies(X2,not(or(X0,X1)))))
| ~ is_a_theorem(implies(X2,or(not(or(X0,X1)),X0))) ),
inference(superposition,[],[f30060,f15856]) ).
fof(f32133,plain,
! [X2,X0,X1] :
( is_a_theorem(or(X0,implies(X2,not(or(X0,X1)))))
| ~ is_a_theorem(implies(X2,or(not(or(X0,X1)),X0))) ),
inference(forward_demodulation,[],[f32017,f95]) ).
fof(f32169,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(and(X2,or(X0,X1)),X0))
| ~ is_a_theorem(implies(X2,or(not(or(X0,X1)),X0))) ),
inference(forward_demodulation,[],[f32133,f1047]) ).
fof(f32194,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(or(X0,X1),X0)))
| is_a_theorem(implies(and(X2,or(X0,X1)),X0)) ),
inference(forward_demodulation,[],[f32169,f490]) ).
fof(f32210,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(and(X2,or(X0,X1)),X0))
| ~ is_a_theorem(implies(X2,implies(X1,X0))) ),
inference(forward_demodulation,[],[f32194,f29779]) ).
fof(f32823,plain,
! [X2,X0,X1] : implies(X1,X2) = implies(implies(X0,X1),implies(X1,X2)),
inference(resolution,[],[f31122,f13435]) ).
fof(f32935,plain,
! [X2,X0,X1] : implies(implies(X2,implies(X0,X1)),X0) = X0,
inference(superposition,[],[f32823,f15537]) ).
fof(f33414,plain,
! [X2,X0,X1] : implies(or(X0,implies(X1,X2)),X1) = X1,
inference(superposition,[],[f32935,f95]) ).
fof(f45497,plain,
! [X2,X0,X1] : implies(not(implies(X1,X0)),X2) = implies(not(implies(X1,X0)),and(not(X0),X2)),
inference(superposition,[],[f28772,f17663]) ).
fof(f45882,plain,
! [X2,X0,X1] : implies(not(implies(X1,X0)),X2) = or(implies(X1,X0),and(not(X0),X2)),
inference(forward_demodulation,[],[f45497,f95]) ).
fof(f45915,plain,
! [X2,X0,X1] : implies(implies(X2,X0),implies(X1,X0)) = implies(not(implies(X1,X0)),X2),
inference(forward_demodulation,[],[f45882,f3145]) ).
fof(f45931,plain,
! [X2,X0,X1] : implies(implies(X2,X0),implies(X1,X0)) = or(implies(X1,X0),X2),
inference(forward_demodulation,[],[f45915,f95]) ).
fof(f46343,plain,
! [X2,X0,X1] : implies(or(X0,X1),implies(X2,X0)) = or(implies(X2,X0),implies(X1,X0)),
inference(superposition,[],[f45931,f29392]) ).
fof(f46421,plain,
! [X2,X0,X1] : implies(implies(X2,X1),or(X0,X1)) = or(or(X0,X1),X2),
inference(superposition,[],[f45931,f95]) ).
fof(f46649,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(implies(X2,X1),implies(X0,X1)),implies(or(implies(X0,X1),X2),implies(X0,X1)))),
inference(superposition,[],[f1197,f45931]) ).
fof(f46758,plain,
! [X2,X0,X1] : or(implies(X0,X1),implies(X2,X1)) = equiv(or(implies(X0,X1),X2),implies(X0,X1)),
inference(superposition,[],[f29757,f45931]) ).
fof(f46813,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = or(implies(X0,X1),implies(X2,X1)),
inference(forward_demodulation,[],[f46758,f30556]) ).
fof(f46845,plain,
! [X2,X0,X1] : is_a_theorem(implies(or(implies(X2,X1),implies(X0,X1)),implies(X2,implies(X0,X1)))),
inference(forward_demodulation,[],[f46649,f29779]) ).
fof(f46953,plain,
! [X2,X0,X1] : implies(X2,implies(X0,X1)) = implies(or(X1,X2),implies(X0,X1)),
inference(forward_demodulation,[],[f46813,f46343]) ).
fof(f46964,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(or(X1,X0),implies(X2,X1)),implies(X2,implies(X0,X1)))),
inference(forward_demodulation,[],[f46845,f46343]) ).
fof(f46998,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X2,X1)),implies(X2,implies(X0,X1)))),
inference(forward_demodulation,[],[f46964,f46953]) ).
fof(f47038,plain,
! [X2,X0,X1] : implies(X1,implies(X0,X2)) = or(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2))),
inference(resolution,[],[f46998,f30884]) ).
fof(f47039,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X2)) = or(implies(X0,implies(X1,X2)),implies(X1,implies(X0,X2))),
inference(resolution,[],[f46998,f31120]) ).
fof(f47313,plain,
! [X2,X0,X1] : implies(X0,implies(X1,X2)) = implies(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f47038,f47039]) ).
fof(f48397,plain,
! [X2,X0,X1] : or(X1,implies(X0,X2)) = implies(X0,implies(not(X1),X2)),
inference(superposition,[],[f95,f47313]) ).
fof(f48455,plain,
! [X2,X0,X1] : implies(X0,or(X1,X2)) = or(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f48397,f95]) ).
fof(f48986,plain,
! [X2,X0,X1] : or(X2,implies(X0,not(X1))) = implies(X1,or(X2,not(X0))),
inference(superposition,[],[f48455,f1081]) ).
fof(f48989,plain,
! [X2,X0,X1] : or(X1,not(X0)) = implies(X0,or(X1,not(or(X0,X2)))),
inference(superposition,[],[f48455,f15856]) ).
fof(f49001,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = implies(implies(X1,X0),or(X2,X0)),
inference(superposition,[],[f48455,f29392]) ).
fof(f49013,plain,
! [X2,X0,X1] : or(X2,implies(X0,not(X1))) = implies(implies(X1,X0),or(X2,not(X1))),
inference(superposition,[],[f48455,f29868]) ).
fof(f49018,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = implies(not(X0),or(X2,X1)),
inference(superposition,[],[f48455,f95]) ).
fof(f49381,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(X0,or(X2,X1)),
inference(forward_demodulation,[],[f49018,f95]) ).
fof(f49383,plain,
! [X2,X0,X1] : or(X2,implies(X0,not(X1))) = implies(implies(X1,X0),implies(X1,X2)),
inference(forward_demodulation,[],[f49013,f1024]) ).
fof(f49388,plain,
! [X2,X0,X1] : or(X2,or(X0,X1)) = or(or(X2,X0),X1),
inference(forward_demodulation,[],[f49001,f46421]) ).
fof(f49398,plain,
! [X2,X0,X1] : or(X1,not(X0)) = implies(X0,implies(or(X0,X2),X1)),
inference(forward_demodulation,[],[f48989,f1024]) ).
fof(f49401,plain,
! [X2,X0,X1] : or(X2,implies(X0,not(X1))) = implies(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f48986,f1024]) ).
fof(f49471,plain,
! [X2,X0,X1] : implies(and(X0,X1),X2) = implies(implies(X1,X0),implies(X1,X2)),
inference(forward_demodulation,[],[f49383,f1047]) ).
fof(f49475,plain,
! [X2,X0,X1] : implies(X0,X1) = implies(X0,implies(or(X0,X2),X1)),
inference(forward_demodulation,[],[f49398,f1024]) ).
fof(f49478,plain,
! [X2,X0,X1] : implies(and(X0,X1),X2) = implies(X1,implies(X0,X2)),
inference(forward_demodulation,[],[f49401,f1047]) ).
fof(f64923,plain,
! [X2,X3,X0,X1] : implies(or(X0,X2),implies(X3,X1)) = implies(or(X0,or(X1,X2)),implies(X3,X1)),
inference(superposition,[],[f46953,f49381]) ).
fof(f66007,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(and(X0,X1),X2))
| ~ is_a_theorem(implies(X1,X0))
| is_a_theorem(implies(X1,X2)) ),
inference(superposition,[],[f94,f49471]) ).
fof(f66427,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| ~ is_a_theorem(implies(X1,X0))
| is_a_theorem(implies(X1,X2)) ),
inference(forward_demodulation,[],[f66007,f49478]) ).
fof(f73067,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(and(X0,X1),X2))
| ~ is_a_theorem(implies(implies(X1,X0),X1))
| is_a_theorem(implies(implies(X1,X0),X2)) ),
inference(superposition,[],[f66427,f49471]) ).
fof(f73106,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| ~ is_a_theorem(implies(implies(X1,X0),X1))
| is_a_theorem(implies(implies(X1,X0),X2)) ),
inference(forward_demodulation,[],[f73067,f49478]) ).
fof(f73212,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| ~ is_a_theorem(X1)
| is_a_theorem(implies(implies(X1,X0),X2)) ),
inference(forward_demodulation,[],[f73106,f15537]) ).
fof(f73989,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(or(X0,implies(X1,X2)))
| is_a_theorem(implies(implies(or(X0,implies(X1,X2)),X1),X2)) ),
inference(superposition,[],[f73212,f29777]) ).
fof(f73993,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,or(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(implies(or(X0,implies(X1,X2)),X1),X2)) ),
inference(forward_demodulation,[],[f73989,f48455]) ).
fof(f74112,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,or(X0,X2)))
| is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(forward_demodulation,[],[f73993,f33414]) ).
fof(f404532,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3))))
| is_a_theorem(implies(and(X0,or(or(X2,X3),X1)),X3))
| ~ is_a_theorem(implies(X2,implies(and(X0,or(or(X2,X3),X1)),X3))) ),
inference(resolution,[],[f32210,f74112]) ).
fof(f404728,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(or(or(X2,X3),X1),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3))))
| ~ is_a_theorem(implies(X2,implies(and(X0,or(or(X2,X3),X1)),X3))) ),
inference(forward_demodulation,[],[f404532,f49478]) ).
fof(f404862,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(or(X2,or(X3,X1)),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3))))
| ~ is_a_theorem(implies(X2,implies(and(X0,or(or(X2,X3),X1)),X3))) ),
inference(forward_demodulation,[],[f404728,f49388]) ).
fof(f404951,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(or(X2,X1),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3))))
| ~ is_a_theorem(implies(X2,implies(and(X0,or(or(X2,X3),X1)),X3))) ),
inference(forward_demodulation,[],[f404862,f64923]) ).
fof(f405017,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(or(or(X2,X3),X1),implies(X0,X3))))
| is_a_theorem(implies(or(X2,X1),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3)))) ),
inference(forward_demodulation,[],[f404951,f49478]) ).
fof(f405061,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(or(X2,or(X3,X1)),implies(X0,X3))))
| is_a_theorem(implies(or(X2,X1),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3)))) ),
inference(forward_demodulation,[],[f405017,f49388]) ).
fof(f405077,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,or(X2,X3))))
| is_a_theorem(implies(or(X2,X1),implies(X0,X3)))
| ~ is_a_theorem(implies(X2,implies(X0,X3))) ),
inference(forward_demodulation,[],[f405061,f49475]) ).
fof(f740868,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(or(X0,or(X0,X1)),implies(X2,X3)))
| ~ is_a_theorem(implies(X0,implies(X2,X3)))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(resolution,[],[f405077,f1472]) ).
fof(f741631,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(or(X0,X1),implies(X2,X3)))
| ~ is_a_theorem(implies(X0,implies(X2,X3)))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(forward_demodulation,[],[f740868,f16130]) ).
fof(f742739,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| ~ is_a_theorem(implies(not(X0),implies(X2,X3)))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(superposition,[],[f741631,f490]) ).
fof(f743168,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(X0,implies(X2,X3)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(forward_demodulation,[],[f742739,f95]) ).
fof(f743263,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| ~ is_a_theorem(implies(X2,or(X0,X3)))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(forward_demodulation,[],[f743168,f48455]) ).
fof(f743312,plain,
( ~ is_a_theorem(implies(implies(sK1,sK2),or(sK0,implies(or(sK0,sK1),sK2))))
| ~ is_a_theorem(implies(implies(sK1,sK2),implies(sK2,implies(or(sK0,sK1),sK2)))) ),
inference(resolution,[],[f743263,f92]) ).
fof(f744447,plain,
~ is_a_theorem(implies(implies(sK1,sK2),or(sK0,implies(or(sK0,sK1),sK2)))),
inference(forward_subsumption_resolution,[],[f743312,f4732]) ).
fof(f744676,plain,
~ is_a_theorem(implies(implies(sK1,sK2),implies(or(sK0,sK1),or(sK0,sK2)))),
inference(forward_demodulation,[],[f744447,f48455]) ).
fof(f744770,plain,
$false,
inference(forward_subsumption_resolution,[],[f744676,f1125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL511+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n009.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 15:54:30 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.60/2.25 % (2210291)Detected formulas, will run a generic FOF schedule.
% 9.60/2.25 % (2210300)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=783159399:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.60/2.25 % (2210300)Refutation not found, incomplete strategy
% 9.60/2.25 % (2210300)------------------------------
% 9.60/2.25 % (2210300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.60/2.25 % (2210300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/2.25 % (2210300)CaDiCaL version: 2.1.3
% 9.60/2.25 % (2210300)Termination reason: Refutation not found, incomplete strategy
% 9.60/2.25 % (2210300)Time elapsed: 0.0000 s
% 9.60/2.25 % (2210300)Peak memory usage: 86 MB
% 9.60/2.25 % (2210301)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4023143337:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.60/2.25 % (2210302)dis-21_1_sil=8000:lcm=predicate:random_seed=2232457736:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.60/2.25 % (2210297)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3577359077:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.60/2.25 % (2210299)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4059549304:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.60/2.25 % (2210296)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=2810244866:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.60/2.25 % (2210298)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1147130766:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.60/2.25 % (2210299)Refutation not found, incomplete strategy
% 9.60/2.25 % (2210299)------------------------------
% 9.60/2.25 % (2210299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.60/2.25 % (2210299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/2.25 % (2210299)CaDiCaL version: 2.1.3
% 9.60/2.25 % (2210299)Termination reason: Refutation not found, incomplete strategy
% 9.60/2.25 % (2210299)Time elapsed: 0.001 s
% 9.60/2.25 % (2210299)Peak memory usage: 86 MB
% 9.60/2.25 % (2210302)Refutation not found, incomplete strategy
% 9.60/2.25 % (2210302)------------------------------
% 9.60/2.25 % (2210302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.60/2.25 % (2210302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/2.25 % (2210302)CaDiCaL version: 2.1.3
% 9.60/2.25 % (2210302)Termination reason: Refutation not found, incomplete strategy
% 9.60/2.25 % (2210302)Time elapsed: 0.002 s
% 9.60/2.25 % (2210302)Peak memory usage: 88 MB
% 9.60/2.25 % (2210302)Instructions burned: 1 (million)
% 9.60/2.25 % (2210301)Instruction limit reached!
% 9.60/2.25 % (2210301)------------------------------
% 9.60/2.25 % (2210301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.60/2.25 % (2210301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/2.25 % (2210301)CaDiCaL version: 2.1.3
% 9.60/2.25 % (2210301)Termination reason: Instruction limit
% 9.60/2.25 % (2210301)Termination phase: Saturation
% 9.60/2.25 % (2210301)Time elapsed: 0.092 s
% 9.60/2.25 % (2210301)Peak memory usage: 90 MB
% 9.60/2.25 % (2210301)Instructions burned: 140 (million)
% 9.60/2.25 % (2210300)------------------------------
% 9.60/2.25 % (2210300)------------------------------
% 9.60/2.25 % (2210311)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2695703604:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.60/2.25 % (2210311)Refutation not found, incomplete strategy
% 9.60/2.25 % (2210311)------------------------------
% 9.60/2.25 % (2210311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.60/2.25 % (2210311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/2.25 % (2210311)CaDiCaL version: 2.1.3
% 9.60/2.25 % (2210311)Termination reason: Refutation not found, incomplete strategy
% 9.60/2.25 % (2210311)Time elapsed: 0.0000 s
% 9.60/2.25 % (2210311)Peak memory usage: 87 MB
% 9.60/2.25 % (2210310)lrs+10_1_sil=8000:sp=occurrence:random_seed=3137449489:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.14/2.74 % (2210310)Refutation not found, incomplete strategy
% 12.14/2.74 % (2210310)------------------------------
% 12.14/2.74 % (2210310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.74 % (2210310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.74 % (2210310)CaDiCaL version: 2.1.3
% 12.14/2.74 % (2210310)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.74 % (2210310)Time elapsed: 0.001 s
% 12.14/2.74 % (2210310)Peak memory usage: 87 MB
% 12.14/2.74 % (2210302)------------------------------
% 12.14/2.74 % (2210302)------------------------------
% 12.14/2.74 % (2210299)------------------------------
% 12.14/2.74 % (2210299)------------------------------
% 12.14/2.74 % (2210311)------------------------------
% 12.14/2.74 % (2210311)------------------------------
% 12.14/2.74 % (2210314)lrs+1011_1_sil=32000:sp=occurrence:random_seed=996702104:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.14/2.74 % (2210315)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=113620700:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 12.14/2.74 % (2210314)Refutation not found, incomplete strategy
% 12.14/2.74 % (2210314)------------------------------
% 12.14/2.74 % (2210314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.74 % (2210314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.74 % (2210314)CaDiCaL version: 2.1.3
% 12.14/2.74 % (2210314)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.74 % (2210314)Time elapsed: 0.001 s
% 12.14/2.74 % (2210314)Peak memory usage: 86 MB
% 12.14/2.74 % (2210310)------------------------------
% 12.14/2.74 % (2210310)------------------------------
% 12.14/2.74 % (2210316)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3061632568:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.14/2.74 % (2210316)Refutation not found, incomplete strategy
% 12.14/2.74 % (2210316)------------------------------
% 12.14/2.74 % (2210316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.74 % (2210316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.74 % (2210316)CaDiCaL version: 2.1.3
% 12.14/2.74 % (2210316)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.74 % (2210316)Time elapsed: 0.0000 s
% 12.14/2.74 % (2210316)Peak memory usage: 86 MB
% 12.14/2.74 % (2210298)Refutation not found, incomplete strategy
% 12.14/2.74 % (2210298)------------------------------
% 12.14/2.74 % (2210298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.74 % (2210298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.74 % (2210298)CaDiCaL version: 2.1.3
% 12.14/2.74 % (2210298)Termination reason: Refutation not found, incomplete strategy
% 12.14/2.74 % (2210298)Time elapsed: 0.565 s
% 12.14/2.74 % (2210298)Peak memory usage: 125 MB
% 12.14/2.74 % (2210298)Instructions burned: 830 (million)
% 12.14/2.74 % (2210315)Instruction limit reached!
% 12.14/2.74 % (2210315)------------------------------
% 12.14/2.74 % (2210315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.74 % (2210315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.14/2.74 % (2210315)CaDiCaL version: 2.1.3
% 12.14/2.74 % (2210315)Termination reason: Instruction limit
% 12.14/2.74 % (2210315)Termination phase: Saturation
% 12.14/2.74 % (2210315)Time elapsed: 0.166 s
% 12.14/2.74 % (2210315)Peak memory usage: 92 MB
% 12.14/2.74 % (2210315)Instructions burned: 248 (million)
% 12.14/2.74 % (2210316)------------------------------
% 12.14/2.74 % (2210316)------------------------------
% 12.14/2.74 % (2210314)------------------------------
% 12.14/2.74 % (2210314)------------------------------
% 12.14/2.74 % (2210319)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1597799755:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 12.14/2.74 % (2210321)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3346929157:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 12.14/2.74 % (2210321)Refutation not found, incomplete strategy
% 12.14/2.74 % (2210321)------------------------------
% 12.14/2.74 % (2210321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.14/2.74 % (2210321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.12 % (2210321)CaDiCaL version: 2.1.3
% 15.78/3.12 % (2210321)Termination reason: Refutation not found, incomplete strategy
% 15.78/3.12 % (2210321)Time elapsed: 0.001 s
% 15.78/3.12 % (2210321)Peak memory usage: 88 MB
% 15.78/3.12 % (2210322)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2290230696:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 15.78/3.12 % (2210298)------------------------------
% 15.78/3.12 % (2210298)------------------------------
% 15.78/3.12 % (2210323)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4047919684:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 15.78/3.12 % (2210323)Refutation not found, incomplete strategy
% 15.78/3.12 % (2210323)------------------------------
% 15.78/3.12 % (2210323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.12 % (2210323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.12 % (2210323)CaDiCaL version: 2.1.3
% 15.78/3.12 % (2210323)Termination reason: Refutation not found, incomplete strategy
% 15.78/3.12 % (2210323)Time elapsed: 0.001 s
% 15.78/3.12 % (2210323)Peak memory usage: 87 MB
% 15.78/3.12 % (2210322)Instruction limit reached!
% 15.78/3.12 % (2210322)------------------------------
% 15.78/3.12 % (2210322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.12 % (2210322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.12 % (2210322)CaDiCaL version: 2.1.3
% 15.78/3.12 % (2210322)Termination reason: Instruction limit
% 15.78/3.12 % (2210322)Termination phase: Saturation
% 15.78/3.12 % (2210322)Time elapsed: 0.036 s
% 15.78/3.12 % (2210322)Peak memory usage: 88 MB
% 15.78/3.12 % (2210322)Instructions burned: 128 (million)
% 15.78/3.12 % (2210329)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=267728244:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 15.78/3.12 % (2210329)Refutation not found, incomplete strategy
% 15.78/3.12 % (2210329)------------------------------
% 15.78/3.12 % (2210329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.12 % (2210329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.12 % (2210329)CaDiCaL version: 2.1.3
% 15.78/3.12 % (2210329)Termination reason: Refutation not found, incomplete strategy
% 15.78/3.12 % (2210329)Time elapsed: 0.001 s
% 15.78/3.12 % (2210329)Peak memory usage: 88 MB
% 15.78/3.12 % (2210327)lrs+10_1_sil=8000:sp=occurrence:random_seed=2523366649:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 15.78/3.12 % (2210321)------------------------------
% 15.78/3.12 % (2210321)------------------------------
% 15.78/3.12 % (2210323)------------------------------
% 15.78/3.12 % (2210323)------------------------------
% 15.78/3.12 % (2210329)------------------------------
% 15.78/3.12 % (2210329)------------------------------
% 15.78/3.12 % (2210332)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=846871125:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 15.78/3.12 % (2210333)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2885672310:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 15.78/3.12 % (2210333)Refutation not found, incomplete strategy
% 15.78/3.12 % (2210333)------------------------------
% 15.78/3.13 % (2210333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.13 % (2210333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.13 % (2210333)CaDiCaL version: 2.1.3
% 15.78/3.13 % (2210333)Termination reason: Refutation not found, incomplete strategy
% 15.78/3.13 % (2210333)Time elapsed: 0.002 s
% 15.78/3.13 % (2210333)Peak memory usage: 89 MB
% 15.78/3.13 % (2210334)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=688175029:st=8:i=592:sd=3:ep=RST:ss=axioms_2987 on theBenchmark for (2987ds/592Mi)
% 15.78/3.13 % (2210334)Refutation not found, incomplete strategy
% 15.78/3.13 % (2210334)------------------------------
% 15.78/3.13 % (2210334)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.78/3.13 % (2210334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.78/3.13 % (2210334)CaDiCaL version: 2.1.3
% 15.78/3.13 % (2210334)Termination reason: Refutation not found, incomplete strategy
% 15.78/3.13 % (2210334)Time elapsed: 0.001 s
% 15.78/3.13 % (2210334)Peak memory usage: 88 MB
% 20.03/3.90 % (2210334)------------------------------
% 20.03/3.90 % (2210334)------------------------------
% 20.03/3.90 % (2210333)------------------------------
% 20.03/3.90 % (2210333)------------------------------
% 20.03/3.90 % (2210327)Instruction limit reached!
% 20.03/3.90 % (2210327)------------------------------
% 20.03/3.90 % (2210327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.90 % (2210327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/3.90 % (2210327)CaDiCaL version: 2.1.3
% 20.03/3.90 % (2210327)Termination reason: Instruction limit
% 20.03/3.90 % (2210327)Termination phase: Saturation
% 20.03/3.90 % (2210327)Time elapsed: 0.538 s
% 20.03/3.90 % (2210327)Peak memory usage: 100 MB
% 20.03/3.90 % (2210327)Instructions burned: 907 (million)
% 20.03/3.90 % (2210338)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3466930891:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 20.03/3.90 % (2210339)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=580491844:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 20.03/3.90 % (2210339)Refutation not found, incomplete strategy
% 20.03/3.90 % (2210339)------------------------------
% 20.03/3.90 % (2210339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.03/3.90 % (2210339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.03/3.90 % (2210339)CaDiCaL version: 2.1.3
% 20.03/3.90 % (2210339)Termination reason: Refutation not found, incomplete strategy
% 20.03/3.90 % (2210339)Time elapsed: 0.001 s
% 20.03/3.90 % (2210339)Peak memory usage: 87 MB
% 20.03/3.90 % (2210340)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1413675405:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 20.03/3.90 [W927 15:54:32.162635284 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162660600 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162682102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162689473 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162703283 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162709539 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162722839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.03/3.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.03/3.90 [W927 15:54:32.162729059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.24/5.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.24/5.42 [W927 15:54:32.162742179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.24/5.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.24/5.42 [W927 15:54:32.162749832 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.24/5.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.24/5.42 [W927 15:54:32.162762785 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.24/5.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.24/5.42 [W927 15:54:32.162768558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.24/5.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.24/5.42 % (2210340)Instruction limit reached!
% 32.24/5.42 % (2210340)------------------------------
% 32.24/5.42 % (2210340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.24/5.42 % (2210340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.24/5.42 % (2210340)CaDiCaL version: 2.1.3
% 32.24/5.42 % (2210340)Termination reason: Instruction limit
% 32.24/5.42 % (2210340)Termination phase: Saturation
% 32.24/5.42 % (2210340)Time elapsed: 0.099 s
% 32.24/5.42 % (2210340)Peak memory usage: 90 MB
% 32.24/5.42 % (2210340)Instructions burned: 134 (million)
% 32.24/5.42 % (2210338)Refutation not found, incomplete strategy
% 32.24/5.42 % (2210338)------------------------------
% 32.24/5.42 % (2210338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.24/5.42 % (2210338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.24/5.42 % (2210338)CaDiCaL version: 2.1.3
% 32.24/5.42 % (2210338)Termination reason: Refutation not found, incomplete strategy
% 32.24/5.42 % (2210338)Time elapsed: 0.302 s
% 32.24/5.42 % (2210338)Peak memory usage: 126 MB
% 32.24/5.42 % (2210338)Instructions burned: 821 (million)
% 32.24/5.42 % (2210339)------------------------------
% 32.24/5.42 % (2210339)------------------------------
% 32.24/5.42 % (2210344)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1993231073:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/141Mi)
% 32.24/5.42 % (2210344)Refutation not found, incomplete strategy
% 32.24/5.42 % (2210344)------------------------------
% 32.24/5.42 % (2210344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.24/5.42 % (2210344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.24/5.42 % (2210344)CaDiCaL version: 2.1.3
% 32.24/5.42 % (2210344)Termination reason: Refutation not found, incomplete strategy
% 32.24/5.42 % (2210344)Time elapsed: 0.001 s
% 32.24/5.42 % (2210344)Peak memory usage: 87 MB
% 32.24/5.42 % (2210338)------------------------------
% 32.24/5.42 % (2210338)------------------------------
% 32.24/5.42 % (2210345)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3531934887:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 32.24/5.42 % (2210345)Refutation not found, incomplete strategy
% 32.24/5.42 % (2210345)------------------------------
% 32.24/5.42 % (2210345)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.24/5.42 % (2210345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.24/5.42 % (2210345)CaDiCaL version: 2.1.3
% 32.24/5.42 % (2210345)Termination reason: Refutation not found, incomplete strategy
% 32.24/5.42 % (2210345)Time elapsed: 0.001 s
% 32.24/5.42 % (2210345)Peak memory usage: 86 MB
% 32.24/5.42 % (2210347)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=133620851:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 35.07/5.97 % (2210344)------------------------------
% 35.07/5.97 % (2210344)------------------------------
% 35.07/5.97 % (2210319)Instruction limit reached!
% 35.07/5.97 % (2210319)------------------------------
% 35.07/5.97 % (2210319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.97 % (2210319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.97 % (2210319)CaDiCaL version: 2.1.3
% 35.07/5.97 % (2210319)Termination reason: Instruction limit
% 35.07/5.97 % (2210319)Termination phase: Saturation
% 35.07/5.97 % (2210319)Time elapsed: 1.504 s
% 35.07/5.97 % (2210319)Peak memory usage: 141 MB
% 35.07/5.97 % (2210319)Instructions burned: 2352 (million)
% 35.07/5.97 % (2210345)------------------------------
% 35.07/5.97 % (2210345)------------------------------
% 35.07/5.97 % (2210350)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1283109630:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2976 on theBenchmark for (2976ds/150Mi)
% 35.07/5.97 % (2210351)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=834384444:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi)
% 35.07/5.97 % (2210352)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=853983254:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi)
% 35.07/5.97 % (2210352)Refutation not found, incomplete strategy
% 35.07/5.97 % (2210352)------------------------------
% 35.07/5.97 % (2210352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.97 % (2210352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.97 % (2210352)CaDiCaL version: 2.1.3
% 35.07/5.97 % (2210352)Termination reason: Refutation not found, incomplete strategy
% 35.07/5.97 % (2210352)Time elapsed: 0.001 s
% 35.07/5.97 % (2210352)Peak memory usage: 88 MB
% 35.07/5.97 % (2210350)Instruction limit reached!
% 35.07/5.97 % (2210350)------------------------------
% 35.07/5.97 % (2210350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.97 % (2210350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.97 % (2210350)CaDiCaL version: 2.1.3
% 35.07/5.97 % (2210350)Termination reason: Instruction limit
% 35.07/5.97 % (2210350)Termination phase: Saturation
% 35.07/5.97 % (2210350)Time elapsed: 0.090 s
% 35.07/5.97 % (2210350)Peak memory usage: 90 MB
% 35.07/5.97 % (2210350)Instructions burned: 150 (million)
% 35.07/5.97 % (2210356)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1794205816:s2a=on:i=185:s2at=1.8:fdi=4_2973 on theBenchmark for (2973ds/185Mi)
% 35.07/5.97 % (2210352)------------------------------
% 35.07/5.97 % (2210352)------------------------------
% 35.07/5.97 % (2210356)Instruction limit reached!
% 35.07/5.97 % (2210356)------------------------------
% 35.07/5.97 % (2210356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.97 % (2210356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.97 % (2210356)CaDiCaL version: 2.1.3
% 35.07/5.97 % (2210356)Termination reason: Instruction limit
% 35.07/5.97 % (2210356)Termination phase: Saturation
% 35.07/5.97 % (2210356)Time elapsed: 0.104 s
% 35.07/5.97 % (2210356)Peak memory usage: 90 MB
% 35.07/5.97 % (2210356)Instructions burned: 185 (million)
% 35.07/5.97 % (2210358)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3902089281:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2971 on theBenchmark for (2971ds/193Mi)
% 35.07/5.97 % (2210358)Refutation not found, incomplete strategy
% 35.07/5.97 % (2210358)------------------------------
% 35.07/5.97 % (2210358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.07/5.97 % (2210358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.07/5.97 % (2210358)CaDiCaL version: 2.1.3
% 35.07/5.97 % (2210358)Termination reason: Refutation not found, incomplete strategy
% 35.07/5.97 % (2210358)Time elapsed: 0.001 s
% 35.07/5.97 % (2210358)Peak memory usage: 86 MB
% 35.07/5.97 % (2210359)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2708442476:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2971 on theBenchmark for (2971ds/4850Mi)
% 35.07/5.97 % (2210359)Refutation not found, incomplete strategy
% 35.07/5.97 % (2210359)------------------------------
% 35.07/5.97 % (2210359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.70/7.55 % (2210359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/7.55 % (2210359)CaDiCaL version: 2.1.3
% 46.70/7.55 % (2210359)Termination reason: Refutation not found, incomplete strategy
% 46.70/7.55 % (2210359)Time elapsed: 0.001 s
% 46.70/7.55 % (2210359)Peak memory usage: 88 MB
% 46.70/7.55 % (2210358)------------------------------
% 46.70/7.55 % (2210358)------------------------------
% 46.70/7.55 % (2210359)------------------------------
% 46.70/7.55 % (2210359)------------------------------
% 46.70/7.55 % (2210362)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=744243287:i=12111:sd=1:ss=included_2967 on theBenchmark for (2967ds/12111Mi)
% 46.70/7.55 % (2210363)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1655452877:i=319:kws=precedence:fsr=off_2967 on theBenchmark for (2967ds/319Mi)
% 46.70/7.55 % (2210363)Instruction limit reached!
% 46.70/7.55 % (2210363)------------------------------
% 46.70/7.55 % (2210363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.70/7.55 % (2210363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/7.55 % (2210363)CaDiCaL version: 2.1.3
% 46.70/7.55 % (2210363)Termination reason: Instruction limit
% 46.70/7.55 % (2210363)Termination phase: Saturation
% 46.70/7.55 % (2210363)Time elapsed: 0.207 s
% 46.70/7.55 % (2210363)Peak memory usage: 93 MB
% 46.70/7.55 % (2210363)Instructions burned: 321 (million)
% 46.70/7.55 % (2210366)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3080095484:i=2064:ep=RST_2963 on theBenchmark for (2963ds/2064Mi)
% 46.70/7.55 % (2210366)Refutation not found, incomplete strategy
% 46.70/7.55 % (2210366)------------------------------
% 46.70/7.55 % (2210366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.70/7.55 % (2210366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/7.55 % (2210366)CaDiCaL version: 2.1.3
% 46.70/7.55 % (2210366)Termination reason: Refutation not found, incomplete strategy
% 46.70/7.55 % (2210366)Time elapsed: 0.001 s
% 46.70/7.55 % (2210366)Peak memory usage: 88 MB
% 46.70/7.55 % (2210366)Instructions burned: 1 (million)
% 46.70/7.55 % (2210366)------------------------------
% 46.70/7.55 % (2210366)------------------------------
% 46.70/7.55 % (2210368)dis-1011_128_sil=32000:random_seed=272626095:i=3706:ep=RST:av=off_2959 on theBenchmark for (2959ds/3706Mi)
% 46.70/7.55 % (2210347)Instruction limit reached!
% 46.70/7.55 % (2210347)------------------------------
% 46.70/7.55 % (2210347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.70/7.55 % (2210347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/7.55 % (2210347)CaDiCaL version: 2.1.3
% 46.70/7.55 % (2210347)Termination reason: Instruction limit
% 46.70/7.55 % (2210347)Termination phase: Saturation
% 46.70/7.55 % (2210347)Time elapsed: 2.051 s
% 46.70/7.55 % (2210347)Peak memory usage: 153 MB
% 46.70/7.55 % (2210347)Instructions burned: 6063 (million)
% 46.70/7.55 % (2210332)Instruction limit reached!
% 46.70/7.55 % (2210332)------------------------------
% 46.70/7.55 % (2210332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.70/7.55 % (2210332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/7.55 % (2210332)CaDiCaL version: 2.1.3
% 46.70/7.55 % (2210332)Termination reason: Instruction limit
% 46.70/7.55 % (2210332)Termination phase: Saturation
% 46.70/7.55 % (2210332)Time elapsed: 3.057 s
% 46.70/7.55 % (2210332)Peak memory usage: 173 MB
% 46.70/7.55 % (2210332)Instructions burned: 5203 (million)
% 46.70/7.55 % (2210370)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2387135621:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2956 on theBenchmark for (2956ds/757Mi)
% 46.70/7.55 % (2210370)Refutation not found, incomplete strategy
% 46.70/7.55 % (2210370)------------------------------
% 46.70/7.55 % (2210370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.70/7.55 % (2210370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.70/7.55 % (2210370)CaDiCaL version: 2.1.3
% 46.70/7.55 % (2210370)Termination reason: Refutation not found, incomplete strategy
% 46.70/7.55 % (2210370)Time elapsed: 0.0000 s
% 46.70/7.55 % (2210370)Peak memory usage: 87 MB
% 46.70/7.55 % (2210371)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=573525462:i=13913:ss=axioms:sgt=8_2955 on theBenchmark for (2955ds/13913Mi)
% 54.42/8.53 % (2210370)------------------------------
% 54.42/8.53 % (2210370)------------------------------
% 54.42/8.53 % (2210374)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3104684814:i=9925:aac=none_2953 on theBenchmark for (2953ds/9925Mi)
% 54.42/8.53 [W927 15:54:35.217728021 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217762005 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217800445 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217813255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217840369 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217851772 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217876882 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217888162 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217912979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217924083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217949763 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 [W927 15:54:35.217960966 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 54.42/8.53 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 54.42/8.53 % (2210371)Refutation not found, incomplete strategy
% 73.68/11.22 % (2210371)------------------------------
% 73.68/11.22 % (2210371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.22 % (2210371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.22 % (2210371)CaDiCaL version: 2.1.3
% 73.68/11.22 % (2210371)Termination reason: Refutation not found, incomplete strategy
% 73.68/11.22 % (2210371)Time elapsed: 0.549 s
% 73.68/11.22 % (2210371)Peak memory usage: 125 MB
% 73.68/11.22 % (2210371)Instructions burned: 827 (million)
% 73.68/11.22 % (2210371)------------------------------
% 73.68/11.22 % (2210371)------------------------------
% 73.68/11.22 % (2210376)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3617092152:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2946 on theBenchmark for (2946ds/2479Mi)
% 73.68/11.22 % (2210376)Refutation not found, incomplete strategy
% 73.68/11.22 % (2210376)------------------------------
% 73.68/11.22 % (2210376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.22 % (2210376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.22 % (2210376)CaDiCaL version: 2.1.3
% 73.68/11.22 % (2210376)Termination reason: Refutation not found, incomplete strategy
% 73.68/11.22 % (2210376)Time elapsed: 0.001 s
% 73.68/11.22 % (2210376)Peak memory usage: 87 MB
% 73.68/11.22 % (2210376)------------------------------
% 73.68/11.22 % (2210376)------------------------------
% 73.68/11.22 % (2210378)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=382715306:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2942 on theBenchmark for (2942ds/440Mi)
% 73.68/11.22 % (2210378)Instruction limit reached!
% 73.68/11.22 % (2210378)------------------------------
% 73.68/11.22 % (2210378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.22 % (2210378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.22 % (2210378)CaDiCaL version: 2.1.3
% 73.68/11.22 % (2210378)Termination reason: Instruction limit
% 73.68/11.22 % (2210378)Termination phase: Saturation
% 73.68/11.22 % (2210378)Time elapsed: 0.225 s
% 73.68/11.22 % (2210378)Peak memory usage: 95 MB
% 73.68/11.22 % (2210378)Instructions burned: 440 (million)
% 73.68/11.22 % (2210380)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=1205306858:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2938 on theBenchmark for (2938ds/11145Mi)
% 73.68/11.22 % (2210368)Instruction limit reached!
% 73.68/11.22 % (2210368)------------------------------
% 73.68/11.22 % (2210368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.22 % (2210368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.22 % (2210368)CaDiCaL version: 2.1.3
% 73.68/11.22 % (2210368)Termination reason: Instruction limit
% 73.68/11.22 % (2210368)Termination phase: Saturation
% 73.68/11.22 % (2210368)Time elapsed: 2.106 s
% 73.68/11.22 % (2210368)Peak memory usage: 143 MB
% 73.68/11.22 % (2210368)Instructions burned: 3708 (million)
% 73.68/11.22 % (2210382)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3076264607:cts=off:i=3034:av=off:er=known:fsd=on_2936 on theBenchmark for (2936ds/3034Mi)
% 73.68/11.22 [W927 15:54:37.973534229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.68/11.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.68/11.22 [W927 15:54:37.973568866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.68/11.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.68/11.22 [W927 15:54:37.973606527 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 73.68/11.22 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 73.68/11.22 [W927 15:54:37.973629203 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973655737 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973666534 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973690414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973701084 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973724744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973735541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973760328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 [W927 15:54:37.973771088 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 75.82/11.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 75.82/11.78 % (2210380)Refutation not found, incomplete strategy
% 75.82/11.78 % (2210380)------------------------------
% 75.82/11.78 % (2210380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.82/11.78 % (2210380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.82/11.78 % (2210380)CaDiCaL version: 2.1.3
% 75.82/11.78 % (2210380)Termination reason: Refutation not found, incomplete strategy
% 75.82/11.78 % (2210380)Time elapsed: 0.546 s
% 75.82/11.78 % (2210380)Peak memory usage: 126 MB
% 75.82/11.78 % (2210380)Instructions burned: 826 (million)
% 75.82/11.78 % (2210380)------------------------------
% 75.82/11.78 % (2210380)------------------------------
% 75.82/11.78 % (2210384)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=393559478:st=2:s2a=on:i=524:s2at=2:ss=axioms_2928 on theBenchmark for (2928ds/524Mi)
% 75.82/11.78 % (2210384)Refutation not found, incomplete strategy
% 75.82/11.78 % (2210384)------------------------------
% 75.82/11.78 % (2210384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.82/11.78 % (2210384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.82/11.78 % (2210384)CaDiCaL version: 2.1.3
% 75.82/11.78 % (2210384)Termination reason: Refutation not found, incomplete strategy
% 75.82/11.78 % (2210384)Time elapsed: 0.001 s
% 75.82/11.78 % (2210384)Peak memory usage: 87 MB
% 75.82/11.78 % (2210384)------------------------------
% 75.82/11.78 % (2210384)------------------------------
% 75.82/11.78 % (2210386)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=438195551:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2924 on theBenchmark for (2924ds/1016Mi)
% 79.83/12.21 % (2210386)Refutation not found, incomplete strategy
% 79.83/12.21 % (2210386)------------------------------
% 79.83/12.21 % (2210386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.83/12.21 % (2210386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.83/12.21 % (2210386)CaDiCaL version: 2.1.3
% 79.83/12.21 % (2210386)Termination reason: Refutation not found, incomplete strategy
% 79.83/12.21 % (2210386)Time elapsed: 0.001 s
% 79.83/12.21 % (2210386)Peak memory usage: 87 MB
% 79.83/12.21 % (2210386)------------------------------
% 79.83/12.21 % (2210386)------------------------------
% 79.83/12.21 % (2210388)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3283777265:i=14123:bd=preordered:ins=4_2920 on theBenchmark for (2920ds/14123Mi)
% 79.83/12.21 % (2210382)Instruction limit reached!
% 79.83/12.21 % (2210382)------------------------------
% 79.83/12.21 % (2210382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.83/12.21 % (2210382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.83/12.21 % (2210382)CaDiCaL version: 2.1.3
% 79.83/12.21 % (2210382)Termination reason: Instruction limit
% 79.83/12.21 % (2210382)Termination phase: Saturation
% 79.83/12.21 % (2210382)Time elapsed: 1.823 s
% 79.83/12.21 % (2210382)Peak memory usage: 145 MB
% 79.83/12.21 % (2210382)Instructions burned: 3035 (million)
% 79.83/12.21 % (2210390)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=3328192504:i=5781:kws=precedence:bd=all:rawr=on_2916 on theBenchmark for (2916ds/5781Mi)
% 79.83/12.21 % (2210374)Instruction limit reached!
% 79.83/12.21 % (2210374)------------------------------
% 79.83/12.21 % (2210374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.83/12.21 % (2210374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.83/12.21 % (2210374)CaDiCaL version: 2.1.3
% 79.83/12.21 % (2210374)Termination reason: Instruction limit
% 79.83/12.21 % (2210374)Termination phase: Saturation
% 79.83/12.21 % (2210374)Time elapsed: 3.948 s
% 79.83/12.21 % (2210374)Peak memory usage: 194 MB
% 79.83/12.21 % (2210374)Instructions burned: 9925 (million)
% 79.83/12.21 % (2210392)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=3739235811:i=2448:gtgl=5:bd=preordered:gtg=all_2913 on theBenchmark for (2913ds/2448Mi)
% 79.83/12.22 % (2210392)Instruction limit reached!
% 79.83/12.22 % (2210392)------------------------------
% 79.83/12.22 % (2210392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.83/12.22 % (2210392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.83/12.22 % (2210392)CaDiCaL version: 2.1.3
% 79.83/12.22 % (2210392)Termination reason: Instruction limit
% 79.83/12.22 % (2210392)Termination phase: Saturation
% 79.83/12.22 % (2210392)Time elapsed: 0.803 s
% 79.83/12.22 % (2210392)Peak memory usage: 145 MB
% 79.83/12.22 % (2210392)Instructions burned: 2448 (million)
% 79.83/12.22 % (2210396)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=2723674453:i=3223:kws=precedence:fgj=on:av=off_2903 on theBenchmark for (2903ds/3223Mi)
% 79.83/12.22 % (2210362)Instruction limit reached!
% 79.83/12.22 % (2210362)------------------------------
% 79.83/12.22 % (2210362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.83/12.22 % (2210362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.83/12.22 % (2210362)CaDiCaL version: 2.1.3
% 79.83/12.22 % (2210362)Termination reason: Instruction limit
% 79.83/12.22 % (2210362)Termination phase: Saturation
% 79.83/12.22 % (2210362)Time elapsed: 6.462 s
% 79.83/12.22 % (2210362)Peak memory usage: 262 MB
% 79.83/12.22 % (2210362)Instructions burned: 12112 (million)
% 79.83/12.22 % (2210398)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2936040012:st=5.6:i=2033:sd=3:ss=axioms_2901 on theBenchmark for (2901ds/2033Mi)
% 79.83/12.22 % (2210351)Instruction limit reached!
% 79.83/12.22 % (2210351)------------------------------
% 79.83/12.22 % (2210351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.83/12.22 % (2210351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.83/12.22 % (2210351)CaDiCaL version: 2.1.3
% 79.83/12.22 % (2210351)Termination reason: Instruction limit
% 79.83/12.22 % (2210351)Termination phase: Saturation
% 79.83/12.22 % (2210351)Time elapsed: 7.854 s
% 79.83/12.22 % (2210351)Peak memory usage: 257 MB
% 81.38/12.39 % (2210351)Instructions burned: 14155 (million)
% 81.38/12.39 % (2210400)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=358491005:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2896 on theBenchmark for (2896ds/2055Mi)
% 81.38/12.39 % (2210398)Refutation not found, incomplete strategy
% 81.38/12.39 % (2210398)------------------------------
% 81.38/12.39 % (2210398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.39 % (2210398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.39 % (2210398)CaDiCaL version: 2.1.3
% 81.38/12.39 % (2210398)Termination reason: Refutation not found, incomplete strategy
% 81.38/12.39 % (2210398)Time elapsed: 0.547 s
% 81.38/12.39 % (2210398)Peak memory usage: 126 MB
% 81.38/12.39 % (2210398)Instructions burned: 824 (million)
% 81.38/12.39 % (2210398)------------------------------
% 81.38/12.39 % (2210398)------------------------------
% 81.38/12.39 % (2210396)Instruction limit reached!
% 81.38/12.39 % (2210396)------------------------------
% 81.38/12.39 % (2210396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 81.38/12.39 % (2210396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.38/12.39 % (2210396)CaDiCaL version: 2.1.3
% 81.38/12.39 % (2210396)Termination reason: Instruction limit
% 81.38/12.39 % (2210396)Termination phase: Saturation
% 81.38/12.39 % (2210396)Time elapsed: 1.103 s
% 81.38/12.39 % (2210396)Peak memory usage: 144 MB
% 81.38/12.39 % (2210396)Instructions burned: 3224 (million)
% 81.38/12.39 [W927 15:54:41.203159128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203194865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203233976 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203247259 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203274919 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203286973 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203313760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203325593 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 81.38/12.39 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 81.38/12.39 [W927 15:54:41.203351590 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.70/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.70/13.29 [W927 15:54:41.203363490 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.70/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.70/13.29 [W927 15:54:41.203395500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.70/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.70/13.29 [W927 15:54:41.203405954 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.70/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.70/13.29 % (2210403)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3184696786:i=4835:sd=13:ss=axioms:sgt=23_2891 on theBenchmark for (2891ds/4835Mi)
% 87.70/13.29 % (2210403)Refutation not found, incomplete strategy
% 87.70/13.29 % (2210403)------------------------------
% 87.70/13.29 % (2210403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/13.29 % (2210403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/13.29 % (2210403)CaDiCaL version: 2.1.3
% 87.70/13.29 % (2210403)Termination reason: Refutation not found, incomplete strategy
% 87.70/13.29 % (2210403)Time elapsed: 0.001 s
% 87.70/13.29 % (2210403)Peak memory usage: 88 MB
% 87.70/13.29 % (2210403)Instructions burned: 1 (million)
% 87.70/13.29 % (2210402)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=3513353142:i=21611:sd=3:ss=axioms_2891 on theBenchmark for (2891ds/21611Mi)
% 87.70/13.29 % (2210400)Refutation not found, incomplete strategy
% 87.70/13.29 % (2210400)------------------------------
% 87.70/13.29 % (2210400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/13.29 % (2210400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/13.29 % (2210400)CaDiCaL version: 2.1.3
% 87.70/13.29 % (2210400)Termination reason: Refutation not found, incomplete strategy
% 87.70/13.29 % (2210400)Time elapsed: 0.550 s
% 87.70/13.29 % (2210400)Peak memory usage: 126 MB
% 87.70/13.29 % (2210400)Instructions burned: 826 (million)
% 87.70/13.29 % (2210403)------------------------------
% 87.70/13.29 % (2210403)------------------------------
% 87.70/13.29 % (2210406)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3955106937:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2888 on theBenchmark for (2888ds/797Mi)
% 87.70/13.29 % (2210406)Refutation not found, incomplete strategy
% 87.70/13.29 % (2210406)------------------------------
% 87.70/13.29 % (2210406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/13.29 % (2210406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/13.29 % (2210406)CaDiCaL version: 2.1.3
% 87.70/13.29 % (2210406)Termination reason: Refutation not found, incomplete strategy
% 87.70/13.29 % (2210406)Time elapsed: 0.001 s
% 87.70/13.29 % (2210406)Peak memory usage: 88 MB
% 87.70/13.29 % (2210406)Instructions burned: 1 (million)
% 87.70/13.29 % (2210400)------------------------------
% 87.70/13.29 % (2210400)------------------------------
% 87.70/13.29 [W927 15:54:41.638238388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.70/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.70/13.29 [W927 15:54:41.638273421 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.70/13.29 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.70/13.29 [W927 15:54:41.638310765 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638324385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638356235 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638366559 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638391152 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638401209 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638425362 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638435476 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638459289 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 [W927 15:54:41.638469489 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 96.38/14.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 96.38/14.42 % (2210406)------------------------------
% 96.38/14.42 % (2210406)------------------------------
% 96.38/14.42 % (2210408)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1666699978:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2886 on theBenchmark for (2886ds/2326Mi)
% 96.38/14.42 % (2210408)Refutation not found, incomplete strategy
% 96.38/14.42 % (2210408)------------------------------
% 96.38/14.42 % (2210408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.38/14.42 % (2210408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.38/14.42 % (2210408)CaDiCaL version: 2.1.3
% 96.38/14.42 % (2210408)Termination reason: Refutation not found, incomplete strategy
% 96.38/14.42 % (2210408)Time elapsed: 0.002 s
% 96.38/14.42 % (2210408)Peak memory usage: 88 MB
% 96.38/14.42 % (2210408)Instructions burned: 1 (million)
% 96.38/14.42 % (2210402)Refutation not found, incomplete strategy
% 96.38/14.42 % (2210402)------------------------------
% 96.38/14.42 % (2210402)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.38/14.42 % (2210402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/17.39 % (2210402)CaDiCaL version: 2.1.3
% 116.86/17.39 % (2210402)Termination reason: Refutation not found, incomplete strategy
% 116.86/17.39 % (2210402)Time elapsed: 0.557 s
% 116.86/17.39 % (2210402)Peak memory usage: 126 MB
% 116.86/17.39 % (2210402)Instructions burned: 825 (million)
% 116.86/17.39 % (2210409)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=2487345709:i=6038:nm=6_2885 on theBenchmark for (2885ds/6038Mi)
% 116.86/17.39 % (2210408)------------------------------
% 116.86/17.39 % (2210408)------------------------------
% 116.86/17.39 % (2210402)------------------------------
% 116.86/17.39 % (2210402)------------------------------
% 116.86/17.39 % (2210390)Instruction limit reached!
% 116.86/17.39 % (2210390)------------------------------
% 116.86/17.39 % (2210390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.86/17.39 % (2210390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/17.39 % (2210390)CaDiCaL version: 2.1.3
% 116.86/17.39 % (2210390)Termination reason: Instruction limit
% 116.86/17.39 % (2210390)Termination phase: Saturation
% 116.86/17.39 % (2210390)Time elapsed: 3.276 s
% 116.86/17.39 % (2210390)Peak memory usage: 146 MB
% 116.86/17.39 % (2210390)Instructions burned: 5782 (million)
% 116.86/17.39 % (2210409)Refutation not found, incomplete strategy
% 116.86/17.39 % (2210409)------------------------------
% 116.86/17.39 % (2210409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.86/17.39 % (2210409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/17.39 % (2210409)CaDiCaL version: 2.1.3
% 116.86/17.39 % (2210409)Termination reason: Refutation not found, incomplete strategy
% 116.86/17.39 % (2210409)Time elapsed: 0.326 s
% 116.86/17.39 % (2210409)Peak memory usage: 128 MB
% 116.86/17.39 % (2210409)Instructions burned: 891 (million)
% 116.86/17.39 % (2210412)lrs+10_1_sil=32000:sp=occurrence:random_seed=1645466570:st=2:i=33334:sd=3:ss=included:sgt=32_2882 on theBenchmark for (2882ds/33334Mi)
% 116.86/17.39 % (2210414)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=1329325422:i=8327:s2at=5:bd=preordered_2882 on theBenchmark for (2882ds/8327Mi)
% 116.86/17.39 % (2210413)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=4087798668:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2882 on theBenchmark for (2882ds/1008Mi)
% 116.86/17.39 % (2210413)Refutation not found, incomplete strategy
% 116.86/17.39 % (2210413)------------------------------
% 116.86/17.39 % (2210413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.86/17.39 % (2210413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/17.39 % (2210413)CaDiCaL version: 2.1.3
% 116.86/17.39 % (2210413)Termination reason: Refutation not found, incomplete strategy
% 116.86/17.39 % (2210413)Time elapsed: 0.001 s
% 116.86/17.39 % (2210413)Peak memory usage: 88 MB
% 116.86/17.39 % (2210409)------------------------------
% 116.86/17.39 % (2210409)------------------------------
% 116.86/17.39 % (2210418)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3155160710:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2879 on theBenchmark for (2879ds/1083Mi)
% 116.86/17.39 % (2210413)------------------------------
% 116.86/17.39 % (2210413)------------------------------
% 116.86/17.39 % (2210420)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=2534193487:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2878 on theBenchmark for (2878ds/1084Mi)
% 116.86/17.39 % (2210420)Refutation not found, incomplete strategy
% 116.86/17.39 % (2210420)------------------------------
% 116.86/17.39 % (2210420)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.86/17.39 % (2210420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/17.39 % (2210420)CaDiCaL version: 2.1.3
% 116.86/17.39 % (2210420)Termination reason: Refutation not found, incomplete strategy
% 116.86/17.39 % (2210420)Time elapsed: 0.001 s
% 116.86/17.39 % (2210420)Peak memory usage: 86 MB
% 116.86/17.39 % (2210418)Instruction limit reached!
% 116.86/17.39 % (2210418)------------------------------
% 116.86/17.39 % (2210418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.86/17.39 % (2210418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/17.77 % (2210418)CaDiCaL version: 2.1.3
% 119.15/17.77 % (2210418)Termination reason: Instruction limit
% 119.15/17.77 % (2210418)Termination phase: Saturation
% 119.15/17.77 % (2210418)Time elapsed: 0.282 s
% 119.15/17.77 % (2210418)Peak memory usage: 98 MB
% 119.15/17.77 % (2210418)Instructions burned: 1083 (million)
% 119.15/17.77 % (2210422)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=264349572:i=6995:s2at=5:gtg=all_2875 on theBenchmark for (2875ds/6995Mi)
% 119.15/17.77 % (2210420)------------------------------
% 119.15/17.77 % (2210420)------------------------------
% 119.15/17.77 % (2210424)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=3233346934:st=2:i=6225:sd=15:ss=axioms_2873 on theBenchmark for (2873ds/6225Mi)
% 119.15/17.77 % (2210424)Refutation not found, incomplete strategy
% 119.15/17.77 % (2210424)------------------------------
% 119.15/17.77 % (2210424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.15/17.77 % (2210424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.15/17.77 % (2210424)CaDiCaL version: 2.1.3
% 119.15/17.77 % (2210424)Termination reason: Refutation not found, incomplete strategy
% 119.15/17.77 % (2210424)Time elapsed: 0.001 s
% 119.15/17.77 % (2210424)Peak memory usage: 87 MB
% 119.15/17.77 % (2210424)------------------------------
% 119.15/17.77 % (2210424)------------------------------
% 119.15/17.77 % (2210426)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1752025411:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2869 on theBenchmark for (2869ds/3372Mi)
% 119.15/17.77 [W927 15:54:44.841355588 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841398502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841438738 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841449555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841478962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841489242 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841513866 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841524106 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 119.15/17.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 119.15/17.77 [W927 15:54:44.841547196 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.47/19.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.47/19.76 [W927 15:54:44.841559256 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.47/19.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.47/19.76 [W927 15:54:44.841593673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.47/19.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.47/19.76 [W927 15:54:44.841610320 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.47/19.76 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.47/19.76 % (2210426)Refutation not found, incomplete strategy
% 133.47/19.76 % (2210426)------------------------------
% 133.47/19.76 % (2210426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.47/19.76 % (2210426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.47/19.76 % (2210426)CaDiCaL version: 2.1.3
% 133.47/19.76 % (2210426)Termination reason: Refutation not found, incomplete strategy
% 133.47/19.76 % (2210426)Time elapsed: 0.569 s
% 133.47/19.76 % (2210426)Peak memory usage: 126 MB
% 133.47/19.76 % (2210426)Instructions burned: 827 (million)
% 133.47/19.76 % (2210426)------------------------------
% 133.47/19.76 % (2210426)------------------------------
% 133.47/19.76 % (2210428)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=2001348453:st=2.3:i=26457:sd=10:ss=included:sgt=8_2859 on theBenchmark for (2859ds/26457Mi)
% 133.47/19.76 % (2210428)Refutation not found, incomplete strategy
% 133.47/19.76 % (2210428)------------------------------
% 133.47/19.76 % (2210428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.47/19.76 % (2210428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.47/19.76 % (2210428)CaDiCaL version: 2.1.3
% 133.47/19.76 % (2210428)Termination reason: Refutation not found, incomplete strategy
% 133.47/19.76 % (2210428)Time elapsed: 0.618 s
% 133.47/19.76 % (2210428)Peak memory usage: 127 MB
% 133.47/19.76 % (2210428)Instructions burned: 886 (million)
% 133.47/19.76 % (2210422)Instruction limit reached!
% 133.47/19.76 % (2210422)------------------------------
% 133.47/19.76 % (2210422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.47/19.76 % (2210422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.47/19.76 % (2210422)CaDiCaL version: 2.1.3
% 133.47/19.76 % (2210422)Termination reason: Instruction limit
% 133.47/19.76 % (2210422)Termination phase: Saturation
% 133.47/19.76 % (2210422)Time elapsed: 2.372 s
% 133.47/19.76 % (2210422)Peak memory usage: 176 MB
% 133.47/19.76 % (2210422)Instructions burned: 6999 (million)
% 133.47/19.76 % (2210428)------------------------------
% 133.47/19.76 % (2210428)------------------------------
% 133.47/19.76 % (2210430)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=1682586293:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2850 on theBenchmark for (2850ds/13494Mi)
% 133.47/19.76 % (2210431)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=3242154098:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2849 on theBenchmark for (2849ds/2503Mi)
% 133.47/19.76 % (2210414)Instruction limit reached!
% 133.47/19.76 % (2210414)------------------------------
% 133.47/19.76 % (2210414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.47/19.76 % (2210414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.47/19.76 % (2210414)CaDiCaL version: 2.1.3
% 133.47/19.76 % (2210414)Termination reason: Instruction limit
% 133.47/19.76 % (2210414)Termination phase: Saturation
% 133.47/19.76 % (2210414)Time elapsed: 4.411 s
% 133.47/19.76 % (2210414)Peak memory usage: 173 MB
% 133.47/19.76 % (2210414)Instructions burned: 8329 (million)
% 133.47/19.76 % (2210434)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2888806596:i=2559:sd=1:ep=RSTC:ss=axioms_2836 on theBenchmark for (2836ds/2559Mi)
% 138.49/20.48 % (2210431)Instruction limit reached!
% 138.49/20.48 % (2210431)------------------------------
% 138.49/20.48 % (2210431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.49/20.48 % (2210431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.49/20.48 % (2210431)CaDiCaL version: 2.1.3
% 138.49/20.48 % (2210431)Termination reason: Instruction limit
% 138.49/20.48 % (2210431)Termination phase: Saturation
% 138.49/20.48 % (2210431)Time elapsed: 1.450 s
% 138.49/20.48 % (2210431)Peak memory usage: 145 MB
% 138.49/20.48 % (2210431)Instructions burned: 2503 (million)
% 138.49/20.48 % (2210436)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2377837776:i=30753:av=off:ss=included_2833 on theBenchmark for (2833ds/30753Mi)
% 138.49/20.48 [W927 15:54:47.190458823 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190492407 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190529910 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190542397 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190569200 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190580387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190606037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190617207 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190642278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190653524 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 138.49/20.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 138.49/20.48 [W927 15:54:47.190678211 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.51/20.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.51/20.61 [W927 15:54:47.190689338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.51/20.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.51/20.61 % (2210388)Instruction limit reached!
% 139.51/20.61 % (2210388)------------------------------
% 139.51/20.61 % (2210388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.61 % (2210388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.61 % (2210388)CaDiCaL version: 2.1.3
% 139.51/20.61 % (2210388)Termination reason: Instruction limit
% 139.51/20.61 % (2210388)Termination phase: Saturation
% 139.51/20.61 % (2210388)Time elapsed: 8.875 s
% 139.51/20.61 % (2210388)Peak memory usage: 254 MB
% 139.51/20.61 % (2210388)Instructions burned: 14124 (million)
% 139.51/20.61 % (2210434)Refutation not found, incomplete strategy
% 139.51/20.61 % (2210434)------------------------------
% 139.51/20.61 % (2210434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.61 % (2210434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.61 % (2210434)CaDiCaL version: 2.1.3
% 139.51/20.61 % (2210434)Termination reason: Refutation not found, incomplete strategy
% 139.51/20.61 % (2210434)Time elapsed: 0.548 s
% 139.51/20.61 % (2210434)Peak memory usage: 125 MB
% 139.51/20.61 % (2210434)Instructions burned: 826 (million)
% 139.51/20.61 % (2210438)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2815133878:i=26473:ep=RSTC_2830 on theBenchmark for (2830ds/26473Mi)
% 139.51/20.61 % (2210434)------------------------------
% 139.51/20.61 % (2210434)------------------------------
% 139.51/20.61 % (2210440)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=958751534:cts=off:i=2759:kws=inv_arity:fgj=on_2826 on theBenchmark for (2826ds/2759Mi)
% 139.51/20.61 % (2210440)Refutation not found, incomplete strategy
% 139.51/20.61 % (2210440)------------------------------
% 139.51/20.61 % (2210440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.51/20.61 % (2210440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.51/20.61 % (2210440)CaDiCaL version: 2.1.3
% 139.51/20.61 % (2210440)Termination reason: Refutation not found, incomplete strategy
% 139.51/20.61 % (2210440)Time elapsed: 0.591 s
% 139.51/20.61 % (2210440)Peak memory usage: 128 MB
% 139.51/20.61 % (2210440)Instructions burned: 892 (million)
% 139.51/20.61 % (2210440)------------------------------
% 139.51/20.61 % (2210440)------------------------------
% 139.51/20.61 % (2210442)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2636794955:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2816 on theBenchmark for (2816ds/5665Mi)
% 139.51/20.61 [W927 15:54:49.178969234 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.51/20.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.51/20.61 [W927 15:54:49.179013908 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.51/20.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.51/20.61 [W927 15:54:49.179052958 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.51/20.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 139.51/20.61 [W927 15:54:49.179065388 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 139.51/20.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.89 [W927 15:54:49.179090828 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.89 [W927 15:54:49.179101815 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.89 [W927 15:54:49.179140059 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.89 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.89 [W927 15:54:49.179150949 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.90 [W927 15:54:49.179176136 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.90 [W927 15:54:49.179186932 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.90 [W927 15:54:49.179211606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.90 [W927 15:54:49.179222513 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.12/20.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.12/20.90 % (2210442)Refutation not found, incomplete strategy
% 141.12/20.90 % (2210442)------------------------------
% 141.12/20.90 % (2210442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.12/20.90 % (2210442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.12/20.90 % (2210442)CaDiCaL version: 2.1.3
% 141.12/20.90 % (2210442)Termination reason: Refutation not found, incomplete strategy
% 141.12/20.90 % (2210442)Time elapsed: 0.551 s
% 141.12/20.90 % (2210442)Peak memory usage: 126 MB
% 141.12/20.90 % (2210442)Instructions burned: 826 (million)
% 141.12/20.90 % (2210430)Instruction limit reached!
% 141.12/20.90 % (2210430)------------------------------
% 141.12/20.90 % (2210430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.12/20.90 % (2210430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.12/20.90 % (2210430)CaDiCaL version: 2.1.3
% 141.12/20.90 % (2210430)Termination reason: Instruction limit
% 141.12/20.90 % (2210430)Termination phase: Saturation
% 141.12/20.90 % (2210430)Time elapsed: 4.218 s
% 141.12/20.90 % (2210430)Peak memory usage: 259 MB
% 141.12/20.90 % (2210430)Instructions burned: 13497 (million)
% 141.12/20.90 % (2210442)------------------------------
% 141.12/20.90 % (2210442)------------------------------
% 141.12/20.90 % (2210444)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=305336356:i=1532:ep=RS:ss=axioms_2806 on theBenchmark for (2806ds/1532Mi)
% 141.12/20.90 % (2210445)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=566776754:i=1565:sd=2:ss=axioms:sgt=32_2806 on theBenchmark for (2806ds/1565Mi)
% 141.12/20.90 [W927 15:54:50.906480978 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906517882 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906540744 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906559421 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906573006 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906578883 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906592386 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906611732 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906624806 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906630047 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906642682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 [W927 15:54:50.906647888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 157.58/23.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 157.58/23.11 % (2210444)Refutation not found, incomplete strategy
% 157.58/23.11 % (2210444)------------------------------
% 157.58/23.11 % (2210444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.58/23.11 % (2210444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.58/23.11 % (2210444)CaDiCaL version: 2.1.3
% 157.58/23.11 % (2210444)Termination reason: Refutation not found, incomplete strategy
% 158.77/23.21 % (2210444)Time elapsed: 0.330 s
% 158.77/23.21 % (2210444)Peak memory usage: 125 MB
% 158.77/23.21 % (2210444)Instructions burned: 822 (million)
% 158.77/23.21 [W927 15:54:50.152059732 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152096233 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152137850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152151003 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152177743 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152189377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152215187 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152227037 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152252771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152264474 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152289404 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 [W927 15:54:50.152300974 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 158.77/23.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 158.77/23.21 % (2210444)------------------------------
% 158.77/23.21 % (2210444)------------------------------
% 158.77/23.21 % (2210448)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=1330064065:i=1572:fgj=on:gsp=on_2800 on theBenchmark for (2800ds/1572Mi)
% 205.55/29.88 % (2210445)Refutation not found, incomplete strategy
% 205.55/29.88 % (2210445)------------------------------
% 205.55/29.88 % (2210445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 205.55/29.88 % (2210445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.55/29.88 % (2210445)CaDiCaL version: 2.1.3
% 205.55/29.88 % (2210445)Termination reason: Refutation not found, incomplete strategy
% 205.55/29.88 % (2210445)Time elapsed: 0.558 s
% 205.55/29.88 % (2210445)Peak memory usage: 125 MB
% 205.55/29.88 % (2210445)Instructions burned: 827 (million)
% 205.55/29.88 % (2210445)------------------------------
% 205.55/29.88 % (2210445)------------------------------
% 205.55/29.88 % (2210450)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1982955986:i=6052:sd=4:ss=axioms:sgt=24_2796 on theBenchmark for (2796ds/6052Mi)
% 205.55/29.88 % (2210448)Instruction limit reached!
% 205.55/29.88 % (2210448)------------------------------
% 205.55/29.88 % (2210448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 205.55/29.88 % (2210448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.55/29.88 % (2210448)CaDiCaL version: 2.1.3
% 205.55/29.88 % (2210448)Termination reason: Instruction limit
% 205.55/29.88 % (2210448)Termination phase: Saturation
% 205.55/29.88 % (2210448)Time elapsed: 0.553 s
% 205.55/29.88 % (2210448)Peak memory usage: 135 MB
% 205.55/29.88 % (2210448)Instructions burned: 1574 (million)
% 205.55/29.88 % (2210452)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=3273329435:i=3500:sd=1:bd=preordered:sup=off:ss=included_2794 on theBenchmark for (2794ds/3500Mi)
% 205.55/29.88 % (2210452)Refutation not found, incomplete strategy
% 205.55/29.88 % (2210452)------------------------------
% 205.55/29.88 % (2210452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 205.55/29.88 % (2210452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.55/29.88 % (2210452)CaDiCaL version: 2.1.3
% 205.55/29.88 % (2210452)Termination reason: Refutation not found, incomplete strategy
% 205.55/29.88 % (2210452)Time elapsed: 0.303 s
% 205.55/29.88 % (2210452)Peak memory usage: 127 MB
% 205.55/29.88 % (2210452)Instructions burned: 828 (million)
% 205.55/29.88 % (2210450)Refutation not found, incomplete strategy
% 205.55/29.88 % (2210450)------------------------------
% 205.55/29.88 % (2210450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 205.55/29.88 % (2210450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.55/29.88 % (2210450)CaDiCaL version: 2.1.3
% 205.55/29.88 % (2210450)Termination reason: Refutation not found, incomplete strategy
% 205.55/29.88 % (2210450)Time elapsed: 0.570 s
% 205.55/29.88 % (2210450)Peak memory usage: 127 MB
% 205.55/29.88 % (2210450)Instructions burned: 853 (million)
% 205.55/29.88 % (2210452)------------------------------
% 205.55/29.88 % (2210452)------------------------------
% 205.55/29.88 % (2210450)------------------------------
% 205.55/29.88 % (2210450)------------------------------
% 205.55/29.88 % (2210454)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=1620850325:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2788 on theBenchmark for (2788ds/1842Mi)
% 205.55/29.88 % (2210455)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2753019052:i=66096:add=on_2787 on theBenchmark for (2787ds/66096Mi)
% 205.55/29.88 % (2210454)Instruction limit reached!
% 205.55/29.88 % (2210454)------------------------------
% 205.55/29.88 % (2210454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 205.55/29.88 % (2210454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.55/29.88 % (2210454)CaDiCaL version: 2.1.3
% 205.55/29.88 % (2210454)Termination reason: Instruction limit
% 205.55/29.88 % (2210454)Termination phase: Saturation
% 205.55/29.88 % (2210454)Time elapsed: 0.608 s
% 205.55/29.88 % (2210454)Peak memory usage: 139 MB
% 205.55/29.88 % (2210454)Instructions burned: 1845 (million)
% 205.55/29.88 % (2210458)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3431169722:i=1884:sd=1:nm=60:ss=axioms_2780 on theBenchmark for (2780ds/1884Mi)
% 205.55/29.88 [W927 15:54:52.534837699 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534876097 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534897863 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534914291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534927893 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534933984 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534947042 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534952823 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534965260 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534971126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534984208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 [W927 15:54:52.534990015 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 128.42/30.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 128.42/30.94 % (2210458)Refutation not found, incomplete strategy
% 128.42/30.94 % (2210458)------------------------------
% 128.42/30.94 % (2210458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210458)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210458)Termination reason: Refutation not found, incomplete strategy
% 128.42/30.94 % (2210458)Time elapsed: 0.308 s
% 128.42/30.94 % (2210458)Peak memory usage: 125 MB
% 128.42/30.94 % (2210458)Instructions burned: 826 (million)
% 128.42/30.94 % (2210458)------------------------------
% 128.42/30.94 % (2210458)------------------------------
% 128.42/30.94 % (2210460)lrs-1011_4:1_sil=16000:bsr=on:random_seed=2176044069:cts=off:i=5469:bs=on:fsr=off_2774 on theBenchmark for (2774ds/5469Mi)
% 128.42/30.94 % (2210460)Instruction limit reached!
% 128.42/30.94 % (2210460)------------------------------
% 128.42/30.94 % (2210460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210460)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210460)Termination reason: Instruction limit
% 128.42/30.94 % (2210460)Termination phase: Saturation
% 128.42/30.94 % (2210460)Time elapsed: 1.742 s
% 128.42/30.94 % (2210460)Peak memory usage: 157 MB
% 128.42/30.94 % (2210460)Instructions burned: 5471 (million)
% 128.42/30.94 % (2210462)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=3212823586:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2755 on theBenchmark for (2755ds/2037Mi)
% 128.42/30.94 % (2210462)Instruction limit reached!
% 128.42/30.94 % (2210462)------------------------------
% 128.42/30.94 % (2210462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210462)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210462)Termination reason: Instruction limit
% 128.42/30.94 % (2210462)Termination phase: Saturation
% 128.42/30.94 % (2210462)Time elapsed: 0.690 s
% 128.42/30.94 % (2210462)Peak memory usage: 140 MB
% 128.42/30.94 % (2210462)Instructions burned: 2037 (million)
% 128.42/30.94 % (2210464)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2097452878:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2747 on theBenchmark for (2747ds/2110Mi)
% 128.42/30.94 % (2210464)Instruction limit reached!
% 128.42/30.94 % (2210464)------------------------------
% 128.42/30.94 % (2210464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210464)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210464)Termination reason: Instruction limit
% 128.42/30.94 % (2210464)Termination phase: Saturation
% 128.42/30.94 % (2210464)Time elapsed: 0.682 s
% 128.42/30.94 % (2210464)Peak memory usage: 140 MB
% 128.42/30.94 % (2210464)Instructions burned: 2111 (million)
% 128.42/30.94 % (2210466)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=157443803:i=2430:add=off:aac=none:nm=16_2739 on theBenchmark for (2739ds/2430Mi)
% 128.42/30.94 % (2210466)Instruction limit reached!
% 128.42/30.94 % (2210466)------------------------------
% 128.42/30.94 % (2210466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210466)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210466)Termination reason: Instruction limit
% 128.42/30.94 % (2210466)Termination phase: Saturation
% 128.42/30.94 % (2210466)Time elapsed: 0.806 s
% 128.42/30.94 % (2210466)Peak memory usage: 147 MB
% 128.42/30.94 % (2210466)Instructions burned: 2432 (million)
% 128.42/30.94 % (2210468)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=2565819110:cond=fast:i=4891_2730 on theBenchmark for (2730ds/4891Mi)
% 128.42/30.94 % (2210468)Instruction limit reached!
% 128.42/30.94 % (2210468)------------------------------
% 128.42/30.94 % (2210468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210468)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210468)Termination reason: Instruction limit
% 128.42/30.94 % (2210468)Termination phase: Saturation
% 128.42/30.94 % (2210468)Time elapsed: 1.798 s
% 128.42/30.94 % (2210468)Peak memory usage: 158 MB
% 128.42/30.94 % (2210468)Instructions burned: 4893 (million)
% 128.42/30.94 % (2210511)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=1956926580:st=2:i=14845:sd=2:ss=included:fsd=on_2710 on theBenchmark for (2710ds/14845Mi)
% 128.42/30.94 % (2210511)Refutation not found, incomplete strategy
% 128.42/30.94 % (2210511)------------------------------
% 128.42/30.94 % (2210511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 128.42/30.94 % (2210511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 128.42/30.94 % (2210511)CaDiCaL version: 2.1.3
% 128.42/30.94 % (2210511)Termination reason: Refutation not found, incomplete strategy
% 128.42/30.94 % (2210511)Time elapsed: 0.318 s
% 128.42/30.94 % (2210511)Peak memory usage: 127 MB
% 128.42/30.94 % (2210511)Instructions burned: 829 (million)
% 128.42/30.94 % (2210511)------------------------------
% 128.42/30.94 % (2210511)------------------------------
% 128.42/30.94 % (2210296)First to succeed.
% 128.42/30.94 % (2210296)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2210291"
% 128.42/30.94 % (2210624)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=2254739691:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2704 on theBenchmark for (2704ds/7534Mi)
% 128.42/30.94 % (2210296)Refutation found. Thanks to Tanya!
% 128.42/30.94 % SZS status Theorem for theBenchmark
% 128.42/30.94 % SZS output start Proof for theBenchmark
% See solution above
% 213.69/31.14 % (2210296)------------------------------
% 213.69/31.14 % (2210296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 213.69/31.14 % (2210296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 213.69/31.14 % (2210296)CaDiCaL version: 2.1.3
% 213.69/31.14 % (2210296)Termination reason: Refutation
% 213.69/31.14 % (2210296)Time elapsed: 29.548 s
% 213.69/31.14 % (2210296)Peak memory usage: 423 MB
% 213.69/31.14 % (2210296)Instructions burned: 46511 (million)
% 213.69/31.14 % (2210296)------------------------------
% 213.69/31.14 % (2210296)------------------------------
% 213.69/31.14 % (2210291)Success in time 30.088 s
% 213.69/31.14 % Vampire exiting
%------------------------------------------------------------------------------