%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL570+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 : n006.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:53:05 AM UTC 2026
% Result : Theorem 15.69s 2.93s
% Output : Refutation 16.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 30
% Syntax : Number of formulae : 258 ( 162 unt; 2 def)
% Number of atoms : 391 ( 96 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 240 ( 107 ~; 98 |; 4 &)
% ( 11 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 19 ( 17 usr; 17 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-2 aty)
% Number of variables : 452 ( 0 sgn 450 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( op_or
=> ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_or) ).
fof(f3,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(f7,axiom,
( modus_ponens_strict_implies
<=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(strict_implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modus_ponens_strict_implies) ).
fof(f8,axiom,
( adjunction
<=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(X1) )
=> is_a_theorem(and(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',adjunction) ).
fof(f9,axiom,
( substitution_strict_equiv
<=> ! [X0,X1] :
( is_a_theorem(strict_equiv(X0,X1))
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',substitution_strict_equiv) ).
fof(f10,axiom,
( axiom_K
<=> ! [X0,X1] : is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_K) ).
fof(f19,axiom,
( axiom_m1
<=> ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_m1) ).
fof(f20,axiom,
( axiom_m2
<=> ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_m2) ).
fof(f21,axiom,
( axiom_m3
<=> ! [X0,X1,X2] : is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_m3) ).
fof(f22,axiom,
( axiom_m4
<=> ! [X0] : is_a_theorem(strict_implies(X0,and(X0,X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_m4) ).
fof(f23,axiom,
( axiom_m5
<=> ! [X0,X1,X2] : is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_m5) ).
fof(f29,axiom,
( op_possibly
=> ! [X0] : possibly(X0) = not(necessarily(not(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_possibly) ).
fof(f31,axiom,
( op_strict_implies
=> ! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_strict_implies) ).
fof(f32,axiom,
( op_strict_equiv
=> ! [X0,X1] : strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',op_strict_equiv) ).
fof(f33,axiom,
op_possibly,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_op_possibly) ).
fof(f36,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_op_strict_implies) ).
fof(f38,axiom,
op_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_op_strict_equiv) ).
fof(f39,axiom,
modus_ponens_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_modus_ponens_strict_implies) ).
fof(f40,axiom,
substitution_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_substitution_strict_equiv) ).
fof(f41,axiom,
adjunction,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_adjunction) ).
fof(f42,axiom,
axiom_m1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_axiom_m1) ).
fof(f43,axiom,
axiom_m2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_axiom_m2) ).
fof(f44,axiom,
axiom_m3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_axiom_m3) ).
fof(f45,axiom,
axiom_m4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_axiom_m4) ).
fof(f46,axiom,
axiom_m5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s1_0_axiom_m5) ).
fof(f48,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_or) ).
fof(f49,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hilbert_op_implies_and) ).
fof(f52,conjecture,
axiom_K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',km5_axiom_K) ).
fof(f53,negated_conjecture,
~ axiom_K,
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f54,plain,
~ axiom_K,
inference(flattening,[],[f53]) ).
fof(f56,plain,
( axiom_m5
=> ! [X0,X1,X2] : is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))) ),
inference(unused_predicate_definition_removal,[],[f23]) ).
fof(f57,plain,
( axiom_m4
=> ! [X0] : is_a_theorem(strict_implies(X0,and(X0,X0))) ),
inference(unused_predicate_definition_removal,[],[f22]) ).
fof(f58,plain,
( axiom_m3
=> ! [X0,X1,X2] : is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))) ),
inference(unused_predicate_definition_removal,[],[f21]) ).
fof(f59,plain,
( axiom_m2
=> ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),X0)) ),
inference(unused_predicate_definition_removal,[],[f20]) ).
fof(f60,plain,
( axiom_m1
=> ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
inference(unused_predicate_definition_removal,[],[f19]) ).
fof(f61,plain,
( ! [X0,X1] : is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1))))
=> axiom_K ),
inference(unused_predicate_definition_removal,[],[f10]) ).
fof(f62,plain,
( substitution_strict_equiv
=> ! [X0,X1] :
( is_a_theorem(strict_equiv(X0,X1))
=> X0 = X1 ) ),
inference(unused_predicate_definition_removal,[],[f9]) ).
fof(f63,plain,
( adjunction
=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(X1) )
=> is_a_theorem(and(X0,X1)) ) ),
inference(unused_predicate_definition_removal,[],[f8]) ).
fof(f64,plain,
( modus_ponens_strict_implies
=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(strict_implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
inference(unused_predicate_definition_removal,[],[f7]) ).
fof(f70,plain,
( ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(ennf_transformation,[],[f1]) ).
fof(f71,plain,
( ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(ennf_transformation,[],[f3]) ).
fof(f73,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(strict_implies(X0,X1)) )
| ~ modus_ponens_strict_implies ),
inference(ennf_transformation,[],[f64]) ).
fof(f74,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(strict_implies(X0,X1)) )
| ~ modus_ponens_strict_implies ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
( ! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(X1) )
| ~ adjunction ),
inference(ennf_transformation,[],[f63]) ).
fof(f76,plain,
( ! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(X1) )
| ~ adjunction ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
( ! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1)) )
| ~ substitution_strict_equiv ),
inference(ennf_transformation,[],[f62]) ).
fof(f78,plain,
( axiom_K
| ? [X0,X1] : ~ is_a_theorem(implies(necessarily(implies(X0,X1)),implies(necessarily(X0),necessarily(X1)))) ),
inference(ennf_transformation,[],[f61]) ).
fof(f79,plain,
( ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| ~ axiom_m1 ),
inference(ennf_transformation,[],[f60]) ).
fof(f80,plain,
( ! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),X0))
| ~ axiom_m2 ),
inference(ennf_transformation,[],[f59]) ).
fof(f81,plain,
( ! [X0,X1,X2] : is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2))))
| ~ axiom_m3 ),
inference(ennf_transformation,[],[f58]) ).
fof(f82,plain,
( ! [X0] : is_a_theorem(strict_implies(X0,and(X0,X0)))
| ~ axiom_m4 ),
inference(ennf_transformation,[],[f57]) ).
fof(f83,plain,
( ! [X0,X1,X2] : is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2)))
| ~ axiom_m5 ),
inference(ennf_transformation,[],[f56]) ).
fof(f85,plain,
( ! [X0] : possibly(X0) = not(necessarily(not(X0)))
| ~ op_possibly ),
inference(ennf_transformation,[],[f29]) ).
fof(f86,plain,
( ! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(ennf_transformation,[],[f31]) ).
fof(f87,plain,
( ! [X0,X1] : strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0))
| ~ op_strict_equiv ),
inference(ennf_transformation,[],[f32]) ).
fof(f88,plain,
( axiom_K
| ~ is_a_theorem(implies(necessarily(implies(sK0,sK1)),implies(necessarily(sK0),necessarily(sK1)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f78]) ).
fof(f89,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[],[f70]) ).
fof(f90,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[],[f71]) ).
fof(f92,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ modus_ponens_strict_implies ),
inference(cnf_transformation,[],[f74]) ).
fof(f93,plain,
! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ adjunction ),
inference(cnf_transformation,[],[f76]) ).
fof(f94,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1))
| ~ substitution_strict_equiv ),
inference(cnf_transformation,[],[f77]) ).
fof(f95,plain,
( axiom_K
| ~ is_a_theorem(implies(necessarily(implies(sK0,sK1)),implies(necessarily(sK0),necessarily(sK1)))) ),
inference(cnf_transformation,[],[f88]) ).
fof(f96,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| ~ axiom_m1 ),
inference(cnf_transformation,[],[f79]) ).
fof(f97,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(and(X0,X1),X0))
| ~ axiom_m2 ),
inference(cnf_transformation,[],[f80]) ).
fof(f98,plain,
! [X2,X0,X1] :
( is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2))))
| ~ axiom_m3 ),
inference(cnf_transformation,[],[f81]) ).
fof(f99,plain,
! [X0] :
( is_a_theorem(strict_implies(X0,and(X0,X0)))
| ~ axiom_m4 ),
inference(cnf_transformation,[],[f82]) ).
fof(f100,plain,
! [X2,X0,X1] :
( is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2)))
| ~ axiom_m5 ),
inference(cnf_transformation,[],[f83]) ).
fof(f102,plain,
! [X0] :
( possibly(X0) = not(necessarily(not(X0)))
| ~ op_possibly ),
inference(cnf_transformation,[],[f85]) ).
fof(f103,plain,
! [X0,X1] :
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[],[f86]) ).
fof(f104,plain,
! [X0,X1] :
( strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0))
| ~ op_strict_equiv ),
inference(cnf_transformation,[],[f87]) ).
fof(f105,plain,
op_possibly,
inference(cnf_transformation,[],[f33]) ).
fof(f107,plain,
op_strict_implies,
inference(cnf_transformation,[],[f36]) ).
fof(f109,plain,
op_strict_equiv,
inference(cnf_transformation,[],[f38]) ).
fof(f110,plain,
modus_ponens_strict_implies,
inference(cnf_transformation,[],[f39]) ).
fof(f111,plain,
substitution_strict_equiv,
inference(cnf_transformation,[],[f40]) ).
fof(f112,plain,
adjunction,
inference(cnf_transformation,[],[f41]) ).
fof(f113,plain,
axiom_m1,
inference(cnf_transformation,[],[f42]) ).
fof(f114,plain,
axiom_m2,
inference(cnf_transformation,[],[f43]) ).
fof(f115,plain,
axiom_m3,
inference(cnf_transformation,[],[f44]) ).
fof(f116,plain,
axiom_m4,
inference(cnf_transformation,[],[f45]) ).
fof(f117,plain,
axiom_m5,
inference(cnf_transformation,[],[f46]) ).
fof(f119,plain,
op_or,
inference(cnf_transformation,[],[f48]) ).
fof(f120,plain,
op_implies_and,
inference(cnf_transformation,[],[f49]) ).
fof(f122,plain,
~ axiom_K,
inference(cnf_transformation,[],[f54]) ).
fof(f123,plain,
! [X0,X1] : strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)),
inference(forward_subsumption_resolution,[],[f104,f109]) ).
fof(f124,plain,
! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1)),
inference(forward_subsumption_resolution,[],[f103,f107]) ).
fof(f125,plain,
! [X0] : possibly(X0) = not(necessarily(not(X0))),
inference(forward_subsumption_resolution,[],[f102,f105]) ).
fof(f127,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))),
inference(forward_subsumption_resolution,[],[f100,f117]) ).
fof(f128,plain,
! [X0] : is_a_theorem(strict_implies(X0,and(X0,X0))),
inference(forward_subsumption_resolution,[],[f99,f116]) ).
fof(f129,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))),
inference(forward_subsumption_resolution,[],[f98,f115]) ).
fof(f130,plain,
! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),X0)),
inference(forward_subsumption_resolution,[],[f97,f114]) ).
fof(f131,plain,
! [X0,X1] : is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))),
inference(forward_subsumption_resolution,[],[f96,f113]) ).
fof(f132,plain,
~ is_a_theorem(implies(necessarily(implies(sK0,sK1)),implies(necessarily(sK0),necessarily(sK1)))),
inference(forward_subsumption_resolution,[],[f95,f122]) ).
fof(f133,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_equiv(X0,X1))
| X0 = X1 ),
inference(forward_subsumption_resolution,[],[f94,f111]) ).
fof(f134,plain,
! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(X1) ),
inference(forward_subsumption_resolution,[],[f93,f112]) ).
fof(f135,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
inference(forward_subsumption_resolution,[],[f92,f110]) ).
fof(f137,plain,
! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))),
inference(forward_subsumption_resolution,[],[f90,f120]) ).
fof(f138,plain,
! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))),
inference(forward_subsumption_resolution,[],[f89,f119]) ).
fof(f139,plain,
~ is_a_theorem(implies(strict_implies(sK0,sK1),implies(necessarily(sK0),necessarily(sK1)))),
inference(forward_demodulation,[],[f132,f124]) ).
fof(f140,plain,
! [X0,X1] : or(X0,X1) = implies(not(X0),X1),
inference(forward_demodulation,[],[f138,f137]) ).
fof(f142,plain,
! [X2,X0,X1] : or(and(X0,not(X1)),X2) = implies(implies(X0,X1),X2),
inference(superposition,[],[f140,f137]) ).
fof(f143,plain,
! [X0,X1] : strict_implies(not(X0),X1) = necessarily(or(X0,X1)),
inference(superposition,[],[f124,f140]) ).
fof(f147,plain,
! [X0,X1] : implies(X1,necessarily(not(X0))) = not(and(X1,possibly(X0))),
inference(superposition,[],[f137,f125]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(and(strict_implies(X0,X1),strict_implies(X1,X2)))
| is_a_theorem(strict_implies(X0,X2)) ),
inference(resolution,[],[f127,f135]) ).
fof(f166,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(X2,X1))
| ~ is_a_theorem(strict_implies(X0,X2))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[],[f165,f134]) ).
fof(f167,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(X0,and(X1,X1)))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[],[f166,f128]) ).
fof(f170,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(X0,and(X1,X2)))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[],[f166,f130]) ).
fof(f172,plain,
! [X0] : is_a_theorem(strict_implies(X0,X0)),
inference(resolution,[],[f170,f128]) ).
fof(f192,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(X1,X0))
| ~ is_a_theorem(strict_implies(X0,X1))
| is_a_theorem(strict_equiv(X0,X1)) ),
inference(superposition,[],[f134,f123]) ).
fof(f197,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,and(X0,X1)))
| is_a_theorem(strict_equiv(X0,and(X0,X1))) ),
inference(resolution,[],[f192,f130]) ).
fof(f201,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| is_a_theorem(strict_equiv(and(X0,X1),and(X1,X0))) ),
inference(resolution,[],[f192,f131]) ).
fof(f204,plain,
! [X0,X1] : is_a_theorem(strict_equiv(and(X0,X1),and(X1,X0))),
inference(forward_subsumption_resolution,[],[f201,f131]) ).
fof(f225,plain,
! [X0] : is_a_theorem(strict_equiv(X0,and(X0,X0))),
inference(resolution,[],[f197,f128]) ).
fof(f234,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(and(X1,X1)) ),
inference(resolution,[],[f167,f135]) ).
fof(f259,plain,
! [X0,X1] : or(X0,necessarily(not(X1))) = not(and(not(X0),possibly(X1))),
inference(superposition,[],[f140,f147]) ).
fof(f267,plain,
! [X0,X1] : and(X0,X1) = and(X1,X0),
inference(resolution,[],[f133,f204]) ).
fof(f268,plain,
! [X0] : and(X0,X0) = X0,
inference(resolution,[],[f133,f225]) ).
fof(f288,plain,
! [X0] : implies(not(X0),X0) = not(not(X0)),
inference(superposition,[],[f137,f268]) ).
fof(f297,plain,
! [X0] : not(not(X0)) = or(X0,X0),
inference(forward_demodulation,[],[f288,f140]) ).
fof(f338,plain,
! [X0,X1] : implies(X1,X0) = not(and(not(X0),X1)),
inference(superposition,[],[f137,f267]) ).
fof(f341,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(X0,and(X1,X2)),and(X1,and(X2,X0)))),
inference(superposition,[],[f129,f267]) ).
fof(f361,plain,
! [X0,X1] : implies(not(X0),X1) = implies(not(X1),X0),
inference(superposition,[],[f137,f338]) ).
fof(f372,plain,
! [X0,X1] : implies(not(X0),X1) = or(X1,X0),
inference(forward_demodulation,[],[f361,f140]) ).
fof(f379,plain,
! [X0,X1] : or(X0,X1) = or(X1,X0),
inference(forward_demodulation,[],[f372,f140]) ).
fof(f385,plain,
! [X0,X1] : necessarily(or(X0,X1)) = strict_implies(not(X1),X0),
inference(superposition,[],[f143,f379]) ).
fof(f386,plain,
! [X2,X0,X1] : or(X0,and(X1,not(X2))) = implies(implies(X1,X2),X0),
inference(superposition,[],[f142,f379]) ).
fof(f387,plain,
! [X0,X1] : strict_implies(not(X0),X1) = strict_implies(not(X1),X0),
inference(forward_demodulation,[],[f385,f143]) ).
fof(f392,plain,
! [X2,X0,X1] : strict_implies(implies(X0,X1),X2) = strict_implies(not(X2),and(X0,not(X1))),
inference(superposition,[],[f387,f137]) ).
fof(f393,plain,
! [X2,X0,X1] : strict_implies(implies(X0,X1),X2) = strict_implies(not(X2),and(not(X1),X0)),
inference(superposition,[],[f387,f338]) ).
fof(f416,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(not(X0),X1))
| ~ is_a_theorem(strict_implies(X2,not(X1)))
| is_a_theorem(strict_implies(X2,X0)) ),
inference(superposition,[],[f166,f387]) ).
fof(f417,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(not(X0),X1))
| ~ is_a_theorem(strict_implies(X0,not(X1)))
| is_a_theorem(strict_equiv(X0,not(X1))) ),
inference(superposition,[],[f192,f387]) ).
fof(f420,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(not(and(X0,X0)),X1))
| ~ is_a_theorem(strict_implies(not(X1),X0)) ),
inference(superposition,[],[f167,f387]) ).
fof(f421,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(not(X1),X0))
| is_a_theorem(strict_implies(not(X0),X1)) ),
inference(forward_demodulation,[],[f420,f268]) ).
fof(f425,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,not(not(X1))))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[],[f416,f172]) ).
fof(f437,plain,
! [X0] : is_a_theorem(strict_implies(not(not(X0)),X0)),
inference(resolution,[],[f421,f172]) ).
fof(f470,plain,
! [X0] : is_a_theorem(strict_implies(not(not(not(not(X0)))),X0)),
inference(resolution,[],[f425,f437]) ).
fof(f513,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(implies(X0,X1),X2))
| is_a_theorem(strict_implies(not(X2),X0)) ),
inference(superposition,[],[f170,f392]) ).
fof(f563,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(implies(X0,X1),X2))
| is_a_theorem(strict_implies(not(X2),not(X1))) ),
inference(superposition,[],[f170,f393]) ).
fof(f615,plain,
! [X0,X1] : is_a_theorem(strict_implies(not(implies(X0,X1)),not(X1))),
inference(resolution,[],[f563,f172]) ).
fof(f631,plain,
! [X0] : strict_implies(not(X0),X0) = necessarily(not(not(X0))),
inference(superposition,[],[f143,f297]) ).
fof(f697,plain,
! [X0,X1] : is_a_theorem(strict_implies(not(implies(X0,not(X1))),X1)),
inference(resolution,[],[f615,f425]) ).
fof(f708,plain,
! [X0,X1] : is_a_theorem(strict_implies(not(not(X0)),implies(X1,X0))),
inference(superposition,[],[f615,f387]) ).
fof(f809,plain,
! [X0] :
( ~ is_a_theorem(strict_implies(not(not(not(X0))),not(X0)))
| is_a_theorem(strict_equiv(not(not(not(X0))),not(X0))) ),
inference(resolution,[],[f470,f417]) ).
fof(f833,plain,
! [X0] : is_a_theorem(strict_equiv(not(not(not(X0))),not(X0))),
inference(forward_subsumption_resolution,[],[f809,f437]) ).
fof(f834,plain,
! [X0] : not(X0) = not(not(not(X0))),
inference(resolution,[],[f833,f133]) ).
fof(f841,plain,
! [X0,X1] : implies(X0,X1) = not(not(implies(X0,X1))),
inference(superposition,[],[f834,f338]) ).
fof(f859,plain,
! [X0,X1] : not(and(not(X0),X1)) = implies(X1,not(not(X0))),
inference(superposition,[],[f338,f834]) ).
fof(f861,plain,
! [X0,X1] : strict_implies(not(X0),X1) = strict_implies(not(X1),not(not(X0))),
inference(superposition,[],[f387,f834]) ).
fof(f865,plain,
! [X2,X0,X1] : strict_implies(implies(X1,X2),not(not(X0))) = strict_implies(not(X0),and(not(X2),X1)),
inference(superposition,[],[f393,f834]) ).
fof(f880,plain,
! [X2,X0,X1] : strict_implies(implies(X1,X2),X0) = strict_implies(implies(X1,X2),not(not(X0))),
inference(forward_demodulation,[],[f865,f393]) ).
fof(f884,plain,
! [X0,X1] : implies(X1,X0) = implies(X1,not(not(X0))),
inference(forward_demodulation,[],[f859,f338]) ).
fof(f898,plain,
! [X0,X1] : not(necessarily(implies(X0,X1))) = possibly(not(implies(X0,X1))),
inference(superposition,[],[f125,f841]) ).
fof(f928,plain,
! [X0,X1] : not(strict_implies(X0,X1)) = possibly(not(implies(X0,X1))),
inference(forward_demodulation,[],[f898,f124]) ).
fof(f932,plain,
! [X0,X1] : implies(X1,necessarily(not(X0))) = implies(X1,not(possibly(X0))),
inference(superposition,[],[f884,f125]) ).
fof(f935,plain,
! [X0,X1] : necessarily(implies(X0,X1)) = strict_implies(X0,not(not(X1))),
inference(superposition,[],[f124,f884]) ).
fof(f954,plain,
! [X0,X1] : strict_implies(X0,X1) = strict_implies(X0,not(not(X1))),
inference(forward_demodulation,[],[f935,f124]) ).
fof(f957,plain,
! [X0,X1] : not(and(X1,possibly(X0))) = implies(X1,not(possibly(X0))),
inference(forward_demodulation,[],[f932,f147]) ).
fof(f980,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(not(not(X1)),X0))
| ~ is_a_theorem(strict_implies(X0,X1))
| is_a_theorem(strict_equiv(not(not(X1)),X0)) ),
inference(superposition,[],[f192,f954]) ).
fof(f1159,plain,
! [X0] :
( ~ is_a_theorem(strict_implies(X0,X0))
| is_a_theorem(strict_equiv(not(not(X0)),X0)) ),
inference(resolution,[],[f980,f437]) ).
fof(f1187,plain,
! [X0] : is_a_theorem(strict_equiv(not(not(X0)),X0)),
inference(forward_subsumption_resolution,[],[f1159,f172]) ).
fof(f1192,plain,
! [X0] : not(not(X0)) = X0,
inference(resolution,[],[f1187,f133]) ).
fof(f1202,plain,
! [X0,X1] : and(not(X1),X0) = not(implies(X0,X1)),
inference(superposition,[],[f1192,f338]) ).
fof(f1203,plain,
! [X0] : not(possibly(X0)) = necessarily(not(X0)),
inference(superposition,[],[f1192,f125]) ).
fof(f1209,plain,
! [X0] : necessarily(X0) = strict_implies(not(X0),X0),
inference(superposition,[],[f631,f1192]) ).
fof(f1210,plain,
! [X0,X1] : is_a_theorem(strict_implies(X0,implies(X1,X0))),
inference(superposition,[],[f708,f1192]) ).
fof(f1224,plain,
! [X0,X1] : implies(X1,not(X0)) = not(and(X0,X1)),
inference(superposition,[],[f338,f1192]) ).
fof(f1239,plain,
! [X0] : necessarily(not(X0)) = strict_implies(X0,not(X0)),
inference(superposition,[],[f631,f1192]) ).
fof(f1245,plain,
! [X0,X1] : strict_implies(X0,X1) = strict_implies(not(X1),not(X0)),
inference(superposition,[],[f861,f1192]) ).
fof(f1374,plain,
! [X0,X1] : strict_implies(X1,not(X0)) = necessarily(not(and(X0,X1))),
inference(superposition,[],[f124,f1224]) ).
fof(f1386,plain,
! [X0,X1] : not(and(X0,not(X1))) = or(X1,not(X0)),
inference(superposition,[],[f140,f1224]) ).
fof(f1387,plain,
! [X0,X1] : implies(X0,X1) = or(X1,not(X0)),
inference(forward_demodulation,[],[f1386,f137]) ).
fof(f1396,plain,
! [X0,X1] : strict_implies(X1,not(X0)) = not(possibly(and(X0,X1))),
inference(forward_demodulation,[],[f1374,f1203]) ).
fof(f1405,plain,
! [X2,X0,X1] :
( is_a_theorem(strict_implies(X0,implies(X2,X1)))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[],[f1210,f166]) ).
fof(f1615,plain,
! [X2,X0,X1] : implies(and(not(X1),X0),X2) = or(X2,implies(X0,X1)),
inference(superposition,[],[f1387,f338]) ).
fof(f1680,plain,
! [X0,X1] : strict_implies(X0,not(X1)) = strict_implies(X1,not(X0)),
inference(superposition,[],[f1245,f1192]) ).
fof(f1768,plain,
! [X0,X1] : necessarily(implies(X0,X1)) = strict_implies(and(X0,not(X1)),implies(X0,X1)),
inference(superposition,[],[f1239,f137]) ).
fof(f1825,plain,
! [X0,X1] : strict_implies(X0,X1) = strict_implies(and(X0,not(X1)),implies(X0,X1)),
inference(forward_demodulation,[],[f1768,f124]) ).
fof(f1886,plain,
! [X2,X0,X1] : implies(X2,implies(X1,X0)) = not(and(X2,and(not(X0),X1))),
inference(superposition,[],[f137,f1202]) ).
fof(f2368,plain,
! [X2,X0,X1] : strict_implies(X2,implies(X0,X1)) = strict_implies(and(X0,not(X1)),not(X2)),
inference(superposition,[],[f1680,f137]) ).
fof(f3506,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(X2,and(X0,X1)),and(X1,and(X0,X2)))),
inference(superposition,[],[f341,f267]) ).
fof(f5598,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(and(X0,and(X1,X2)),and(X2,and(X1,X0))))
| is_a_theorem(strict_equiv(and(X0,and(X1,X2)),and(X2,and(X1,X0)))) ),
inference(resolution,[],[f3506,f192]) ).
fof(f5624,plain,
! [X2,X0,X1] : is_a_theorem(strict_equiv(and(X0,and(X1,X2)),and(X2,and(X1,X0)))),
inference(forward_subsumption_resolution,[],[f5598,f3506]) ).
fof(f5625,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X2,and(X1,X0)),
inference(resolution,[],[f5624,f133]) ).
fof(f5656,plain,
! [X0,X1] : and(X1,X0) = and(X0,and(X0,X1)),
inference(superposition,[],[f5625,f268]) ).
fof(f5658,plain,
! [X2,X0,X1] : and(X0,and(X1,X2)) = and(X2,and(X0,X1)),
inference(superposition,[],[f5625,f267]) ).
fof(f6176,plain,
! [X0,X1] : not(possibly(and(X0,X1))) = strict_implies(and(X1,X0),not(X1)),
inference(superposition,[],[f1396,f5656]) ).
fof(f6210,plain,
! [X0,X1] : strict_implies(X1,not(X0)) = strict_implies(and(X1,X0),not(X1)),
inference(forward_demodulation,[],[f6176,f1396]) ).
fof(f6267,plain,
! [X0,X1] : strict_implies(X1,not(X0)) = strict_implies(and(X0,X1),not(X1)),
inference(superposition,[],[f6210,f267]) ).
fof(f6398,plain,
! [X0,X1] : strict_implies(not(X0),not(X1)) = strict_implies(and(X1,not(X0)),X0),
inference(superposition,[],[f954,f6267]) ).
fof(f6424,plain,
! [X0,X1] : strict_implies(X1,X0) = strict_implies(and(X1,not(X0)),X0),
inference(forward_demodulation,[],[f6398,f1245]) ).
fof(f6467,plain,
! [X0,X1] : strict_implies(X1,not(not(X0))) = strict_implies(and(X1,not(X0)),not(not(X0))),
inference(superposition,[],[f6424,f834]) ).
fof(f6549,plain,
! [X0,X1] : strict_implies(X1,not(not(X0))) = strict_implies(not(X0),implies(X1,X0)),
inference(forward_demodulation,[],[f6467,f2368]) ).
fof(f6570,plain,
! [X0,X1] : strict_implies(X1,X0) = strict_implies(not(X0),implies(X1,X0)),
inference(forward_demodulation,[],[f6549,f954]) ).
fof(f6612,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(strict_implies(not(X1),X1)) ),
inference(superposition,[],[f1405,f6570]) ).
fof(f6630,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(necessarily(X1)) ),
inference(forward_demodulation,[],[f6612,f1209]) ).
fof(f6753,plain,
! [X0,X1] :
( ~ is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X1)
| is_a_theorem(and(X0,X0)) ),
inference(resolution,[],[f6630,f234]) ).
fof(f6828,definition,
( spl2_1
<=> ! [X1] : ~ is_a_theorem(X1) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f6829,plain,
( ! [X1] : ~ is_a_theorem(X1)
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f6828]) ).
fof(f6835,plain,
! [X0,X1] :
( is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X1) ),
inference(forward_demodulation,[],[f6753,f268]) ).
fof(f6837,definition,
( spl2_3
<=> ! [X0] :
( ~ is_a_theorem(necessarily(X0))
| is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition]) ).
fof(f6838,plain,
( ! [X0] :
( ~ is_a_theorem(necessarily(X0))
| is_a_theorem(X0) )
| ~ spl2_3 ),
inference(avatar_component_clause,[],[f6837]) ).
fof(f6847,plain,
( spl2_1
| spl2_3 ),
inference(avatar_split_clause,[],[f6835,f6837,f6828]) ).
fof(f6967,plain,
( ! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,X1))
| is_a_theorem(implies(X0,X1)) )
| ~ spl2_3 ),
inference(superposition,[],[f6838,f124]) ).
fof(f11718,plain,
! [X2,X0,X1] : not(and(X0,and(not(X1),X2))) = implies(and(X2,X0),X1),
inference(superposition,[],[f338,f5658]) ).
fof(f11910,plain,
! [X2,X0,X1] : implies(X0,implies(X2,X1)) = implies(and(X2,X0),X1),
inference(forward_demodulation,[],[f11718,f1886]) ).
fof(f12063,plain,
! [X2,X0,X1] : strict_implies(and(X1,X0),X2) = necessarily(implies(X0,implies(X1,X2))),
inference(superposition,[],[f124,f11910]) ).
fof(f12114,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(not(implies(X0,implies(X1,not(X2)))),X2)),
inference(superposition,[],[f697,f11910]) ).
fof(f12140,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(not(implies(X1,not(X2))),X0),X2)),
inference(forward_demodulation,[],[f12114,f1202]) ).
fof(f12156,plain,
! [X2,X0,X1] : strict_implies(X0,implies(X1,X2)) = strict_implies(and(X1,X0),X2),
inference(forward_demodulation,[],[f12063,f124]) ).
fof(f12182,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(and(not(not(X2)),X1),X0),X2)),
inference(forward_demodulation,[],[f12140,f1202]) ).
fof(f12205,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(X0,implies(and(not(not(X2)),X1),X2))),
inference(forward_demodulation,[],[f12182,f12156]) ).
fof(f12220,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(X0,or(X2,implies(X1,not(X2))))),
inference(forward_demodulation,[],[f12205,f1615]) ).
fof(f12223,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(X0,or(X2,not(and(X2,X1))))),
inference(forward_demodulation,[],[f12220,f1224]) ).
fof(f12224,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(X0,implies(and(X2,X1),X2))),
inference(forward_demodulation,[],[f12223,f1387]) ).
fof(f12225,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(X0,implies(X1,implies(X2,X2)))),
inference(forward_demodulation,[],[f12224,f11910]) ).
fof(f12425,plain,
! [X0,X1] : is_a_theorem(strict_implies(X0,implies(X1,X1))),
inference(superposition,[],[f12225,f1825]) ).
fof(f12502,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(implies(X0,X0),X1))
| is_a_theorem(strict_equiv(implies(X0,X0),X1)) ),
inference(resolution,[],[f12425,f192]) ).
fof(f12645,plain,
! [X0,X1] : is_a_theorem(strict_implies(X0,implies(X1,and(X0,X1)))),
inference(superposition,[],[f131,f12156]) ).
fof(f12870,plain,
! [X0,X1] : is_a_theorem(strict_implies(X1,or(X0,and(X1,not(X0))))),
inference(superposition,[],[f12645,f140]) ).
fof(f12881,plain,
! [X0,X1] : is_a_theorem(strict_implies(X1,implies(implies(X1,X0),X0))),
inference(forward_demodulation,[],[f12870,f386]) ).
fof(f12939,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f12881,f135]) ).
fof(f15062,plain,
! [X0,X1] : is_a_theorem(strict_equiv(implies(X0,X0),implies(X1,X1))),
inference(resolution,[],[f12502,f12425]) ).
fof(f15137,plain,
! [X0,X1] : implies(X0,X0) = implies(X1,X1),
inference(resolution,[],[f15062,f133]) ).
fof(f15346,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(strict_implies(implies(X0,X0),X2))
| is_a_theorem(strict_implies(not(X2),X1)) ),
inference(superposition,[],[f513,f15137]) ).
fof(f15358,plain,
! [X0,X1] : possibly(not(implies(X0,X0))) = not(strict_implies(X1,X1)),
inference(superposition,[],[f928,f15137]) ).
fof(f15459,plain,
! [X0,X1] : not(strict_implies(X0,X0)) = not(strict_implies(X1,X1)),
inference(forward_demodulation,[],[f15358,f928]) ).
fof(f19233,plain,
! [X2,X0,X1] : implies(strict_implies(X1,X1),X2) = or(X2,not(strict_implies(X0,X0))),
inference(superposition,[],[f1387,f15459]) ).
fof(f19276,plain,
! [X2,X0,X1] : implies(strict_implies(X1,X1),X2) = implies(strict_implies(X0,X0),X2),
inference(forward_demodulation,[],[f19233,f1387]) ).
fof(f21790,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(not(implies(implies(implies(X0,X0),X1),X1)),X2)),
inference(resolution,[],[f15346,f12881]) ).
fof(f21886,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(not(X1),implies(implies(X0,X0),X1)),X2)),
inference(forward_demodulation,[],[f21790,f1202]) ).
fof(f21936,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(implies(implies(X0,X0),X1),implies(not(X1),X2))),
inference(forward_demodulation,[],[f21886,f12156]) ).
fof(f21980,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(implies(implies(X0,X0),X1),or(X1,X2))),
inference(forward_demodulation,[],[f21936,f140]) ).
fof(f23364,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(strict_implies(X0,X0),X1),X1))
| ~ is_a_theorem(strict_implies(X2,X2)) ),
inference(superposition,[],[f12939,f19276]) ).
fof(f23428,plain,
! [X0,X1] : is_a_theorem(implies(implies(strict_implies(X0,X0),X1),X1)),
inference(forward_subsumption_resolution,[],[f23364,f172]) ).
fof(f23645,plain,
! [X0,X1] : is_a_theorem(not(and(implies(strict_implies(X0,X0),not(possibly(X1))),possibly(X1)))),
inference(superposition,[],[f23428,f957]) ).
fof(f23651,plain,
! [X0,X1] : is_a_theorem(not(and(not(and(strict_implies(X0,X0),possibly(X1))),possibly(X1)))),
inference(forward_demodulation,[],[f23645,f957]) ).
fof(f23668,plain,
! [X0,X1] : is_a_theorem(or(and(strict_implies(X0,X0),possibly(X1)),necessarily(not(X1)))),
inference(forward_demodulation,[],[f23651,f259]) ).
fof(f23676,plain,
! [X0,X1] : is_a_theorem(or(and(strict_implies(X0,X0),possibly(X1)),not(possibly(X1)))),
inference(forward_demodulation,[],[f23668,f1203]) ).
fof(f23679,plain,
! [X0,X1] : is_a_theorem(implies(possibly(X1),and(strict_implies(X0,X0),possibly(X1)))),
inference(forward_demodulation,[],[f23676,f1387]) ).
fof(f24209,plain,
! [X0,X1] : is_a_theorem(strict_implies(implies(implies(X1,X1),X0),not(not(X0)))),
inference(superposition,[],[f21980,f297]) ).
fof(f24223,plain,
! [X0,X1] : is_a_theorem(strict_implies(implies(implies(X1,X1),X0),X0)),
inference(forward_demodulation,[],[f24209,f880]) ).
fof(f24272,plain,
! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,implies(implies(X1,X1),X0)))
| is_a_theorem(strict_equiv(X0,implies(implies(X1,X1),X0))) ),
inference(resolution,[],[f24223,f192]) ).
fof(f24367,plain,
! [X0,X1] : is_a_theorem(strict_equiv(X0,implies(implies(X1,X1),X0))),
inference(forward_subsumption_resolution,[],[f24272,f1210]) ).
fof(f24389,plain,
! [X0,X1] : implies(implies(X1,X1),X0) = X0,
inference(resolution,[],[f24367,f133]) ).
fof(f24536,plain,
! [X0,X1] : necessarily(X0) = strict_implies(implies(X1,X1),X0),
inference(superposition,[],[f124,f24389]) ).
fof(f24811,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(and(strict_implies(implies(X1,X1),X2),strict_implies(X2,X0)),necessarily(X0))),
inference(superposition,[],[f127,f24536]) ).
fof(f24930,plain,
! [X2,X0,X1] : is_a_theorem(strict_implies(strict_implies(X2,X0),implies(strict_implies(implies(X1,X1),X2),necessarily(X0)))),
inference(forward_demodulation,[],[f24811,f12156]) ).
fof(f25028,plain,
! [X2,X0] : is_a_theorem(strict_implies(strict_implies(X2,X0),implies(necessarily(X2),necessarily(X0)))),
inference(forward_demodulation,[],[f24930,f24536]) ).
fof(f25087,plain,
( ! [X0,X1] : is_a_theorem(implies(strict_implies(X0,X1),implies(necessarily(X0),necessarily(X1))))
| ~ spl2_3 ),
inference(resolution,[],[f25028,f6967]) ).
fof(f25569,plain,
( $false
| ~ spl2_3 ),
inference(resolution,[],[f25087,f139]) ).
fof(f25671,plain,
~ spl2_3,
inference(avatar_contradiction_clause,[],[f25569]) ).
fof(f25841,plain,
( $false
| ~ spl2_1 ),
inference(forward_subsumption_resolution,[],[f23679,f6829]) ).
fof(f25842,plain,
~ spl2_1,
inference(avatar_contradiction_clause,[],[f25841]) ).
cnf(s4,plain,
( spl2_1
| spl2_3 ),
inference(sat_conversion,[],[f6847]) ).
cnf(s18,plain,
~ spl2_3,
inference(sat_conversion,[],[f25671]) ).
cnf(s34,plain,
~ spl2_1,
inference(sat_conversion,[],[f25842]) ).
cnf(s42,plain,
$false,
inference(rat,[],[s4,s18,s34]) ).
fof(f25845,plain,
$false,
inference(avatar_sat_refutation,[],[s42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL570+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.11/0.37 % Computer : n006.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 16:02:55 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/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
% 10.23/2.07 % (3136828)Detected formulas, will run a generic FOF schedule.
% 10.23/2.07 % (3136838)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4114864192:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.23/2.07 % (3136839)dis-21_1_sil=8000:lcm=predicate:random_seed=2697168659: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)
% 10.23/2.07 % (3136837)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1722025055:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.23/2.07 % (3136834)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=1487842452:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.23/2.07 % (3136836)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1817072578:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.23/2.07 % (3136833)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=3435463988:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.23/2.07 % (3136835)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=1690750616:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.23/2.07 % (3136837)Refutation not found, incomplete strategy
% 10.23/2.07 % (3136837)------------------------------
% 10.23/2.07 % (3136837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/2.07 % (3136837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/2.07 % (3136837)CaDiCaL version: 2.1.3
% 10.23/2.07 % (3136837)Termination reason: Refutation not found, incomplete strategy
% 10.23/2.07 % (3136837)Time elapsed: 0.001 s
% 10.23/2.07 % (3136837)Peak memory usage: 87 MB
% 10.23/2.07 % (3136836)Refutation not found, incomplete strategy
% 10.23/2.07 % (3136836)------------------------------
% 10.23/2.07 % (3136836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/2.07 % (3136836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/2.07 % (3136836)CaDiCaL version: 2.1.3
% 10.23/2.07 % (3136836)Termination reason: Refutation not found, incomplete strategy
% 10.23/2.07 % (3136836)Time elapsed: 0.001 s
% 10.23/2.07 % (3136836)Peak memory usage: 87 MB
% 10.23/2.07 % (3136839)Refutation not found, incomplete strategy
% 10.23/2.07 % (3136839)------------------------------
% 10.23/2.07 % (3136839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/2.07 % (3136839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/2.07 % (3136839)CaDiCaL version: 2.1.3
% 10.23/2.07 % (3136839)Termination reason: Refutation not found, incomplete strategy
% 10.23/2.07 % (3136839)Time elapsed: 0.001 s
% 10.23/2.07 % (3136839)Peak memory usage: 88 MB
% 10.23/2.07 % (3136839)Instructions burned: 1 (million)
% 10.23/2.07 % (3136838)Instruction limit reached!
% 10.23/2.07 % (3136838)------------------------------
% 10.23/2.07 % (3136838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/2.07 % (3136838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/2.07 % (3136838)CaDiCaL version: 2.1.3
% 10.23/2.07 % (3136838)Termination reason: Instruction limit
% 10.23/2.07 % (3136838)Termination phase: Saturation
% 10.23/2.07 % (3136838)Time elapsed: 0.048 s
% 10.23/2.07 % (3136838)Peak memory usage: 91 MB
% 10.23/2.07 % (3136838)Instructions burned: 141 (million)
% 10.23/2.07 % (3136847)lrs+10_1_sil=8000:sp=occurrence:random_seed=1729894878:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 10.23/2.07 % (3136847)Refutation not found, incomplete strategy
% 10.23/2.07 % (3136847)------------------------------
% 10.23/2.07 % (3136847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.23/2.07 % (3136847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.23/2.07 % (3136847)CaDiCaL version: 2.1.3
% 10.23/2.07 % (3136847)Termination reason: Refutation not found, incomplete strategy
% 10.23/2.07 % (3136847)Time elapsed: 0.0000 s
% 10.23/2.07 % (3136847)Peak memory usage: 87 MB
% 10.23/2.07 % (3136837)------------------------------
% 10.23/2.07 % (3136837)------------------------------
% 10.23/2.07 % (3136836)------------------------------
% 10.23/2.07 % (3136836)------------------------------
% 13.06/2.55 % (3136839)------------------------------
% 13.06/2.55 % (3136839)------------------------------
% 13.06/2.55 % (3136847)------------------------------
% 13.06/2.55 % (3136847)------------------------------
% 13.06/2.55 % (3136850)lrs+1011_1_sil=32000:sp=occurrence:random_seed=324936605:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 13.06/2.55 % (3136849)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2509512564:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 13.06/2.55 % (3136851)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=2973226653:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 13.06/2.55 % (3136850)Refutation not found, incomplete strategy
% 13.06/2.55 % (3136850)------------------------------
% 13.06/2.55 % (3136850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/2.55 % (3136850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/2.55 % (3136850)CaDiCaL version: 2.1.3
% 13.06/2.55 % (3136850)Termination reason: Refutation not found, incomplete strategy
% 13.06/2.55 % (3136850)Time elapsed: 0.001 s
% 13.06/2.55 % (3136850)Peak memory usage: 87 MB
% 13.06/2.55 % (3136849)Refutation not found, incomplete strategy
% 13.06/2.55 % (3136849)------------------------------
% 13.06/2.55 % (3136849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/2.55 % (3136849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/2.55 % (3136849)CaDiCaL version: 2.1.3
% 13.06/2.55 % (3136849)Termination reason: Refutation not found, incomplete strategy
% 13.06/2.55 % (3136849)Time elapsed: 0.001 s
% 13.06/2.55 % (3136849)Peak memory usage: 87 MB
% 13.06/2.55 % (3136852)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3457004311:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 13.06/2.55 % (3136852)Refutation not found, incomplete strategy
% 13.06/2.55 % (3136852)------------------------------
% 13.06/2.55 % (3136852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/2.55 % (3136852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/2.55 % (3136852)CaDiCaL version: 2.1.3
% 13.06/2.55 % (3136852)Termination reason: Refutation not found, incomplete strategy
% 13.06/2.55 % (3136852)Time elapsed: 0.0000 s
% 13.06/2.55 % (3136852)Peak memory usage: 87 MB
% 13.06/2.55 % (3136835)Refutation not found, incomplete strategy
% 13.06/2.55 % (3136835)------------------------------
% 13.06/2.55 % (3136835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/2.55 % (3136835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/2.55 % (3136835)CaDiCaL version: 2.1.3
% 13.06/2.55 % (3136835)Termination reason: Refutation not found, incomplete strategy
% 13.06/2.55 % (3136835)Time elapsed: 0.560 s
% 13.06/2.55 % (3136835)Peak memory usage: 125 MB
% 13.06/2.55 % (3136835)Instructions burned: 827 (million)
% 13.06/2.55 % (3136851)Instruction limit reached!
% 13.06/2.55 % (3136851)------------------------------
% 13.06/2.55 % (3136851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/2.55 % (3136851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.06/2.55 % (3136851)CaDiCaL version: 2.1.3
% 13.06/2.55 % (3136851)Termination reason: Instruction limit
% 13.06/2.55 % (3136851)Termination phase: Saturation
% 13.06/2.55 % (3136851)Time elapsed: 0.146 s
% 13.06/2.55 % (3136851)Peak memory usage: 92 MB
% 13.06/2.55 % (3136851)Instructions burned: 250 (million)
% 13.06/2.55 % (3136852)------------------------------
% 13.06/2.55 % (3136852)------------------------------
% 13.06/2.55 % (3136850)------------------------------
% 13.06/2.55 % (3136850)------------------------------
% 13.06/2.55 % (3136849)------------------------------
% 13.06/2.55 % (3136849)------------------------------
% 13.06/2.55 % (3136857)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=452468692:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 13.06/2.55 % (3136858)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3454407268:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 13.06/2.55 % (3136858)Refutation not found, incomplete strategy
% 13.06/2.55 % (3136858)------------------------------
% 13.06/2.55 % (3136858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.06/2.55 % (3136858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.92 % (3136858)CaDiCaL version: 2.1.3
% 15.69/2.92 % (3136858)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.92 % (3136858)Time elapsed: 0.001 s
% 15.69/2.92 % (3136858)Peak memory usage: 88 MB
% 15.69/2.92 % (3136835)------------------------------
% 15.69/2.92 % (3136835)------------------------------
% 15.69/2.92 % (3136860)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3080402780:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 15.69/2.92 % (3136859)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3943164526:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 15.69/2.92 % (3136860)Refutation not found, incomplete strategy
% 15.69/2.92 % (3136860)------------------------------
% 15.69/2.92 % (3136860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.92 % (3136860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.92 % (3136860)CaDiCaL version: 2.1.3
% 15.69/2.92 % (3136860)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.92 % (3136860)Time elapsed: 0.002 s
% 15.69/2.92 % (3136860)Peak memory usage: 88 MB
% 15.69/2.92 % (3136860)Instructions burned: 1 (million)
% 15.69/2.92 % (3136858)------------------------------
% 15.69/2.92 % (3136858)------------------------------
% 15.69/2.92 % (3136859)Instruction limit reached!
% 15.69/2.92 % (3136859)------------------------------
% 15.69/2.92 % (3136859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.92 % (3136859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.92 % (3136859)CaDiCaL version: 2.1.3
% 15.69/2.92 % (3136859)Termination reason: Instruction limit
% 15.69/2.92 % (3136859)Termination phase: Saturation
% 15.69/2.92 % (3136859)Time elapsed: 0.067 s
% 15.69/2.92 % (3136859)Peak memory usage: 88 MB
% 15.69/2.92 % (3136859)Instructions burned: 129 (million)
% 15.69/2.92 % (3136863)lrs+10_1_sil=8000:sp=occurrence:random_seed=746560657:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 15.69/2.92 % (3136866)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=787066677:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 15.69/2.92 % (3136866)Refutation not found, incomplete strategy
% 15.69/2.92 % (3136866)------------------------------
% 15.69/2.92 % (3136866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.92 % (3136866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.92 % (3136866)CaDiCaL version: 2.1.3
% 15.69/2.92 % (3136866)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.92 % (3136866)Time elapsed: 0.001 s
% 15.69/2.92 % (3136866)Peak memory usage: 88 MB
% 15.69/2.92 % (3136867)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=50925413:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 15.69/2.92 % (3136860)------------------------------
% 15.69/2.92 % (3136860)------------------------------
% 15.69/2.92 % (3136866)------------------------------
% 15.69/2.92 % (3136866)------------------------------
% 15.69/2.92 % (3136871)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2934147515:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 15.69/2.92 % (3136871)Refutation not found, incomplete strategy
% 15.69/2.92 % (3136871)------------------------------
% 15.69/2.92 % (3136871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.92 % (3136871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.92 % (3136871)CaDiCaL version: 2.1.3
% 15.69/2.92 % (3136871)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.92 % (3136871)Time elapsed: 0.001 s
% 15.69/2.92 % (3136871)Peak memory usage: 89 MB
% 15.69/2.92 % (3136872)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1835915113:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 15.69/2.92 % (3136872)Refutation not found, incomplete strategy
% 15.69/2.92 % (3136872)------------------------------
% 15.69/2.92 % (3136872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.92 % (3136872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.92 % (3136872)CaDiCaL version: 2.1.3
% 15.69/2.92 % (3136872)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.92 % (3136872)Time elapsed: 0.001 s
% 15.69/2.93 % (3136872)Peak memory usage: 88 MB
% 15.69/2.93 % (3136872)------------------------------
% 15.69/2.93 % (3136872)------------------------------
% 15.69/2.93 % (3136871)------------------------------
% 15.69/2.93 % (3136871)------------------------------
% 15.69/2.93 % (3136863)Instruction limit reached!
% 15.69/2.93 % (3136863)------------------------------
% 15.69/2.93 % (3136863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.93 % (3136863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.93 % (3136863)CaDiCaL version: 2.1.3
% 15.69/2.93 % (3136863)Termination reason: Instruction limit
% 15.69/2.93 % (3136863)Termination phase: Saturation
% 15.69/2.93 % (3136863)Time elapsed: 0.513 s
% 15.69/2.93 % (3136863)Peak memory usage: 101 MB
% 15.69/2.93 % (3136863)Instructions burned: 907 (million)
% 15.69/2.93 % (3136875)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1766159016:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 15.69/2.93 % (3136877)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3082921204:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 15.69/2.93 % (3136876)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=1075590242:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 15.69/2.93 % (3136876)Refutation not found, incomplete strategy
% 15.69/2.93 % (3136876)------------------------------
% 15.69/2.93 % (3136876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.93 % (3136876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.93 % (3136876)CaDiCaL version: 2.1.3
% 15.69/2.93 % (3136876)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.93 % (3136876)Time elapsed: 0.001 s
% 15.69/2.93 % (3136876)Peak memory usage: 87 MB
% 15.69/2.93 % (3136877)Instruction limit reached!
% 15.69/2.93 % (3136877)------------------------------
% 15.69/2.93 % (3136877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.93 % (3136877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.93 % (3136877)CaDiCaL version: 2.1.3
% 15.69/2.93 % (3136877)Termination reason: Instruction limit
% 15.69/2.93 % (3136877)Termination phase: Saturation
% 15.69/2.93 % (3136877)Time elapsed: 0.081 s
% 15.69/2.93 % (3136877)Peak memory usage: 90 MB
% 15.69/2.93 % (3136877)Instructions burned: 135 (million)
% 15.69/2.93 [W927 16:02:57.260152701 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260178487 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260199937 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260206302 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260219918 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260227104 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260241324 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260249527 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260262089 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260268384 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260281281 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 [W927 16:02:57.260287278 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.
% 15.69/2.93 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.69/2.93 % (3136833)First to succeed.
% 15.69/2.93 % (3136875)Refutation not found, incomplete strategy
% 15.69/2.93 % (3136875)------------------------------
% 15.69/2.93 % (3136875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.93 % (3136875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.93 % (3136875)CaDiCaL version: 2.1.3
% 15.69/2.93 % (3136875)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.93 % (3136875)Time elapsed: 0.311 s
% 15.69/2.93 % (3136875)Peak memory usage: 126 MB
% 15.69/2.93 % (3136875)Instructions burned: 827 (million)
% 15.69/2.93 % (3136876)------------------------------
% 15.69/2.93 % (3136876)------------------------------
% 15.69/2.93 % (3136833)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3136828"
% 15.69/2.93 % (3136881)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1527443676:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 15.69/2.93 % (3136881)Refutation not found, incomplete strategy
% 15.69/2.93 % (3136881)------------------------------
% 15.69/2.93 % (3136881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.93 % (3136881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.93 % (3136881)CaDiCaL version: 2.1.3
% 15.69/2.93 % (3136881)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.93 % (3136881)Time elapsed: 0.001 s
% 15.69/2.93 % (3136881)Peak memory usage: 87 MB
% 15.69/2.93 % (3136875)------------------------------
% 15.69/2.93 % (3136875)------------------------------
% 15.69/2.93 % (3136883)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1560369096:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 15.69/2.93 % (3136883)Refutation not found, incomplete strategy
% 15.69/2.93 % (3136883)------------------------------
% 15.69/2.93 % (3136883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.69/2.93 % (3136883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.69/2.93 % (3136883)CaDiCaL version: 2.1.3
% 15.69/2.93 % (3136883)Termination reason: Refutation not found, incomplete strategy
% 15.69/2.93 % (3136883)Time elapsed: 0.001 s
% 15.69/2.93 % (3136883)Peak memory usage: 87 MB
% 15.69/2.93 % (3136881)------------------------------
% 15.69/2.93 % (3136881)------------------------------
% 15.69/2.93 % (3136833)Refutation found. Thanks to Tanya!
% 15.69/2.93 % SZS status Theorem for theBenchmark
% 15.69/2.93 % SZS output start Proof for theBenchmark
% See solution above
% 16.73/3.13 % (3136833)------------------------------
% 16.73/3.13 % (3136833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.73/3.13 % (3136833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.73/3.13 % (3136833)CaDiCaL version: 2.1.3
% 16.73/3.13 % (3136833)Termination reason: Refutation
% 16.73/3.13 % (3136833)Time elapsed: 1.894 s
% 16.73/3.13 % (3136833)Peak memory usage: 146 MB
% 16.73/3.13 % (3136833)Instructions burned: 2915 (million)
% 16.73/3.13 % (3136833)------------------------------
% 16.73/3.13 % (3136833)------------------------------
% 16.73/3.13 % (3136828)Success in time 2.323 s
% 16.73/3.13 % Vampire exiting
%------------------------------------------------------------------------------