%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG016+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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:20:04 AM UTC 2026
% Result : Theorem 0.21s 0.34s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 129
% Syntax : Number of formulae : 824 ( 190 unt; 113 def)
% Number of atoms : 2681 (1264 equ)
% Maximal formula atoms : 128 ( 3 avg)
% Number of connectives : 3176 (1319 ~;1324 |; 404 &)
% ( 113 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 117 ( 115 usr; 116 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e10,e10) = e10
| op1(e10,e10) = e11
| op1(e10,e10) = e12
| op1(e10,e10) = e13 )
& ( op1(e10,e11) = e10
| op1(e10,e11) = e11
| op1(e10,e11) = e12
| op1(e10,e11) = e13 )
& ( op1(e10,e12) = e10
| op1(e10,e12) = e11
| op1(e10,e12) = e12
| op1(e10,e12) = e13 )
& ( op1(e10,e13) = e10
| op1(e10,e13) = e11
| op1(e10,e13) = e12
| op1(e10,e13) = e13 )
& ( op1(e11,e10) = e10
| op1(e11,e10) = e11
| op1(e11,e10) = e12
| op1(e11,e10) = e13 )
& ( op1(e11,e11) = e10
| op1(e11,e11) = e11
| op1(e11,e11) = e12
| op1(e11,e11) = e13 )
& ( op1(e11,e12) = e10
| op1(e11,e12) = e11
| op1(e11,e12) = e12
| op1(e11,e12) = e13 )
& ( op1(e11,e13) = e10
| op1(e11,e13) = e11
| op1(e11,e13) = e12
| op1(e11,e13) = e13 )
& ( op1(e12,e10) = e10
| op1(e12,e10) = e11
| op1(e12,e10) = e12
| op1(e12,e10) = e13 )
& ( op1(e12,e11) = e10
| op1(e12,e11) = e11
| op1(e12,e11) = e12
| op1(e12,e11) = e13 )
& ( op1(e12,e12) = e10
| op1(e12,e12) = e11
| op1(e12,e12) = e12
| op1(e12,e12) = e13 )
& ( op1(e12,e13) = e10
| op1(e12,e13) = e11
| op1(e12,e13) = e12
| op1(e12,e13) = e13 )
& ( op1(e13,e10) = e10
| op1(e13,e10) = e11
| op1(e13,e10) = e12
| op1(e13,e10) = e13 )
& ( op1(e13,e11) = e10
| op1(e13,e11) = e11
| op1(e13,e11) = e12
| op1(e13,e11) = e13 )
& ( op1(e13,e12) = e10
| op1(e13,e12) = e11
| op1(e13,e12) = e12
| op1(e13,e12) = e13 )
& ( op1(e13,e13) = e10
| op1(e13,e13) = e11
| op1(e13,e13) = e12
| op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f3,axiom,
( op1(unit1,e10) = e10
& op1(e10,unit1) = e10
& op1(unit1,e11) = e11
& op1(e11,unit1) = e11
& op1(unit1,e12) = e12
& op1(e12,unit1) = e12
& op1(unit1,e13) = e13
& op1(e13,unit1) = e13
& ( unit1 = e10
| unit1 = e11
| unit1 = e12
| unit1 = e13 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f5,axiom,
( ( op2(e20,e20) = e20
| op2(e20,e20) = e21
| op2(e20,e20) = e22
| op2(e20,e20) = e23 )
& ( op2(e20,e21) = e20
| op2(e20,e21) = e21
| op2(e20,e21) = e22
| op2(e20,e21) = e23 )
& ( op2(e20,e22) = e20
| op2(e20,e22) = e21
| op2(e20,e22) = e22
| op2(e20,e22) = e23 )
& ( op2(e20,e23) = e20
| op2(e20,e23) = e21
| op2(e20,e23) = e22
| op2(e20,e23) = e23 )
& ( op2(e21,e20) = e20
| op2(e21,e20) = e21
| op2(e21,e20) = e22
| op2(e21,e20) = e23 )
& ( op2(e21,e21) = e20
| op2(e21,e21) = e21
| op2(e21,e21) = e22
| op2(e21,e21) = e23 )
& ( op2(e21,e22) = e20
| op2(e21,e22) = e21
| op2(e21,e22) = e22
| op2(e21,e22) = e23 )
& ( op2(e21,e23) = e20
| op2(e21,e23) = e21
| op2(e21,e23) = e22
| op2(e21,e23) = e23 )
& ( op2(e22,e20) = e20
| op2(e22,e20) = e21
| op2(e22,e20) = e22
| op2(e22,e20) = e23 )
& ( op2(e22,e21) = e20
| op2(e22,e21) = e21
| op2(e22,e21) = e22
| op2(e22,e21) = e23 )
& ( op2(e22,e22) = e20
| op2(e22,e22) = e21
| op2(e22,e22) = e22
| op2(e22,e22) = e23 )
& ( op2(e22,e23) = e20
| op2(e22,e23) = e21
| op2(e22,e23) = e22
| op2(e22,e23) = e23 )
& ( op2(e23,e20) = e20
| op2(e23,e20) = e21
| op2(e23,e20) = e22
| op2(e23,e20) = e23 )
& ( op2(e23,e21) = e20
| op2(e23,e21) = e21
| op2(e23,e21) = e22
| op2(e23,e21) = e23 )
& ( op2(e23,e22) = e20
| op2(e23,e22) = e21
| op2(e23,e22) = e22
| op2(e23,e22) = e23 )
& ( op2(e23,e23) = e20
| op2(e23,e23) = e21
| op2(e23,e23) = e22
| op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f7,axiom,
( op2(unit2,e20) = e20
& op2(e20,unit2) = e20
& op2(unit2,e21) = e21
& op2(e21,unit2) = e21
& op2(unit2,e22) = e22
& op2(e22,unit2) = e22
& op2(unit2,e23) = e23
& op2(e23,unit2) = e23
& ( unit2 = e20
| unit2 = e21
| unit2 = e22
| unit2 = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( op2(e20,inv2(e20)) = unit2
& op2(inv2(e20),e20) = unit2
& op2(e21,inv2(e21)) = unit2
& op2(inv2(e21),e21) = unit2
& op2(e22,inv2(e22)) = unit2
& op2(inv2(e22),e22) = unit2
& op2(e23,inv2(e23)) = unit2
& op2(inv2(e23),e23) = unit2
& ( inv2(e20) = e20
| inv2(e20) = e21
| inv2(e20) = e22
| inv2(e20) = e23 )
& ( inv2(e21) = e20
| inv2(e21) = e21
| inv2(e21) = e22
| inv2(e21) = e23 )
& ( inv2(e22) = e20
| inv2(e22) = e21
| inv2(e22) = e22
| inv2(e22) = e23 )
& ( inv2(e23) = e20
| inv2(e23) = e21
| inv2(e23) = e22
| inv2(e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f13,axiom,
inv2(unit2) = unit2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f15,axiom,
( ( inv2(e20) = e20
=> inv2(e20) = e20 )
& ( inv2(e20) = e21
=> inv2(e21) = e20 )
& ( inv2(e20) = e22
=> inv2(e22) = e20 )
& ( inv2(e20) = e23
=> inv2(e23) = e20 )
& ( inv2(e21) = e20
=> inv2(e20) = e21 )
& ( inv2(e21) = e21
=> inv2(e21) = e21 )
& ( inv2(e21) = e22
=> inv2(e22) = e21 )
& ( inv2(e21) = e23
=> inv2(e23) = e21 )
& ( inv2(e22) = e20
=> inv2(e20) = e22 )
& ( inv2(e22) = e21
=> inv2(e21) = e22 )
& ( inv2(e22) = e22
=> inv2(e22) = e22 )
& ( inv2(e22) = e23
=> inv2(e23) = e22 )
& ( inv2(e23) = e20
=> inv2(e20) = e23 )
& ( inv2(e23) = e21
=> inv2(e21) = e23 )
& ( inv2(e23) = e22
=> inv2(e22) = e23 )
& ( inv2(e23) = e23
=> inv2(e23) = e23 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( inv2(e20) != inv2(e21)
& inv2(e20) != inv2(e22)
& inv2(e20) != inv2(e23)
& inv2(e21) != inv2(e22)
& inv2(e21) != inv2(e23)
& inv2(e22) != inv2(e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( op1(e10,e10) != op1(e11,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e10,e11) != op1(e11,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e10,e12) != op1(e11,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e10,e13) != op1(e11,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e10,e10) != op1(e10,e11)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e12) != op1(e10,e13)
& op1(e11,e10) != op1(e11,e11)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e12) != op1(e11,e13)
& op1(e12,e10) != op1(e12,e11)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e12) != op1(e12,e13)
& op1(e13,e10) != op1(e13,e11)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e12) != op1(e13,e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
( op2(e20,e20) != op2(e21,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e20,e21) != op2(e21,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e20,e22) != op2(e21,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e20,e23) != op2(e21,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e20,e20) != op2(e20,e21)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e22) != op2(e20,e23)
& op2(e21,e20) != op2(e21,e21)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e22) != op2(e21,e23)
& op2(e22,e20) != op2(e22,e21)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e22) != op2(e22,e23)
& op2(e23,e20) != op2(e23,e21)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e22) != op2(e23,e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
fof(f20,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax20) ).
fof(f24,axiom,
( e10 = op1(op1(e12,op1(e12,e12)),e12)
& e11 = op1(e12,op1(e12,e12))
& e13 = op1(e12,e12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( e20 = op2(op2(e22,op2(e22,e22)),e22)
& e21 = op2(e22,op2(e22,e22))
& e23 = op2(e22,e22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f27,axiom,
( h2(e12) = e21
& h2(e10) = op2(op2(e21,op2(e21,e21)),e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e13) = op2(e21,e21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27) ).
fof(f28,axiom,
( h3(e12) = e22
& h3(e10) = op2(op2(e22,op2(e22,e22)),e22)
& h3(e11) = op2(e22,op2(e22,e22))
& h3(e13) = op2(e22,e22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f30,conjecture,
( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f31,negated_conjecture,
~ ( ( h1(op1(e10,e10)) = op2(h1(e10),h1(e10))
& h1(op1(e10,e11)) = op2(h1(e10),h1(e11))
& h1(op1(e10,e12)) = op2(h1(e10),h1(e12))
& h1(op1(e10,e13)) = op2(h1(e10),h1(e13))
& h1(op1(e11,e10)) = op2(h1(e11),h1(e10))
& h1(op1(e11,e11)) = op2(h1(e11),h1(e11))
& h1(op1(e11,e12)) = op2(h1(e11),h1(e12))
& h1(op1(e11,e13)) = op2(h1(e11),h1(e13))
& h1(op1(e12,e10)) = op2(h1(e12),h1(e10))
& h1(op1(e12,e11)) = op2(h1(e12),h1(e11))
& h1(op1(e12,e12)) = op2(h1(e12),h1(e12))
& h1(op1(e12,e13)) = op2(h1(e12),h1(e13))
& h1(op1(e13,e10)) = op2(h1(e13),h1(e10))
& h1(op1(e13,e11)) = op2(h1(e13),h1(e11))
& h1(op1(e13,e12)) = op2(h1(e13),h1(e12))
& h1(op1(e13,e13)) = op2(h1(e13),h1(e13))
& ( h1(e10) = e20
| h1(e11) = e20
| h1(e12) = e20
| h1(e13) = e20 )
& ( h1(e10) = e21
| h1(e11) = e21
| h1(e12) = e21
| h1(e13) = e21 )
& ( h1(e10) = e22
| h1(e11) = e22
| h1(e12) = e22
| h1(e13) = e22 )
& ( h1(e10) = e23
| h1(e11) = e23
| h1(e12) = e23
| h1(e13) = e23 ) )
| ( h2(op1(e10,e10)) = op2(h2(e10),h2(e10))
& h2(op1(e10,e11)) = op2(h2(e10),h2(e11))
& h2(op1(e10,e12)) = op2(h2(e10),h2(e12))
& h2(op1(e10,e13)) = op2(h2(e10),h2(e13))
& h2(op1(e11,e10)) = op2(h2(e11),h2(e10))
& h2(op1(e11,e11)) = op2(h2(e11),h2(e11))
& h2(op1(e11,e12)) = op2(h2(e11),h2(e12))
& h2(op1(e11,e13)) = op2(h2(e11),h2(e13))
& h2(op1(e12,e10)) = op2(h2(e12),h2(e10))
& h2(op1(e12,e11)) = op2(h2(e12),h2(e11))
& h2(op1(e12,e12)) = op2(h2(e12),h2(e12))
& h2(op1(e12,e13)) = op2(h2(e12),h2(e13))
& h2(op1(e13,e10)) = op2(h2(e13),h2(e10))
& h2(op1(e13,e11)) = op2(h2(e13),h2(e11))
& h2(op1(e13,e12)) = op2(h2(e13),h2(e12))
& h2(op1(e13,e13)) = op2(h2(e13),h2(e13))
& ( h2(e10) = e20
| h2(e11) = e20
| h2(e12) = e20
| h2(e13) = e20 )
& ( h2(e10) = e21
| h2(e11) = e21
| h2(e12) = e21
| h2(e13) = e21 )
& ( h2(e10) = e22
| h2(e11) = e22
| h2(e12) = e22
| h2(e13) = e22 )
& ( h2(e10) = e23
| h2(e11) = e23
| h2(e12) = e23
| h2(e13) = e23 ) )
| ( h3(op1(e10,e10)) = op2(h3(e10),h3(e10))
& h3(op1(e10,e11)) = op2(h3(e10),h3(e11))
& h3(op1(e10,e12)) = op2(h3(e10),h3(e12))
& h3(op1(e10,e13)) = op2(h3(e10),h3(e13))
& h3(op1(e11,e10)) = op2(h3(e11),h3(e10))
& h3(op1(e11,e11)) = op2(h3(e11),h3(e11))
& h3(op1(e11,e12)) = op2(h3(e11),h3(e12))
& h3(op1(e11,e13)) = op2(h3(e11),h3(e13))
& h3(op1(e12,e10)) = op2(h3(e12),h3(e10))
& h3(op1(e12,e11)) = op2(h3(e12),h3(e11))
& h3(op1(e12,e12)) = op2(h3(e12),h3(e12))
& h3(op1(e12,e13)) = op2(h3(e12),h3(e13))
& h3(op1(e13,e10)) = op2(h3(e13),h3(e10))
& h3(op1(e13,e11)) = op2(h3(e13),h3(e11))
& h3(op1(e13,e12)) = op2(h3(e13),h3(e12))
& h3(op1(e13,e13)) = op2(h3(e13),h3(e13))
& ( h3(e10) = e20
| h3(e11) = e20
| h3(e12) = e20
| h3(e13) = e20 )
& ( h3(e10) = e21
| h3(e11) = e21
| h3(e12) = e21
| h3(e13) = e21 )
& ( h3(e10) = e22
| h3(e11) = e22
| h3(e12) = e22
| h3(e13) = e22 )
& ( h3(e10) = e23
| h3(e11) = e23
| h3(e12) = e23
| h3(e13) = e23 ) )
| ( h4(op1(e10,e10)) = op2(h4(e10),h4(e10))
& h4(op1(e10,e11)) = op2(h4(e10),h4(e11))
& h4(op1(e10,e12)) = op2(h4(e10),h4(e12))
& h4(op1(e10,e13)) = op2(h4(e10),h4(e13))
& h4(op1(e11,e10)) = op2(h4(e11),h4(e10))
& h4(op1(e11,e11)) = op2(h4(e11),h4(e11))
& h4(op1(e11,e12)) = op2(h4(e11),h4(e12))
& h4(op1(e11,e13)) = op2(h4(e11),h4(e13))
& h4(op1(e12,e10)) = op2(h4(e12),h4(e10))
& h4(op1(e12,e11)) = op2(h4(e12),h4(e11))
& h4(op1(e12,e12)) = op2(h4(e12),h4(e12))
& h4(op1(e12,e13)) = op2(h4(e12),h4(e13))
& h4(op1(e13,e10)) = op2(h4(e13),h4(e10))
& h4(op1(e13,e11)) = op2(h4(e13),h4(e11))
& h4(op1(e13,e12)) = op2(h4(e13),h4(e12))
& h4(op1(e13,e13)) = op2(h4(e13),h4(e13))
& ( h4(e10) = e20
| h4(e11) = e20
| h4(e12) = e20
| h4(e13) = e20 )
& ( h4(e10) = e21
| h4(e11) = e21
| h4(e12) = e21
| h4(e13) = e21 )
& ( h4(e10) = e22
| h4(e11) = e22
| h4(e12) = e22
| h4(e13) = e22 )
& ( h4(e10) = e23
| h4(e11) = e23
| h4(e12) = e23
| h4(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f30]) ).
fof(f33,plain,
( ( inv2(e20) = e20
| e20 != inv2(e20) )
& ( inv2(e21) = e20
| e21 != inv2(e20) )
& ( inv2(e22) = e20
| e22 != inv2(e20) )
& ( inv2(e23) = e20
| e23 != inv2(e20) )
& ( inv2(e20) = e21
| e20 != inv2(e21) )
& ( inv2(e21) = e21
| e21 != inv2(e21) )
& ( inv2(e22) = e21
| e22 != inv2(e21) )
& ( inv2(e23) = e21
| e23 != inv2(e21) )
& ( inv2(e20) = e22
| e20 != inv2(e22) )
& ( inv2(e21) = e22
| e21 != inv2(e22) )
& ( inv2(e22) = e22
| e22 != inv2(e22) )
& ( inv2(e23) = e22
| e23 != inv2(e22) )
& ( inv2(e20) = e23
| e20 != inv2(e23) )
& ( inv2(e21) = e23
| e21 != inv2(e23) )
& ( inv2(e22) = e23
| e22 != inv2(e23) )
& ( inv2(e23) = e23
| e23 != inv2(e23) ) ),
inference(ennf_transformation,[],[f15]) ).
fof(f36,plain,
( ( h1(op1(e10,e10)) != op2(h1(e10),h1(e10))
| h1(op1(e10,e11)) != op2(h1(e10),h1(e11))
| h1(op1(e10,e12)) != op2(h1(e10),h1(e12))
| h1(op1(e10,e13)) != op2(h1(e10),h1(e13))
| h1(op1(e11,e10)) != op2(h1(e11),h1(e10))
| h1(op1(e11,e11)) != op2(h1(e11),h1(e11))
| h1(op1(e11,e12)) != op2(h1(e11),h1(e12))
| h1(op1(e11,e13)) != op2(h1(e11),h1(e13))
| h1(op1(e12,e10)) != op2(h1(e12),h1(e10))
| h1(op1(e12,e11)) != op2(h1(e12),h1(e11))
| h1(op1(e12,e12)) != op2(h1(e12),h1(e12))
| h1(op1(e12,e13)) != op2(h1(e12),h1(e13))
| h1(op1(e13,e10)) != op2(h1(e13),h1(e10))
| h1(op1(e13,e11)) != op2(h1(e13),h1(e11))
| h1(op1(e13,e12)) != op2(h1(e13),h1(e12))
| h1(op1(e13,e13)) != op2(h1(e13),h1(e13))
| ( e20 != h1(e10)
& e20 != h1(e11)
& e20 != h1(e12)
& e20 != h1(e13) )
| ( e21 != h1(e10)
& e21 != h1(e11)
& e21 != h1(e12)
& e21 != h1(e13) )
| ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) ) )
& ( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| ( e20 != h2(e10)
& e20 != h2(e11)
& e20 != h2(e12)
& e20 != h2(e13) )
| ( e21 != h2(e10)
& e21 != h2(e11)
& e21 != h2(e12)
& e21 != h2(e13) )
| ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) ) )
& ( h3(op1(e10,e10)) != op2(h3(e10),h3(e10))
| h3(op1(e10,e11)) != op2(h3(e10),h3(e11))
| h3(op1(e10,e12)) != op2(h3(e10),h3(e12))
| h3(op1(e10,e13)) != op2(h3(e10),h3(e13))
| h3(op1(e11,e10)) != op2(h3(e11),h3(e10))
| h3(op1(e11,e11)) != op2(h3(e11),h3(e11))
| h3(op1(e11,e12)) != op2(h3(e11),h3(e12))
| h3(op1(e11,e13)) != op2(h3(e11),h3(e13))
| h3(op1(e12,e10)) != op2(h3(e12),h3(e10))
| h3(op1(e12,e11)) != op2(h3(e12),h3(e11))
| h3(op1(e12,e12)) != op2(h3(e12),h3(e12))
| h3(op1(e12,e13)) != op2(h3(e12),h3(e13))
| h3(op1(e13,e10)) != op2(h3(e13),h3(e10))
| h3(op1(e13,e11)) != op2(h3(e13),h3(e11))
| h3(op1(e13,e12)) != op2(h3(e13),h3(e12))
| h3(op1(e13,e13)) != op2(h3(e13),h3(e13))
| ( e20 != h3(e10)
& e20 != h3(e11)
& e20 != h3(e12)
& e20 != h3(e13) )
| ( e21 != h3(e10)
& e21 != h3(e11)
& e21 != h3(e12)
& e21 != h3(e13) )
| ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) ) )
& ( h4(op1(e10,e10)) != op2(h4(e10),h4(e10))
| h4(op1(e10,e11)) != op2(h4(e10),h4(e11))
| h4(op1(e10,e12)) != op2(h4(e10),h4(e12))
| h4(op1(e10,e13)) != op2(h4(e10),h4(e13))
| h4(op1(e11,e10)) != op2(h4(e11),h4(e10))
| h4(op1(e11,e11)) != op2(h4(e11),h4(e11))
| h4(op1(e11,e12)) != op2(h4(e11),h4(e12))
| h4(op1(e11,e13)) != op2(h4(e11),h4(e13))
| h4(op1(e12,e10)) != op2(h4(e12),h4(e10))
| h4(op1(e12,e11)) != op2(h4(e12),h4(e11))
| h4(op1(e12,e12)) != op2(h4(e12),h4(e12))
| h4(op1(e12,e13)) != op2(h4(e12),h4(e13))
| h4(op1(e13,e10)) != op2(h4(e13),h4(e10))
| h4(op1(e13,e11)) != op2(h4(e13),h4(e11))
| h4(op1(e13,e12)) != op2(h4(e13),h4(e12))
| h4(op1(e13,e13)) != op2(h4(e13),h4(e13))
| ( e20 != h4(e10)
& e20 != h4(e11)
& e20 != h4(e12)
& e20 != h4(e13) )
| ( e21 != h4(e10)
& e21 != h4(e11)
& e21 != h4(e12)
& e21 != h4(e13) )
| ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) ) ) ),
inference(ennf_transformation,[],[f31]) ).
fof(f42,plain,
( e13 = op1(e11,e11)
| e12 = op1(e11,e11)
| e11 = op1(e11,e11)
| e10 = op1(e11,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f44,plain,
( e13 = op1(e11,e13)
| e12 = op1(e11,e13)
| e11 = op1(e11,e13)
| e10 = op1(e11,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f46,plain,
( e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f50,plain,
( e13 = op1(e13,e11)
| e12 = op1(e13,e11)
| e11 = op1(e13,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f51,plain,
( e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f52,plain,
( e13 = op1(e13,e13)
| e12 = op1(e13,e13)
| e11 = op1(e13,e13)
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f117,plain,
( e13 = unit1
| e12 = unit1
| e11 = unit1
| e10 = unit1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f118,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f3]) ).
fof(f120,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f3]) ).
fof(f122,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f3]) ).
fof(f124,plain,
e10 = op1(e10,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
e10 = op1(unit1,e10),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
( e23 = op2(e21,e21)
| e22 = op2(e21,e21)
| e21 = op2(e21,e21)
| e20 = op2(e21,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
( e23 = op2(e21,e23)
| e22 = op2(e21,e23)
| e21 = op2(e21,e23)
| e20 = op2(e21,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
( e23 = op2(e22,e20)
| e22 = op2(e22,e20)
| e21 = op2(e22,e20)
| e20 = op2(e22,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
( e23 = op2(e22,e21)
| e22 = op2(e22,e21)
| e21 = op2(e22,e21)
| e20 = op2(e22,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
( e23 = op2(e23,e21)
| e22 = op2(e23,e21)
| e21 = op2(e23,e21)
| e20 = op2(e23,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
( e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f153,plain,
( e23 = op2(e23,e23)
| e22 = op2(e23,e23)
| e21 = op2(e23,e23)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f218,plain,
( e23 = unit2
| e22 = unit2
| e21 = unit2
| e20 = unit2 ),
inference(cnf_transformation,[],[f7]) ).
fof(f219,plain,
e23 = op2(e23,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f220,plain,
e23 = op2(unit2,e23),
inference(cnf_transformation,[],[f7]) ).
fof(f221,plain,
e22 = op2(e22,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f222,plain,
e22 = op2(unit2,e22),
inference(cnf_transformation,[],[f7]) ).
fof(f223,plain,
e21 = op2(e21,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f224,plain,
e21 = op2(unit2,e21),
inference(cnf_transformation,[],[f7]) ).
fof(f225,plain,
e20 = op2(e20,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f226,plain,
e20 = op2(unit2,e20),
inference(cnf_transformation,[],[f7]) ).
fof(f229,plain,
( e23 = inv2(e22)
| e22 = inv2(e22)
| e21 = inv2(e22)
| e20 = inv2(e22) ),
inference(cnf_transformation,[],[f8]) ).
fof(f231,plain,
unit2 = op2(inv2(e23),e23),
inference(cnf_transformation,[],[f8]) ).
fof(f233,plain,
unit2 = op2(inv2(e22),e22),
inference(cnf_transformation,[],[f8]) ).
fof(f262,plain,
unit2 = inv2(unit2),
inference(cnf_transformation,[],[f13]) ).
fof(f275,plain,
( e23 != inv2(e22)
| e22 = inv2(e23) ),
inference(cnf_transformation,[],[f33]) ).
fof(f283,plain,
inv2(e20) != inv2(e22),
inference(cnf_transformation,[],[f16]) ).
fof(f287,plain,
op1(e13,e11) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f290,plain,
op1(e13,e10) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f292,plain,
op1(e12,e11) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f293,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f296,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f297,plain,
op1(e11,e12) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f298,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f299,plain,
op1(e11,e11) != op1(e11,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f301,plain,
op1(e11,e10) != op1(e11,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f309,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f310,plain,
op1(e11,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f311,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f312,plain,
op1(e10,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f314,plain,
op1(e10,e13) != op1(e11,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f315,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f316,plain,
op1(e11,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f321,plain,
op1(e12,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f324,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f326,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f334,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f335,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f336,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f338,plain,
op2(e23,e20) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f340,plain,
op2(e22,e21) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f341,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f342,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f343,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f344,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f345,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f346,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f347,plain,
op2(e21,e21) != op2(e21,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f348,plain,
op2(e21,e20) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f357,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f358,plain,
op2(e21,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f362,plain,
op2(e20,e23) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f363,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f364,plain,
op2(e21,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f366,plain,
op2(e20,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f374,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f377,plain,
op2(e21,e20) != op2(e22,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f389,plain,
e21 != e22,
inference(cnf_transformation,[],[f20]) ).
fof(f392,plain,
e20 != e21,
inference(cnf_transformation,[],[f20]) ).
fof(f417,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f24]) ).
fof(f418,plain,
e11 = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f24]) ).
fof(f419,plain,
e10 = op1(op1(e12,op1(e12,e12)),e12),
inference(cnf_transformation,[],[f24]) ).
fof(f420,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f25]) ).
fof(f421,plain,
e21 = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f25]) ).
fof(f427,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f27]) ).
fof(f428,plain,
op2(e21,op2(e21,e21)) = h2(e11),
inference(cnf_transformation,[],[f27]) ).
fof(f429,plain,
h2(e10) = op2(op2(e21,op2(e21,e21)),e21),
inference(cnf_transformation,[],[f27]) ).
fof(f430,plain,
e21 = h2(e12),
inference(cnf_transformation,[],[f27]) ).
fof(f434,plain,
e22 = h3(e12),
inference(cnf_transformation,[],[f28]) ).
fof(f450,plain,
( e20 != h2(e10)
| ~ sP5 ),
inference(cnf_transformation,[],[f36]) ).
fof(f452,plain,
( e21 != h2(e12)
| ~ sP4 ),
inference(cnf_transformation,[],[f36]) ).
fof(f501,plain,
( e23 != h2(e13)
| e22 != h2(e11)
| sP4
| sP5
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f36]) ).
fof(f568,plain,
( e23 != h2(e13)
| e22 != h2(e11)
| sP4
| ~ sP5
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(consistent_polarity_flipping,[],[f501]) ).
fof(f611,plain,
( e20 != h2(e10)
| sP5 ),
inference(consistent_polarity_flipping,[],[f450]) ).
fof(f668,definition,
( spl8_11
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition]) ).
fof(f687,definition,
( spl8_15
<=> e20 = h2(e10) ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
fof(f688,plain,
( e20 = h2(e10)
| ~ spl8_15 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( spl8_11
| ~ spl8_15 ),
inference(avatar_split_clause,[],[f611,f687,f668]) ).
fof(f692,definition,
( spl8_16
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl8_16])],[avatar_definition]) ).
fof(f701,definition,
( spl8_18
<=> e21 = h2(e12) ),
introduced(definition,[new_symbols(definition,[spl8_18])],[avatar_definition]) ).
fof(f702,plain,
( e21 = h2(e12)
| ~ spl8_18 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f704,plain,
( ~ spl8_16
| ~ spl8_18 ),
inference(avatar_split_clause,[],[f452,f701,f692]) ).
fof(f749,definition,
( spl8_28
<=> e21 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl8_28])],[avatar_definition]) ).
fof(f750,plain,
( e21 = h3(e12)
| ~ spl8_28 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f751,plain,
( e21 != h3(e12)
| spl8_28 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f924,definition,
( spl8_65
<=> h2(op1(e10,e10)) = op2(h2(e10),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_65])],[avatar_definition]) ).
fof(f926,plain,
( h2(op1(e10,e10)) != op2(h2(e10),h2(e10))
| spl8_65 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f928,definition,
( spl8_66
<=> h2(op1(e10,e11)) = op2(h2(e10),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_66])],[avatar_definition]) ).
fof(f930,plain,
( h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| spl8_66 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f932,definition,
( spl8_67
<=> h2(op1(e10,e12)) = op2(h2(e10),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_67])],[avatar_definition]) ).
fof(f934,plain,
( h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| spl8_67 ),
inference(avatar_component_clause,[],[f932]) ).
fof(f936,definition,
( spl8_68
<=> h2(op1(e10,e13)) = op2(h2(e10),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_68])],[avatar_definition]) ).
fof(f938,plain,
( h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| spl8_68 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f940,definition,
( spl8_69
<=> h2(op1(e11,e10)) = op2(h2(e11),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_69])],[avatar_definition]) ).
fof(f942,plain,
( h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| spl8_69 ),
inference(avatar_component_clause,[],[f940]) ).
fof(f944,definition,
( spl8_70
<=> h2(op1(e11,e11)) = op2(h2(e11),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition]) ).
fof(f946,plain,
( h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| spl8_70 ),
inference(avatar_component_clause,[],[f944]) ).
fof(f948,definition,
( spl8_71
<=> h2(op1(e11,e12)) = op2(h2(e11),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f950,plain,
( h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| spl8_71 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f952,definition,
( spl8_72
<=> h2(op1(e11,e13)) = op2(h2(e11),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_72])],[avatar_definition]) ).
fof(f954,plain,
( h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| spl8_72 ),
inference(avatar_component_clause,[],[f952]) ).
fof(f956,definition,
( spl8_73
<=> h2(op1(e12,e10)) = op2(h2(e12),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_73])],[avatar_definition]) ).
fof(f958,plain,
( h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| spl8_73 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f960,definition,
( spl8_74
<=> h2(op1(e12,e11)) = op2(h2(e12),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_74])],[avatar_definition]) ).
fof(f962,plain,
( h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| spl8_74 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f964,definition,
( spl8_75
<=> h2(op1(e12,e12)) = op2(h2(e12),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_75])],[avatar_definition]) ).
fof(f966,plain,
( h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| spl8_75 ),
inference(avatar_component_clause,[],[f964]) ).
fof(f968,definition,
( spl8_76
<=> h2(op1(e12,e13)) = op2(h2(e12),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_76])],[avatar_definition]) ).
fof(f970,plain,
( h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| spl8_76 ),
inference(avatar_component_clause,[],[f968]) ).
fof(f972,definition,
( spl8_77
<=> h2(op1(e13,e10)) = op2(h2(e13),h2(e10)) ),
introduced(definition,[new_symbols(definition,[spl8_77])],[avatar_definition]) ).
fof(f974,plain,
( h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| spl8_77 ),
inference(avatar_component_clause,[],[f972]) ).
fof(f976,definition,
( spl8_78
<=> h2(op1(e13,e11)) = op2(h2(e13),h2(e11)) ),
introduced(definition,[new_symbols(definition,[spl8_78])],[avatar_definition]) ).
fof(f978,plain,
( h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| spl8_78 ),
inference(avatar_component_clause,[],[f976]) ).
fof(f980,definition,
( spl8_79
<=> h2(op1(e13,e12)) = op2(h2(e13),h2(e12)) ),
introduced(definition,[new_symbols(definition,[spl8_79])],[avatar_definition]) ).
fof(f982,plain,
( h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| spl8_79 ),
inference(avatar_component_clause,[],[f980]) ).
fof(f984,definition,
( spl8_80
<=> h2(op1(e13,e13)) = op2(h2(e13),h2(e13)) ),
introduced(definition,[new_symbols(definition,[spl8_80])],[avatar_definition]) ).
fof(f986,plain,
( h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| spl8_80 ),
inference(avatar_component_clause,[],[f984]) ).
fof(f1002,definition,
( spl8_84
<=> e22 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl8_84])],[avatar_definition]) ).
fof(f1003,plain,
( e22 = h2(e11)
| ~ spl8_84 ),
inference(avatar_component_clause,[],[f1002]) ).
fof(f1028,definition,
( spl8_88
<=> e23 = h2(e13) ),
introduced(definition,[new_symbols(definition,[spl8_88])],[avatar_definition]) ).
fof(f1029,plain,
( e23 = h2(e13)
| ~ spl8_88 ),
inference(avatar_component_clause,[],[f1028]) ).
fof(f1033,plain,
( ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_70
| ~ spl8_71
| ~ spl8_72
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80
| ~ spl8_11
| spl8_16
| ~ spl8_84
| ~ spl8_88 ),
inference(avatar_split_clause,[],[f568,f1028,f1002,f692,f668,f984,f980,f976,f972,f968,f964,f960,f956,f952,f948,f944,f940,f936,f932,f928,f924]) ).
fof(f1109,definition,
( spl8_107
<=> e22 = h3(e12) ),
introduced(definition,[new_symbols(definition,[spl8_107])],[avatar_definition]) ).
fof(f1110,plain,
( e22 = h3(e12)
| ~ spl8_107 ),
inference(avatar_component_clause,[],[f1109]) ).
fof(f1260,plain,
spl8_107,
inference(avatar_split_clause,[],[f434,f1109]) ).
fof(f1261,plain,
spl8_18,
inference(avatar_split_clause,[],[f430,f701]) ).
fof(f1264,definition,
( spl8_137
<=> e20 = op2(e20,e20) ),
introduced(definition,[new_symbols(definition,[spl8_137])],[avatar_definition]) ).
fof(f1265,plain,
( e20 = op2(e20,e20)
| ~ spl8_137 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1268,definition,
( spl8_138
<=> e20 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_138])],[avatar_definition]) ).
fof(f1276,definition,
( spl8_140
<=> e20 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_140])],[avatar_definition]) ).
fof(f1277,plain,
( e20 = op2(e23,e23)
| ~ spl8_140 ),
inference(avatar_component_clause,[],[f1276]) ).
fof(f1285,definition,
( spl8_142
<=> e21 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_142])],[avatar_definition]) ).
fof(f1286,plain,
( e21 = op2(e21,e21)
| ~ spl8_142 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1293,definition,
( spl8_144
<=> e21 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_144])],[avatar_definition]) ).
fof(f1294,plain,
( e21 = op2(e23,e23)
| ~ spl8_144 ),
inference(avatar_component_clause,[],[f1293]) ).
fof(f1302,definition,
( spl8_146
<=> e22 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_146])],[avatar_definition]) ).
fof(f1303,plain,
( e22 = op2(e21,e21)
| ~ spl8_146 ),
inference(avatar_component_clause,[],[f1302]) ).
fof(f1310,definition,
( spl8_148
<=> e22 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_148])],[avatar_definition]) ).
fof(f1319,definition,
( spl8_150
<=> e23 = op2(e21,e21) ),
introduced(definition,[new_symbols(definition,[spl8_150])],[avatar_definition]) ).
fof(f1320,plain,
( e23 = op2(e21,e21)
| ~ spl8_150 ),
inference(avatar_component_clause,[],[f1319]) ).
fof(f1323,definition,
( spl8_151
<=> e23 = op2(e22,e22) ),
introduced(definition,[new_symbols(definition,[spl8_151])],[avatar_definition]) ).
fof(f1324,plain,
( e23 = op2(e22,e22)
| ~ spl8_151 ),
inference(avatar_component_clause,[],[f1323]) ).
fof(f1327,definition,
( spl8_152
<=> e23 = op2(e23,e23) ),
introduced(definition,[new_symbols(definition,[spl8_152])],[avatar_definition]) ).
fof(f1328,plain,
( e23 = op2(e23,e23)
| ~ spl8_152 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f1332,definition,
( spl8_153
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl8_153])],[avatar_definition]) ).
fof(f1333,plain,
( e10 = op1(e10,e10)
| ~ spl8_153 ),
inference(avatar_component_clause,[],[f1332]) ).
fof(f1336,definition,
( spl8_154
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_154])],[avatar_definition]) ).
fof(f1344,definition,
( spl8_156
<=> e10 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_156])],[avatar_definition]) ).
fof(f1345,plain,
( e10 = op1(e13,e13)
| ~ spl8_156 ),
inference(avatar_component_clause,[],[f1344]) ).
fof(f1353,definition,
( spl8_158
<=> e11 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_158])],[avatar_definition]) ).
fof(f1361,definition,
( spl8_160
<=> e11 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_160])],[avatar_definition]) ).
fof(f1362,plain,
( e11 = op1(e13,e13)
| ~ spl8_160 ),
inference(avatar_component_clause,[],[f1361]) ).
fof(f1370,definition,
( spl8_162
<=> e12 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_162])],[avatar_definition]) ).
fof(f1378,definition,
( spl8_164
<=> e12 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_164])],[avatar_definition]) ).
fof(f1387,definition,
( spl8_166
<=> e13 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl8_166])],[avatar_definition]) ).
fof(f1388,plain,
( e13 = op1(e11,e11)
| ~ spl8_166 ),
inference(avatar_component_clause,[],[f1387]) ).
fof(f1391,definition,
( spl8_167
<=> e13 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl8_167])],[avatar_definition]) ).
fof(f1392,plain,
( e13 = op1(e12,e12)
| ~ spl8_167 ),
inference(avatar_component_clause,[],[f1391]) ).
fof(f1395,definition,
( spl8_168
<=> e13 = op1(e13,e13) ),
introduced(definition,[new_symbols(definition,[spl8_168])],[avatar_definition]) ).
fof(f1409,definition,
( spl8_171
<=> e20 = inv2(e22) ),
introduced(definition,[new_symbols(definition,[spl8_171])],[avatar_definition]) ).
fof(f1428,definition,
( spl8_175
<=> e21 = inv2(e22) ),
introduced(definition,[new_symbols(definition,[spl8_175])],[avatar_definition]) ).
fof(f1430,plain,
( e21 = inv2(e22)
| ~ spl8_175 ),
inference(avatar_component_clause,[],[f1428]) ).
fof(f1448,definition,
( spl8_179
<=> e22 = inv2(e23) ),
introduced(definition,[new_symbols(definition,[spl8_179])],[avatar_definition]) ).
fof(f1450,plain,
( e22 = inv2(e23)
| ~ spl8_179 ),
inference(avatar_component_clause,[],[f1448]) ).
fof(f1452,definition,
( spl8_180
<=> e23 = inv2(e22) ),
introduced(definition,[new_symbols(definition,[spl8_180])],[avatar_definition]) ).
fof(f1455,plain,
( spl8_179
| ~ spl8_180 ),
inference(avatar_split_clause,[],[f275,f1452,f1448]) ).
fof(f1520,definition,
( spl8_193
<=> e20 = inv2(e20) ),
introduced(definition,[new_symbols(definition,[spl8_193])],[avatar_definition]) ).
fof(f1522,plain,
( e20 = inv2(e20)
| ~ spl8_193 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1530,definition,
( spl8_195
<=> e22 = inv2(e22) ),
introduced(definition,[new_symbols(definition,[spl8_195])],[avatar_definition]) ).
fof(f1532,plain,
( e22 = inv2(e22)
| ~ spl8_195 ),
inference(avatar_component_clause,[],[f1530]) ).
fof(f1533,plain,
( spl8_171
| spl8_175
| spl8_195
| spl8_180 ),
inference(avatar_split_clause,[],[f229,f1452,f1530,f1428,f1409]) ).
fof(f1540,definition,
( spl8_197
<=> e20 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_197])],[avatar_definition]) ).
fof(f1542,plain,
( e20 = unit2
| ~ spl8_197 ),
inference(avatar_component_clause,[],[f1540]) ).
fof(f1544,definition,
( spl8_198
<=> e21 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_198])],[avatar_definition]) ).
fof(f1546,plain,
( e21 = unit2
| ~ spl8_198 ),
inference(avatar_component_clause,[],[f1544]) ).
fof(f1548,definition,
( spl8_199
<=> e22 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_199])],[avatar_definition]) ).
fof(f1550,plain,
( e22 = unit2
| ~ spl8_199 ),
inference(avatar_component_clause,[],[f1548]) ).
fof(f1552,definition,
( spl8_200
<=> e23 = unit2 ),
introduced(definition,[new_symbols(definition,[spl8_200])],[avatar_definition]) ).
fof(f1554,plain,
( e23 = unit2
| ~ spl8_200 ),
inference(avatar_component_clause,[],[f1552]) ).
fof(f1555,plain,
( spl8_197
| spl8_198
| spl8_199
| spl8_200 ),
inference(avatar_split_clause,[],[f218,f1552,f1548,f1544,f1540]) ).
fof(f1562,definition,
( spl8_202
<=> e21 = op2(e20,e21) ),
introduced(definition,[new_symbols(definition,[spl8_202])],[avatar_definition]) ).
fof(f1564,plain,
( e21 = op2(e20,e21)
| ~ spl8_202 ),
inference(avatar_component_clause,[],[f1562]) ).
fof(f1583,definition,
( spl8_207
<=> e22 = op2(e20,e22) ),
introduced(definition,[new_symbols(definition,[spl8_207])],[avatar_definition]) ).
fof(f1585,plain,
( e22 = op2(e20,e22)
| ~ spl8_207 ),
inference(avatar_component_clause,[],[f1583]) ).
fof(f1604,definition,
( spl8_212
<=> e23 = op2(e20,e23) ),
introduced(definition,[new_symbols(definition,[spl8_212])],[avatar_definition]) ).
fof(f1606,plain,
( e23 = op2(e20,e23)
| ~ spl8_212 ),
inference(avatar_component_clause,[],[f1604]) ).
fof(f1609,definition,
( spl8_213
<=> e20 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_213])],[avatar_definition]) ).
fof(f1611,plain,
( e20 = op2(e21,e20)
| ~ spl8_213 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1613,definition,
( spl8_214
<=> e21 = op2(e21,e20) ),
introduced(definition,[new_symbols(definition,[spl8_214])],[avatar_definition]) ).
fof(f1615,plain,
( e21 = op2(e21,e20)
| ~ spl8_214 ),
inference(avatar_component_clause,[],[f1613]) ).
fof(f1625,plain,
( spl8_138
| spl8_142
| spl8_146
| spl8_150 ),
inference(avatar_split_clause,[],[f143,f1319,f1302,f1285,f1268]) ).
fof(f1627,definition,
( spl8_217
<=> e20 = op2(e21,e22) ),
introduced(definition,[new_symbols(definition,[spl8_217])],[avatar_definition]) ).
fof(f1629,plain,
( e20 = op2(e21,e22)
| ~ spl8_217 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1644,definition,
( spl8_221
<=> e20 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_221])],[avatar_definition]) ).
fof(f1648,definition,
( spl8_222
<=> e21 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_222])],[avatar_definition]) ).
fof(f1650,plain,
( e21 = op2(e21,e23)
| ~ spl8_222 ),
inference(avatar_component_clause,[],[f1648]) ).
fof(f1652,definition,
( spl8_223
<=> e22 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_223])],[avatar_definition]) ).
fof(f1654,plain,
( e22 = op2(e21,e23)
| ~ spl8_223 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1656,definition,
( spl8_224
<=> e23 = op2(e21,e23) ),
introduced(definition,[new_symbols(definition,[spl8_224])],[avatar_definition]) ).
fof(f1658,plain,
( e23 = op2(e21,e23)
| ~ spl8_224 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1659,plain,
( spl8_221
| spl8_222
| spl8_223
| spl8_224 ),
inference(avatar_split_clause,[],[f145,f1656,f1652,f1648,f1644]) ).
fof(f1661,definition,
( spl8_225
<=> e20 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_225])],[avatar_definition]) ).
fof(f1665,definition,
( spl8_226
<=> e21 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_226])],[avatar_definition]) ).
fof(f1667,plain,
( e21 = op2(e22,e20)
| ~ spl8_226 ),
inference(avatar_component_clause,[],[f1665]) ).
fof(f1669,definition,
( spl8_227
<=> e22 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_227])],[avatar_definition]) ).
fof(f1671,plain,
( e22 = op2(e22,e20)
| ~ spl8_227 ),
inference(avatar_component_clause,[],[f1669]) ).
fof(f1673,definition,
( spl8_228
<=> e23 = op2(e22,e20) ),
introduced(definition,[new_symbols(definition,[spl8_228])],[avatar_definition]) ).
fof(f1676,plain,
( spl8_225
| spl8_226
| spl8_227
| spl8_228 ),
inference(avatar_split_clause,[],[f146,f1673,f1669,f1665,f1661]) ).
fof(f1678,definition,
( spl8_229
<=> e20 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_229])],[avatar_definition]) ).
fof(f1680,plain,
( e20 = op2(e22,e21)
| ~ spl8_229 ),
inference(avatar_component_clause,[],[f1678]) ).
fof(f1682,definition,
( spl8_230
<=> e21 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_230])],[avatar_definition]) ).
fof(f1686,definition,
( spl8_231
<=> e22 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_231])],[avatar_definition]) ).
fof(f1690,definition,
( spl8_232
<=> e23 = op2(e22,e21) ),
introduced(definition,[new_symbols(definition,[spl8_232])],[avatar_definition]) ).
fof(f1693,plain,
( spl8_229
| spl8_230
| spl8_231
| spl8_232 ),
inference(avatar_split_clause,[],[f147,f1690,f1686,f1682,f1678]) ).
fof(f1696,definition,
( spl8_233
<=> e20 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_233])],[avatar_definition]) ).
fof(f1697,plain,
( e20 != op2(e22,e23)
| spl8_233 ),
inference(avatar_component_clause,[],[f1696]) ).
fof(f1698,plain,
( e20 = op2(e22,e23)
| ~ spl8_233 ),
inference(avatar_component_clause,[],[f1696]) ).
fof(f1700,definition,
( spl8_234
<=> e21 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_234])],[avatar_definition]) ).
fof(f1702,plain,
( e21 = op2(e22,e23)
| ~ spl8_234 ),
inference(avatar_component_clause,[],[f1700]) ).
fof(f1704,definition,
( spl8_235
<=> e22 = op2(e22,e23) ),
introduced(definition,[new_symbols(definition,[spl8_235])],[avatar_definition]) ).
fof(f1706,plain,
( e22 = op2(e22,e23)
| ~ spl8_235 ),
inference(avatar_component_clause,[],[f1704]) ).
fof(f1725,definition,
( spl8_240
<=> e23 = op2(e23,e20) ),
introduced(definition,[new_symbols(definition,[spl8_240])],[avatar_definition]) ).
fof(f1727,plain,
( e23 = op2(e23,e20)
| ~ spl8_240 ),
inference(avatar_component_clause,[],[f1725]) ).
fof(f1730,definition,
( spl8_241
<=> e20 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_241])],[avatar_definition]) ).
fof(f1734,definition,
( spl8_242
<=> e21 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_242])],[avatar_definition]) ).
fof(f1736,plain,
( e21 = op2(e23,e21)
| ~ spl8_242 ),
inference(avatar_component_clause,[],[f1734]) ).
fof(f1738,definition,
( spl8_243
<=> e22 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_243])],[avatar_definition]) ).
fof(f1740,plain,
( e22 = op2(e23,e21)
| ~ spl8_243 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1742,definition,
( spl8_244
<=> e23 = op2(e23,e21) ),
introduced(definition,[new_symbols(definition,[spl8_244])],[avatar_definition]) ).
fof(f1744,plain,
( e23 = op2(e23,e21)
| ~ spl8_244 ),
inference(avatar_component_clause,[],[f1742]) ).
fof(f1745,plain,
( spl8_241
| spl8_242
| spl8_243
| spl8_244 ),
inference(avatar_split_clause,[],[f151,f1742,f1738,f1734,f1730]) ).
fof(f1747,definition,
( spl8_245
<=> e20 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_245])],[avatar_definition]) ).
fof(f1749,plain,
( e20 = op2(e23,e22)
| ~ spl8_245 ),
inference(avatar_component_clause,[],[f1747]) ).
fof(f1751,definition,
( spl8_246
<=> e21 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_246])],[avatar_definition]) ).
fof(f1753,plain,
( e21 = op2(e23,e22)
| ~ spl8_246 ),
inference(avatar_component_clause,[],[f1751]) ).
fof(f1755,definition,
( spl8_247
<=> e22 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_247])],[avatar_definition]) ).
fof(f1759,definition,
( spl8_248
<=> e23 = op2(e23,e22) ),
introduced(definition,[new_symbols(definition,[spl8_248])],[avatar_definition]) ).
fof(f1760,plain,
( e23 != op2(e23,e22)
| spl8_248 ),
inference(avatar_component_clause,[],[f1759]) ).
fof(f1762,plain,
( spl8_245
| spl8_246
| spl8_247
| spl8_248 ),
inference(avatar_split_clause,[],[f152,f1759,f1755,f1751,f1747]) ).
fof(f1763,plain,
( spl8_140
| spl8_144
| spl8_148
| spl8_152 ),
inference(avatar_split_clause,[],[f153,f1327,f1310,f1293,f1276]) ).
fof(f1785,definition,
( spl8_253
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_253])],[avatar_definition]) ).
fof(f1787,plain,
( e10 = unit1
| ~ spl8_253 ),
inference(avatar_component_clause,[],[f1785]) ).
fof(f1789,definition,
( spl8_254
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_254])],[avatar_definition]) ).
fof(f1791,plain,
( e11 = unit1
| ~ spl8_254 ),
inference(avatar_component_clause,[],[f1789]) ).
fof(f1793,definition,
( spl8_255
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_255])],[avatar_definition]) ).
fof(f1795,plain,
( e12 = unit1
| ~ spl8_255 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1797,definition,
( spl8_256
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl8_256])],[avatar_definition]) ).
fof(f1799,plain,
( e13 = unit1
| ~ spl8_256 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1800,plain,
( spl8_253
| spl8_254
| spl8_255
| spl8_256 ),
inference(avatar_split_clause,[],[f117,f1797,f1793,f1789,f1785]) ).
fof(f1807,definition,
( spl8_258
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl8_258])],[avatar_definition]) ).
fof(f1809,plain,
( e11 = op1(e10,e11)
| ~ spl8_258 ),
inference(avatar_component_clause,[],[f1807]) ).
fof(f1828,definition,
( spl8_263
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl8_263])],[avatar_definition]) ).
fof(f1830,plain,
( e12 = op1(e10,e12)
| ~ spl8_263 ),
inference(avatar_component_clause,[],[f1828]) ).
fof(f1849,definition,
( spl8_268
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl8_268])],[avatar_definition]) ).
fof(f1851,plain,
( e13 = op1(e10,e13)
| ~ spl8_268 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1854,definition,
( spl8_269
<=> e10 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_269])],[avatar_definition]) ).
fof(f1858,definition,
( spl8_270
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl8_270])],[avatar_definition]) ).
fof(f1860,plain,
( e11 = op1(e11,e10)
| ~ spl8_270 ),
inference(avatar_component_clause,[],[f1858]) ).
fof(f1870,plain,
( spl8_154
| spl8_158
| spl8_162
| spl8_166 ),
inference(avatar_split_clause,[],[f42,f1387,f1370,f1353,f1336]) ).
fof(f1872,definition,
( spl8_273
<=> e10 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl8_273])],[avatar_definition]) ).
fof(f1874,plain,
( e10 = op1(e11,e12)
| ~ spl8_273 ),
inference(avatar_component_clause,[],[f1872]) ).
fof(f1889,definition,
( spl8_277
<=> e10 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_277])],[avatar_definition]) ).
fof(f1893,definition,
( spl8_278
<=> e11 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_278])],[avatar_definition]) ).
fof(f1897,definition,
( spl8_279
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_279])],[avatar_definition]) ).
fof(f1899,plain,
( e12 = op1(e11,e13)
| ~ spl8_279 ),
inference(avatar_component_clause,[],[f1897]) ).
fof(f1901,definition,
( spl8_280
<=> e13 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl8_280])],[avatar_definition]) ).
fof(f1903,plain,
( e13 = op1(e11,e13)
| ~ spl8_280 ),
inference(avatar_component_clause,[],[f1901]) ).
fof(f1904,plain,
( spl8_277
| spl8_278
| spl8_279
| spl8_280 ),
inference(avatar_split_clause,[],[f44,f1901,f1897,f1893,f1889]) ).
fof(f1914,definition,
( spl8_283
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl8_283])],[avatar_definition]) ).
fof(f1916,plain,
( e12 = op1(e12,e10)
| ~ spl8_283 ),
inference(avatar_component_clause,[],[f1914]) ).
fof(f1923,definition,
( spl8_285
<=> e10 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_285])],[avatar_definition]) ).
fof(f1925,plain,
( e10 = op1(e12,e11)
| ~ spl8_285 ),
inference(avatar_component_clause,[],[f1923]) ).
fof(f1927,definition,
( spl8_286
<=> e11 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_286])],[avatar_definition]) ).
fof(f1931,definition,
( spl8_287
<=> e12 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_287])],[avatar_definition]) ).
fof(f1933,plain,
( e12 = op1(e12,e11)
| ~ spl8_287 ),
inference(avatar_component_clause,[],[f1931]) ).
fof(f1935,definition,
( spl8_288
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl8_288])],[avatar_definition]) ).
fof(f1938,plain,
( spl8_285
| spl8_286
| spl8_287
| spl8_288 ),
inference(avatar_split_clause,[],[f46,f1935,f1931,f1927,f1923]) ).
fof(f1945,definition,
( spl8_290
<=> e11 = op1(e12,e13) ),
introduced(definition,[new_symbols(definition,[spl8_290])],[avatar_definition]) ).
fof(f1947,plain,
( e11 = op1(e12,e13)
| ~ spl8_290 ),
inference(avatar_component_clause,[],[f1945]) ).
fof(f1970,definition,
( spl8_296
<=> e13 = op1(e13,e10) ),
introduced(definition,[new_symbols(definition,[spl8_296])],[avatar_definition]) ).
fof(f1972,plain,
( e13 = op1(e13,e10)
| ~ spl8_296 ),
inference(avatar_component_clause,[],[f1970]) ).
fof(f1975,definition,
( spl8_297
<=> e10 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_297])],[avatar_definition]) ).
fof(f1979,definition,
( spl8_298
<=> e11 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_298])],[avatar_definition]) ).
fof(f1983,definition,
( spl8_299
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_299])],[avatar_definition]) ).
fof(f1985,plain,
( e12 = op1(e13,e11)
| ~ spl8_299 ),
inference(avatar_component_clause,[],[f1983]) ).
fof(f1987,definition,
( spl8_300
<=> e13 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl8_300])],[avatar_definition]) ).
fof(f1989,plain,
( e13 = op1(e13,e11)
| ~ spl8_300 ),
inference(avatar_component_clause,[],[f1987]) ).
fof(f1990,plain,
( spl8_297
| spl8_298
| spl8_299
| spl8_300 ),
inference(avatar_split_clause,[],[f50,f1987,f1983,f1979,f1975]) ).
fof(f1992,definition,
( spl8_301
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_301])],[avatar_definition]) ).
fof(f1996,definition,
( spl8_302
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_302])],[avatar_definition]) ).
fof(f1998,plain,
( e11 = op1(e13,e12)
| ~ spl8_302 ),
inference(avatar_component_clause,[],[f1996]) ).
fof(f2000,definition,
( spl8_303
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_303])],[avatar_definition]) ).
fof(f2002,plain,
( e12 = op1(e13,e12)
| ~ spl8_303 ),
inference(avatar_component_clause,[],[f2000]) ).
fof(f2004,definition,
( spl8_304
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl8_304])],[avatar_definition]) ).
fof(f2007,plain,
( spl8_301
| spl8_302
| spl8_303
| spl8_304 ),
inference(avatar_split_clause,[],[f51,f2004,f2000,f1996,f1992]) ).
fof(f2008,plain,
( spl8_156
| spl8_160
| spl8_164
| spl8_168 ),
inference(avatar_split_clause,[],[f52,f1395,f1378,f1361,f1344]) ).
fof(f2013,plain,
( h2(op1(e12,e11)) != op2(e21,h2(e11))
| ~ spl8_18
| spl8_74 ),
inference(forward_demodulation,[],[f962,f702]) ).
fof(f2016,plain,
( e20 = inv2(e20)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f262,f1542]) ).
fof(f2017,plain,
( spl8_193
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f2016,f1540,f1520]) ).
fof(f2024,plain,
( e21 = e22
| ~ spl8_28
| ~ spl8_107 ),
inference(forward_demodulation,[],[f750,f1110]) ).
fof(f2032,plain,
( $false
| ~ spl8_28
| ~ spl8_107 ),
inference(forward_subsumption_resolution,[],[f389,f2024]) ).
fof(f2033,plain,
( ~ spl8_28
| ~ spl8_107 ),
inference(avatar_contradiction_clause,[],[f2032]) ).
fof(f2034,plain,
( e21 != e22
| spl8_28
| ~ spl8_107 ),
inference(forward_demodulation,[],[f751,f1110]) ).
fof(f2139,plain,
( e10 = op1(e11,e10)
| ~ spl8_254 ),
inference(forward_demodulation,[],[f125,f1791]) ).
fof(f2140,plain,
( spl8_269
| ~ spl8_254 ),
inference(avatar_split_clause,[],[f2139,f1789,f1854]) ).
fof(f2153,plain,
( e22 = op2(e22,e21)
| ~ spl8_198 ),
inference(forward_demodulation,[],[f221,f1546]) ).
fof(f2154,plain,
( spl8_231
| ~ spl8_198 ),
inference(avatar_split_clause,[],[f2153,f1544,f1686]) ).
fof(f2175,plain,
( e20 = op2(e21,e20)
| ~ spl8_198 ),
inference(forward_demodulation,[],[f226,f1546]) ).
fof(f2176,plain,
( spl8_213
| ~ spl8_198 ),
inference(avatar_split_clause,[],[f2175,f1544,f1609]) ).
fof(f2204,plain,
spl8_167,
inference(avatar_split_clause,[],[f417,f1391]) ).
fof(f2205,plain,
spl8_151,
inference(avatar_split_clause,[],[f420,f1323]) ).
fof(f2304,plain,
( h2(e10) != op2(e21,h2(e11))
| ~ spl8_18
| spl8_74
| ~ spl8_285 ),
inference(superposition,[],[f2013,f1925]) ).
fof(f2393,plain,
( e11 = op1(e11,e13)
| ~ spl8_256 ),
inference(forward_demodulation,[],[f122,f1799]) ).
fof(f2394,plain,
( spl8_278
| ~ spl8_256 ),
inference(avatar_split_clause,[],[f2393,f1797,f1893]) ).
fof(f2473,plain,
( e22 = op2(e22,e23)
| ~ spl8_200 ),
inference(forward_demodulation,[],[f221,f1554]) ).
fof(f2474,plain,
( spl8_235
| ~ spl8_200 ),
inference(avatar_split_clause,[],[f2473,f1552,f1704]) ).
fof(f2664,plain,
( e23 = h2(e13)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f427,f1320]) ).
fof(f2665,plain,
( spl8_88
| ~ spl8_150 ),
inference(avatar_split_clause,[],[f2664,f1319,f1028]) ).
fof(f2679,plain,
( e12 != op1(e13,e11)
| ~ spl8_303 ),
inference(forward_demodulation,[],[f287,f2002]) ).
fof(f2680,plain,
( ~ spl8_299
| ~ spl8_303 ),
inference(avatar_split_clause,[],[f2679,f2000,f1983]) ).
fof(f2687,plain,
( e13 != op1(e13,e10)
| ~ spl8_300 ),
inference(forward_demodulation,[],[f290,f1989]) ).
fof(f2702,plain,
( e13 != op1(e12,e11)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f293,f1392]) ).
fof(f2714,plain,
( e12 != op1(e12,e10)
| ~ spl8_287 ),
inference(forward_demodulation,[],[f296,f1933]) ).
fof(f2745,plain,
( ~ spl8_288
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f2702,f1391,f1935]) ).
fof(f2831,plain,
( e11 != op1(e12,e13)
| ~ spl8_160 ),
inference(forward_demodulation,[],[f309,f1362]) ).
fof(f2837,plain,
( e13 != op1(e10,e13)
| ~ spl8_280 ),
inference(forward_demodulation,[],[f314,f1903]) ).
fof(f2857,plain,
( ~ spl8_290
| ~ spl8_160 ),
inference(avatar_split_clause,[],[f2831,f1361,f1945]) ).
fof(f2863,plain,
( ~ spl8_268
| ~ spl8_280 ),
inference(avatar_split_clause,[],[f2837,f1901,f1849]) ).
fof(f2864,plain,
( ~ spl8_283
| ~ spl8_287 ),
inference(avatar_split_clause,[],[f2714,f1931,f1914]) ).
fof(f2942,plain,
( e13 != op1(e13,e12)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f315,f1392]) ).
fof(f2946,plain,
( ~ spl8_304
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f2942,f1391,f2004]) ).
fof(f2951,plain,
( ~ spl8_296
| ~ spl8_300 ),
inference(avatar_split_clause,[],[f2687,f1987,f1970]) ).
fof(f2986,plain,
( e23 != op2(e23,e20)
| ~ spl8_152 ),
inference(forward_demodulation,[],[f336,f1328]) ).
fof(f2987,plain,
( ~ spl8_240
| ~ spl8_152 ),
inference(avatar_split_clause,[],[f2986,f1327,f1725]) ).
fof(f3002,plain,
( e23 != op2(e22,e21)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f341,f1324]) ).
fof(f3003,plain,
( ~ spl8_232
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3002,f1323,f1690]) ).
fof(f3006,plain,
( e23 != op2(e22,e20)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f343,f1324]) ).
fof(f3011,plain,
( ~ spl8_228
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3006,f1323,f1673]) ).
fof(f3111,plain,
( e21 != op2(e22,e21)
| ~ spl8_234 ),
inference(forward_demodulation,[],[f340,f1702]) ).
fof(f3117,plain,
( e21 != op2(e22,e23)
| ~ spl8_226 ),
inference(forward_demodulation,[],[f342,f1667]) ).
fof(f3118,plain,
( ~ spl8_234
| ~ spl8_226 ),
inference(avatar_split_clause,[],[f3117,f1665,f1700]) ).
fof(f3168,plain,
( e21 != op2(e22,e23)
| ~ spl8_144 ),
inference(forward_demodulation,[],[f357,f1294]) ).
fof(f3174,plain,
( e23 != op2(e20,e23)
| ~ spl8_224 ),
inference(forward_demodulation,[],[f362,f1658]) ).
fof(f3178,plain,
( ~ spl8_212
| ~ spl8_224 ),
inference(avatar_split_clause,[],[f3174,f1656,f1604]) ).
fof(f3200,plain,
( e23 != op2(e23,e22)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f363,f1324]) ).
fof(f3205,plain,
( ~ spl8_248
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3200,f1323,f1759]) ).
fof(f3208,plain,
( e23 != op2(e23,e20)
| ~ spl8_244 ),
inference(forward_demodulation,[],[f338,f1744]) ).
fof(f3210,plain,
( ~ spl8_240
| ~ spl8_244 ),
inference(avatar_split_clause,[],[f3208,f1742,f1725]) ).
fof(f3232,plain,
( e21 != op2(e20,e21)
| ~ spl8_142 ),
inference(forward_demodulation,[],[f374,f1286]) ).
fof(f3241,plain,
( e11 = op1(e12,e13)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f418,f1392]) ).
fof(f3247,plain,
( spl8_290
| ~ spl8_167 ),
inference(avatar_split_clause,[],[f3241,f1391,f1945]) ).
fof(f3374,plain,
( e13 = op1(e13,e10)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f118,f1787]) ).
fof(f3375,plain,
( spl8_296
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3374,f1785,f1970]) ).
fof(f3387,plain,
( e13 = op1(e10,e13)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f119,f1787]) ).
fof(f3388,plain,
( spl8_268
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3387,f1785,f1849]) ).
fof(f3389,plain,
( e12 = op1(e12,e10)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f120,f1787]) ).
fof(f3390,plain,
( spl8_283
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3389,f1785,f1914]) ).
fof(f3391,plain,
( e12 = op1(e10,e12)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f121,f1787]) ).
fof(f3392,plain,
( e11 = op1(e11,e10)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f122,f1787]) ).
fof(f3393,plain,
( spl8_270
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3392,f1785,f1858]) ).
fof(f3394,plain,
( e11 = op1(e10,e11)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f123,f1787]) ).
fof(f3395,plain,
( spl8_258
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3394,f1785,f1807]) ).
fof(f3396,plain,
( e10 = op1(e10,e10)
| ~ spl8_253 ),
inference(forward_demodulation,[],[f124,f1787]) ).
fof(f3397,plain,
( spl8_153
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3396,f1785,f1332]) ).
fof(f3530,plain,
( e11 != op1(e12,e11)
| ~ spl8_290 ),
inference(forward_demodulation,[],[f292,f1947]) ).
fof(f3537,plain,
( e10 != op1(e11,e11)
| ~ spl8_273 ),
inference(forward_demodulation,[],[f299,f1874]) ).
fof(f3540,plain,
( ~ spl8_154
| ~ spl8_273 ),
inference(avatar_split_clause,[],[f3537,f1872,f1336]) ).
fof(f3547,plain,
( e10 != op1(e11,e13)
| ~ spl8_273 ),
inference(forward_demodulation,[],[f297,f1874]) ).
fof(f3554,plain,
( e10 != op1(e11,e10)
| ~ spl8_273 ),
inference(forward_demodulation,[],[f301,f1874]) ).
fof(f3568,plain,
( e11 != op1(e11,e13)
| ~ spl8_290 ),
inference(forward_demodulation,[],[f311,f1947]) ).
fof(f3593,plain,
( e21 = op2(e22,e23)
| ~ spl8_151 ),
inference(forward_demodulation,[],[f421,f1324]) ).
fof(f3594,plain,
( e20 = e21
| ~ spl8_151
| ~ spl8_233 ),
inference(forward_demodulation,[],[f3593,f1698]) ).
fof(f3595,plain,
( $false
| ~ spl8_151
| ~ spl8_233 ),
inference(forward_subsumption_resolution,[],[f3594,f392]) ).
fof(f3596,plain,
( ~ spl8_151
| ~ spl8_233 ),
inference(avatar_contradiction_clause,[],[f3595]) ).
fof(f3600,plain,
( ~ spl8_234
| ~ spl8_144 ),
inference(avatar_split_clause,[],[f3168,f1293,f1700]) ).
fof(f3603,plain,
( spl8_234
| ~ spl8_151 ),
inference(avatar_split_clause,[],[f3593,f1323,f1700]) ).
fof(f3606,plain,
( e20 != op2(e22,e20)
| ~ spl8_213 ),
inference(forward_demodulation,[],[f377,f1611]) ).
fof(f3619,plain,
( ~ spl8_225
| ~ spl8_213 ),
inference(avatar_split_clause,[],[f3606,f1609,f1661]) ).
fof(f3624,plain,
( ~ spl8_230
| ~ spl8_234 ),
inference(avatar_split_clause,[],[f3111,f1700,f1682]) ).
fof(f3644,plain,
( e20 != op2(e21,e22)
| ~ spl8_245 ),
inference(forward_demodulation,[],[f364,f1749]) ).
fof(f3647,plain,
( ~ spl8_217
| ~ spl8_245 ),
inference(avatar_split_clause,[],[f3644,f1747,f1627]) ).
fof(f3696,plain,
( op2(e22,e22) = unit2
| ~ spl8_195 ),
inference(forward_demodulation,[],[f233,f1532]) ).
fof(f3718,plain,
( e23 = op2(e23,e22)
| ~ spl8_199 ),
inference(forward_demodulation,[],[f219,f1550]) ).
fof(f3719,plain,
( $false
| ~ spl8_199
| spl8_248 ),
inference(forward_subsumption_resolution,[],[f3718,f1760]) ).
fof(f3720,plain,
( ~ spl8_199
| spl8_248 ),
inference(avatar_contradiction_clause,[],[f3719]) ).
fof(f3725,plain,
( e23 = unit2
| ~ spl8_151
| ~ spl8_195 ),
inference(forward_demodulation,[],[f3696,f1324]) ).
fof(f3749,plain,
( spl8_200
| ~ spl8_151
| ~ spl8_195 ),
inference(avatar_split_clause,[],[f3725,f1530,f1323,f1552]) ).
fof(f3899,plain,
( e21 = e22
| ~ spl8_234
| ~ spl8_235 ),
inference(superposition,[],[f1706,f1702]) ).
fof(f3905,plain,
( $false
| spl8_28
| ~ spl8_107
| ~ spl8_234
| ~ spl8_235 ),
inference(forward_subsumption_resolution,[],[f3899,f2034]) ).
fof(f3906,plain,
( spl8_28
| ~ spl8_107
| ~ spl8_234
| ~ spl8_235 ),
inference(avatar_contradiction_clause,[],[f3905]) ).
fof(f3912,plain,
( e20 != inv2(e22)
| ~ spl8_193 ),
inference(forward_demodulation,[],[f283,f1522]) ).
fof(f3917,plain,
( ~ spl8_171
| ~ spl8_193 ),
inference(avatar_split_clause,[],[f3912,f1520,f1409]) ).
fof(f3930,plain,
( e23 = op2(e23,e20)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f219,f1542]) ).
fof(f3931,plain,
( spl8_240
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3930,f1540,f1725]) ).
fof(f3932,plain,
( e23 = op2(e20,e23)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f220,f1542]) ).
fof(f3935,plain,
( spl8_212
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3932,f1540,f1604]) ).
fof(f3936,plain,
( e22 = op2(e22,e20)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f221,f1542]) ).
fof(f3939,plain,
( spl8_227
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3936,f1540,f1669]) ).
fof(f3940,plain,
( e22 = op2(e20,e22)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f222,f1542]) ).
fof(f3941,plain,
( e21 = op2(e21,e20)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f223,f1542]) ).
fof(f3942,plain,
( e21 = op2(e20,e21)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f224,f1542]) ).
fof(f3943,plain,
( e20 = op2(e20,e20)
| ~ spl8_197 ),
inference(forward_demodulation,[],[f225,f1542]) ).
fof(f3946,plain,
( spl8_137
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3943,f1540,f1264]) ).
fof(f4007,plain,
( op2(e22,e23) = unit2
| ~ spl8_179 ),
inference(forward_demodulation,[],[f231,f1450]) ).
fof(f4008,plain,
( e20 = op2(e22,e23)
| ~ spl8_179
| ~ spl8_197 ),
inference(forward_demodulation,[],[f4007,f1542]) ).
fof(f4009,plain,
( $false
| ~ spl8_179
| ~ spl8_197
| spl8_233 ),
inference(forward_subsumption_resolution,[],[f4008,f1697]) ).
fof(f4010,plain,
( ~ spl8_179
| ~ spl8_197
| spl8_233 ),
inference(avatar_contradiction_clause,[],[f4009]) ).
fof(f4035,plain,
( op2(e21,e22) = unit2
| ~ spl8_175 ),
inference(forward_demodulation,[],[f233,f1430]) ).
fof(f4036,plain,
( e20 = op2(e21,e22)
| ~ spl8_175
| ~ spl8_197 ),
inference(forward_demodulation,[],[f4035,f1542]) ).
fof(f4039,plain,
( spl8_217
| ~ spl8_175
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f4036,f1540,f1428,f1627]) ).
fof(f4077,plain,
( e20 != op2(e23,e21)
| ~ spl8_140 ),
inference(forward_demodulation,[],[f334,f1277]) ).
fof(f4092,plain,
( e20 != op2(e21,e21)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f347,f1629]) ).
fof(f4097,plain,
( ~ spl8_138
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f4092,f1627,f1268]) ).
fof(f4107,plain,
( e21 != op2(e21,e20)
| ~ spl8_222 ),
inference(forward_demodulation,[],[f348,f1650]) ).
fof(f4113,plain,
( spl8_214
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3941,f1540,f1613]) ).
fof(f4114,plain,
( ~ spl8_214
| ~ spl8_222 ),
inference(avatar_split_clause,[],[f4107,f1648,f1613]) ).
fof(f4115,plain,
( e20 != op2(e21,e23)
| ~ spl8_217 ),
inference(forward_demodulation,[],[f345,f1629]) ).
fof(f4116,plain,
( e22 != op2(e21,e23)
| ~ spl8_146 ),
inference(forward_demodulation,[],[f346,f1303]) ).
fof(f4117,plain,
( ~ spl8_221
| ~ spl8_217 ),
inference(avatar_split_clause,[],[f4115,f1627,f1644]) ).
fof(f4118,plain,
( ~ spl8_223
| ~ spl8_146 ),
inference(avatar_split_clause,[],[f4116,f1302,f1652]) ).
fof(f4121,plain,
( $false
| ~ spl8_142
| ~ spl8_202 ),
inference(forward_subsumption_resolution,[],[f3232,f1564]) ).
fof(f4122,plain,
( ~ spl8_142
| ~ spl8_202 ),
inference(avatar_contradiction_clause,[],[f4121]) ).
fof(f4168,plain,
( e21 != op2(e23,e22)
| ~ spl8_242 ),
inference(forward_demodulation,[],[f335,f1736]) ).
fof(f4171,plain,
( e22 != op2(e23,e22)
| ~ spl8_207 ),
inference(forward_demodulation,[],[f366,f1585]) ).
fof(f4172,plain,
( ~ spl8_246
| ~ spl8_242 ),
inference(avatar_split_clause,[],[f4168,f1734,f1751]) ).
fof(f4173,plain,
( ~ spl8_247
| ~ spl8_207 ),
inference(avatar_split_clause,[],[f4171,f1583,f1755]) ).
fof(f4175,plain,
( ~ spl8_241
| ~ spl8_140 ),
inference(avatar_split_clause,[],[f4077,f1276,f1730]) ).
fof(f4180,plain,
( e22 != op2(e23,e23)
| ~ spl8_223 ),
inference(forward_demodulation,[],[f358,f1654]) ).
fof(f4183,plain,
( ~ spl8_148
| ~ spl8_223 ),
inference(avatar_split_clause,[],[f4180,f1652,f1310]) ).
fof(f4185,plain,
( spl8_207
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3940,f1540,f1583]) ).
fof(f4226,plain,
( op2(e21,e23) = h2(e11)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f428,f1320]) ).
fof(f4227,plain,
( e22 = h2(e11)
| ~ spl8_150
| ~ spl8_223 ),
inference(forward_demodulation,[],[f4226,f1654]) ).
fof(f4228,plain,
( spl8_84
| ~ spl8_150
| ~ spl8_223 ),
inference(avatar_split_clause,[],[f4227,f1652,f1319,f1002]) ).
fof(f4229,plain,
( op2(e21,e22) != h2(e10)
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_285 ),
inference(superposition,[],[f2304,f1003]) ).
fof(f4231,plain,
( e20 != h2(e10)
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_217
| ~ spl8_285 ),
inference(forward_demodulation,[],[f4229,f1629]) ).
fof(f4248,plain,
( e10 = op1(op1(e12,e13),e12)
| ~ spl8_167 ),
inference(forward_demodulation,[],[f419,f1392]) ).
fof(f4249,plain,
( e10 = op1(e11,e12)
| ~ spl8_167
| ~ spl8_290 ),
inference(forward_demodulation,[],[f4248,f1947]) ).
fof(f4312,plain,
( e12 != op1(e11,e11)
| ~ spl8_279 ),
inference(forward_demodulation,[],[f298,f1899]) ).
fof(f4314,plain,
( e11 != op1(e11,e11)
| ~ spl8_258 ),
inference(forward_demodulation,[],[f326,f1809]) ).
fof(f4317,plain,
( ~ spl8_162
| ~ spl8_279 ),
inference(avatar_split_clause,[],[f4312,f1897,f1370]) ).
fof(f4323,plain,
( ~ spl8_158
| ~ spl8_258 ),
inference(avatar_split_clause,[],[f4314,f1807,f1353]) ).
fof(f4325,plain,
( e10 != op1(e13,e11)
| ~ spl8_285 ),
inference(forward_demodulation,[],[f321,f1925]) ).
fof(f4326,plain,
( e11 != op1(e13,e11)
| ~ spl8_258 ),
inference(forward_demodulation,[],[f324,f1809]) ).
fof(f4329,plain,
( ~ spl8_277
| ~ spl8_273 ),
inference(avatar_split_clause,[],[f3547,f1872,f1889]) ).
fof(f4331,plain,
( ~ spl8_297
| ~ spl8_285 ),
inference(avatar_split_clause,[],[f4325,f1923,f1975]) ).
fof(f4447,plain,
( op2(op2(e21,e23),e21) = h2(e10)
| ~ spl8_150 ),
inference(forward_demodulation,[],[f429,f1320]) ).
fof(f4448,plain,
( op2(e22,e21) = h2(e10)
| ~ spl8_150
| ~ spl8_223 ),
inference(forward_demodulation,[],[f4447,f1654]) ).
fof(f4449,plain,
( e20 = h2(e10)
| ~ spl8_150
| ~ spl8_223
| ~ spl8_229 ),
inference(forward_demodulation,[],[f4448,f1680]) ).
fof(f4452,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_217
| ~ spl8_285 ),
inference(avatar_split_clause,[],[f4231,f1923,f1627,f1002,f960,f701,f687]) ).
fof(f4453,plain,
( spl8_15
| ~ spl8_150
| ~ spl8_223
| ~ spl8_229 ),
inference(avatar_split_clause,[],[f4449,f1678,f1652,f1319,f687]) ).
fof(f4454,plain,
( h2(e10) != op2(h2(e10),h2(e10))
| spl8_65
| ~ spl8_153 ),
inference(forward_demodulation,[],[f926,f1333]) ).
fof(f4460,plain,
( e20 != op2(e20,e20)
| ~ spl8_15
| spl8_65
| ~ spl8_153 ),
inference(forward_demodulation,[],[f4454,f688]) ).
fof(f4461,plain,
( $false
| ~ spl8_15
| spl8_65
| ~ spl8_137
| ~ spl8_153 ),
inference(forward_subsumption_resolution,[],[f4460,f1265]) ).
fof(f4462,plain,
( ~ spl8_15
| spl8_65
| ~ spl8_137
| ~ spl8_153 ),
inference(avatar_contradiction_clause,[],[f4461]) ).
fof(f4464,plain,
( h2(op1(e10,e11)) != op2(h2(e10),e22)
| spl8_66
| ~ spl8_84 ),
inference(forward_demodulation,[],[f930,f1003]) ).
fof(f4466,plain,
( op2(e20,e22) != h2(op1(e10,e11))
| ~ spl8_15
| spl8_66
| ~ spl8_84 ),
inference(forward_demodulation,[],[f4464,f688]) ).
fof(f4468,plain,
( op2(e20,e22) != h2(e11)
| ~ spl8_15
| spl8_66
| ~ spl8_84
| ~ spl8_258 ),
inference(forward_demodulation,[],[f4466,f1809]) ).
fof(f4469,plain,
( e22 != op2(e20,e22)
| ~ spl8_15
| spl8_66
| ~ spl8_84
| ~ spl8_258 ),
inference(forward_demodulation,[],[f4468,f1003]) ).
fof(f4470,plain,
( $false
| ~ spl8_15
| spl8_66
| ~ spl8_84
| ~ spl8_207
| ~ spl8_258 ),
inference(forward_subsumption_resolution,[],[f4469,f1585]) ).
fof(f4471,plain,
( ~ spl8_15
| spl8_66
| ~ spl8_84
| ~ spl8_207
| ~ spl8_258 ),
inference(avatar_contradiction_clause,[],[f4470]) ).
fof(f4473,plain,
( h2(op1(e10,e12)) != op2(h2(e10),e21)
| ~ spl8_18
| spl8_67 ),
inference(forward_demodulation,[],[f934,f702]) ).
fof(f4475,plain,
( op2(e20,e21) != h2(op1(e10,e12))
| ~ spl8_15
| ~ spl8_18
| spl8_67 ),
inference(forward_demodulation,[],[f4473,f688]) ).
fof(f4477,plain,
( op2(e20,e21) != h2(e12)
| ~ spl8_15
| ~ spl8_18
| spl8_67
| ~ spl8_263 ),
inference(forward_demodulation,[],[f4475,f1830]) ).
fof(f4479,plain,
( e21 != op2(e20,e21)
| ~ spl8_15
| ~ spl8_18
| spl8_67
| ~ spl8_263 ),
inference(forward_demodulation,[],[f4477,f702]) ).
fof(f4483,plain,
( h2(op1(e10,e13)) != op2(h2(e10),e23)
| spl8_68
| ~ spl8_88 ),
inference(forward_demodulation,[],[f938,f1029]) ).
fof(f4485,plain,
( op2(e20,e23) != h2(op1(e10,e13))
| ~ spl8_15
| spl8_68
| ~ spl8_88 ),
inference(forward_demodulation,[],[f4483,f688]) ).
fof(f4487,plain,
( op2(e20,e23) != h2(e13)
| ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_268 ),
inference(forward_demodulation,[],[f4485,f1851]) ).
fof(f4489,plain,
( e23 != op2(e20,e23)
| ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_268 ),
inference(forward_demodulation,[],[f4487,f1029]) ).
fof(f4490,plain,
( $false
| ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_212
| ~ spl8_268 ),
inference(forward_subsumption_resolution,[],[f4489,f1606]) ).
fof(f4491,plain,
( ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_212
| ~ spl8_268 ),
inference(avatar_contradiction_clause,[],[f4490]) ).
fof(f4493,plain,
( h2(op1(e11,e10)) != op2(h2(e11),e20)
| ~ spl8_15
| spl8_69 ),
inference(forward_demodulation,[],[f942,f688]) ).
fof(f4495,plain,
( op2(e22,e20) != h2(op1(e11,e10))
| ~ spl8_15
| spl8_69
| ~ spl8_84 ),
inference(forward_demodulation,[],[f4493,f1003]) ).
fof(f4497,plain,
( op2(e22,e20) != h2(e11)
| ~ spl8_15
| spl8_69
| ~ spl8_84
| ~ spl8_270 ),
inference(forward_demodulation,[],[f4495,f1860]) ).
fof(f4499,plain,
( e22 != op2(e22,e20)
| ~ spl8_15
| spl8_69
| ~ spl8_84
| ~ spl8_270 ),
inference(forward_demodulation,[],[f4497,f1003]) ).
fof(f4500,plain,
( $false
| ~ spl8_15
| spl8_69
| ~ spl8_84
| ~ spl8_227
| ~ spl8_270 ),
inference(forward_subsumption_resolution,[],[f4499,f1671]) ).
fof(f4501,plain,
( ~ spl8_15
| spl8_69
| ~ spl8_84
| ~ spl8_227
| ~ spl8_270 ),
inference(avatar_contradiction_clause,[],[f4500]) ).
fof(f4503,plain,
( op2(e22,e22) != h2(op1(e11,e11))
| spl8_70
| ~ spl8_84 ),
inference(forward_demodulation,[],[f946,f1003]) ).
fof(f4505,plain,
( op2(e22,e22) != h2(e13)
| spl8_70
| ~ spl8_84
| ~ spl8_166 ),
inference(forward_demodulation,[],[f4503,f1388]) ).
fof(f4507,plain,
( e23 != op2(e22,e22)
| spl8_70
| ~ spl8_84
| ~ spl8_88
| ~ spl8_166 ),
inference(forward_demodulation,[],[f4505,f1029]) ).
fof(f4509,plain,
( $false
| spl8_70
| ~ spl8_84
| ~ spl8_88
| ~ spl8_151
| ~ spl8_166 ),
inference(forward_subsumption_resolution,[],[f4507,f1324]) ).
fof(f4510,plain,
( spl8_70
| ~ spl8_84
| ~ spl8_88
| ~ spl8_151
| ~ spl8_166 ),
inference(avatar_contradiction_clause,[],[f4509]) ).
fof(f4512,plain,
( h2(op1(e11,e12)) != op2(h2(e11),e21)
| ~ spl8_18
| spl8_71 ),
inference(forward_demodulation,[],[f950,f702]) ).
fof(f4514,plain,
( op2(e22,e21) != h2(op1(e11,e12))
| ~ spl8_18
| spl8_71
| ~ spl8_84 ),
inference(forward_demodulation,[],[f4512,f1003]) ).
fof(f4516,plain,
( op2(e22,e21) != h2(e10)
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_273 ),
inference(forward_demodulation,[],[f4514,f1874]) ).
fof(f4517,plain,
( e20 != op2(e22,e21)
| ~ spl8_15
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_273 ),
inference(forward_demodulation,[],[f4516,f688]) ).
fof(f4518,plain,
( $false
| ~ spl8_15
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_229
| ~ spl8_273 ),
inference(forward_subsumption_resolution,[],[f4517,f1680]) ).
fof(f4519,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_229
| ~ spl8_273 ),
inference(avatar_contradiction_clause,[],[f4518]) ).
fof(f4521,plain,
( h2(op1(e11,e13)) != op2(h2(e11),e23)
| spl8_72
| ~ spl8_88 ),
inference(forward_demodulation,[],[f954,f1029]) ).
fof(f4523,plain,
( op2(e22,e23) != h2(op1(e11,e13))
| spl8_72
| ~ spl8_84
| ~ spl8_88 ),
inference(forward_demodulation,[],[f4521,f1003]) ).
fof(f4525,plain,
( op2(e22,e23) != h2(e12)
| spl8_72
| ~ spl8_84
| ~ spl8_88
| ~ spl8_279 ),
inference(forward_demodulation,[],[f4523,f1899]) ).
fof(f4527,plain,
( e21 != op2(e22,e23)
| ~ spl8_18
| spl8_72
| ~ spl8_84
| ~ spl8_88
| ~ spl8_279 ),
inference(forward_demodulation,[],[f4525,f702]) ).
fof(f4528,plain,
( $false
| ~ spl8_18
| spl8_72
| ~ spl8_84
| ~ spl8_88
| ~ spl8_234
| ~ spl8_279 ),
inference(forward_subsumption_resolution,[],[f4527,f1702]) ).
fof(f4529,plain,
( ~ spl8_18
| spl8_72
| ~ spl8_84
| ~ spl8_88
| ~ spl8_234
| ~ spl8_279 ),
inference(avatar_contradiction_clause,[],[f4528]) ).
fof(f4531,plain,
( h2(op1(e12,e10)) != op2(h2(e12),e20)
| ~ spl8_15
| spl8_73 ),
inference(forward_demodulation,[],[f958,f688]) ).
fof(f4533,plain,
( op2(e21,e20) != h2(op1(e12,e10))
| ~ spl8_15
| ~ spl8_18
| spl8_73 ),
inference(forward_demodulation,[],[f4531,f702]) ).
fof(f4535,plain,
( op2(e21,e20) != h2(e12)
| ~ spl8_15
| ~ spl8_18
| spl8_73
| ~ spl8_283 ),
inference(forward_demodulation,[],[f4533,f1916]) ).
fof(f4537,plain,
( e21 != op2(e21,e20)
| ~ spl8_15
| ~ spl8_18
| spl8_73
| ~ spl8_283 ),
inference(forward_demodulation,[],[f4535,f702]) ).
fof(f4538,plain,
( $false
| ~ spl8_15
| ~ spl8_18
| spl8_73
| ~ spl8_214
| ~ spl8_283 ),
inference(forward_subsumption_resolution,[],[f4537,f1615]) ).
fof(f4539,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_73
| ~ spl8_214
| ~ spl8_283 ),
inference(avatar_contradiction_clause,[],[f4538]) ).
fof(f4541,plain,
( op2(e21,e21) != h2(op1(e12,e12))
| ~ spl8_18
| spl8_75 ),
inference(forward_demodulation,[],[f966,f702]) ).
fof(f4543,plain,
( op2(e21,e21) != h2(e13)
| ~ spl8_18
| spl8_75
| ~ spl8_167 ),
inference(forward_demodulation,[],[f4541,f1392]) ).
fof(f4545,plain,
( e23 != op2(e21,e21)
| ~ spl8_18
| spl8_75
| ~ spl8_88
| ~ spl8_167 ),
inference(forward_demodulation,[],[f4543,f1029]) ).
fof(f4547,plain,
( $false
| ~ spl8_18
| spl8_75
| ~ spl8_88
| ~ spl8_150
| ~ spl8_167 ),
inference(forward_subsumption_resolution,[],[f4545,f1320]) ).
fof(f4548,plain,
( ~ spl8_18
| spl8_75
| ~ spl8_88
| ~ spl8_150
| ~ spl8_167 ),
inference(avatar_contradiction_clause,[],[f4547]) ).
fof(f4550,plain,
( h2(op1(e12,e13)) != op2(h2(e12),e23)
| spl8_76
| ~ spl8_88 ),
inference(forward_demodulation,[],[f970,f1029]) ).
fof(f4552,plain,
( op2(e21,e23) != h2(op1(e12,e13))
| ~ spl8_18
| spl8_76
| ~ spl8_88 ),
inference(forward_demodulation,[],[f4550,f702]) ).
fof(f4554,plain,
( op2(e21,e23) != h2(e11)
| ~ spl8_18
| spl8_76
| ~ spl8_88
| ~ spl8_290 ),
inference(forward_demodulation,[],[f4552,f1947]) ).
fof(f4555,plain,
( e22 != op2(e21,e23)
| ~ spl8_18
| spl8_76
| ~ spl8_84
| ~ spl8_88
| ~ spl8_290 ),
inference(forward_demodulation,[],[f4554,f1003]) ).
fof(f4556,plain,
( $false
| ~ spl8_18
| spl8_76
| ~ spl8_84
| ~ spl8_88
| ~ spl8_223
| ~ spl8_290 ),
inference(forward_subsumption_resolution,[],[f4555,f1654]) ).
fof(f4557,plain,
( ~ spl8_18
| spl8_76
| ~ spl8_84
| ~ spl8_88
| ~ spl8_223
| ~ spl8_290 ),
inference(avatar_contradiction_clause,[],[f4556]) ).
fof(f4559,plain,
( h2(op1(e13,e10)) != op2(h2(e13),e20)
| ~ spl8_15
| spl8_77 ),
inference(forward_demodulation,[],[f974,f688]) ).
fof(f4561,plain,
( op2(e23,e20) != h2(op1(e13,e10))
| ~ spl8_15
| spl8_77
| ~ spl8_88 ),
inference(forward_demodulation,[],[f4559,f1029]) ).
fof(f4563,plain,
( op2(e23,e20) != h2(e13)
| ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_296 ),
inference(forward_demodulation,[],[f4561,f1972]) ).
fof(f4565,plain,
( e23 != op2(e23,e20)
| ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_296 ),
inference(forward_demodulation,[],[f4563,f1029]) ).
fof(f4566,plain,
( $false
| ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_240
| ~ spl8_296 ),
inference(forward_subsumption_resolution,[],[f4565,f1727]) ).
fof(f4567,plain,
( ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_240
| ~ spl8_296 ),
inference(avatar_contradiction_clause,[],[f4566]) ).
fof(f4569,plain,
( h2(op1(e13,e11)) != op2(h2(e13),e22)
| spl8_78
| ~ spl8_84 ),
inference(forward_demodulation,[],[f978,f1003]) ).
fof(f4571,plain,
( op2(e23,e22) != h2(op1(e13,e11))
| spl8_78
| ~ spl8_84
| ~ spl8_88 ),
inference(forward_demodulation,[],[f4569,f1029]) ).
fof(f4573,plain,
( op2(e23,e22) != h2(e12)
| spl8_78
| ~ spl8_84
| ~ spl8_88
| ~ spl8_299 ),
inference(forward_demodulation,[],[f4571,f1985]) ).
fof(f4575,plain,
( e21 != op2(e23,e22)
| ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_88
| ~ spl8_299 ),
inference(forward_demodulation,[],[f4573,f702]) ).
fof(f4576,plain,
( $false
| ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_88
| ~ spl8_246
| ~ spl8_299 ),
inference(forward_subsumption_resolution,[],[f4575,f1753]) ).
fof(f4577,plain,
( ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_88
| ~ spl8_246
| ~ spl8_299 ),
inference(avatar_contradiction_clause,[],[f4576]) ).
fof(f4579,plain,
( h2(op1(e13,e12)) != op2(h2(e13),e21)
| ~ spl8_18
| spl8_79 ),
inference(forward_demodulation,[],[f982,f702]) ).
fof(f4581,plain,
( op2(e23,e21) != h2(op1(e13,e12))
| ~ spl8_18
| spl8_79
| ~ spl8_88 ),
inference(forward_demodulation,[],[f4579,f1029]) ).
fof(f4583,plain,
( op2(e23,e21) != h2(e11)
| ~ spl8_18
| spl8_79
| ~ spl8_88
| ~ spl8_302 ),
inference(forward_demodulation,[],[f4581,f1998]) ).
fof(f4585,plain,
( e22 != op2(e23,e21)
| ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_88
| ~ spl8_302 ),
inference(forward_demodulation,[],[f4583,f1003]) ).
fof(f4586,plain,
( $false
| ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_88
| ~ spl8_243
| ~ spl8_302 ),
inference(forward_subsumption_resolution,[],[f4585,f1740]) ).
fof(f4587,plain,
( ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_88
| ~ spl8_243
| ~ spl8_302 ),
inference(avatar_contradiction_clause,[],[f4586]) ).
fof(f4589,plain,
( op2(e23,e23) != h2(op1(e13,e13))
| spl8_80
| ~ spl8_88 ),
inference(forward_demodulation,[],[f986,f1029]) ).
fof(f4591,plain,
( op2(e23,e23) != h2(e10)
| spl8_80
| ~ spl8_88
| ~ spl8_156 ),
inference(forward_demodulation,[],[f4589,f1345]) ).
fof(f4593,plain,
( e20 != op2(e23,e23)
| ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_156 ),
inference(forward_demodulation,[],[f4591,f688]) ).
fof(f4595,plain,
( $false
| ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_140
| ~ spl8_156 ),
inference(forward_subsumption_resolution,[],[f4593,f1277]) ).
fof(f4596,plain,
( ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_140
| ~ spl8_156 ),
inference(avatar_contradiction_clause,[],[f4595]) ).
fof(f4600,plain,
( ~ spl8_202
| ~ spl8_15
| ~ spl8_18
| spl8_67
| ~ spl8_263 ),
inference(avatar_split_clause,[],[f4479,f1828,f932,f701,f687,f1562]) ).
fof(f4604,plain,
( spl8_202
| ~ spl8_197 ),
inference(avatar_split_clause,[],[f3942,f1540,f1562]) ).
fof(f4617,plain,
( spl8_263
| ~ spl8_253 ),
inference(avatar_split_clause,[],[f3391,f1785,f1828]) ).
fof(f4630,plain,
( e10 != op1(e13,e12)
| ~ spl8_273 ),
inference(forward_demodulation,[],[f316,f1874]) ).
fof(f4635,plain,
( ~ spl8_298
| ~ spl8_258 ),
inference(avatar_split_clause,[],[f4326,f1807,f1979]) ).
fof(f4654,plain,
( ~ spl8_301
| ~ spl8_273 ),
inference(avatar_split_clause,[],[f4630,f1872,f1992]) ).
fof(f4661,plain,
( e22 != op2(e22,e21)
| ~ spl8_227 ),
inference(forward_demodulation,[],[f344,f1671]) ).
fof(f4666,plain,
( e12 != op1(e13,e13)
| ~ spl8_279 ),
inference(forward_demodulation,[],[f310,f1899]) ).
fof(f4667,plain,
( e13 != op1(e13,e13)
| ~ spl8_268 ),
inference(forward_demodulation,[],[f312,f1851]) ).
fof(f4683,plain,
( ~ spl8_231
| ~ spl8_227 ),
inference(avatar_split_clause,[],[f4661,f1669,f1686]) ).
fof(f4685,plain,
( ~ spl8_168
| ~ spl8_268 ),
inference(avatar_split_clause,[],[f4667,f1849,f1395]) ).
fof(f4710,plain,
( ~ spl8_286
| ~ spl8_290 ),
inference(avatar_split_clause,[],[f3530,f1945,f1927]) ).
fof(f4720,plain,
( spl8_273
| ~ spl8_167
| ~ spl8_290 ),
inference(avatar_split_clause,[],[f4249,f1945,f1391,f1872]) ).
fof(f4724,plain,
( ~ spl8_164
| ~ spl8_279 ),
inference(avatar_split_clause,[],[f4666,f1897,f1378]) ).
fof(f4757,plain,
( ~ spl8_278
| ~ spl8_290 ),
inference(avatar_split_clause,[],[f3568,f1945,f1893]) ).
fof(f4780,plain,
( ~ spl8_269
| ~ spl8_273 ),
inference(avatar_split_clause,[],[f3554,f1872,f1854]) ).
fof(f4826,plain,
( e13 = op1(e13,e12)
| ~ spl8_255 ),
inference(forward_demodulation,[],[f118,f1795]) ).
fof(f4827,plain,
( spl8_304
| ~ spl8_255 ),
inference(avatar_split_clause,[],[f4826,f1793,f2004]) ).
cnf(s12,plain,
( spl8_11
| ~ spl8_15 ),
inference(sat_conversion,[],[f690]) ).
cnf(s14,plain,
( ~ spl8_16
| ~ spl8_18 ),
inference(sat_conversion,[],[f704]) ).
cnf(s63,plain,
( ~ spl8_11
| spl8_16
| ~ spl8_65
| ~ spl8_66
| ~ spl8_67
| ~ spl8_68
| ~ spl8_69
| ~ spl8_70
| ~ spl8_71
| ~ spl8_72
| ~ spl8_73
| ~ spl8_74
| ~ spl8_75
| ~ spl8_76
| ~ spl8_77
| ~ spl8_78
| ~ spl8_79
| ~ spl8_80
| ~ spl8_84
| ~ spl8_88 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s98,plain,
spl8_107,
inference(sat_conversion,[],[f1260]) ).
cnf(s99,plain,
spl8_18,
inference(sat_conversion,[],[f1261]) ).
cnf(s117,plain,
( spl8_179
| ~ spl8_180 ),
inference(sat_conversion,[],[f1455]) ).
cnf(s135,plain,
( spl8_171
| spl8_175
| spl8_180
| spl8_195 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s137,plain,
( spl8_197
| spl8_198
| spl8_199
| spl8_200 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s143,plain,
( spl8_138
| spl8_142
| spl8_146
| spl8_150 ),
inference(sat_conversion,[],[f1625]) ).
cnf(s145,plain,
( spl8_221
| spl8_222
| spl8_223
| spl8_224 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s146,plain,
( spl8_225
| spl8_226
| spl8_227
| spl8_228 ),
inference(sat_conversion,[],[f1676]) ).
cnf(s147,plain,
( spl8_229
| spl8_230
| spl8_231
| spl8_232 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s151,plain,
( spl8_241
| spl8_242
| spl8_243
| spl8_244 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s152,plain,
( spl8_245
| spl8_246
| spl8_247
| spl8_248 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s153,plain,
( spl8_140
| spl8_144
| spl8_148
| spl8_152 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s158,plain,
( spl8_253
| spl8_254
| spl8_255
| spl8_256 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s164,plain,
( spl8_154
| spl8_158
| spl8_162
| spl8_166 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s166,plain,
( spl8_277
| spl8_278
| spl8_279
| spl8_280 ),
inference(sat_conversion,[],[f1904]) ).
cnf(s168,plain,
( spl8_285
| spl8_286
| spl8_287
| spl8_288 ),
inference(sat_conversion,[],[f1938]) ).
cnf(s172,plain,
( spl8_297
| spl8_298
| spl8_299
| spl8_300 ),
inference(sat_conversion,[],[f1990]) ).
cnf(s173,plain,
( spl8_301
| spl8_302
| spl8_303
| spl8_304 ),
inference(sat_conversion,[],[f2007]) ).
cnf(s174,plain,
( spl8_156
| spl8_160
| spl8_164
| spl8_168 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s176,plain,
( spl8_193
| ~ spl8_197 ),
inference(sat_conversion,[],[f2017]) ).
cnf(s179,plain,
( ~ spl8_28
| ~ spl8_107 ),
inference(sat_conversion,[],[f2033]) ).
cnf(s207,plain,
( ~ spl8_254
| spl8_269 ),
inference(sat_conversion,[],[f2140]) ).
cnf(s213,plain,
( ~ spl8_198
| spl8_231 ),
inference(sat_conversion,[],[f2154]) ).
cnf(s226,plain,
( ~ spl8_198
| spl8_213 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s227,plain,
spl8_167,
inference(sat_conversion,[],[f2204]) ).
cnf(s228,plain,
spl8_151,
inference(sat_conversion,[],[f2205]) ).
cnf(s286,plain,
( ~ spl8_256
| spl8_278 ),
inference(sat_conversion,[],[f2394]) ).
cnf(s308,plain,
( ~ spl8_200
| spl8_235 ),
inference(sat_conversion,[],[f2474]) ).
cnf(s377,plain,
( spl8_88
| ~ spl8_150 ),
inference(sat_conversion,[],[f2665]) ).
cnf(s381,plain,
( ~ spl8_299
| ~ spl8_303 ),
inference(sat_conversion,[],[f2680]) ).
cnf(s408,plain,
( ~ spl8_167
| ~ spl8_288 ),
inference(sat_conversion,[],[f2745]) ).
cnf(s475,plain,
( ~ spl8_160
| ~ spl8_290 ),
inference(sat_conversion,[],[f2857]) ).
cnf(s516,plain,
( ~ spl8_268
| ~ spl8_280 ),
inference(sat_conversion,[],[f2863]) ).
cnf(s521,plain,
( ~ spl8_283
| ~ spl8_287 ),
inference(sat_conversion,[],[f2864]) ).
cnf(s537,plain,
( ~ spl8_167
| ~ spl8_304 ),
inference(sat_conversion,[],[f2946]) ).
cnf(s540,plain,
( ~ spl8_296
| ~ spl8_300 ),
inference(sat_conversion,[],[f2951]) ).
cnf(s543,plain,
( ~ spl8_152
| ~ spl8_240 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s548,plain,
( ~ spl8_151
| ~ spl8_232 ),
inference(sat_conversion,[],[f3003]) ).
cnf(s552,plain,
( ~ spl8_151
| ~ spl8_228 ),
inference(sat_conversion,[],[f3011]) ).
cnf(s614,plain,
( ~ spl8_226
| ~ spl8_234 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s627,plain,
( ~ spl8_212
| ~ spl8_224 ),
inference(sat_conversion,[],[f3178]) ).
cnf(s635,plain,
( ~ spl8_151
| ~ spl8_248 ),
inference(sat_conversion,[],[f3205]) ).
cnf(s638,plain,
( ~ spl8_240
| ~ spl8_244 ),
inference(sat_conversion,[],[f3210]) ).
cnf(s644,plain,
( ~ spl8_167
| spl8_290 ),
inference(sat_conversion,[],[f3247]) ).
cnf(s709,plain,
( ~ spl8_253
| spl8_296 ),
inference(sat_conversion,[],[f3375]) ).
cnf(s720,plain,
( ~ spl8_253
| spl8_268 ),
inference(sat_conversion,[],[f3388]) ).
cnf(s721,plain,
( ~ spl8_253
| spl8_283 ),
inference(sat_conversion,[],[f3390]) ).
cnf(s722,plain,
( ~ spl8_253
| spl8_270 ),
inference(sat_conversion,[],[f3393]) ).
cnf(s724,plain,
( ~ spl8_253
| spl8_258 ),
inference(sat_conversion,[],[f3395]) ).
cnf(s725,plain,
( spl8_153
| ~ spl8_253 ),
inference(sat_conversion,[],[f3397]) ).
cnf(s745,plain,
( ~ spl8_154
| ~ spl8_273 ),
inference(sat_conversion,[],[f3540]) ).
cnf(s749,plain,
( ~ spl8_151
| ~ spl8_233 ),
inference(sat_conversion,[],[f3596]) ).
cnf(s752,plain,
( ~ spl8_144
| ~ spl8_234 ),
inference(sat_conversion,[],[f3600]) ).
cnf(s753,plain,
( ~ spl8_151
| spl8_234 ),
inference(sat_conversion,[],[f3603]) ).
cnf(s758,plain,
( ~ spl8_213
| ~ spl8_225 ),
inference(sat_conversion,[],[f3619]) ).
cnf(s767,plain,
( ~ spl8_230
| ~ spl8_234 ),
inference(sat_conversion,[],[f3624]) ).
cnf(s780,plain,
( ~ spl8_217
| ~ spl8_245 ),
inference(sat_conversion,[],[f3647]) ).
cnf(s799,plain,
( ~ spl8_199
| spl8_248 ),
inference(sat_conversion,[],[f3720]) ).
cnf(s844,plain,
( ~ spl8_151
| ~ spl8_195
| spl8_200 ),
inference(sat_conversion,[],[f3749]) ).
cnf(s898,plain,
( spl8_28
| ~ spl8_107
| ~ spl8_234
| ~ spl8_235 ),
inference(sat_conversion,[],[f3906]) ).
cnf(s903,plain,
( ~ spl8_171
| ~ spl8_193 ),
inference(sat_conversion,[],[f3917]) ).
cnf(s905,plain,
( ~ spl8_197
| spl8_240 ),
inference(sat_conversion,[],[f3931]) ).
cnf(s907,plain,
( ~ spl8_197
| spl8_212 ),
inference(sat_conversion,[],[f3935]) ).
cnf(s909,plain,
( ~ spl8_197
| spl8_227 ),
inference(sat_conversion,[],[f3939]) ).
cnf(s912,plain,
( spl8_137
| ~ spl8_197 ),
inference(sat_conversion,[],[f3946]) ).
cnf(s922,plain,
( ~ spl8_179
| ~ spl8_197
| spl8_233 ),
inference(sat_conversion,[],[f4010]) ).
cnf(s926,plain,
( ~ spl8_175
| ~ spl8_197
| spl8_217 ),
inference(sat_conversion,[],[f4039]) ).
cnf(s936,plain,
( ~ spl8_138
| ~ spl8_217 ),
inference(sat_conversion,[],[f4097]) ).
cnf(s941,plain,
( ~ spl8_197
| spl8_214 ),
inference(sat_conversion,[],[f4113]) ).
cnf(s942,plain,
( ~ spl8_214
| ~ spl8_222 ),
inference(sat_conversion,[],[f4114]) ).
cnf(s943,plain,
( ~ spl8_217
| ~ spl8_221 ),
inference(sat_conversion,[],[f4117]) ).
cnf(s944,plain,
( ~ spl8_146
| ~ spl8_223 ),
inference(sat_conversion,[],[f4118]) ).
cnf(s946,plain,
( ~ spl8_142
| ~ spl8_202 ),
inference(sat_conversion,[],[f4122]) ).
cnf(s954,plain,
( ~ spl8_242
| ~ spl8_246 ),
inference(sat_conversion,[],[f4172]) ).
cnf(s955,plain,
( ~ spl8_207
| ~ spl8_247 ),
inference(sat_conversion,[],[f4173]) ).
cnf(s956,plain,
( ~ spl8_140
| ~ spl8_241 ),
inference(sat_conversion,[],[f4175]) ).
cnf(s962,plain,
( ~ spl8_148
| ~ spl8_223 ),
inference(sat_conversion,[],[f4183]) ).
cnf(s967,plain,
( ~ spl8_197
| spl8_207 ),
inference(sat_conversion,[],[f4185]) ).
cnf(s972,plain,
( spl8_84
| ~ spl8_150
| ~ spl8_223 ),
inference(sat_conversion,[],[f4228]) ).
cnf(s985,plain,
( ~ spl8_162
| ~ spl8_279 ),
inference(sat_conversion,[],[f4317]) ).
cnf(s989,plain,
( ~ spl8_158
| ~ spl8_258 ),
inference(sat_conversion,[],[f4323]) ).
cnf(s991,plain,
( ~ spl8_273
| ~ spl8_277 ),
inference(sat_conversion,[],[f4329]) ).
cnf(s994,plain,
( ~ spl8_285
| ~ spl8_297 ),
inference(sat_conversion,[],[f4331]) ).
cnf(s1010,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_74
| ~ spl8_84
| ~ spl8_217
| ~ spl8_285 ),
inference(sat_conversion,[],[f4452]) ).
cnf(s1011,plain,
( spl8_15
| ~ spl8_150
| ~ spl8_223
| ~ spl8_229 ),
inference(sat_conversion,[],[f4453]) ).
cnf(s1013,plain,
( ~ spl8_15
| spl8_65
| ~ spl8_137
| ~ spl8_153 ),
inference(sat_conversion,[],[f4462]) ).
cnf(s1014,plain,
( ~ spl8_15
| spl8_66
| ~ spl8_84
| ~ spl8_207
| ~ spl8_258 ),
inference(sat_conversion,[],[f4471]) ).
cnf(s1016,plain,
( ~ spl8_15
| spl8_68
| ~ spl8_88
| ~ spl8_212
| ~ spl8_268 ),
inference(sat_conversion,[],[f4491]) ).
cnf(s1017,plain,
( ~ spl8_15
| spl8_69
| ~ spl8_84
| ~ spl8_227
| ~ spl8_270 ),
inference(sat_conversion,[],[f4501]) ).
cnf(s1018,plain,
( spl8_70
| ~ spl8_84
| ~ spl8_88
| ~ spl8_151
| ~ spl8_166 ),
inference(sat_conversion,[],[f4510]) ).
cnf(s1019,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_71
| ~ spl8_84
| ~ spl8_229
| ~ spl8_273 ),
inference(sat_conversion,[],[f4519]) ).
cnf(s1020,plain,
( ~ spl8_18
| spl8_72
| ~ spl8_84
| ~ spl8_88
| ~ spl8_234
| ~ spl8_279 ),
inference(sat_conversion,[],[f4529]) ).
cnf(s1021,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_73
| ~ spl8_214
| ~ spl8_283 ),
inference(sat_conversion,[],[f4539]) ).
cnf(s1022,plain,
( ~ spl8_18
| spl8_75
| ~ spl8_88
| ~ spl8_150
| ~ spl8_167 ),
inference(sat_conversion,[],[f4548]) ).
cnf(s1023,plain,
( ~ spl8_18
| spl8_76
| ~ spl8_84
| ~ spl8_88
| ~ spl8_223
| ~ spl8_290 ),
inference(sat_conversion,[],[f4557]) ).
cnf(s1024,plain,
( ~ spl8_15
| spl8_77
| ~ spl8_88
| ~ spl8_240
| ~ spl8_296 ),
inference(sat_conversion,[],[f4567]) ).
cnf(s1025,plain,
( ~ spl8_18
| spl8_78
| ~ spl8_84
| ~ spl8_88
| ~ spl8_246
| ~ spl8_299 ),
inference(sat_conversion,[],[f4577]) ).
cnf(s1026,plain,
( ~ spl8_18
| spl8_79
| ~ spl8_84
| ~ spl8_88
| ~ spl8_243
| ~ spl8_302 ),
inference(sat_conversion,[],[f4587]) ).
cnf(s1027,plain,
( ~ spl8_15
| spl8_80
| ~ spl8_88
| ~ spl8_140
| ~ spl8_156 ),
inference(sat_conversion,[],[f4596]) ).
cnf(s1028,plain,
( ~ spl8_15
| ~ spl8_18
| spl8_67
| ~ spl8_202
| ~ spl8_263 ),
inference(sat_conversion,[],[f4600]) ).
cnf(s1031,plain,
( ~ spl8_197
| spl8_202 ),
inference(sat_conversion,[],[f4604]) ).
cnf(s1036,plain,
( ~ spl8_253
| spl8_263 ),
inference(sat_conversion,[],[f4617]) ).
cnf(s1042,plain,
( ~ spl8_258
| ~ spl8_298 ),
inference(sat_conversion,[],[f4635]) ).
cnf(s1050,plain,
( ~ spl8_273
| ~ spl8_301 ),
inference(sat_conversion,[],[f4654]) ).
cnf(s1059,plain,
( ~ spl8_227
| ~ spl8_231 ),
inference(sat_conversion,[],[f4683]) ).
cnf(s1061,plain,
( ~ spl8_168
| ~ spl8_268 ),
inference(sat_conversion,[],[f4685]) ).
cnf(s1067,plain,
( ~ spl8_286
| ~ spl8_290 ),
inference(sat_conversion,[],[f4710]) ).
cnf(s1068,plain,
( ~ spl8_167
| spl8_273
| ~ spl8_290 ),
inference(sat_conversion,[],[f4720]) ).
cnf(s1069,plain,
( ~ spl8_164
| ~ spl8_279 ),
inference(sat_conversion,[],[f4724]) ).
cnf(s1093,plain,
( ~ spl8_278
| ~ spl8_290 ),
inference(sat_conversion,[],[f4757]) ).
cnf(s1134,plain,
( ~ spl8_269
| ~ spl8_273 ),
inference(sat_conversion,[],[f4780]) ).
cnf(s1176,plain,
( ~ spl8_255
| spl8_304 ),
inference(sat_conversion,[],[f4827]) ).
cnf(s1179,plain,
spl8_234,
inference(rat,[],[s753,s228]) ).
cnf(s1180,plain,
~ spl8_233,
inference(rat,[],[s749,s228]) ).
cnf(s1181,plain,
~ spl8_248,
inference(rat,[],[s635,s228]) ).
cnf(s1183,plain,
~ spl8_228,
inference(rat,[],[s552,s228]) ).
cnf(s1184,plain,
~ spl8_232,
inference(rat,[],[s548,s228]) ).
cnf(s1186,plain,
~ spl8_230,
inference(rat,[],[s767,s1179]) ).
cnf(s1187,plain,
~ spl8_144,
inference(rat,[],[s752,s1179]) ).
cnf(s1188,plain,
~ spl8_226,
inference(rat,[],[s614,s1179]) ).
cnf(s1190,plain,
~ spl8_199,
inference(rat,[],[s799,s1181]) ).
cnf(s1194,plain,
spl8_290,
inference(rat,[],[s644,s227]) ).
cnf(s1196,plain,
~ spl8_304,
inference(rat,[],[s537,s227]) ).
cnf(s1198,plain,
~ spl8_288,
inference(rat,[],[s408,s227]) ).
cnf(s1202,plain,
~ spl8_278,
inference(rat,[],[s1093,s1194]) ).
cnf(s1203,plain,
~ spl8_286,
inference(rat,[],[s1067,s1194]) ).
cnf(s1205,plain,
~ spl8_160,
inference(rat,[],[s475,s1194]) ).
cnf(s1207,plain,
spl8_273,
inference(rat,[],[s1068,s227,s1194]) ).
cnf(s1208,plain,
~ spl8_255,
inference(rat,[],[s1176,s1196]) ).
cnf(s1209,plain,
~ spl8_256,
inference(rat,[],[s286,s1202]) ).
cnf(s1210,plain,
~ spl8_269,
inference(rat,[],[s1134,s1207]) ).
cnf(s1211,plain,
~ spl8_301,
inference(rat,[],[s1050,s1207]) ).
cnf(s1213,plain,
~ spl8_277,
inference(rat,[],[s991,s1207]) ).
cnf(s1214,plain,
~ spl8_154,
inference(rat,[],[s745,s1207]) ).
cnf(s1217,plain,
~ spl8_254,
inference(rat,[],[s207,s1210]) ).
cnf(s1218,plain,
( spl8_156
| spl8_164
| spl8_168 ),
inference(rat,[],[s174,s1205]) ).
cnf(s1219,plain,
( spl8_302
| spl8_303 ),
inference(rat,[],[s173,s1196,s1211]) ).
cnf(s1220,plain,
( spl8_285
| spl8_287 ),
inference(rat,[],[s168,s1198,s1203]) ).
cnf(s1222,plain,
( spl8_279
| spl8_280 ),
inference(rat,[],[s166,s1202,s1213]) ).
cnf(s1223,plain,
( spl8_158
| spl8_162
| spl8_166 ),
inference(rat,[],[s164,s1214]) ).
cnf(s1227,plain,
spl8_253,
inference(rat,[],[s158,s1209,s1208,s1217]) ).
cnf(s1228,plain,
spl8_263,
inference(rat,[],[s1036,s1227]) ).
cnf(s1230,plain,
spl8_153,
inference(rat,[],[s725,s1227]) ).
cnf(s1231,plain,
spl8_258,
inference(rat,[],[s724,s1227]) ).
cnf(s1232,plain,
spl8_270,
inference(rat,[],[s722,s1227]) ).
cnf(s1233,plain,
spl8_283,
inference(rat,[],[s721,s1227]) ).
cnf(s1234,plain,
spl8_268,
inference(rat,[],[s720,s1227]) ).
cnf(s1235,plain,
spl8_296,
inference(rat,[],[s709,s1227]) ).
cnf(s1245,plain,
~ spl8_298,
inference(rat,[],[s1042,s1231]) ).
cnf(s1246,plain,
~ spl8_158,
inference(rat,[],[s989,s1231]) ).
cnf(s1250,plain,
~ spl8_287,
inference(rat,[],[s521,s1233]) ).
cnf(s1252,plain,
~ spl8_168,
inference(rat,[],[s1061,s1234]) ).
cnf(s1254,plain,
~ spl8_280,
inference(rat,[],[s516,s1234]) ).
cnf(s1255,plain,
~ spl8_300,
inference(rat,[],[s540,s1235]) ).
cnf(s1259,plain,
spl8_285,
inference(rat,[],[s1220,s1250]) ).
cnf(s1260,plain,
spl8_279,
inference(rat,[],[s1222,s1254]) ).
cnf(s1261,plain,
~ spl8_297,
inference(rat,[],[s994,s1259]) ).
cnf(s1262,plain,
~ spl8_164,
inference(rat,[],[s1069,s1260]) ).
cnf(s1263,plain,
~ spl8_162,
inference(rat,[],[s985,s1260]) ).
cnf(s1264,plain,
spl8_299,
inference(rat,[],[s172,s1255,s1245,s1261]) ).
cnf(s1265,plain,
spl8_156,
inference(rat,[],[s1218,s1252,s1262]) ).
cnf(s1266,plain,
spl8_166,
inference(rat,[],[s1223,s1246,s1263]) ).
cnf(s1267,plain,
~ spl8_303,
inference(rat,[],[s381,s1264]) ).
cnf(s1269,plain,
spl8_302,
inference(rat,[],[s1219,s1267]) ).
cnf(s1272,plain,
( spl8_140
| spl8_148
| spl8_152 ),
inference(rat,[],[s153,s1187]) ).
cnf(s1273,plain,
( spl8_245
| spl8_246
| spl8_247 ),
inference(rat,[],[s152,s1181]) ).
cnf(s1274,plain,
( spl8_229
| spl8_231 ),
inference(rat,[],[s147,s1184,s1186]) ).
cnf(s1275,plain,
( spl8_225
| spl8_227 ),
inference(rat,[],[s146,s1183,s1188]) ).
cnf(s1278,plain,
( spl8_197
| spl8_198
| spl8_200 ),
inference(rat,[],[s137,s1190]) ).
cnf(s1284,plain,
~ spl8_28,
inference(rat,[],[s179,s98]) ).
cnf(s1285,plain,
~ spl8_235,
inference(rat,[],[s898,s98,s1179,s1284]) ).
cnf(s1286,plain,
~ spl8_200,
inference(rat,[],[s308,s1285]) ).
cnf(s1287,plain,
~ spl8_195,
inference(rat,[],[s844,s228,s1286]) ).
cnf(s1300,plain,
~ spl8_16,
inference(rat,[],[s14,s99]) ).
cnf(s1302,plain,
~ spl8_198,
inference(rat,[],[s1275,s1059,s758,s213,s226]) ).
cnf(s1303,plain,
spl8_197,
inference(rat,[],[s1278,s1286,s1302]) ).
cnf(s1304,plain,
spl8_202,
inference(rat,[],[s1031,s1303]) ).
cnf(s1305,plain,
spl8_207,
inference(rat,[],[s967,s1303]) ).
cnf(s1306,plain,
spl8_214,
inference(rat,[],[s941,s1303]) ).
cnf(s1307,plain,
~ spl8_179,
inference(rat,[],[s922,s1180,s1303]) ).
cnf(s1308,plain,
spl8_137,
inference(rat,[],[s912,s1303]) ).
cnf(s1309,plain,
spl8_227,
inference(rat,[],[s909,s1303]) ).
cnf(s1310,plain,
spl8_212,
inference(rat,[],[s907,s1303]) ).
cnf(s1311,plain,
spl8_240,
inference(rat,[],[s905,s1303]) ).
cnf(s1312,plain,
spl8_193,
inference(rat,[],[s176,s1303]) ).
cnf(s1313,plain,
~ spl8_142,
inference(rat,[],[s946,s1304]) ).
cnf(s1315,plain,
~ spl8_247,
inference(rat,[],[s955,s1305]) ).
cnf(s1318,plain,
~ spl8_222,
inference(rat,[],[s942,s1306]) ).
cnf(s1319,plain,
~ spl8_180,
inference(rat,[],[s117,s1307]) ).
cnf(s1341,plain,
~ spl8_231,
inference(rat,[],[s1059,s1309]) ).
cnf(s1344,plain,
~ spl8_224,
inference(rat,[],[s627,s1310]) ).
cnf(s1345,plain,
~ spl8_244,
inference(rat,[],[s638,s1311]) ).
cnf(s1346,plain,
~ spl8_152,
inference(rat,[],[s543,s1311]) ).
cnf(s1347,plain,
~ spl8_171,
inference(rat,[],[s903,s1312]) ).
cnf(s1351,plain,
spl8_175,
inference(rat,[],[s135,s1287,s1347,s1319]) ).
cnf(s1353,plain,
spl8_229,
inference(rat,[],[s1274,s1341]) ).
cnf(s1357,plain,
spl8_217,
inference(rat,[],[s926,s1303,s1351]) ).
cnf(s1362,plain,
~ spl8_221,
inference(rat,[],[s943,s1357]) ).
cnf(s1363,plain,
~ spl8_138,
inference(rat,[],[s936,s1357]) ).
cnf(s1365,plain,
~ spl8_245,
inference(rat,[],[s780,s1357]) ).
cnf(s1366,plain,
spl8_223,
inference(rat,[],[s145,s1344,s1318,s1362]) ).
cnf(s1368,plain,
spl8_246,
inference(rat,[],[s1273,s1315,s1365]) ).
cnf(s1369,plain,
~ spl8_148,
inference(rat,[],[s962,s1366]) ).
cnf(s1370,plain,
~ spl8_146,
inference(rat,[],[s944,s1366]) ).
cnf(s1371,plain,
~ spl8_242,
inference(rat,[],[s954,s1368]) ).
cnf(s1372,plain,
spl8_140,
inference(rat,[],[s1272,s1346,s1369]) ).
cnf(s1374,plain,
spl8_150,
inference(rat,[],[s143,s1363,s1313,s1370]) ).
cnf(s1376,plain,
~ spl8_241,
inference(rat,[],[s956,s1372]) ).
cnf(s1379,plain,
spl8_15,
inference(rat,[],[s1011,s1353,s1366,s1374]) ).
cnf(s1380,plain,
spl8_84,
inference(rat,[],[s972,s1366,s1374]) ).
cnf(s1381,plain,
spl8_88,
inference(rat,[],[s377,s1374]) ).
cnf(s1382,plain,
spl8_243,
inference(rat,[],[s151,s1345,s1371,s1376]) ).
cnf(s1384,plain,
spl8_11,
inference(rat,[],[s12,s1379]) ).
cnf(s1385,plain,
spl8_67,
inference(rat,[],[s1028,s1228,s1304,s99,s1379]) ).
cnf(s1386,plain,
spl8_73,
inference(rat,[],[s1021,s1233,s1306,s99,s1379]) ).
cnf(s1387,plain,
spl8_65,
inference(rat,[],[s1013,s1230,s1308,s1379]) ).
cnf(s1388,plain,
spl8_70,
inference(rat,[],[s1018,s1266,s228,s1381,s1380]) ).
cnf(s1389,plain,
spl8_79,
inference(rat,[],[s1026,s1269,s1382,s1381,s99,s1380]) ).
cnf(s1390,plain,
spl8_78,
inference(rat,[],[s1025,s1264,s1368,s1381,s99,s1380]) ).
cnf(s1391,plain,
spl8_76,
inference(rat,[],[s1023,s1194,s1366,s1381,s99,s1380]) ).
cnf(s1392,plain,
spl8_72,
inference(rat,[],[s1020,s1260,s1179,s1381,s99,s1380]) ).
cnf(s1393,plain,
spl8_71,
inference(rat,[],[s1019,s1207,s1353,s1379,s99,s1380]) ).
cnf(s1394,plain,
spl8_69,
inference(rat,[],[s1017,s1232,s1309,s1379,s1380]) ).
cnf(s1395,plain,
spl8_66,
inference(rat,[],[s1014,s1231,s1305,s1379,s1380]) ).
cnf(s1396,plain,
spl8_74,
inference(rat,[],[s1010,s1259,s1357,s1379,s99,s1380]) ).
cnf(s1397,plain,
spl8_75,
inference(rat,[],[s1022,s227,s1374,s99,s1381]) ).
cnf(s1398,plain,
spl8_80,
inference(rat,[],[s1027,s1265,s1372,s1379,s1381]) ).
cnf(s1399,plain,
spl8_77,
inference(rat,[],[s1024,s1235,s1311,s1379,s1381]) ).
cnf(s1400,plain,
spl8_68,
inference(rat,[],[s1016,s1234,s1310,s1379,s1381]) ).
cnf(s1401,plain,
$false,
inference(rat,[],[s63,s1381,s1380,s1398,s1389,s1390,s1399,s1391,s1397,s1396,s1386,s1392,s1393,s1388,s1394,s1387,s1385,s1384,s1300,s1400,s1395]) ).
fof(f4828,plain,
$false,
inference(avatar_sat_refutation,[],[s1401]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n007.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:16:10 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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.34 % (2725881)Will run a generic schedule for satisfiability detection.
% 0.21/0.34 % (2725887)% WARNING: option uhcvi not known.
% 0.21/0.34 % (2725887)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4170153728:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.34 % (2725886)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3944974188_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.34 % (2725889)dis+10_1_sil=32000:sp=arity:random_seed=1316403859:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.34 % (2725888)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2242101547:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.34 % (2725890)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2291491181:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.34 % (2725891)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3114809197:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.34 % (2725892)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=894277211:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.34 % Detected minimum model sizes of [8]
% 0.21/0.34 % Detected maximum model sizes of [max]
% 0.21/0.34 % TRYING [8]
% 0.21/0.34 % (2725887) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2725881-2725887"...
% 0.21/0.34 % (2725889)Instruction limit reached!
% 0.21/0.34 % (2725889)------------------------------
% 0.21/0.34 % (2725889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.34 % (2725889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.34 % (2725889)CaDiCaL version: 2.1.3
% 0.21/0.34 % (2725889)Termination reason: Instruction limit
% 0.21/0.34 % (2725889)Termination phase: Saturation
% 0.21/0.34 % (2725889)Time elapsed: 0.052 s
% 0.21/0.34 % (2725889)Peak memory usage: 12 MB
% 0.21/0.34 % (2725889)Instructions burned: 103 (million)
% 0.21/0.34 % (2725887)...printing done.
% 0.21/0.34 % (2725890)Instruction limit reached!
% 0.21/0.34 % (2725890)------------------------------
% 0.21/0.34 % (2725890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.34 % (2725890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.34 % (2725887)Refutation found. Thanks to Tanya!
% 0.21/0.34 % SZS status Theorem for theBenchmark
% 0.21/0.34 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.35 % (2725887)------------------------------
% 0.21/0.35 % (2725887)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35 % (2725887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35 % (2725887)CaDiCaL version: 2.1.3
% 0.21/0.35 % (2725887)Termination reason: Refutation
% 0.21/0.35 % (2725887)Time elapsed: 0.065 s
% 0.21/0.35 % (2725887)Peak memory usage: 14 MB
% 0.21/0.35 % (2725887)Instructions burned: 227 (million)
% 0.21/0.35 % (2725881)Success in time 0.105 s
% 0.21/0.35 % Vampire exiting
%------------------------------------------------------------------------------