%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL348-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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:52:03 AM UTC 2026
% Result : Unsatisfiable 13.63s 2.79s
% Output : Refutation 14.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 55
% Syntax : Number of formulae : 309 ( 152 unt; 43 def)
% Number of atoms : 640 ( 234 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 640 ( 309 ~; 303 |; 0 &)
% ( 28 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 30 ( 28 usr; 29 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 18 con; 0-4 aty)
% Number of variables : 204 ( 0 sgn 204 !; 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(and(p,q),not(q)),or(p,not(q)))) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f19,plain,
true != theorem(equivalent(or(and(p,q),not(q)),or(p,not(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(not(or(not(p),not(q))),not(q))),or(p,not(q)))),not(or(not(or(p,not(q))),or(not(or(not(p),not(q))),not(q))))))),
inference(definition_unfolding,[],[f19,f20,f16]) ).
fof(f28,definition,
sF0 = not(p),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f29,plain,
not(p) = sF0,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF1 = not(q),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f31,plain,
not(q) = sF1,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF2 = or(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f33,plain,
or(sF0,sF1) = sF2,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF3 = not(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f35,plain,
not(sF2) = sF3,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF4 = or(sF3,sF1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f37,plain,
or(sF3,sF1) = sF4,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF5 = not(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f39,plain,
not(sF4) = sF5,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF6 = or(p,sF1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f41,plain,
or(p,sF1) = sF6,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF7 = or(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f43,plain,
or(sF5,sF6) = sF7,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF8 = not(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f45,plain,
not(sF7) = sF8,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF9 = not(sF6),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f47,plain,
not(sF6) = sF9,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF10 = or(sF9,sF4),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f49,plain,
or(sF9,sF4) = sF10,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF11 = not(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f51,plain,
not(sF10) = sF11,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF12 = or(sF8,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f53,plain,
or(sF8,sF11) = sF12,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF13 = not(sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f55,plain,
not(sF12) = sF13,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF14 = theorem(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f57,plain,
theorem(sF13) = sF14,
inference(reorient_equations,[],[f56]) ).
fof(f58,plain,
true != sF14,
inference(definition_folding,[],[f27,f57,f55,f53,f51,f49,f37,f31,f35,f33,f31,f29,f47,f41,f31,f45,f43,f41,f31,f39,f37,f31,f35,f33,f31,f29]) ).
fof(f60,definition,
( spl15_1
<=> theorem(sF13) = sF14 ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
fof(f62,plain,
( theorem(sF13) = sF14
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f60]) ).
fof(f63,plain,
spl15_1,
inference(avatar_split_clause,[],[f57,f60]) ).
fof(f65,plain,
( ! [X0] : true = ifeq(theorem(or(not(X0),sF13)),true,ifeq(theorem(X0),true,sF14,true),true)
| ~ spl15_1 ),
inference(superposition,[],[f26,f62]) ).
fof(f67,definition,
( spl15_2
<=> true = sF14 ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
fof(f69,plain,
( true != sF14
| spl15_2 ),
inference(avatar_component_clause,[],[f67]) ).
fof(f70,plain,
~ spl15_2,
inference(avatar_split_clause,[],[f58,f67]) ).
fof(f79,definition,
( spl15_4
<=> not(p) = sF0 ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
fof(f81,plain,
( not(p) = sF0
| ~ spl15_4 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f82,plain,
spl15_4,
inference(avatar_split_clause,[],[f29,f79]) ).
fof(f86,definition,
( spl15_5
<=> not(sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
fof(f88,plain,
( not(sF4) = sF5
| ~ spl15_5 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f89,plain,
spl15_5,
inference(avatar_split_clause,[],[f39,f86]) ).
fof(f91,definition,
( spl15_6
<=> not(sF6) = sF9 ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
fof(f93,plain,
( not(sF6) = sF9
| ~ spl15_6 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f94,plain,
spl15_6,
inference(avatar_split_clause,[],[f47,f91]) ).
fof(f100,definition,
( spl15_7
<=> not(sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition]) ).
fof(f102,plain,
( not(sF2) = sF3
| ~ spl15_7 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,plain,
spl15_7,
inference(avatar_split_clause,[],[f35,f100]) ).
fof(f107,definition,
( spl15_8
<=> not(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition]) ).
fof(f109,plain,
( not(sF10) = sF11
| ~ spl15_8 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f110,plain,
spl15_8,
inference(avatar_split_clause,[],[f51,f107]) ).
fof(f114,definition,
( spl15_9
<=> not(sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition]) ).
fof(f116,plain,
( not(sF12) = sF13
| ~ spl15_9 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f117,plain,
spl15_9,
inference(avatar_split_clause,[],[f55,f114]) ).
fof(f119,definition,
( spl15_10
<=> not(sF7) = sF8 ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
fof(f121,plain,
( not(sF7) = sF8
| ~ spl15_10 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f122,plain,
spl15_10,
inference(avatar_split_clause,[],[f45,f119]) ).
fof(f127,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(X1,X0))),true),
inference(superposition,[],[f13,f23]) ).
fof(f128,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X1,X0))),true),
inference(superposition,[],[f13,f22]) ).
fof(f129,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(f130,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),X0)),true),
inference(superposition,[],[f13,f21]) ).
fof(f132,plain,
! [X0] : true = theorem(or(not(or(X0,X0)),X0)),
inference(forward_demodulation,[],[f130,f1]) ).
fof(f133,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(forward_demodulation,[],[f129,f1]) ).
fof(f134,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X1,X0))),
inference(forward_demodulation,[],[f128,f1]) ).
fof(f135,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(forward_demodulation,[],[f127,f1]) ).
fof(f136,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f135]) ).
fof(f142,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f136,f1]) ).
fof(f143,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,f133]) ).
fof(f149,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),
inference(forward_demodulation,[],[f143,f1]) ).
fof(f191,definition,
( spl15_11
<=> or(sF9,sF4) = sF10 ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
fof(f193,plain,
( or(sF9,sF4) = sF10
| ~ spl15_11 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,plain,
spl15_11,
inference(avatar_split_clause,[],[f49,f191]) ).
fof(f202,plain,
( true = theorem(or(not(sF4),sF10))
| ~ spl15_11 ),
inference(superposition,[],[f134,f193]) ).
fof(f208,plain,
( true = theorem(or(sF5,sF10))
| ~ spl15_5
| ~ spl15_11 ),
inference(forward_demodulation,[],[f202,f88]) ).
fof(f212,definition,
( spl15_12
<=> or(sF5,sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
fof(f214,plain,
( or(sF5,sF6) = sF7
| ~ spl15_12 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,plain,
spl15_12,
inference(avatar_split_clause,[],[f43,f212]) ).
fof(f227,plain,
( ! [X0] : true = ifeq(theorem(or(sF5,or(X0,sF6))),true,theorem(or(X0,sF7)),true)
| ~ spl15_12 ),
inference(superposition,[],[f149,f214]) ).
fof(f233,definition,
( spl15_13
<=> or(sF0,sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
fof(f235,plain,
( or(sF0,sF1) = sF2
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,plain,
spl15_13,
inference(avatar_split_clause,[],[f33,f233]) ).
fof(f252,definition,
( spl15_14
<=> or(p,sF1) = sF6 ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
fof(f254,plain,
( or(p,sF1) = sF6
| ~ spl15_14 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f255,plain,
spl15_14,
inference(avatar_split_clause,[],[f41,f252]) ).
fof(f271,definition,
( spl15_15
<=> or(sF8,sF11) = sF12 ),
introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition]) ).
fof(f273,plain,
( or(sF8,sF11) = sF12
| ~ spl15_15 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f274,plain,
spl15_15,
inference(avatar_split_clause,[],[f53,f271]) ).
fof(f307,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(f308,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(forward_demodulation,[],[f307,f1]) ).
fof(f317,definition,
( spl15_16
<=> or(sF3,sF1) = sF4 ),
introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition]) ).
fof(f319,plain,
( or(sF3,sF1) = sF4
| ~ spl15_16 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f320,plain,
spl15_16,
inference(avatar_split_clause,[],[f37,f317]) ).
fof(f358,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,f308]) ).
fof(f360,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,[],[f149,f308]) ).
fof(f366,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),
inference(forward_demodulation,[],[f360,f1]) ).
fof(f367,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,[],[f358,f1]) ).
fof(f385,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f367,f135]) ).
fof(f387,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f367,f134]) ).
fof(f389,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),true),
inference(superposition,[],[f367,f132]) ).
fof(f414,plain,
! [X0,X1] : true = theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),
inference(forward_demodulation,[],[f389,f1]) ).
fof(f416,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f387,f1]) ).
fof(f418,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f385,f1]) ).
fof(f443,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,f366]) ).
fof(f452,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,[],[f443,f1]) ).
fof(f470,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),true),
inference(superposition,[],[f26,f414]) ).
fof(f478,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),
inference(forward_demodulation,[],[f470,f1]) ).
fof(f490,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF1)),or(X0,sF4)))
| ~ spl15_16 ),
inference(superposition,[],[f416,f319]) ).
fof(f496,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,f416]) ).
fof(f504,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f496,f1]) ).
fof(f528,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,f418]) ).
fof(f536,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f528,f1]) ).
fof(f592,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(X0),X0)),true),
inference(superposition,[],[f478,f134]) ).
fof(f618,plain,
! [X0] : true = theorem(or(not(X0),X0)),
inference(forward_demodulation,[],[f592,f1]) ).
fof(f638,plain,
! [X0] : true = ifeq(true,true,theorem(or(X0,not(X0))),true),
inference(superposition,[],[f142,f618]) ).
fof(f644,plain,
! [X0] : true = theorem(or(X0,not(X0))),
inference(forward_demodulation,[],[f638,f1]) ).
fof(f671,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X0,X1))),true),
inference(superposition,[],[f536,f134]) ).
fof(f703,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X0,X1))),
inference(forward_demodulation,[],[f671,f1]) ).
fof(f706,plain,
( true = theorem(or(p,sF0))
| ~ spl15_4 ),
inference(superposition,[],[f644,f81]) ).
fof(f714,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),true),
inference(superposition,[],[f367,f644]) ).
fof(f726,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),
inference(forward_demodulation,[],[f714,f1]) ).
fof(f730,plain,
( ! [X0] : true = ifeq(theorem(sF7),true,theorem(or(sF5,or(X0,sF6))),true)
| ~ spl15_12 ),
inference(superposition,[],[f504,f214]) ).
fof(f792,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF4)),true,theorem(or(not(or(sF5,X1)),or(X0,X1))),true)
| ~ spl15_5 ),
inference(superposition,[],[f452,f88]) ).
fof(f794,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF7)),true,theorem(or(not(or(sF8,X1)),or(X0,X1))),true)
| ~ spl15_10 ),
inference(superposition,[],[f452,f121]) ).
fof(f848,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f367,f703]) ).
fof(f874,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f848,f1]) ).
fof(f895,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f536,f726]) ).
fof(f914,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f895,f1]) ).
fof(f998,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,f874]) ).
fof(f1022,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f998,f1]) ).
fof(f1052,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF0)),true,theorem(or(X0,sF2)),true)
| ~ spl15_13 ),
inference(superposition,[],[f1022,f235]) ).
fof(f1186,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),true),
inference(superposition,[],[f26,f914]) ).
fof(f1213,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),
inference(forward_demodulation,[],[f1186,f1]) ).
fof(f1450,definition,
( spl15_22
<=> true = theorem(or(p,sF0)) ),
introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition]) ).
fof(f1452,plain,
( true = theorem(or(p,sF0))
| ~ spl15_22 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1453,plain,
( spl15_22
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f706,f79,f1450]) ).
fof(f1777,plain,
( true = ifeq(true,true,theorem(or(p,sF2)),true)
| ~ spl15_13
| ~ spl15_22 ),
inference(superposition,[],[f1052,f1452]) ).
fof(f1782,plain,
( true = theorem(or(p,sF2))
| ~ spl15_13
| ~ spl15_22 ),
inference(forward_demodulation,[],[f1777,f1]) ).
fof(f1787,definition,
( spl15_26
<=> true = theorem(or(p,sF2)) ),
introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition]) ).
fof(f1789,plain,
( true = theorem(or(p,sF2))
| ~ spl15_26 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1790,plain,
( spl15_26
| ~ spl15_13
| ~ spl15_22 ),
inference(avatar_split_clause,[],[f1782,f1450,f233,f1787]) ).
fof(f1795,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF2),X0)),or(p,X0))),true)
| ~ spl15_26 ),
inference(superposition,[],[f452,f1789]) ).
fof(f1811,plain,
( ! [X0] : true = theorem(or(not(or(not(sF2),X0)),or(p,X0)))
| ~ spl15_26 ),
inference(forward_demodulation,[],[f1795,f1]) ).
fof(f1815,plain,
( ! [X0] : true = theorem(or(not(or(sF3,X0)),or(p,X0)))
| ~ spl15_7
| ~ spl15_26 ),
inference(forward_demodulation,[],[f1811,f102]) ).
fof(f1960,plain,
( true = theorem(or(not(or(sF3,sF1)),sF6))
| ~ spl15_7
| ~ spl15_14
| ~ spl15_26 ),
inference(superposition,[],[f1815,f254]) ).
fof(f1997,plain,
( true = theorem(or(not(sF4),sF6))
| ~ spl15_7
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f1960,f319]) ).
fof(f1999,plain,
( true = theorem(or(sF5,sF6))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f1997,f88]) ).
fof(f2001,plain,
( true = theorem(sF7)
| ~ spl15_5
| ~ spl15_7
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f1999,f214]) ).
fof(f2007,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF5,or(X0,sF6))),true)
| ~ spl15_5
| ~ spl15_7
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(backward_demodulation,[],[f730,f2001]) ).
fof(f2019,plain,
( ! [X0] : true = theorem(or(sF5,or(X0,sF6)))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f2007,f1]) ).
fof(f2023,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF7)),true)
| ~ spl15_5
| ~ spl15_7
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(backward_demodulation,[],[f227,f2019]) ).
fof(f2024,plain,
( ! [X0] : true = theorem(or(X0,sF7))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f2023,f1]) ).
fof(f2028,plain,
( ! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(sF8,X1)),or(X0,X1))),true)
| ~ spl15_5
| ~ spl15_7
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(backward_demodulation,[],[f794,f2024]) ).
fof(f2036,plain,
( ! [X0,X1] : true = theorem(or(not(or(sF8,X1)),or(X0,X1)))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f2028,f1]) ).
fof(f2067,plain,
( ! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(sF8,X0)),or(X0,X1))),true)
| ~ spl15_5
| ~ spl15_7
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(superposition,[],[f536,f2036]) ).
fof(f2095,plain,
( ! [X0,X1] : true = theorem(or(not(or(sF8,X0)),or(X0,X1)))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f2067,f1]) ).
fof(f2837,plain,
( true = theorem(or(not(sF6),or(p,sF4)))
| ~ spl15_14
| ~ spl15_16 ),
inference(superposition,[],[f490,f254]) ).
fof(f2882,plain,
( true = theorem(or(sF9,or(p,sF4)))
| ~ spl15_6
| ~ spl15_14
| ~ spl15_16 ),
inference(forward_demodulation,[],[f2837,f93]) ).
fof(f3049,definition,
( spl15_31
<=> true = theorem(or(sF5,sF10)) ),
introduced(definition,[new_symbols(definition,[spl15_31])],[avatar_definition]) ).
fof(f3051,plain,
( true = theorem(or(sF5,sF10))
| ~ spl15_31 ),
inference(avatar_component_clause,[],[f3049]) ).
fof(f3052,plain,
( spl15_31
| ~ spl15_5
| ~ spl15_11 ),
inference(avatar_split_clause,[],[f208,f191,f86,f3049]) ).
fof(f3065,plain,
( true = ifeq(true,true,theorem(or(not(not(sF10)),sF5)),true)
| ~ spl15_31 ),
inference(superposition,[],[f1213,f3051]) ).
fof(f3078,plain,
( true = theorem(or(not(not(sF10)),sF5))
| ~ spl15_31 ),
inference(forward_demodulation,[],[f3065,f1]) ).
fof(f3086,plain,
( true = theorem(or(not(sF11),sF5))
| ~ spl15_8
| ~ spl15_31 ),
inference(forward_demodulation,[],[f3078,f109]) ).
fof(f3437,plain,
( ! [X0] : true = theorem(or(not(sF12),or(sF11,X0)))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_15
| ~ spl15_16
| ~ spl15_26 ),
inference(superposition,[],[f2095,f273]) ).
fof(f3488,plain,
( ! [X0] : true = theorem(or(sF13,or(sF11,X0)))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_9
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_15
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f3437,f116]) ).
fof(f4174,definition,
( spl15_34
<=> true = theorem(or(sF9,or(p,sF4))) ),
introduced(definition,[new_symbols(definition,[spl15_34])],[avatar_definition]) ).
fof(f4176,plain,
( true = theorem(or(sF9,or(p,sF4)))
| ~ spl15_34 ),
inference(avatar_component_clause,[],[f4174]) ).
fof(f4177,plain,
( spl15_34
| ~ spl15_6
| ~ spl15_14
| ~ spl15_16 ),
inference(avatar_split_clause,[],[f2882,f317,f252,f91,f4174]) ).
fof(f4184,plain,
( true = ifeq(true,true,theorem(or(p,or(sF9,sF4))),true)
| ~ spl15_34 ),
inference(superposition,[],[f149,f4176]) ).
fof(f4221,plain,
( true = theorem(or(p,or(sF9,sF4)))
| ~ spl15_34 ),
inference(forward_demodulation,[],[f4184,f1]) ).
fof(f4227,plain,
( true = theorem(or(p,sF10))
| ~ spl15_11
| ~ spl15_34 ),
inference(forward_demodulation,[],[f4221,f193]) ).
fof(f4229,definition,
( spl15_35
<=> true = theorem(or(p,sF10)) ),
introduced(definition,[new_symbols(definition,[spl15_35])],[avatar_definition]) ).
fof(f4231,plain,
( true = theorem(or(p,sF10))
| ~ spl15_35 ),
inference(avatar_component_clause,[],[f4229]) ).
fof(f4232,plain,
( spl15_35
| ~ spl15_11
| ~ spl15_34 ),
inference(avatar_split_clause,[],[f4227,f4174,f191,f4229]) ).
fof(f4243,plain,
( true = ifeq(true,true,theorem(or(not(not(sF10)),p)),true)
| ~ spl15_35 ),
inference(superposition,[],[f1213,f4231]) ).
fof(f4258,plain,
( true = theorem(or(not(not(sF10)),p))
| ~ spl15_35 ),
inference(forward_demodulation,[],[f4243,f1]) ).
fof(f4264,plain,
( true = theorem(or(not(sF11),p))
| ~ spl15_8
| ~ spl15_35 ),
inference(forward_demodulation,[],[f4258,f109]) ).
fof(f4375,definition,
( spl15_37
<=> true = theorem(or(not(sF11),p)) ),
introduced(definition,[new_symbols(definition,[spl15_37])],[avatar_definition]) ).
fof(f4377,plain,
( true = theorem(or(not(sF11),p))
| ~ spl15_37 ),
inference(avatar_component_clause,[],[f4375]) ).
fof(f4378,plain,
( spl15_37
| ~ spl15_8
| ~ spl15_35 ),
inference(avatar_split_clause,[],[f4264,f4229,f107,f4375]) ).
fof(f4382,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF11)),or(X0,p))),true)
| ~ spl15_37 ),
inference(superposition,[],[f367,f4377]) ).
fof(f4415,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF11)),or(X0,p)))
| ~ spl15_37 ),
inference(forward_demodulation,[],[f4382,f1]) ).
fof(f4425,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF11)),true,theorem(or(X0,p)),true),true)
| ~ spl15_37 ),
inference(superposition,[],[f26,f4415]) ).
fof(f4470,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF11)),true,theorem(or(X0,p)),true)
| ~ spl15_37 ),
inference(forward_demodulation,[],[f4425,f1]) ).
fof(f5690,definition,
( spl15_47
<=> true = theorem(or(not(sF11),sF5)) ),
introduced(definition,[new_symbols(definition,[spl15_47])],[avatar_definition]) ).
fof(f5692,plain,
( true = theorem(or(not(sF11),sF5))
| ~ spl15_47 ),
inference(avatar_component_clause,[],[f5690]) ).
fof(f5693,plain,
( spl15_47
| ~ spl15_8
| ~ spl15_31 ),
inference(avatar_split_clause,[],[f3086,f3049,f107,f5690]) ).
fof(f5697,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF11)),or(X0,sF5))),true)
| ~ spl15_47 ),
inference(superposition,[],[f367,f5692]) ).
fof(f5729,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF11)),or(X0,sF5)))
| ~ spl15_47 ),
inference(forward_demodulation,[],[f5697,f1]) ).
fof(f5736,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF11)),true,theorem(or(X0,sF5)),true),true)
| ~ spl15_47 ),
inference(superposition,[],[f26,f5729]) ).
fof(f5781,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF11)),true,theorem(or(X0,sF5)),true)
| ~ spl15_47 ),
inference(forward_demodulation,[],[f5736,f1]) ).
fof(f5967,plain,
( true = ifeq(true,true,theorem(or(sF13,sF11)),true)
| ~ spl15_5
| ~ spl15_7
| ~ spl15_9
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_15
| ~ spl15_16
| ~ spl15_26 ),
inference(superposition,[],[f478,f3488]) ).
fof(f5996,plain,
( true = theorem(or(sF13,sF11))
| ~ spl15_5
| ~ spl15_7
| ~ spl15_9
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_15
| ~ spl15_16
| ~ spl15_26 ),
inference(forward_demodulation,[],[f5967,f1]) ).
fof(f6004,definition,
( spl15_49
<=> true = theorem(or(sF13,sF11)) ),
introduced(definition,[new_symbols(definition,[spl15_49])],[avatar_definition]) ).
fof(f6006,plain,
( true = theorem(or(sF13,sF11))
| ~ spl15_49 ),
inference(avatar_component_clause,[],[f6004]) ).
fof(f6007,plain,
( spl15_49
| ~ spl15_5
| ~ spl15_7
| ~ spl15_9
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_15
| ~ spl15_16
| ~ spl15_26 ),
inference(avatar_split_clause,[],[f5996,f1787,f317,f271,f252,f212,f119,f114,f100,f86,f6004]) ).
fof(f6010,plain,
( true = ifeq(true,true,theorem(or(sF13,sF5)),true)
| ~ spl15_47
| ~ spl15_49 ),
inference(superposition,[],[f5781,f6006]) ).
fof(f6011,plain,
( true = ifeq(true,true,theorem(or(sF13,p)),true)
| ~ spl15_37
| ~ spl15_49 ),
inference(superposition,[],[f4470,f6006]) ).
fof(f6042,plain,
( true = theorem(or(sF13,p))
| ~ spl15_37
| ~ spl15_49 ),
inference(forward_demodulation,[],[f6011,f1]) ).
fof(f6043,plain,
( true = theorem(or(sF13,sF5))
| ~ spl15_47
| ~ spl15_49 ),
inference(forward_demodulation,[],[f6010,f1]) ).
fof(f6049,definition,
( spl15_50
<=> true = theorem(or(sF13,p)) ),
introduced(definition,[new_symbols(definition,[spl15_50])],[avatar_definition]) ).
fof(f6051,plain,
( true = theorem(or(sF13,p))
| ~ spl15_50 ),
inference(avatar_component_clause,[],[f6049]) ).
fof(f6052,plain,
( spl15_50
| ~ spl15_37
| ~ spl15_49 ),
inference(avatar_split_clause,[],[f6042,f6004,f4375,f6049]) ).
fof(f6059,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(p),X0)),or(sF13,X0))),true)
| ~ spl15_50 ),
inference(superposition,[],[f452,f6051]) ).
fof(f6083,plain,
( ! [X0] : true = theorem(or(not(or(not(p),X0)),or(sF13,X0)))
| ~ spl15_50 ),
inference(forward_demodulation,[],[f6059,f1]) ).
fof(f6090,plain,
( ! [X0] : true = theorem(or(not(or(sF0,X0)),or(sF13,X0)))
| ~ spl15_4
| ~ spl15_50 ),
inference(forward_demodulation,[],[f6083,f81]) ).
fof(f6172,definition,
( spl15_53
<=> true = theorem(or(sF13,sF5)) ),
introduced(definition,[new_symbols(definition,[spl15_53])],[avatar_definition]) ).
fof(f6174,plain,
( true = theorem(or(sF13,sF5))
| ~ spl15_53 ),
inference(avatar_component_clause,[],[f6172]) ).
fof(f6175,plain,
( spl15_53
| ~ spl15_47
| ~ spl15_49 ),
inference(avatar_split_clause,[],[f6043,f6004,f5690,f6172]) ).
fof(f6180,plain,
( true = ifeq(true,true,theorem(or(sF5,sF13)),true)
| ~ spl15_53 ),
inference(superposition,[],[f142,f6174]) ).
fof(f6207,plain,
( true = theorem(or(sF5,sF13))
| ~ spl15_53 ),
inference(forward_demodulation,[],[f6180,f1]) ).
fof(f6213,definition,
( spl15_54
<=> true = theorem(or(sF5,sF13)) ),
introduced(definition,[new_symbols(definition,[spl15_54])],[avatar_definition]) ).
fof(f6215,plain,
( true = theorem(or(sF5,sF13))
| ~ spl15_54 ),
inference(avatar_component_clause,[],[f6213]) ).
fof(f6216,plain,
( spl15_54
| ~ spl15_53 ),
inference(avatar_split_clause,[],[f6207,f6172,f6213]) ).
fof(f6237,plain,
( true = ifeq(theorem(or(not(or(sF5,sF13)),sF13)),true,ifeq(true,true,sF14,true),true)
| ~ spl15_1
| ~ spl15_54 ),
inference(superposition,[],[f65,f6215]) ).
fof(f6244,plain,
( true = ifeq(theorem(or(not(or(sF5,sF13)),sF13)),true,sF14,true)
| ~ spl15_1
| ~ spl15_54 ),
inference(forward_demodulation,[],[f6237,f1]) ).
fof(f6366,plain,
( true = theorem(or(not(sF2),or(sF13,sF1)))
| ~ spl15_4
| ~ spl15_13
| ~ spl15_50 ),
inference(superposition,[],[f6090,f235]) ).
fof(f6418,plain,
( true = theorem(or(sF3,or(sF13,sF1)))
| ~ spl15_4
| ~ spl15_7
| ~ spl15_13
| ~ spl15_50 ),
inference(forward_demodulation,[],[f6366,f102]) ).
fof(f6680,definition,
( spl15_59
<=> true = theorem(or(sF3,or(sF13,sF1))) ),
introduced(definition,[new_symbols(definition,[spl15_59])],[avatar_definition]) ).
fof(f6682,plain,
( true = theorem(or(sF3,or(sF13,sF1)))
| ~ spl15_59 ),
inference(avatar_component_clause,[],[f6680]) ).
fof(f6683,plain,
( spl15_59
| ~ spl15_4
| ~ spl15_7
| ~ spl15_13
| ~ spl15_50 ),
inference(avatar_split_clause,[],[f6418,f6049,f233,f100,f79,f6680]) ).
fof(f6688,plain,
( true = ifeq(true,true,theorem(or(sF13,or(sF3,sF1))),true)
| ~ spl15_59 ),
inference(superposition,[],[f149,f6682]) ).
fof(f6725,plain,
( true = theorem(or(sF13,or(sF3,sF1)))
| ~ spl15_59 ),
inference(forward_demodulation,[],[f6688,f1]) ).
fof(f6730,plain,
( true = theorem(or(sF13,sF4))
| ~ spl15_16
| ~ spl15_59 ),
inference(forward_demodulation,[],[f6725,f319]) ).
fof(f6734,definition,
( spl15_60
<=> true = theorem(or(sF13,sF4)) ),
introduced(definition,[new_symbols(definition,[spl15_60])],[avatar_definition]) ).
fof(f6736,plain,
( true = theorem(or(sF13,sF4))
| ~ spl15_60 ),
inference(avatar_component_clause,[],[f6734]) ).
fof(f6737,plain,
( spl15_60
| ~ spl15_16
| ~ spl15_59 ),
inference(avatar_split_clause,[],[f6730,f6680,f317,f6734]) ).
fof(f6742,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF5,X0)),or(sF13,X0))),true)
| ~ spl15_5
| ~ spl15_60 ),
inference(superposition,[],[f792,f6736]) ).
fof(f6777,plain,
( ! [X0] : true = theorem(or(not(or(sF5,X0)),or(sF13,X0)))
| ~ spl15_5
| ~ spl15_60 ),
inference(forward_demodulation,[],[f6742,f1]) ).
fof(f6845,plain,
( true = ifeq(true,true,theorem(or(not(or(sF5,sF13)),sF13)),true)
| ~ spl15_5
| ~ spl15_60 ),
inference(superposition,[],[f478,f6777]) ).
fof(f6874,plain,
( true = theorem(or(not(or(sF5,sF13)),sF13))
| ~ spl15_5
| ~ spl15_60 ),
inference(forward_demodulation,[],[f6845,f1]) ).
fof(f6883,plain,
( true = ifeq(true,true,sF14,true)
| ~ spl15_1
| ~ spl15_5
| ~ spl15_54
| ~ spl15_60 ),
inference(backward_demodulation,[],[f6244,f6874]) ).
fof(f6884,plain,
( true = sF14
| ~ spl15_1
| ~ spl15_5
| ~ spl15_54
| ~ spl15_60 ),
inference(forward_demodulation,[],[f6883,f1]) ).
fof(f6885,plain,
( $false
| ~ spl15_1
| spl15_2
| ~ spl15_5
| ~ spl15_54
| ~ spl15_60 ),
inference(forward_subsumption_resolution,[],[f6884,f69]) ).
fof(f6886,plain,
( ~ spl15_1
| spl15_2
| ~ spl15_5
| ~ spl15_54
| ~ spl15_60 ),
inference(avatar_contradiction_clause,[],[f6885]) ).
cnf(s1,plain,
spl15_1,
inference(sat_conversion,[],[f63]) ).
cnf(s2,plain,
~ spl15_2,
inference(sat_conversion,[],[f70]) ).
cnf(s4,plain,
spl15_4,
inference(sat_conversion,[],[f82]) ).
cnf(s5,plain,
spl15_5,
inference(sat_conversion,[],[f89]) ).
cnf(s6,plain,
spl15_6,
inference(sat_conversion,[],[f94]) ).
cnf(s7,plain,
spl15_7,
inference(sat_conversion,[],[f103]) ).
cnf(s8,plain,
spl15_8,
inference(sat_conversion,[],[f110]) ).
cnf(s9,plain,
spl15_9,
inference(sat_conversion,[],[f117]) ).
cnf(s10,plain,
spl15_10,
inference(sat_conversion,[],[f122]) ).
cnf(s11,plain,
spl15_11,
inference(sat_conversion,[],[f194]) ).
cnf(s12,plain,
spl15_12,
inference(sat_conversion,[],[f215]) ).
cnf(s13,plain,
spl15_13,
inference(sat_conversion,[],[f236]) ).
cnf(s14,plain,
spl15_14,
inference(sat_conversion,[],[f255]) ).
cnf(s15,plain,
spl15_15,
inference(sat_conversion,[],[f274]) ).
cnf(s16,plain,
spl15_16,
inference(sat_conversion,[],[f320]) ).
cnf(s22,plain,
( ~ spl15_4
| spl15_22 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s26,plain,
( ~ spl15_13
| ~ spl15_22
| spl15_26 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s31,plain,
( ~ spl15_5
| ~ spl15_11
| spl15_31 ),
inference(sat_conversion,[],[f3052]) ).
cnf(s34,plain,
( ~ spl15_6
| ~ spl15_14
| ~ spl15_16
| spl15_34 ),
inference(sat_conversion,[],[f4177]) ).
cnf(s35,plain,
( ~ spl15_11
| ~ spl15_34
| spl15_35 ),
inference(sat_conversion,[],[f4232]) ).
cnf(s37,plain,
( ~ spl15_8
| ~ spl15_35
| spl15_37 ),
inference(sat_conversion,[],[f4378]) ).
cnf(s47,plain,
( ~ spl15_8
| ~ spl15_31
| spl15_47 ),
inference(sat_conversion,[],[f5693]) ).
cnf(s49,plain,
( ~ spl15_5
| ~ spl15_7
| ~ spl15_9
| ~ spl15_10
| ~ spl15_12
| ~ spl15_14
| ~ spl15_15
| ~ spl15_16
| ~ spl15_26
| spl15_49 ),
inference(sat_conversion,[],[f6007]) ).
cnf(s50,plain,
( ~ spl15_37
| ~ spl15_49
| spl15_50 ),
inference(sat_conversion,[],[f6052]) ).
cnf(s53,plain,
( ~ spl15_47
| ~ spl15_49
| spl15_53 ),
inference(sat_conversion,[],[f6175]) ).
cnf(s54,plain,
( ~ spl15_53
| spl15_54 ),
inference(sat_conversion,[],[f6216]) ).
cnf(s59,plain,
( ~ spl15_4
| ~ spl15_7
| ~ spl15_13
| ~ spl15_50
| spl15_59 ),
inference(sat_conversion,[],[f6683]) ).
cnf(s60,plain,
( ~ spl15_16
| ~ spl15_59
| spl15_60 ),
inference(sat_conversion,[],[f6737]) ).
cnf(s62,plain,
( ~ spl15_1
| spl15_2
| ~ spl15_5
| ~ spl15_54
| ~ spl15_60 ),
inference(sat_conversion,[],[f6886]) ).
cnf(s64,plain,
spl15_34,
inference(rat,[],[s34,s14,s16,s6]) ).
cnf(s65,plain,
spl15_35,
inference(rat,[],[s35,s11,s64]) ).
cnf(s66,plain,
spl15_37,
inference(rat,[],[s37,s8,s65]) ).
cnf(s70,plain,
spl15_31,
inference(rat,[],[s31,s11,s5]) ).
cnf(s71,plain,
spl15_47,
inference(rat,[],[s47,s8,s70]) ).
cnf(s73,plain,
spl15_22,
inference(rat,[],[s22,s4]) ).
cnf(s75,plain,
spl15_26,
inference(rat,[],[s26,s13,s73]) ).
cnf(s79,plain,
spl15_49,
inference(rat,[],[s49,s5,s7,s16,s15,s14,s12,s10,s9,s75]) ).
cnf(s86,plain,
spl15_53,
inference(rat,[],[s53,s71,s79]) ).
cnf(s87,plain,
spl15_50,
inference(rat,[],[s50,s66,s79]) ).
cnf(s89,plain,
spl15_54,
inference(rat,[],[s54,s86]) ).
cnf(s92,plain,
spl15_59,
inference(rat,[],[s59,s4,s7,s13,s87]) ).
cnf(s94,plain,
spl15_60,
inference(rat,[],[s60,s16,s92]) ).
cnf(s108,plain,
~ spl15_1,
inference(rat,[],[s62,s94,s89,s5,s2]) ).
cnf(s109,plain,
$false,
inference(rat,[],[s1,s108]) ).
fof(f6887,plain,
$false,
inference(avatar_sat_refutation,[],[s109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL348-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.11/0.36 % Computer : n009.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 15:36:00 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 Running first-order theorem proving
% 0.11/0.40 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
% 13.63/2.79 % (2185259)Detected a unit-equality problem, will run specialized UEQ schedule.
% 13.63/2.79 % (2185379)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3084381080:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 13.63/2.79 % (2185378)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1948200104:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 13.63/2.79 % (2185374)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=3221894983:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 13.63/2.79 % (2185377)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1515697159:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 13.63/2.79 % (2185376)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2524610206:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 13.63/2.79 % (2185375)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=1746541045:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 13.63/2.79 % (2185380)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1934999915:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 13.63/2.79 % (2185379)Instruction limit reached!
% 13.63/2.79 % (2185379)------------------------------
% 13.63/2.79 % (2185379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185379)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185379)Termination reason: Instruction limit
% 13.63/2.79 % (2185379)Termination phase: Saturation
% 13.63/2.79 % (2185379)Time elapsed: 0.081 s
% 13.63/2.79 % (2185379)Peak memory usage: 91 MB
% 13.63/2.79 % (2185379)Instructions burned: 260 (million)
% 13.63/2.79 % (2185377)Instruction limit reached!
% 13.63/2.79 % (2185377)------------------------------
% 13.63/2.79 % (2185377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185377)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185377)Termination reason: Instruction limit
% 13.63/2.79 % (2185377)Termination phase: Saturation
% 13.63/2.79 % (2185377)Time elapsed: 0.085 s
% 13.63/2.79 % (2185377)Peak memory usage: 89 MB
% 13.63/2.79 % (2185377)Instructions burned: 136 (million)
% 13.63/2.79 % (2185378)Instruction limit reached!
% 13.63/2.79 % (2185378)------------------------------
% 13.63/2.79 % (2185378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185378)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185378)Termination reason: Instruction limit
% 13.63/2.79 % (2185378)Termination phase: Saturation
% 13.63/2.79 % (2185378)Time elapsed: 0.113 s
% 13.63/2.79 % (2185378)Peak memory usage: 89 MB
% 13.63/2.79 % (2185378)Instructions burned: 182 (million)
% 13.63/2.79 % (2185435)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1367044369:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 13.63/2.79 % (2185436)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3882338545:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 13.63/2.79 % (2185437)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2762737421:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 13.63/2.79 % (2185437)Instruction limit reached!
% 13.63/2.79 % (2185437)------------------------------
% 13.63/2.79 % (2185437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185437)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185437)Termination reason: Instruction limit
% 13.63/2.79 % (2185437)Termination phase: Saturation
% 13.63/2.79 % (2185437)Time elapsed: 0.106 s
% 13.63/2.79 % (2185437)Peak memory usage: 88 MB
% 13.63/2.79 % (2185437)Instructions burned: 215 (million)
% 13.63/2.79 % (2185441)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=3127080450:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 13.63/2.79 % (2185441)Instruction limit reached!
% 13.63/2.79 % (2185441)------------------------------
% 13.63/2.79 % (2185441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185441)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185441)Termination reason: Instruction limit
% 13.63/2.79 % (2185441)Termination phase: Saturation
% 13.63/2.79 % (2185441)Time elapsed: 0.195 s
% 13.63/2.79 % (2185441)Peak memory usage: 94 MB
% 13.63/2.79 % (2185441)Instructions burned: 318 (million)
% 13.63/2.79 % (2185380)Instruction limit reached!
% 13.63/2.79 % (2185380)------------------------------
% 13.63/2.79 % (2185380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185380)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185380)Termination reason: Instruction limit
% 13.63/2.79 % (2185380)Termination phase: Saturation
% 13.63/2.79 % (2185380)Time elapsed: 0.690 s
% 13.63/2.79 % (2185380)Peak memory usage: 101 MB
% 13.63/2.79 % (2185380)Instructions burned: 1187 (million)
% 13.63/2.79 % (2185443)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=1329362598:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 13.63/2.79 % (2185444)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1195729455:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2991 on theBenchmark for (2991ds/2836Mi)
% 13.63/2.79 % (2185435)Instruction limit reached!
% 13.63/2.79 % (2185435)------------------------------
% 13.63/2.79 % (2185435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.63/2.79 % (2185435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.63/2.79 % (2185435)CaDiCaL version: 2.1.3
% 13.63/2.79 % (2185435)Termination reason: Instruction limit
% 13.63/2.79 % (2185435)Termination phase: Saturation
% 13.63/2.79 % (2185435)Time elapsed: 0.741 s
% 13.63/2.79 % (2185435)Peak memory usage: 144 MB
% 13.63/2.79 % (2185435)Instructions burned: 2054 (million)
% 13.63/2.79 % (2185447)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1394670879:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 13.63/2.79 % (2185374)First to succeed.
% 13.63/2.79 % (2185374)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2185259"
% 13.63/2.79 % (2185374)Refutation found. Thanks to Tanya!
% 13.63/2.79 % SZS status Unsatisfiable for theBenchmark
% 13.63/2.79 % SZS output start Proof for theBenchmark
% See solution above
% 14.43/2.99 % (2185374)------------------------------
% 14.43/2.99 % (2185374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.43/2.99 % (2185374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.43/2.99 % (2185374)CaDiCaL version: 2.1.3
% 14.43/2.99 % (2185374)Termination reason: Refutation
% 14.43/2.99 % (2185374)Time elapsed: 1.552 s
% 14.43/2.99 % (2185374)Peak memory usage: 145 MB
% 14.43/2.99 % (2185374)Instructions burned: 2447 (million)
% 14.43/2.99 % (2185374)------------------------------
% 14.43/2.99 % (2185374)------------------------------
% 14.43/2.99 % (2185259)Success in time 1.957 s
% 14.43/2.99 % Vampire exiting
%------------------------------------------------------------------------------