%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL063+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:51:05 AM UTC 2026
% Result : Theorem 50.97s 14.12s
% Output : Refutation 0.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 114
% Number of leaves : 18
% Syntax : Number of formulae : 242 ( 120 unt; 13 def)
% Number of atoms : 399 ( 22 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 315 ( 158 ~; 153 |; 1 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 16 con; 0-2 aty)
% Number of variables : 381 ( 0 sgn 381 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ( is_a_theorem(implies(X0,X1))
& is_a_theorem(X0) )
=> is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_1) ).
fof(f3,axiom,
! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_2) ).
fof(f4,axiom,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
fof(f5,conjecture,
is_a_theorem(implies(implies(implies(implies(implies(a,b),implies(not(c),not(e))),c),falsehood),implies(implies(falsehood,a),implies(e,a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_CAMeredith) ).
fof(f6,negated_conjecture,
~ is_a_theorem(implies(implies(implies(implies(implies(a,b),implies(not(c),not(e))),c),falsehood),implies(implies(falsehood,a),implies(e,a)))),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f7,plain,
~ is_a_theorem(implies(implies(implies(implies(implies(a,b),implies(not(c),not(e))),c),falsehood),implies(implies(falsehood,a),implies(e,a)))),
inference(flattening,[],[f6]) ).
fof(f8,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f9,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(cnf_transformation,[],[f9]) ).
fof(f11,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
inference(cnf_transformation,[],[f2]) ).
fof(f12,plain,
! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)),
inference(cnf_transformation,[],[f3]) ).
fof(f13,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
inference(cnf_transformation,[],[f4]) ).
fof(f14,plain,
~ is_a_theorem(implies(implies(implies(implies(implies(a,b),implies(not(c),not(e))),c),falsehood),implies(implies(falsehood,a),implies(e,a)))),
inference(cnf_transformation,[],[f7]) ).
fof(f15,definition,
sF0 = implies(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f16,plain,
implies(a,b) = sF0,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF1 = not(c),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f18,plain,
not(c) = sF1,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF2 = not(e),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f20,plain,
not(e) = sF2,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF3 = implies(sF1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f22,plain,
implies(sF1,sF2) = sF3,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF4 = implies(sF0,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f24,plain,
implies(sF0,sF3) = sF4,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF5 = implies(sF4,c),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f26,plain,
implies(sF4,c) = sF5,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF6 = implies(sF5,falsehood),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f28,plain,
implies(sF5,falsehood) = sF6,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF7 = implies(falsehood,a),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f30,plain,
implies(falsehood,a) = sF7,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF8 = implies(e,a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f32,plain,
implies(e,a) = sF8,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF9 = implies(sF7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f34,plain,
implies(sF7,sF8) = sF9,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF10 = implies(sF6,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f36,plain,
implies(sF6,sF9) = sF10,
inference(reorient_equations,[],[f35]) ).
fof(f37,plain,
~ is_a_theorem(sF10),
inference(definition_folding,[],[f14,f36,f34,f32,f30,f28,f26,f24,f22,f20,f18,f16]) ).
fof(f38,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(X2,X0)) ),
inference(resolution,[],[f11,f10]) ).
fof(f39,plain,
! [X0,X1] :
( is_a_theorem(implies(not(X0),X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f13,f10]) ).
fof(f44,plain,
! [X0] : is_a_theorem(implies(implies(e,X0),implies(implies(X0,a),sF8))),
inference(superposition,[],[f11,f32]) ).
fof(f147,plain,
! [X0] :
( ~ is_a_theorem(implies(not(X0),X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f12,f10]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f38,f10]) ).
fof(f169,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,X2))))
| ~ is_a_theorem(implies(X0,implies(X3,X1))) ),
inference(resolution,[],[f150,f11]) ).
fof(f170,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X3,X2)))
| is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f150,f38]) ).
fof(f171,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(not(X1),X2)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f150,f13]) ).
fof(f172,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f150,f12]) ).
fof(f203,plain,
! [X0] : is_a_theorem(implies(X0,X0)),
inference(resolution,[],[f172,f13]) ).
fof(f210,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X3))))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(resolution,[],[f170,f11]) ).
fof(f211,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,X0))
| ~ is_a_theorem(implies(X2,X3))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) ),
inference(resolution,[],[f170,f38]) ).
fof(f212,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X1,not(X0))) ),
inference(resolution,[],[f170,f13]) ).
fof(f224,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),not(X1)))
| is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f212,f172]) ).
fof(f244,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(X3,implies(X4,X1)))
| is_a_theorem(implies(X3,implies(X0,implies(X4,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f210,f150]) ).
fof(f269,plain,
! [X0,X1] :
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f39,f224]) ).
fof(f289,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),X0))
| is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f269,f172]) ).
fof(f290,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,X0))
| is_a_theorem(implies(X2,implies(X3,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f269,f170]) ).
fof(f312,plain,
is_a_theorem(implies(implies(e,falsehood),implies(sF7,sF8))),
inference(superposition,[],[f44,f30]) ).
fof(f321,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),X1)))
| is_a_theorem(implies(implies(X1,X2),implies(X0,X2))) ),
inference(resolution,[],[f211,f12]) ).
fof(f390,plain,
! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,implies(implies(X1,X3),X4))))
| ~ is_a_theorem(implies(X2,implies(implies(X0,X3),X4))) ),
inference(resolution,[],[f244,f11]) ).
fof(f397,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X3,X2)))
| is_a_theorem(implies(X0,implies(X1,implies(not(X0),X2)))) ),
inference(resolution,[],[f244,f13]) ).
fof(f427,plain,
is_a_theorem(implies(implies(e,falsehood),sF9)),
inference(forward_demodulation,[],[f312,f34]) ).
fof(f528,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(not(X0),X2)))),
inference(resolution,[],[f397,f13]) ).
fof(f561,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X3)))
| is_a_theorem(implies(X0,implies(implies(X4,X2),X3)))
| ~ is_a_theorem(implies(X1,X4)) ),
inference(resolution,[],[f390,f10]) ).
fof(f580,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X3),implies(X0,X3))))
| ~ is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f561,f11]) ).
fof(f656,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(not(X0),X1),X2),implies(X0,X2))),
inference(resolution,[],[f321,f528]) ).
fof(f658,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(not(X0),X0),X1))),
inference(resolution,[],[f321,f203]) ).
fof(f670,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),X0),X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f658,f10]) ).
fof(f692,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(not(X0),X2),X1))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f656,f10]) ).
fof(f726,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),X0))
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f670,f10]) ).
fof(f760,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(not(X1),X3),X2))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f290,f13]) ).
fof(f775,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))),
inference(resolution,[],[f760,f12]) ).
fof(f801,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X1,X1),X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f775,f726]) ).
fof(f804,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X2)))),
inference(resolution,[],[f775,f760]) ).
fof(f810,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),
inference(resolution,[],[f804,f321]) ).
fof(f841,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),X1)),
inference(resolution,[],[f810,f172]) ).
fof(f858,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X2),X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f841,f150]) ).
fof(f868,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f858,f580]) ).
fof(f869,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X2),X0))
| is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[],[f858,f38]) ).
fof(f903,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(not(X1),X0),X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f868,f172]) ).
fof(f930,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f869,f269]) ).
fof(f961,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(not(X1),X0)))
| is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f903,f150]) ).
fof(f973,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(not(X2),X0)) ),
inference(resolution,[],[f961,f38]) ).
fof(f990,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X1),X2))
| ~ is_a_theorem(implies(X2,X1))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f961,f269]) ).
fof(f1054,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f930,f150]) ).
fof(f1180,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,X2))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f1054,f580]) ).
fof(f1221,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(not(X2),X2)))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f1180,f12]) ).
fof(f1277,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(not(X1),X1)),implies(X0,X1))),
inference(resolution,[],[f1221,f203]) ).
fof(f1307,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(not(X2),X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f1277,f150]) ).
fof(f1437,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X1),implies(implies(X1,X0),X0))),
inference(resolution,[],[f1307,f11]) ).
fof(f1451,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(resolution,[],[f1307,f528]) ).
fof(f1474,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X0),implies(X1,X0))),
inference(resolution,[],[f1451,f1307]) ).
fof(f1484,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X1),X2))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f1451,f290]) ).
fof(f1486,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f1451,f150]) ).
fof(f1601,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[],[f1474,f760]) ).
fof(f2148,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(implies(X1,X2),X2)))),
inference(resolution,[],[f1484,f1437]) ).
fof(f2172,plain,
! [X0] : is_a_theorem(implies(X0,implies(falsehood,sF9))),
inference(resolution,[],[f1484,f427]) ).
fof(f2204,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(resolution,[],[f2148,f801]) ).
fof(f2223,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f2204,f170]) ).
fof(f2251,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),X0),implies(implies(X0,X1),X1))),
inference(resolution,[],[f2223,f658]) ).
fof(f2266,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(not(X1),X0),X1))),
inference(resolution,[],[f2223,f1437]) ).
fof(f2282,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X0)))),
inference(resolution,[],[f2223,f1601]) ).
fof(f2288,plain,
! [X0,X1] : is_a_theorem(implies(not(X0),implies(X0,X1))),
inference(resolution,[],[f2223,f13]) ).
fof(f2289,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(not(X0),implies(X1,X2)))
| ~ is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f2223,f171]) ).
fof(f2323,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(not(X0)),X1))),
inference(resolution,[],[f2288,f321]) ).
fof(f2347,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(not(X1),not(X0)),X1))),
inference(resolution,[],[f2266,f692]) ).
fof(f2648,definition,
( spl11_61
<=> ! [X0] : is_a_theorem(implies(X0,sF10)) ),
introduced(definition,[new_symbols(definition,[spl11_61])],[avatar_definition]) ).
fof(f2649,plain,
( ! [X0] : is_a_theorem(implies(X0,sF10))
| ~ spl11_61 ),
inference(avatar_component_clause,[],[f2648]) ).
fof(f2752,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X2,X1)))),
inference(resolution,[],[f2282,f1221]) ).
fof(f2755,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X0),X1))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f2282,f961]) ).
fof(f2817,plain,
! [X0] : is_a_theorem(implies(implies(X0,a),implies(X0,sF8))),
inference(superposition,[],[f2752,f32]) ).
fof(f2821,plain,
! [X0] : is_a_theorem(implies(implies(X0,c),implies(X0,sF5))),
inference(superposition,[],[f2752,f26]) ).
fof(f2823,plain,
! [X0] : is_a_theorem(implies(implies(X0,sF9),implies(X0,sF10))),
inference(superposition,[],[f2752,f36]) ).
fof(f2824,plain,
! [X0] : is_a_theorem(implies(implies(X0,sF8),implies(X0,sF9))),
inference(superposition,[],[f2752,f34]) ).
fof(f2996,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f2289,f147]) ).
fof(f2997,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X2),X1))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X3,X1)) ),
inference(resolution,[],[f2289,f990]) ).
fof(f3010,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),X1))
| is_a_theorem(implies(not(X1),X0)) ),
inference(resolution,[],[f2289,f172]) ).
fof(f3053,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) ),
inference(resolution,[],[f2996,f169]) ).
fof(f3077,plain,
! [X0,X1] : is_a_theorem(implies(not(implies(X0,X1)),X0)),
inference(resolution,[],[f3010,f2288]) ).
fof(f3124,plain,
is_a_theorem(implies(not(sF0),a)),
inference(superposition,[],[f3077,f16]) ).
fof(f3131,plain,
is_a_theorem(implies(not(sF10),sF6)),
inference(superposition,[],[f3077,f36]) ).
fof(f4730,plain,
! [X0,X1] : is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0))),
inference(resolution,[],[f2347,f2223]) ).
fof(f4843,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(X1),implies(X1,X2)))),
inference(resolution,[],[f4730,f1484]) ).
fof(f4908,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2))),
inference(resolution,[],[f4843,f3053]) ).
fof(f4943,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(implies(X1,X2),X1)),implies(X0,X1))),
inference(resolution,[],[f4908,f1221]) ).
fof(f4945,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),X0)),
inference(resolution,[],[f4908,f172]) ).
fof(f4954,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X2),X1))
| is_a_theorem(implies(not(X0),X1)) ),
inference(resolution,[],[f4908,f10]) ).
fof(f4978,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f4945,f10]) ).
fof(f4979,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f4945,f150]) ).
fof(f5011,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X1,X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f4979,f169]) ).
fof(f5022,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))),
inference(resolution,[],[f4979,f11]) ).
fof(f5102,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,implies(X0,X1)),X1))),
inference(resolution,[],[f5022,f2223]) ).
fof(f5106,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X2,X1)))
| ~ is_a_theorem(implies(X2,X0)) ),
inference(resolution,[],[f5022,f170]) ).
fof(f5210,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f5011,f210]) ).
fof(f5263,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF6,sF10)))
| is_a_theorem(implies(X0,sF10)) ),
inference(superposition,[],[f5011,f36]) ).
fof(f5282,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X0,X2))))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f5210,f5011]) ).
fof(f6685,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,not(X0)),implies(X0,X1))),
inference(resolution,[],[f5282,f13]) ).
fof(f6884,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X1,X2)))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f5106,f10]) ).
fof(f6934,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X1),X2))
| ~ is_a_theorem(implies(X0,implies(X2,X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f6884,f38]) ).
fof(f7072,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(implies(not(X1),X1)) ),
inference(resolution,[],[f6934,f973]) ).
fof(f7078,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X2)))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X1,implies(X1,X2))) ),
inference(resolution,[],[f6934,f38]) ).
fof(f7107,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(not(X1),X1)) ),
inference(forward_subsumption_resolution,[],[f7072,f289]) ).
fof(f7148,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(implies(X1,X2)),implies(X1,X2)))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f7107,f11]) ).
fof(f7308,plain,
! [X0] : is_a_theorem(implies(implies(X0,falsehood),implies(X0,sF9))),
inference(resolution,[],[f7148,f2172]) ).
fof(f7394,plain,
is_a_theorem(implies(implies(sF6,falsehood),sF10)),
inference(superposition,[],[f7308,f36]) ).
fof(f7455,plain,
! [X0] : is_a_theorem(implies(X0,implies(falsehood,sF10))),
inference(resolution,[],[f7394,f1484]) ).
fof(f7504,plain,
! [X0] : is_a_theorem(implies(implies(X0,falsehood),implies(X0,sF10))),
inference(resolution,[],[f7455,f7148]) ).
fof(f7565,plain,
is_a_theorem(implies(sF6,implies(sF5,sF10))),
inference(superposition,[],[f7504,f28]) ).
fof(f7570,plain,
is_a_theorem(implies(sF5,implies(sF6,sF10))),
inference(resolution,[],[f7565,f2223]) ).
fof(f7822,plain,
( is_a_theorem(sF10)
| ~ spl11_61 ),
inference(resolution,[],[f2649,f147]) ).
fof(f7849,plain,
( $false
| ~ spl11_61 ),
inference(forward_subsumption_resolution,[],[f7822,f37]) ).
fof(f7850,plain,
~ spl11_61,
inference(avatar_contradiction_clause,[],[f7849]) ).
fof(f8541,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0))),
inference(resolution,[],[f4943,f2755]) ).
fof(f8610,plain,
! [X2,X0,X1] : is_a_theorem(implies(not(implies(X0,X1)),implies(X2,X0))),
inference(resolution,[],[f8541,f4954]) ).
fof(f9319,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),X0),X1))
| ~ is_a_theorem(implies(X0,implies(X0,X1))) ),
inference(resolution,[],[f7078,f2251]) ).
fof(f9429,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| ~ is_a_theorem(implies(not(X0),X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f9319,f2997]) ).
fof(f9436,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(not(X0),X0)))
| is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(implies(X0,implies(X0,X1))) ),
inference(resolution,[],[f9319,f150]) ).
fof(f9655,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X1,X2)))
| is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(not(X1),X0)) ),
inference(resolution,[],[f9436,f38]) ).
fof(f9742,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(not(X1),X0)) ),
inference(resolution,[],[f9655,f2282]) ).
fof(f9781,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(not(X1),X0))
| ~ is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f9655,f269]) ).
fof(f9926,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),implies(X1,X0)))
| is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f9742,f4978]) ).
fof(f9942,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(not(X1),implies(X2,X0)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(resolution,[],[f9742,f4954]) ).
fof(f9990,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(X1,X0)))
| is_a_theorem(implies(X2,implies(X3,X0)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(resolution,[],[f9742,f150]) ).
fof(f10119,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X0),X1))
| is_a_theorem(implies(not(X1),X2))
| ~ is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f9942,f961]) ).
fof(f10267,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),X1))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f9781,f4978]) ).
fof(f17995,definition,
( spl11_216
<=> is_a_theorem(implies(not(sF5),sF10)) ),
introduced(definition,[new_symbols(definition,[spl11_216])],[avatar_definition]) ).
fof(f17996,plain,
( is_a_theorem(implies(not(sF5),sF10))
| ~ spl11_216 ),
inference(avatar_component_clause,[],[f17995]) ).
fof(f17997,plain,
( ~ is_a_theorem(implies(not(sF5),sF10))
| spl11_216 ),
inference(avatar_component_clause,[],[f17995]) ).
fof(f23628,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X2),implies(X0,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f9990,f2204]) ).
fof(f23782,plain,
! [X0] :
( is_a_theorem(implies(sF5,implies(X0,sF10)))
| ~ is_a_theorem(implies(not(sF10),sF6)) ),
inference(resolution,[],[f9990,f7570]) ).
fof(f23816,plain,
! [X0] : is_a_theorem(implies(sF5,implies(X0,sF10))),
inference(forward_subsumption_resolution,[],[f23782,f3131]) ).
fof(f23826,plain,
! [X0] :
( ~ is_a_theorem(implies(not(sF5),sF10))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f23816,f9429]) ).
fof(f23864,plain,
! [X0] : is_a_theorem(implies(implies(X0,sF5),implies(X0,sF10))),
inference(resolution,[],[f23816,f1221]) ).
fof(f23939,plain,
is_a_theorem(implies(implies(sF6,sF5),sF10)),
inference(resolution,[],[f23864,f5263]) ).
fof(f24074,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF6,sF5)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f23939,f150]) ).
fof(f24163,plain,
is_a_theorem(implies(implies(sF6,c),sF10)),
inference(resolution,[],[f24074,f2821]) ).
fof(f24201,plain,
! [X0] : is_a_theorem(implies(X0,implies(c,sF10))),
inference(resolution,[],[f24163,f1484]) ).
fof(f24321,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(c,sF10),X0))
| is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f24201,f990]) ).
fof(f24894,plain,
! [X0] : is_a_theorem(implies(X0,implies(not(not(c)),sF10))),
inference(resolution,[],[f24321,f2323]) ).
fof(f24940,plain,
! [X0] : is_a_theorem(implies(X0,implies(not(sF1),sF10))),
inference(forward_demodulation,[],[f24894,f18]) ).
fof(f25024,plain,
! [X0] : is_a_theorem(implies(not(sF1),implies(X0,sF10))),
inference(resolution,[],[f24940,f23628]) ).
fof(f25323,plain,
! [X0] :
( ~ is_a_theorem(implies(sF1,implies(X0,sF10)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f25024,f10267]) ).
fof(f25403,plain,
is_a_theorem(implies(implies(sF1,sF10),sF10)),
inference(resolution,[],[f25323,f2204]) ).
fof(f25431,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF1,sF10)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f25403,f150]) ).
fof(f25434,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,sF10)))
| ~ is_a_theorem(implies(X1,implies(sF1,sF10))) ),
inference(resolution,[],[f25403,f1180]) ).
fof(f25478,plain,
is_a_theorem(implies(implies(sF1,sF9),sF10)),
inference(resolution,[],[f25431,f2823]) ).
fof(f25743,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF1,sF9)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f25478,f150]) ).
fof(f25784,plain,
is_a_theorem(implies(implies(sF1,sF8),sF10)),
inference(resolution,[],[f25743,f2824]) ).
fof(f25836,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF1,sF8)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f25784,f150]) ).
fof(f26280,plain,
is_a_theorem(implies(implies(sF1,a),sF10)),
inference(resolution,[],[f25836,f2817]) ).
fof(f26323,plain,
is_a_theorem(implies(a,sF10)),
inference(resolution,[],[f26280,f2755]) ).
fof(f26346,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,a))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f26323,f150]) ).
fof(f27083,plain,
is_a_theorem(implies(not(sF0),sF10)),
inference(resolution,[],[f26346,f3124]) ).
fof(f27111,plain,
! [X0] :
( is_a_theorem(implies(not(sF10),X0))
| ~ is_a_theorem(implies(sF0,X0)) ),
inference(resolution,[],[f27083,f10119]) ).
fof(f33892,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(sF1,sF10)))
| is_a_theorem(implies(X1,sF10))
| ~ is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f25434,f10]) ).
fof(f39644,plain,
! [X0] :
( ~ is_a_theorem(implies(sF0,implies(X0,sF10)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f27111,f9926]) ).
fof(f39951,plain,
is_a_theorem(implies(implies(sF0,sF10),sF10)),
inference(resolution,[],[f39644,f2204]) ).
fof(f39982,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF0,sF10)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f39951,f150]) ).
fof(f39985,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,sF10)))
| ~ is_a_theorem(implies(X1,implies(sF0,sF10))) ),
inference(resolution,[],[f39951,f1180]) ).
fof(f40053,plain,
is_a_theorem(implies(implies(sF0,sF9),sF10)),
inference(resolution,[],[f39982,f2823]) ).
fof(f40659,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF0,sF9)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f40053,f150]) ).
fof(f40680,plain,
is_a_theorem(implies(implies(sF0,implies(sF0,sF9)),sF10)),
inference(resolution,[],[f40659,f5022]) ).
fof(f41108,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(sF0,sF10)))
| is_a_theorem(implies(X1,sF10))
| ~ is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f39985,f10]) ).
fof(f48332,plain,
! [X0] : is_a_theorem(implies(X0,implies(implies(sF0,sF9),sF10))),
inference(resolution,[],[f40680,f1484]) ).
fof(f48492,plain,
! [X0] : is_a_theorem(implies(implies(X0,implies(sF0,sF9)),implies(X0,sF10))),
inference(resolution,[],[f48332,f7148]) ).
fof(f48560,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,implies(sF0,sF9)),implies(X1,sF10)))
| ~ is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f48492,f170]) ).
fof(f48760,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X1,implies(sF0,sF9)))
| is_a_theorem(implies(X0,sF10))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f48560,f10]) ).
fof(f48784,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X1,sF9))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f48760,f1486]) ).
fof(f48850,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(e,falsehood)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f48784,f427]) ).
fof(f48897,plain,
is_a_theorem(implies(implies(e,not(e)),sF10)),
inference(resolution,[],[f48850,f6685]) ).
fof(f48942,plain,
is_a_theorem(implies(implies(e,sF2),sF10)),
inference(forward_demodulation,[],[f48897,f20]) ).
fof(f48983,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(e,sF2)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f48942,f150]) ).
fof(f49005,plain,
is_a_theorem(implies(implies(e,implies(e,sF2)),sF10)),
inference(resolution,[],[f48983,f5022]) ).
fof(f52053,plain,
! [X0] : is_a_theorem(implies(X0,implies(implies(e,sF2),sF10))),
inference(resolution,[],[f49005,f1484]) ).
fof(f52303,plain,
! [X0] : is_a_theorem(implies(implies(X0,implies(e,sF2)),implies(X0,sF10))),
inference(resolution,[],[f52053,f7148]) ).
fof(f52434,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF1,implies(e,sF2))))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f52303,f33892]) ).
fof(f52539,plain,
! [X0] :
( ~ is_a_theorem(implies(sF1,implies(X0,sF2)))
| is_a_theorem(implies(implies(e,X0),sF10)) ),
inference(resolution,[],[f52434,f210]) ).
fof(f58006,plain,
is_a_theorem(implies(implies(e,implies(sF1,sF2)),sF10)),
inference(resolution,[],[f52539,f2204]) ).
fof(f58017,plain,
is_a_theorem(implies(implies(e,sF3),sF10)),
inference(forward_demodulation,[],[f58006,f22]) ).
fof(f58031,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(e,sF3)))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f58017,f150]) ).
fof(f58052,plain,
is_a_theorem(implies(implies(e,implies(e,sF3)),sF10)),
inference(resolution,[],[f58031,f5022]) ).
fof(f58159,plain,
! [X0] : is_a_theorem(implies(X0,implies(implies(e,sF3),sF10))),
inference(resolution,[],[f58052,f1484]) ).
fof(f58418,plain,
! [X0] : is_a_theorem(implies(implies(X0,implies(e,sF3)),implies(X0,sF10))),
inference(resolution,[],[f58159,f7148]) ).
fof(f58547,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF0,implies(e,sF3))))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f58418,f41108]) ).
fof(f58583,plain,
! [X0] :
( ~ is_a_theorem(implies(sF0,implies(X0,sF3)))
| is_a_theorem(implies(implies(e,X0),sF10)) ),
inference(resolution,[],[f58547,f210]) ).
fof(f61982,plain,
is_a_theorem(implies(implies(e,implies(sF0,implies(sF0,sF3))),sF10)),
inference(resolution,[],[f58583,f5102]) ).
fof(f61990,plain,
is_a_theorem(implies(implies(e,implies(sF0,sF4)),sF10)),
inference(forward_demodulation,[],[f61982,f24]) ).
fof(f64467,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(e,implies(sF0,sF4))))
| is_a_theorem(implies(X0,sF10)) ),
inference(resolution,[],[f61990,f150]) ).
fof(f64796,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF0,sF4)))
| is_a_theorem(implies(implies(e,X0),sF10)) ),
inference(resolution,[],[f64467,f868]) ).
fof(f64875,plain,
! [X0] :
( is_a_theorem(implies(implies(e,X0),sF10))
| ~ is_a_theorem(implies(X0,sF4)) ),
inference(resolution,[],[f64796,f1486]) ).
fof(f64973,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X1,implies(e,X0)))
| is_a_theorem(implies(X1,sF10))
| ~ is_a_theorem(implies(X0,sF4)) ),
inference(resolution,[],[f64875,f150]) ).
fof(f65150,plain,
! [X0,X1] :
( is_a_theorem(implies(not(implies(X0,X1)),sF10))
| ~ is_a_theorem(implies(X0,sF4)) ),
inference(resolution,[],[f64973,f8610]) ).
fof(f65663,plain,
( is_a_theorem(implies(not(sF5),sF10))
| ~ is_a_theorem(implies(sF4,sF4)) ),
inference(superposition,[],[f65150,f26]) ).
fof(f65668,plain,
( ~ is_a_theorem(implies(sF4,sF4))
| spl11_216 ),
inference(forward_subsumption_resolution,[],[f65663,f17997]) ).
fof(f65677,plain,
( $false
| spl11_216 ),
inference(forward_subsumption_resolution,[],[f65668,f203]) ).
fof(f65678,plain,
spl11_216,
inference(avatar_contradiction_clause,[],[f65677]) ).
fof(f65680,plain,
( ! [X0] : is_a_theorem(implies(X0,sF10))
| ~ spl11_216 ),
inference(forward_subsumption_resolution,[],[f23826,f17996]) ).
fof(f65687,plain,
( spl11_61
| ~ spl11_216 ),
inference(avatar_split_clause,[],[f65680,f17995,f2648]) ).
cnf(s87,plain,
~ spl11_61,
inference(sat_conversion,[],[f7850]) ).
cnf(s900,plain,
spl11_216,
inference(sat_conversion,[],[f65678]) ).
cnf(s902,plain,
( spl11_61
| ~ spl11_216 ),
inference(sat_conversion,[],[f65687]) ).
cnf(s908,plain,
spl11_61,
inference(rat,[],[s902,s900]) ).
cnf(s951,plain,
$false,
inference(rat,[],[s87,s908]) ).
fof(f65688,plain,
$false,
inference(avatar_sat_refutation,[],[s951]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL063+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.49 % Computer : n015.cluster.edu
% 0.23/0.49 % Model : x86_64 x86_64
% 0.23/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.49 % Memory : 8046.5625MB
% 0.23/0.49 % OS : Linux 6.8.0-71-generic
% 0.23/0.49 % CPULimit : 300
% 0.24/0.49 % WCLimit : 300
% 0.24/0.49 % DateTime : Sun Sep 27 15:23:31 UTC 2026
% 0.24/0.49 % CPUTime :
% 0.24/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.55 Running first-order theorem proving
% 0.24/0.55 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.44/4.49 % (1774517)Detected formulas, will run a generic FOF schedule.
% 22.44/4.49 % (1774522)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=2418146027:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 22.44/4.49 % (1774523)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=2034479442:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 22.44/4.49 % (1774524)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=1926770008:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 22.44/4.49 % (1774525)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4162511740:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 22.44/4.49 % (1774525)Refutation not found, incomplete strategy
% 22.44/4.49 % (1774525)------------------------------
% 22.44/4.49 % (1774525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.44/4.49 % (1774525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/4.49 % (1774525)CaDiCaL version: 2.1.3
% 22.44/4.49 % (1774525)Termination reason: Refutation not found, incomplete strategy
% 22.44/4.49 % (1774525)Time elapsed: 0.001 s
% 22.44/4.49 % (1774525)Peak memory usage: 87 MB
% 22.44/4.49 % (1774526)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=850557803:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 22.44/4.49 % (1774528)dis-21_1_sil=8000:lcm=predicate:random_seed=2590442594: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)
% 22.44/4.49 % (1774527)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1737562806:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 22.44/4.49 % (1774526)Instruction limit reached!
% 22.44/4.49 % (1774526)------------------------------
% 22.44/4.49 % (1774526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.44/4.49 % (1774526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/4.49 % (1774526)CaDiCaL version: 2.1.3
% 22.44/4.49 % (1774526)Termination reason: Instruction limit
% 22.44/4.49 % (1774526)Termination phase: Saturation
% 22.44/4.49 % (1774526)Time elapsed: 0.111 s
% 22.44/4.49 % (1774526)Peak memory usage: 87 MB
% 22.44/4.49 % (1774526)Instructions burned: 120 (million)
% 22.44/4.49 % (1774528)Instruction limit reached!
% 22.44/4.49 % (1774528)------------------------------
% 22.44/4.49 % (1774528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.44/4.49 % (1774528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/4.49 % (1774528)CaDiCaL version: 2.1.3
% 22.44/4.49 % (1774528)Termination reason: Instruction limit
% 22.44/4.49 % (1774528)Termination phase: Saturation
% 22.44/4.49 % (1774528)Time elapsed: 0.125 s
% 22.44/4.49 % (1774528)Peak memory usage: 89 MB
% 22.44/4.49 % (1774528)Instructions burned: 132 (million)
% 22.44/4.49 % (1774527)Instruction limit reached!
% 22.44/4.49 % (1774527)------------------------------
% 22.44/4.49 % (1774527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.44/4.49 % (1774527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.44/4.49 % (1774527)CaDiCaL version: 2.1.3
% 22.44/4.49 % (1774527)Termination reason: Instruction limit
% 22.44/4.49 % (1774527)Termination phase: Saturation
% 22.44/4.49 % (1774527)Time elapsed: 0.146 s
% 22.44/4.49 % (1774527)Peak memory usage: 89 MB
% 22.44/4.49 % (1774527)Instructions burned: 140 (million)
% 22.44/4.49 % (1774536)lrs+10_1_sil=8000:sp=occurrence:random_seed=238615460:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 22.44/4.49 % (1774537)lrs+10_1_sil=32000:urr=on:br=off:random_seed=203133632:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 22.44/4.49 % (1774538)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2507896677:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 22.44/4.49 % (1774525)------------------------------
% 22.44/4.49 % (1774525)------------------------------
% 22.44/4.49 % (1774537)Instruction limit reached!
% 22.44/4.49 % (1774537)------------------------------
% 22.44/4.49 % (1774537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.44/4.49 % (1774537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774537)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774537)Termination reason: Instruction limit
% 32.46/5.90 % (1774537)Termination phase: Saturation
% 32.46/5.90 % (1774537)Time elapsed: 0.145 s
% 32.46/5.90 % (1774537)Peak memory usage: 89 MB
% 32.46/5.90 % (1774537)Instructions burned: 157 (million)
% 32.46/5.90 % (1774542)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=4188810177:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 32.46/5.90 % (1774536)Instruction limit reached!
% 32.46/5.90 % (1774536)------------------------------
% 32.46/5.90 % (1774536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.46/5.90 % (1774536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774536)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774536)Termination reason: Instruction limit
% 32.46/5.90 % (1774536)Termination phase: Saturation
% 32.46/5.90 % (1774536)Time elapsed: 0.300 s
% 32.46/5.90 % (1774536)Peak memory usage: 90 MB
% 32.46/5.90 % (1774536)Instructions burned: 285 (million)
% 32.46/5.90 % (1774542)Instruction limit reached!
% 32.46/5.90 % (1774542)------------------------------
% 32.46/5.90 % (1774542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.46/5.90 % (1774542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774542)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774542)Termination reason: Instruction limit
% 32.46/5.90 % (1774542)Termination phase: Saturation
% 32.46/5.90 % (1774542)Time elapsed: 0.113 s
% 32.46/5.90 % (1774542)Peak memory usage: 89 MB
% 32.46/5.90 % (1774542)Instructions burned: 248 (million)
% 32.46/5.90 % (1774538)Instruction limit reached!
% 32.46/5.90 % (1774538)------------------------------
% 32.46/5.90 % (1774538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.46/5.90 % (1774538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774538)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774538)Termination reason: Instruction limit
% 32.46/5.90 % (1774538)Termination phase: Saturation
% 32.46/5.90 % (1774538)Time elapsed: 0.335 s
% 32.46/5.90 % (1774538)Peak memory usage: 93 MB
% 32.46/5.90 % (1774538)Instructions burned: 325 (million)
% 32.46/5.90 % (1774543)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=388585760:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 32.46/5.90 % (1774543)Refutation not found, incomplete strategy
% 32.46/5.90 % (1774543)------------------------------
% 32.46/5.90 % (1774543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.46/5.90 % (1774543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774543)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774543)Termination reason: Refutation not found, incomplete strategy
% 32.46/5.90 % (1774543)Time elapsed: 0.001 s
% 32.46/5.90 % (1774543)Peak memory usage: 87 MB
% 32.46/5.90 % (1774546)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=840546497:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 32.46/5.90 % (1774545)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1887906451:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 32.46/5.90 % (1774546)Instruction limit reached!
% 32.46/5.90 % (1774546)------------------------------
% 32.46/5.90 % (1774546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.46/5.90 % (1774546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774546)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774546)Termination reason: Instruction limit
% 32.46/5.90 % (1774546)Termination phase: Saturation
% 32.46/5.90 % (1774546)Time elapsed: 0.057 s
% 32.46/5.90 % (1774546)Peak memory usage: 89 MB
% 32.46/5.90 % (1774546)Instructions burned: 114 (million)
% 32.46/5.90 % (1774547)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1162188676:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 32.46/5.90 % (1774547)Instruction limit reached!
% 32.46/5.90 % (1774547)------------------------------
% 32.46/5.90 % (1774547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.46/5.90 % (1774547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.46/5.90 % (1774547)CaDiCaL version: 2.1.3
% 32.46/5.90 % (1774547)Termination reason: Instruction limit
% 32.46/5.90 % (1774547)Termination phase: Saturation
% 82.03/12.89 % (1774547)Time elapsed: 0.118 s
% 82.03/12.89 % (1774547)Peak memory usage: 88 MB
% 82.03/12.89 % (1774547)Instructions burned: 127 (million)
% 82.03/12.89 % (1774551)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3739764335:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 82.03/12.89 % (1774543)------------------------------
% 82.03/12.89 % (1774543)------------------------------
% 82.03/12.89 % (1774551)Instruction limit reached!
% 82.03/12.89 % (1774551)------------------------------
% 82.03/12.89 % (1774551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.03/12.89 % (1774551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.03/12.89 % (1774551)CaDiCaL version: 2.1.3
% 82.03/12.89 % (1774551)Termination reason: Instruction limit
% 82.03/12.89 % (1774551)Termination phase: Saturation
% 82.03/12.89 % (1774551)Time elapsed: 0.062 s
% 82.03/12.89 % (1774551)Peak memory usage: 89 MB
% 82.03/12.89 % (1774551)Instructions burned: 114 (million)
% 82.03/12.89 % (1774553)lrs+10_1_sil=8000:sp=occurrence:random_seed=368468828:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 82.03/12.89 % (1774555)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3360255195:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 82.03/12.89 % (1774555)Refutation not found, incomplete strategy
% 82.03/12.89 % (1774555)------------------------------
% 82.03/12.89 % (1774555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.03/12.89 % (1774555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.03/12.89 % (1774555)CaDiCaL version: 2.1.3
% 82.03/12.89 % (1774555)Termination reason: Refutation not found, incomplete strategy
% 82.03/12.89 % (1774555)Time elapsed: 0.001 s
% 82.03/12.89 % (1774555)Peak memory usage: 88 MB
% 82.03/12.89 % (1774556)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2430375927:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 82.03/12.89 % (1774555)------------------------------
% 82.03/12.89 % (1774555)------------------------------
% 82.03/12.89 % (1774560)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=787409171:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 82.03/12.89 % (1774560)Instruction limit reached!
% 82.03/12.89 % (1774560)------------------------------
% 82.03/12.89 % (1774560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.03/12.89 % (1774560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.03/12.89 % (1774560)CaDiCaL version: 2.1.3
% 82.03/12.89 % (1774560)Termination reason: Instruction limit
% 82.03/12.89 % (1774560)Termination phase: Saturation
% 82.03/12.89 % (1774560)Time elapsed: 0.120 s
% 82.03/12.89 % (1774560)Peak memory usage: 89 MB
% 82.03/12.89 % (1774560)Instructions burned: 134 (million)
% 82.03/12.89 % (1774553)Instruction limit reached!
% 82.03/12.89 % (1774553)------------------------------
% 82.03/12.89 % (1774553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.03/12.89 % (1774553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.03/12.89 % (1774553)CaDiCaL version: 2.1.3
% 82.03/12.89 % (1774553)Termination reason: Instruction limit
% 82.03/12.89 % (1774553)Termination phase: Saturation
% 82.03/12.89 % (1774553)Time elapsed: 0.906 s
% 82.03/12.89 % (1774553)Peak memory usage: 95 MB
% 82.03/12.89 % (1774553)Instructions burned: 907 (million)
% 82.03/12.89 % (1774562)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2174000652:st=8:i=592:sd=3:ep=RST:ss=axioms_2976 on theBenchmark for (2976ds/592Mi)
% 82.03/12.89 % (1774562)Refutation not found, incomplete strategy
% 82.03/12.89 % (1774562)------------------------------
% 82.03/12.89 % (1774562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 82.03/12.89 % (1774562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 82.03/12.89 % (1774562)CaDiCaL version: 2.1.3
% 82.03/12.89 % (1774562)Termination reason: Refutation not found, incomplete strategy
% 82.03/12.89 % (1774562)Time elapsed: 0.001 s
% 82.03/12.89 % (1774562)Peak memory usage: 87 MB
% 82.03/12.89 % (1774563)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=760842147:st=3:i=13193:sd=3:ss=axioms_2975 on theBenchmark for (2975ds/13193Mi)
% 82.03/12.89 % (1774562)------------------------------
% 82.03/12.89 % (1774562)------------------------------
% 82.03/12.89 % (1774566)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=1593495476:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 50.97/14.12 % (1774566)Instruction limit reached!
% 50.97/14.12 % (1774566)------------------------------
% 50.97/14.12 % (1774566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774566)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774566)Termination reason: Instruction limit
% 50.97/14.12 % (1774566)Termination phase: Saturation
% 50.97/14.12 % (1774566)Time elapsed: 0.119 s
% 50.97/14.12 % (1774566)Peak memory usage: 89 MB
% 50.97/14.12 % (1774566)Instructions burned: 126 (million)
% 50.97/14.12 % (1774545)Instruction limit reached!
% 50.97/14.12 % (1774545)------------------------------
% 50.97/14.12 % (1774545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774545)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774545)Termination reason: Instruction limit
% 50.97/14.12 % (1774545)Termination phase: Saturation
% 50.97/14.12 % (1774545)Time elapsed: 2.476 s
% 50.97/14.12 % (1774545)Peak memory usage: 141 MB
% 50.97/14.12 % (1774545)Instructions burned: 2350 (million)
% 50.97/14.12 % (1774568)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2447121880:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 50.97/14.12 % (1774568)Instruction limit reached!
% 50.97/14.12 % (1774568)------------------------------
% 50.97/14.12 % (1774568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774568)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774568)Termination reason: Instruction limit
% 50.97/14.12 % (1774568)Termination phase: Saturation
% 50.97/14.12 % (1774568)Time elapsed: 0.146 s
% 50.97/14.12 % (1774568)Peak memory usage: 90 MB
% 50.97/14.12 % (1774568)Instructions burned: 134 (million)
% 50.97/14.12 % (1774569)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=319778276:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2964 on theBenchmark for (2964ds/141Mi)
% 50.97/14.12 % (1774569)Refutation not found, incomplete strategy
% 50.97/14.12 % (1774569)------------------------------
% 50.97/14.12 % (1774569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774569)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774569)Termination reason: Refutation not found, incomplete strategy
% 50.97/14.12 % (1774569)Time elapsed: 0.001 s
% 50.97/14.12 % (1774569)Peak memory usage: 88 MB
% 50.97/14.12 % (1774571)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=26714339:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2962 on theBenchmark for (2962ds/431Mi)
% 50.97/14.12 % (1774569)------------------------------
% 50.97/14.12 % (1774569)------------------------------
% 50.97/14.12 % (1774571)Instruction limit reached!
% 50.97/14.12 % (1774571)------------------------------
% 50.97/14.12 % (1774571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774571)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774571)Termination reason: Instruction limit
% 50.97/14.12 % (1774571)Termination phase: Saturation
% 50.97/14.12 % (1774571)Time elapsed: 0.416 s
% 50.97/14.12 % (1774571)Peak memory usage: 91 MB
% 50.97/14.12 % (1774571)Instructions burned: 432 (million)
% 50.97/14.12 % (1774556)Instruction limit reached!
% 50.97/14.12 % (1774556)------------------------------
% 50.97/14.12 % (1774556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774556)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774556)Termination reason: Instruction limit
% 50.97/14.12 % (1774556)Termination phase: Saturation
% 50.97/14.12 % (1774556)Time elapsed: 2.792 s
% 50.97/14.12 % (1774556)Peak memory usage: 155 MB
% 50.97/14.12 % (1774556)Instructions burned: 5202 (million)
% 50.97/14.12 % (1774574)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=4230013815:i=6060:aac=none:ins=25_2958 on theBenchmark for (2958ds/6060Mi)
% 50.97/14.12 % (1774575)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=2013470051:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2956 on theBenchmark for (2956ds/150Mi)
% 50.97/14.12 % (1774577)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2598640899:i=14155:bd=all_2955 on theBenchmark for (2955ds/14155Mi)
% 50.97/14.12 % (1774575)Instruction limit reached!
% 50.97/14.12 % (1774575)------------------------------
% 50.97/14.12 % (1774575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774575)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774575)Termination reason: Instruction limit
% 50.97/14.12 % (1774575)Termination phase: Saturation
% 50.97/14.12 % (1774575)Time elapsed: 0.152 s
% 50.97/14.12 % (1774575)Peak memory usage: 90 MB
% 50.97/14.12 % (1774575)Instructions burned: 150 (million)
% 50.97/14.12 % (1774580)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2449775505:i=667:av=off:fsr=off_2952 on theBenchmark for (2952ds/667Mi)
% 50.97/14.12 % (1774580)Refutation not found, incomplete strategy
% 50.97/14.12 % (1774580)------------------------------
% 50.97/14.12 % (1774580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774580)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774580)Termination reason: Refutation not found, incomplete strategy
% 50.97/14.12 % (1774580)Time elapsed: 0.001 s
% 50.97/14.12 % (1774580)Peak memory usage: 87 MB
% 50.97/14.12 % (1774580)------------------------------
% 50.97/14.12 % (1774580)------------------------------
% 50.97/14.12 % (1774582)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=4273831862:s2a=on:i=185:s2at=1.8:fdi=4_2945 on theBenchmark for (2945ds/185Mi)
% 50.97/14.12 % (1774582)Instruction limit reached!
% 50.97/14.12 % (1774582)------------------------------
% 50.97/14.12 % (1774582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774582)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774582)Termination reason: Instruction limit
% 50.97/14.12 % (1774582)Termination phase: Saturation
% 50.97/14.12 % (1774582)Time elapsed: 0.178 s
% 50.97/14.12 % (1774582)Peak memory usage: 90 MB
% 50.97/14.12 % (1774582)Instructions burned: 186 (million)
% 50.97/14.12 % (1774584)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3549883540:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2941 on theBenchmark for (2941ds/193Mi)
% 50.97/14.12 % (1774584)Instruction limit reached!
% 50.97/14.12 % (1774584)------------------------------
% 50.97/14.12 % (1774584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774584)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774584)Termination reason: Instruction limit
% 50.97/14.12 % (1774584)Termination phase: Saturation
% 50.97/14.12 % (1774584)Time elapsed: 0.200 s
% 50.97/14.12 % (1774584)Peak memory usage: 92 MB
% 50.97/14.12 % (1774584)Instructions burned: 193 (million)
% 50.97/14.12 % (1774586)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=975189217:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2935 on theBenchmark for (2935ds/4850Mi)
% 50.97/14.12 % (1774574)Instruction limit reached!
% 50.97/14.12 % (1774574)------------------------------
% 50.97/14.12 % (1774574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774574)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774574)Termination reason: Instruction limit
% 50.97/14.12 % (1774574)Termination phase: Saturation
% 50.97/14.12 % (1774574)Time elapsed: 5.392 s
% 50.97/14.12 % (1774574)Peak memory usage: 143 MB
% 50.97/14.12 % (1774574)Instructions burned: 6060 (million)
% 50.97/14.12 % (1774588)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=2069780725:i=12111:sd=1:ss=included_2901 on theBenchmark for (2901ds/12111Mi)
% 50.97/14.12 % (1774577)Instruction limit reached!
% 50.97/14.12 % (1774577)------------------------------
% 50.97/14.12 % (1774577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774577)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774577)Termination reason: Instruction limit
% 50.97/14.12 % (1774577)Termination phase: Saturation
% 50.97/14.12 % (1774577)Time elapsed: 6.974 s
% 50.97/14.12 % (1774577)Peak memory usage: 252 MB
% 50.97/14.12 % (1774577)Instructions burned: 14156 (million)
% 50.97/14.12 % (1774590)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1455037997:i=319:kws=precedence:fsr=off_2883 on theBenchmark for (2883ds/319Mi)
% 50.97/14.12 % (1774586)Instruction limit reached!
% 50.97/14.12 % (1774586)------------------------------
% 50.97/14.12 % (1774586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774586)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774586)Termination reason: Instruction limit
% 50.97/14.12 % (1774586)Termination phase: Saturation
% 50.97/14.12 % (1774586)Time elapsed: 5.254 s
% 50.97/14.12 % (1774586)Peak memory usage: 124 MB
% 50.97/14.12 % (1774586)Instructions burned: 4850 (million)
% 50.97/14.12 % (1774590)Instruction limit reached!
% 50.97/14.12 % (1774590)------------------------------
% 50.97/14.12 % (1774590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774590)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774590)Termination reason: Instruction limit
% 50.97/14.12 % (1774590)Termination phase: Saturation
% 50.97/14.12 % (1774590)Time elapsed: 0.160 s
% 50.97/14.12 % (1774590)Peak memory usage: 92 MB
% 50.97/14.12 % (1774590)Instructions burned: 320 (million)
% 50.97/14.12 % (1774592)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=748271931:i=2064:ep=RST_2880 on theBenchmark for (2880ds/2064Mi)
% 50.97/14.12 % (1774592)Refutation not found, incomplete strategy
% 50.97/14.12 % (1774592)------------------------------
% 50.97/14.12 % (1774592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774592)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774592)Termination reason: Refutation not found, incomplete strategy
% 50.97/14.12 % (1774592)Time elapsed: 0.001 s
% 50.97/14.12 % (1774592)Peak memory usage: 88 MB
% 50.97/14.12 % (1774593)dis-1011_128_sil=32000:random_seed=185214102:i=3706:ep=RST:av=off_2880 on theBenchmark for (2880ds/3706Mi)
% 50.97/14.12 % (1774592)------------------------------
% 50.97/14.12 % (1774592)------------------------------
% 50.97/14.12 % (1774522)First to succeed.
% 50.97/14.12 % (1774522)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1774517"
% 50.97/14.12 % (1774596)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=3905850533:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2877 on theBenchmark for (2877ds/757Mi)
% 50.97/14.12 % (1774596)Refutation not found, incomplete strategy
% 50.97/14.12 % (1774596)------------------------------
% 50.97/14.12 % (1774596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.97/14.12 % (1774596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.97/14.12 % (1774596)CaDiCaL version: 2.1.3
% 50.97/14.12 % (1774596)Termination reason: Refutation not found, incomplete strategy
% 50.97/14.12 % (1774596)Time elapsed: 0.001 s
% 50.97/14.12 % (1774596)Peak memory usage: 88 MB
% 50.97/14.12 % (1774596)------------------------------
% 50.97/14.12 % (1774596)------------------------------
% 50.97/14.12 % (1774522)Refutation found. Thanks to Tanya!
% 50.97/14.12 % SZS status Theorem for theBenchmark
% 50.97/14.12 % SZS output start Proof for theBenchmark
% See solution above
% 0.30/14.50 % (1774522)------------------------------
% 0.30/14.50 % (1774522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.30/14.50 % (1774522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/14.50 % (1774522)CaDiCaL version: 2.1.3
% 0.30/14.50 % (1774522)Termination reason: Refutation
% 0.30/14.50 % (1774522)Time elapsed: 12.190 s
% 0.30/14.50 % (1774522)Peak memory usage: 228 MB
% 0.30/14.50 % (1774522)Instructions burned: 12225 (million)
% 0.30/14.50 % (1774522)------------------------------
% 0.30/14.50 % (1774522)------------------------------
% 0.30/14.50 % (1774517)Success in time 12.809 s
% 0.30/14.50 % Vampire exiting
%------------------------------------------------------------------------------