%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL304-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:51:55 AM UTC 2026
% Result : Unsatisfiable 40.15s 6.57s
% Output : Refutation 40.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 78
% Syntax : Number of formulae : 450 ( 194 unt; 66 def)
% Number of atoms : 971 ( 327 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1002 ( 481 ~; 475 |; 0 &)
% ( 46 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 48 ( 46 usr; 47 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 23 con; 0-4 aty)
% Number of variables : 222 ( 0 sgn 222 !; 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(implies(p,q),equivalent(q,or(p,q)))) != true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f19,plain,
true != theorem(equivalent(implies(p,q),equivalent(q,or(p,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(p),q)),not(or(not(or(not(q),or(p,q))),not(or(not(or(p,q)),q)))))),not(or(not(not(or(not(or(not(q),or(p,q))),not(or(not(or(p,q)),q))))),or(not(p),q)))))),
inference(definition_unfolding,[],[f19,f20,f11,f20]) ).
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 = or(sF0,q),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f31,plain,
or(sF0,q) = sF1,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF2 = not(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f33,plain,
not(sF1) = sF2,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF3 = not(q),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f35,plain,
not(q) = sF3,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF4 = or(p,q),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f37,plain,
or(p,q) = sF4,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF5 = or(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f39,plain,
or(sF3,sF4) = sF5,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF6 = not(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f41,plain,
not(sF5) = sF6,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF7 = not(sF4),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f43,plain,
not(sF4) = sF7,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF8 = or(sF7,q),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f45,plain,
or(sF7,q) = sF8,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF9 = not(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f47,plain,
not(sF8) = sF9,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF10 = or(sF6,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f49,plain,
or(sF6,sF9) = 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(sF2,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f53,plain,
or(sF2,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 = not(sF11),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f57,plain,
not(sF11) = sF14,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF15 = or(sF14,sF1),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f59,plain,
or(sF14,sF1) = sF15,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF16 = not(sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f61,plain,
not(sF15) = sF16,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF17 = or(sF13,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f63,plain,
or(sF13,sF16) = sF17,
inference(reorient_equations,[],[f62]) ).
fof(f64,definition,
sF18 = not(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f65,plain,
not(sF17) = sF18,
inference(reorient_equations,[],[f64]) ).
fof(f66,definition,
sF19 = theorem(sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f67,plain,
theorem(sF18) = sF19,
inference(reorient_equations,[],[f66]) ).
fof(f68,plain,
true != sF19,
inference(definition_folding,[],[f27,f67,f65,f63,f61,f59,f31,f29,f57,f51,f49,f47,f45,f43,f37,f41,f39,f37,f35,f55,f53,f51,f49,f47,f45,f43,f37,f41,f39,f37,f35,f33,f31,f29]) ).
fof(f70,definition,
( spl20_1
<=> theorem(sF18) = sF19 ),
introduced(definition,[new_symbols(definition,[spl20_1])],[avatar_definition]) ).
fof(f72,plain,
( theorem(sF18) = sF19
| ~ spl20_1 ),
inference(avatar_component_clause,[],[f70]) ).
fof(f73,plain,
spl20_1,
inference(avatar_split_clause,[],[f67,f70]) ).
fof(f75,definition,
( spl20_2
<=> true = sF19 ),
introduced(definition,[new_symbols(definition,[spl20_2])],[avatar_definition]) ).
fof(f77,plain,
( true != sF19
| spl20_2 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f78,plain,
~ spl20_2,
inference(avatar_split_clause,[],[f68,f75]) ).
fof(f80,plain,
( ! [X0] : true = ifeq(theorem(or(not(X0),sF18)),true,ifeq(theorem(X0),true,sF19,true),true)
| ~ spl20_1 ),
inference(superposition,[],[f26,f72]) ).
fof(f82,definition,
( spl20_3
<=> not(p) = sF0 ),
introduced(definition,[new_symbols(definition,[spl20_3])],[avatar_definition]) ).
fof(f84,plain,
( not(p) = sF0
| ~ spl20_3 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f85,plain,
spl20_3,
inference(avatar_split_clause,[],[f29,f82]) ).
fof(f87,definition,
( spl20_4
<=> not(q) = sF3 ),
introduced(definition,[new_symbols(definition,[spl20_4])],[avatar_definition]) ).
fof(f89,plain,
( not(q) = sF3
| ~ spl20_4 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f90,plain,
spl20_4,
inference(avatar_split_clause,[],[f35,f87]) ).
fof(f96,definition,
( spl20_5
<=> not(sF11) = sF14 ),
introduced(definition,[new_symbols(definition,[spl20_5])],[avatar_definition]) ).
fof(f98,plain,
( not(sF11) = sF14
| ~ spl20_5 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f99,plain,
spl20_5,
inference(avatar_split_clause,[],[f57,f96]) ).
fof(f101,definition,
( spl20_6
<=> not(sF1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl20_6])],[avatar_definition]) ).
fof(f103,plain,
( not(sF1) = sF2
| ~ spl20_6 ),
inference(avatar_component_clause,[],[f101]) ).
fof(f104,plain,
spl20_6,
inference(avatar_split_clause,[],[f33,f101]) ).
fof(f106,definition,
( spl20_7
<=> not(sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl20_7])],[avatar_definition]) ).
fof(f108,plain,
( not(sF10) = sF11
| ~ spl20_7 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,plain,
spl20_7,
inference(avatar_split_clause,[],[f51,f106]) ).
fof(f111,definition,
( spl20_8
<=> not(sF4) = sF7 ),
introduced(definition,[new_symbols(definition,[spl20_8])],[avatar_definition]) ).
fof(f113,plain,
( not(sF4) = sF7
| ~ spl20_8 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
spl20_8,
inference(avatar_split_clause,[],[f43,f111]) ).
fof(f116,definition,
( spl20_9
<=> not(sF17) = sF18 ),
introduced(definition,[new_symbols(definition,[spl20_9])],[avatar_definition]) ).
fof(f118,plain,
( not(sF17) = sF18
| ~ spl20_9 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f119,plain,
spl20_9,
inference(avatar_split_clause,[],[f65,f116]) ).
fof(f125,definition,
( spl20_10
<=> not(sF5) = sF6 ),
introduced(definition,[new_symbols(definition,[spl20_10])],[avatar_definition]) ).
fof(f127,plain,
( not(sF5) = sF6
| ~ spl20_10 ),
inference(avatar_component_clause,[],[f125]) ).
fof(f128,plain,
spl20_10,
inference(avatar_split_clause,[],[f41,f125]) ).
fof(f130,definition,
( spl20_11
<=> not(sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl20_11])],[avatar_definition]) ).
fof(f132,plain,
( not(sF8) = sF9
| ~ spl20_11 ),
inference(avatar_component_clause,[],[f130]) ).
fof(f133,plain,
spl20_11,
inference(avatar_split_clause,[],[f47,f130]) ).
fof(f139,definition,
( spl20_12
<=> not(sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl20_12])],[avatar_definition]) ).
fof(f141,plain,
( not(sF12) = sF13
| ~ spl20_12 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,plain,
spl20_12,
inference(avatar_split_clause,[],[f55,f139]) ).
fof(f144,definition,
( spl20_13
<=> not(sF15) = sF16 ),
introduced(definition,[new_symbols(definition,[spl20_13])],[avatar_definition]) ).
fof(f146,plain,
( not(sF15) = sF16
| ~ spl20_13 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,plain,
spl20_13,
inference(avatar_split_clause,[],[f61,f144]) ).
fof(f148,plain,
( ! [X0] : true = ifeq(theorem(or(sF6,X0)),true,ifeq(theorem(sF5),true,theorem(X0),true),true)
| ~ spl20_10 ),
inference(superposition,[],[f26,f127]) ).
fof(f158,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(X1,X0))),true),
inference(superposition,[],[f13,f23]) ).
fof(f159,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X1,X0))),true),
inference(superposition,[],[f13,f22]) ).
fof(f160,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(f161,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,X0)),X0)),true),
inference(superposition,[],[f13,f21]) ).
fof(f163,plain,
! [X0] : true = theorem(or(not(or(X0,X0)),X0)),
inference(forward_demodulation,[],[f161,f1]) ).
fof(f164,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(forward_demodulation,[],[f160,f1]) ).
fof(f165,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X1,X0))),
inference(forward_demodulation,[],[f159,f1]) ).
fof(f166,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(forward_demodulation,[],[f158,f1]) ).
fof(f167,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,f164]) ).
fof(f173,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X1,or(X0,X2))),true),
inference(forward_demodulation,[],[f167,f1]) ).
fof(f174,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f166]) ).
fof(f180,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f174,f1]) ).
fof(f203,definition,
( spl20_14
<=> or(sF3,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl20_14])],[avatar_definition]) ).
fof(f205,plain,
( or(sF3,sF4) = sF5
| ~ spl20_14 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,plain,
spl20_14,
inference(avatar_split_clause,[],[f39,f203]) ).
fof(f246,definition,
( spl20_15
<=> or(p,q) = sF4 ),
introduced(definition,[new_symbols(definition,[spl20_15])],[avatar_definition]) ).
fof(f248,plain,
( or(p,q) = sF4
| ~ spl20_15 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
spl20_15,
inference(avatar_split_clause,[],[f37,f246]) ).
fof(f257,plain,
( true = theorem(or(not(q),sF4))
| ~ spl20_15 ),
inference(superposition,[],[f165,f248]) ).
fof(f260,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF4)),true,theorem(or(p,or(X0,q))),true)
| ~ spl20_15 ),
inference(superposition,[],[f173,f248]) ).
fof(f263,plain,
( true = theorem(or(sF3,sF4))
| ~ spl20_4
| ~ spl20_15 ),
inference(forward_demodulation,[],[f257,f89]) ).
fof(f266,plain,
( true = theorem(sF5)
| ~ spl20_4
| ~ spl20_14
| ~ spl20_15 ),
inference(forward_demodulation,[],[f263,f205]) ).
fof(f268,plain,
( ! [X0] : true = ifeq(theorem(or(sF6,X0)),true,ifeq(true,true,theorem(X0),true),true)
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15 ),
inference(backward_demodulation,[],[f148,f266]) ).
fof(f269,plain,
( ! [X0] : true = ifeq(theorem(or(sF6,X0)),true,theorem(X0),true)
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15 ),
inference(forward_demodulation,[],[f268,f1]) ).
fof(f285,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(f286,plain,
! [X2,X0,X1] : true = theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(forward_demodulation,[],[f285,f1]) ).
fof(f292,definition,
( spl20_16
<=> or(sF2,sF11) = sF12 ),
introduced(definition,[new_symbols(definition,[spl20_16])],[avatar_definition]) ).
fof(f294,plain,
( or(sF2,sF11) = sF12
| ~ spl20_16 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,plain,
spl20_16,
inference(avatar_split_clause,[],[f53,f292]) ).
fof(f305,plain,
( true = theorem(or(not(sF11),sF12))
| ~ spl20_16 ),
inference(superposition,[],[f165,f294]) ).
fof(f311,plain,
( true = theorem(or(sF14,sF12))
| ~ spl20_5
| ~ spl20_16 ),
inference(forward_demodulation,[],[f305,f98]) ).
fof(f317,definition,
( spl20_17
<=> or(sF7,q) = sF8 ),
introduced(definition,[new_symbols(definition,[spl20_17])],[avatar_definition]) ).
fof(f319,plain,
( or(sF7,q) = sF8
| ~ spl20_17 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f320,plain,
spl20_17,
inference(avatar_split_clause,[],[f45,f317]) ).
fof(f342,definition,
( spl20_18
<=> or(sF14,sF1) = sF15 ),
introduced(definition,[new_symbols(definition,[spl20_18])],[avatar_definition]) ).
fof(f344,plain,
( or(sF14,sF1) = sF15
| ~ spl20_18 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
spl20_18,
inference(avatar_split_clause,[],[f59,f342]) ).
fof(f359,plain,
( ! [X0] : true = ifeq(theorem(or(sF14,or(X0,sF1))),true,theorem(or(X0,sF15)),true)
| ~ spl20_18 ),
inference(superposition,[],[f173,f344]) ).
fof(f367,definition,
( spl20_19
<=> or(sF6,sF9) = sF10 ),
introduced(definition,[new_symbols(definition,[spl20_19])],[avatar_definition]) ).
fof(f369,plain,
( or(sF6,sF9) = sF10
| ~ spl20_19 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f370,plain,
spl20_19,
inference(avatar_split_clause,[],[f49,f367]) ).
fof(f389,definition,
( spl20_20
<=> or(sF13,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl20_20])],[avatar_definition]) ).
fof(f391,plain,
( or(sF13,sF16) = sF17
| ~ spl20_20 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,plain,
spl20_20,
inference(avatar_split_clause,[],[f63,f389]) ).
fof(f411,definition,
( spl20_21
<=> or(sF0,q) = sF1 ),
introduced(definition,[new_symbols(definition,[spl20_21])],[avatar_definition]) ).
fof(f413,plain,
( or(sF0,q) = sF1
| ~ spl20_21 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f414,plain,
spl20_21,
inference(avatar_split_clause,[],[f31,f411]) ).
fof(f462,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,f286]) ).
fof(f464,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,[],[f173,f286]) ).
fof(f470,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(not(or(not(X0),X1)),or(X2,X1)))),
inference(forward_demodulation,[],[f464,f1]) ).
fof(f471,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,[],[f462,f1]) ).
fof(f499,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f471,f166]) ).
fof(f500,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),true),
inference(superposition,[],[f471,f163]) ).
fof(f502,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),true),
inference(superposition,[],[f471,f165]) ).
fof(f507,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF9),X0)),true,theorem(or(not(sF10),or(sF6,X0))),true)
| ~ spl20_19 ),
inference(superposition,[],[f471,f369]) ).
fof(f509,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF16),X0)),true,theorem(or(not(sF17),or(sF13,X0))),true)
| ~ spl20_20 ),
inference(superposition,[],[f471,f391]) ).
fof(f526,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF16),X0)),true,theorem(or(sF18,or(sF13,X0))),true)
| ~ spl20_9
| ~ spl20_20 ),
inference(forward_demodulation,[],[f509,f118]) ).
fof(f528,plain,
( ! [X0] : true = ifeq(theorem(or(not(sF9),X0)),true,theorem(or(sF11,or(sF6,X0))),true)
| ~ spl20_7
| ~ spl20_19 ),
inference(forward_demodulation,[],[f507,f108]) ).
fof(f533,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,X0)),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f502,f1]) ).
fof(f535,plain,
! [X0,X1] : true = theorem(or(not(or(X1,or(X0,X0))),or(X1,X0))),
inference(forward_demodulation,[],[f500,f1]) ).
fof(f536,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,X1))),or(X2,or(X1,X0)))),
inference(forward_demodulation,[],[f499,f1]) ).
fof(f573,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,f470]) ).
fof(f582,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,[],[f573,f1]) ).
fof(f607,plain,
! [X2,X0,X1] : true = ifeq(true,true,theorem(or(not(or(X2,or(X0,or(X1,X1)))),or(X2,or(X0,X1)))),true),
inference(superposition,[],[f471,f535]) ).
fof(f608,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),true),
inference(superposition,[],[f26,f535]) ).
fof(f616,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X0,X1)),true),
inference(forward_demodulation,[],[f608,f1]) ).
fof(f617,plain,
! [X2,X0,X1] : true = theorem(or(not(or(X2,or(X0,or(X1,X1)))),or(X2,or(X0,X1)))),
inference(forward_demodulation,[],[f607,f1]) ).
fof(f638,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,f536]) ).
fof(f646,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,X2))),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f638,f1]) ).
fof(f668,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,f533]) ).
fof(f676,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(X0,or(X2,X1))),true),
inference(forward_demodulation,[],[f668,f1]) ).
fof(f752,plain,
! [X0] : true = ifeq(true,true,theorem(or(not(X0),X0)),true),
inference(superposition,[],[f616,f165]) ).
fof(f773,plain,
! [X0] : true = theorem(or(not(X0),X0)),
inference(forward_demodulation,[],[f752,f1]) ).
fof(f784,plain,
( true = theorem(or(sF7,sF4))
| ~ spl20_8 ),
inference(superposition,[],[f773,f113]) ).
fof(f800,plain,
! [X0] : true = ifeq(true,true,theorem(or(X0,not(X0))),true),
inference(superposition,[],[f180,f773]) ).
fof(f806,plain,
! [X0] : true = theorem(or(X0,not(X0))),
inference(forward_demodulation,[],[f800,f1]) ).
fof(f836,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,or(X1,X1))),or(X1,X0))),true),
inference(superposition,[],[f646,f535]) ).
fof(f841,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(X0),or(X0,X1))),true),
inference(superposition,[],[f646,f165]) ).
fof(f863,plain,
! [X0,X1] : true = theorem(or(not(X0),or(X0,X1))),
inference(forward_demodulation,[],[f841,f1]) ).
fof(f868,plain,
! [X0,X1] : true = theorem(or(not(or(X0,or(X1,X1))),or(X1,X0))),
inference(forward_demodulation,[],[f836,f1]) ).
fof(f879,plain,
( ! [X0] : true = ifeq(theorem(sF15),true,theorem(or(sF14,or(X0,sF1))),true)
| ~ spl20_18 ),
inference(superposition,[],[f676,f344]) ).
fof(f894,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF9)),true,theorem(or(X0,sF10)),true)
| ~ spl20_19 ),
inference(superposition,[],[f676,f369]) ).
fof(f895,plain,
( ! [X0] : true = ifeq(theorem(or(X0,q)),true,theorem(or(X0,sF8)),true)
| ~ spl20_17 ),
inference(superposition,[],[f676,f319]) ).
fof(f940,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),true),
inference(superposition,[],[f471,f806]) ).
fof(f954,plain,
! [X0,X1] : true = theorem(or(not(or(X1,X0)),or(X1,not(not(X0))))),
inference(forward_demodulation,[],[f940,f1]) ).
fof(f974,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,p)),true,theorem(or(not(or(sF0,X1)),or(X0,X1))),true)
| ~ spl20_3 ),
inference(superposition,[],[f582,f84]) ).
fof(f982,plain,
( ! [X0,X1] : true = ifeq(theorem(or(X0,sF12)),true,theorem(or(not(or(sF13,X1)),or(X0,X1))),true)
| ~ spl20_12 ),
inference(superposition,[],[f582,f141]) ).
fof(f1118,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),true),
inference(superposition,[],[f646,f954]) ).
fof(f1137,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(not(not(X1)),X0))),
inference(forward_demodulation,[],[f1118,f1]) ).
fof(f1200,plain,
( true = theorem(or(not(p),sF4))
| ~ spl20_15 ),
inference(superposition,[],[f863,f248]) ).
fof(f1235,plain,
( true = theorem(or(sF0,sF4))
| ~ spl20_3
| ~ spl20_15 ),
inference(forward_demodulation,[],[f1200,f84]) ).
fof(f1581,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),true),
inference(superposition,[],[f26,f1137]) ).
fof(f1608,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(not(X1)),X0)),true),
inference(forward_demodulation,[],[f1581,f1]) ).
fof(f1896,definition,
( spl20_24
<=> true = theorem(or(sF0,sF4)) ),
introduced(definition,[new_symbols(definition,[spl20_24])],[avatar_definition]) ).
fof(f1898,plain,
( true = theorem(or(sF0,sF4))
| ~ spl20_24 ),
inference(avatar_component_clause,[],[f1896]) ).
fof(f1899,plain,
( spl20_24
| ~ spl20_3
| ~ spl20_15 ),
inference(avatar_split_clause,[],[f1235,f246,f82,f1896]) ).
fof(f1902,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(not(sF4),X0)),or(sF0,X0))),true)
| ~ spl20_24 ),
inference(superposition,[],[f582,f1898]) ).
fof(f1917,plain,
( ! [X0] : true = theorem(or(not(or(not(sF4),X0)),or(sF0,X0)))
| ~ spl20_24 ),
inference(forward_demodulation,[],[f1902,f1]) ).
fof(f1919,plain,
( ! [X0] : true = theorem(or(not(or(sF7,X0)),or(sF0,X0)))
| ~ spl20_8
| ~ spl20_24 ),
inference(forward_demodulation,[],[f1917,f113]) ).
fof(f1921,plain,
( true = theorem(or(not(or(sF7,q)),sF1))
| ~ spl20_8
| ~ spl20_21
| ~ spl20_24 ),
inference(superposition,[],[f1919,f413]) ).
fof(f1955,plain,
( true = theorem(or(not(sF8),sF1))
| ~ spl20_8
| ~ spl20_17
| ~ spl20_21
| ~ spl20_24 ),
inference(forward_demodulation,[],[f1921,f319]) ).
fof(f1957,plain,
( true = theorem(or(sF9,sF1))
| ~ spl20_8
| ~ spl20_11
| ~ spl20_17
| ~ spl20_21
| ~ spl20_24 ),
inference(forward_demodulation,[],[f1955,f132]) ).
fof(f1960,definition,
( spl20_25
<=> true = theorem(or(sF9,sF1)) ),
introduced(definition,[new_symbols(definition,[spl20_25])],[avatar_definition]) ).
fof(f1962,plain,
( true = theorem(or(sF9,sF1))
| ~ spl20_25 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1963,plain,
( spl20_25
| ~ spl20_8
| ~ spl20_11
| ~ spl20_17
| ~ spl20_21
| ~ spl20_24 ),
inference(avatar_split_clause,[],[f1957,f1896,f411,f317,f130,f111,f1960]) ).
fof(f1966,plain,
( true = ifeq(true,true,theorem(or(sF1,sF9)),true)
| ~ spl20_25 ),
inference(superposition,[],[f180,f1962]) ).
fof(f1984,plain,
( true = theorem(or(sF1,sF9))
| ~ spl20_25 ),
inference(forward_demodulation,[],[f1966,f1]) ).
fof(f2163,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF10)),true,theorem(or(not(sF11),X0)),true)
| ~ spl20_7 ),
inference(superposition,[],[f1608,f108]) ).
fof(f2166,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF15)),true,theorem(or(not(sF16),X0)),true)
| ~ spl20_13 ),
inference(superposition,[],[f1608,f146]) ).
fof(f2175,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF10)),true,theorem(or(sF14,X0)),true)
| ~ spl20_5
| ~ spl20_7 ),
inference(forward_demodulation,[],[f2163,f98]) ).
fof(f2219,plain,
( true = ifeq(theorem(or(sF1,sF10)),true,theorem(sF15),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18 ),
inference(superposition,[],[f2175,f344]) ).
fof(f2229,definition,
( spl20_27
<=> true = theorem(or(sF1,sF9)) ),
introduced(definition,[new_symbols(definition,[spl20_27])],[avatar_definition]) ).
fof(f2231,plain,
( true = theorem(or(sF1,sF9))
| ~ spl20_27 ),
inference(avatar_component_clause,[],[f2229]) ).
fof(f2232,plain,
( spl20_27
| ~ spl20_25 ),
inference(avatar_split_clause,[],[f1984,f1960,f2229]) ).
fof(f2233,plain,
( true = ifeq(true,true,theorem(or(sF1,sF10)),true)
| ~ spl20_19
| ~ spl20_27 ),
inference(superposition,[],[f894,f2231]) ).
fof(f2255,plain,
( true = theorem(or(sF1,sF10))
| ~ spl20_19
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2233,f1]) ).
fof(f2256,plain,
( true = ifeq(true,true,theorem(sF15),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(backward_demodulation,[],[f2219,f2255]) ).
fof(f2257,plain,
( true = theorem(sF15)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2256,f1]) ).
fof(f2262,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF14,or(X0,sF1))),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(backward_demodulation,[],[f879,f2257]) ).
fof(f2272,plain,
( ! [X0] : true = theorem(or(sF14,or(X0,sF1)))
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2262,f1]) ).
fof(f2276,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(X0,sF15)),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(backward_demodulation,[],[f359,f2272]) ).
fof(f2277,plain,
( ! [X0] : true = theorem(or(X0,sF15))
| ~ spl20_5
| ~ spl20_7
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2276,f1]) ).
fof(f2283,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(sF16),X0)),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(backward_demodulation,[],[f2166,f2277]) ).
fof(f2286,plain,
( ! [X0] : true = theorem(or(not(sF16),X0))
| ~ spl20_5
| ~ spl20_7
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2283,f1]) ).
fof(f2289,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(sF18,or(sF13,X0))),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(backward_demodulation,[],[f526,f2286]) ).
fof(f2290,plain,
( ! [X0] : true = theorem(or(sF18,or(sF13,X0)))
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2289,f1]) ).
fof(f2768,plain,
( true = ifeq(true,true,theorem(or(sF18,sF13)),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(superposition,[],[f616,f2290]) ).
fof(f2793,plain,
( true = theorem(or(sF18,sF13))
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(forward_demodulation,[],[f2768,f1]) ).
fof(f3830,plain,
! [X2,X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,or(X2,X2)))),true,theorem(or(X0,or(X1,X2))),true),true),
inference(superposition,[],[f26,f617]) ).
fof(f3869,plain,
! [X2,X0,X1] : true = ifeq(theorem(or(X0,or(X1,or(X2,X2)))),true,theorem(or(X0,or(X1,X2))),true),
inference(forward_demodulation,[],[f3830,f1]) ).
fof(f5430,definition,
( spl20_42
<=> true = theorem(or(sF14,sF12)) ),
introduced(definition,[new_symbols(definition,[spl20_42])],[avatar_definition]) ).
fof(f5432,plain,
( true = theorem(or(sF14,sF12))
| ~ spl20_42 ),
inference(avatar_component_clause,[],[f5430]) ).
fof(f5433,plain,
( spl20_42
| ~ spl20_5
| ~ spl20_16 ),
inference(avatar_split_clause,[],[f311,f292,f96,f5430]) ).
fof(f5449,plain,
( true = ifeq(true,true,theorem(or(not(not(sF12)),sF14)),true)
| ~ spl20_42 ),
inference(superposition,[],[f1608,f5432]) ).
fof(f5465,plain,
( true = theorem(or(not(not(sF12)),sF14))
| ~ spl20_42 ),
inference(forward_demodulation,[],[f5449,f1]) ).
fof(f5473,plain,
( true = theorem(or(not(sF13),sF14))
| ~ spl20_12
| ~ spl20_42 ),
inference(forward_demodulation,[],[f5465,f141]) ).
fof(f8267,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X1,X0)),true),true),
inference(superposition,[],[f26,f868]) ).
fof(f8321,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,or(X1,X1))),true,theorem(or(X1,X0)),true),
inference(forward_demodulation,[],[f8267,f1]) ).
fof(f8380,plain,
( true = ifeq(true,true,theorem(or(sF13,sF18)),true)
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(superposition,[],[f8321,f2290]) ).
fof(f8478,plain,
( true = theorem(or(sF13,sF18))
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(forward_demodulation,[],[f8380,f1]) ).
fof(f9691,plain,
! [X0,X1] : true = ifeq(true,true,theorem(or(not(or(X0,X1)),or(not(or(not(X1),X0)),X0))),true),
inference(superposition,[],[f3869,f470]) ).
fof(f9826,plain,
! [X0,X1] : true = theorem(or(not(or(X0,X1)),or(not(or(not(X1),X0)),X0))),
inference(forward_demodulation,[],[f9691,f1]) ).
fof(f10100,plain,
! [X0,X1] : true = ifeq(true,true,ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X1),X0)),X0)),true),true),
inference(superposition,[],[f26,f9826]) ).
fof(f10159,plain,
! [X0,X1] : true = ifeq(theorem(or(X0,X1)),true,theorem(or(not(or(not(X1),X0)),X0)),true),
inference(forward_demodulation,[],[f10100,f1]) ).
fof(f12167,plain,
( true = ifeq(theorem(or(sF7,sF4)),true,theorem(or(p,sF8)),true)
| ~ spl20_15
| ~ spl20_17 ),
inference(superposition,[],[f260,f319]) ).
fof(f12171,plain,
( true = ifeq(true,true,theorem(or(p,sF8)),true)
| ~ spl20_8
| ~ spl20_15
| ~ spl20_17 ),
inference(forward_demodulation,[],[f12167,f784]) ).
fof(f12182,plain,
( true = theorem(or(p,sF8))
| ~ spl20_8
| ~ spl20_15
| ~ spl20_17 ),
inference(forward_demodulation,[],[f12171,f1]) ).
fof(f12189,definition,
( spl20_58
<=> true = theorem(or(p,sF8)) ),
introduced(definition,[new_symbols(definition,[spl20_58])],[avatar_definition]) ).
fof(f12191,plain,
( true = theorem(or(p,sF8))
| ~ spl20_58 ),
inference(avatar_component_clause,[],[f12189]) ).
fof(f12192,plain,
( spl20_58
| ~ spl20_8
| ~ spl20_15
| ~ spl20_17 ),
inference(avatar_split_clause,[],[f12182,f317,f246,f111,f12189]) ).
fof(f12206,plain,
( true = ifeq(true,true,theorem(or(not(not(sF8)),p)),true)
| ~ spl20_58 ),
inference(superposition,[],[f1608,f12191]) ).
fof(f12235,plain,
( true = theorem(or(not(not(sF8)),p))
| ~ spl20_58 ),
inference(forward_demodulation,[],[f12206,f1]) ).
fof(f12246,plain,
( true = theorem(or(not(sF9),p))
| ~ spl20_11
| ~ spl20_58 ),
inference(forward_demodulation,[],[f12235,f132]) ).
fof(f12450,definition,
( spl20_61
<=> true = theorem(or(not(sF9),p)) ),
introduced(definition,[new_symbols(definition,[spl20_61])],[avatar_definition]) ).
fof(f12452,plain,
( true = theorem(or(not(sF9),p))
| ~ spl20_61 ),
inference(avatar_component_clause,[],[f12450]) ).
fof(f12453,plain,
( spl20_61
| ~ spl20_11
| ~ spl20_58 ),
inference(avatar_split_clause,[],[f12246,f12189,f130,f12450]) ).
fof(f12454,plain,
( true = ifeq(true,true,theorem(or(sF11,or(sF6,p))),true)
| ~ spl20_7
| ~ spl20_19
| ~ spl20_61 ),
inference(superposition,[],[f528,f12452]) ).
fof(f12508,plain,
( true = theorem(or(sF11,or(sF6,p)))
| ~ spl20_7
| ~ spl20_19
| ~ spl20_61 ),
inference(forward_demodulation,[],[f12454,f1]) ).
fof(f12623,definition,
( spl20_62
<=> true = theorem(or(sF11,or(sF6,p))) ),
introduced(definition,[new_symbols(definition,[spl20_62])],[avatar_definition]) ).
fof(f12625,plain,
( true = theorem(or(sF11,or(sF6,p)))
| ~ spl20_62 ),
inference(avatar_component_clause,[],[f12623]) ).
fof(f12626,plain,
( spl20_62
| ~ spl20_7
| ~ spl20_19
| ~ spl20_61 ),
inference(avatar_split_clause,[],[f12508,f12450,f367,f106,f12623]) ).
fof(f12631,plain,
( true = ifeq(true,true,theorem(or(sF6,or(sF11,p))),true)
| ~ spl20_62 ),
inference(superposition,[],[f173,f12625]) ).
fof(f12686,plain,
( true = theorem(or(sF6,or(sF11,p)))
| ~ spl20_62 ),
inference(forward_demodulation,[],[f12631,f1]) ).
fof(f13808,definition,
( spl20_65
<=> true = theorem(or(sF18,sF13)) ),
introduced(definition,[new_symbols(definition,[spl20_65])],[avatar_definition]) ).
fof(f13810,plain,
( true = theorem(or(sF18,sF13))
| ~ spl20_65 ),
inference(avatar_component_clause,[],[f13808]) ).
fof(f13811,plain,
( spl20_65
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(avatar_split_clause,[],[f2793,f2229,f389,f367,f342,f144,f116,f106,f96,f13808]) ).
fof(f14252,definition,
( spl20_70
<=> true = theorem(or(not(sF13),sF14)) ),
introduced(definition,[new_symbols(definition,[spl20_70])],[avatar_definition]) ).
fof(f14254,plain,
( true = theorem(or(not(sF13),sF14))
| ~ spl20_70 ),
inference(avatar_component_clause,[],[f14252]) ).
fof(f14255,plain,
( spl20_70
| ~ spl20_12
| ~ spl20_42 ),
inference(avatar_split_clause,[],[f5473,f5430,f139,f14252]) ).
fof(f14259,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(X0,sF13)),or(X0,sF14))),true)
| ~ spl20_70 ),
inference(superposition,[],[f471,f14254]) ).
fof(f14308,plain,
( ! [X0] : true = theorem(or(not(or(X0,sF13)),or(X0,sF14)))
| ~ spl20_70 ),
inference(forward_demodulation,[],[f14259,f1]) ).
fof(f14320,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(X0,sF13)),true,theorem(or(X0,sF14)),true),true)
| ~ spl20_70 ),
inference(superposition,[],[f26,f14308]) ).
fof(f14387,plain,
( ! [X0] : true = ifeq(theorem(or(X0,sF13)),true,theorem(or(X0,sF14)),true)
| ~ spl20_70 ),
inference(forward_demodulation,[],[f14320,f1]) ).
fof(f14399,plain,
( true = ifeq(true,true,theorem(or(sF18,sF14)),true)
| ~ spl20_65
| ~ spl20_70 ),
inference(superposition,[],[f14387,f13810]) ).
fof(f14411,plain,
( true = theorem(or(sF18,sF14))
| ~ spl20_65
| ~ spl20_70 ),
inference(forward_demodulation,[],[f14399,f1]) ).
fof(f14419,definition,
( spl20_71
<=> true = theorem(or(sF18,sF14)) ),
introduced(definition,[new_symbols(definition,[spl20_71])],[avatar_definition]) ).
fof(f14421,plain,
( true = theorem(or(sF18,sF14))
| ~ spl20_71 ),
inference(avatar_component_clause,[],[f14419]) ).
fof(f14422,plain,
( spl20_71
| ~ spl20_65
| ~ spl20_70 ),
inference(avatar_split_clause,[],[f14411,f14252,f13808,f14419]) ).
fof(f14428,plain,
( true = ifeq(true,true,theorem(or(sF14,sF18)),true)
| ~ spl20_71 ),
inference(superposition,[],[f180,f14421]) ).
fof(f14470,plain,
( true = theorem(or(sF14,sF18))
| ~ spl20_71 ),
inference(forward_demodulation,[],[f14428,f1]) ).
fof(f14475,definition,
( spl20_72
<=> true = theorem(or(sF14,sF18)) ),
introduced(definition,[new_symbols(definition,[spl20_72])],[avatar_definition]) ).
fof(f14477,plain,
( true = theorem(or(sF14,sF18))
| ~ spl20_72 ),
inference(avatar_component_clause,[],[f14475]) ).
fof(f14478,plain,
( spl20_72
| ~ spl20_71 ),
inference(avatar_split_clause,[],[f14470,f14419,f14475]) ).
fof(f14512,plain,
( true = ifeq(theorem(or(not(or(sF14,sF18)),sF18)),true,ifeq(true,true,sF19,true),true)
| ~ spl20_1
| ~ spl20_72 ),
inference(superposition,[],[f80,f14477]) ).
fof(f14516,plain,
( true = ifeq(theorem(or(not(or(sF14,sF18)),sF18)),true,sF19,true)
| ~ spl20_1
| ~ spl20_72 ),
inference(forward_demodulation,[],[f14512,f1]) ).
fof(f16854,definition,
( spl20_82
<=> true = theorem(or(sF13,sF18)) ),
introduced(definition,[new_symbols(definition,[spl20_82])],[avatar_definition]) ).
fof(f16856,plain,
( true = theorem(or(sF13,sF18))
| ~ spl20_82 ),
inference(avatar_component_clause,[],[f16854]) ).
fof(f16857,plain,
( spl20_82
| ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27 ),
inference(avatar_split_clause,[],[f8478,f2229,f389,f367,f342,f144,f116,f106,f96,f16854]) ).
fof(f16983,definition,
( spl20_84
<=> true = theorem(or(sF6,or(sF11,p))) ),
introduced(definition,[new_symbols(definition,[spl20_84])],[avatar_definition]) ).
fof(f16985,plain,
( true = theorem(or(sF6,or(sF11,p)))
| ~ spl20_84 ),
inference(avatar_component_clause,[],[f16983]) ).
fof(f16986,plain,
( spl20_84
| ~ spl20_62 ),
inference(avatar_split_clause,[],[f12686,f12623,f16983]) ).
fof(f16990,plain,
( true = ifeq(true,true,theorem(or(sF11,p)),true)
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_84 ),
inference(superposition,[],[f269,f16985]) ).
fof(f17050,plain,
( true = theorem(or(sF11,p))
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_84 ),
inference(forward_demodulation,[],[f16990,f1]) ).
fof(f17055,definition,
( spl20_85
<=> true = theorem(or(sF11,p)) ),
introduced(definition,[new_symbols(definition,[spl20_85])],[avatar_definition]) ).
fof(f17057,plain,
( true = theorem(or(sF11,p))
| ~ spl20_85 ),
inference(avatar_component_clause,[],[f17055]) ).
fof(f17058,plain,
( spl20_85
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_84 ),
inference(avatar_split_clause,[],[f17050,f16983,f246,f203,f125,f87,f17055]) ).
fof(f17062,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF0,X0)),or(sF11,X0))),true)
| ~ spl20_3
| ~ spl20_85 ),
inference(superposition,[],[f974,f17057]) ).
fof(f17112,plain,
( ! [X0] : true = theorem(or(not(or(sF0,X0)),or(sF11,X0)))
| ~ spl20_3
| ~ spl20_85 ),
inference(forward_demodulation,[],[f17062,f1]) ).
fof(f17770,plain,
( true = theorem(or(not(sF1),or(sF11,q)))
| ~ spl20_3
| ~ spl20_21
| ~ spl20_85 ),
inference(superposition,[],[f17112,f413]) ).
fof(f17859,plain,
( true = theorem(or(sF2,or(sF11,q)))
| ~ spl20_3
| ~ spl20_6
| ~ spl20_21
| ~ spl20_85 ),
inference(forward_demodulation,[],[f17770,f103]) ).
fof(f18632,definition,
( spl20_98
<=> true = theorem(or(sF2,or(sF11,q))) ),
introduced(definition,[new_symbols(definition,[spl20_98])],[avatar_definition]) ).
fof(f18634,plain,
( true = theorem(or(sF2,or(sF11,q)))
| ~ spl20_98 ),
inference(avatar_component_clause,[],[f18632]) ).
fof(f18635,plain,
( spl20_98
| ~ spl20_3
| ~ spl20_6
| ~ spl20_21
| ~ spl20_85 ),
inference(avatar_split_clause,[],[f17859,f17055,f411,f101,f82,f18632]) ).
fof(f18645,plain,
( true = ifeq(true,true,theorem(or(sF2,or(q,sF11))),true)
| ~ spl20_98 ),
inference(superposition,[],[f646,f18634]) ).
fof(f18700,plain,
( true = theorem(or(sF2,or(q,sF11)))
| ~ spl20_98 ),
inference(forward_demodulation,[],[f18645,f1]) ).
fof(f19736,definition,
( spl20_104
<=> true = theorem(or(sF2,or(q,sF11))) ),
introduced(definition,[new_symbols(definition,[spl20_104])],[avatar_definition]) ).
fof(f19738,plain,
( true = theorem(or(sF2,or(q,sF11)))
| ~ spl20_104 ),
inference(avatar_component_clause,[],[f19736]) ).
fof(f19739,plain,
( spl20_104
| ~ spl20_98 ),
inference(avatar_split_clause,[],[f18700,f18632,f19736]) ).
fof(f19747,plain,
( true = ifeq(true,true,theorem(or(q,or(sF2,sF11))),true)
| ~ spl20_104 ),
inference(superposition,[],[f173,f19738]) ).
fof(f19805,plain,
( true = theorem(or(q,or(sF2,sF11)))
| ~ spl20_104 ),
inference(forward_demodulation,[],[f19747,f1]) ).
fof(f19814,plain,
( true = theorem(or(q,sF12))
| ~ spl20_16
| ~ spl20_104 ),
inference(forward_demodulation,[],[f19805,f294]) ).
fof(f19816,definition,
( spl20_105
<=> true = theorem(or(q,sF12)) ),
introduced(definition,[new_symbols(definition,[spl20_105])],[avatar_definition]) ).
fof(f19818,plain,
( true = theorem(or(q,sF12))
| ~ spl20_105 ),
inference(avatar_component_clause,[],[f19816]) ).
fof(f19819,plain,
( spl20_105
| ~ spl20_16
| ~ spl20_104 ),
inference(avatar_split_clause,[],[f19814,f19736,f292,f19816]) ).
fof(f19820,plain,
( ! [X0] : true = ifeq(true,true,theorem(or(not(or(sF13,X0)),or(q,X0))),true)
| ~ spl20_12
| ~ spl20_105 ),
inference(superposition,[],[f982,f19818]) ).
fof(f19869,plain,
( ! [X0] : true = theorem(or(not(or(sF13,X0)),or(q,X0)))
| ~ spl20_12
| ~ spl20_105 ),
inference(forward_demodulation,[],[f19820,f1]) ).
fof(f19953,plain,
( ! [X0] : true = ifeq(true,true,ifeq(theorem(or(sF13,X0)),true,theorem(or(q,X0)),true),true)
| ~ spl20_12
| ~ spl20_105 ),
inference(superposition,[],[f26,f19869]) ).
fof(f20026,plain,
( ! [X0] : true = ifeq(theorem(or(sF13,X0)),true,theorem(or(q,X0)),true)
| ~ spl20_12
| ~ spl20_105 ),
inference(forward_demodulation,[],[f19953,f1]) ).
fof(f20106,plain,
( true = ifeq(true,true,theorem(or(q,sF18)),true)
| ~ spl20_12
| ~ spl20_82
| ~ spl20_105 ),
inference(superposition,[],[f20026,f16856]) ).
fof(f20125,plain,
( true = theorem(or(q,sF18))
| ~ spl20_12
| ~ spl20_82
| ~ spl20_105 ),
inference(forward_demodulation,[],[f20106,f1]) ).
fof(f20131,definition,
( spl20_108
<=> true = theorem(or(q,sF18)) ),
introduced(definition,[new_symbols(definition,[spl20_108])],[avatar_definition]) ).
fof(f20133,plain,
( true = theorem(or(q,sF18))
| ~ spl20_108 ),
inference(avatar_component_clause,[],[f20131]) ).
fof(f20134,plain,
( spl20_108
| ~ spl20_12
| ~ spl20_82
| ~ spl20_105 ),
inference(avatar_split_clause,[],[f20125,f19816,f16854,f139,f20131]) ).
fof(f20136,plain,
( true = ifeq(true,true,theorem(or(sF18,q)),true)
| ~ spl20_108 ),
inference(superposition,[],[f180,f20133]) ).
fof(f20181,plain,
( true = theorem(or(sF18,q))
| ~ spl20_108 ),
inference(forward_demodulation,[],[f20136,f1]) ).
fof(f20193,definition,
( spl20_109
<=> true = theorem(or(sF18,q)) ),
introduced(definition,[new_symbols(definition,[spl20_109])],[avatar_definition]) ).
fof(f20195,plain,
( true = theorem(or(sF18,q))
| ~ spl20_109 ),
inference(avatar_component_clause,[],[f20193]) ).
fof(f20196,plain,
( spl20_109
| ~ spl20_108 ),
inference(avatar_split_clause,[],[f20181,f20131,f20193]) ).
fof(f20200,plain,
( true = ifeq(true,true,theorem(or(sF18,sF8)),true)
| ~ spl20_17
| ~ spl20_109 ),
inference(superposition,[],[f895,f20195]) ).
fof(f20251,plain,
( true = theorem(or(sF18,sF8))
| ~ spl20_17
| ~ spl20_109 ),
inference(forward_demodulation,[],[f20200,f1]) ).
fof(f20422,definition,
( spl20_112
<=> true = theorem(or(sF18,sF8)) ),
introduced(definition,[new_symbols(definition,[spl20_112])],[avatar_definition]) ).
fof(f20424,plain,
( true = theorem(or(sF18,sF8))
| ~ spl20_112 ),
inference(avatar_component_clause,[],[f20422]) ).
fof(f20425,plain,
( spl20_112
| ~ spl20_17
| ~ spl20_109 ),
inference(avatar_split_clause,[],[f20251,f20193,f317,f20422]) ).
fof(f20447,plain,
( true = ifeq(true,true,theorem(or(not(not(sF8)),sF18)),true)
| ~ spl20_112 ),
inference(superposition,[],[f1608,f20424]) ).
fof(f20479,plain,
( true = theorem(or(not(not(sF8)),sF18))
| ~ spl20_112 ),
inference(forward_demodulation,[],[f20447,f1]) ).
fof(f20490,plain,
( true = theorem(or(not(sF9),sF18))
| ~ spl20_11
| ~ spl20_112 ),
inference(forward_demodulation,[],[f20479,f132]) ).
fof(f22751,definition,
( spl20_125
<=> true = theorem(or(not(sF9),sF18)) ),
introduced(definition,[new_symbols(definition,[spl20_125])],[avatar_definition]) ).
fof(f22753,plain,
( true = theorem(or(not(sF9),sF18))
| ~ spl20_125 ),
inference(avatar_component_clause,[],[f22751]) ).
fof(f22754,plain,
( spl20_125
| ~ spl20_11
| ~ spl20_112 ),
inference(avatar_split_clause,[],[f20490,f20422,f130,f22751]) ).
fof(f22755,plain,
( true = ifeq(true,true,theorem(or(sF11,or(sF6,sF18))),true)
| ~ spl20_7
| ~ spl20_19
| ~ spl20_125 ),
inference(superposition,[],[f528,f22753]) ).
fof(f22815,plain,
( true = theorem(or(sF11,or(sF6,sF18)))
| ~ spl20_7
| ~ spl20_19
| ~ spl20_125 ),
inference(forward_demodulation,[],[f22755,f1]) ).
fof(f22938,definition,
( spl20_126
<=> true = theorem(or(sF11,or(sF6,sF18))) ),
introduced(definition,[new_symbols(definition,[spl20_126])],[avatar_definition]) ).
fof(f22940,plain,
( true = theorem(or(sF11,or(sF6,sF18)))
| ~ spl20_126 ),
inference(avatar_component_clause,[],[f22938]) ).
fof(f22941,plain,
( spl20_126
| ~ spl20_7
| ~ spl20_19
| ~ spl20_125 ),
inference(avatar_split_clause,[],[f22815,f22751,f367,f106,f22938]) ).
fof(f22948,plain,
( true = ifeq(true,true,theorem(or(sF6,or(sF11,sF18))),true)
| ~ spl20_126 ),
inference(superposition,[],[f173,f22940]) ).
fof(f23006,plain,
( true = theorem(or(sF6,or(sF11,sF18)))
| ~ spl20_126 ),
inference(forward_demodulation,[],[f22948,f1]) ).
fof(f23014,definition,
( spl20_127
<=> true = theorem(or(sF6,or(sF11,sF18))) ),
introduced(definition,[new_symbols(definition,[spl20_127])],[avatar_definition]) ).
fof(f23016,plain,
( true = theorem(or(sF6,or(sF11,sF18)))
| ~ spl20_127 ),
inference(avatar_component_clause,[],[f23014]) ).
fof(f23017,plain,
( spl20_127
| ~ spl20_126 ),
inference(avatar_split_clause,[],[f23006,f22938,f23014]) ).
fof(f23021,plain,
( true = ifeq(true,true,theorem(or(sF11,sF18)),true)
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_127 ),
inference(superposition,[],[f269,f23016]) ).
fof(f23081,plain,
( true = theorem(or(sF11,sF18))
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_127 ),
inference(forward_demodulation,[],[f23021,f1]) ).
fof(f23088,definition,
( spl20_128
<=> true = theorem(or(sF11,sF18)) ),
introduced(definition,[new_symbols(definition,[spl20_128])],[avatar_definition]) ).
fof(f23090,plain,
( true = theorem(or(sF11,sF18))
| ~ spl20_128 ),
inference(avatar_component_clause,[],[f23088]) ).
fof(f23091,plain,
( spl20_128
| ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_127 ),
inference(avatar_split_clause,[],[f23081,f23014,f246,f203,f125,f87,f23088]) ).
fof(f23099,plain,
( true = ifeq(true,true,theorem(or(sF18,sF11)),true)
| ~ spl20_128 ),
inference(superposition,[],[f180,f23090]) ).
fof(f23144,plain,
( true = theorem(or(sF18,sF11))
| ~ spl20_128 ),
inference(forward_demodulation,[],[f23099,f1]) ).
fof(f23155,definition,
( spl20_129
<=> true = theorem(or(sF18,sF11)) ),
introduced(definition,[new_symbols(definition,[spl20_129])],[avatar_definition]) ).
fof(f23157,plain,
( true = theorem(or(sF18,sF11))
| ~ spl20_129 ),
inference(avatar_component_clause,[],[f23155]) ).
fof(f23158,plain,
( spl20_129
| ~ spl20_128 ),
inference(avatar_split_clause,[],[f23144,f23088,f23155]) ).
fof(f23188,plain,
( true = ifeq(true,true,theorem(or(not(or(not(sF11),sF18)),sF18)),true)
| ~ spl20_129 ),
inference(superposition,[],[f10159,f23157]) ).
fof(f23204,plain,
( true = theorem(or(not(or(not(sF11),sF18)),sF18))
| ~ spl20_129 ),
inference(forward_demodulation,[],[f23188,f1]) ).
fof(f23217,plain,
( true = theorem(or(not(or(sF14,sF18)),sF18))
| ~ spl20_5
| ~ spl20_129 ),
inference(forward_demodulation,[],[f23204,f98]) ).
fof(f23221,plain,
( true = ifeq(true,true,sF19,true)
| ~ spl20_1
| ~ spl20_5
| ~ spl20_72
| ~ spl20_129 ),
inference(backward_demodulation,[],[f14516,f23217]) ).
fof(f23222,plain,
( true = sF19
| ~ spl20_1
| ~ spl20_5
| ~ spl20_72
| ~ spl20_129 ),
inference(forward_demodulation,[],[f23221,f1]) ).
fof(f23223,plain,
( $false
| ~ spl20_1
| spl20_2
| ~ spl20_5
| ~ spl20_72
| ~ spl20_129 ),
inference(forward_subsumption_resolution,[],[f23222,f77]) ).
fof(f23224,plain,
( ~ spl20_1
| spl20_2
| ~ spl20_5
| ~ spl20_72
| ~ spl20_129 ),
inference(avatar_contradiction_clause,[],[f23223]) ).
cnf(s1,plain,
spl20_1,
inference(sat_conversion,[],[f73]) ).
cnf(s2,plain,
~ spl20_2,
inference(sat_conversion,[],[f78]) ).
cnf(s3,plain,
spl20_3,
inference(sat_conversion,[],[f85]) ).
cnf(s4,plain,
spl20_4,
inference(sat_conversion,[],[f90]) ).
cnf(s5,plain,
spl20_5,
inference(sat_conversion,[],[f99]) ).
cnf(s6,plain,
spl20_6,
inference(sat_conversion,[],[f104]) ).
cnf(s7,plain,
spl20_7,
inference(sat_conversion,[],[f109]) ).
cnf(s8,plain,
spl20_8,
inference(sat_conversion,[],[f114]) ).
cnf(s9,plain,
spl20_9,
inference(sat_conversion,[],[f119]) ).
cnf(s10,plain,
spl20_10,
inference(sat_conversion,[],[f128]) ).
cnf(s11,plain,
spl20_11,
inference(sat_conversion,[],[f133]) ).
cnf(s12,plain,
spl20_12,
inference(sat_conversion,[],[f142]) ).
cnf(s13,plain,
spl20_13,
inference(sat_conversion,[],[f147]) ).
cnf(s14,plain,
spl20_14,
inference(sat_conversion,[],[f206]) ).
cnf(s15,plain,
spl20_15,
inference(sat_conversion,[],[f249]) ).
cnf(s16,plain,
spl20_16,
inference(sat_conversion,[],[f295]) ).
cnf(s17,plain,
spl20_17,
inference(sat_conversion,[],[f320]) ).
cnf(s18,plain,
spl20_18,
inference(sat_conversion,[],[f345]) ).
cnf(s19,plain,
spl20_19,
inference(sat_conversion,[],[f370]) ).
cnf(s20,plain,
spl20_20,
inference(sat_conversion,[],[f392]) ).
cnf(s21,plain,
spl20_21,
inference(sat_conversion,[],[f414]) ).
cnf(s24,plain,
( ~ spl20_3
| ~ spl20_15
| spl20_24 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s25,plain,
( ~ spl20_8
| ~ spl20_11
| ~ spl20_17
| ~ spl20_21
| ~ spl20_24
| spl20_25 ),
inference(sat_conversion,[],[f1963]) ).
cnf(s27,plain,
( ~ spl20_25
| spl20_27 ),
inference(sat_conversion,[],[f2232]) ).
cnf(s42,plain,
( ~ spl20_5
| ~ spl20_16
| spl20_42 ),
inference(sat_conversion,[],[f5433]) ).
cnf(s58,plain,
( ~ spl20_8
| ~ spl20_15
| ~ spl20_17
| spl20_58 ),
inference(sat_conversion,[],[f12192]) ).
cnf(s61,plain,
( ~ spl20_11
| ~ spl20_58
| spl20_61 ),
inference(sat_conversion,[],[f12453]) ).
cnf(s62,plain,
( ~ spl20_7
| ~ spl20_19
| ~ spl20_61
| spl20_62 ),
inference(sat_conversion,[],[f12626]) ).
cnf(s65,plain,
( ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27
| spl20_65 ),
inference(sat_conversion,[],[f13811]) ).
cnf(s70,plain,
( ~ spl20_12
| ~ spl20_42
| spl20_70 ),
inference(sat_conversion,[],[f14255]) ).
cnf(s71,plain,
( ~ spl20_65
| ~ spl20_70
| spl20_71 ),
inference(sat_conversion,[],[f14422]) ).
cnf(s72,plain,
( ~ spl20_71
| spl20_72 ),
inference(sat_conversion,[],[f14478]) ).
cnf(s82,plain,
( ~ spl20_5
| ~ spl20_7
| ~ spl20_9
| ~ spl20_13
| ~ spl20_18
| ~ spl20_19
| ~ spl20_20
| ~ spl20_27
| spl20_82 ),
inference(sat_conversion,[],[f16857]) ).
cnf(s84,plain,
( ~ spl20_62
| spl20_84 ),
inference(sat_conversion,[],[f16986]) ).
cnf(s85,plain,
( ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_84
| spl20_85 ),
inference(sat_conversion,[],[f17058]) ).
cnf(s98,plain,
( ~ spl20_3
| ~ spl20_6
| ~ spl20_21
| ~ spl20_85
| spl20_98 ),
inference(sat_conversion,[],[f18635]) ).
cnf(s104,plain,
( ~ spl20_98
| spl20_104 ),
inference(sat_conversion,[],[f19739]) ).
cnf(s105,plain,
( ~ spl20_16
| ~ spl20_104
| spl20_105 ),
inference(sat_conversion,[],[f19819]) ).
cnf(s108,plain,
( ~ spl20_12
| ~ spl20_82
| ~ spl20_105
| spl20_108 ),
inference(sat_conversion,[],[f20134]) ).
cnf(s109,plain,
( ~ spl20_108
| spl20_109 ),
inference(sat_conversion,[],[f20196]) ).
cnf(s112,plain,
( ~ spl20_17
| ~ spl20_109
| spl20_112 ),
inference(sat_conversion,[],[f20425]) ).
cnf(s125,plain,
( ~ spl20_11
| ~ spl20_112
| spl20_125 ),
inference(sat_conversion,[],[f22754]) ).
cnf(s126,plain,
( ~ spl20_7
| ~ spl20_19
| ~ spl20_125
| spl20_126 ),
inference(sat_conversion,[],[f22941]) ).
cnf(s127,plain,
( ~ spl20_126
| spl20_127 ),
inference(sat_conversion,[],[f23017]) ).
cnf(s128,plain,
( ~ spl20_4
| ~ spl20_10
| ~ spl20_14
| ~ spl20_15
| ~ spl20_127
| spl20_128 ),
inference(sat_conversion,[],[f23091]) ).
cnf(s129,plain,
( ~ spl20_128
| spl20_129 ),
inference(sat_conversion,[],[f23158]) ).
cnf(s130,plain,
( ~ spl20_1
| spl20_2
| ~ spl20_5
| ~ spl20_72
| ~ spl20_129 ),
inference(sat_conversion,[],[f23224]) ).
cnf(s134,plain,
spl20_58,
inference(rat,[],[s58,s15,s17,s8]) ).
cnf(s136,plain,
spl20_61,
inference(rat,[],[s61,s11,s134]) ).
cnf(s140,plain,
spl20_62,
inference(rat,[],[s62,s136,s19,s7]) ).
cnf(s141,plain,
spl20_84,
inference(rat,[],[s84,s140]) ).
cnf(s145,plain,
spl20_42,
inference(rat,[],[s42,s16,s5]) ).
cnf(s146,plain,
spl20_70,
inference(rat,[],[s70,s12,s145]) ).
cnf(s147,plain,
spl20_85,
inference(rat,[],[s85,s141,s10,s15,s14,s4]) ).
cnf(s174,plain,
spl20_98,
inference(rat,[],[s98,s147,s6,s21,s3]) ).
cnf(s177,plain,
spl20_24,
inference(rat,[],[s24,s15,s3]) ).
cnf(s178,plain,
spl20_104,
inference(rat,[],[s104,s174]) ).
cnf(s183,plain,
spl20_25,
inference(rat,[],[s25,s8,s11,s21,s17,s177]) ).
cnf(s185,plain,
spl20_105,
inference(rat,[],[s105,s16,s178]) ).
cnf(s192,plain,
spl20_27,
inference(rat,[],[s27,s183]) ).
cnf(s202,plain,
spl20_82,
inference(rat,[],[s82,s5,s7,s20,s19,s18,s13,s9,s192]) ).
cnf(s203,plain,
spl20_65,
inference(rat,[],[s65,s5,s7,s20,s19,s18,s13,s9,s192]) ).
cnf(s216,plain,
spl20_108,
inference(rat,[],[s108,s185,s12,s202]) ).
cnf(s218,plain,
spl20_71,
inference(rat,[],[s71,s146,s203]) ).
cnf(s221,plain,
spl20_109,
inference(rat,[],[s109,s216]) ).
cnf(s223,plain,
spl20_72,
inference(rat,[],[s72,s218]) ).
cnf(s225,plain,
spl20_112,
inference(rat,[],[s112,s17,s221]) ).
cnf(s228,plain,
spl20_125,
inference(rat,[],[s125,s11,s225]) ).
cnf(s235,plain,
spl20_126,
inference(rat,[],[s126,s7,s19,s228]) ).
cnf(s236,plain,
spl20_127,
inference(rat,[],[s127,s235]) ).
cnf(s237,plain,
spl20_128,
inference(rat,[],[s128,s4,s10,s15,s14,s236]) ).
cnf(s238,plain,
spl20_129,
inference(rat,[],[s129,s237]) ).
cnf(s239,plain,
~ spl20_1,
inference(rat,[],[s130,s238,s223,s5,s2]) ).
cnf(s240,plain,
$false,
inference(rat,[],[s1,s239]) ).
fof(f23225,plain,
$false,
inference(avatar_sat_refutation,[],[s240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL304-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n020.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 15:34:19 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/0.42 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
% 40.15/6.57 % (3547643)Detected a unit-equality problem, will run specialized UEQ schedule.
% 40.15/6.57 % (3547743)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=2744407220:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 40.15/6.57 % (3547744)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=467629654:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 40.15/6.57 % (3547746)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=310240147:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 40.15/6.57 % (3547745)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3314291733:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 40.15/6.57 % (3547748)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=990322736:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 40.15/6.57 % (3547749)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=1273555550:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 40.15/6.57 % (3547747)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2954589035:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 40.15/6.57 % (3547746)Instruction limit reached!
% 40.15/6.57 % (3547746)------------------------------
% 40.15/6.57 % (3547746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547746)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547746)Termination reason: Instruction limit
% 40.15/6.57 % (3547746)Termination phase: Saturation
% 40.15/6.57 % (3547746)Time elapsed: 0.084 s
% 40.15/6.57 % (3547746)Peak memory usage: 89 MB
% 40.15/6.57 % (3547746)Instructions burned: 137 (million)
% 40.15/6.57 % (3547747)Instruction limit reached!
% 40.15/6.57 % (3547747)------------------------------
% 40.15/6.57 % (3547747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547747)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547747)Termination reason: Instruction limit
% 40.15/6.57 % (3547747)Termination phase: Saturation
% 40.15/6.57 % (3547747)Time elapsed: 0.069 s
% 40.15/6.57 % (3547747)Peak memory usage: 89 MB
% 40.15/6.57 % (3547747)Instructions burned: 184 (million)
% 40.15/6.57 % (3547748)Instruction limit reached!
% 40.15/6.57 % (3547748)------------------------------
% 40.15/6.57 % (3547748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547748)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547748)Termination reason: Instruction limit
% 40.15/6.57 % (3547748)Termination phase: Saturation
% 40.15/6.57 % (3547748)Time elapsed: 0.176 s
% 40.15/6.57 % (3547748)Peak memory usage: 90 MB
% 40.15/6.57 % (3547748)Instructions burned: 258 (million)
% 40.15/6.57 % (3547768)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3579892186:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 40.15/6.57 % (3547763)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3530876632:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 40.15/6.57 % (3547778)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=765511785:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 40.15/6.57 % (3547778)Instruction limit reached!
% 40.15/6.57 % (3547778)------------------------------
% 40.15/6.57 % (3547778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547778)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547778)Termination reason: Instruction limit
% 40.15/6.57 % (3547778)Termination phase: Saturation
% 40.15/6.57 % (3547778)Time elapsed: 0.105 s
% 40.15/6.57 % (3547778)Peak memory usage: 88 MB
% 40.15/6.57 % (3547778)Instructions burned: 215 (million)
% 40.15/6.57 % (3547782)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=2272023213:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 40.15/6.57 % (3547782)Instruction limit reached!
% 40.15/6.57 % (3547782)------------------------------
% 40.15/6.57 % (3547782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547782)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547782)Termination reason: Instruction limit
% 40.15/6.57 % (3547782)Termination phase: Saturation
% 40.15/6.57 % (3547782)Time elapsed: 0.245 s
% 40.15/6.57 % (3547782)Peak memory usage: 93 MB
% 40.15/6.57 % (3547782)Instructions burned: 317 (million)
% 40.15/6.57 % (3547749)Instruction limit reached!
% 40.15/6.57 % (3547749)------------------------------
% 40.15/6.57 % (3547749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547749)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547749)Termination reason: Instruction limit
% 40.15/6.57 % (3547749)Termination phase: Saturation
% 40.15/6.57 % (3547749)Time elapsed: 0.849 s
% 40.15/6.57 % (3547749)Peak memory usage: 101 MB
% 40.15/6.57 % (3547749)Instructions burned: 1187 (million)
% 40.15/6.57 % (3547794)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=2355148034:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2989 on theBenchmark for (2989ds/12125Mi)
% 40.15/6.57 % (3547796)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=4205837073:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2989 on theBenchmark for (2989ds/2836Mi)
% 40.15/6.57 % (3547768)Instruction limit reached!
% 40.15/6.57 % (3547768)------------------------------
% 40.15/6.57 % (3547768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547768)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547768)Termination reason: Instruction limit
% 40.15/6.57 % (3547768)Termination phase: Saturation
% 40.15/6.57 % (3547768)Time elapsed: 1.851 s
% 40.15/6.57 % (3547768)Peak memory usage: 170 MB
% 40.15/6.57 % (3547768)Instructions burned: 4949 (million)
% 40.15/6.57 % (3547763)Instruction limit reached!
% 40.15/6.57 % (3547763)------------------------------
% 40.15/6.57 % (3547763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547763)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547763)Termination reason: Instruction limit
% 40.15/6.57 % (3547763)Termination phase: Saturation
% 40.15/6.57 % (3547763)Time elapsed: 1.898 s
% 40.15/6.57 % (3547763)Peak memory usage: 143 MB
% 40.15/6.57 % (3547763)Instructions burned: 2051 (million)
% 40.15/6.57 % (3547824)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=996859768:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2977 on theBenchmark for (2977ds/14534Mi)
% 40.15/6.57 % (3547825)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1928780977:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/11832Mi)
% 40.15/6.57 % (3547796)Instruction limit reached!
% 40.15/6.57 % (3547796)------------------------------
% 40.15/6.57 % (3547796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.15/6.57 % (3547796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.15/6.57 % (3547796)CaDiCaL version: 2.1.3
% 40.15/6.57 % (3547796)Termination reason: Instruction limit
% 40.15/6.57 % (3547796)Termination phase: Saturation
% 40.15/6.57 % (3547796)Time elapsed: 2.602 s
% 40.15/6.57 % (3547796)Peak memory usage: 121 MB
% 40.15/6.57 % (3547796)Instructions burned: 2836 (million)
% 40.15/6.57 % (3547843)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=2091156131:i=2279:fgj=on:bd=all_2960 on theBenchmark for (2960ds/2279Mi)
% 40.15/6.57 % (3547743)First to succeed.
% 40.15/6.57 % (3547743)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3547643"
% 40.15/6.57 % (3547743)Refutation found. Thanks to Tanya!
% 40.15/6.57 % SZS status Unsatisfiable for theBenchmark
% 40.15/6.57 % SZS output start Proof for theBenchmark
% See solution above
% 40.90/6.85 % (3547743)------------------------------
% 40.90/6.85 % (3547743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.90/6.85 % (3547743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.90/6.85 % (3547743)CaDiCaL version: 2.1.3
% 40.90/6.85 % (3547743)Termination reason: Refutation
% 40.90/6.85 % (3547743)Time elapsed: 5.101 s
% 40.90/6.85 % (3547743)Peak memory usage: 177 MB
% 40.90/6.85 % (3547743)Instructions burned: 5420 (million)
% 40.90/6.85 % (3547743)------------------------------
% 40.90/6.85 % (3547743)------------------------------
% 40.90/6.85 % (3547643)Success in time 5.692 s
% 40.90/6.85 % Vampire exiting
%------------------------------------------------------------------------------