%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG015+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:07:32 AM UTC 2026
% Result : Theorem 7.94s 1.73s
% Output : Refutation 9.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 130
% Syntax : Number of formulae : 836 ( 191 unt; 106 def)
% Number of atoms : 3973 (2612 equ)
% Maximal formula atoms : 384 ( 4 avg)
% Number of connectives : 4933 (1796 ~;1966 |;1093 &)
% ( 78 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 4 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 108 ( 106 usr; 107 prp; 0-2 aty)
% Number of functors : 24 ( 24 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/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op1(op1(e10,e10),e10) = op1(e10,op1(e10,e10))
& op1(op1(e10,e10),e11) = op1(e10,op1(e10,e11))
& op1(op1(e10,e10),e12) = op1(e10,op1(e10,e12))
& op1(op1(e10,e10),e13) = op1(e10,op1(e10,e13))
& op1(op1(e10,e11),e10) = op1(e10,op1(e11,e10))
& op1(op1(e10,e11),e11) = op1(e10,op1(e11,e11))
& op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12))
& op1(op1(e10,e11),e13) = op1(e10,op1(e11,e13))
& op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10))
& op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11))
& op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12))
& op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13))
& op1(op1(e10,e13),e10) = op1(e10,op1(e13,e10))
& op1(op1(e10,e13),e11) = op1(e10,op1(e13,e11))
& op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12))
& op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13))
& op1(op1(e11,e10),e10) = op1(e11,op1(e10,e10))
& op1(op1(e11,e10),e11) = op1(e11,op1(e10,e11))
& op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12))
& op1(op1(e11,e10),e13) = op1(e11,op1(e10,e13))
& op1(op1(e11,e11),e10) = op1(e11,op1(e11,e10))
& op1(op1(e11,e11),e11) = op1(e11,op1(e11,e11))
& op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12))
& op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13))
& op1(op1(e11,e12),e10) = op1(e11,op1(e12,e10))
& op1(op1(e11,e12),e11) = op1(e11,op1(e12,e11))
& op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12))
& op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13))
& op1(op1(e11,e13),e10) = op1(e11,op1(e13,e10))
& op1(op1(e11,e13),e11) = op1(e11,op1(e13,e11))
& op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12))
& op1(op1(e11,e13),e13) = op1(e11,op1(e13,e13))
& op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10))
& op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11))
& op1(op1(e12,e10),e12) = op1(e12,op1(e10,e12))
& op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13))
& op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10))
& op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11))
& op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12))
& op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13))
& op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10))
& op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11))
& op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12))
& op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13))
& op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10))
& op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11))
& op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12))
& op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13))
& op1(op1(e13,e10),e10) = op1(e13,op1(e10,e10))
& op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11))
& op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12))
& op1(op1(e13,e10),e13) = op1(e13,op1(e10,e13))
& op1(op1(e13,e11),e10) = op1(e13,op1(e11,e10))
& op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11))
& op1(op1(e13,e11),e12) = op1(e13,op1(e11,e12))
& op1(op1(e13,e11),e13) = op1(e13,op1(e11,e13))
& op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10))
& op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11))
& op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12))
& op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13))
& op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10))
& op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11))
& op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12))
& op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
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/sandbox/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/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20))
& op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21))
& op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22))
& op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23))
& op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20))
& op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21))
& op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22))
& op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23))
& op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20))
& op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21))
& op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22))
& op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23))
& op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20))
& op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21))
& op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22))
& op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23))
& op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20))
& op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21))
& op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22))
& op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23))
& op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20))
& op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21))
& op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22))
& op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23))
& op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20))
& op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21))
& op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22))
& op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23))
& op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20))
& op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21))
& op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22))
& op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23))
& op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20))
& op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21))
& op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22))
& op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23))
& op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20))
& op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21))
& op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22))
& op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23))
& op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20))
& op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21))
& op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22))
& op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23))
& op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20))
& op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21))
& op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22))
& op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23))
& op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20))
& op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21))
& op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22))
& op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23))
& op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20))
& op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21))
& op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22))
& op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23))
& op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20))
& op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21))
& op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22))
& op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23))
& op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20))
& op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21))
& op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22))
& op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
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/sandbox/benchmark/theBenchmark.p',ax7) ).
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/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f19,axiom,
( e10 != e11
& e10 != e12
& e10 != e13
& e11 != e12
& e11 != e13
& e12 != e13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f20,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e21 != e22
& e21 != e23
& e22 != e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
fof(f22,axiom,
( ( op1(e10,e10) = e10
& op1(e11,e11) = e10
& op1(e12,e12) = e10
& op1(e13,e13) = e10 )
| ( op1(e10,e10) = e11
& op1(e11,e11) = e11
& op1(e12,e12) = e11
& op1(e13,e13) = e11 )
| ( op1(e10,e10) = e12
& op1(e11,e11) = e12
& op1(e12,e12) = e12
& op1(e13,e13) = e12 )
| ( op1(e10,e10) = e13
& op1(e11,e11) = e13
& op1(e12,e12) = e13
& op1(e13,e13) = e13 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
( ( op2(e20,e20) = e20
& op2(e21,e21) = e20
& op2(e22,e22) = e20
& op2(e23,e23) = e20 )
| ( op2(e20,e20) = e21
& op2(e21,e21) = e21
& op2(e22,e22) = e21
& op2(e23,e23) = e21 )
| ( op2(e20,e20) = e22
& op2(e21,e21) = e22
& op2(e22,e22) = e22
& op2(e23,e23) = e22 )
| ( op2(e20,e20) = e23
& op2(e21,e21) = e23
& op2(e22,e22) = e23
& op2(e23,e23) = e23 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
( e10 = op1(e13,e13)
& e11 = op1(e12,e13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( e20 = op2(e23,e23)
& e21 = op2(e22,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
( h1(e12) = e20
& h1(e13) = e21
& h1(e10) = op2(e21,e21)
& h1(e11) = op2(e20,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f27,axiom,
( h2(e12) = e20
& h2(e13) = e22
& h2(e10) = op2(e22,e22)
& h2(e11) = op2(e20,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f28,axiom,
( h3(e12) = e20
& h3(e13) = e23
& h3(e10) = op2(e23,e23)
& h3(e11) = op2(e20,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f29,axiom,
( h4(e12) = e21
& h4(e13) = e20
& h4(e10) = op2(e20,e20)
& h4(e11) = op2(e21,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f30,axiom,
( h5(e12) = e21
& h5(e13) = e22
& h5(e10) = op2(e22,e22)
& h5(e11) = op2(e21,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax30) ).
fof(f32,axiom,
( h7(e12) = e22
& h7(e13) = e20
& h7(e10) = op2(e20,e20)
& h7(e11) = op2(e22,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax32) ).
fof(f33,axiom,
( h8(e12) = e22
& h8(e13) = e21
& h8(e10) = op2(e21,e21)
& h8(e11) = op2(e22,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax33) ).
fof(f34,axiom,
( h9(e12) = e22
& h9(e13) = e23
& h9(e10) = op2(e23,e23)
& h9(e11) = op2(e22,e23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax34) ).
fof(f36,axiom,
( h11(e12) = e23
& h11(e13) = e21
& h11(e10) = op2(e21,e21)
& h11(e11) = op2(e23,e21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax36) ).
fof(f37,axiom,
( h12(e12) = e23
& h12(e13) = e22
& h12(e10) = op2(e22,e22)
& h12(e11) = op2(e23,e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax37) ).
fof(f38,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 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f39,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 ) )
| ( h5(op1(e10,e10)) = op2(h5(e10),h5(e10))
& h5(op1(e10,e11)) = op2(h5(e10),h5(e11))
& h5(op1(e10,e12)) = op2(h5(e10),h5(e12))
& h5(op1(e10,e13)) = op2(h5(e10),h5(e13))
& h5(op1(e11,e10)) = op2(h5(e11),h5(e10))
& h5(op1(e11,e11)) = op2(h5(e11),h5(e11))
& h5(op1(e11,e12)) = op2(h5(e11),h5(e12))
& h5(op1(e11,e13)) = op2(h5(e11),h5(e13))
& h5(op1(e12,e10)) = op2(h5(e12),h5(e10))
& h5(op1(e12,e11)) = op2(h5(e12),h5(e11))
& h5(op1(e12,e12)) = op2(h5(e12),h5(e12))
& h5(op1(e12,e13)) = op2(h5(e12),h5(e13))
& h5(op1(e13,e10)) = op2(h5(e13),h5(e10))
& h5(op1(e13,e11)) = op2(h5(e13),h5(e11))
& h5(op1(e13,e12)) = op2(h5(e13),h5(e12))
& h5(op1(e13,e13)) = op2(h5(e13),h5(e13))
& ( h5(e10) = e20
| h5(e11) = e20
| h5(e12) = e20
| h5(e13) = e20 )
& ( h5(e10) = e21
| h5(e11) = e21
| h5(e12) = e21
| h5(e13) = e21 )
& ( h5(e10) = e22
| h5(e11) = e22
| h5(e12) = e22
| h5(e13) = e22 )
& ( h5(e10) = e23
| h5(e11) = e23
| h5(e12) = e23
| h5(e13) = e23 ) )
| ( h6(op1(e10,e10)) = op2(h6(e10),h6(e10))
& h6(op1(e10,e11)) = op2(h6(e10),h6(e11))
& h6(op1(e10,e12)) = op2(h6(e10),h6(e12))
& h6(op1(e10,e13)) = op2(h6(e10),h6(e13))
& h6(op1(e11,e10)) = op2(h6(e11),h6(e10))
& h6(op1(e11,e11)) = op2(h6(e11),h6(e11))
& h6(op1(e11,e12)) = op2(h6(e11),h6(e12))
& h6(op1(e11,e13)) = op2(h6(e11),h6(e13))
& h6(op1(e12,e10)) = op2(h6(e12),h6(e10))
& h6(op1(e12,e11)) = op2(h6(e12),h6(e11))
& h6(op1(e12,e12)) = op2(h6(e12),h6(e12))
& h6(op1(e12,e13)) = op2(h6(e12),h6(e13))
& h6(op1(e13,e10)) = op2(h6(e13),h6(e10))
& h6(op1(e13,e11)) = op2(h6(e13),h6(e11))
& h6(op1(e13,e12)) = op2(h6(e13),h6(e12))
& h6(op1(e13,e13)) = op2(h6(e13),h6(e13))
& ( h6(e10) = e20
| h6(e11) = e20
| h6(e12) = e20
| h6(e13) = e20 )
& ( h6(e10) = e21
| h6(e11) = e21
| h6(e12) = e21
| h6(e13) = e21 )
& ( h6(e10) = e22
| h6(e11) = e22
| h6(e12) = e22
| h6(e13) = e22 )
& ( h6(e10) = e23
| h6(e11) = e23
| h6(e12) = e23
| h6(e13) = e23 ) )
| ( h7(op1(e10,e10)) = op2(h7(e10),h7(e10))
& h7(op1(e10,e11)) = op2(h7(e10),h7(e11))
& h7(op1(e10,e12)) = op2(h7(e10),h7(e12))
& h7(op1(e10,e13)) = op2(h7(e10),h7(e13))
& h7(op1(e11,e10)) = op2(h7(e11),h7(e10))
& h7(op1(e11,e11)) = op2(h7(e11),h7(e11))
& h7(op1(e11,e12)) = op2(h7(e11),h7(e12))
& h7(op1(e11,e13)) = op2(h7(e11),h7(e13))
& h7(op1(e12,e10)) = op2(h7(e12),h7(e10))
& h7(op1(e12,e11)) = op2(h7(e12),h7(e11))
& h7(op1(e12,e12)) = op2(h7(e12),h7(e12))
& h7(op1(e12,e13)) = op2(h7(e12),h7(e13))
& h7(op1(e13,e10)) = op2(h7(e13),h7(e10))
& h7(op1(e13,e11)) = op2(h7(e13),h7(e11))
& h7(op1(e13,e12)) = op2(h7(e13),h7(e12))
& h7(op1(e13,e13)) = op2(h7(e13),h7(e13))
& ( h7(e10) = e20
| h7(e11) = e20
| h7(e12) = e20
| h7(e13) = e20 )
& ( h7(e10) = e21
| h7(e11) = e21
| h7(e12) = e21
| h7(e13) = e21 )
& ( h7(e10) = e22
| h7(e11) = e22
| h7(e12) = e22
| h7(e13) = e22 )
& ( h7(e10) = e23
| h7(e11) = e23
| h7(e12) = e23
| h7(e13) = e23 ) )
| ( h8(op1(e10,e10)) = op2(h8(e10),h8(e10))
& h8(op1(e10,e11)) = op2(h8(e10),h8(e11))
& h8(op1(e10,e12)) = op2(h8(e10),h8(e12))
& h8(op1(e10,e13)) = op2(h8(e10),h8(e13))
& h8(op1(e11,e10)) = op2(h8(e11),h8(e10))
& h8(op1(e11,e11)) = op2(h8(e11),h8(e11))
& h8(op1(e11,e12)) = op2(h8(e11),h8(e12))
& h8(op1(e11,e13)) = op2(h8(e11),h8(e13))
& h8(op1(e12,e10)) = op2(h8(e12),h8(e10))
& h8(op1(e12,e11)) = op2(h8(e12),h8(e11))
& h8(op1(e12,e12)) = op2(h8(e12),h8(e12))
& h8(op1(e12,e13)) = op2(h8(e12),h8(e13))
& h8(op1(e13,e10)) = op2(h8(e13),h8(e10))
& h8(op1(e13,e11)) = op2(h8(e13),h8(e11))
& h8(op1(e13,e12)) = op2(h8(e13),h8(e12))
& h8(op1(e13,e13)) = op2(h8(e13),h8(e13))
& ( h8(e10) = e20
| h8(e11) = e20
| h8(e12) = e20
| h8(e13) = e20 )
& ( h8(e10) = e21
| h8(e11) = e21
| h8(e12) = e21
| h8(e13) = e21 )
& ( h8(e10) = e22
| h8(e11) = e22
| h8(e12) = e22
| h8(e13) = e22 )
& ( h8(e10) = e23
| h8(e11) = e23
| h8(e12) = e23
| h8(e13) = e23 ) )
| ( h9(op1(e10,e10)) = op2(h9(e10),h9(e10))
& h9(op1(e10,e11)) = op2(h9(e10),h9(e11))
& h9(op1(e10,e12)) = op2(h9(e10),h9(e12))
& h9(op1(e10,e13)) = op2(h9(e10),h9(e13))
& h9(op1(e11,e10)) = op2(h9(e11),h9(e10))
& h9(op1(e11,e11)) = op2(h9(e11),h9(e11))
& h9(op1(e11,e12)) = op2(h9(e11),h9(e12))
& h9(op1(e11,e13)) = op2(h9(e11),h9(e13))
& h9(op1(e12,e10)) = op2(h9(e12),h9(e10))
& h9(op1(e12,e11)) = op2(h9(e12),h9(e11))
& h9(op1(e12,e12)) = op2(h9(e12),h9(e12))
& h9(op1(e12,e13)) = op2(h9(e12),h9(e13))
& h9(op1(e13,e10)) = op2(h9(e13),h9(e10))
& h9(op1(e13,e11)) = op2(h9(e13),h9(e11))
& h9(op1(e13,e12)) = op2(h9(e13),h9(e12))
& h9(op1(e13,e13)) = op2(h9(e13),h9(e13))
& ( h9(e10) = e20
| h9(e11) = e20
| h9(e12) = e20
| h9(e13) = e20 )
& ( h9(e10) = e21
| h9(e11) = e21
| h9(e12) = e21
| h9(e13) = e21 )
& ( h9(e10) = e22
| h9(e11) = e22
| h9(e12) = e22
| h9(e13) = e22 )
& ( h9(e10) = e23
| h9(e11) = e23
| h9(e12) = e23
| h9(e13) = e23 ) )
| ( h10(op1(e10,e10)) = op2(h10(e10),h10(e10))
& h10(op1(e10,e11)) = op2(h10(e10),h10(e11))
& h10(op1(e10,e12)) = op2(h10(e10),h10(e12))
& h10(op1(e10,e13)) = op2(h10(e10),h10(e13))
& h10(op1(e11,e10)) = op2(h10(e11),h10(e10))
& h10(op1(e11,e11)) = op2(h10(e11),h10(e11))
& h10(op1(e11,e12)) = op2(h10(e11),h10(e12))
& h10(op1(e11,e13)) = op2(h10(e11),h10(e13))
& h10(op1(e12,e10)) = op2(h10(e12),h10(e10))
& h10(op1(e12,e11)) = op2(h10(e12),h10(e11))
& h10(op1(e12,e12)) = op2(h10(e12),h10(e12))
& h10(op1(e12,e13)) = op2(h10(e12),h10(e13))
& h10(op1(e13,e10)) = op2(h10(e13),h10(e10))
& h10(op1(e13,e11)) = op2(h10(e13),h10(e11))
& h10(op1(e13,e12)) = op2(h10(e13),h10(e12))
& h10(op1(e13,e13)) = op2(h10(e13),h10(e13))
& ( h10(e10) = e20
| h10(e11) = e20
| h10(e12) = e20
| h10(e13) = e20 )
& ( h10(e10) = e21
| h10(e11) = e21
| h10(e12) = e21
| h10(e13) = e21 )
& ( h10(e10) = e22
| h10(e11) = e22
| h10(e12) = e22
| h10(e13) = e22 )
& ( h10(e10) = e23
| h10(e11) = e23
| h10(e12) = e23
| h10(e13) = e23 ) )
| ( h11(op1(e10,e10)) = op2(h11(e10),h11(e10))
& h11(op1(e10,e11)) = op2(h11(e10),h11(e11))
& h11(op1(e10,e12)) = op2(h11(e10),h11(e12))
& h11(op1(e10,e13)) = op2(h11(e10),h11(e13))
& h11(op1(e11,e10)) = op2(h11(e11),h11(e10))
& h11(op1(e11,e11)) = op2(h11(e11),h11(e11))
& h11(op1(e11,e12)) = op2(h11(e11),h11(e12))
& h11(op1(e11,e13)) = op2(h11(e11),h11(e13))
& h11(op1(e12,e10)) = op2(h11(e12),h11(e10))
& h11(op1(e12,e11)) = op2(h11(e12),h11(e11))
& h11(op1(e12,e12)) = op2(h11(e12),h11(e12))
& h11(op1(e12,e13)) = op2(h11(e12),h11(e13))
& h11(op1(e13,e10)) = op2(h11(e13),h11(e10))
& h11(op1(e13,e11)) = op2(h11(e13),h11(e11))
& h11(op1(e13,e12)) = op2(h11(e13),h11(e12))
& h11(op1(e13,e13)) = op2(h11(e13),h11(e13))
& ( h11(e10) = e20
| h11(e11) = e20
| h11(e12) = e20
| h11(e13) = e20 )
& ( h11(e10) = e21
| h11(e11) = e21
| h11(e12) = e21
| h11(e13) = e21 )
& ( h11(e10) = e22
| h11(e11) = e22
| h11(e12) = e22
| h11(e13) = e22 )
& ( h11(e10) = e23
| h11(e11) = e23
| h11(e12) = e23
| h11(e13) = e23 ) )
| ( h12(op1(e10,e10)) = op2(h12(e10),h12(e10))
& h12(op1(e10,e11)) = op2(h12(e10),h12(e11))
& h12(op1(e10,e12)) = op2(h12(e10),h12(e12))
& h12(op1(e10,e13)) = op2(h12(e10),h12(e13))
& h12(op1(e11,e10)) = op2(h12(e11),h12(e10))
& h12(op1(e11,e11)) = op2(h12(e11),h12(e11))
& h12(op1(e11,e12)) = op2(h12(e11),h12(e12))
& h12(op1(e11,e13)) = op2(h12(e11),h12(e13))
& h12(op1(e12,e10)) = op2(h12(e12),h12(e10))
& h12(op1(e12,e11)) = op2(h12(e12),h12(e11))
& h12(op1(e12,e12)) = op2(h12(e12),h12(e12))
& h12(op1(e12,e13)) = op2(h12(e12),h12(e13))
& h12(op1(e13,e10)) = op2(h12(e13),h12(e10))
& h12(op1(e13,e11)) = op2(h12(e13),h12(e11))
& h12(op1(e13,e12)) = op2(h12(e13),h12(e12))
& h12(op1(e13,e13)) = op2(h12(e13),h12(e13))
& ( h12(e10) = e20
| h12(e11) = e20
| h12(e12) = e20
| h12(e13) = e20 )
& ( h12(e10) = e21
| h12(e11) = e21
| h12(e12) = e21
| h12(e13) = e21 )
& ( h12(e10) = e22
| h12(e11) = e22
| h12(e12) = e22
| h12(e13) = e22 )
& ( h12(e10) = e23
| h12(e11) = e23
| h12(e12) = e23
| h12(e13) = e23 ) ) ),
inference(negated_conjecture,[status(cth)],[f38]) ).
fof(f42,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) ) )
& ( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| ( e20 != h5(e10)
& e20 != h5(e11)
& e20 != h5(e12)
& e20 != h5(e13) )
| ( e21 != h5(e10)
& e21 != h5(e11)
& e21 != h5(e12)
& e21 != h5(e13) )
| ( e22 != h5(e10)
& e22 != h5(e11)
& e22 != h5(e12)
& e22 != h5(e13) )
| ( e23 != h5(e10)
& e23 != h5(e11)
& e23 != h5(e12)
& e23 != h5(e13) ) )
& ( h6(op1(e10,e10)) != op2(h6(e10),h6(e10))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| ( e20 != h6(e10)
& e20 != h6(e11)
& e20 != h6(e12)
& e20 != h6(e13) )
| ( e21 != h6(e10)
& e21 != h6(e11)
& e21 != h6(e12)
& e21 != h6(e13) )
| ( e22 != h6(e10)
& e22 != h6(e11)
& e22 != h6(e12)
& e22 != h6(e13) )
| ( e23 != h6(e10)
& e23 != h6(e11)
& e23 != h6(e12)
& e23 != h6(e13) ) )
& ( h7(op1(e10,e10)) != op2(h7(e10),h7(e10))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| ( e20 != h7(e10)
& e20 != h7(e11)
& e20 != h7(e12)
& e20 != h7(e13) )
| ( e21 != h7(e10)
& e21 != h7(e11)
& e21 != h7(e12)
& e21 != h7(e13) )
| ( e22 != h7(e10)
& e22 != h7(e11)
& e22 != h7(e12)
& e22 != h7(e13) )
| ( e23 != h7(e10)
& e23 != h7(e11)
& e23 != h7(e12)
& e23 != h7(e13) ) )
& ( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| ( e20 != h8(e10)
& e20 != h8(e11)
& e20 != h8(e12)
& e20 != h8(e13) )
| ( e21 != h8(e10)
& e21 != h8(e11)
& e21 != h8(e12)
& e21 != h8(e13) )
| ( e22 != h8(e10)
& e22 != h8(e11)
& e22 != h8(e12)
& e22 != h8(e13) )
| ( e23 != h8(e10)
& e23 != h8(e11)
& e23 != h8(e12)
& e23 != h8(e13) ) )
& ( h9(op1(e10,e10)) != op2(h9(e10),h9(e10))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| ( e20 != h9(e10)
& e20 != h9(e11)
& e20 != h9(e12)
& e20 != h9(e13) )
| ( e21 != h9(e10)
& e21 != h9(e11)
& e21 != h9(e12)
& e21 != h9(e13) )
| ( e22 != h9(e10)
& e22 != h9(e11)
& e22 != h9(e12)
& e22 != h9(e13) )
| ( e23 != h9(e10)
& e23 != h9(e11)
& e23 != h9(e12)
& e23 != h9(e13) ) )
& ( h10(op1(e10,e10)) != op2(h10(e10),h10(e10))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| ( e20 != h10(e10)
& e20 != h10(e11)
& e20 != h10(e12)
& e20 != h10(e13) )
| ( e21 != h10(e10)
& e21 != h10(e11)
& e21 != h10(e12)
& e21 != h10(e13) )
| ( e22 != h10(e10)
& e22 != h10(e11)
& e22 != h10(e12)
& e22 != h10(e13) )
| ( e23 != h10(e10)
& e23 != h10(e11)
& e23 != h10(e12)
& e23 != h10(e13) ) )
& ( h11(op1(e10,e10)) != op2(h11(e10),h11(e10))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| ( e20 != h11(e10)
& e20 != h11(e11)
& e20 != h11(e12)
& e20 != h11(e13) )
| ( e21 != h11(e10)
& e21 != h11(e11)
& e21 != h11(e12)
& e21 != h11(e13) )
| ( e22 != h11(e10)
& e22 != h11(e11)
& e22 != h11(e12)
& e22 != h11(e13) )
| ( e23 != h11(e10)
& e23 != h11(e11)
& e23 != h11(e12)
& e23 != h11(e13) ) )
& ( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| ( e20 != h12(e10)
& e20 != h12(e11)
& e20 != h12(e12)
& e20 != h12(e13) )
| ( e21 != h12(e10)
& e21 != h12(e11)
& e21 != h12(e12)
& e21 != h12(e13) )
| ( e22 != h12(e10)
& e22 != h12(e11)
& e22 != h12(e12)
& e22 != h12(e13) )
| ( e23 != h12(e10)
& e23 != h12(e11)
& e23 != h12(e12)
& e23 != h12(e13) ) ) ),
inference(ennf_transformation,[],[f39]) ).
fof(f43,definition,
( ( op1(e10,e10) = e13
& op1(e11,e11) = e13
& op1(e12,e12) = e13
& op1(e13,e13) = e13 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f44,definition,
( ( op1(e10,e10) = e12
& op1(e11,e11) = e12
& op1(e12,e12) = e12
& op1(e13,e13) = e12 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f45,plain,
( ( op1(e10,e10) = e10
& op1(e11,e11) = e10
& op1(e12,e12) = e10
& op1(e13,e13) = e10 )
| ( op1(e10,e10) = e11
& op1(e11,e11) = e11
& op1(e12,e12) = e11
& op1(e13,e13) = e11 )
| sP1
| sP0 ),
inference(definition_folding,[],[f22,f44,f43]) ).
fof(f46,definition,
( ( op2(e20,e20) = e23
& op2(e21,e21) = e23
& op2(e22,e22) = e23
& op2(e23,e23) = e23 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f47,definition,
( ( op2(e20,e20) = e22
& op2(e21,e21) = e22
& op2(e22,e22) = e22
& op2(e23,e23) = e22 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f48,plain,
( ( op2(e20,e20) = e20
& op2(e21,e21) = e20
& op2(e22,e22) = e20
& op2(e23,e23) = e20 )
| ( op2(e20,e20) = e21
& op2(e21,e21) = e21
& op2(e22,e22) = e21
& op2(e23,e23) = e21 )
| sP3
| sP2 ),
inference(definition_folding,[],[f23,f47,f46]) ).
fof(f49,definition,
( ( e23 != h12(e10)
& e23 != h12(e11)
& e23 != h12(e12)
& e23 != h12(e13) )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f50,definition,
( ( e22 != h12(e10)
& e22 != h12(e11)
& e22 != h12(e12)
& e22 != h12(e13) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f51,definition,
( ( e23 != h11(e10)
& e23 != h11(e11)
& e23 != h11(e12)
& e23 != h11(e13) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f52,definition,
( ( e22 != h11(e10)
& e22 != h11(e11)
& e22 != h11(e12)
& e22 != h11(e13) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f53,definition,
( ( e23 != h10(e10)
& e23 != h10(e11)
& e23 != h10(e12)
& e23 != h10(e13) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f54,definition,
( ( e22 != h10(e10)
& e22 != h10(e11)
& e22 != h10(e12)
& e22 != h10(e13) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( e23 != h9(e10)
& e23 != h9(e11)
& e23 != h9(e12)
& e23 != h9(e13) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( e22 != h9(e10)
& e22 != h9(e11)
& e22 != h9(e12)
& e22 != h9(e13) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f57,definition,
( ( e23 != h8(e10)
& e23 != h8(e11)
& e23 != h8(e12)
& e23 != h8(e13) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f58,definition,
( ( e22 != h8(e10)
& e22 != h8(e11)
& e22 != h8(e12)
& e22 != h8(e13) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f59,definition,
( ( e23 != h7(e10)
& e23 != h7(e11)
& e23 != h7(e12)
& e23 != h7(e13) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f60,definition,
( ( e22 != h7(e10)
& e22 != h7(e11)
& e22 != h7(e12)
& e22 != h7(e13) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f61,definition,
( ( e23 != h6(e10)
& e23 != h6(e11)
& e23 != h6(e12)
& e23 != h6(e13) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f62,definition,
( ( e22 != h6(e10)
& e22 != h6(e11)
& e22 != h6(e12)
& e22 != h6(e13) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f63,definition,
( ( e23 != h5(e10)
& e23 != h5(e11)
& e23 != h5(e12)
& e23 != h5(e13) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f64,definition,
( ( e22 != h5(e10)
& e22 != h5(e11)
& e22 != h5(e12)
& e22 != h5(e13) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f65,definition,
( ( e23 != h4(e10)
& e23 != h4(e11)
& e23 != h4(e12)
& e23 != h4(e13) )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f66,definition,
( ( e22 != h4(e10)
& e22 != h4(e11)
& e22 != h4(e12)
& e22 != h4(e13) )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f67,definition,
( ( e23 != h3(e10)
& e23 != h3(e11)
& e23 != h3(e12)
& e23 != h3(e13) )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f68,definition,
( ( e22 != h3(e10)
& e22 != h3(e11)
& e22 != h3(e12)
& e22 != h3(e13) )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f69,definition,
( ( e23 != h2(e10)
& e23 != h2(e11)
& e23 != h2(e12)
& e23 != h2(e13) )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f70,definition,
( ( e22 != h2(e10)
& e22 != h2(e11)
& e22 != h2(e12)
& e22 != h2(e13) )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f71,definition,
( ( e23 != h1(e10)
& e23 != h1(e11)
& e23 != h1(e12)
& e23 != h1(e13) )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f72,definition,
( ( e22 != h1(e10)
& e22 != h1(e11)
& e22 != h1(e12)
& e22 != h1(e13) )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f73,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) )
| sP27
| sP26 )
& ( 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) )
| sP25
| sP24 )
& ( 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) )
| sP23
| sP22 )
& ( 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) )
| sP21
| sP20 )
& ( h5(op1(e10,e10)) != op2(h5(e10),h5(e10))
| h5(op1(e10,e11)) != op2(h5(e10),h5(e11))
| h5(op1(e10,e12)) != op2(h5(e10),h5(e12))
| h5(op1(e10,e13)) != op2(h5(e10),h5(e13))
| h5(op1(e11,e10)) != op2(h5(e11),h5(e10))
| h5(op1(e11,e11)) != op2(h5(e11),h5(e11))
| h5(op1(e11,e12)) != op2(h5(e11),h5(e12))
| h5(op1(e11,e13)) != op2(h5(e11),h5(e13))
| h5(op1(e12,e10)) != op2(h5(e12),h5(e10))
| h5(op1(e12,e11)) != op2(h5(e12),h5(e11))
| h5(op1(e12,e12)) != op2(h5(e12),h5(e12))
| h5(op1(e12,e13)) != op2(h5(e12),h5(e13))
| h5(op1(e13,e10)) != op2(h5(e13),h5(e10))
| h5(op1(e13,e11)) != op2(h5(e13),h5(e11))
| h5(op1(e13,e12)) != op2(h5(e13),h5(e12))
| h5(op1(e13,e13)) != op2(h5(e13),h5(e13))
| ( e20 != h5(e10)
& e20 != h5(e11)
& e20 != h5(e12)
& e20 != h5(e13) )
| ( e21 != h5(e10)
& e21 != h5(e11)
& e21 != h5(e12)
& e21 != h5(e13) )
| sP19
| sP18 )
& ( h6(op1(e10,e10)) != op2(h6(e10),h6(e10))
| h6(op1(e10,e11)) != op2(h6(e10),h6(e11))
| h6(op1(e10,e12)) != op2(h6(e10),h6(e12))
| h6(op1(e10,e13)) != op2(h6(e10),h6(e13))
| h6(op1(e11,e10)) != op2(h6(e11),h6(e10))
| h6(op1(e11,e11)) != op2(h6(e11),h6(e11))
| h6(op1(e11,e12)) != op2(h6(e11),h6(e12))
| h6(op1(e11,e13)) != op2(h6(e11),h6(e13))
| h6(op1(e12,e10)) != op2(h6(e12),h6(e10))
| h6(op1(e12,e11)) != op2(h6(e12),h6(e11))
| h6(op1(e12,e12)) != op2(h6(e12),h6(e12))
| h6(op1(e12,e13)) != op2(h6(e12),h6(e13))
| h6(op1(e13,e10)) != op2(h6(e13),h6(e10))
| h6(op1(e13,e11)) != op2(h6(e13),h6(e11))
| h6(op1(e13,e12)) != op2(h6(e13),h6(e12))
| h6(op1(e13,e13)) != op2(h6(e13),h6(e13))
| ( e20 != h6(e10)
& e20 != h6(e11)
& e20 != h6(e12)
& e20 != h6(e13) )
| ( e21 != h6(e10)
& e21 != h6(e11)
& e21 != h6(e12)
& e21 != h6(e13) )
| sP17
| sP16 )
& ( h7(op1(e10,e10)) != op2(h7(e10),h7(e10))
| h7(op1(e10,e11)) != op2(h7(e10),h7(e11))
| h7(op1(e10,e12)) != op2(h7(e10),h7(e12))
| h7(op1(e10,e13)) != op2(h7(e10),h7(e13))
| h7(op1(e11,e10)) != op2(h7(e11),h7(e10))
| h7(op1(e11,e11)) != op2(h7(e11),h7(e11))
| h7(op1(e11,e12)) != op2(h7(e11),h7(e12))
| h7(op1(e11,e13)) != op2(h7(e11),h7(e13))
| h7(op1(e12,e10)) != op2(h7(e12),h7(e10))
| h7(op1(e12,e11)) != op2(h7(e12),h7(e11))
| h7(op1(e12,e12)) != op2(h7(e12),h7(e12))
| h7(op1(e12,e13)) != op2(h7(e12),h7(e13))
| h7(op1(e13,e10)) != op2(h7(e13),h7(e10))
| h7(op1(e13,e11)) != op2(h7(e13),h7(e11))
| h7(op1(e13,e12)) != op2(h7(e13),h7(e12))
| h7(op1(e13,e13)) != op2(h7(e13),h7(e13))
| ( e20 != h7(e10)
& e20 != h7(e11)
& e20 != h7(e12)
& e20 != h7(e13) )
| ( e21 != h7(e10)
& e21 != h7(e11)
& e21 != h7(e12)
& e21 != h7(e13) )
| sP15
| sP14 )
& ( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| ( e20 != h8(e10)
& e20 != h8(e11)
& e20 != h8(e12)
& e20 != h8(e13) )
| ( e21 != h8(e10)
& e21 != h8(e11)
& e21 != h8(e12)
& e21 != h8(e13) )
| sP13
| sP12 )
& ( h9(op1(e10,e10)) != op2(h9(e10),h9(e10))
| h9(op1(e10,e11)) != op2(h9(e10),h9(e11))
| h9(op1(e10,e12)) != op2(h9(e10),h9(e12))
| h9(op1(e10,e13)) != op2(h9(e10),h9(e13))
| h9(op1(e11,e10)) != op2(h9(e11),h9(e10))
| h9(op1(e11,e11)) != op2(h9(e11),h9(e11))
| h9(op1(e11,e12)) != op2(h9(e11),h9(e12))
| h9(op1(e11,e13)) != op2(h9(e11),h9(e13))
| h9(op1(e12,e10)) != op2(h9(e12),h9(e10))
| h9(op1(e12,e11)) != op2(h9(e12),h9(e11))
| h9(op1(e12,e12)) != op2(h9(e12),h9(e12))
| h9(op1(e12,e13)) != op2(h9(e12),h9(e13))
| h9(op1(e13,e10)) != op2(h9(e13),h9(e10))
| h9(op1(e13,e11)) != op2(h9(e13),h9(e11))
| h9(op1(e13,e12)) != op2(h9(e13),h9(e12))
| h9(op1(e13,e13)) != op2(h9(e13),h9(e13))
| ( e20 != h9(e10)
& e20 != h9(e11)
& e20 != h9(e12)
& e20 != h9(e13) )
| ( e21 != h9(e10)
& e21 != h9(e11)
& e21 != h9(e12)
& e21 != h9(e13) )
| sP11
| sP10 )
& ( h10(op1(e10,e10)) != op2(h10(e10),h10(e10))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| ( e20 != h10(e10)
& e20 != h10(e11)
& e20 != h10(e12)
& e20 != h10(e13) )
| ( e21 != h10(e10)
& e21 != h10(e11)
& e21 != h10(e12)
& e21 != h10(e13) )
| sP9
| sP8 )
& ( h11(op1(e10,e10)) != op2(h11(e10),h11(e10))
| h11(op1(e10,e11)) != op2(h11(e10),h11(e11))
| h11(op1(e10,e12)) != op2(h11(e10),h11(e12))
| h11(op1(e10,e13)) != op2(h11(e10),h11(e13))
| h11(op1(e11,e10)) != op2(h11(e11),h11(e10))
| h11(op1(e11,e11)) != op2(h11(e11),h11(e11))
| h11(op1(e11,e12)) != op2(h11(e11),h11(e12))
| h11(op1(e11,e13)) != op2(h11(e11),h11(e13))
| h11(op1(e12,e10)) != op2(h11(e12),h11(e10))
| h11(op1(e12,e11)) != op2(h11(e12),h11(e11))
| h11(op1(e12,e12)) != op2(h11(e12),h11(e12))
| h11(op1(e12,e13)) != op2(h11(e12),h11(e13))
| h11(op1(e13,e10)) != op2(h11(e13),h11(e10))
| h11(op1(e13,e11)) != op2(h11(e13),h11(e11))
| h11(op1(e13,e12)) != op2(h11(e13),h11(e12))
| h11(op1(e13,e13)) != op2(h11(e13),h11(e13))
| ( e20 != h11(e10)
& e20 != h11(e11)
& e20 != h11(e12)
& e20 != h11(e13) )
| ( e21 != h11(e10)
& e21 != h11(e11)
& e21 != h11(e12)
& e21 != h11(e13) )
| sP7
| sP6 )
& ( h12(op1(e10,e10)) != op2(h12(e10),h12(e10))
| h12(op1(e10,e11)) != op2(h12(e10),h12(e11))
| h12(op1(e10,e12)) != op2(h12(e10),h12(e12))
| h12(op1(e10,e13)) != op2(h12(e10),h12(e13))
| h12(op1(e11,e10)) != op2(h12(e11),h12(e10))
| h12(op1(e11,e11)) != op2(h12(e11),h12(e11))
| h12(op1(e11,e12)) != op2(h12(e11),h12(e12))
| h12(op1(e11,e13)) != op2(h12(e11),h12(e13))
| h12(op1(e12,e10)) != op2(h12(e12),h12(e10))
| h12(op1(e12,e11)) != op2(h12(e12),h12(e11))
| h12(op1(e12,e12)) != op2(h12(e12),h12(e12))
| h12(op1(e12,e13)) != op2(h12(e12),h12(e13))
| h12(op1(e13,e10)) != op2(h12(e13),h12(e10))
| h12(op1(e13,e11)) != op2(h12(e13),h12(e11))
| h12(op1(e13,e12)) != op2(h12(e13),h12(e12))
| h12(op1(e13,e13)) != op2(h12(e13),h12(e13))
| ( e20 != h12(e10)
& e20 != h12(e11)
& e20 != h12(e12)
& e20 != h12(e13) )
| ( e21 != h12(e10)
& e21 != h12(e11)
& e21 != h12(e12)
& e21 != h12(e13) )
| sP5
| sP4 ) ),
inference(definition_folding,[],[f42,f72,f71,f70,f69,f68,f67,f66,f65,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,f53,f52,f51,f50,f49]) ).
fof(f74,plain,
( ( op1(e10,e10) = e12
& op1(e11,e11) = e12
& op1(e12,e12) = e12
& op1(e13,e13) = e12 )
| ~ sP1 ),
inference(nnf_transformation,[],[f44]) ).
fof(f75,plain,
( ( op1(e10,e10) = e13
& op1(e11,e11) = e13
& op1(e12,e12) = e13
& op1(e13,e13) = e13 )
| ~ sP0 ),
inference(nnf_transformation,[],[f43]) ).
fof(f76,plain,
( ( op2(e20,e20) = e22
& op2(e21,e21) = e22
& op2(e22,e22) = e22
& op2(e23,e23) = e22 )
| ~ sP3 ),
inference(nnf_transformation,[],[f47]) ).
fof(f77,plain,
( ( op2(e20,e20) = e23
& op2(e21,e21) = e23
& op2(e22,e22) = e23
& op2(e23,e23) = e23 )
| ~ sP2 ),
inference(nnf_transformation,[],[f46]) ).
fof(f92,plain,
( ( e22 != h8(e10)
& e22 != h8(e11)
& e22 != h8(e12)
& e22 != h8(e13) )
| ~ sP13 ),
inference(nnf_transformation,[],[f58]) ).
fof(f93,plain,
( ( e23 != h8(e10)
& e23 != h8(e11)
& e23 != h8(e12)
& e23 != h8(e13) )
| ~ sP12 ),
inference(nnf_transformation,[],[f57]) ).
fof(f103,plain,
( e10 = op1(e13,e12)
| e11 = op1(e13,e12)
| e12 = op1(e13,e12)
| e13 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f115,plain,
( e10 = op1(e10,e12)
| e11 = op1(e10,e12)
| e12 = op1(e10,e12)
| e13 = op1(e10,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f118,plain,
op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f119,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f128,plain,
op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f134,plain,
op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f135,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f182,plain,
( e10 = unit1
| e11 = unit1
| e12 = unit1
| e13 = unit1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f183,plain,
e13 = op1(e13,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f184,plain,
e13 = op1(unit1,e13),
inference(cnf_transformation,[],[f3]) ).
fof(f185,plain,
e12 = op1(e12,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f186,plain,
e12 = op1(unit1,e12),
inference(cnf_transformation,[],[f3]) ).
fof(f187,plain,
e11 = op1(e11,unit1),
inference(cnf_transformation,[],[f3]) ).
fof(f188,plain,
e11 = op1(unit1,e11),
inference(cnf_transformation,[],[f3]) ).
fof(f209,plain,
( e20 = op2(e22,e21)
| e21 = op2(e22,e21)
| e22 = op2(e22,e21)
| e23 = op2(e22,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f210,plain,
( e20 = op2(e22,e20)
| e21 = op2(e22,e20)
| e22 = op2(e22,e20)
| e23 = op2(e22,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
( e20 = op2(e21,e22)
| e21 = op2(e21,e22)
| e22 = op2(e21,e22)
| e23 = op2(e21,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f214,plain,
( e20 = op2(e21,e20)
| e21 = op2(e21,e20)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f215,plain,
( e20 = op2(e20,e23)
| e21 = op2(e20,e23)
| e22 = op2(e20,e23)
| e23 = op2(e20,e23) ),
inference(cnf_transformation,[],[f5]) ).
fof(f235,plain,
op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f239,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f240,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f242,plain,
op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f244,plain,
op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f245,plain,
op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f246,plain,
op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f247,plain,
op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f255,plain,
op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f260,plain,
op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f261,plain,
op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f271,plain,
op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f273,plain,
op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f283,plain,
( e20 = unit2
| e21 = unit2
| e22 = unit2
| e23 = unit2 ),
inference(cnf_transformation,[],[f7]) ).
fof(f284,plain,
e23 = op2(e23,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f285,plain,
e23 = op2(unit2,e23),
inference(cnf_transformation,[],[f7]) ).
fof(f286,plain,
e22 = op2(e22,unit2),
inference(cnf_transformation,[],[f7]) ).
fof(f287,plain,
e22 = op2(unit2,e22),
inference(cnf_transformation,[],[f7]) ).
fof(f289,plain,
e21 = op2(unit2,e21),
inference(cnf_transformation,[],[f7]) ).
fof(f291,plain,
e20 = op2(unit2,e20),
inference(cnf_transformation,[],[f7]) ).
fof(f358,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f390,plain,
op1(e11,e12) != op1(e12,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f454,plain,
e12 != e13,
inference(cnf_transformation,[],[f19]) ).
fof(f456,plain,
e11 != e12,
inference(cnf_transformation,[],[f19]) ).
fof(f457,plain,
e10 != e13,
inference(cnf_transformation,[],[f19]) ).
fof(f458,plain,
e10 != e12,
inference(cnf_transformation,[],[f19]) ).
fof(f459,plain,
e10 != e11,
inference(cnf_transformation,[],[f19]) ).
fof(f460,plain,
e22 != e23,
inference(cnf_transformation,[],[f20]) ).
fof(f461,plain,
e21 != e23,
inference(cnf_transformation,[],[f20]) ).
fof(f462,plain,
e21 != e22,
inference(cnf_transformation,[],[f20]) ).
fof(f463,plain,
e20 != e23,
inference(cnf_transformation,[],[f20]) ).
fof(f464,plain,
e20 != e22,
inference(cnf_transformation,[],[f20]) ).
fof(f465,plain,
e20 != e21,
inference(cnf_transformation,[],[f20]) ).
fof(f482,plain,
( e12 = op1(e13,e13)
| ~ sP1 ),
inference(cnf_transformation,[],[f74]) ).
fof(f486,plain,
( e13 = op1(e13,e13)
| ~ sP0 ),
inference(cnf_transformation,[],[f75]) ).
fof(f494,plain,
( e10 = op1(e12,e12)
| e11 = op1(e13,e13)
| sP1
| sP0 ),
inference(cnf_transformation,[],[f45]) ).
fof(f498,plain,
( e10 = op1(e11,e11)
| e11 = op1(e13,e13)
| sP1
| sP0 ),
inference(cnf_transformation,[],[f45]) ).
fof(f502,plain,
( e10 = op1(e10,e10)
| e11 = op1(e13,e13)
| sP1
| sP0 ),
inference(cnf_transformation,[],[f45]) ).
fof(f506,plain,
( e22 = op2(e23,e23)
| ~ sP3 ),
inference(cnf_transformation,[],[f76]) ).
fof(f510,plain,
( e23 = op2(e23,e23)
| ~ sP2 ),
inference(cnf_transformation,[],[f77]) ).
fof(f518,plain,
( e20 = op2(e22,e22)
| e21 = op2(e23,e23)
| sP3
| sP2 ),
inference(cnf_transformation,[],[f48]) ).
fof(f522,plain,
( e20 = op2(e21,e21)
| e21 = op2(e23,e23)
| sP3
| sP2 ),
inference(cnf_transformation,[],[f48]) ).
fof(f530,plain,
e11 = op1(e12,e13),
inference(cnf_transformation,[],[f24]) ).
fof(f531,plain,
e10 = op1(e13,e13),
inference(cnf_transformation,[],[f24]) ).
fof(f532,plain,
e21 = op2(e22,e23),
inference(cnf_transformation,[],[f25]) ).
fof(f533,plain,
e20 = op2(e23,e23),
inference(cnf_transformation,[],[f25]) ).
fof(f535,plain,
op2(e21,e21) = h1(e10),
inference(cnf_transformation,[],[f26]) ).
fof(f538,plain,
op2(e20,e22) = h2(e11),
inference(cnf_transformation,[],[f27]) ).
fof(f542,plain,
op2(e20,e23) = h3(e11),
inference(cnf_transformation,[],[f28]) ).
fof(f546,plain,
op2(e21,e20) = h4(e11),
inference(cnf_transformation,[],[f29]) ).
fof(f550,plain,
op2(e21,e22) = h5(e11),
inference(cnf_transformation,[],[f30]) ).
fof(f558,plain,
op2(e22,e20) = h7(e11),
inference(cnf_transformation,[],[f32]) ).
fof(f562,plain,
op2(e22,e21) = h8(e11),
inference(cnf_transformation,[],[f33]) ).
fof(f563,plain,
op2(e21,e21) = h8(e10),
inference(cnf_transformation,[],[f33]) ).
fof(f564,plain,
e21 = h8(e13),
inference(cnf_transformation,[],[f33]) ).
fof(f565,plain,
e22 = h8(e12),
inference(cnf_transformation,[],[f33]) ).
fof(f566,plain,
op2(e22,e23) = h9(e11),
inference(cnf_transformation,[],[f34]) ).
fof(f567,plain,
op2(e23,e23) = h9(e10),
inference(cnf_transformation,[],[f34]) ).
fof(f575,plain,
op2(e21,e21) = h11(e10),
inference(cnf_transformation,[],[f36]) ).
fof(f579,plain,
op2(e22,e22) = h12(e10),
inference(cnf_transformation,[],[f37]) ).
fof(f639,plain,
( e22 != h8(e12)
| ~ sP13 ),
inference(cnf_transformation,[],[f92]) ).
fof(f644,plain,
( e23 != h8(e11)
| ~ sP12 ),
inference(cnf_transformation,[],[f93]) ).
fof(f754,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| e20 != h8(e10)
| e21 != h8(e13)
| sP13
| sP12 ),
inference(cnf_transformation,[],[f73]) ).
fof(f958,definition,
( spl28_26
<=> e20 = h12(e10) ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
fof(f1052,definition,
( spl28_52
<=> e20 = h11(e10) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
fof(f1222,definition,
( spl28_101
<=> e21 = h9(e10) ),
introduced(definition,[new_symbols(definition,[spl28_101])],[avatar_definition]) ).
fof(f1247,definition,
( spl28_105
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl28_105])],[avatar_definition]) ).
fof(f1250,definition,
( spl28_106
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl28_106])],[avatar_definition]) ).
fof(f1253,definition,
( spl28_107
<=> e21 = h8(e13) ),
introduced(definition,[new_symbols(definition,[spl28_107])],[avatar_definition]) ).
fof(f1254,plain,
( e21 != h8(e13)
| spl28_107 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1259,definition,
( spl28_109
<=> h8(op1(e13,e13)) = op2(h8(e13),h8(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_109])],[avatar_definition]) ).
fof(f1260,plain,
( h8(op1(e13,e13)) != op2(h8(e13),h8(e13))
| spl28_109 ),
inference(avatar_component_clause,[],[f1259]) ).
fof(f1262,definition,
( spl28_110
<=> h8(op1(e13,e12)) = op2(h8(e13),h8(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_110])],[avatar_definition]) ).
fof(f1263,plain,
( h8(op1(e13,e12)) != op2(h8(e13),h8(e12))
| spl28_110 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1265,definition,
( spl28_111
<=> h8(op1(e13,e11)) = op2(h8(e13),h8(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_111])],[avatar_definition]) ).
fof(f1266,plain,
( h8(op1(e13,e11)) != op2(h8(e13),h8(e11))
| spl28_111 ),
inference(avatar_component_clause,[],[f1265]) ).
fof(f1268,definition,
( spl28_112
<=> h8(op1(e13,e10)) = op2(h8(e13),h8(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_112])],[avatar_definition]) ).
fof(f1269,plain,
( h8(op1(e13,e10)) != op2(h8(e13),h8(e10))
| spl28_112 ),
inference(avatar_component_clause,[],[f1268]) ).
fof(f1271,definition,
( spl28_113
<=> h8(op1(e12,e13)) = op2(h8(e12),h8(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_113])],[avatar_definition]) ).
fof(f1272,plain,
( h8(op1(e12,e13)) != op2(h8(e12),h8(e13))
| spl28_113 ),
inference(avatar_component_clause,[],[f1271]) ).
fof(f1274,definition,
( spl28_114
<=> h8(op1(e12,e12)) = op2(h8(e12),h8(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_114])],[avatar_definition]) ).
fof(f1275,plain,
( h8(op1(e12,e12)) != op2(h8(e12),h8(e12))
| spl28_114 ),
inference(avatar_component_clause,[],[f1274]) ).
fof(f1277,definition,
( spl28_115
<=> h8(op1(e12,e11)) = op2(h8(e12),h8(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_115])],[avatar_definition]) ).
fof(f1278,plain,
( h8(op1(e12,e11)) != op2(h8(e12),h8(e11))
| spl28_115 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1280,definition,
( spl28_116
<=> h8(op1(e12,e10)) = op2(h8(e12),h8(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_116])],[avatar_definition]) ).
fof(f1281,plain,
( h8(op1(e12,e10)) != op2(h8(e12),h8(e10))
| spl28_116 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1283,definition,
( spl28_117
<=> h8(op1(e11,e13)) = op2(h8(e11),h8(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_117])],[avatar_definition]) ).
fof(f1284,plain,
( h8(op1(e11,e13)) != op2(h8(e11),h8(e13))
| spl28_117 ),
inference(avatar_component_clause,[],[f1283]) ).
fof(f1286,definition,
( spl28_118
<=> h8(op1(e11,e12)) = op2(h8(e11),h8(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_118])],[avatar_definition]) ).
fof(f1287,plain,
( h8(op1(e11,e12)) != op2(h8(e11),h8(e12))
| spl28_118 ),
inference(avatar_component_clause,[],[f1286]) ).
fof(f1289,definition,
( spl28_119
<=> h8(op1(e11,e11)) = op2(h8(e11),h8(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_119])],[avatar_definition]) ).
fof(f1290,plain,
( h8(op1(e11,e11)) != op2(h8(e11),h8(e11))
| spl28_119 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1292,definition,
( spl28_120
<=> h8(op1(e11,e10)) = op2(h8(e11),h8(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_120])],[avatar_definition]) ).
fof(f1293,plain,
( h8(op1(e11,e10)) != op2(h8(e11),h8(e10))
| spl28_120 ),
inference(avatar_component_clause,[],[f1292]) ).
fof(f1295,definition,
( spl28_121
<=> h8(op1(e10,e13)) = op2(h8(e10),h8(e13)) ),
introduced(definition,[new_symbols(definition,[spl28_121])],[avatar_definition]) ).
fof(f1296,plain,
( h8(op1(e10,e13)) != op2(h8(e10),h8(e13))
| spl28_121 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1298,definition,
( spl28_122
<=> h8(op1(e10,e12)) = op2(h8(e10),h8(e12)) ),
introduced(definition,[new_symbols(definition,[spl28_122])],[avatar_definition]) ).
fof(f1299,plain,
( h8(op1(e10,e12)) != op2(h8(e10),h8(e12))
| spl28_122 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1301,definition,
( spl28_123
<=> h8(op1(e10,e11)) = op2(h8(e10),h8(e11)) ),
introduced(definition,[new_symbols(definition,[spl28_123])],[avatar_definition]) ).
fof(f1302,plain,
( h8(op1(e10,e11)) != op2(h8(e10),h8(e11))
| spl28_123 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1304,definition,
( spl28_124
<=> h8(op1(e10,e10)) = op2(h8(e10),h8(e10)) ),
introduced(definition,[new_symbols(definition,[spl28_124])],[avatar_definition]) ).
fof(f1305,plain,
( h8(op1(e10,e10)) != op2(h8(e10),h8(e10))
| spl28_124 ),
inference(avatar_component_clause,[],[f1304]) ).
fof(f1312,definition,
( spl28_126
<=> e21 = h8(e11) ),
introduced(definition,[new_symbols(definition,[spl28_126])],[avatar_definition]) ).
fof(f1313,plain,
( e21 != h8(e11)
| spl28_126 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f1327,definition,
( spl28_129
<=> e20 = h8(e11) ),
introduced(definition,[new_symbols(definition,[spl28_129])],[avatar_definition]) ).
fof(f1334,definition,
( spl28_130
<=> e20 = h8(e10) ),
introduced(definition,[new_symbols(definition,[spl28_130])],[avatar_definition]) ).
fof(f1335,plain,
( e20 != h8(e10)
| spl28_130 ),
inference(avatar_component_clause,[],[f1334]) ).
fof(f1336,plain,
( spl28_105
| spl28_106
| ~ spl28_107
| ~ spl28_130
| ~ spl28_109
| ~ spl28_110
| ~ spl28_111
| ~ spl28_112
| ~ spl28_113
| ~ spl28_114
| ~ spl28_115
| ~ spl28_116
| ~ spl28_117
| ~ spl28_118
| ~ spl28_119
| ~ spl28_120
| ~ spl28_121
| ~ spl28_122
| ~ spl28_123
| ~ spl28_124 ),
inference(avatar_split_clause,[],[f754,f1304,f1301,f1298,f1295,f1292,f1289,f1286,f1283,f1280,f1277,f1274,f1271,f1268,f1265,f1262,f1259,f1334,f1253,f1250,f1247]) ).
fof(f1406,definition,
( spl28_152
<=> e21 = h7(e11) ),
introduced(definition,[new_symbols(definition,[spl28_152])],[avatar_definition]) ).
fof(f1421,definition,
( spl28_155
<=> e20 = h7(e11) ),
introduced(definition,[new_symbols(definition,[spl28_155])],[avatar_definition]) ).
fof(f1594,definition,
( spl28_204
<=> e21 = h5(e11) ),
introduced(definition,[new_symbols(definition,[spl28_204])],[avatar_definition]) ).
fof(f1609,definition,
( spl28_207
<=> e20 = h5(e11) ),
introduced(definition,[new_symbols(definition,[spl28_207])],[avatar_definition]) ).
fof(f1688,definition,
( spl28_230
<=> e21 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl28_230])],[avatar_definition]) ).
fof(f1703,definition,
( spl28_233
<=> e20 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl28_233])],[avatar_definition]) ).
fof(f1782,definition,
( spl28_256
<=> e21 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl28_256])],[avatar_definition]) ).
fof(f1797,definition,
( spl28_259
<=> e20 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl28_259])],[avatar_definition]) ).
fof(f1891,definition,
( spl28_285
<=> e20 = h2(e11) ),
introduced(definition,[new_symbols(definition,[spl28_285])],[avatar_definition]) ).
fof(f1892,plain,
( e20 != h2(e11)
| spl28_285 ),
inference(avatar_component_clause,[],[f1891]) ).
fof(f2114,definition,
( spl28_340
<=> e23 = h9(e10) ),
introduced(definition,[new_symbols(definition,[spl28_340])],[avatar_definition]) ).
fof(f2131,definition,
( spl28_344
<=> e22 = h9(e10) ),
introduced(definition,[new_symbols(definition,[spl28_344])],[avatar_definition]) ).
fof(f2144,definition,
( spl28_347
<=> e23 = h8(e11) ),
introduced(definition,[new_symbols(definition,[spl28_347])],[avatar_definition]) ).
fof(f2146,plain,
( ~ spl28_105
| ~ spl28_347 ),
inference(avatar_split_clause,[],[f644,f2144,f1247]) ).
fof(f2157,definition,
( spl28_350
<=> e22 = h8(e12) ),
introduced(definition,[new_symbols(definition,[spl28_350])],[avatar_definition]) ).
fof(f2158,plain,
( e22 != h8(e12)
| spl28_350 ),
inference(avatar_component_clause,[],[f2157]) ).
fof(f2159,plain,
( ~ spl28_106
| ~ spl28_350 ),
inference(avatar_split_clause,[],[f639,f2157,f1250]) ).
fof(f2161,definition,
( spl28_351
<=> e22 = h8(e11) ),
introduced(definition,[new_symbols(definition,[spl28_351])],[avatar_definition]) ).
fof(f2178,definition,
( spl28_355
<=> e23 = h7(e11) ),
introduced(definition,[new_symbols(definition,[spl28_355])],[avatar_definition]) ).
fof(f2195,definition,
( spl28_359
<=> e22 = h7(e11) ),
introduced(definition,[new_symbols(definition,[spl28_359])],[avatar_definition]) ).
fof(f2246,definition,
( spl28_371
<=> e23 = h5(e11) ),
introduced(definition,[new_symbols(definition,[spl28_371])],[avatar_definition]) ).
fof(f2263,definition,
( spl28_375
<=> e22 = h5(e11) ),
introduced(definition,[new_symbols(definition,[spl28_375])],[avatar_definition]) ).
fof(f2280,definition,
( spl28_379
<=> e23 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl28_379])],[avatar_definition]) ).
fof(f2297,definition,
( spl28_383
<=> e22 = h4(e11) ),
introduced(definition,[new_symbols(definition,[spl28_383])],[avatar_definition]) ).
fof(f2314,definition,
( spl28_387
<=> e23 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl28_387])],[avatar_definition]) ).
fof(f2331,definition,
( spl28_391
<=> e22 = h3(e11) ),
introduced(definition,[new_symbols(definition,[spl28_391])],[avatar_definition]) ).
fof(f2406,plain,
( e20 = h12(e10)
| e21 = op2(e23,e23)
| sP3
| sP2 ),
inference(forward_demodulation,[],[f518,f579]) ).
fof(f2410,plain,
( e20 = h11(e10)
| e21 = op2(e23,e23)
| sP3
| sP2 ),
inference(forward_demodulation,[],[f522,f575]) ).
fof(f2418,plain,
( e23 = h9(e10)
| ~ sP2 ),
inference(forward_demodulation,[],[f510,f567]) ).
fof(f2422,plain,
( e22 = h9(e10)
| ~ sP3 ),
inference(forward_demodulation,[],[f506,f567]) ).
fof(f2426,plain,
( e10 = e11
| e10 = op1(e12,e12)
| sP1
| sP0 ),
inference(forward_demodulation,[],[f494,f531]) ).
fof(f2428,definition,
( spl28_409
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl28_409])],[avatar_definition]) ).
fof(f2431,definition,
( spl28_410
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl28_410])],[avatar_definition]) ).
fof(f2437,definition,
( spl28_412
<=> e10 = op1(e12,e12) ),
introduced(definition,[new_symbols(definition,[spl28_412])],[avatar_definition]) ).
fof(f2438,plain,
( e10 = op1(e12,e12)
| ~ spl28_412 ),
inference(avatar_component_clause,[],[f2437]) ).
fof(f2448,plain,
( e10 = e11
| e10 = op1(e11,e11)
| sP1
| sP0 ),
inference(forward_demodulation,[],[f498,f531]) ).
fof(f2450,definition,
( spl28_415
<=> e10 = op1(e11,e11) ),
introduced(definition,[new_symbols(definition,[spl28_415])],[avatar_definition]) ).
fof(f2451,plain,
( e10 = op1(e11,e11)
| ~ spl28_415 ),
inference(avatar_component_clause,[],[f2450]) ).
fof(f2455,plain,
( e10 = e11
| e10 = op1(e10,e10)
| sP1
| sP0 ),
inference(forward_demodulation,[],[f502,f531]) ).
fof(f2457,definition,
( spl28_416
<=> e10 = op1(e10,e10) ),
introduced(definition,[new_symbols(definition,[spl28_416])],[avatar_definition]) ).
fof(f2458,plain,
( e10 = op1(e10,e10)
| ~ spl28_416 ),
inference(avatar_component_clause,[],[f2457]) ).
fof(f2462,plain,
( e10 = e13
| ~ sP0 ),
inference(forward_demodulation,[],[f486,f531]) ).
fof(f2476,plain,
( e10 = e12
| ~ sP1 ),
inference(forward_demodulation,[],[f482,f531]) ).
fof(f2538,plain,
e10 != op1(e13,e12),
inference(forward_demodulation,[],[f358,f531]) ).
fof(f2686,definition,
( spl28_451
<=> e23 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_451])],[avatar_definition]) ).
fof(f2687,plain,
( e23 = unit2
| ~ spl28_451 ),
inference(avatar_component_clause,[],[f2686]) ).
fof(f2689,definition,
( spl28_452
<=> e22 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_452])],[avatar_definition]) ).
fof(f2690,plain,
( e22 = unit2
| ~ spl28_452 ),
inference(avatar_component_clause,[],[f2689]) ).
fof(f2692,definition,
( spl28_453
<=> e21 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_453])],[avatar_definition]) ).
fof(f2693,plain,
( e21 = unit2
| ~ spl28_453 ),
inference(avatar_component_clause,[],[f2692]) ).
fof(f2695,definition,
( spl28_454
<=> e20 = unit2 ),
introduced(definition,[new_symbols(definition,[spl28_454])],[avatar_definition]) ).
fof(f2696,plain,
( e20 = unit2
| ~ spl28_454 ),
inference(avatar_component_clause,[],[f2695]) ).
fof(f2697,plain,
( spl28_451
| spl28_452
| spl28_453
| spl28_454 ),
inference(avatar_split_clause,[],[f283,f2695,f2692,f2689,f2686]) ).
fof(f2714,plain,
op2(op2(e22,e23),e23) = op2(e22,h9(e10)),
inference(forward_demodulation,[],[f235,f567]) ).
fof(f2718,plain,
op2(op2(e22,e22),e23) = op2(e22,h9(e11)),
inference(forward_demodulation,[],[f239,f566]) ).
fof(f2719,plain,
op2(h12(e10),e22) = op2(e22,h12(e10)),
inference(forward_demodulation,[],[f240,f579]) ).
fof(f2721,plain,
op2(op2(e22,e22),e20) = op2(e22,h7(e11)),
inference(forward_demodulation,[],[f242,f558]) ).
fof(f2723,plain,
op2(op2(e22,e21),e22) = op2(e22,h5(e11)),
inference(forward_demodulation,[],[f244,f550]) ).
fof(f2724,plain,
op2(op2(e22,e21),e21) = op2(e22,h11(e10)),
inference(forward_demodulation,[],[f245,f575]) ).
fof(f2725,plain,
op2(op2(e22,e21),e20) = op2(e22,h4(e11)),
inference(forward_demodulation,[],[f246,f546]) ).
fof(f2726,plain,
op2(op2(e22,e20),e23) = op2(e22,h3(e11)),
inference(forward_demodulation,[],[f247,f542]) ).
fof(f2734,plain,
op2(op2(e21,e22),e23) = op2(e21,h9(e11)),
inference(forward_demodulation,[],[f255,f566]) ).
fof(f2739,plain,
op2(op2(e21,e21),e22) = op2(e21,h5(e11)),
inference(forward_demodulation,[],[f260,f550]) ).
fof(f2740,plain,
op2(h11(e10),e21) = op2(e21,h11(e10)),
inference(forward_demodulation,[],[f261,f575]) ).
fof(f2750,plain,
op2(op2(e20,e22),e23) = op2(e20,h9(e11)),
inference(forward_demodulation,[],[f271,f566]) ).
fof(f2752,plain,
op2(op2(e20,e22),e21) = op2(e20,h8(e11)),
inference(forward_demodulation,[],[f273,f562]) ).
fof(f2766,plain,
( e20 = h8(e11)
| e21 = op2(e22,e21)
| e22 = op2(e22,e21)
| e23 = op2(e22,e21) ),
inference(forward_demodulation,[],[f209,f562]) ).
fof(f2767,plain,
( e20 = h7(e11)
| e21 = op2(e22,e20)
| e22 = op2(e22,e20)
| e23 = op2(e22,e20) ),
inference(forward_demodulation,[],[f210,f558]) ).
fof(f2769,plain,
( e20 = h5(e11)
| e21 = op2(e21,e22)
| e22 = op2(e21,e22)
| e23 = op2(e21,e22) ),
inference(forward_demodulation,[],[f212,f550]) ).
fof(f2771,plain,
( e20 = h4(e11)
| e21 = op2(e21,e20)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(forward_demodulation,[],[f214,f546]) ).
fof(f2772,plain,
( e20 = h3(e11)
| e21 = op2(e20,e23)
| e22 = op2(e20,e23)
| e23 = op2(e20,e23) ),
inference(forward_demodulation,[],[f215,f542]) ).
fof(f2793,definition,
( spl28_459
<=> e13 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_459])],[avatar_definition]) ).
fof(f2794,plain,
( e13 = unit1
| ~ spl28_459 ),
inference(avatar_component_clause,[],[f2793]) ).
fof(f2796,definition,
( spl28_460
<=> e12 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_460])],[avatar_definition]) ).
fof(f2797,plain,
( e12 = unit1
| ~ spl28_460 ),
inference(avatar_component_clause,[],[f2796]) ).
fof(f2799,definition,
( spl28_461
<=> e11 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_461])],[avatar_definition]) ).
fof(f2800,plain,
( e11 = unit1
| ~ spl28_461 ),
inference(avatar_component_clause,[],[f2799]) ).
fof(f2802,definition,
( spl28_462
<=> e10 = unit1 ),
introduced(definition,[new_symbols(definition,[spl28_462])],[avatar_definition]) ).
fof(f2803,plain,
( e10 = unit1
| ~ spl28_462 ),
inference(avatar_component_clause,[],[f2802]) ).
fof(f2804,plain,
( spl28_459
| spl28_460
| spl28_461
| spl28_462 ),
inference(avatar_split_clause,[],[f182,f2802,f2799,f2796,f2793]) ).
fof(f2805,plain,
op1(e10,e13) = op1(e13,e10),
inference(forward_demodulation,[],[f118,f531]) ).
fof(f2806,plain,
op1(e10,e12) = op1(e13,op1(e13,e12)),
inference(forward_demodulation,[],[f119,f531]) ).
fof(f2810,plain,
op1(e12,e10) = op1(op1(e12,e13),e13),
inference(forward_demodulation,[],[f134,f531]) ).
fof(f2811,plain,
op1(e11,e12) = op1(e12,op1(e13,e12)),
inference(forward_demodulation,[],[f135,f530]) ).
fof(f2820,definition,
( spl28_463
<=> e13 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_463])],[avatar_definition]) ).
fof(f2821,plain,
( e13 = op1(e13,e12)
| ~ spl28_463 ),
inference(avatar_component_clause,[],[f2820]) ).
fof(f2823,definition,
( spl28_464
<=> e12 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_464])],[avatar_definition]) ).
fof(f2824,plain,
( e12 = op1(e13,e12)
| ~ spl28_464 ),
inference(avatar_component_clause,[],[f2823]) ).
fof(f2826,definition,
( spl28_465
<=> e11 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_465])],[avatar_definition]) ).
fof(f2827,plain,
( e11 = op1(e13,e12)
| ~ spl28_465 ),
inference(avatar_component_clause,[],[f2826]) ).
fof(f2829,definition,
( spl28_466
<=> e10 = op1(e13,e12) ),
introduced(definition,[new_symbols(definition,[spl28_466])],[avatar_definition]) ).
fof(f2830,plain,
( e10 = op1(e13,e12)
| ~ spl28_466 ),
inference(avatar_component_clause,[],[f2829]) ).
fof(f2831,plain,
( spl28_463
| spl28_464
| spl28_465
| spl28_466 ),
inference(avatar_split_clause,[],[f103,f2829,f2826,f2823,f2820]) ).
fof(f2836,definition,
( spl28_468
<=> e12 = op1(e13,e11) ),
introduced(definition,[new_symbols(definition,[spl28_468])],[avatar_definition]) ).
fof(f2837,plain,
( e12 = op1(e13,e11)
| ~ spl28_468 ),
inference(avatar_component_clause,[],[f2836]) ).
fof(f2860,definition,
( spl28_475
<=> e13 = op1(e12,e11) ),
introduced(definition,[new_symbols(definition,[spl28_475])],[avatar_definition]) ).
fof(f2861,plain,
( e13 = op1(e12,e11)
| ~ spl28_475 ),
inference(avatar_component_clause,[],[f2860]) ).
fof(f2876,definition,
( spl28_480
<=> e12 = op1(e12,e10) ),
introduced(definition,[new_symbols(definition,[spl28_480])],[avatar_definition]) ).
fof(f2877,plain,
( e12 = op1(e12,e10)
| ~ spl28_480 ),
inference(avatar_component_clause,[],[f2876]) ).
fof(f2889,definition,
( spl28_484
<=> e12 = op1(e11,e13) ),
introduced(definition,[new_symbols(definition,[spl28_484])],[avatar_definition]) ).
fof(f2890,plain,
( e12 = op1(e11,e13)
| ~ spl28_484 ),
inference(avatar_component_clause,[],[f2889]) ).
fof(f2899,definition,
( spl28_487
<=> e13 = op1(e11,e12) ),
introduced(definition,[new_symbols(definition,[spl28_487])],[avatar_definition]) ).
fof(f2900,plain,
( e13 = op1(e11,e12)
| ~ spl28_487 ),
inference(avatar_component_clause,[],[f2899]) ).
fof(f2919,definition,
( spl28_493
<=> e11 = op1(e11,e10) ),
introduced(definition,[new_symbols(definition,[spl28_493])],[avatar_definition]) ).
fof(f2920,plain,
( e11 = op1(e11,e10)
| ~ spl28_493 ),
inference(avatar_component_clause,[],[f2919]) ).
fof(f2926,definition,
( spl28_495
<=> e13 = op1(e10,e13) ),
introduced(definition,[new_symbols(definition,[spl28_495])],[avatar_definition]) ).
fof(f2927,plain,
( e13 = op1(e10,e13)
| ~ spl28_495 ),
inference(avatar_component_clause,[],[f2926]) ).
fof(f2939,definition,
( spl28_499
<=> e13 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl28_499])],[avatar_definition]) ).
fof(f2940,plain,
( e13 = op1(e10,e12)
| ~ spl28_499 ),
inference(avatar_component_clause,[],[f2939]) ).
fof(f2942,definition,
( spl28_500
<=> e12 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl28_500])],[avatar_definition]) ).
fof(f2943,plain,
( e12 = op1(e10,e12)
| ~ spl28_500 ),
inference(avatar_component_clause,[],[f2942]) ).
fof(f2945,definition,
( spl28_501
<=> e11 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl28_501])],[avatar_definition]) ).
fof(f2946,plain,
( e11 = op1(e10,e12)
| ~ spl28_501 ),
inference(avatar_component_clause,[],[f2945]) ).
fof(f2948,definition,
( spl28_502
<=> e10 = op1(e10,e12) ),
introduced(definition,[new_symbols(definition,[spl28_502])],[avatar_definition]) ).
fof(f2949,plain,
( e10 = op1(e10,e12)
| ~ spl28_502 ),
inference(avatar_component_clause,[],[f2948]) ).
fof(f2950,plain,
( spl28_499
| spl28_500
| spl28_501
| spl28_502 ),
inference(avatar_split_clause,[],[f115,f2948,f2945,f2942,f2939]) ).
fof(f2958,definition,
( spl28_505
<=> e11 = op1(e10,e11) ),
introduced(definition,[new_symbols(definition,[spl28_505])],[avatar_definition]) ).
fof(f2959,plain,
( e11 = op1(e10,e11)
| ~ spl28_505 ),
inference(avatar_component_clause,[],[f2958]) ).
fof(f2965,plain,
( e21 = h9(e10)
| e20 = h12(e10)
| sP3
| sP2 ),
inference(forward_demodulation,[],[f2406,f567]) ).
fof(f2969,plain,
( e21 = h9(e10)
| e20 = h11(e10)
| sP3
| sP2 ),
inference(forward_demodulation,[],[f2410,f567]) ).
fof(f2978,definition,
( spl28_507
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl28_507])],[avatar_definition]) ).
fof(f2980,plain,
( e23 = h9(e10)
| ~ spl28_340 ),
inference(avatar_component_clause,[],[f2114]) ).
fof(f2981,plain,
( ~ spl28_507
| spl28_340 ),
inference(avatar_split_clause,[],[f2418,f2114,f2978]) ).
fof(f2989,definition,
( spl28_508
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl28_508])],[avatar_definition]) ).
fof(f2991,plain,
( e22 = h9(e10)
| ~ spl28_344 ),
inference(avatar_component_clause,[],[f2131]) ).
fof(f2992,plain,
( ~ spl28_508
| spl28_344 ),
inference(avatar_split_clause,[],[f2422,f2131,f2989]) ).
fof(f2999,plain,
( e10 = op1(e12,e12)
| sP1
| sP0 ),
inference(forward_subsumption_resolution,[],[f2426,f459]) ).
fof(f3000,plain,
( e10 = op1(e11,e11)
| sP1
| sP0 ),
inference(forward_subsumption_resolution,[],[f2448,f459]) ).
fof(f3001,plain,
( e10 = op1(e10,e10)
| sP1
| sP0 ),
inference(forward_subsumption_resolution,[],[f2455,f459]) ).
fof(f3002,plain,
~ sP0,
inference(forward_subsumption_resolution,[],[f2462,f457]) ).
fof(f3003,plain,
~ sP1,
inference(forward_subsumption_resolution,[],[f2476,f458]) ).
fof(f3068,plain,
op2(e22,h9(e10)) = op2(h9(e11),e23),
inference(forward_demodulation,[],[f2714,f566]) ).
fof(f3072,plain,
op2(e22,h9(e11)) = op2(h12(e10),e23),
inference(forward_demodulation,[],[f2718,f579]) ).
fof(f3074,plain,
op2(e22,h7(e11)) = op2(h12(e10),e20),
inference(forward_demodulation,[],[f2721,f579]) ).
fof(f3076,plain,
op2(e22,h5(e11)) = op2(h8(e11),e22),
inference(forward_demodulation,[],[f2723,f562]) ).
fof(f3077,plain,
op2(e22,h11(e10)) = op2(h8(e11),e21),
inference(forward_demodulation,[],[f2724,f562]) ).
fof(f3078,plain,
op2(e22,h4(e11)) = op2(h8(e11),e20),
inference(forward_demodulation,[],[f2725,f562]) ).
fof(f3079,plain,
op2(e22,h3(e11)) = op2(h7(e11),e23),
inference(forward_demodulation,[],[f2726,f558]) ).
fof(f3087,plain,
op2(e21,h9(e11)) = op2(h5(e11),e23),
inference(forward_demodulation,[],[f2734,f550]) ).
fof(f3092,plain,
op2(e21,h5(e11)) = op2(h11(e10),e22),
inference(forward_demodulation,[],[f2739,f575]) ).
fof(f3102,plain,
op2(e20,h9(e11)) = op2(h2(e11),e23),
inference(forward_demodulation,[],[f2750,f538]) ).
fof(f3104,plain,
op2(e20,h8(e11)) = op2(h2(e11),e21),
inference(forward_demodulation,[],[f2752,f538]) ).
fof(f3117,plain,
( e21 = h8(e11)
| e20 = h8(e11)
| e22 = op2(e22,e21)
| e23 = op2(e22,e21) ),
inference(forward_demodulation,[],[f2766,f562]) ).
fof(f3118,plain,
( e21 = h7(e11)
| e20 = h7(e11)
| e22 = op2(e22,e20)
| e23 = op2(e22,e20) ),
inference(forward_demodulation,[],[f2767,f558]) ).
fof(f3120,plain,
( e21 = h5(e11)
| e20 = h5(e11)
| e22 = op2(e21,e22)
| e23 = op2(e21,e22) ),
inference(forward_demodulation,[],[f2769,f550]) ).
fof(f3122,plain,
( e21 = h4(e11)
| e20 = h4(e11)
| e22 = op2(e21,e20)
| e23 = op2(e21,e20) ),
inference(forward_demodulation,[],[f2771,f546]) ).
fof(f3123,plain,
( e21 = h3(e11)
| e20 = h3(e11)
| e22 = op2(e20,e23)
| e23 = op2(e20,e23) ),
inference(forward_demodulation,[],[f2772,f542]) ).
fof(f3128,plain,
op1(e11,e13) = op1(e12,e10),
inference(forward_demodulation,[],[f2810,f530]) ).
fof(f3132,plain,
( e20 = h12(e10)
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f3133,plain,
( e21 = h9(e10)
| ~ spl28_101 ),
inference(avatar_component_clause,[],[f1222]) ).
fof(f3134,plain,
( spl28_507
| spl28_508
| spl28_26
| spl28_101 ),
inference(avatar_split_clause,[],[f2965,f1222,f958,f2989,f2978]) ).
fof(f3141,plain,
( e20 = h11(e10)
| ~ spl28_52 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f3142,plain,
( spl28_507
| spl28_508
| spl28_52
| spl28_101 ),
inference(avatar_split_clause,[],[f2969,f1222,f1052,f2989,f2978]) ).
fof(f3151,plain,
( spl28_409
| spl28_410
| spl28_412 ),
inference(avatar_split_clause,[],[f2999,f2437,f2431,f2428]) ).
fof(f3152,plain,
( spl28_409
| spl28_410
| spl28_415 ),
inference(avatar_split_clause,[],[f3000,f2450,f2431,f2428]) ).
fof(f3153,plain,
( spl28_409
| spl28_410
| spl28_416 ),
inference(avatar_split_clause,[],[f3001,f2457,f2431,f2428]) ).
fof(f3154,plain,
~ spl28_409,
inference(avatar_split_clause,[],[f3002,f2428]) ).
fof(f3155,plain,
~ spl28_410,
inference(avatar_split_clause,[],[f3003,f2431]) ).
fof(f3160,plain,
( e22 = h8(e11)
| e21 = h8(e11)
| e20 = h8(e11)
| e23 = op2(e22,e21) ),
inference(forward_demodulation,[],[f3117,f562]) ).
fof(f3161,plain,
( e22 = h7(e11)
| e21 = h7(e11)
| e20 = h7(e11)
| e23 = op2(e22,e20) ),
inference(forward_demodulation,[],[f3118,f558]) ).
fof(f3163,plain,
( e22 = h5(e11)
| e21 = h5(e11)
| e20 = h5(e11)
| e23 = op2(e21,e22) ),
inference(forward_demodulation,[],[f3120,f550]) ).
fof(f3165,plain,
( e22 = h4(e11)
| e21 = h4(e11)
| e20 = h4(e11)
| e23 = op2(e21,e20) ),
inference(forward_demodulation,[],[f3122,f546]) ).
fof(f3166,plain,
( e22 = h3(e11)
| e21 = h3(e11)
| e20 = h3(e11)
| e23 = op2(e20,e23) ),
inference(forward_demodulation,[],[f3123,f542]) ).
fof(f3174,plain,
( e23 = h8(e11)
| e22 = h8(e11)
| e21 = h8(e11)
| e20 = h8(e11) ),
inference(forward_demodulation,[],[f3160,f562]) ).
fof(f3175,plain,
( e23 = h7(e11)
| e22 = h7(e11)
| e21 = h7(e11)
| e20 = h7(e11) ),
inference(forward_demodulation,[],[f3161,f558]) ).
fof(f3177,plain,
( e23 = h5(e11)
| e22 = h5(e11)
| e21 = h5(e11)
| e20 = h5(e11) ),
inference(forward_demodulation,[],[f3163,f550]) ).
fof(f3179,plain,
( e23 = h4(e11)
| e22 = h4(e11)
| e21 = h4(e11)
| e20 = h4(e11) ),
inference(forward_demodulation,[],[f3165,f546]) ).
fof(f3180,plain,
( e23 = h3(e11)
| e22 = h3(e11)
| e21 = h3(e11)
| e20 = h3(e11) ),
inference(forward_demodulation,[],[f3166,f542]) ).
fof(f3200,plain,
( e20 = h8(e11)
| ~ spl28_129 ),
inference(avatar_component_clause,[],[f1327]) ).
fof(f3201,plain,
( e21 = h8(e11)
| ~ spl28_126 ),
inference(avatar_component_clause,[],[f1312]) ).
fof(f3202,plain,
( e22 = h8(e11)
| ~ spl28_351 ),
inference(avatar_component_clause,[],[f2161]) ).
fof(f3203,plain,
( e23 = h8(e11)
| ~ spl28_347 ),
inference(avatar_component_clause,[],[f2144]) ).
fof(f3204,plain,
( spl28_129
| spl28_126
| spl28_351
| spl28_347 ),
inference(avatar_split_clause,[],[f3174,f2144,f2161,f1312,f1327]) ).
fof(f3205,plain,
( e20 = h7(e11)
| ~ spl28_155 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f3206,plain,
( e21 = h7(e11)
| ~ spl28_152 ),
inference(avatar_component_clause,[],[f1406]) ).
fof(f3207,plain,
( e22 = h7(e11)
| ~ spl28_359 ),
inference(avatar_component_clause,[],[f2195]) ).
fof(f3208,plain,
( e23 = h7(e11)
| ~ spl28_355 ),
inference(avatar_component_clause,[],[f2178]) ).
fof(f3209,plain,
( spl28_155
| spl28_152
| spl28_359
| spl28_355 ),
inference(avatar_split_clause,[],[f3175,f2178,f2195,f1406,f1421]) ).
fof(f3215,plain,
( e20 = h5(e11)
| ~ spl28_207 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f3216,plain,
( e21 = h5(e11)
| ~ spl28_204 ),
inference(avatar_component_clause,[],[f1594]) ).
fof(f3217,plain,
( e22 = h5(e11)
| ~ spl28_375 ),
inference(avatar_component_clause,[],[f2263]) ).
fof(f3218,plain,
( e23 = h5(e11)
| ~ spl28_371 ),
inference(avatar_component_clause,[],[f2246]) ).
fof(f3219,plain,
( spl28_207
| spl28_204
| spl28_375
| spl28_371 ),
inference(avatar_split_clause,[],[f3177,f2246,f2263,f1594,f1609]) ).
fof(f3221,plain,
( e20 = h4(e11)
| ~ spl28_233 ),
inference(avatar_component_clause,[],[f1703]) ).
fof(f3222,plain,
( e21 = h4(e11)
| ~ spl28_230 ),
inference(avatar_component_clause,[],[f1688]) ).
fof(f3223,plain,
( e22 = h4(e11)
| ~ spl28_383 ),
inference(avatar_component_clause,[],[f2297]) ).
fof(f3224,plain,
( e23 = h4(e11)
| ~ spl28_379 ),
inference(avatar_component_clause,[],[f2280]) ).
fof(f3225,plain,
( spl28_233
| spl28_230
| spl28_383
| spl28_379 ),
inference(avatar_split_clause,[],[f3179,f2280,f2297,f1688,f1703]) ).
fof(f3226,plain,
( e20 = h3(e11)
| ~ spl28_259 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f3227,plain,
( e21 = h3(e11)
| ~ spl28_256 ),
inference(avatar_component_clause,[],[f1782]) ).
fof(f3228,plain,
( e22 = h3(e11)
| ~ spl28_391 ),
inference(avatar_component_clause,[],[f2331]) ).
fof(f3229,plain,
( e23 = h3(e11)
| ~ spl28_387 ),
inference(avatar_component_clause,[],[f2314]) ).
fof(f3230,plain,
( spl28_259
| spl28_256
| spl28_391
| spl28_387 ),
inference(avatar_split_clause,[],[f3180,f2314,f2331,f1782,f1797]) ).
fof(f3231,plain,
( e20 = h2(e11)
| ~ spl28_285 ),
inference(avatar_component_clause,[],[f1891]) ).
fof(f3246,plain,
( op2(e21,e21) != h8(op1(e13,e13))
| spl28_109 ),
inference(forward_demodulation,[],[f1260,f564]) ).
fof(f3270,plain,
( op2(e21,e21) != h8(e10)
| spl28_109 ),
inference(forward_demodulation,[],[f3246,f531]) ).
fof(f3283,plain,
( $false
| spl28_109 ),
inference(forward_subsumption_resolution,[],[f3270,f563]) ).
fof(f3284,plain,
spl28_109,
inference(avatar_contradiction_clause,[],[f3283]) ).
fof(f3375,plain,
( h8(op1(e13,e10)) != op2(e21,h8(e10))
| spl28_112 ),
inference(forward_demodulation,[],[f1269,f564]) ).
fof(f3376,plain,
( h8(op1(e10,e13)) != op2(e21,h8(e10))
| spl28_112 ),
inference(forward_demodulation,[],[f3375,f2805]) ).
fof(f3377,plain,
( h8(e13) != op2(e21,h8(e10))
| spl28_112
| ~ spl28_495 ),
inference(forward_demodulation,[],[f3376,f2927]) ).
fof(f3378,plain,
( e21 != op2(e21,h8(e10))
| spl28_112
| ~ spl28_495 ),
inference(forward_demodulation,[],[f3377,f564]) ).
fof(f3390,plain,
h8(e10) = h11(e10),
inference(superposition,[],[f563,f575]) ).
fof(f3391,plain,
( e20 = h8(e10)
| ~ spl28_52 ),
inference(forward_demodulation,[],[f3390,f3141]) ).
fof(f3394,plain,
e20 = h9(e10),
inference(superposition,[],[f533,f567]) ).
fof(f3426,plain,
h1(e10) = h8(e10),
inference(superposition,[],[f563,f535]) ).
fof(f3427,plain,
( e20 = h1(e10)
| ~ spl28_52 ),
inference(forward_demodulation,[],[f3426,f3391]) ).
fof(f3432,plain,
e21 = h9(e11),
inference(superposition,[],[f532,f566]) ).
fof(f3436,plain,
( e23 = op2(e23,e23)
| ~ spl28_451 ),
inference(superposition,[],[f284,f2687]) ).
fof(f3439,plain,
( e20 = e23
| ~ spl28_451 ),
inference(forward_demodulation,[],[f3436,f533]) ).
fof(f3442,plain,
( $false
| ~ spl28_451 ),
inference(forward_subsumption_resolution,[],[f3439,f463]) ).
fof(f3443,plain,
~ spl28_451,
inference(avatar_contradiction_clause,[],[f3442]) ).
fof(f3445,plain,
( e23 = op2(e22,e23)
| ~ spl28_452 ),
inference(superposition,[],[f285,f2690]) ).
fof(f3450,plain,
( e21 = e23
| ~ spl28_452 ),
inference(forward_demodulation,[],[f3445,f532]) ).
fof(f3451,plain,
( $false
| ~ spl28_452 ),
inference(forward_subsumption_resolution,[],[f3450,f461]) ).
fof(f3452,plain,
~ spl28_452,
inference(avatar_contradiction_clause,[],[f3451]) ).
fof(f3455,plain,
( e13 = op1(e13,e13)
| ~ spl28_459 ),
inference(superposition,[],[f183,f2794]) ).
fof(f3458,plain,
( e10 = e13
| ~ spl28_459 ),
inference(forward_demodulation,[],[f3455,f531]) ).
fof(f3465,plain,
( $false
| ~ spl28_459 ),
inference(forward_subsumption_resolution,[],[f3458,f457]) ).
fof(f3466,plain,
~ spl28_459,
inference(avatar_contradiction_clause,[],[f3465]) ).
fof(f3470,plain,
( e12 = op1(e12,e12)
| ~ spl28_460 ),
inference(superposition,[],[f185,f2797]) ).
fof(f3471,plain,
( e10 = e12
| ~ spl28_412
| ~ spl28_460 ),
inference(forward_demodulation,[],[f3470,f2438]) ).
fof(f3474,plain,
( $false
| ~ spl28_412
| ~ spl28_460 ),
inference(forward_subsumption_resolution,[],[f3471,f458]) ).
fof(f3475,plain,
( ~ spl28_412
| ~ spl28_460 ),
inference(avatar_contradiction_clause,[],[f3474]) ).
fof(f3476,plain,
( e11 = op1(e11,e11)
| ~ spl28_461 ),
inference(superposition,[],[f187,f2800]) ).
fof(f3482,plain,
( e10 = e11
| ~ spl28_415
| ~ spl28_461 ),
inference(forward_demodulation,[],[f3476,f2451]) ).
fof(f3485,plain,
( $false
| ~ spl28_415
| ~ spl28_461 ),
inference(forward_subsumption_resolution,[],[f3482,f459]) ).
fof(f3486,plain,
( ~ spl28_415
| ~ spl28_461 ),
inference(avatar_contradiction_clause,[],[f3485]) ).
fof(f3487,plain,
( e11 = op1(e11,e10)
| ~ spl28_462 ),
inference(superposition,[],[f187,f2803]) ).
fof(f3490,plain,
( e12 = op1(e12,e10)
| ~ spl28_462 ),
inference(superposition,[],[f185,f2803]) ).
fof(f3492,plain,
( spl28_493
| ~ spl28_462 ),
inference(avatar_split_clause,[],[f3487,f2802,f2919]) ).
fof(f3510,plain,
( e21 = op2(e21,e21)
| ~ spl28_453 ),
inference(superposition,[],[f289,f2693]) ).
fof(f3515,plain,
( e13 = op1(e10,e13)
| ~ spl28_462 ),
inference(superposition,[],[f184,f2803]) ).
fof(f3516,plain,
( e12 = op1(e11,e13)
| ~ spl28_480 ),
inference(superposition,[],[f3128,f2877]) ).
fof(f3526,plain,
( spl28_480
| ~ spl28_462 ),
inference(avatar_split_clause,[],[f3490,f2802,f2876]) ).
fof(f3527,plain,
( spl28_484
| ~ spl28_480 ),
inference(avatar_split_clause,[],[f3516,f2876,f2889]) ).
fof(f3561,plain,
( e20 = e21
| ~ spl28_101 ),
inference(forward_demodulation,[],[f3133,f3394]) ).
fof(f3571,plain,
( $false
| ~ spl28_101 ),
inference(forward_subsumption_resolution,[],[f3561,f465]) ).
fof(f3572,plain,
~ spl28_101,
inference(avatar_contradiction_clause,[],[f3571]) ).
fof(f3599,plain,
( op2(e20,e22) = op2(e22,e20)
| ~ spl28_26 ),
inference(superposition,[],[f2719,f3132]) ).
fof(f3600,plain,
( op2(e20,e22) = h7(e11)
| ~ spl28_26 ),
inference(forward_demodulation,[],[f3599,f558]) ).
fof(f3615,plain,
( e20 = op2(e20,e22)
| ~ spl28_26
| ~ spl28_155 ),
inference(forward_demodulation,[],[f3600,f3205]) ).
fof(f3625,plain,
( op2(e20,e20) = op2(e22,h7(e11))
| ~ spl28_26 ),
inference(superposition,[],[f3074,f3132]) ).
fof(f3633,plain,
( e12 = op1(e10,e12)
| ~ spl28_462 ),
inference(superposition,[],[f186,f2803]) ).
fof(f3634,plain,
( e12 = e13
| ~ spl28_462
| ~ spl28_499 ),
inference(forward_demodulation,[],[f3633,f2940]) ).
fof(f3635,plain,
( $false
| ~ spl28_462
| ~ spl28_499 ),
inference(forward_subsumption_resolution,[],[f3634,f454]) ).
fof(f3636,plain,
( ~ spl28_462
| ~ spl28_499 ),
inference(avatar_contradiction_clause,[],[f3635]) ).
fof(f3698,plain,
( op2(e20,e23) = op2(e22,h9(e11))
| ~ spl28_26 ),
inference(superposition,[],[f3072,f3132]) ).
fof(f3699,plain,
( op2(e20,e23) = op2(e22,e21)
| ~ spl28_26 ),
inference(forward_demodulation,[],[f3698,f3432]) ).
fof(f3700,plain,
( op2(e20,e23) = h8(e11)
| ~ spl28_26 ),
inference(forward_demodulation,[],[f3699,f562]) ).
fof(f3701,plain,
( e20 = op2(e20,e23)
| ~ spl28_26
| ~ spl28_129 ),
inference(forward_demodulation,[],[f3700,f3200]) ).
fof(f3706,plain,
( op2(e20,e21) = op2(e21,e20)
| ~ spl28_52 ),
inference(superposition,[],[f2740,f3141]) ).
fof(f3707,plain,
( op2(e20,e21) = h4(e11)
| ~ spl28_52 ),
inference(forward_demodulation,[],[f3706,f546]) ).
fof(f3712,plain,
( e20 = op2(e20,e21)
| ~ spl28_52
| ~ spl28_233 ),
inference(forward_demodulation,[],[f3707,f3221]) ).
fof(f3735,plain,
op2(e21,e23) = op2(e22,h9(e10)),
inference(superposition,[],[f3068,f3432]) ).
fof(f3736,plain,
op2(e21,e23) = op2(e22,e20),
inference(forward_demodulation,[],[f3735,f3394]) ).
fof(f3737,plain,
op2(e21,e23) = h7(e11),
inference(forward_demodulation,[],[f3736,f558]) ).
fof(f3772,plain,
( e11 = op1(e10,e11)
| ~ spl28_462 ),
inference(superposition,[],[f188,f2803]) ).
fof(f3773,plain,
( spl28_505
| ~ spl28_462 ),
inference(avatar_split_clause,[],[f3772,f2802,f2958]) ).
fof(f3924,plain,
( op2(e20,e23) = op2(e21,h9(e11))
| ~ spl28_207 ),
inference(superposition,[],[f3087,f3215]) ).
fof(f3925,plain,
( op2(e20,e23) = op2(e21,e21)
| ~ spl28_207 ),
inference(forward_demodulation,[],[f3924,f3432]) ).
fof(f3926,plain,
( op2(e20,e23) = h11(e10)
| ~ spl28_207 ),
inference(forward_demodulation,[],[f3925,f575]) ).
fof(f3927,plain,
( e20 = op2(e20,e23)
| ~ spl28_52
| ~ spl28_207 ),
inference(forward_demodulation,[],[f3926,f3141]) ).
fof(f4083,plain,
( op2(e20,e23) = op2(e20,h9(e11))
| ~ spl28_285 ),
inference(superposition,[],[f3102,f3231]) ).
fof(f4084,plain,
( op2(e20,e21) = op2(e20,e23)
| ~ spl28_285 ),
inference(forward_demodulation,[],[f4083,f3432]) ).
fof(f4085,plain,
( op2(e20,e21) = h3(e11)
| ~ spl28_285 ),
inference(forward_demodulation,[],[f4084,f542]) ).
fof(f4086,plain,
( e20 = op2(e20,e21)
| ~ spl28_259
| ~ spl28_285 ),
inference(forward_demodulation,[],[f4085,f3226]) ).
fof(f4235,plain,
( op1(e11,e12) = op1(e12,e11)
| ~ spl28_465 ),
inference(superposition,[],[f2811,f2827]) ).
fof(f4236,plain,
( e13 = op1(e11,e12)
| ~ spl28_465
| ~ spl28_475 ),
inference(forward_demodulation,[],[f4235,f2861]) ).
fof(f4239,plain,
( e21 != op2(e21,e20)
| ~ spl28_52
| spl28_112
| ~ spl28_495 ),
inference(superposition,[],[f3378,f3391]) ).
fof(f4240,plain,
( e21 != h4(e11)
| ~ spl28_52
| spl28_112
| ~ spl28_495 ),
inference(forward_demodulation,[],[f4239,f546]) ).
fof(f4241,plain,
( e21 = h1(e10)
| ~ spl28_453 ),
inference(superposition,[],[f3510,f535]) ).
fof(f4252,plain,
( e20 = e21
| ~ spl28_52
| ~ spl28_453 ),
inference(forward_demodulation,[],[f4241,f3427]) ).
fof(f4263,plain,
( $false
| ~ spl28_52
| ~ spl28_453 ),
inference(forward_subsumption_resolution,[],[f4252,f465]) ).
fof(f4264,plain,
( ~ spl28_52
| ~ spl28_453 ),
inference(avatar_contradiction_clause,[],[f4263]) ).
fof(f4266,plain,
( e23 = op2(e20,e23)
| ~ spl28_454 ),
inference(superposition,[],[f285,f2696]) ).
fof(f4267,plain,
( e22 = op2(e22,e20)
| ~ spl28_454 ),
inference(superposition,[],[f286,f2696]) ).
fof(f4268,plain,
( e22 = op2(e20,e22)
| ~ spl28_454 ),
inference(superposition,[],[f287,f2696]) ).
fof(f4270,plain,
( e21 = op2(e20,e21)
| ~ spl28_454 ),
inference(superposition,[],[f289,f2696]) ).
fof(f4272,plain,
( e20 = op2(e20,e20)
| ~ spl28_454 ),
inference(superposition,[],[f291,f2696]) ).
fof(f4275,plain,
( e20 = e22
| ~ spl28_26
| ~ spl28_155
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4268,f3615]) ).
fof(f4281,plain,
( $false
| ~ spl28_26
| ~ spl28_155
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4275,f464]) ).
fof(f4282,plain,
( ~ spl28_26
| ~ spl28_155
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4281]) ).
fof(f4290,plain,
( op2(e20,e20) = op2(e22,e21)
| ~ spl28_26
| ~ spl28_152 ),
inference(forward_demodulation,[],[f3625,f3206]) ).
fof(f4302,plain,
( e20 = e21
| ~ spl28_52
| ~ spl28_233
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4270,f3712]) ).
fof(f4320,plain,
( e20 = e23
| ~ spl28_26
| ~ spl28_129
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4266,f3701]) ).
fof(f4323,plain,
( op2(e20,e20) = h8(e11)
| ~ spl28_26
| ~ spl28_152 ),
inference(forward_demodulation,[],[f4290,f562]) ).
fof(f4332,plain,
( $false
| ~ spl28_52
| ~ spl28_233
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4302,f465]) ).
fof(f4333,plain,
( ~ spl28_52
| ~ spl28_233
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4332]) ).
fof(f4348,plain,
( $false
| ~ spl28_26
| ~ spl28_129
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4320,f463]) ).
fof(f4349,plain,
( ~ spl28_26
| ~ spl28_129
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4348]) ).
fof(f4389,plain,
( e23 = op2(e20,e21)
| ~ spl28_52
| ~ spl28_379 ),
inference(forward_demodulation,[],[f3707,f3224]) ).
fof(f4398,plain,
( e20 = e21
| ~ spl28_259
| ~ spl28_285
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4270,f4086]) ).
fof(f4405,plain,
( e20 = e23
| ~ spl28_52
| ~ spl28_207
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4266,f3927]) ).
fof(f4424,plain,
( $false
| ~ spl28_259
| ~ spl28_285
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4398,f465]) ).
fof(f4425,plain,
( ~ spl28_259
| ~ spl28_285
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4424]) ).
fof(f4434,plain,
( $false
| ~ spl28_52
| ~ spl28_207
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4405,f463]) ).
fof(f4435,plain,
( ~ spl28_52
| ~ spl28_207
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4434]) ).
fof(f4486,plain,
( e22 = op2(e20,e23)
| ~ spl28_26
| ~ spl28_351 ),
inference(forward_demodulation,[],[f3700,f3202]) ).
fof(f4490,plain,
( e23 = op2(e20,e21)
| ~ spl28_285
| ~ spl28_387 ),
inference(forward_demodulation,[],[f4085,f3229]) ).
fof(f4492,plain,
( e21 = e23
| ~ spl28_52
| ~ spl28_379
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4389,f4270]) ).
fof(f4503,plain,
( e22 = e23
| ~ spl28_26
| ~ spl28_351
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4486,f4266]) ).
fof(f4507,plain,
( e21 = e23
| ~ spl28_285
| ~ spl28_387
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4490,f4270]) ).
fof(f4509,plain,
( $false
| ~ spl28_52
| ~ spl28_379
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4492,f461]) ).
fof(f4510,plain,
( ~ spl28_52
| ~ spl28_379
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4509]) ).
fof(f4522,plain,
( $false
| ~ spl28_26
| ~ spl28_351
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4503,f460]) ).
fof(f4523,plain,
( ~ spl28_26
| ~ spl28_351
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4522]) ).
fof(f4529,plain,
( $false
| ~ spl28_285
| ~ spl28_387
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4507,f461]) ).
fof(f4530,plain,
( ~ spl28_285
| ~ spl28_387
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4529]) ).
fof(f4560,plain,
( op2(e20,e20) = e21
| ~ spl28_26
| ~ spl28_126
| ~ spl28_152 ),
inference(forward_demodulation,[],[f4323,f3201]) ).
fof(f4568,plain,
( $false
| ~ spl28_52
| spl28_112
| ~ spl28_230
| ~ spl28_495 ),
inference(forward_subsumption_resolution,[],[f4240,f3222]) ).
fof(f4569,plain,
( ~ spl28_52
| spl28_112
| ~ spl28_230
| ~ spl28_495 ),
inference(avatar_contradiction_clause,[],[f4568]) ).
fof(f4573,plain,
( e20 = e21
| ~ spl28_26
| ~ spl28_126
| ~ spl28_152
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4560,f4272]) ).
fof(f4578,plain,
( $false
| ~ spl28_26
| ~ spl28_126
| ~ spl28_152
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4573,f465]) ).
fof(f4579,plain,
( ~ spl28_26
| ~ spl28_126
| ~ spl28_152
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4578]) ).
fof(f4587,plain,
( op2(e20,e20) = e23
| ~ spl28_26
| ~ spl28_152
| ~ spl28_347 ),
inference(forward_demodulation,[],[f4323,f3203]) ).
fof(f4607,plain,
( e20 = e23
| ~ spl28_26
| ~ spl28_152
| ~ spl28_347
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4587,f4272]) ).
fof(f4619,plain,
( $false
| ~ spl28_26
| ~ spl28_152
| ~ spl28_347
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4607,f463]) ).
fof(f4620,plain,
( ~ spl28_26
| ~ spl28_152
| ~ spl28_347
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4619]) ).
fof(f4651,plain,
( op2(e20,e20) = op2(e22,e23)
| ~ spl28_26
| ~ spl28_355 ),
inference(forward_demodulation,[],[f3625,f3208]) ).
fof(f4667,plain,
( op2(e20,e20) = h9(e11)
| ~ spl28_26
| ~ spl28_355 ),
inference(forward_demodulation,[],[f4651,f566]) ).
fof(f4681,plain,
( op2(e20,e20) = e21
| ~ spl28_26
| ~ spl28_355 ),
inference(forward_demodulation,[],[f4667,f3432]) ).
fof(f4694,plain,
( e20 = e21
| ~ spl28_26
| ~ spl28_355
| ~ spl28_454 ),
inference(forward_demodulation,[],[f4681,f4272]) ).
fof(f4700,plain,
( $false
| ~ spl28_26
| ~ spl28_355
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f4694,f465]) ).
fof(f4701,plain,
( ~ spl28_26
| ~ spl28_355
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f4700]) ).
fof(f4718,plain,
( e22 = op2(e21,e23)
| ~ spl28_359 ),
inference(forward_demodulation,[],[f3737,f3207]) ).
fof(f4850,plain,
( e20 = e23
| ~ spl28_340 ),
inference(forward_demodulation,[],[f2980,f3394]) ).
fof(f4869,plain,
( $false
| ~ spl28_340 ),
inference(forward_subsumption_resolution,[],[f4850,f463]) ).
fof(f4870,plain,
~ spl28_340,
inference(avatar_contradiction_clause,[],[f4869]) ).
fof(f4905,plain,
( e20 = e22
| ~ spl28_344 ),
inference(forward_demodulation,[],[f2991,f3394]) ).
fof(f4923,plain,
( $false
| ~ spl28_344 ),
inference(forward_subsumption_resolution,[],[f4905,f464]) ).
fof(f4924,plain,
~ spl28_344,
inference(avatar_contradiction_clause,[],[f4923]) ).
fof(f4949,plain,
( h8(op1(e12,e13)) != op2(h8(e12),e21)
| spl28_113 ),
inference(forward_demodulation,[],[f1272,f564]) ).
fof(f4960,plain,
( op2(e22,e21) != h8(op1(e12,e13))
| spl28_113 ),
inference(forward_demodulation,[],[f4949,f565]) ).
fof(f4967,plain,
( op2(e22,e21) != h8(e11)
| spl28_113 ),
inference(forward_demodulation,[],[f4960,f530]) ).
fof(f4974,plain,
( $false
| spl28_113 ),
inference(forward_subsumption_resolution,[],[f4967,f562]) ).
fof(f4975,plain,
spl28_113,
inference(avatar_contradiction_clause,[],[f4974]) ).
fof(f5072,plain,
( h8(op1(e10,e12)) != op2(h8(e10),e22)
| spl28_122 ),
inference(forward_demodulation,[],[f1299,f565]) ).
fof(f5080,plain,
( h8(op1(e10,e12)) != op2(h1(e10),e22)
| spl28_122 ),
inference(forward_demodulation,[],[f5072,f3426]) ).
fof(f5194,plain,
( op2(e20,e22) = op2(e21,h5(e11))
| ~ spl28_52 ),
inference(superposition,[],[f3092,f3141]) ).
fof(f5196,plain,
( op2(e20,e21) = op2(e21,e20)
| ~ spl28_52 ),
inference(superposition,[],[f2740,f3141]) ).
fof(f5197,plain,
( op2(e20,e21) = h4(e11)
| ~ spl28_52 ),
inference(forward_demodulation,[],[f5196,f546]) ).
fof(f5228,plain,
( op2(e20,e22) != h8(op1(e10,e12))
| ~ spl28_52
| spl28_122 ),
inference(forward_demodulation,[],[f5080,f3427]) ).
fof(f5235,plain,
( op2(e20,e22) != h8(e12)
| ~ spl28_52
| spl28_122
| ~ spl28_500 ),
inference(forward_demodulation,[],[f5228,f2943]) ).
fof(f5240,plain,
( e22 != op2(e20,e22)
| ~ spl28_52
| spl28_122
| ~ spl28_500 ),
inference(forward_demodulation,[],[f5235,f565]) ).
fof(f5246,plain,
( $false
| ~ spl28_52
| spl28_122
| ~ spl28_454
| ~ spl28_500 ),
inference(forward_subsumption_resolution,[],[f5240,f4268]) ).
fof(f5247,plain,
( ~ spl28_52
| spl28_122
| ~ spl28_454
| ~ spl28_500 ),
inference(avatar_contradiction_clause,[],[f5246]) ).
fof(f5274,plain,
( h8(op1(e12,e10)) != op2(h8(e12),h1(e10))
| spl28_116 ),
inference(forward_demodulation,[],[f1281,f3426]) ).
fof(f5276,plain,
( h8(op1(e12,e10)) != op2(h8(e12),e20)
| ~ spl28_52
| spl28_116 ),
inference(forward_demodulation,[],[f5274,f3427]) ).
fof(f5278,plain,
( op2(e22,e20) != h8(op1(e12,e10))
| ~ spl28_52
| spl28_116 ),
inference(forward_demodulation,[],[f5276,f565]) ).
fof(f5280,plain,
( op2(e22,e20) != h8(op1(e11,e13))
| ~ spl28_52
| spl28_116 ),
inference(forward_demodulation,[],[f5278,f3128]) ).
fof(f5283,plain,
( op2(e22,e20) != h8(e12)
| ~ spl28_52
| spl28_116
| ~ spl28_484 ),
inference(forward_demodulation,[],[f5280,f2890]) ).
fof(f5284,plain,
( e22 != op2(e22,e20)
| ~ spl28_52
| spl28_116
| ~ spl28_484 ),
inference(forward_demodulation,[],[f5283,f565]) ).
fof(f5285,plain,
( $false
| ~ spl28_52
| spl28_116
| ~ spl28_454
| ~ spl28_484 ),
inference(forward_subsumption_resolution,[],[f5284,f4267]) ).
fof(f5286,plain,
( ~ spl28_52
| spl28_116
| ~ spl28_454
| ~ spl28_484 ),
inference(avatar_contradiction_clause,[],[f5285]) ).
fof(f5287,plain,
( h8(op1(e11,e13)) != op2(h8(e11),e21)
| spl28_117 ),
inference(forward_demodulation,[],[f1284,f564]) ).
fof(f5293,plain,
( h8(op1(e11,e13)) != op2(e22,h11(e10))
| spl28_117 ),
inference(forward_demodulation,[],[f5287,f3077]) ).
fof(f5294,plain,
( op2(e22,e20) != h8(op1(e11,e13))
| ~ spl28_52
| spl28_117 ),
inference(forward_demodulation,[],[f5293,f3141]) ).
fof(f5295,plain,
( op2(e22,e20) != h8(e12)
| ~ spl28_52
| spl28_117
| ~ spl28_484 ),
inference(forward_demodulation,[],[f5294,f2890]) ).
fof(f5296,plain,
( e22 != op2(e22,e20)
| ~ spl28_52
| spl28_117
| ~ spl28_484 ),
inference(forward_demodulation,[],[f5295,f565]) ).
fof(f5297,plain,
( $false
| ~ spl28_52
| spl28_117
| ~ spl28_454
| ~ spl28_484 ),
inference(forward_subsumption_resolution,[],[f5296,f4267]) ).
fof(f5298,plain,
( ~ spl28_52
| spl28_117
| ~ spl28_454
| ~ spl28_484 ),
inference(avatar_contradiction_clause,[],[f5297]) ).
fof(f5299,plain,
( h8(op1(e11,e10)) != op2(h8(e11),h1(e10))
| spl28_120 ),
inference(forward_demodulation,[],[f1293,f3426]) ).
fof(f5304,plain,
( h8(op1(e11,e10)) != op2(h8(e11),e20)
| ~ spl28_52
| spl28_120 ),
inference(forward_demodulation,[],[f5299,f3427]) ).
fof(f5305,plain,
( h8(op1(e11,e10)) != op2(e22,h4(e11))
| ~ spl28_52
| spl28_120 ),
inference(forward_demodulation,[],[f5304,f3078]) ).
fof(f5306,plain,
( op2(e22,e21) != h8(op1(e11,e10))
| ~ spl28_52
| spl28_120
| ~ spl28_230 ),
inference(forward_demodulation,[],[f5305,f3222]) ).
fof(f5307,plain,
( op2(e22,e21) != h8(e11)
| ~ spl28_52
| spl28_120
| ~ spl28_230
| ~ spl28_493 ),
inference(forward_demodulation,[],[f5306,f2920]) ).
fof(f5308,plain,
( $false
| ~ spl28_52
| spl28_120
| ~ spl28_230
| ~ spl28_493 ),
inference(forward_subsumption_resolution,[],[f5307,f562]) ).
fof(f5309,plain,
( ~ spl28_52
| spl28_120
| ~ spl28_230
| ~ spl28_493 ),
inference(avatar_contradiction_clause,[],[f5308]) ).
fof(f5310,plain,
( h8(op1(e10,e13)) != op2(h8(e10),e21)
| spl28_121 ),
inference(forward_demodulation,[],[f1296,f564]) ).
fof(f5311,plain,
( h8(op1(e10,e13)) != op2(h1(e10),e21)
| spl28_121 ),
inference(forward_demodulation,[],[f5310,f3426]) ).
fof(f5312,plain,
( op2(e20,e21) != h8(op1(e10,e13))
| ~ spl28_52
| spl28_121 ),
inference(forward_demodulation,[],[f5311,f3427]) ).
fof(f5313,plain,
( op2(e20,e21) != h8(e13)
| ~ spl28_52
| spl28_121
| ~ spl28_495 ),
inference(forward_demodulation,[],[f5312,f2927]) ).
fof(f5314,plain,
( e21 != op2(e20,e21)
| ~ spl28_52
| spl28_121
| ~ spl28_495 ),
inference(forward_demodulation,[],[f5313,f564]) ).
fof(f5315,plain,
( $false
| ~ spl28_52
| spl28_121
| ~ spl28_454
| ~ spl28_495 ),
inference(forward_subsumption_resolution,[],[f5314,f4270]) ).
fof(f5316,plain,
( ~ spl28_52
| spl28_121
| ~ spl28_454
| ~ spl28_495 ),
inference(avatar_contradiction_clause,[],[f5315]) ).
fof(f5317,plain,
( op2(h1(e10),h1(e10)) != h8(op1(e10,e10))
| spl28_124 ),
inference(forward_demodulation,[],[f1305,f3426]) ).
fof(f5318,plain,
( h8(e10) != op2(h1(e10),h1(e10))
| spl28_124
| ~ spl28_416 ),
inference(forward_demodulation,[],[f5317,f2458]) ).
fof(f5319,plain,
( op2(e20,e20) != h8(e10)
| ~ spl28_52
| spl28_124
| ~ spl28_416 ),
inference(forward_demodulation,[],[f5318,f3427]) ).
fof(f5320,plain,
( op2(e20,e20) != h1(e10)
| ~ spl28_52
| spl28_124
| ~ spl28_416 ),
inference(forward_demodulation,[],[f5319,f3426]) ).
fof(f5321,plain,
( e20 != op2(e20,e20)
| ~ spl28_52
| spl28_124
| ~ spl28_416 ),
inference(forward_demodulation,[],[f5320,f3427]) ).
fof(f5322,plain,
( $false
| ~ spl28_52
| spl28_124
| ~ spl28_416
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f5321,f4272]) ).
fof(f5323,plain,
( ~ spl28_52
| spl28_124
| ~ spl28_416
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f5322]) ).
fof(f5324,plain,
( op2(e22,e22) != h8(op1(e12,e12))
| spl28_114 ),
inference(forward_demodulation,[],[f1275,f565]) ).
fof(f5325,plain,
( op2(e22,e22) != h8(e10)
| spl28_114
| ~ spl28_412 ),
inference(forward_demodulation,[],[f5324,f2438]) ).
fof(f5326,plain,
( op2(e22,e22) != h1(e10)
| spl28_114
| ~ spl28_412 ),
inference(forward_demodulation,[],[f5325,f3426]) ).
fof(f5327,plain,
( e20 != op2(e22,e22)
| ~ spl28_52
| spl28_114
| ~ spl28_412 ),
inference(forward_demodulation,[],[f5326,f3427]) ).
fof(f5328,plain,
( e20 != h12(e10)
| ~ spl28_52
| spl28_114
| ~ spl28_412 ),
inference(forward_demodulation,[],[f5327,f579]) ).
fof(f5329,plain,
( $false
| ~ spl28_26
| ~ spl28_52
| spl28_114
| ~ spl28_412 ),
inference(forward_subsumption_resolution,[],[f5328,f3132]) ).
fof(f5330,plain,
( ~ spl28_26
| ~ spl28_52
| spl28_114
| ~ spl28_412 ),
inference(avatar_contradiction_clause,[],[f5329]) ).
fof(f5333,plain,
( $false
| ~ spl28_52
| spl28_130 ),
inference(forward_subsumption_resolution,[],[f1335,f3391]) ).
fof(f5334,plain,
( ~ spl28_52
| spl28_130 ),
inference(avatar_contradiction_clause,[],[f5333]) ).
fof(f5361,plain,
( op2(e21,e21) = op2(e22,h11(e10))
| ~ spl28_126 ),
inference(superposition,[],[f3077,f3201]) ).
fof(f5362,plain,
( op2(e21,e21) = op2(e22,e20)
| ~ spl28_52
| ~ spl28_126 ),
inference(forward_demodulation,[],[f5361,f3141]) ).
fof(f5366,plain,
( op2(e21,e21) = h7(e11)
| ~ spl28_52
| ~ spl28_126 ),
inference(forward_demodulation,[],[f5362,f558]) ).
fof(f5370,plain,
( e22 = op2(e21,e21)
| ~ spl28_52
| ~ spl28_126
| ~ spl28_359 ),
inference(forward_demodulation,[],[f5366,f3207]) ).
fof(f5488,plain,
( e22 = op2(e20,e21)
| ~ spl28_52
| ~ spl28_383 ),
inference(forward_demodulation,[],[f5197,f3223]) ).
fof(f5501,plain,
( e21 = e22
| ~ spl28_52
| ~ spl28_383
| ~ spl28_454 ),
inference(forward_demodulation,[],[f5488,f4270]) ).
fof(f5510,plain,
( $false
| ~ spl28_52
| ~ spl28_383
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f5501,f462]) ).
fof(f5511,plain,
( ~ spl28_52
| ~ spl28_383
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f5510]) ).
fof(f5601,plain,
( op2(e20,e22) = op2(e21,e21)
| ~ spl28_52
| ~ spl28_204 ),
inference(forward_demodulation,[],[f5194,f3216]) ).
fof(f5609,plain,
( op2(e20,e22) = h11(e10)
| ~ spl28_52
| ~ spl28_204 ),
inference(forward_demodulation,[],[f5601,f575]) ).
fof(f5616,plain,
( e20 = op2(e20,e22)
| ~ spl28_52
| ~ spl28_204 ),
inference(forward_demodulation,[],[f5609,f3141]) ).
fof(f5670,plain,
( op2(e20,e21) = op2(e20,h8(e11))
| ~ spl28_285 ),
inference(superposition,[],[f3104,f3231]) ).
fof(f5681,plain,
( op2(e22,e23) = op2(e22,h3(e11))
| ~ spl28_359 ),
inference(superposition,[],[f3079,f3207]) ).
fof(f5684,plain,
( op2(e22,e21) = op2(e22,e23)
| ~ spl28_256
| ~ spl28_359 ),
inference(forward_demodulation,[],[f5681,f3227]) ).
fof(f5686,plain,
( op2(e22,e21) = h9(e11)
| ~ spl28_256
| ~ spl28_359 ),
inference(forward_demodulation,[],[f5684,f566]) ).
fof(f5688,plain,
( e21 = op2(e22,e21)
| ~ spl28_256
| ~ spl28_359 ),
inference(forward_demodulation,[],[f5686,f3432]) ).
fof(f5753,plain,
( e20 = h2(e11)
| ~ spl28_52
| ~ spl28_204 ),
inference(superposition,[],[f5616,f538]) ).
fof(f5757,plain,
( e21 = h8(e11)
| ~ spl28_256
| ~ spl28_359 ),
inference(superposition,[],[f5688,f562]) ).
fof(f5759,plain,
( e22 = h1(e10)
| ~ spl28_52
| ~ spl28_126
| ~ spl28_359 ),
inference(superposition,[],[f5370,f535]) ).
fof(f5770,plain,
( e20 = e22
| ~ spl28_52
| ~ spl28_126
| ~ spl28_359 ),
inference(forward_demodulation,[],[f5759,f3427]) ).
fof(f5781,plain,
( $false
| ~ spl28_52
| ~ spl28_126
| ~ spl28_359 ),
inference(forward_subsumption_resolution,[],[f5770,f464]) ).
fof(f5782,plain,
( ~ spl28_52
| ~ spl28_126
| ~ spl28_359 ),
inference(avatar_contradiction_clause,[],[f5781]) ).
fof(f5784,plain,
( $false
| spl28_107 ),
inference(forward_subsumption_resolution,[],[f1254,f564]) ).
fof(f5785,plain,
spl28_107,
inference(avatar_contradiction_clause,[],[f5784]) ).
fof(f5792,plain,
( op2(e20,e21) = op2(e20,e23)
| ~ spl28_285
| ~ spl28_347 ),
inference(forward_demodulation,[],[f5670,f3203]) ).
fof(f5796,plain,
( $false
| spl28_126
| ~ spl28_256
| ~ spl28_359 ),
inference(forward_subsumption_resolution,[],[f5757,f1313]) ).
fof(f5797,plain,
( spl28_126
| ~ spl28_256
| ~ spl28_359 ),
inference(avatar_contradiction_clause,[],[f5796]) ).
fof(f5815,plain,
( op2(e20,e21) = h3(e11)
| ~ spl28_285
| ~ spl28_347 ),
inference(forward_demodulation,[],[f5792,f542]) ).
fof(f5840,plain,
( h8(op1(e10,e11)) != op2(h8(e10),e23)
| spl28_123
| ~ spl28_347 ),
inference(forward_demodulation,[],[f1302,f3203]) ).
fof(f5850,plain,
( e22 = op2(e20,e21)
| ~ spl28_285
| ~ spl28_347
| ~ spl28_391 ),
inference(forward_demodulation,[],[f5815,f3228]) ).
fof(f5852,plain,
( h8(op1(e10,e11)) != op2(h1(e10),e23)
| spl28_123
| ~ spl28_347 ),
inference(forward_demodulation,[],[f5840,f3426]) ).
fof(f5861,plain,
( e21 = e22
| ~ spl28_285
| ~ spl28_347
| ~ spl28_391
| ~ spl28_454 ),
inference(forward_demodulation,[],[f5850,f4270]) ).
fof(f5864,plain,
( op2(e20,e23) != h8(op1(e10,e11))
| ~ spl28_52
| spl28_123
| ~ spl28_347 ),
inference(forward_demodulation,[],[f5852,f3427]) ).
fof(f5874,plain,
( $false
| ~ spl28_285
| ~ spl28_347
| ~ spl28_391
| ~ spl28_454 ),
inference(forward_subsumption_resolution,[],[f5861,f462]) ).
fof(f5875,plain,
( ~ spl28_285
| ~ spl28_347
| ~ spl28_391
| ~ spl28_454 ),
inference(avatar_contradiction_clause,[],[f5874]) ).
fof(f5876,plain,
( op2(e20,e23) != h8(e11)
| ~ spl28_52
| spl28_123
| ~ spl28_347
| ~ spl28_505 ),
inference(forward_demodulation,[],[f5864,f2959]) ).
fof(f5879,plain,
( e23 != op2(e20,e23)
| ~ spl28_52
| spl28_123
| ~ spl28_347
| ~ spl28_505 ),
inference(forward_demodulation,[],[f5876,f3203]) ).
fof(f5883,plain,
( $false
| ~ spl28_52
| spl28_123
| ~ spl28_347
| ~ spl28_454
| ~ spl28_505 ),
inference(forward_subsumption_resolution,[],[f5879,f4266]) ).
fof(f5884,plain,
( ~ spl28_52
| spl28_123
| ~ spl28_347
| ~ spl28_454
| ~ spl28_505 ),
inference(avatar_contradiction_clause,[],[f5883]) ).
fof(f5888,plain,
( op2(e23,e23) != h8(op1(e11,e11))
| spl28_119
| ~ spl28_347 ),
inference(forward_demodulation,[],[f1290,f3203]) ).
fof(f5895,plain,
( $false
| ~ spl28_52
| ~ spl28_204
| spl28_285 ),
inference(forward_subsumption_resolution,[],[f5753,f1892]) ).
fof(f5896,plain,
( ~ spl28_52
| ~ spl28_204
| spl28_285 ),
inference(avatar_contradiction_clause,[],[f5895]) ).
fof(f5904,plain,
( op2(e23,e23) != h8(e10)
| spl28_119
| ~ spl28_347
| ~ spl28_415 ),
inference(forward_demodulation,[],[f5888,f2451]) ).
fof(f5913,plain,
( op2(e23,e23) != h1(e10)
| spl28_119
| ~ spl28_347
| ~ spl28_415 ),
inference(forward_demodulation,[],[f5904,f3426]) ).
fof(f5923,plain,
( e20 != op2(e23,e23)
| ~ spl28_52
| spl28_119
| ~ spl28_347
| ~ spl28_415 ),
inference(forward_demodulation,[],[f5913,f3427]) ).
fof(f5930,plain,
( $false
| ~ spl28_52
| spl28_119
| ~ spl28_347
| ~ spl28_415 ),
inference(forward_subsumption_resolution,[],[f5923,f533]) ).
fof(f5931,plain,
( ~ spl28_52
| spl28_119
| ~ spl28_347
| ~ spl28_415 ),
inference(avatar_contradiction_clause,[],[f5930]) ).
fof(f5944,plain,
( $false
| spl28_350 ),
inference(forward_subsumption_resolution,[],[f2158,f565]) ).
fof(f5945,plain,
spl28_350,
inference(avatar_contradiction_clause,[],[f5944]) ).
fof(f5976,plain,
( h8(op1(e13,e12)) != op2(h8(e13),e22)
| spl28_110 ),
inference(forward_demodulation,[],[f1263,f565]) ).
fof(f5982,plain,
( op2(e21,e22) != h8(op1(e13,e12))
| spl28_110 ),
inference(forward_demodulation,[],[f5976,f564]) ).
fof(f5989,plain,
( op2(e21,e22) != h8(e11)
| spl28_110
| ~ spl28_465 ),
inference(forward_demodulation,[],[f5982,f2827]) ).
fof(f5994,plain,
( e23 != op2(e21,e22)
| spl28_110
| ~ spl28_347
| ~ spl28_465 ),
inference(forward_demodulation,[],[f5989,f3203]) ).
fof(f5999,plain,
( e23 != h5(e11)
| spl28_110
| ~ spl28_347
| ~ spl28_465 ),
inference(forward_demodulation,[],[f5994,f550]) ).
fof(f6097,plain,
( e11 = e12
| ~ spl28_462
| ~ spl28_501 ),
inference(forward_demodulation,[],[f3633,f2946]) ).
fof(f6101,plain,
( $false
| ~ spl28_462
| ~ spl28_501 ),
inference(forward_subsumption_resolution,[],[f6097,f456]) ).
fof(f6102,plain,
( ~ spl28_462
| ~ spl28_501 ),
inference(avatar_contradiction_clause,[],[f6101]) ).
fof(f6172,plain,
( op2(e22,e23) = op2(e21,h9(e11))
| ~ spl28_375 ),
inference(superposition,[],[f3087,f3217]) ).
fof(f6179,plain,
( op2(e21,e21) = op2(e22,e23)
| ~ spl28_375 ),
inference(forward_demodulation,[],[f6172,f3432]) ).
fof(f6183,plain,
( op2(e21,e21) = h9(e11)
| ~ spl28_375 ),
inference(forward_demodulation,[],[f6179,f566]) ).
fof(f6187,plain,
( e21 = op2(e21,e21)
| ~ spl28_375 ),
inference(forward_demodulation,[],[f6183,f3432]) ).
fof(f6340,plain,
( e21 = h1(e10)
| ~ spl28_375 ),
inference(superposition,[],[f6187,f535]) ).
fof(f6351,plain,
( e20 = e21
| ~ spl28_52
| ~ spl28_375 ),
inference(forward_demodulation,[],[f6340,f3427]) ).
fof(f6362,plain,
( $false
| ~ spl28_52
| ~ spl28_375 ),
inference(forward_subsumption_resolution,[],[f6351,f465]) ).
fof(f6363,plain,
( ~ spl28_52
| ~ spl28_375 ),
inference(avatar_contradiction_clause,[],[f6362]) ).
fof(f6369,plain,
( $false
| spl28_110
| ~ spl28_347
| ~ spl28_371
| ~ spl28_465 ),
inference(forward_subsumption_resolution,[],[f5999,f3218]) ).
fof(f6370,plain,
( spl28_110
| ~ spl28_347
| ~ spl28_371
| ~ spl28_465 ),
inference(avatar_contradiction_clause,[],[f6369]) ).
fof(f6381,plain,
( h8(op1(e13,e11)) != op2(h8(e13),e23)
| spl28_111
| ~ spl28_347 ),
inference(forward_demodulation,[],[f1266,f3203]) ).
fof(f6385,plain,
( op2(e21,e23) != h8(op1(e13,e11))
| spl28_111
| ~ spl28_347 ),
inference(forward_demodulation,[],[f6381,f564]) ).
fof(f6388,plain,
( op2(e21,e23) != h8(e12)
| spl28_111
| ~ spl28_347
| ~ spl28_468 ),
inference(forward_demodulation,[],[f6385,f2837]) ).
fof(f6392,plain,
( e22 != op2(e21,e23)
| spl28_111
| ~ spl28_347
| ~ spl28_468 ),
inference(forward_demodulation,[],[f6388,f565]) ).
fof(f6395,plain,
( $false
| spl28_111
| ~ spl28_347
| ~ spl28_359
| ~ spl28_468 ),
inference(forward_subsumption_resolution,[],[f6392,f4718]) ).
fof(f6396,plain,
( spl28_111
| ~ spl28_347
| ~ spl28_359
| ~ spl28_468 ),
inference(avatar_contradiction_clause,[],[f6395]) ).
fof(f6397,plain,
( h8(op1(e12,e11)) != op2(h8(e12),e23)
| spl28_115
| ~ spl28_347 ),
inference(forward_demodulation,[],[f1278,f3203]) ).
fof(f6398,plain,
( op2(e22,e23) != h8(op1(e12,e11))
| spl28_115
| ~ spl28_347 ),
inference(forward_demodulation,[],[f6397,f565]) ).
fof(f6399,plain,
( op2(e22,e23) != h8(e13)
| spl28_115
| ~ spl28_347
| ~ spl28_475 ),
inference(forward_demodulation,[],[f6398,f2861]) ).
fof(f6400,plain,
( e21 != op2(e22,e23)
| spl28_115
| ~ spl28_347
| ~ spl28_475 ),
inference(forward_demodulation,[],[f6399,f564]) ).
fof(f6401,plain,
( $false
| spl28_115
| ~ spl28_347
| ~ spl28_475 ),
inference(forward_subsumption_resolution,[],[f6400,f532]) ).
fof(f6402,plain,
( spl28_115
| ~ spl28_347
| ~ spl28_475 ),
inference(avatar_contradiction_clause,[],[f6401]) ).
fof(f6403,plain,
( h8(op1(e11,e12)) != op2(h8(e11),e22)
| spl28_118 ),
inference(forward_demodulation,[],[f1287,f565]) ).
fof(f6405,plain,
( h8(op1(e11,e12)) != op2(e22,h5(e11))
| spl28_118 ),
inference(forward_demodulation,[],[f6403,f3076]) ).
fof(f6407,plain,
( op2(e22,e23) != h8(op1(e11,e12))
| spl28_118
| ~ spl28_371 ),
inference(forward_demodulation,[],[f6405,f3218]) ).
fof(f6409,plain,
( op2(e22,e23) != h8(e13)
| spl28_118
| ~ spl28_371
| ~ spl28_487 ),
inference(forward_demodulation,[],[f6407,f2900]) ).
fof(f6412,plain,
( e21 != op2(e22,e23)
| spl28_118
| ~ spl28_371
| ~ spl28_487 ),
inference(forward_demodulation,[],[f6409,f564]) ).
fof(f6413,plain,
( $false
| spl28_118
| ~ spl28_371
| ~ spl28_487 ),
inference(forward_subsumption_resolution,[],[f6412,f532]) ).
fof(f6414,plain,
( spl28_118
| ~ spl28_371
| ~ spl28_487 ),
inference(avatar_contradiction_clause,[],[f6413]) ).
fof(f6418,plain,
( e10 = e12
| ~ spl28_462
| ~ spl28_502 ),
inference(forward_demodulation,[],[f3633,f2949]) ).
fof(f6423,plain,
( $false
| ~ spl28_462
| ~ spl28_502 ),
inference(forward_subsumption_resolution,[],[f6418,f458]) ).
fof(f6424,plain,
( ~ spl28_462
| ~ spl28_502 ),
inference(avatar_contradiction_clause,[],[f6423]) ).
fof(f6443,plain,
( $false
| ~ spl28_466 ),
inference(forward_subsumption_resolution,[],[f2830,f2538]) ).
fof(f6444,plain,
~ spl28_466,
inference(avatar_contradiction_clause,[],[f6443]) ).
fof(f6500,plain,
( op1(e10,e12) = op1(e13,e13)
| ~ spl28_463 ),
inference(superposition,[],[f2806,f2821]) ).
fof(f6501,plain,
( e10 = op1(e10,e12)
| ~ spl28_463 ),
inference(forward_demodulation,[],[f6500,f531]) ).
fof(f6503,plain,
( spl28_502
| ~ spl28_463 ),
inference(avatar_split_clause,[],[f6501,f2820,f2948]) ).
fof(f6505,plain,
( op1(e11,e12) = op1(e12,e12)
| ~ spl28_464 ),
inference(superposition,[],[f2811,f2824]) ).
fof(f6509,plain,
( $false
| ~ spl28_464 ),
inference(forward_subsumption_resolution,[],[f6505,f390]) ).
fof(f6510,plain,
~ spl28_464,
inference(avatar_contradiction_clause,[],[f6509]) ).
fof(f6515,plain,
( spl28_495
| ~ spl28_462 ),
inference(avatar_split_clause,[],[f3515,f2802,f2926]) ).
fof(f6535,plain,
( spl28_487
| ~ spl28_465
| ~ spl28_475 ),
inference(avatar_split_clause,[],[f4236,f2860,f2826,f2899]) ).
fof(f6579,plain,
( op1(e10,e12) = op1(e13,e11)
| ~ spl28_465 ),
inference(superposition,[],[f2806,f2827]) ).
fof(f6585,plain,
( e12 = op1(e13,e11)
| ~ spl28_465
| ~ spl28_500 ),
inference(forward_demodulation,[],[f6579,f2943]) ).
fof(f6586,plain,
( spl28_468
| ~ spl28_465
| ~ spl28_500 ),
inference(avatar_split_clause,[],[f6585,f2942,f2826,f2836]) ).
fof(f6988,plain,
( op1(e12,e11) = op1(e13,op1(e11,e11))
| ~ spl28_468 ),
inference(superposition,[],[f128,f2837]) ).
fof(f6989,plain,
( op1(e12,e11) = op1(e13,e10)
| ~ spl28_415
| ~ spl28_468 ),
inference(forward_demodulation,[],[f6988,f2451]) ).
fof(f6990,plain,
( op1(e10,e13) = op1(e12,e11)
| ~ spl28_415
| ~ spl28_468 ),
inference(forward_demodulation,[],[f6989,f2805]) ).
fof(f7000,plain,
( e13 = op1(e12,e11)
| ~ spl28_415
| ~ spl28_468
| ~ spl28_495 ),
inference(forward_demodulation,[],[f6990,f2927]) ).
fof(f7004,plain,
( spl28_475
| ~ spl28_415
| ~ spl28_468
| ~ spl28_495 ),
inference(avatar_split_clause,[],[f7000,f2926,f2836,f2450,f2860]) ).
cnf(s77,plain,
( spl28_105
| spl28_106
| ~ spl28_107
| ~ spl28_109
| ~ spl28_110
| ~ spl28_111
| ~ spl28_112
| ~ spl28_113
| ~ spl28_114
| ~ spl28_115
| ~ spl28_116
| ~ spl28_117
| ~ spl28_118
| ~ spl28_119
| ~ spl28_120
| ~ spl28_121
| ~ spl28_122
| ~ spl28_123
| ~ spl28_124
| ~ spl28_130 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s227,plain,
( ~ spl28_105
| ~ spl28_347 ),
inference(sat_conversion,[],[f2146]) ).
cnf(s230,plain,
( ~ spl28_106
| ~ spl28_350 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s332,plain,
( spl28_451
| spl28_452
| spl28_453
| spl28_454 ),
inference(sat_conversion,[],[f2697]) ).
cnf(s337,plain,
( spl28_459
| spl28_460
| spl28_461
| spl28_462 ),
inference(sat_conversion,[],[f2804]) ).
cnf(s338,plain,
( spl28_463
| spl28_464
| spl28_465
| spl28_466 ),
inference(sat_conversion,[],[f2831]) ).
cnf(s349,plain,
( spl28_499
| spl28_500
| spl28_501
| spl28_502 ),
inference(sat_conversion,[],[f2950]) ).
cnf(s352,plain,
( spl28_340
| ~ spl28_507 ),
inference(sat_conversion,[],[f2981]) ).
cnf(s356,plain,
( spl28_344
| ~ spl28_508 ),
inference(sat_conversion,[],[f2992]) ).
cnf(s360,plain,
( spl28_26
| spl28_101
| spl28_507
| spl28_508 ),
inference(sat_conversion,[],[f3134]) ).
cnf(s364,plain,
( spl28_52
| spl28_101
| spl28_507
| spl28_508 ),
inference(sat_conversion,[],[f3142]) ).
cnf(s372,plain,
( spl28_409
| spl28_410
| spl28_412 ),
inference(sat_conversion,[],[f3151]) ).
cnf(s373,plain,
( spl28_409
| spl28_410
| spl28_415 ),
inference(sat_conversion,[],[f3152]) ).
cnf(s374,plain,
( spl28_409
| spl28_410
| spl28_416 ),
inference(sat_conversion,[],[f3153]) ).
cnf(s375,plain,
~ spl28_409,
inference(sat_conversion,[],[f3154]) ).
cnf(s376,plain,
~ spl28_410,
inference(sat_conversion,[],[f3155]) ).
cnf(s381,plain,
( spl28_126
| spl28_129
| spl28_347
| spl28_351 ),
inference(sat_conversion,[],[f3204]) ).
cnf(s382,plain,
( spl28_152
| spl28_155
| spl28_355
| spl28_359 ),
inference(sat_conversion,[],[f3209]) ).
cnf(s384,plain,
( spl28_204
| spl28_207
| spl28_371
| spl28_375 ),
inference(sat_conversion,[],[f3219]) ).
cnf(s386,plain,
( spl28_230
| spl28_233
| spl28_379
| spl28_383 ),
inference(sat_conversion,[],[f3225]) ).
cnf(s387,plain,
( spl28_256
| spl28_259
| spl28_387
| spl28_391 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s392,plain,
spl28_109,
inference(sat_conversion,[],[f3284]) ).
cnf(s405,plain,
~ spl28_451,
inference(sat_conversion,[],[f3443]) ).
cnf(s406,plain,
~ spl28_452,
inference(sat_conversion,[],[f3452]) ).
cnf(s410,plain,
~ spl28_459,
inference(sat_conversion,[],[f3466]) ).
cnf(s413,plain,
( ~ spl28_412
| ~ spl28_460 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s416,plain,
( ~ spl28_415
| ~ spl28_461 ),
inference(sat_conversion,[],[f3486]) ).
cnf(s417,plain,
( ~ spl28_462
| spl28_493 ),
inference(sat_conversion,[],[f3492]) ).
cnf(s424,plain,
( ~ spl28_462
| spl28_480 ),
inference(sat_conversion,[],[f3526]) ).
cnf(s425,plain,
( ~ spl28_480
| spl28_484 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s430,plain,
~ spl28_101,
inference(sat_conversion,[],[f3572]) ).
cnf(s435,plain,
( ~ spl28_462
| ~ spl28_499 ),
inference(sat_conversion,[],[f3636]) ).
cnf(s441,plain,
( ~ spl28_462
| spl28_505 ),
inference(sat_conversion,[],[f3773]) ).
cnf(s484,plain,
( ~ spl28_52
| ~ spl28_453 ),
inference(sat_conversion,[],[f4264]) ).
cnf(s487,plain,
( ~ spl28_26
| ~ spl28_155
| ~ spl28_454 ),
inference(sat_conversion,[],[f4282]) ).
cnf(s489,plain,
( ~ spl28_52
| ~ spl28_233
| ~ spl28_454 ),
inference(sat_conversion,[],[f4333]) ).
cnf(s491,plain,
( ~ spl28_26
| ~ spl28_129
| ~ spl28_454 ),
inference(sat_conversion,[],[f4349]) ).
cnf(s506,plain,
( ~ spl28_259
| ~ spl28_285
| ~ spl28_454 ),
inference(sat_conversion,[],[f4425]) ).
cnf(s509,plain,
( ~ spl28_52
| ~ spl28_207
| ~ spl28_454 ),
inference(sat_conversion,[],[f4435]) ).
cnf(s523,plain,
( ~ spl28_52
| ~ spl28_379
| ~ spl28_454 ),
inference(sat_conversion,[],[f4510]) ).
cnf(s525,plain,
( ~ spl28_26
| ~ spl28_351
| ~ spl28_454 ),
inference(sat_conversion,[],[f4523]) ).
cnf(s528,plain,
( ~ spl28_285
| ~ spl28_387
| ~ spl28_454 ),
inference(sat_conversion,[],[f4530]) ).
cnf(s534,plain,
( ~ spl28_52
| spl28_112
| ~ spl28_230
| ~ spl28_495 ),
inference(sat_conversion,[],[f4569]) ).
cnf(s535,plain,
( ~ spl28_26
| ~ spl28_126
| ~ spl28_152
| ~ spl28_454 ),
inference(sat_conversion,[],[f4579]) ).
cnf(s540,plain,
( ~ spl28_26
| ~ spl28_152
| ~ spl28_347
| ~ spl28_454 ),
inference(sat_conversion,[],[f4620]) ).
cnf(s548,plain,
( ~ spl28_26
| ~ spl28_355
| ~ spl28_454 ),
inference(sat_conversion,[],[f4701]) ).
cnf(s575,plain,
~ spl28_340,
inference(sat_conversion,[],[f4870]) ).
cnf(s584,plain,
~ spl28_344,
inference(sat_conversion,[],[f4924]) ).
cnf(s590,plain,
spl28_113,
inference(sat_conversion,[],[f4975]) ).
cnf(s628,plain,
( ~ spl28_52
| spl28_122
| ~ spl28_454
| ~ spl28_500 ),
inference(sat_conversion,[],[f5247]) ).
cnf(s633,plain,
( ~ spl28_52
| spl28_116
| ~ spl28_454
| ~ spl28_484 ),
inference(sat_conversion,[],[f5286]) ).
cnf(s636,plain,
( ~ spl28_52
| spl28_117
| ~ spl28_454
| ~ spl28_484 ),
inference(sat_conversion,[],[f5298]) ).
cnf(s637,plain,
( ~ spl28_52
| spl28_120
| ~ spl28_230
| ~ spl28_493 ),
inference(sat_conversion,[],[f5309]) ).
cnf(s638,plain,
( ~ spl28_52
| spl28_121
| ~ spl28_454
| ~ spl28_495 ),
inference(sat_conversion,[],[f5316]) ).
cnf(s639,plain,
( ~ spl28_52
| spl28_124
| ~ spl28_416
| ~ spl28_454 ),
inference(sat_conversion,[],[f5323]) ).
cnf(s640,plain,
( ~ spl28_26
| ~ spl28_52
| spl28_114
| ~ spl28_412 ),
inference(sat_conversion,[],[f5330]) ).
cnf(s641,plain,
( ~ spl28_52
| spl28_130 ),
inference(sat_conversion,[],[f5334]) ).
cnf(s648,plain,
( ~ spl28_52
| ~ spl28_383
| ~ spl28_454 ),
inference(sat_conversion,[],[f5511]) ).
cnf(s666,plain,
( ~ spl28_52
| ~ spl28_126
| ~ spl28_359 ),
inference(sat_conversion,[],[f5782]) ).
cnf(s667,plain,
spl28_107,
inference(sat_conversion,[],[f5785]) ).
cnf(s669,plain,
( spl28_126
| ~ spl28_256
| ~ spl28_359 ),
inference(sat_conversion,[],[f5797]) ).
cnf(s675,plain,
( ~ spl28_285
| ~ spl28_347
| ~ spl28_391
| ~ spl28_454 ),
inference(sat_conversion,[],[f5875]) ).
cnf(s677,plain,
( ~ spl28_52
| spl28_123
| ~ spl28_347
| ~ spl28_454
| ~ spl28_505 ),
inference(sat_conversion,[],[f5884]) ).
cnf(s680,plain,
( ~ spl28_52
| ~ spl28_204
| spl28_285 ),
inference(sat_conversion,[],[f5896]) ).
cnf(s683,plain,
( ~ spl28_52
| spl28_119
| ~ spl28_347
| ~ spl28_415 ),
inference(sat_conversion,[],[f5931]) ).
cnf(s687,plain,
spl28_350,
inference(sat_conversion,[],[f5945]) ).
cnf(s709,plain,
( ~ spl28_462
| ~ spl28_501 ),
inference(sat_conversion,[],[f6102]) ).
cnf(s727,plain,
( ~ spl28_52
| ~ spl28_375 ),
inference(sat_conversion,[],[f6363]) ).
cnf(s729,plain,
( spl28_110
| ~ spl28_347
| ~ spl28_371
| ~ spl28_465 ),
inference(sat_conversion,[],[f6370]) ).
cnf(s732,plain,
( spl28_111
| ~ spl28_347
| ~ spl28_359
| ~ spl28_468 ),
inference(sat_conversion,[],[f6396]) ).
cnf(s733,plain,
( spl28_115
| ~ spl28_347
| ~ spl28_475 ),
inference(sat_conversion,[],[f6402]) ).
cnf(s735,plain,
( spl28_118
| ~ spl28_371
| ~ spl28_487 ),
inference(sat_conversion,[],[f6414]) ).
cnf(s736,plain,
( ~ spl28_462
| ~ spl28_502 ),
inference(sat_conversion,[],[f6424]) ).
cnf(s740,plain,
~ spl28_466,
inference(sat_conversion,[],[f6444]) ).
cnf(s751,plain,
( ~ spl28_463
| spl28_502 ),
inference(sat_conversion,[],[f6503]) ).
cnf(s754,plain,
~ spl28_464,
inference(sat_conversion,[],[f6510]) ).
cnf(s757,plain,
( ~ spl28_462
| spl28_495 ),
inference(sat_conversion,[],[f6515]) ).
cnf(s758,plain,
( ~ spl28_465
| ~ spl28_475
| spl28_487 ),
inference(sat_conversion,[],[f6535]) ).
cnf(s764,plain,
( ~ spl28_465
| spl28_468
| ~ spl28_500 ),
inference(sat_conversion,[],[f6586]) ).
cnf(s794,plain,
( ~ spl28_415
| ~ spl28_468
| spl28_475
| ~ spl28_495 ),
inference(sat_conversion,[],[f7004]) ).
cnf(s795,plain,
spl28_416,
inference(rat,[],[s374,s376,s375]) ).
cnf(s797,plain,
spl28_415,
inference(rat,[],[s373,s376,s375]) ).
cnf(s798,plain,
~ spl28_461,
inference(rat,[],[s416,s797]) ).
cnf(s799,plain,
spl28_412,
inference(rat,[],[s372,s376,s375]) ).
cnf(s800,plain,
~ spl28_460,
inference(rat,[],[s413,s799]) ).
cnf(s802,plain,
( spl28_52
| spl28_507
| spl28_508 ),
inference(rat,[],[s364,s430]) ).
cnf(s803,plain,
( spl28_26
| spl28_507
| spl28_508 ),
inference(rat,[],[s360,s430]) ).
cnf(s804,plain,
~ spl28_508,
inference(rat,[],[s356,s584]) ).
cnf(s805,plain,
~ spl28_507,
inference(rat,[],[s352,s575]) ).
cnf(s807,plain,
spl28_52,
inference(rat,[],[s802,s804,s805]) ).
cnf(s808,plain,
spl28_26,
inference(rat,[],[s803,s804,s805]) ).
cnf(s817,plain,
~ spl28_375,
inference(rat,[],[s727,s807]) ).
cnf(s818,plain,
spl28_130,
inference(rat,[],[s641,s807]) ).
cnf(s823,plain,
~ spl28_453,
inference(rat,[],[s484,s807]) ).
cnf(s828,plain,
spl28_114,
inference(rat,[],[s640,s799,s807,s808]) ).
cnf(s837,plain,
( spl28_463
| spl28_465 ),
inference(rat,[],[s338,s740,s754]) ).
cnf(s838,plain,
spl28_462,
inference(rat,[],[s337,s798,s800,s410]) ).
cnf(s839,plain,
spl28_495,
inference(rat,[],[s757,s838]) ).
cnf(s840,plain,
~ spl28_502,
inference(rat,[],[s736,s838]) ).
cnf(s841,plain,
~ spl28_501,
inference(rat,[],[s709,s838]) ).
cnf(s842,plain,
spl28_505,
inference(rat,[],[s441,s838]) ).
cnf(s843,plain,
~ spl28_499,
inference(rat,[],[s435,s838]) ).
cnf(s844,plain,
spl28_480,
inference(rat,[],[s424,s838]) ).
cnf(s846,plain,
spl28_493,
inference(rat,[],[s417,s838]) ).
cnf(s847,plain,
~ spl28_463,
inference(rat,[],[s751,s840]) ).
cnf(s850,plain,
spl28_500,
inference(rat,[],[s349,s840,s841,s843]) ).
cnf(s851,plain,
spl28_484,
inference(rat,[],[s425,s844]) ).
cnf(s857,plain,
spl28_465,
inference(rat,[],[s837,s847]) ).
cnf(s859,plain,
spl28_468,
inference(rat,[],[s764,s850,s857]) ).
cnf(s861,plain,
spl28_475,
inference(rat,[],[s794,s839,s797,s859]) ).
cnf(s863,plain,
spl28_487,
inference(rat,[],[s758,s857,s861]) ).
cnf(s865,plain,
spl28_454,
inference(rat,[],[s332,s823,s406,s405]) ).
cnf(s893,plain,
~ spl28_383,
inference(rat,[],[s648,s807,s865]) ).
cnf(s894,plain,
spl28_124,
inference(rat,[],[s639,s807,s795,s865]) ).
cnf(s895,plain,
spl28_121,
inference(rat,[],[s638,s839,s807,s865]) ).
cnf(s896,plain,
spl28_117,
inference(rat,[],[s636,s851,s807,s865]) ).
cnf(s897,plain,
spl28_116,
inference(rat,[],[s633,s851,s807,s865]) ).
cnf(s900,plain,
spl28_122,
inference(rat,[],[s628,s850,s807,s865]) ).
cnf(s906,plain,
~ spl28_379,
inference(rat,[],[s523,s807,s865]) ).
cnf(s907,plain,
~ spl28_207,
inference(rat,[],[s509,s807,s865]) ).
cnf(s908,plain,
~ spl28_233,
inference(rat,[],[s489,s807,s865]) ).
cnf(s917,plain,
~ spl28_355,
inference(rat,[],[s548,s808,s865]) ).
cnf(s918,plain,
~ spl28_351,
inference(rat,[],[s525,s808,s865]) ).
cnf(s919,plain,
~ spl28_129,
inference(rat,[],[s491,s808,s865]) ).
cnf(s920,plain,
~ spl28_155,
inference(rat,[],[s487,s808,s865]) ).
cnf(s921,plain,
spl28_230,
inference(rat,[],[s386,s893,s906,s908]) ).
cnf(s926,plain,
spl28_120,
inference(rat,[],[s637,s846,s807,s921]) ).
cnf(s928,plain,
spl28_112,
inference(rat,[],[s534,s839,s807,s921]) ).
cnf(s930,plain,
~ spl28_106,
inference(rat,[],[s230,s687]) ).
cnf(s1034,plain,
( spl28_105
| ~ spl28_110
| ~ spl28_111
| ~ spl28_115
| ~ spl28_118
| ~ spl28_119
| ~ spl28_123 ),
inference(rat,[],[s77,s818,s894,s900,s895,s926,s896,s897,s828,s590,s928,s392,s667,s930]) ).
cnf(s1088,plain,
~ spl28_126,
inference(rat,[],[s382,s535,s666,s917,s920,s808,s865,s807]) ).
cnf(s1089,plain,
spl28_347,
inference(rat,[],[s381,s918,s919,s1088]) ).
cnf(s1090,plain,
spl28_115,
inference(rat,[],[s733,s861,s1089]) ).
cnf(s1092,plain,
spl28_119,
inference(rat,[],[s683,s797,s807,s1089]) ).
cnf(s1093,plain,
spl28_123,
inference(rat,[],[s677,s842,s865,s807,s1089]) ).
cnf(s1094,plain,
~ spl28_152,
inference(rat,[],[s540,s865,s808,s1089]) ).
cnf(s1095,plain,
~ spl28_105,
inference(rat,[],[s227,s1089]) ).
cnf(s1097,plain,
spl28_359,
inference(rat,[],[s382,s920,s917,s1094]) ).
cnf(s1116,plain,
~ spl28_256,
inference(rat,[],[s669,s1088,s1097]) ).
cnf(s1117,plain,
spl28_111,
inference(rat,[],[s732,s859,s1089,s1097]) ).
cnf(s1119,plain,
~ spl28_285,
inference(rat,[],[s387,s506,s528,s675,s1116,s865,s1089]) ).
cnf(s1120,plain,
~ spl28_204,
inference(rat,[],[s680,s807,s1119]) ).
cnf(s1121,plain,
spl28_371,
inference(rat,[],[s384,s817,s907,s1120]) ).
cnf(s1123,plain,
spl28_118,
inference(rat,[],[s735,s863,s1121]) ).
cnf(s1126,plain,
spl28_110,
inference(rat,[],[s729,s857,s1089,s1121]) ).
cnf(s1128,plain,
$false,
inference(rat,[],[s1034,s1093,s1092,s1117,s1090,s1095,s1123,s1126]) ).
fof(f7005,plain,
$false,
inference(avatar_sat_refutation,[],[s1128]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG015+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n018.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 19:19:55 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.49/1.06 % (3683908)Detected formulas, will run a generic FOF schedule.
% 4.49/1.06 % (3683919)dis-21_1_sil=8000:lcm=predicate:random_seed=3564200675:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.49/1.06 % (3683919)Refutation not found, incomplete strategy
% 4.49/1.06 % (3683919)------------------------------
% 4.49/1.06 % (3683919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.49/1.06 % (3683919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.49/1.06 % (3683919)CaDiCaL version: 2.1.3
% 4.49/1.06 % (3683919)Termination reason: Refutation not found, incomplete strategy
% 4.49/1.06 % (3683919)Time elapsed: 0.016 s
% 4.49/1.06 % (3683919)Peak memory usage: 90 MB
% 4.49/1.06 % (3683919)Instructions burned: 59 (million)
% 4.49/1.06 % (3683913)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=719526026:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.49/1.06 % (3683916)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4011852642:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.49/1.06 % (3683915)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1840425560:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.49/1.06 % (3683917)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1986796484:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.49/1.06 % (3683918)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2913901908:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.49/1.06 % (3683914)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3320347255:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.49/1.06 % (3683916)Instruction limit reached!
% 4.49/1.06 % (3683916)------------------------------
% 4.49/1.06 % (3683916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.49/1.06 % (3683916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.49/1.06 % (3683916)CaDiCaL version: 2.1.3
% 4.49/1.06 % (3683916)Termination reason: Instruction limit
% 4.49/1.06 % (3683916)Termination phase: Saturation
% 4.49/1.06 % (3683916)Time elapsed: 0.051 s
% 4.49/1.06 % (3683916)Peak memory usage: 90 MB
% 4.49/1.06 % (3683916)Instructions burned: 111 (million)
% 4.49/1.06 % (3683917)Instruction limit reached!
% 4.49/1.06 % (3683917)------------------------------
% 4.49/1.06 % (3683917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.49/1.06 % (3683917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.49/1.06 % (3683917)CaDiCaL version: 2.1.3
% 4.49/1.06 % (3683917)Termination reason: Instruction limit
% 4.49/1.06 % (3683917)Termination phase: Saturation
% 4.49/1.06 % (3683917)Time elapsed: 0.052 s
% 4.49/1.06 % (3683917)Peak memory usage: 88 MB
% 4.49/1.06 % (3683917)Instructions burned: 122 (million)
% 4.49/1.06 % (3683918)Instruction limit reached!
% 4.49/1.06 % (3683918)------------------------------
% 4.49/1.06 % (3683918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.49/1.06 % (3683918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.49/1.06 % (3683918)CaDiCaL version: 2.1.3
% 4.49/1.06 % (3683918)Termination reason: Instruction limit
% 4.49/1.06 % (3683918)Termination phase: Saturation
% 4.49/1.06 % (3683918)Time elapsed: 0.067 s
% 4.49/1.06 % (3683918)Peak memory usage: 90 MB
% 4.49/1.06 % (3683918)Instructions burned: 140 (million)
% 4.49/1.06 % (3683919)------------------------------
% 4.49/1.06 % (3683919)------------------------------
% 4.49/1.06 % (3683928)lrs+10_1_sil=32000:urr=on:br=off:random_seed=692841584:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.49/1.06 % (3683929)lrs+1011_1_sil=32000:sp=occurrence:random_seed=356531916:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.49/1.06 % (3683927)lrs+10_1_sil=8000:sp=occurrence:random_seed=2954463256:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.49/1.06 % (3683930)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=44269805:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 6.00/1.31 % (3683928)Instruction limit reached!
% 6.00/1.31 % (3683928)------------------------------
% 6.00/1.31 % (3683928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.00/1.31 % (3683928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.00/1.31 % (3683928)CaDiCaL version: 2.1.3
% 6.00/1.31 % (3683928)Termination reason: Instruction limit
% 6.00/1.31 % (3683928)Termination phase: Saturation
% 6.00/1.31 % (3683928)Time elapsed: 0.063 s
% 6.00/1.31 % (3683928)Peak memory usage: 89 MB
% 6.00/1.31 % (3683928)Instructions burned: 157 (million)
% 6.00/1.31 % (3683930)Instruction limit reached!
% 6.00/1.31 % (3683930)------------------------------
% 6.00/1.31 % (3683930)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.00/1.31 % (3683930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.00/1.31 % (3683930)CaDiCaL version: 2.1.3
% 6.00/1.31 % (3683930)Termination reason: Instruction limit
% 6.00/1.31 % (3683930)Termination phase: Saturation
% 6.00/1.31 % (3683930)Time elapsed: 0.070 s
% 6.00/1.31 % (3683930)Peak memory usage: 91 MB
% 6.00/1.31 % (3683930)Instructions burned: 249 (million)
% 6.00/1.31 % (3683927)Instruction limit reached!
% 6.00/1.31 % (3683927)------------------------------
% 6.00/1.31 % (3683927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.00/1.31 % (3683927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.00/1.31 % (3683927)CaDiCaL version: 2.1.3
% 6.00/1.31 % (3683927)Termination reason: Instruction limit
% 6.00/1.31 % (3683927)Termination phase: Saturation
% 6.00/1.31 % (3683927)Time elapsed: 0.120 s
% 6.00/1.31 % (3683927)Peak memory usage: 90 MB
% 6.00/1.31 % (3683927)Instructions burned: 285 (million)
% 6.00/1.31 % (3683929)Instruction limit reached!
% 6.00/1.31 % (3683929)------------------------------
% 6.00/1.31 % (3683929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.00/1.31 % (3683929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.00/1.31 % (3683929)CaDiCaL version: 2.1.3
% 6.00/1.31 % (3683929)Termination reason: Instruction limit
% 6.00/1.31 % (3683929)Termination phase: Saturation
% 6.00/1.31 % (3683929)Time elapsed: 0.136 s
% 6.00/1.31 % (3683929)Peak memory usage: 90 MB
% 6.00/1.31 % (3683929)Instructions burned: 327 (million)
% 6.00/1.31 [W928 19:19:56.702094231 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.00/1.31 [W928 19:19:56.702133148 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.00/1.31 [W928 19:19:56.702170578 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.00/1.31 [W928 19:19:56.702183035 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.00/1.31 [W928 19:19:56.702211645 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.00/1.31 [W928 19:19:56.702222718 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 6.00/1.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 6.00/1.31 [W928 19:19:56.702727126 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702733979 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702763416 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702766793 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702811760 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702813260 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702824986 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702834726 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702850680 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702861170 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702861107 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.702872083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 % (3683935)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3618118109:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 7.94/1.73 % (3683936)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2554102673:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 7.94/1.73 % (3683937)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3612672948:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 7.94/1.73 % (3683938)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1155011082:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 7.94/1.73 % (3683935)Instruction limit reached!
% 7.94/1.73 % (3683935)------------------------------
% 7.94/1.73 % (3683935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/1.73 % (3683935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.73 % (3683935)CaDiCaL version: 2.1.3
% 7.94/1.73 % (3683935)Termination reason: Instruction limit
% 7.94/1.73 % (3683935)Termination phase: Saturation
% 7.94/1.73 % (3683935)Time elapsed: 0.107 s
% 7.94/1.73 % (3683935)Peak memory usage: 89 MB
% 7.94/1.73 % (3683935)Instructions burned: 295 (million)
% 7.94/1.73 % (3683937)Instruction limit reached!
% 7.94/1.73 % (3683937)------------------------------
% 7.94/1.73 % (3683937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/1.73 % (3683937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.73 % (3683937)CaDiCaL version: 2.1.3
% 7.94/1.73 % (3683937)Termination reason: Instruction limit
% 7.94/1.73 % (3683937)Termination phase: Saturation
% 7.94/1.73 % (3683937)Time elapsed: 0.056 s
% 7.94/1.73 % (3683937)Peak memory usage: 91 MB
% 7.94/1.73 % (3683937)Instructions burned: 113 (million)
% 7.94/1.73 % (3683938)Refutation not found, incomplete strategy
% 7.94/1.73 % (3683938)------------------------------
% 7.94/1.73 % (3683938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/1.73 % (3683938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.73 % (3683938)CaDiCaL version: 2.1.3
% 7.94/1.73 % (3683938)Termination reason: Refutation not found, incomplete strategy
% 7.94/1.73 % (3683938)Time elapsed: 0.038 s
% 7.94/1.73 % (3683938)Peak memory usage: 88 MB
% 7.94/1.73 % (3683938)Instructions burned: 95 (million)
% 7.94/1.73 [W928 19:19:56.948756942 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.948798771 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.948820710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.948827567 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.948842110 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 [W928 19:19:56.948848240 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 7.94/1.73 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 7.94/1.73 % (3683943)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3791406868:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 7.94/1.73 % (3683944)lrs+10_1_sil=8000:sp=occurrence:random_seed=1089543317:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 7.94/1.73 % (3683943)Instruction limit reached!
% 7.94/1.73 % (3683943)------------------------------
% 7.94/1.73 % (3683943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/1.73 % (3683943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.73 % (3683943)CaDiCaL version: 2.1.3
% 7.94/1.73 % (3683943)Termination reason: Instruction limit
% 7.94/1.73 % (3683943)Termination phase: Property scanning
% 7.94/1.73 % (3683943)Time elapsed: 0.039 s
% 7.94/1.73 % (3683943)Peak memory usage: 86 MB
% 7.94/1.73 % (3683943)Instructions burned: 115 (million)
% 7.94/1.73 % (3683938)------------------------------
% 7.94/1.73 % (3683938)------------------------------
% 7.94/1.73 % (3683914)First to succeed.
% 7.94/1.73 % (3683914)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3683908"
% 7.94/1.73 % (3683947)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4114917235:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 7.94/1.73 % (3683948)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1350637316:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 7.94/1.73 % (3683947)Refutation not found, incomplete strategy
% 7.94/1.73 % (3683947)------------------------------
% 7.94/1.73 % (3683947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/1.73 % (3683947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.73 % (3683947)CaDiCaL version: 2.1.3
% 7.94/1.73 % (3683947)Termination reason: Refutation not found, incomplete strategy
% 7.94/1.73 % (3683947)Time elapsed: 0.083 s
% 7.94/1.73 % (3683947)Peak memory usage: 89 MB
% 7.94/1.73 % (3683947)Instructions burned: 211 (million)
% 7.94/1.73 % (3683944)Also succeeded, but the first one will report.
% 7.94/1.73 % (3683915)Refutation not found, incomplete strategy
% 7.94/1.73 % (3683915)------------------------------
% 7.94/1.73 % (3683915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/1.73 % (3683915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.73 % (3683915)CaDiCaL version: 2.1.3
% 7.94/1.73 % (3683915)Termination reason: Refutation not found, incomplete strategy
% 7.94/1.73 % (3683915)Time elapsed: 1.047 s
% 7.94/1.73 % (3683915)Peak memory usage: 133 MB
% 7.94/1.73 % (3683915)Instructions burned: 1955 (million)
% 7.94/1.73 % (3683914)Refutation found. Thanks to Tanya!
% 7.94/1.73 % SZS status Theorem for theBenchmark
% 7.94/1.73 % SZS output start Proof for theBenchmark
% See solution above
% 9.60/1.92 % (3683914)------------------------------
% 9.60/1.92 % (3683914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.60/1.92 % (3683914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/1.92 % (3683914)CaDiCaL version: 2.1.3
% 9.60/1.92 % (3683914)Termination reason: Refutation
% 9.60/1.92 % (3683914)Time elapsed: 0.873 s
% 9.60/1.92 % (3683914)Peak memory usage: 135 MB
% 9.60/1.92 % (3683914)Instructions burned: 1403 (million)
% 9.60/1.92 % (3683914)------------------------------
% 9.60/1.92 % (3683914)------------------------------
% 9.60/1.92 % (3683908)Success in time 1.308 s
% 9.60/1.92 % Vampire exiting
%------------------------------------------------------------------------------