%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG020+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 09:20:05 AM UTC 2026
% Result : Theorem 0.21s 0.30s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 36
% Syntax : Number of formulae : 358 ( 43 unt; 31 def)
% Number of atoms : 1113 ( 539 equ)
% Maximal formula atoms : 72 ( 3 avg)
% Number of connectives : 1172 ( 417 ~; 496 |; 226 &)
% ( 31 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 33 ( 31 usr; 32 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( op1(e10,e10) = e10
& op1(e10,e11) = e11
& op1(e10,e12) = e12
& op1(e10,e13) = e13
& op1(e11,e10) = e11
& op1(e11,e11) = e10
& op1(e11,e12) = e13
& op1(e11,e13) = e12
& op1(e12,e10) = e12
& op1(e12,e11) = e13
& op1(e12,e12) = e10
& op1(e12,e13) = e11
& op1(e13,e10) = e13
& op1(e13,e11) = e12
& op1(e13,e12) = e11
& op1(e13,e13) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(e20,e20) = e20
& op2(e20,e21) = e21
& op2(e20,e22) = e22
& op2(e20,e23) = e23
& op2(e21,e20) = e21
& op2(e21,e21) = e23
& op2(e21,e22) = e20
& op2(e21,e23) = e22
& op2(e22,e20) = e22
& op2(e22,e21) = e20
& op2(e22,e22) = e23
& op2(e22,e23) = e21
& op2(e23,e20) = e23
& op2(e23,e21) = e22
& op2(e23,e22) = e21
& op2(e23,e23) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,conjecture,
( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f7,negated_conjecture,
~ ( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13 ) ),
inference(flattening,[],[f8]) ).
fof(f10,plain,
e12 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f12,plain,
e11 != e12,
inference(cnf_transformation,[],[f1]) ).
fof(f13,plain,
e10 != e13,
inference(cnf_transformation,[],[f1]) ).
fof(f14,plain,
e10 != e12,
inference(cnf_transformation,[],[f1]) ).
fof(f15,plain,
e10 != e11,
inference(cnf_transformation,[],[f1]) ).
fof(f16,plain,
e22 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f19,plain,
e20 != e23,
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
e20 != e22,
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
e10 = op1(e13,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f43,plain,
e10 = op1(e12,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f48,plain,
e10 = op1(e11,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f53,plain,
e10 = op1(e10,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f54,plain,
e20 = op2(e23,e23),
inference(cnf_transformation,[],[f5]) ).
fof(f59,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f5]) ).
fof(f70,plain,
( e23 = h(e10)
| e22 = h(e10)
| e21 = h(e10)
| e20 = h(e10) ),
inference(cnf_transformation,[],[f9]) ).
fof(f71,plain,
( e23 = h(e11)
| e22 = h(e11)
| e21 = h(e11)
| e20 = h(e11) ),
inference(cnf_transformation,[],[f9]) ).
fof(f72,plain,
( e23 = h(e12)
| e22 = h(e12)
| e21 = h(e12)
| e20 = h(e12) ),
inference(cnf_transformation,[],[f9]) ).
fof(f73,plain,
( e23 = h(e13)
| e22 = h(e13)
| e21 = h(e13)
| e20 = h(e13) ),
inference(cnf_transformation,[],[f9]) ).
fof(f74,plain,
( e13 = j(e20)
| e12 = j(e20)
| e11 = j(e20)
| e10 = j(e20) ),
inference(cnf_transformation,[],[f9]) ).
fof(f76,plain,
( e13 = j(e22)
| e12 = j(e22)
| e11 = j(e22)
| e10 = j(e22) ),
inference(cnf_transformation,[],[f9]) ).
fof(f77,plain,
( e13 = j(e23)
| e12 = j(e23)
| e11 = j(e23)
| e10 = j(e23) ),
inference(cnf_transformation,[],[f9]) ).
fof(f78,plain,
e13 = j(h(e13)),
inference(cnf_transformation,[],[f9]) ).
fof(f79,plain,
e12 = j(h(e12)),
inference(cnf_transformation,[],[f9]) ).
fof(f80,plain,
e11 = j(h(e11)),
inference(cnf_transformation,[],[f9]) ).
fof(f81,plain,
e10 = j(h(e10)),
inference(cnf_transformation,[],[f9]) ).
fof(f82,plain,
e23 = h(j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f83,plain,
e22 = h(j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f85,plain,
e20 = h(j(e20)),
inference(cnf_transformation,[],[f9]) ).
fof(f86,plain,
j(op2(e23,e23)) = op1(j(e23),j(e23)),
inference(cnf_transformation,[],[f9]) ).
fof(f91,plain,
j(op2(e22,e22)) = op1(j(e22),j(e22)),
inference(cnf_transformation,[],[f9]) ).
fof(f119,definition,
( spl0_1
<=> e20 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f120,plain,
( e20 != h(e10)
| spl0_1 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f121,plain,
( e20 = h(e10)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f119]) ).
fof(f123,definition,
( spl0_2
<=> e21 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f125,plain,
( e21 = h(e10)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f123]) ).
fof(f127,definition,
( spl0_3
<=> e22 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f129,plain,
( e22 = h(e10)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f131,definition,
( spl0_4
<=> e23 = h(e10) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f133,plain,
( e23 = h(e10)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f134,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f70,f131,f127,f123,f119]) ).
fof(f136,definition,
( spl0_5
<=> e20 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f138,plain,
( e20 = h(e11)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f140,definition,
( spl0_6
<=> e21 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f142,plain,
( e21 = h(e11)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f144,definition,
( spl0_7
<=> e22 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f146,plain,
( e22 = h(e11)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f148,definition,
( spl0_8
<=> e23 = h(e11) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f150,plain,
( e23 = h(e11)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f148]) ).
fof(f151,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8 ),
inference(avatar_split_clause,[],[f71,f148,f144,f140,f136]) ).
fof(f153,definition,
( spl0_9
<=> e20 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f155,plain,
( e20 = h(e12)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f157,definition,
( spl0_10
<=> e21 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f159,plain,
( e21 = h(e12)
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f161,definition,
( spl0_11
<=> e22 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f163,plain,
( e22 = h(e12)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f165,definition,
( spl0_12
<=> e23 = h(e12) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f167,plain,
( e23 = h(e12)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f168,plain,
( spl0_9
| spl0_10
| spl0_11
| spl0_12 ),
inference(avatar_split_clause,[],[f72,f165,f161,f157,f153]) ).
fof(f170,definition,
( spl0_13
<=> e20 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f172,plain,
( e20 = h(e13)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f174,definition,
( spl0_14
<=> e21 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f176,plain,
( e21 = h(e13)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f174]) ).
fof(f178,definition,
( spl0_15
<=> e22 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f180,plain,
( e22 = h(e13)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f178]) ).
fof(f182,definition,
( spl0_16
<=> e23 = h(e13) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f184,plain,
( e23 = h(e13)
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,plain,
( spl0_13
| spl0_14
| spl0_15
| spl0_16 ),
inference(avatar_split_clause,[],[f73,f182,f178,f174,f170]) ).
fof(f187,definition,
( spl0_17
<=> e10 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f189,plain,
( e10 = j(e20)
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f187]) ).
fof(f191,definition,
( spl0_18
<=> e11 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f193,plain,
( e11 = j(e20)
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f195,definition,
( spl0_19
<=> e12 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f197,plain,
( e12 = j(e20)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f199,definition,
( spl0_20
<=> e13 = j(e20) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f201,plain,
( e13 = j(e20)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,plain,
( spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f74,f199,f195,f191,f187]) ).
fof(f204,definition,
( spl0_21
<=> e10 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f206,plain,
( e10 = j(e21)
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f208,definition,
( spl0_22
<=> e11 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f209,plain,
( e11 != j(e21)
| spl0_22 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( e11 = j(e21)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f212,definition,
( spl0_23
<=> e12 = j(e21) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f214,plain,
( e12 = j(e21)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f221,definition,
( spl0_25
<=> e10 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f223,plain,
( e10 = j(e22)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f225,definition,
( spl0_26
<=> e11 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f227,plain,
( e11 = j(e22)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f229,definition,
( spl0_27
<=> e12 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f231,plain,
( e12 = j(e22)
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f233,definition,
( spl0_28
<=> e13 = j(e22) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f235,plain,
( e13 = j(e22)
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f236,plain,
( spl0_25
| spl0_26
| spl0_27
| spl0_28 ),
inference(avatar_split_clause,[],[f76,f233,f229,f225,f221]) ).
fof(f238,definition,
( spl0_29
<=> e10 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f240,plain,
( e10 = j(e23)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f242,definition,
( spl0_30
<=> e11 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f244,plain,
( e11 = j(e23)
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f246,definition,
( spl0_31
<=> e12 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f247,plain,
( e12 != j(e23)
| spl0_31 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( e12 = j(e23)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f250,definition,
( spl0_32
<=> e13 = j(e23) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f252,plain,
( e13 = j(e23)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,plain,
( spl0_29
| spl0_30
| spl0_31
| spl0_32 ),
inference(avatar_split_clause,[],[f77,f250,f246,f242,f238]) ).
fof(f254,plain,
( e13 = j(e20)
| ~ spl0_13 ),
inference(superposition,[],[f78,f172]) ).
fof(f255,plain,
( e10 = e13
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_demodulation,[],[f254,f189]) ).
fof(f256,plain,
( $false
| ~ spl0_13
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f255,f13]) ).
fof(f257,plain,
( ~ spl0_13
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f256]) ).
fof(f259,plain,
( e13 = j(e21)
| ~ spl0_14 ),
inference(superposition,[],[f78,f176]) ).
fof(f260,plain,
( e10 = e13
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_demodulation,[],[f259,f206]) ).
fof(f261,plain,
( $false
| ~ spl0_14
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f260,f13]) ).
fof(f262,plain,
( ~ spl0_14
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f261]) ).
fof(f265,plain,
( e13 = j(e22)
| ~ spl0_15 ),
inference(superposition,[],[f78,f180]) ).
fof(f272,plain,
( e13 = j(e23)
| ~ spl0_16 ),
inference(superposition,[],[f78,f184]) ).
fof(f276,plain,
( spl0_20
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f254,f170,f199]) ).
fof(f286,plain,
( e12 = j(e20)
| ~ spl0_9 ),
inference(superposition,[],[f79,f155]) ).
fof(f287,plain,
( spl0_19
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f286,f153,f195]) ).
fof(f289,plain,
( e12 = j(e21)
| ~ spl0_10 ),
inference(superposition,[],[f79,f159]) ).
fof(f290,plain,
( e10 = e12
| ~ spl0_10
| ~ spl0_21 ),
inference(forward_demodulation,[],[f289,f206]) ).
fof(f291,plain,
( $false
| ~ spl0_10
| ~ spl0_21 ),
inference(forward_subsumption_resolution,[],[f290,f14]) ).
fof(f292,plain,
( ~ spl0_10
| ~ spl0_21 ),
inference(avatar_contradiction_clause,[],[f291]) ).
fof(f293,plain,
( e11 = e12
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_demodulation,[],[f289,f210]) ).
fof(f294,plain,
( $false
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f293,f12]) ).
fof(f295,plain,
( ~ spl0_10
| ~ spl0_22 ),
inference(avatar_contradiction_clause,[],[f294]) ).
fof(f298,plain,
( e11 = j(e20)
| ~ spl0_5 ),
inference(superposition,[],[f80,f138]) ).
fof(f301,plain,
( e12 = e13
| ~ spl0_14
| ~ spl0_23 ),
inference(forward_demodulation,[],[f259,f214]) ).
fof(f304,plain,
( $false
| ~ spl0_14
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f301,f10]) ).
fof(f305,plain,
( ~ spl0_14
| ~ spl0_23 ),
inference(avatar_contradiction_clause,[],[f304]) ).
fof(f308,plain,
( spl0_28
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f265,f178,f233]) ).
fof(f330,plain,
( e12 = j(e22)
| ~ spl0_11 ),
inference(superposition,[],[f79,f163]) ).
fof(f331,plain,
( spl0_27
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f330,f161,f229]) ).
fof(f335,plain,
( e12 = j(e23)
| ~ spl0_12 ),
inference(superposition,[],[f79,f167]) ).
fof(f346,plain,
( e10 = j(e21)
| ~ spl0_2 ),
inference(superposition,[],[f81,f125]) ).
fof(f350,plain,
( e10 = j(e20)
| ~ spl0_1 ),
inference(superposition,[],[f81,f121]) ).
fof(f355,plain,
( e10 = j(e22)
| ~ spl0_3 ),
inference(superposition,[],[f81,f129]) ).
fof(f361,plain,
( e10 = j(e23)
| ~ spl0_4 ),
inference(superposition,[],[f81,f133]) ).
fof(f364,plain,
( spl0_21
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f346,f123,f204]) ).
fof(f376,plain,
( spl0_29
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f361,f131,f238]) ).
fof(f385,plain,
( spl0_17
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f350,f119,f187]) ).
fof(f414,plain,
( op1(e12,e12) = j(op2(e23,e23))
| ~ spl0_31 ),
inference(superposition,[],[f86,f248]) ).
fof(f415,plain,
( op1(e12,e12) = j(e20)
| ~ spl0_31 ),
inference(forward_demodulation,[],[f414,f54]) ).
fof(f416,plain,
( e11 = op1(e12,e12)
| ~ spl0_18
| ~ spl0_31 ),
inference(forward_demodulation,[],[f415,f193]) ).
fof(f417,plain,
( e10 = e11
| ~ spl0_18
| ~ spl0_31 ),
inference(forward_demodulation,[],[f416,f43]) ).
fof(f418,plain,
( $false
| ~ spl0_18
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f417,f15]) ).
fof(f419,plain,
( ~ spl0_18
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f418]) ).
fof(f420,plain,
( $false
| ~ spl0_12
| spl0_31 ),
inference(forward_subsumption_resolution,[],[f335,f247]) ).
fof(f421,plain,
( ~ spl0_12
| spl0_31 ),
inference(avatar_contradiction_clause,[],[f420]) ).
fof(f429,plain,
( e11 = j(e21)
| ~ spl0_6 ),
inference(superposition,[],[f80,f142]) ).
fof(f430,plain,
( $false
| ~ spl0_6
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f429,f209]) ).
fof(f431,plain,
( ~ spl0_6
| spl0_22 ),
inference(avatar_contradiction_clause,[],[f430]) ).
fof(f434,plain,
( e11 = j(e22)
| ~ spl0_7 ),
inference(superposition,[],[f80,f146]) ).
fof(f448,plain,
( op1(e12,e12) = j(op2(e23,e23))
| ~ spl0_31 ),
inference(superposition,[],[f86,f248]) ).
fof(f449,plain,
( e23 = h(e12)
| ~ spl0_31 ),
inference(superposition,[],[f82,f248]) ).
fof(f451,plain,
( op1(e12,e12) = j(e20)
| ~ spl0_31 ),
inference(forward_demodulation,[],[f448,f54]) ).
fof(f452,plain,
( e13 = op1(e12,e12)
| ~ spl0_20
| ~ spl0_31 ),
inference(forward_demodulation,[],[f451,f201]) ).
fof(f453,plain,
( e10 = e13
| ~ spl0_20
| ~ spl0_31 ),
inference(forward_demodulation,[],[f452,f43]) ).
fof(f454,plain,
( $false
| ~ spl0_20
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f453,f13]) ).
fof(f455,plain,
( ~ spl0_20
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f454]) ).
fof(f458,plain,
( e12 = op1(e12,e12)
| ~ spl0_19
| ~ spl0_31 ),
inference(forward_demodulation,[],[f451,f197]) ).
fof(f460,plain,
( e10 = e12
| ~ spl0_19
| ~ spl0_31 ),
inference(forward_demodulation,[],[f458,f43]) ).
fof(f461,plain,
( $false
| ~ spl0_19
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f460,f14]) ).
fof(f462,plain,
( ~ spl0_19
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f461]) ).
fof(f470,plain,
( e20 = h(e10)
| ~ spl0_17 ),
inference(superposition,[],[f85,f189]) ).
fof(f471,plain,
( $false
| spl0_1
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f470,f120]) ).
fof(f472,plain,
( spl0_1
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f471]) ).
fof(f486,plain,
( spl0_25
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f355,f127,f221]) ).
fof(f506,plain,
( e10 = e12
| ~ spl0_11
| ~ spl0_25 ),
inference(forward_demodulation,[],[f330,f223]) ).
fof(f510,plain,
( $false
| ~ spl0_11
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f506,f14]) ).
fof(f511,plain,
( ~ spl0_11
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f510]) ).
fof(f533,plain,
( e22 = h(e12)
| ~ spl0_27 ),
inference(superposition,[],[f83,f231]) ).
fof(f535,plain,
( op1(e10,e10) = j(op2(e23,e23))
| ~ spl0_29 ),
inference(superposition,[],[f86,f240]) ).
fof(f536,plain,
( e23 = h(e10)
| ~ spl0_29 ),
inference(superposition,[],[f82,f240]) ).
fof(f538,plain,
( op1(e10,e10) = j(e20)
| ~ spl0_29 ),
inference(forward_demodulation,[],[f535,f54]) ).
fof(f539,plain,
( e13 = op1(e10,e10)
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f538,f201]) ).
fof(f540,plain,
( e10 = e13
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_demodulation,[],[f539,f53]) ).
fof(f541,plain,
( $false
| ~ spl0_20
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f540,f13]) ).
fof(f542,plain,
( ~ spl0_20
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f541]) ).
fof(f561,plain,
( e11 = j(e23)
| ~ spl0_8 ),
inference(superposition,[],[f80,f150]) ).
fof(f564,plain,
( op1(e11,e11) = j(op2(e23,e23))
| ~ spl0_30 ),
inference(superposition,[],[f86,f244]) ).
fof(f566,plain,
( op1(e11,e11) = j(e20)
| ~ spl0_30 ),
inference(forward_demodulation,[],[f564,f54]) ).
fof(f567,plain,
( e13 = op1(e11,e11)
| ~ spl0_20
| ~ spl0_30 ),
inference(forward_demodulation,[],[f566,f201]) ).
fof(f568,plain,
( e10 = e13
| ~ spl0_20
| ~ spl0_30 ),
inference(forward_demodulation,[],[f567,f48]) ).
fof(f569,plain,
( $false
| ~ spl0_20
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f568,f13]) ).
fof(f570,plain,
( ~ spl0_20
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f569]) ).
fof(f571,plain,
( spl0_26
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f434,f144,f225]) ).
fof(f573,plain,
( spl0_23
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f289,f157,f212]) ).
fof(f575,plain,
( e10 = e11
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f227,f223]) ).
fof(f582,plain,
( $false
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f575,f15]) ).
fof(f583,plain,
( ~ spl0_25
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f582]) ).
fof(f584,plain,
( spl0_18
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f298,f136,f191]) ).
fof(f606,plain,
( e22 = h(e10)
| ~ spl0_25 ),
inference(superposition,[],[f83,f223]) ).
fof(f607,plain,
( op1(e13,e13) = j(op2(e23,e23))
| ~ spl0_32 ),
inference(superposition,[],[f86,f252]) ).
fof(f609,plain,
( op1(e13,e13) = j(e20)
| ~ spl0_32 ),
inference(forward_demodulation,[],[f607,f54]) ).
fof(f610,plain,
( e11 = op1(e13,e13)
| ~ spl0_18
| ~ spl0_32 ),
inference(forward_demodulation,[],[f609,f193]) ).
fof(f611,plain,
( e10 = e11
| ~ spl0_18
| ~ spl0_32 ),
inference(forward_demodulation,[],[f610,f38]) ).
fof(f612,plain,
( $false
| ~ spl0_18
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f611,f15]) ).
fof(f613,plain,
( ~ spl0_18
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f612]) ).
fof(f644,plain,
( e12 = j(e20)
| ~ spl0_9 ),
inference(superposition,[],[f79,f155]) ).
fof(f651,plain,
( op1(e13,e13) = j(op2(e23,e23))
| ~ spl0_32 ),
inference(superposition,[],[f86,f252]) ).
fof(f653,plain,
( op1(e13,e13) = j(e20)
| ~ spl0_32 ),
inference(forward_demodulation,[],[f651,f54]) ).
fof(f654,plain,
( e12 = op1(e13,e13)
| ~ spl0_19
| ~ spl0_32 ),
inference(forward_demodulation,[],[f653,f197]) ).
fof(f655,plain,
( e10 = e12
| ~ spl0_19
| ~ spl0_32 ),
inference(forward_demodulation,[],[f654,f38]) ).
fof(f656,plain,
( $false
| ~ spl0_19
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f655,f14]) ).
fof(f657,plain,
( ~ spl0_19
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f656]) ).
fof(f673,plain,
( e20 = e23
| ~ spl0_1
| ~ spl0_29 ),
inference(forward_demodulation,[],[f536,f121]) ).
fof(f674,plain,
( $false
| ~ spl0_1
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f673,f19]) ).
fof(f675,plain,
( ~ spl0_1
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f674]) ).
fof(f693,plain,
( op1(e10,e10) = j(op2(e23,e23))
| ~ spl0_29 ),
inference(superposition,[],[f86,f240]) ).
fof(f695,plain,
( op1(e10,e10) = j(e20)
| ~ spl0_29 ),
inference(forward_demodulation,[],[f693,f54]) ).
fof(f696,plain,
( e12 = op1(e10,e10)
| ~ spl0_19
| ~ spl0_29 ),
inference(forward_demodulation,[],[f695,f197]) ).
fof(f697,plain,
( e10 = e12
| ~ spl0_19
| ~ spl0_29 ),
inference(forward_demodulation,[],[f696,f53]) ).
fof(f698,plain,
( $false
| ~ spl0_19
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f697,f14]) ).
fof(f699,plain,
( ~ spl0_19
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f698]) ).
fof(f706,plain,
( e11 = op1(e10,e10)
| ~ spl0_18
| ~ spl0_29 ),
inference(forward_demodulation,[],[f695,f193]) ).
fof(f711,plain,
( e10 = e11
| ~ spl0_18
| ~ spl0_29 ),
inference(forward_demodulation,[],[f706,f53]) ).
fof(f712,plain,
( $false
| ~ spl0_18
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f711,f15]) ).
fof(f713,plain,
( ~ spl0_18
| ~ spl0_29 ),
inference(avatar_contradiction_clause,[],[f712]) ).
fof(f715,plain,
( spl0_31
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f335,f165,f246]) ).
fof(f726,plain,
( spl0_30
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f561,f148,f242]) ).
fof(f792,plain,
( op1(e13,e13) = j(op2(e22,e22))
| ~ spl0_28 ),
inference(superposition,[],[f91,f235]) ).
fof(f793,plain,
( op1(e13,e13) = j(e23)
| ~ spl0_28 ),
inference(forward_demodulation,[],[f792,f59]) ).
fof(f794,plain,
( e11 = op1(e13,e13)
| ~ spl0_28
| ~ spl0_30 ),
inference(forward_demodulation,[],[f793,f244]) ).
fof(f795,plain,
( e10 = e11
| ~ spl0_28
| ~ spl0_30 ),
inference(forward_demodulation,[],[f794,f38]) ).
fof(f796,plain,
( $false
| ~ spl0_28
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f795,f15]) ).
fof(f797,plain,
( ~ spl0_28
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f796]) ).
fof(f806,plain,
( e13 = op1(e13,e13)
| ~ spl0_28
| ~ spl0_32 ),
inference(forward_demodulation,[],[f793,f252]) ).
fof(f817,plain,
( e10 = e13
| ~ spl0_28
| ~ spl0_32 ),
inference(forward_demodulation,[],[f806,f38]) ).
fof(f821,plain,
( $false
| ~ spl0_28
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f817,f13]) ).
fof(f822,plain,
( ~ spl0_28
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f821]) ).
fof(f830,plain,
( e22 = e23
| ~ spl0_11
| ~ spl0_31 ),
inference(forward_demodulation,[],[f449,f163]) ).
fof(f835,plain,
( e12 = op1(e13,e13)
| ~ spl0_28
| ~ spl0_31 ),
inference(forward_demodulation,[],[f793,f248]) ).
fof(f838,plain,
( $false
| ~ spl0_11
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f830,f16]) ).
fof(f839,plain,
( ~ spl0_11
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f838]) ).
fof(f843,plain,
( e10 = e12
| ~ spl0_28
| ~ spl0_31 ),
inference(forward_demodulation,[],[f835,f38]) ).
fof(f847,plain,
( $false
| ~ spl0_28
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f843,f14]) ).
fof(f848,plain,
( ~ spl0_28
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f847]) ).
fof(f878,plain,
( op1(e12,e12) = j(op2(e22,e22))
| ~ spl0_27 ),
inference(superposition,[],[f91,f231]) ).
fof(f881,plain,
( op1(e12,e12) = j(e23)
| ~ spl0_27 ),
inference(forward_demodulation,[],[f878,f59]) ).
fof(f884,plain,
( e11 = op1(e12,e12)
| ~ spl0_27
| ~ spl0_30 ),
inference(forward_demodulation,[],[f881,f244]) ).
fof(f887,plain,
( e10 = e11
| ~ spl0_27
| ~ spl0_30 ),
inference(forward_demodulation,[],[f884,f43]) ).
fof(f890,plain,
( $false
| ~ spl0_27
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f887,f15]) ).
fof(f891,plain,
( ~ spl0_27
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f890]) ).
fof(f893,plain,
( e10 = e12
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_demodulation,[],[f644,f189]) ).
fof(f896,plain,
( e20 = e22
| ~ spl0_1
| ~ spl0_25 ),
inference(forward_demodulation,[],[f606,f121]) ).
fof(f903,plain,
( $false
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f893,f14]) ).
fof(f904,plain,
( ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f903]) ).
fof(f907,plain,
( $false
| ~ spl0_1
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f896,f20]) ).
fof(f908,plain,
( ~ spl0_1
| ~ spl0_25 ),
inference(avatar_contradiction_clause,[],[f907]) ).
fof(f926,plain,
( op1(e10,e10) = j(op2(e22,e22))
| ~ spl0_25 ),
inference(superposition,[],[f91,f223]) ).
fof(f928,plain,
( op1(e10,e10) = j(e23)
| ~ spl0_25 ),
inference(forward_demodulation,[],[f926,f59]) ).
fof(f931,plain,
( e11 = op1(e10,e10)
| ~ spl0_25
| ~ spl0_30 ),
inference(forward_demodulation,[],[f928,f244]) ).
fof(f934,plain,
( e10 = e11
| ~ spl0_25
| ~ spl0_30 ),
inference(forward_demodulation,[],[f931,f53]) ).
fof(f937,plain,
( $false
| ~ spl0_25
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f934,f15]) ).
fof(f938,plain,
( ~ spl0_25
| ~ spl0_30 ),
inference(avatar_contradiction_clause,[],[f937]) ).
fof(f974,plain,
( op1(e11,e11) = j(op2(e22,e22))
| ~ spl0_26 ),
inference(superposition,[],[f91,f227]) ).
fof(f976,plain,
( op1(e11,e11) = j(e23)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f974,f59]) ).
fof(f979,plain,
( e12 = op1(e11,e11)
| ~ spl0_26
| ~ spl0_31 ),
inference(forward_demodulation,[],[f976,f248]) ).
fof(f982,plain,
( e10 = e12
| ~ spl0_26
| ~ spl0_31 ),
inference(forward_demodulation,[],[f979,f48]) ).
fof(f985,plain,
( $false
| ~ spl0_26
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f982,f14]) ).
fof(f986,plain,
( ~ spl0_26
| ~ spl0_31 ),
inference(avatar_contradiction_clause,[],[f985]) ).
fof(f988,plain,
( spl0_32
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f272,f182,f250]) ).
fof(f993,plain,
( e13 = op1(e11,e11)
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_demodulation,[],[f976,f252]) ).
fof(f999,plain,
( e10 = e13
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_demodulation,[],[f993,f48]) ).
fof(f1003,plain,
( $false
| ~ spl0_26
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f999,f13]) ).
fof(f1004,plain,
( ~ spl0_26
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1003]) ).
fof(f1007,plain,
( spl0_11
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f533,f229,f161]) ).
fof(f1031,plain,
( op1(e12,e12) = j(op2(e22,e22))
| ~ spl0_27 ),
inference(superposition,[],[f91,f231]) ).
fof(f1034,plain,
( op1(e12,e12) = j(e23)
| ~ spl0_27 ),
inference(forward_demodulation,[],[f1031,f59]) ).
fof(f1037,plain,
( e13 = op1(e12,e12)
| ~ spl0_27
| ~ spl0_32 ),
inference(forward_demodulation,[],[f1034,f252]) ).
fof(f1040,plain,
( e10 = e13
| ~ spl0_27
| ~ spl0_32 ),
inference(forward_demodulation,[],[f1037,f43]) ).
fof(f1043,plain,
( $false
| ~ spl0_27
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1040,f13]) ).
fof(f1044,plain,
( ~ spl0_27
| ~ spl0_32 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f134]) ).
cnf(s2,plain,
( spl0_5
| spl0_6
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f151]) ).
cnf(s3,plain,
( spl0_9
| spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f168]) ).
cnf(s4,plain,
( spl0_13
| spl0_14
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f185]) ).
cnf(s5,plain,
( spl0_17
| spl0_18
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f202]) ).
cnf(s7,plain,
( spl0_25
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f236]) ).
cnf(s8,plain,
( spl0_29
| spl0_30
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f253]) ).
cnf(s9,plain,
( ~ spl0_13
| ~ spl0_17 ),
inference(sat_conversion,[],[f257]) ).
cnf(s10,plain,
( ~ spl0_14
| ~ spl0_21 ),
inference(sat_conversion,[],[f262]) ).
cnf(s13,plain,
( ~ spl0_13
| spl0_20 ),
inference(sat_conversion,[],[f276]) ).
cnf(s15,plain,
( ~ spl0_9
| spl0_19 ),
inference(sat_conversion,[],[f287]) ).
cnf(s16,plain,
( ~ spl0_10
| ~ spl0_21 ),
inference(sat_conversion,[],[f292]) ).
cnf(s17,plain,
( ~ spl0_10
| ~ spl0_22 ),
inference(sat_conversion,[],[f295]) ).
cnf(s19,plain,
( ~ spl0_14
| ~ spl0_23 ),
inference(sat_conversion,[],[f305]) ).
cnf(s21,plain,
( ~ spl0_15
| spl0_28 ),
inference(sat_conversion,[],[f308]) ).
cnf(s25,plain,
( ~ spl0_11
| spl0_27 ),
inference(sat_conversion,[],[f331]) ).
cnf(s32,plain,
( ~ spl0_2
| spl0_21 ),
inference(sat_conversion,[],[f364]) ).
cnf(s35,plain,
( ~ spl0_4
| spl0_29 ),
inference(sat_conversion,[],[f376]) ).
cnf(s38,plain,
( ~ spl0_1
| spl0_17 ),
inference(sat_conversion,[],[f385]) ).
cnf(s43,plain,
( ~ spl0_18
| ~ spl0_31 ),
inference(sat_conversion,[],[f419]) ).
cnf(s44,plain,
( ~ spl0_12
| spl0_31 ),
inference(sat_conversion,[],[f421]) ).
cnf(s46,plain,
( ~ spl0_6
| spl0_22 ),
inference(sat_conversion,[],[f431]) ).
cnf(s50,plain,
( ~ spl0_20
| ~ spl0_31 ),
inference(sat_conversion,[],[f455]) ).
cnf(s51,plain,
( ~ spl0_19
| ~ spl0_31 ),
inference(sat_conversion,[],[f462]) ).
cnf(s52,plain,
( spl0_1
| ~ spl0_17 ),
inference(sat_conversion,[],[f472]) ).
cnf(s56,plain,
( ~ spl0_3
| spl0_25 ),
inference(sat_conversion,[],[f486]) ).
cnf(s62,plain,
( ~ spl0_11
| ~ spl0_25 ),
inference(sat_conversion,[],[f511]) ).
cnf(s66,plain,
( ~ spl0_20
| ~ spl0_29 ),
inference(sat_conversion,[],[f542]) ).
cnf(s73,plain,
( ~ spl0_20
| ~ spl0_30 ),
inference(sat_conversion,[],[f570]) ).
cnf(s75,plain,
( ~ spl0_7
| spl0_26 ),
inference(sat_conversion,[],[f571]) ).
cnf(s76,plain,
( ~ spl0_10
| spl0_23 ),
inference(sat_conversion,[],[f573]) ).
cnf(s77,plain,
( ~ spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f583]) ).
cnf(s78,plain,
( ~ spl0_5
| spl0_18 ),
inference(sat_conversion,[],[f584]) ).
cnf(s79,plain,
( ~ spl0_18
| ~ spl0_32 ),
inference(sat_conversion,[],[f613]) ).
cnf(s88,plain,
( ~ spl0_19
| ~ spl0_32 ),
inference(sat_conversion,[],[f657]) ).
cnf(s95,plain,
( ~ spl0_1
| ~ spl0_29 ),
inference(sat_conversion,[],[f675]) ).
cnf(s96,plain,
( ~ spl0_19
| ~ spl0_29 ),
inference(sat_conversion,[],[f699]) ).
cnf(s103,plain,
( ~ spl0_18
| ~ spl0_29 ),
inference(sat_conversion,[],[f713]) ).
cnf(s110,plain,
( ~ spl0_12
| spl0_31 ),
inference(sat_conversion,[],[f715]) ).
cnf(s113,plain,
( ~ spl0_8
| spl0_30 ),
inference(sat_conversion,[],[f726]) ).
cnf(s116,plain,
( ~ spl0_28
| ~ spl0_30 ),
inference(sat_conversion,[],[f797]) ).
cnf(s124,plain,
( ~ spl0_28
| ~ spl0_32 ),
inference(sat_conversion,[],[f822]) ).
cnf(s128,plain,
( ~ spl0_11
| ~ spl0_31 ),
inference(sat_conversion,[],[f839]) ).
cnf(s129,plain,
( ~ spl0_28
| ~ spl0_31 ),
inference(sat_conversion,[],[f848]) ).
cnf(s134,plain,
( ~ spl0_27
| ~ spl0_30 ),
inference(sat_conversion,[],[f891]) ).
cnf(s136,plain,
( ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f904]) ).
cnf(s138,plain,
( ~ spl0_1
| ~ spl0_25 ),
inference(sat_conversion,[],[f908]) ).
cnf(s141,plain,
( ~ spl0_25
| ~ spl0_30 ),
inference(sat_conversion,[],[f938]) ).
cnf(s152,plain,
( ~ spl0_26
| ~ spl0_31 ),
inference(sat_conversion,[],[f986]) ).
cnf(s156,plain,
( ~ spl0_16
| spl0_32 ),
inference(sat_conversion,[],[f988]) ).
cnf(s159,plain,
( ~ spl0_26
| ~ spl0_32 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s166,plain,
( spl0_11
| ~ spl0_27 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s168,plain,
( ~ spl0_27
| ~ spl0_32 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s169,plain,
( ~ spl0_29
| spl0_17 ),
inference(rat,[],[s5,s66,s96,s103]) ).
cnf(s170,plain,
( spl0_19
| spl0_10
| spl0_18
| spl0_11
| spl0_17 ),
inference(rat,[],[s44,s50,s3,s5,s15]) ).
cnf(s171,plain,
( ~ spl0_19
| spl0_30
| spl0_29 ),
inference(rat,[],[s8,s51,s88]) ).
cnf(s172,plain,
( spl0_18
| ~ spl0_25
| spl0_17 ),
inference(rat,[],[s46,s17,s2,s170,s78,s62,s113,s75,s77,s171,s141,s169]) ).
cnf(s173,plain,
( ~ spl0_25
| spl0_17 ),
inference(rat,[],[s8,s43,s79,s172,s141,s169]) ).
cnf(s174,plain,
( spl0_19
| spl0_18
| spl0_1 ),
inference(rat,[],[s168,s8,s73,s25,s128,s5,s170,s16,s32,s1,s56,s173,s35,s169,s52]) ).
cnf(s175,plain,
( ~ spl0_19
| spl0_1 ),
inference(rat,[],[s4,s13,s21,s73,s116,s156,s171,s88,s10,s32,s1,s56,s173,s35,s169,s52]) ).
cnf(s176,plain,
spl0_1,
inference(rat,[],[s25,s134,s3,s8,s110,s43,s79,s174,s15,s175,s16,s32,s1,s56,s173,s35,s169,s52]) ).
cnf(s177,plain,
~ spl0_25,
inference(rat,[],[s138,s176]) ).
cnf(s178,plain,
~ spl0_29,
inference(rat,[],[s95,s176]) ).
cnf(s181,plain,
spl0_17,
inference(rat,[],[s38,s176]) ).
cnf(s185,plain,
~ spl0_9,
inference(rat,[],[s136,s181]) ).
cnf(s187,plain,
~ spl0_13,
inference(rat,[],[s9,s181]) ).
cnf(s190,plain,
~ spl0_31,
inference(rat,[],[s166,s7,s128,s129,s152,s177]) ).
cnf(s191,plain,
~ spl0_12,
inference(rat,[],[s110,s190]) ).
cnf(s192,plain,
~ spl0_32,
inference(rat,[],[s7,s124,s159,s168,s177]) ).
cnf(s193,plain,
~ spl0_16,
inference(rat,[],[s156,s192]) ).
cnf(s194,plain,
spl0_30,
inference(rat,[],[s8,s178,s190,s192]) ).
cnf(s195,plain,
~ spl0_27,
inference(rat,[],[s134,s194]) ).
cnf(s196,plain,
~ spl0_28,
inference(rat,[],[s116,s194]) ).
cnf(s197,plain,
~ spl0_11,
inference(rat,[],[s25,s195]) ).
cnf(s198,plain,
~ spl0_15,
inference(rat,[],[s21,s196]) ).
cnf(s200,plain,
spl0_10,
inference(rat,[],[s3,s185,s191,s197]) ).
cnf(s201,plain,
spl0_14,
inference(rat,[],[s4,s187,s193,s198]) ).
cnf(s202,plain,
spl0_23,
inference(rat,[],[s76,s200]) ).
cnf(s205,plain,
$false,
inference(rat,[],[s19,s202,s201]) ).
fof(f1045,plain,
$false,
inference(avatar_sat_refutation,[],[s205]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG020+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:23:19 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.30 % (3912725)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (3912733)dis+10_1_sil=32000:sp=arity:random_seed=1776663481:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (3912731)% WARNING: option uhcvi not known.
% 0.21/0.30 % (3912730)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=884237312_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (3912731)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=575110964:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (3912732)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=758649188:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (3912734)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2466846138:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % (3912735)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=148648828:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % (3912736)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3881548964:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % Detected minimum model sizes of [8]
% 0.21/0.30 % Detected maximum model sizes of [max]
% 0.21/0.30 % TRYING [8]
% 0.21/0.30 % (3912734) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3912725-3912734"...
% 0.21/0.30 % (3912734)...printing done.
% 0.21/0.30 % (3912734)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Theorem for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.30 % (3912734)------------------------------
% 0.21/0.30 % (3912734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3912734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3912734)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3912734)Termination reason: Refutation
% 0.21/0.30 % (3912734)Time elapsed: 0.020 s
% 0.21/0.30 % (3912734)Peak memory usage: 13 MB
% 0.21/0.30 % (3912734)Instructions burned: 37 (million)
% 0.21/0.30 % (3912725)Success in time 0.063 s
% 0.21/0.30 % Vampire exiting
%------------------------------------------------------------------------------