%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL330-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:52:00 AM UTC 2026
% Result : Unsatisfiable 16.02s 3.62s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 50
% Syntax : Number of formulae : 290 ( 158 unt; 38 def)
% Number of atoms : 607 ( 227 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 616 ( 299 ~; 293 |; 0 &)
% ( 24 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 26 ( 24 usr; 25 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 17 con; 0-4 aty)
% Number of variables : 236 ( 0 sgn 236 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_3) ).
fof(f4,plain,
! [X0,X1] : true = axiom(implies(X0,or(X1,X0))),
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_4) ).
fof(f6,plain,
! [X0,X1] : true = axiom(implies(or(X0,X1),or(X1,X0))),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_5) ).
fof(f8,plain,
! [X2,X0,X1] : true = axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X2,X0,X1] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_6) ).
fof(f10,plain,
! [X2,X0,X1] : true = axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
inference(reorient_equations,[],[f9]) ).
fof(f11,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_definition) ).
fof(f12,axiom,
! [X0] : ifeq(axiom(X0),true,theorem(X0),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_1) ).
fof(f13,plain,
! [X0] : true = ifeq(axiom(X0),true,theorem(X0),true),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X0,X1] : ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_2) ).
fof(f15,plain,
! [X0,X1] : true = ifeq(theorem(implies(X0,X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_defn) ).
fof(f17,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f18,negated_conjecture,
theorem(equivalent(or(p,q),implies(implies(p,q),q))) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f19,plain,
true != theorem(equivalent(or(p,q),implies(implies(p,q),q))),
inference(reorient_equations,[],[f18]) ).
fof(f20,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f17,f16,f11,f11]) ).
fof(f21,plain,
! [X0] : true = axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f2,f11]) ).
fof(f22,plain,
! [X0,X1] : true = axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f4,f11]) ).
fof(f23,plain,
! [X0,X1] : true = axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f6,f11]) ).
fof(f24,plain,
! [X2,X0,X1] : true = axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f8,f11]) ).
fof(f25,plain,
! [X2,X0,X1] : true = axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f10,f11,f11,f11]) ).
fof(f26,plain,
! [X0,X1] : true = ifeq(theorem(or(not(X0),X1)),true,ifeq(theorem(X0),true,theorem(X1),true),true),
inference(definition_unfolding,[],[f15,f11]) ).
fof(f27,plain,
true != theorem(not(or(not(or(not(or(p,q)),or(not(or(not(p),q)),q))),not(or(not(or(not(or(not(p),q)),q)),or(p,q)))))),
inference(definition_unfolding,[],[f19,f20,f11,f11]) ).
fof(f28,definition,
sF0 = or(p,q),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f29,plain,
or(p,q) = sF0,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF1 = not(sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f31,plain,
not(sF0) = sF1,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF2 = not(p),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f33,plain,
not(p) = sF2,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF3 = or(sF2,q),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f35,plain,
or(sF2,q) = sF3,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF4 = not(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f37,plain,
not(sF3) = sF4,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF5 = or(sF4,q),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f39,plain,
or(sF4,q) = sF5,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF6 = or(sF1,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f41,plain,
or(sF1,sF5) = sF6,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF7 = not(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f43,plain,
not(sF6) = sF7,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF8 = not(sF5),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f45,plain,
not(sF5) = sF8,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF9 = or(sF8,sF0),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f47,plain,
or(sF8,sF0) = sF9,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF10 = not(sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f49,plain,
not(sF9) = sF10,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF11 = or(sF7,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f51,plain,
or(sF7,sF10) = sF11,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF12 = not(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f53,plain,
not(sF11) = sF12,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF13 = theorem(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f55,plain,
theorem(sF12) = sF13,
inference(reorient_equations,[],[f54]) ).
fof(f56,plain,
true != sF13,
inference(definition_folding,[],[f27,f55,f53,f51,f49,f47,f29,f45,f39,f37,f35,f33,f43,f41,f39,f37,f35,f33,f31,f29]) ).
fof(f58,definition,
( spl14_1
<=> theorem(sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f60,plain,
( theorem(sF12) = sF13
| ~ spl14_1 ),
inference(avatar_component_clause,[],[f58]) ).
fof(f61,plain,
spl14_1,
inference(avatar_split_clause,[],[f55,f58]) ).
fof(f63,definition,
( spl14_2
<=> true = sF13 ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
fof(f65,plain,
( true != sF13
| spl14_2 ),
inference(avatar_component_clause,[],[f63]) ).
fof(f66,plain,
~ spl14_2,
inference(avatar_split_clause,[],[f56,f63]) ).
fof(f70,definition,
( spl14_3
<=> not(p) = sF2 ),
introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition]) ).
fof(f72,plain,
( not(p) = sF2
| ~ spl14_3 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f73,plain,
spl14_3,
inference(avatar_split_clause,[],[f33,f70]) ).
fof(f77,definition,
( spl14_4
<=> not(sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f79,plain,
( not(sF0) = sF1
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f77]) ).
fof(f80,plain,
spl14_4,
inference(avatar_split_clause,[],[f31,f77]) ).
fof(f84,definition,
( spl14_5
<=> not(sF5) = sF8 ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f86,plain,
( not(sF5) = sF8
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f84]) ).
fof(f87,plain,
spl14_5,
inference(avatar_split_clause,[],[f45,f84]) ).
fof(f91,definition,
( spl14_6
<=> not(sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f93,plain,
( not(sF3) = sF4
| ~ spl14_6 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f94,plain,
spl14_6,
inference(avatar_split_clause,[],[f37,f91]) ).
fof(f98,definition,
( spl14_7
<=> not(sF11) = sF12 ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f100,plain,
( not(sF11) = sF12
| ~ spl14_7 ),
inference(avatar_component_clause,[],[f98]) ).
fof(f101,plain,
spl14_7,
inference(avatar_split_clause,[],[f53,f98]) ).
fof(f103,definition,
( spl14_8
<=> not(sF9) = sF10 ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f105,plain,
( not(sF9) = sF10
| ~ spl14_8 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f106,plain,
spl14_8,
inference(avatar_split_clause,[],[f49,f103]) ).
fof(f112,definition,
( spl14_9
<=> not(sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f114,plain,
( not(sF6) = sF7
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
spl14_9,
inference(avatar_split_clause,[],[f43,f112]) ).
fof(f118,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(X1,X0))),true),
inference(superposition,[],[f13,f23]) ).
fof(f119,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X1,X0))),true),
inference(superposition,[],[f13,f22]) ).
fof(f120,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),true),
inference(superposition,[],[f13,f24]) ).
fof(f121,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),X0)),true),
inference(superposition,[],[f13,f21]) ).
fof(f123,plain,
! [X0] : true = theorem(or(not(or(X0,X0)),X0)),
inference(forward_demodulation,[],[f121,f1]) ).
fof(f124,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(forward_demodulation,[],[f120,f1]) ).
fof(f125,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X1,X0))),
inference(forward_demodulation,[],[f119,f1]) ).
fof(f126,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(forward_demodulation,[],[f118,f1]) ).
fof(f127,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),true),
inference(superposition,[],[f26,f124]) ).
fof(f133,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),
inference(forward_demodulation,[],[f127,f1]) ).
fof(f134,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f126]) ).
fof(f140,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f134,f1]) ).
fof(f169,plain,
! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,X0)),true,theorem(X0),true),true),
inference(superposition,[],[f26,f123]) ).
fof(f178,plain,
! [X0] : true = ifeq(theorem(or(X0,X0)),true,theorem(X0),true),
inference(forward_demodulation,[],[f169,f1]) ).
fof(f181,definition,
( spl14_10
<=> or(sF1,sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
fof(f183,plain,
( or(sF1,sF5) = sF6
| ~ spl14_10 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f184,plain,
spl14_10,
inference(avatar_split_clause,[],[f41,f181]) ).
fof(f202,definition,
( spl14_11
<=> or(sF8,sF0) = sF9 ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
fof(f204,plain,
( or(sF8,sF0) = sF9
| ~ spl14_11 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,plain,
spl14_11,
inference(avatar_split_clause,[],[f47,f202]) ).
fof(f217,plain,
( ! [X0] : true = ifeq(theorem(or(sF8,or(X0,sF0))),true,theorem(or(X0,sF9)),true)
| ~ spl14_11 ),
inference(superposition,[],[f133,f204]) ).
fof(f223,definition,
( spl14_12
<=> or(p,q) = sF0 ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f225,plain,
( or(p,q) = sF0
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,plain,
spl14_12,
inference(avatar_split_clause,[],[f29,f223]) ).
fof(f242,definition,
( spl14_13
<=> or(sF4,q) = sF5 ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f244,plain,
( or(sF4,q) = sF5
| ~ spl14_13 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f245,plain,
spl14_13,
inference(avatar_split_clause,[],[f39,f242]) ).
fof(f257,plain,
( ! [X0] : true = ifeq(theorem(or(sF4,or(X0,q))),true,theorem(or(X0,sF5)),true)
| ~ spl14_13 ),
inference(superposition,[],[f133,f244]) ).
fof(f261,definition,
( spl14_14
<=> or(sF7,sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
fof(f263,plain,
( or(sF7,sF10) = sF11
| ~ spl14_14 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f264,plain,
spl14_14,
inference(avatar_split_clause,[],[f51,f261]) ).
fof(f280,definition,
( spl14_15
<=> or(sF2,q) = sF3 ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
fof(f282,plain,
( or(sF2,q) = sF3
| ~ spl14_15 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f283,plain,
spl14_15,
inference(avatar_split_clause,[],[f35,f280]) ).
fof(f317,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),true),
inference(superposition,[],[f13,f25]) ).
fof(f318,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(forward_demodulation,[],[f317,f1]) ).
fof(f346,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X2,X0)),or(X2,X1))),true),true),
inference(superposition,[],[f26,f318]) ).
fof(f348,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),true),
inference(superposition,[],[f133,f318]) ).
fof(f354,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),
inference(forward_demodulation,[],[f348,f1]) ).
fof(f355,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(not(X0),X1)),true,theorem(or(not(or(X2,X0)),or(X2,X1))),true),
inference(forward_demodulation,[],[f346,f1]) ).
fof(f373,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f355,f126]) ).
fof(f374,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f355,f125]) ).
fof(f376,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),true),
inference(superposition,[],[f355,f123]) ).
fof(f401,plain,
! [X0,X1] : true = theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),
inference(forward_demodulation,[],[f376,f1]) ).
fof(f403,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f374,f1]) ).
fof(f404,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f373,f1]) ).
fof(f416,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),true),
inference(superposition,[],[f26,f401]) ).
fof(f424,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),
inference(forward_demodulation,[],[f416,f1]) ).
fof(f449,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X1),X2)),or(X0,X2))),true),true),
inference(superposition,[],[f26,f354]) ).
fof(f458,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X1),X2)),or(X0,X2))),true),
inference(forward_demodulation,[],[f449,f1]) ).
fof(f482,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),true),
inference(superposition,[],[f26,f404]) ).
fof(f490,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f482,f1]) ).
fof(f503,plain,
( ! [X0] : true = theorem(or(not(or(X0,q)),or(X0,sF5)))
| ~ spl14_13 ),
inference(superposition,[],[f403,f244]) ).
fof(f508,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),true),
inference(superposition,[],[f26,f403]) ).
fof(f516,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f508,f1]) ).
fof(f578,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(X0),X0)),true),
inference(superposition,[],[f424,f125]) ).
fof(f604,plain,
! [X0] : true = theorem(or(not(X0),X0)),
inference(forward_demodulation,[],[f578,f1]) ).
fof(f610,plain,
( true = theorem(or(sF4,sF3))
| ~ spl14_6 ),
inference(superposition,[],[f604,f93]) ).
fof(f623,plain,
! [X0] : true = ifeq(true,true,theorem(or(X0,not(X0))),true),
inference(superposition,[],[f140,f604]) ).
fof(f629,plain,
! [X0] : true = theorem(or(X0,not(X0))),
inference(forward_demodulation,[],[f623,f1]) ).
fof(f656,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X0,X1))),true),
inference(superposition,[],[f490,f125]) ).
fof(f688,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X0,X1))),
inference(forward_demodulation,[],[f656,f1]) ).
fof(f691,plain,
( true = theorem(or(p,sF2))
| ~ spl14_3 ),
inference(superposition,[],[f629,f72]) ).
fof(f698,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),true),
inference(superposition,[],[f355,f629]) ).
fof(f710,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),
inference(forward_demodulation,[],[f698,f1]) ).
fof(f716,plain,
( ! [X0] : true = ifeq(theorem(sF9),true,theorem(or(sF8,or(X0,sF0))),true)
| ~ spl14_11 ),
inference(superposition,[],[f516,f204]) ).
fof(f725,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),or(X1,X0))),true),
inference(superposition,[],[f516,f123]) ).
fof(f729,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF5)),true,theorem(or(X0,sF6)),true)
| ~ spl14_10 ),
inference(superposition,[],[f516,f183]) ).
fof(f747,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X0)),or(X1,X0))),
inference(forward_demodulation,[],[f725,f1]) ).
fof(f777,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF6)),true,theorem(or(not(or(sF7,X1)),or(X0,X1))),true)
| ~ spl14_9 ),
inference(superposition,[],[f458,f114]) ).
fof(f835,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f490,f710]) ).
fof(f854,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f835,f1]) ).
fof(f888,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f355,f688]) ).
fof(f916,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f888,f1]) ).
fof(f961,plain,
( true = ifeq(theorem(or(sF12,sF12)),true,sF13,true)
| ~ spl14_1 ),
inference(superposition,[],[f178,f60]) ).
fof(f992,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X1,X2))),true),true),
inference(superposition,[],[f26,f916]) ).
fof(f1016,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f992,f1]) ).
fof(f1041,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),or(X0,X1))),true),
inference(superposition,[],[f1016,f123]) ).
fof(f1047,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF2)),true,theorem(or(X0,sF3)),true)
| ~ spl14_15 ),
inference(superposition,[],[f1016,f282]) ).
fof(f1069,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X0)),or(X0,X1))),
inference(forward_demodulation,[],[f1041,f1]) ).
fof(f1157,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),true),
inference(superposition,[],[f26,f854]) ).
fof(f1184,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),
inference(forward_demodulation,[],[f1157,f1]) ).
fof(f1326,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF9)),true,theorem(or(not(sF10),X0)),true)
| ~ spl14_8 ),
inference(superposition,[],[f1184,f105]) ).
fof(f1553,definition,
( spl14_18
<=> true = theorem(or(p,sF2)) ),
introduced(definition,[new_symbols(definition,[spl14_18])],[avatar_definition]) ).
fof(f1555,plain,
( true = theorem(or(p,sF2))
| ~ spl14_18 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1556,plain,
( spl14_18
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f691,f70,f1553]) ).
fof(f1602,plain,
( true = ifeq(true,true,theorem(or(p,sF3)),true)
| ~ spl14_15
| ~ spl14_18 ),
inference(superposition,[],[f1047,f1555]) ).
fof(f1606,plain,
( true = theorem(or(p,sF3))
| ~ spl14_15
| ~ spl14_18 ),
inference(forward_demodulation,[],[f1602,f1]) ).
fof(f1610,definition,
( spl14_19
<=> true = theorem(or(p,sF3)) ),
introduced(definition,[new_symbols(definition,[spl14_19])],[avatar_definition]) ).
fof(f1612,plain,
( true = theorem(or(p,sF3))
| ~ spl14_19 ),
inference(avatar_component_clause,[],[f1610]) ).
fof(f1613,plain,
( spl14_19
| ~ spl14_15
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f1606,f1553,f280,f1610]) ).
fof(f1618,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF3),X0)),or(p,X0))),true)
| ~ spl14_19 ),
inference(superposition,[],[f458,f1612]) ).
fof(f1633,plain,
( ! [X0] : true = theorem(or(not(or(not(sF3),X0)),or(p,X0)))
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1618,f1]) ).
fof(f1637,plain,
( ! [X0] : true = theorem(or(not(or(sF4,X0)),or(p,X0)))
| ~ spl14_6
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1633,f93]) ).
fof(f1667,plain,
( true = theorem(or(not(or(sF4,q)),sF0))
| ~ spl14_6
| ~ spl14_12
| ~ spl14_19 ),
inference(superposition,[],[f1637,f225]) ).
fof(f1702,plain,
( true = theorem(or(not(sF5),sF0))
| ~ spl14_6
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1667,f244]) ).
fof(f1704,plain,
( true = theorem(or(sF8,sF0))
| ~ spl14_5
| ~ spl14_6
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1702,f86]) ).
fof(f1706,plain,
( true = theorem(sF9)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1704,f204]) ).
fof(f1712,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF8,or(X0,sF0))),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(backward_demodulation,[],[f716,f1706]) ).
fof(f1721,plain,
( ! [X0] : true = theorem(or(sF8,or(X0,sF0)))
| ~ spl14_5
| ~ spl14_6
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1712,f1]) ).
fof(f1725,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF9)),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(backward_demodulation,[],[f217,f1721]) ).
fof(f1726,plain,
( ! [X0] : true = theorem(or(X0,sF9))
| ~ spl14_5
| ~ spl14_6
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1725,f1]) ).
fof(f1732,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(sF10),X0)),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(backward_demodulation,[],[f1326,f1726]) ).
fof(f1737,plain,
( ! [X0] : true = theorem(or(not(sF10),X0))
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1732,f1]) ).
fof(f1832,plain,
( ! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,sF10)),or(X1,X0))),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(superposition,[],[f355,f1737]) ).
fof(f1883,plain,
( ! [X0,X1] : true = theorem(or(not(or(X1,sF10)),or(X1,X0)))
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1832,f1]) ).
fof(f1969,plain,
( ! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,sF10)),true,theorem(or(X0,X1)),true),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(superposition,[],[f26,f1883]) ).
fof(f2002,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF10)),true,theorem(or(X0,X1)),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19 ),
inference(forward_demodulation,[],[f1969,f1]) ).
fof(f2680,plain,
( true = ifeq(theorem(or(sF4,sF3)),true,theorem(or(sF2,sF5)),true)
| ~ spl14_13
| ~ spl14_15 ),
inference(superposition,[],[f257,f282]) ).
fof(f2691,plain,
( true = ifeq(true,true,theorem(or(sF2,sF5)),true)
| ~ spl14_6
| ~ spl14_13
| ~ spl14_15 ),
inference(forward_demodulation,[],[f2680,f610]) ).
fof(f2692,plain,
( true = theorem(or(sF2,sF5))
| ~ spl14_6
| ~ spl14_13
| ~ spl14_15 ),
inference(forward_demodulation,[],[f2691,f1]) ).
fof(f2698,definition,
( spl14_24
<=> true = theorem(or(sF2,sF5)) ),
introduced(definition,[new_symbols(definition,[spl14_24])],[avatar_definition]) ).
fof(f2700,plain,
( true = theorem(or(sF2,sF5))
| ~ spl14_24 ),
inference(avatar_component_clause,[],[f2698]) ).
fof(f2701,plain,
( spl14_24
| ~ spl14_6
| ~ spl14_13
| ~ spl14_15 ),
inference(avatar_split_clause,[],[f2692,f280,f242,f91,f2698]) ).
fof(f2707,plain,
( true = ifeq(true,true,theorem(or(sF2,sF6)),true)
| ~ spl14_10
| ~ spl14_24 ),
inference(superposition,[],[f729,f2700]) ).
fof(f2734,plain,
( true = theorem(or(sF2,sF6))
| ~ spl14_10
| ~ spl14_24 ),
inference(forward_demodulation,[],[f2707,f1]) ).
fof(f2783,definition,
( spl14_25
<=> true = theorem(or(sF2,sF6)) ),
introduced(definition,[new_symbols(definition,[spl14_25])],[avatar_definition]) ).
fof(f2785,plain,
( true = theorem(or(sF2,sF6))
| ~ spl14_25 ),
inference(avatar_component_clause,[],[f2783]) ).
fof(f2786,plain,
( spl14_25
| ~ spl14_10
| ~ spl14_24 ),
inference(avatar_split_clause,[],[f2734,f2698,f181,f2783]) ).
fof(f3311,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,X0))),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f355,f1069]) ).
fof(f3349,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,X0))),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f3311,f1]) ).
fof(f3421,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,or(X1,X2))),true),true),
inference(superposition,[],[f26,f3349]) ).
fof(f3458,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f3421,f1]) ).
fof(f3612,plain,
( true = theorem(or(not(sF0),or(p,sF5)))
| ~ spl14_12
| ~ spl14_13 ),
inference(superposition,[],[f503,f225]) ).
fof(f3661,plain,
( true = theorem(or(sF1,or(p,sF5)))
| ~ spl14_4
| ~ spl14_12
| ~ spl14_13 ),
inference(forward_demodulation,[],[f3612,f79]) ).
fof(f3663,definition,
( spl14_31
<=> true = theorem(or(sF1,or(p,sF5))) ),
introduced(definition,[new_symbols(definition,[spl14_31])],[avatar_definition]) ).
fof(f3665,plain,
( true = theorem(or(sF1,or(p,sF5)))
| ~ spl14_31 ),
inference(avatar_component_clause,[],[f3663]) ).
fof(f3666,plain,
( spl14_31
| ~ spl14_4
| ~ spl14_12
| ~ spl14_13 ),
inference(avatar_split_clause,[],[f3661,f242,f223,f77,f3663]) ).
fof(f3672,plain,
( true = ifeq(true,true,theorem(or(p,or(sF1,sF5))),true)
| ~ spl14_31 ),
inference(superposition,[],[f133,f3665]) ).
fof(f3706,plain,
( true = theorem(or(p,or(sF1,sF5)))
| ~ spl14_31 ),
inference(forward_demodulation,[],[f3672,f1]) ).
fof(f3711,plain,
( true = theorem(or(p,sF6))
| ~ spl14_10
| ~ spl14_31 ),
inference(forward_demodulation,[],[f3706,f183]) ).
fof(f3713,definition,
( spl14_32
<=> true = theorem(or(p,sF6)) ),
introduced(definition,[new_symbols(definition,[spl14_32])],[avatar_definition]) ).
fof(f3715,plain,
( true = theorem(or(p,sF6))
| ~ spl14_32 ),
inference(avatar_component_clause,[],[f3713]) ).
fof(f3716,plain,
( spl14_32
| ~ spl14_10
| ~ spl14_31 ),
inference(avatar_split_clause,[],[f3711,f3663,f181,f3713]) ).
fof(f3720,plain,
( true = ifeq(true,true,theorem(or(sF6,p)),true)
| ~ spl14_32 ),
inference(superposition,[],[f140,f3715]) ).
fof(f3745,plain,
( true = theorem(or(sF6,p))
| ~ spl14_32 ),
inference(forward_demodulation,[],[f3720,f1]) ).
fof(f3814,definition,
( spl14_33
<=> true = theorem(or(sF6,p)) ),
introduced(definition,[new_symbols(definition,[spl14_33])],[avatar_definition]) ).
fof(f3816,plain,
( true = theorem(or(sF6,p))
| ~ spl14_33 ),
inference(avatar_component_clause,[],[f3814]) ).
fof(f3817,plain,
( spl14_33
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f3745,f3713,f3814]) ).
fof(f3822,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(p),X0)),or(sF6,X0))),true)
| ~ spl14_33 ),
inference(superposition,[],[f458,f3816]) ).
fof(f3843,plain,
( ! [X0] : true = theorem(or(not(or(not(p),X0)),or(sF6,X0)))
| ~ spl14_33 ),
inference(forward_demodulation,[],[f3822,f1]) ).
fof(f3848,plain,
( ! [X0] : true = theorem(or(not(or(sF2,X0)),or(sF6,X0)))
| ~ spl14_3
| ~ spl14_33 ),
inference(forward_demodulation,[],[f3843,f72]) ).
fof(f3991,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF2,X0)),true,theorem(or(sF6,X0)),true),true)
| ~ spl14_3
| ~ spl14_33 ),
inference(superposition,[],[f26,f3848]) ).
fof(f4031,plain,
( ! [X0] : true = ifeq(theorem(or(sF2,X0)),true,theorem(or(sF6,X0)),true)
| ~ spl14_3
| ~ spl14_33 ),
inference(forward_demodulation,[],[f3991,f1]) ).
fof(f4038,plain,
( true = ifeq(true,true,theorem(or(sF6,sF6)),true)
| ~ spl14_3
| ~ spl14_25
| ~ spl14_33 ),
inference(superposition,[],[f4031,f2785]) ).
fof(f4053,plain,
( true = theorem(or(sF6,sF6))
| ~ spl14_3
| ~ spl14_25
| ~ spl14_33 ),
inference(forward_demodulation,[],[f4038,f1]) ).
fof(f4731,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X0)),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f747]) ).
fof(f4771,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X0)),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f4731,f1]) ).
fof(f6180,definition,
( spl14_50
<=> true = theorem(or(sF6,sF6)) ),
introduced(definition,[new_symbols(definition,[spl14_50])],[avatar_definition]) ).
fof(f6182,plain,
( true = theorem(or(sF6,sF6))
| ~ spl14_50 ),
inference(avatar_component_clause,[],[f6180]) ).
fof(f6183,plain,
( spl14_50
| ~ spl14_3
| ~ spl14_25
| ~ spl14_33 ),
inference(avatar_split_clause,[],[f4053,f3814,f2783,f70,f6180]) ).
fof(f6188,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF6)),true)
| ~ spl14_50 ),
inference(superposition,[],[f4771,f6182]) ).
fof(f6220,plain,
( ! [X0] : true = theorem(or(X0,sF6))
| ~ spl14_50 ),
inference(forward_demodulation,[],[f6188,f1]) ).
fof(f6252,plain,
( ! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(sF7,X1)),or(X0,X1))),true)
| ~ spl14_9
| ~ spl14_50 ),
inference(backward_demodulation,[],[f777,f6220]) ).
fof(f6281,plain,
( ! [X0,X1] : true = theorem(or(not(or(sF7,X1)),or(X0,X1)))
| ~ spl14_9
| ~ spl14_50 ),
inference(forward_demodulation,[],[f6252,f1]) ).
fof(f6312,plain,
( ! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(sF7,X0)),or(X0,X1))),true)
| ~ spl14_9
| ~ spl14_50 ),
inference(superposition,[],[f3458,f6281]) ).
fof(f6346,plain,
( ! [X0,X1] : true = theorem(or(not(or(sF7,X0)),or(X0,X1)))
| ~ spl14_9
| ~ spl14_50 ),
inference(forward_demodulation,[],[f6312,f1]) ).
fof(f7293,plain,
( ! [X0] : true = theorem(or(not(sF11),or(sF10,X0)))
| ~ spl14_9
| ~ spl14_14
| ~ spl14_50 ),
inference(superposition,[],[f6346,f263]) ).
fof(f7358,plain,
( ! [X0] : true = theorem(or(sF12,or(sF10,X0)))
| ~ spl14_7
| ~ spl14_9
| ~ spl14_14
| ~ spl14_50 ),
inference(forward_demodulation,[],[f7293,f100]) ).
fof(f7757,plain,
( true = ifeq(true,true,theorem(or(sF12,sF10)),true)
| ~ spl14_7
| ~ spl14_9
| ~ spl14_14
| ~ spl14_50 ),
inference(superposition,[],[f424,f7358]) ).
fof(f7793,plain,
( true = theorem(or(sF12,sF10))
| ~ spl14_7
| ~ spl14_9
| ~ spl14_14
| ~ spl14_50 ),
inference(forward_demodulation,[],[f7757,f1]) ).
fof(f7800,definition,
( spl14_54
<=> true = theorem(or(sF12,sF10)) ),
introduced(definition,[new_symbols(definition,[spl14_54])],[avatar_definition]) ).
fof(f7802,plain,
( true = theorem(or(sF12,sF10))
| ~ spl14_54 ),
inference(avatar_component_clause,[],[f7800]) ).
fof(f7803,plain,
( spl14_54
| ~ spl14_7
| ~ spl14_9
| ~ spl14_14
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f7793,f6180,f261,f112,f98,f7800]) ).
fof(f7805,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF12,X0)),true)
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(superposition,[],[f2002,f7802]) ).
fof(f7838,plain,
( ! [X0] : true = theorem(or(sF12,X0))
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(forward_demodulation,[],[f7805,f1]) ).
fof(f7849,plain,
( true = ifeq(true,true,sF13,true)
| ~ spl14_1
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(backward_demodulation,[],[f961,f7838]) ).
fof(f7852,plain,
( true = sF13
| ~ spl14_1
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(forward_demodulation,[],[f7849,f1]) ).
fof(f7863,plain,
( $false
| ~ spl14_1
| spl14_2
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(forward_subsumption_resolution,[],[f7852,f65]) ).
fof(f7864,plain,
( ~ spl14_1
| spl14_2
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(avatar_contradiction_clause,[],[f7863]) ).
cnf(s1,plain,
spl14_1,
inference(sat_conversion,[],[f61]) ).
cnf(s2,plain,
~ spl14_2,
inference(sat_conversion,[],[f66]) ).
cnf(s3,plain,
spl14_3,
inference(sat_conversion,[],[f73]) ).
cnf(s4,plain,
spl14_4,
inference(sat_conversion,[],[f80]) ).
cnf(s5,plain,
spl14_5,
inference(sat_conversion,[],[f87]) ).
cnf(s6,plain,
spl14_6,
inference(sat_conversion,[],[f94]) ).
cnf(s7,plain,
spl14_7,
inference(sat_conversion,[],[f101]) ).
cnf(s8,plain,
spl14_8,
inference(sat_conversion,[],[f106]) ).
cnf(s9,plain,
spl14_9,
inference(sat_conversion,[],[f115]) ).
cnf(s10,plain,
spl14_10,
inference(sat_conversion,[],[f184]) ).
cnf(s11,plain,
spl14_11,
inference(sat_conversion,[],[f205]) ).
cnf(s12,plain,
spl14_12,
inference(sat_conversion,[],[f226]) ).
cnf(s13,plain,
spl14_13,
inference(sat_conversion,[],[f245]) ).
cnf(s14,plain,
spl14_14,
inference(sat_conversion,[],[f264]) ).
cnf(s15,plain,
spl14_15,
inference(sat_conversion,[],[f283]) ).
cnf(s18,plain,
( ~ spl14_3
| spl14_18 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s19,plain,
( ~ spl14_15
| ~ spl14_18
| spl14_19 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s24,plain,
( ~ spl14_6
| ~ spl14_13
| ~ spl14_15
| spl14_24 ),
inference(sat_conversion,[],[f2701]) ).
cnf(s25,plain,
( ~ spl14_10
| ~ spl14_24
| spl14_25 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s31,plain,
( ~ spl14_4
| ~ spl14_12
| ~ spl14_13
| spl14_31 ),
inference(sat_conversion,[],[f3666]) ).
cnf(s32,plain,
( ~ spl14_10
| ~ spl14_31
| spl14_32 ),
inference(sat_conversion,[],[f3716]) ).
cnf(s33,plain,
( ~ spl14_32
| spl14_33 ),
inference(sat_conversion,[],[f3817]) ).
cnf(s50,plain,
( ~ spl14_3
| ~ spl14_25
| ~ spl14_33
| spl14_50 ),
inference(sat_conversion,[],[f6183]) ).
cnf(s54,plain,
( ~ spl14_7
| ~ spl14_9
| ~ spl14_14
| ~ spl14_50
| spl14_54 ),
inference(sat_conversion,[],[f7803]) ).
cnf(s57,plain,
( ~ spl14_1
| spl14_2
| ~ spl14_5
| ~ spl14_6
| ~ spl14_8
| ~ spl14_11
| ~ spl14_12
| ~ spl14_13
| ~ spl14_19
| ~ spl14_54 ),
inference(sat_conversion,[],[f7864]) ).
cnf(s61,plain,
spl14_24,
inference(rat,[],[s24,s13,s15,s6]) ).
cnf(s63,plain,
spl14_25,
inference(rat,[],[s25,s10,s61]) ).
cnf(s71,plain,
spl14_31,
inference(rat,[],[s31,s12,s13,s4]) ).
cnf(s73,plain,
spl14_32,
inference(rat,[],[s32,s10,s71]) ).
cnf(s75,plain,
spl14_33,
inference(rat,[],[s33,s73]) ).
cnf(s78,plain,
spl14_50,
inference(rat,[],[s50,s75,s63,s3]) ).
cnf(s81,plain,
spl14_18,
inference(rat,[],[s18,s3]) ).
cnf(s86,plain,
spl14_54,
inference(rat,[],[s54,s7,s9,s14,s78]) ).
cnf(s87,plain,
spl14_19,
inference(rat,[],[s19,s15,s81]) ).
cnf(s97,plain,
~ spl14_1,
inference(rat,[],[s57,s86,s87,s13,s12,s11,s8,s6,s5,s2]) ).
cnf(s98,plain,
$false,
inference(rat,[],[s1,s97]) ).
fof(f7865,plain,
$false,
inference(avatar_sat_refutation,[],[s98]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL330-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n007.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 15:32:56 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44 Running first-order theorem proving
% 0.12/0.44 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
% 16.02/3.62 % (1598327)Detected a unit-equality problem, will run specialized UEQ schedule.
% 16.02/3.62 % (1598353)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1871723473:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 16.02/3.62 % (1598354)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=245633242:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 16.02/3.62 % (1598352)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=2677408879:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 16.02/3.62 % (1598356)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=68137603:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 16.02/3.62 % (1598358)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=270502806:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 16.02/3.62 % (1598357)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2586206347:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 16.02/3.62 % (1598359)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1524749824:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 16.02/3.62 % (1598356)Instruction limit reached!
% 16.02/3.62 % (1598356)------------------------------
% 16.02/3.62 % (1598356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598356)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598356)Termination reason: Instruction limit
% 16.02/3.62 % (1598356)Termination phase: Saturation
% 16.02/3.62 % (1598356)Time elapsed: 0.131 s
% 16.02/3.62 % (1598356)Peak memory usage: 89 MB
% 16.02/3.62 % (1598356)Instructions burned: 136 (million)
% 16.02/3.62 % (1598357)Instruction limit reached!
% 16.02/3.62 % (1598357)------------------------------
% 16.02/3.62 % (1598357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598357)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598357)Termination reason: Instruction limit
% 16.02/3.62 % (1598357)Termination phase: Saturation
% 16.02/3.62 % (1598357)Time elapsed: 0.178 s
% 16.02/3.62 % (1598357)Peak memory usage: 89 MB
% 16.02/3.62 % (1598357)Instructions burned: 181 (million)
% 16.02/3.62 % (1598358)Instruction limit reached!
% 16.02/3.62 % (1598358)------------------------------
% 16.02/3.62 % (1598358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598358)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598358)Termination reason: Instruction limit
% 16.02/3.62 % (1598358)Termination phase: Saturation
% 16.02/3.62 % (1598358)Time elapsed: 0.196 s
% 16.02/3.62 % (1598358)Peak memory usage: 91 MB
% 16.02/3.62 % (1598358)Instructions burned: 258 (million)
% 16.02/3.62 % (1598373)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3900121218:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 16.02/3.62 % (1598374)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=269777985:i=4948:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/4948Mi)
% 16.02/3.62 % (1598375)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=797306591:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 16.02/3.62 % (1598375)Instruction limit reached!
% 16.02/3.62 % (1598375)------------------------------
% 16.02/3.62 % (1598375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598375)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598375)Termination reason: Instruction limit
% 16.02/3.62 % (1598375)Termination phase: Saturation
% 16.02/3.62 % (1598375)Time elapsed: 0.181 s
% 16.02/3.62 % (1598375)Peak memory usage: 88 MB
% 16.02/3.62 % (1598375)Instructions burned: 215 (million)
% 16.02/3.62 % (1598385)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=495876053:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2991 on theBenchmark for (2991ds/317Mi)
% 16.02/3.62 % (1598385)Instruction limit reached!
% 16.02/3.62 % (1598385)------------------------------
% 16.02/3.62 % (1598385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598385)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598385)Termination reason: Instruction limit
% 16.02/3.62 % (1598385)Termination phase: Saturation
% 16.02/3.62 % (1598385)Time elapsed: 0.314 s
% 16.02/3.62 % (1598385)Peak memory usage: 94 MB
% 16.02/3.62 % (1598385)Instructions burned: 317 (million)
% 16.02/3.62 % (1598359)Instruction limit reached!
% 16.02/3.62 % (1598359)------------------------------
% 16.02/3.62 % (1598359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598359)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598359)Termination reason: Instruction limit
% 16.02/3.62 % (1598359)Termination phase: Saturation
% 16.02/3.62 % (1598359)Time elapsed: 1.125 s
% 16.02/3.62 % (1598359)Peak memory usage: 101 MB
% 16.02/3.62 % (1598359)Instructions burned: 1187 (million)
% 16.02/3.62 % (1598391)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=3857749380:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2986 on theBenchmark for (2986ds/12125Mi)
% 16.02/3.62 % (1598394)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2200747068:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2986 on theBenchmark for (2986ds/2836Mi)
% 16.02/3.62 % (1598373)Instruction limit reached!
% 16.02/3.62 % (1598373)------------------------------
% 16.02/3.62 % (1598373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.02/3.62 % (1598373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.02/3.62 % (1598373)CaDiCaL version: 2.1.3
% 16.02/3.62 % (1598373)Termination reason: Instruction limit
% 16.02/3.62 % (1598373)Termination phase: Saturation
% 16.02/3.62 % (1598373)Time elapsed: 1.681 s
% 16.02/3.62 % (1598373)Peak memory usage: 143 MB
% 16.02/3.62 % (1598373)Instructions burned: 2052 (million)
% 16.02/3.62 % (1598491)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=328653251:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2978 on theBenchmark for (2978ds/14534Mi)
% 16.02/3.62 % (1598352)First to succeed.
% 16.02/3.62 % (1598352)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1598327"
% 16.02/3.62 % (1598352)Refutation found. Thanks to Tanya!
% 16.02/3.62 % SZS status Unsatisfiable for theBenchmark
% 16.02/3.62 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/3.80 % (1598352)------------------------------
% 0.20/3.80 % (1598352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/3.80 % (1598352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/3.80 % (1598352)CaDiCaL version: 2.1.3
% 0.20/3.80 % (1598352)Termination reason: Refutation
% 0.20/3.80 % (1598352)Time elapsed: 2.180 s
% 0.20/3.80 % (1598352)Peak memory usage: 145 MB
% 0.20/3.80 % (1598352)Instructions burned: 2530 (million)
% 0.20/3.80 % (1598352)------------------------------
% 0.20/3.80 % (1598352)------------------------------
% 0.20/3.80 % (1598327)Success in time 2.648 s
% 0.20/3.80 % Vampire exiting
%------------------------------------------------------------------------------