%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG206+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:29:45 AM UTC 2026
% Result : Theorem 0.87s 0.40s
% Output : Refutation 0.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 13
% Syntax : Number of formulae : 117 ( 32 unt; 9 def)
% Number of atoms : 1168 (1040 equ)
% Maximal formula atoms : 210 ( 9 avg)
% Number of connectives : 1160 ( 109 ~; 426 |; 614 &)
% ( 9 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 126 ( 8 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 10 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( e20 != e21
& e20 != e22
& e20 != e23
& e20 != e24
& e20 != e25
& e20 != e26
& e21 != e22
& e21 != e23
& e21 != e24
& e21 != e25
& e21 != e26
& e22 != e23
& e22 != e24
& e22 != e25
& e22 != e26
& e23 != e24
& e23 != e25
& e23 != e26
& e24 != e25
& e24 != e26
& e25 != e26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f4,axiom,
( op1(e10,e10) = e10
& op1(e10,e11) = e13
& op1(e10,e12) = e11
& op1(e10,e13) = e12
& op1(e10,e14) = e16
& op1(e10,e15) = e14
& op1(e10,e16) = e15
& op1(e11,e10) = e13
& op1(e11,e11) = e11
& op1(e11,e12) = e16
& op1(e11,e13) = e15
& op1(e11,e14) = e12
& op1(e11,e15) = e10
& op1(e11,e16) = e14
& op1(e12,e10) = e11
& op1(e12,e11) = e16
& op1(e12,e12) = e12
& op1(e12,e13) = e14
& op1(e12,e14) = e15
& op1(e12,e15) = e13
& op1(e12,e16) = e10
& op1(e13,e10) = e12
& op1(e13,e11) = e15
& op1(e13,e12) = e14
& op1(e13,e13) = e13
& op1(e13,e14) = e10
& op1(e13,e15) = e16
& op1(e13,e16) = e11
& op1(e14,e10) = e16
& op1(e14,e11) = e12
& op1(e14,e12) = e15
& op1(e14,e13) = e10
& op1(e14,e14) = e14
& op1(e14,e15) = e11
& op1(e14,e16) = e13
& op1(e15,e10) = e14
& op1(e15,e11) = e10
& op1(e15,e12) = e13
& op1(e15,e13) = e16
& op1(e15,e14) = e11
& op1(e15,e15) = e15
& op1(e15,e16) = e12
& op1(e16,e10) = e15
& op1(e16,e11) = e14
& op1(e16,e12) = e10
& op1(e16,e13) = e11
& op1(e16,e14) = e13
& op1(e16,e15) = e12
& op1(e16,e16) = e16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( op2(e20,e20) = e22
& op2(e20,e21) = e20
& op2(e20,e22) = e21
& op2(e20,e23) = e25
& op2(e20,e24) = e23
& op2(e20,e25) = e24
& op2(e20,e26) = e26
& op2(e21,e20) = e20
& op2(e21,e21) = e26
& op2(e21,e22) = e24
& op2(e21,e23) = e21
& op2(e21,e24) = e25
& op2(e21,e25) = e22
& op2(e21,e26) = e23
& op2(e22,e20) = e21
& op2(e22,e21) = e24
& op2(e22,e22) = e23
& op2(e22,e23) = e26
& op2(e22,e24) = e20
& op2(e22,e25) = e25
& op2(e22,e26) = e22
& op2(e23,e20) = e25
& op2(e23,e21) = e21
& op2(e23,e22) = e26
& op2(e23,e23) = e20
& op2(e23,e24) = e22
& op2(e23,e25) = e23
& op2(e23,e26) = e24
& op2(e24,e20) = e23
& op2(e24,e21) = e25
& op2(e24,e22) = e20
& op2(e24,e23) = e22
& op2(e24,e24) = e24
& op2(e24,e25) = e26
& op2(e24,e26) = e21
& op2(e25,e20) = e24
& op2(e25,e21) = e22
& op2(e25,e22) = e25
& op2(e25,e23) = e23
& op2(e25,e24) = e26
& op2(e25,e25) = e21
& op2(e25,e26) = e20
& op2(e26,e20) = e26
& op2(e26,e21) = e23
& op2(e26,e22) = e22
& op2(e26,e23) = e24
& op2(e26,e24) = e21
& op2(e26,e25) = e20
& op2(e26,e26) = e25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,conjecture,
( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24
| h(e10) = e25
| h(e10) = e26 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24
| h(e11) = e25
| h(e11) = e26 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24
| h(e12) = e25
| h(e12) = e26 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24
| h(e13) = e25
| h(e13) = e26 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24
| h(e14) = e25
| h(e14) = e26 )
& ( h(e15) = e20
| h(e15) = e21
| h(e15) = e22
| h(e15) = e23
| h(e15) = e24
| h(e15) = e25
| h(e15) = e26 )
& ( h(e16) = e20
| h(e16) = e21
| h(e16) = e22
| h(e16) = e23
| h(e16) = e24
| h(e16) = e25
| h(e16) = e26 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14
| j(e20) = e15
| j(e20) = e16 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14
| j(e21) = e15
| j(e21) = e16 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14
| j(e22) = e15
| j(e22) = e16 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14
| j(e23) = e15
| j(e23) = e16 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14
| j(e24) = e15
| j(e24) = e16 )
& ( j(e25) = e10
| j(e25) = e11
| j(e25) = e12
| j(e25) = e13
| j(e25) = e14
| j(e25) = e15
| j(e25) = e16 )
& ( j(e26) = e10
| j(e26) = e11
| j(e26) = e12
| j(e26) = e13
| j(e26) = e14
| j(e26) = e15
| j(e26) = e16 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e16)) = op2(h(e10),h(e16))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e16)) = op2(h(e11),h(e16))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e16)) = op2(h(e12),h(e16))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e16)) = op2(h(e13),h(e16))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e16)) = op2(h(e16),h(e16))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e26)) = op1(j(e20),j(e26))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e26)) = op1(j(e21),j(e26))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e26)) = op1(j(e22),j(e26))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e26)) = op1(j(e23),j(e26))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& h(j(e25)) = e25
& h(j(e26)) = e26
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& j(h(e15)) = e15
& j(h(e16)) = e16 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f7,negated_conjecture,
~ ( ( ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24
| h(e10) = e25
| h(e10) = e26 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24
| h(e11) = e25
| h(e11) = e26 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24
| h(e12) = e25
| h(e12) = e26 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24
| h(e13) = e25
| h(e13) = e26 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24
| h(e14) = e25
| h(e14) = e26 )
& ( h(e15) = e20
| h(e15) = e21
| h(e15) = e22
| h(e15) = e23
| h(e15) = e24
| h(e15) = e25
| h(e15) = e26 )
& ( h(e16) = e20
| h(e16) = e21
| h(e16) = e22
| h(e16) = e23
| h(e16) = e24
| h(e16) = e25
| h(e16) = e26 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14
| j(e20) = e15
| j(e20) = e16 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14
| j(e21) = e15
| j(e21) = e16 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14
| j(e22) = e15
| j(e22) = e16 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14
| j(e23) = e15
| j(e23) = e16 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14
| j(e24) = e15
| j(e24) = e16 )
& ( j(e25) = e10
| j(e25) = e11
| j(e25) = e12
| j(e25) = e13
| j(e25) = e14
| j(e25) = e15
| j(e25) = e16 )
& ( j(e26) = e10
| j(e26) = e11
| j(e26) = e12
| j(e26) = e13
| j(e26) = e14
| j(e26) = e15
| j(e26) = e16 ) )
=> ~ ( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e16)) = op2(h(e10),h(e16))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e16)) = op2(h(e11),h(e16))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e16)) = op2(h(e12),h(e16))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e16)) = op2(h(e13),h(e16))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e16)) = op2(h(e16),h(e16))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e26)) = op1(j(e20),j(e26))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e26)) = op1(j(e21),j(e26))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e26)) = op1(j(e22),j(e26))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e26)) = op1(j(e23),j(e26))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& h(j(e25)) = e25
& h(j(e26)) = e26
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& j(h(e15)) = e15
& j(h(e16)) = e16 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e16)) = op2(h(e10),h(e16))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e16)) = op2(h(e11),h(e16))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e16)) = op2(h(e12),h(e16))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e16)) = op2(h(e13),h(e16))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e16)) = op2(h(e16),h(e16))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e26)) = op1(j(e20),j(e26))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e26)) = op1(j(e21),j(e26))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e26)) = op1(j(e22),j(e26))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e26)) = op1(j(e23),j(e26))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& h(j(e25)) = e25
& h(j(e26)) = e26
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& j(h(e15)) = e15
& j(h(e16)) = e16
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24
| h(e10) = e25
| h(e10) = e26 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24
| h(e11) = e25
| h(e11) = e26 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24
| h(e12) = e25
| h(e12) = e26 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24
| h(e13) = e25
| h(e13) = e26 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24
| h(e14) = e25
| h(e14) = e26 )
& ( h(e15) = e20
| h(e15) = e21
| h(e15) = e22
| h(e15) = e23
| h(e15) = e24
| h(e15) = e25
| h(e15) = e26 )
& ( h(e16) = e20
| h(e16) = e21
| h(e16) = e22
| h(e16) = e23
| h(e16) = e24
| h(e16) = e25
| h(e16) = e26 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14
| j(e20) = e15
| j(e20) = e16 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14
| j(e21) = e15
| j(e21) = e16 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14
| j(e22) = e15
| j(e22) = e16 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14
| j(e23) = e15
| j(e23) = e16 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14
| j(e24) = e15
| j(e24) = e16 )
& ( j(e25) = e10
| j(e25) = e11
| j(e25) = e12
| j(e25) = e13
| j(e25) = e14
| j(e25) = e15
| j(e25) = e16 )
& ( j(e26) = e10
| j(e26) = e11
| j(e26) = e12
| j(e26) = e13
| j(e26) = e14
| j(e26) = e15
| j(e26) = e16 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
( h(op1(e10,e10)) = op2(h(e10),h(e10))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e16)) = op2(h(e10),h(e16))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e16)) = op2(h(e11),h(e16))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e16)) = op2(h(e12),h(e16))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e16)) = op2(h(e13),h(e16))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e16)) = op2(h(e16),h(e16))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e26)) = op1(j(e20),j(e26))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e26)) = op1(j(e21),j(e26))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e26)) = op1(j(e22),j(e26))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e26)) = op1(j(e23),j(e26))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& h(j(e20)) = e20
& h(j(e21)) = e21
& h(j(e22)) = e22
& h(j(e23)) = e23
& h(j(e24)) = e24
& h(j(e25)) = e25
& h(j(e26)) = e26
& j(h(e10)) = e10
& j(h(e11)) = e11
& j(h(e12)) = e12
& j(h(e13)) = e13
& j(h(e14)) = e14
& j(h(e15)) = e15
& j(h(e16)) = e16
& ( h(e10) = e20
| h(e10) = e21
| h(e10) = e22
| h(e10) = e23
| h(e10) = e24
| h(e10) = e25
| h(e10) = e26 )
& ( h(e11) = e20
| h(e11) = e21
| h(e11) = e22
| h(e11) = e23
| h(e11) = e24
| h(e11) = e25
| h(e11) = e26 )
& ( h(e12) = e20
| h(e12) = e21
| h(e12) = e22
| h(e12) = e23
| h(e12) = e24
| h(e12) = e25
| h(e12) = e26 )
& ( h(e13) = e20
| h(e13) = e21
| h(e13) = e22
| h(e13) = e23
| h(e13) = e24
| h(e13) = e25
| h(e13) = e26 )
& ( h(e14) = e20
| h(e14) = e21
| h(e14) = e22
| h(e14) = e23
| h(e14) = e24
| h(e14) = e25
| h(e14) = e26 )
& ( h(e15) = e20
| h(e15) = e21
| h(e15) = e22
| h(e15) = e23
| h(e15) = e24
| h(e15) = e25
| h(e15) = e26 )
& ( h(e16) = e20
| h(e16) = e21
| h(e16) = e22
| h(e16) = e23
| h(e16) = e24
| h(e16) = e25
| h(e16) = e26 )
& ( j(e20) = e10
| j(e20) = e11
| j(e20) = e12
| j(e20) = e13
| j(e20) = e14
| j(e20) = e15
| j(e20) = e16 )
& ( j(e21) = e10
| j(e21) = e11
| j(e21) = e12
| j(e21) = e13
| j(e21) = e14
| j(e21) = e15
| j(e21) = e16 )
& ( j(e22) = e10
| j(e22) = e11
| j(e22) = e12
| j(e22) = e13
| j(e22) = e14
| j(e22) = e15
| j(e22) = e16 )
& ( j(e23) = e10
| j(e23) = e11
| j(e23) = e12
| j(e23) = e13
| j(e23) = e14
| j(e23) = e15
| j(e23) = e16 )
& ( j(e24) = e10
| j(e24) = e11
| j(e24) = e12
| j(e24) = e13
| j(e24) = e14
| j(e24) = e15
| j(e24) = e16 )
& ( j(e25) = e10
| j(e25) = e11
| j(e25) = e12
| j(e25) = e13
| j(e25) = e14
| j(e25) = e15
| j(e25) = e16 )
& ( j(e26) = e10
| j(e26) = e11
| j(e26) = e12
| j(e26) = e13
| j(e26) = e14
| j(e26) = e15
| j(e26) = e16 ) ),
inference(flattening,[],[f8]) ).
fof(f31,plain,
e25 != e26,
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
e16 = op1(e16,e16),
inference(cnf_transformation,[],[f4]) ).
fof(f109,plain,
e15 = op1(e15,e15),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
e14 = op1(e14,e14),
inference(cnf_transformation,[],[f4]) ).
fof(f125,plain,
e13 = op1(e13,e13),
inference(cnf_transformation,[],[f4]) ).
fof(f133,plain,
e12 = op1(e12,e12),
inference(cnf_transformation,[],[f4]) ).
fof(f141,plain,
e11 = op1(e11,e11),
inference(cnf_transformation,[],[f4]) ).
fof(f149,plain,
e10 = op1(e10,e10),
inference(cnf_transformation,[],[f4]) ).
fof(f150,plain,
e25 = op2(e26,e26),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( e10 = j(e26)
| e11 = j(e26)
| e12 = j(e26)
| e13 = j(e26)
| e14 = j(e26)
| e15 = j(e26)
| e16 = j(e26) ),
inference(cnf_transformation,[],[f9]) ).
fof(f220,plain,
e26 = h(j(e26)),
inference(cnf_transformation,[],[f9]) ).
fof(f221,plain,
e25 = h(j(e25)),
inference(cnf_transformation,[],[f9]) ).
fof(f227,plain,
j(op2(e26,e26)) = op1(j(e26),j(e26)),
inference(cnf_transformation,[],[f9]) ).
fof(f276,plain,
h(op1(e16,e16)) = op2(h(e16),h(e16)),
inference(cnf_transformation,[],[f9]) ).
fof(f292,plain,
h(op1(e14,e14)) = op2(h(e14),h(e14)),
inference(cnf_transformation,[],[f9]) ).
fof(f300,plain,
h(op1(e13,e13)) = op2(h(e13),h(e13)),
inference(cnf_transformation,[],[f9]) ).
fof(f308,plain,
h(op1(e12,e12)) = op2(h(e12),h(e12)),
inference(cnf_transformation,[],[f9]) ).
fof(f316,plain,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(cnf_transformation,[],[f9]) ).
fof(f326,definition,
( spl0_1
<=> e16 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f328,plain,
( e16 = j(e26)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f330,definition,
( spl0_2
<=> e15 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f332,plain,
( e15 = j(e26)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f334,definition,
( spl0_3
<=> e14 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f336,plain,
( e14 = j(e26)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f338,definition,
( spl0_4
<=> e13 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f340,plain,
( e13 = j(e26)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f338]) ).
fof(f342,definition,
( spl0_5
<=> e12 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f344,plain,
( e12 = j(e26)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f346,definition,
( spl0_6
<=> e11 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f348,plain,
( e11 = j(e26)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f350,definition,
( spl0_7
<=> e10 = j(e26) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f352,plain,
( e10 = j(e26)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7 ),
inference(avatar_split_clause,[],[f199,f350,f346,f342,f338,f334,f330,f326]) ).
fof(f387,definition,
( spl0_9
<=> e15 = j(e25) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f388,plain,
( e15 != j(e25)
| spl0_9 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f389,plain,
( e15 = j(e25)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f407,definition,
( spl0_14
<=> e10 = j(e25) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f408,plain,
( e10 != j(e25)
| spl0_14 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( e10 = j(e25)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f449,plain,
( e26 = h(e10)
| ~ spl0_7 ),
inference(superposition,[],[f220,f352]) ).
fof(f561,plain,
( e25 = h(e10)
| ~ spl0_14 ),
inference(superposition,[],[f221,f409]) ).
fof(f595,plain,
( e25 = e26
| ~ spl0_7
| ~ spl0_14 ),
inference(superposition,[],[f449,f561]) ).
fof(f596,plain,
( $false
| ~ spl0_7
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f595,f31]) ).
fof(f597,plain,
( ~ spl0_7
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f596]) ).
fof(f1949,plain,
( e26 = h(e12)
| ~ spl0_5 ),
inference(superposition,[],[f220,f344]) ).
fof(f1990,plain,
( op2(e26,e26) = h(op1(e12,e12))
| ~ spl0_5 ),
inference(superposition,[],[f308,f1949]) ).
fof(f2193,plain,
( op2(e26,e26) = h(e12)
| ~ spl0_5 ),
inference(superposition,[],[f1990,f133]) ).
fof(f2194,plain,
( e26 = op2(e26,e26)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f2193,f1949]) ).
fof(f2261,plain,
( e25 = e26
| ~ spl0_5 ),
inference(superposition,[],[f150,f2194]) ).
fof(f2267,plain,
( $false
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f2261,f31]) ).
fof(f2268,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f2267]) ).
fof(f2289,plain,
( e26 = h(e13)
| ~ spl0_4 ),
inference(superposition,[],[f220,f340]) ).
fof(f2405,plain,
( op2(e26,e26) = h(op1(e13,e13))
| ~ spl0_4 ),
inference(superposition,[],[f300,f2289]) ).
fof(f2418,plain,
( op2(e26,e26) = h(e13)
| ~ spl0_4 ),
inference(forward_demodulation,[],[f2405,f125]) ).
fof(f2431,plain,
( e26 = op2(e26,e26)
| ~ spl0_4 ),
inference(forward_demodulation,[],[f2418,f2289]) ).
fof(f2440,plain,
( e25 = e26
| ~ spl0_4 ),
inference(forward_demodulation,[],[f2431,f150]) ).
fof(f2447,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f2440,f31]) ).
fof(f2448,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f2447]) ).
fof(f2501,plain,
( e26 = h(e11)
| ~ spl0_6 ),
inference(superposition,[],[f220,f348]) ).
fof(f2563,plain,
( e25 = h(e15)
| ~ spl0_9 ),
inference(superposition,[],[f221,f389]) ).
fof(f2714,plain,
( op2(e26,e26) = h(op1(e11,e11))
| ~ spl0_6 ),
inference(superposition,[],[f316,f2501]) ).
fof(f2719,plain,
( op2(e26,e26) = h(e11)
| ~ spl0_6 ),
inference(forward_demodulation,[],[f2714,f141]) ).
fof(f2732,plain,
( e26 = op2(e26,e26)
| ~ spl0_6 ),
inference(forward_demodulation,[],[f2719,f2501]) ).
fof(f2743,plain,
( e25 = e26
| ~ spl0_6 ),
inference(forward_demodulation,[],[f2732,f150]) ).
fof(f2748,plain,
( $false
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f2743,f31]) ).
fof(f2749,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f2748]) ).
fof(f2854,plain,
( e26 = h(e15)
| ~ spl0_2 ),
inference(superposition,[],[f220,f332]) ).
fof(f3051,plain,
( e25 = e26
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f2854,f2563]) ).
fof(f3052,plain,
( $false
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f3051,f31]) ).
fof(f3053,plain,
( ~ spl0_2
| ~ spl0_9 ),
inference(avatar_contradiction_clause,[],[f3052]) ).
fof(f3109,plain,
( e26 = h(e16)
| ~ spl0_1 ),
inference(superposition,[],[f220,f328]) ).
fof(f3322,plain,
( op2(e26,e26) = h(op1(e16,e16))
| ~ spl0_1 ),
inference(superposition,[],[f276,f3109]) ).
fof(f3347,plain,
( op2(e26,e26) = h(e16)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f3322,f101]) ).
fof(f3358,plain,
( e26 = op2(e26,e26)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f3347,f3109]) ).
fof(f3361,plain,
( e25 = e26
| ~ spl0_1 ),
inference(forward_demodulation,[],[f3358,f150]) ).
fof(f3362,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f3361,f31]) ).
fof(f3363,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f3362]) ).
fof(f3368,plain,
( e26 = h(e14)
| ~ spl0_3 ),
inference(superposition,[],[f220,f336]) ).
fof(f3666,plain,
( op2(e26,e26) = h(op1(e14,e14))
| ~ spl0_3 ),
inference(superposition,[],[f292,f3368]) ).
fof(f3683,plain,
( op2(e26,e26) = h(e14)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f3666,f117]) ).
fof(f3696,plain,
( e26 = op2(e26,e26)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f3683,f3368]) ).
fof(f3703,plain,
( e25 = e26
| ~ spl0_3 ),
inference(forward_demodulation,[],[f3696,f150]) ).
fof(f3706,plain,
( $false
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f3703,f31]) ).
fof(f3707,plain,
~ spl0_3,
inference(avatar_contradiction_clause,[],[f3706]) ).
fof(f3709,plain,
( op1(e10,e10) = j(op2(e26,e26))
| ~ spl0_7 ),
inference(superposition,[],[f227,f352]) ).
fof(f3740,plain,
( op1(e10,e10) = j(e25)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f3709,f150]) ).
fof(f3762,plain,
( e10 = j(e25)
| ~ spl0_7 ),
inference(forward_demodulation,[],[f3740,f149]) ).
fof(f3763,plain,
( $false
| ~ spl0_7
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f3762,f408]) ).
fof(f3764,plain,
( ~ spl0_7
| spl0_14 ),
inference(avatar_contradiction_clause,[],[f3763]) ).
fof(f3766,plain,
( op1(e15,e15) = j(op2(e26,e26))
| ~ spl0_2 ),
inference(superposition,[],[f227,f332]) ).
fof(f3793,plain,
( op1(e15,e15) = j(e25)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3766,f150]) ).
fof(f3803,plain,
( e15 = j(e25)
| ~ spl0_2 ),
inference(forward_demodulation,[],[f3793,f109]) ).
fof(f3806,plain,
( $false
| ~ spl0_2
| spl0_9 ),
inference(forward_subsumption_resolution,[],[f3803,f388]) ).
fof(f3807,plain,
( ~ spl0_2
| spl0_9 ),
inference(avatar_contradiction_clause,[],[f3806]) ).
cnf(s520,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f353]) ).
cnf(s758,plain,
( ~ spl0_7
| ~ spl0_14 ),
inference(sat_conversion,[],[f597]) ).
cnf(s2211,plain,
~ spl0_5,
inference(sat_conversion,[],[f2268]) ).
cnf(s2315,plain,
~ spl0_4,
inference(sat_conversion,[],[f2448]) ).
cnf(s2469,plain,
~ spl0_6,
inference(sat_conversion,[],[f2749]) ).
cnf(s2623,plain,
( ~ spl0_2
| ~ spl0_9 ),
inference(sat_conversion,[],[f3053]) ).
cnf(s2797,plain,
~ spl0_1,
inference(sat_conversion,[],[f3363]) ).
cnf(s2960,plain,
~ spl0_3,
inference(sat_conversion,[],[f3707]) ).
cnf(s3004,plain,
( ~ spl0_7
| spl0_14 ),
inference(sat_conversion,[],[f3764]) ).
cnf(s3024,plain,
( ~ spl0_2
| spl0_9 ),
inference(sat_conversion,[],[f3807]) ).
cnf(s3025,plain,
( spl0_2
| spl0_7 ),
inference(rat,[],[s520,s2469,s2211,s2315,s2960,s2797]) ).
cnf(s3026,plain,
~ spl0_7,
inference(rat,[],[s758,s3004]) ).
cnf(s3027,plain,
spl0_2,
inference(rat,[],[s3025,s3026]) ).
cnf(s3028,plain,
spl0_9,
inference(rat,[],[s3024,s3027]) ).
cnf(s3032,plain,
$false,
inference(rat,[],[s2623,s3028,s3027]) ).
fof(f3808,plain,
$false,
inference(avatar_sat_refutation,[],[s3032]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG206+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n010.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 19:42:32 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.87/0.40 % (2242744)Will run a generic schedule for satisfiability detection.
% 0.87/0.40 % (2242752)dis+10_1_sil=32000:sp=arity:random_seed=3017697990:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.87/0.40 % (2242750)% WARNING: option uhcvi not known.
% 0.87/0.40 % (2242750)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=732444483:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.87/0.40 % (2242751)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=53641765:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.87/0.40 % (2242749)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1624803640_2999 on theBenchmark for (2999ds/0Mi)
% 0.87/0.40 % (2242753)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2328006332:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.87/0.40 % (2242754)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2293894801:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.87/0.40 % (2242755)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3626138122:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.87/0.40 % (2242752)Instruction limit reached!
% 0.87/0.40 % (2242752)------------------------------
% 0.87/0.40 % (2242752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (2242752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (2242752)CaDiCaL version: 2.1.3
% 0.87/0.40 % (2242752)Termination reason: Instruction limit
% 0.87/0.40 % (2242752)Termination phase: Saturation
% 0.87/0.40 % (2242752)Time elapsed: 0.028 s
% 0.87/0.40 % (2242752)Peak memory usage: 12 MB
% 0.87/0.40 % (2242752)Instructions burned: 104 (million)
% 0.87/0.40 % Detected minimum model sizes of [14]
% 0.87/0.40 % Detected maximum model sizes of [max]
% 0.87/0.40 % TRYING [14]
% 0.87/0.40 % (2242763)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1951999972:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.87/0.40 % Detected minimum model sizes of [14]
% 0.87/0.40 % Detected maximum model sizes of [max]
% 0.87/0.40 % TRYING [14]
% 0.87/0.40 % (2242754)Instruction limit reached!
% 0.87/0.40 % (2242754)------------------------------
% 0.87/0.40 % (2242754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (2242754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (2242754)CaDiCaL version: 2.1.3
% 0.87/0.40 % (2242754)Termination reason: Instruction limit
% 0.87/0.40 % (2242754)Termination phase: Saturation
% 0.87/0.40 % (2242754)Time elapsed: 0.060 s
% 0.87/0.40 % (2242754)Peak memory usage: 13 MB
% 0.87/0.40 % (2242754)Instructions burned: 132 (million)
% 0.87/0.40 % (2242753)Instruction limit reached!
% 0.87/0.40 % (2242753)------------------------------
% 0.87/0.40 % (2242753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (2242753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (2242753)CaDiCaL version: 2.1.3
% 0.87/0.40 % (2242753)Termination reason: Instruction limit
% 0.87/0.40 % (2242753)Termination phase: Saturation
% 0.87/0.40 % (2242753)Time elapsed: 0.060 s
% 0.87/0.40 % (2242753)Peak memory usage: 12 MB
% 0.87/0.40 % (2242753)Instructions burned: 116 (million)
% 0.87/0.40 % (2242765)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3868145051:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.87/0.40 % (2242766)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1990704460:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.87/0.40 % (2242755)Instruction limit reached!
% 0.87/0.40 % (2242755)------------------------------
% 0.87/0.40 % (2242755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.40 % (2242755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.40 % (2242755)CaDiCaL version: 2.1.3
% 0.87/0.40 % (2242755)Termination reason: Instruction limit
% 0.87/0.40 % (2242755)Termination phase: Saturation
% 0.87/0.40 % (2242755)Time elapsed: 0.086 s
% 0.87/0.40 % (2242755)Peak memory usage: 13 MB
% 0.87/0.40 % (2242755)Instructions burned: 160 (million)
% 0.87/0.40 % (2242751) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2242744-2242751"...
% 0.87/0.40 % (2242751)...printing done.
% 0.87/0.40 % (2242769)ott-21_1_sil=16000:fs=off:random_seed=2406908926:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.87/0.40 % (2242751)Refutation found. Thanks to Tanya!
% 0.87/0.40 % SZS status Theorem for theBenchmark
% 0.87/0.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.87/0.41 % (2242751)------------------------------
% 0.87/0.41 % (2242751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.41 % (2242751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.41 % (2242751)CaDiCaL version: 2.1.3
% 0.87/0.41 % (2242751)Termination reason: Refutation
% 0.87/0.41 % (2242751)Time elapsed: 0.106 s
% 0.87/0.41 % (2242751)Peak memory usage: 14 MB
% 0.87/0.41 % (2242751)Instructions burned: 211 (million)
% 0.87/0.41 % (2242744)Success in time 0.16 s
% 0.87/0.41 % Vampire exiting
%------------------------------------------------------------------------------