%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG206+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 : Sun Sep 27 06:49:44 AM UTC 2026
% Result : Theorem 16.69s 2.52s
% Output : CNFRefutation 16.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 105
% Number of leaves : 4
% Syntax : Number of formulae : 146 ( 38 unt; 0 def)
% Number of atoms : 1279 (1278 equ)
% Maximal formula atoms : 210 ( 8 avg)
% Number of connectives : 1159 ( 26 ~; 767 |; 364 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 115 ( 7 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 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(ax2,axiom,
( e25 != e26
& e24 != e26
& e24 != e25
& e23 != e26
& e23 != e25
& e23 != e24
& e22 != e26
& e22 != e25
& e22 != e24
& e22 != e23
& e21 != e26
& e21 != e25
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e26
& e20 != e25
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax2) ).
fof(ax4,axiom,
( op1(e16,e16) = e16
& op1(e16,e15) = e12
& op1(e16,e14) = e13
& op1(e16,e13) = e11
& op1(e16,e12) = e10
& op1(e16,e11) = e14
& op1(e16,e10) = e15
& op1(e15,e16) = e12
& op1(e15,e15) = e15
& op1(e15,e14) = e11
& op1(e15,e13) = e16
& op1(e15,e12) = e13
& op1(e15,e11) = e10
& op1(e15,e10) = e14
& op1(e14,e16) = e13
& op1(e14,e15) = e11
& op1(e14,e14) = e14
& op1(e14,e13) = e10
& op1(e14,e12) = e15
& op1(e14,e11) = e12
& op1(e14,e10) = e16
& op1(e13,e16) = e11
& op1(e13,e15) = e16
& op1(e13,e14) = e10
& op1(e13,e13) = e13
& op1(e13,e12) = e14
& op1(e13,e11) = e15
& op1(e13,e10) = e12
& op1(e12,e16) = e10
& op1(e12,e15) = e13
& op1(e12,e14) = e15
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e16
& op1(e12,e10) = e11
& op1(e11,e16) = e14
& op1(e11,e15) = e10
& op1(e11,e14) = e12
& op1(e11,e13) = e15
& op1(e11,e12) = e16
& op1(e11,e11) = e11
& op1(e11,e10) = e13
& op1(e10,e16) = e15
& op1(e10,e15) = e14
& op1(e10,e14) = e16
& op1(e10,e13) = e12
& op1(e10,e12) = e11
& op1(e10,e11) = e13
& op1(e10,e10) = e10 ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op2(e26,e26) = e25
& op2(e26,e25) = e20
& op2(e26,e24) = e21
& op2(e26,e23) = e24
& op2(e26,e22) = e22
& op2(e26,e21) = e23
& op2(e26,e20) = e26
& op2(e25,e26) = e20
& op2(e25,e25) = e21
& op2(e25,e24) = e26
& op2(e25,e23) = e23
& op2(e25,e22) = e25
& op2(e25,e21) = e22
& op2(e25,e20) = e24
& op2(e24,e26) = e21
& op2(e24,e25) = e26
& op2(e24,e24) = e24
& op2(e24,e23) = e22
& op2(e24,e22) = e20
& op2(e24,e21) = e25
& op2(e24,e20) = e23
& op2(e23,e26) = e24
& op2(e23,e25) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e20
& op2(e23,e22) = e26
& op2(e23,e21) = e21
& op2(e23,e20) = e25
& op2(e22,e26) = e22
& op2(e22,e25) = e25
& op2(e22,e24) = e20
& op2(e22,e23) = e26
& op2(e22,e22) = e23
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e26) = e23
& op2(e21,e25) = e22
& op2(e21,e24) = e25
& op2(e21,e23) = e21
& op2(e21,e22) = e24
& op2(e21,e21) = e26
& op2(e21,e20) = e20
& op2(e20,e26) = e26
& op2(e20,e25) = e24
& op2(e20,e24) = e23
& op2(e20,e23) = e25
& op2(e20,e22) = e21
& op2(e20,e21) = e20
& op2(e20,e20) = e22 ),
file('theBenchmark.p',ax5) ).
fof(co1,conjecture,
( ( ( j(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e16)) = e16
& j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e26)) = e26
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e26)) = op1(j(e23),j(e26))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e26)) = op1(j(e22),j(e26))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e26)) = op1(j(e21),j(e26))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e26)) = op1(j(e20),j(e26))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e16)) = op2(h(e13),h(e16))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e16)) = op2(h(e12),h(e16))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e16)) = op2(h(e11),h(e16))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e16)) = op2(h(e10),h(e16))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10)) ) ),
file('theBenchmark.p',co1) ).
fof(co1_neg,negated_conjecture,
~ ( ( ( j(e26) = e16
| j(e26) = e15
| j(e26) = e14
| j(e26) = e13
| j(e26) = e12
| j(e26) = e11
| j(e26) = e10 )
& ( j(e25) = e16
| j(e25) = e15
| j(e25) = e14
| j(e25) = e13
| j(e25) = e12
| j(e25) = e11
| j(e25) = e10 )
& ( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e16
| j(e23) = e15
| j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e16
| j(e22) = e15
| j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e16
| j(e21) = e15
| j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e16) = e26
| h(e16) = e25
| h(e16) = e24
| h(e16) = e23
| h(e16) = e22
| h(e16) = e21
| h(e16) = e20 )
& ( h(e15) = e26
| h(e15) = e25
| h(e15) = e24
| h(e15) = e23
| h(e15) = e22
| h(e15) = e21
| h(e15) = e20 )
& ( h(e14) = e26
| h(e14) = e25
| h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e26
| h(e13) = e25
| h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e26
| h(e12) = e25
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e26
| h(e11) = e25
| h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e26
| h(e10) = e25
| h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e16)) = e16
& j(h(e15)) = e15
& j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e26)) = e26
& h(j(e25)) = e25
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& j(op2(e26,e26)) = op1(j(e26),j(e26))
& j(op2(e26,e25)) = op1(j(e26),j(e25))
& j(op2(e26,e24)) = op1(j(e26),j(e24))
& j(op2(e26,e23)) = op1(j(e26),j(e23))
& j(op2(e26,e22)) = op1(j(e26),j(e22))
& j(op2(e26,e21)) = op1(j(e26),j(e21))
& j(op2(e26,e20)) = op1(j(e26),j(e20))
& j(op2(e25,e26)) = op1(j(e25),j(e26))
& j(op2(e25,e25)) = op1(j(e25),j(e25))
& j(op2(e25,e24)) = op1(j(e25),j(e24))
& j(op2(e25,e23)) = op1(j(e25),j(e23))
& j(op2(e25,e22)) = op1(j(e25),j(e22))
& j(op2(e25,e21)) = op1(j(e25),j(e21))
& j(op2(e25,e20)) = op1(j(e25),j(e20))
& j(op2(e24,e26)) = op1(j(e24),j(e26))
& j(op2(e24,e25)) = op1(j(e24),j(e25))
& j(op2(e24,e24)) = op1(j(e24),j(e24))
& j(op2(e24,e23)) = op1(j(e24),j(e23))
& j(op2(e24,e22)) = op1(j(e24),j(e22))
& j(op2(e24,e21)) = op1(j(e24),j(e21))
& j(op2(e24,e20)) = op1(j(e24),j(e20))
& j(op2(e23,e26)) = op1(j(e23),j(e26))
& j(op2(e23,e25)) = op1(j(e23),j(e25))
& j(op2(e23,e24)) = op1(j(e23),j(e24))
& j(op2(e23,e23)) = op1(j(e23),j(e23))
& j(op2(e23,e22)) = op1(j(e23),j(e22))
& j(op2(e23,e21)) = op1(j(e23),j(e21))
& j(op2(e23,e20)) = op1(j(e23),j(e20))
& j(op2(e22,e26)) = op1(j(e22),j(e26))
& j(op2(e22,e25)) = op1(j(e22),j(e25))
& j(op2(e22,e24)) = op1(j(e22),j(e24))
& j(op2(e22,e23)) = op1(j(e22),j(e23))
& j(op2(e22,e22)) = op1(j(e22),j(e22))
& j(op2(e22,e21)) = op1(j(e22),j(e21))
& j(op2(e22,e20)) = op1(j(e22),j(e20))
& j(op2(e21,e26)) = op1(j(e21),j(e26))
& j(op2(e21,e25)) = op1(j(e21),j(e25))
& j(op2(e21,e24)) = op1(j(e21),j(e24))
& j(op2(e21,e23)) = op1(j(e21),j(e23))
& j(op2(e21,e22)) = op1(j(e21),j(e22))
& j(op2(e21,e21)) = op1(j(e21),j(e21))
& j(op2(e21,e20)) = op1(j(e21),j(e20))
& j(op2(e20,e26)) = op1(j(e20),j(e26))
& j(op2(e20,e25)) = op1(j(e20),j(e25))
& j(op2(e20,e24)) = op1(j(e20),j(e24))
& j(op2(e20,e23)) = op1(j(e20),j(e23))
& j(op2(e20,e22)) = op1(j(e20),j(e22))
& j(op2(e20,e21)) = op1(j(e20),j(e21))
& j(op2(e20,e20)) = op1(j(e20),j(e20))
& h(op1(e16,e16)) = op2(h(e16),h(e16))
& h(op1(e16,e15)) = op2(h(e16),h(e15))
& h(op1(e16,e14)) = op2(h(e16),h(e14))
& h(op1(e16,e13)) = op2(h(e16),h(e13))
& h(op1(e16,e12)) = op2(h(e16),h(e12))
& h(op1(e16,e11)) = op2(h(e16),h(e11))
& h(op1(e16,e10)) = op2(h(e16),h(e10))
& h(op1(e15,e16)) = op2(h(e15),h(e16))
& h(op1(e15,e15)) = op2(h(e15),h(e15))
& h(op1(e15,e14)) = op2(h(e15),h(e14))
& h(op1(e15,e13)) = op2(h(e15),h(e13))
& h(op1(e15,e12)) = op2(h(e15),h(e12))
& h(op1(e15,e11)) = op2(h(e15),h(e11))
& h(op1(e15,e10)) = op2(h(e15),h(e10))
& h(op1(e14,e16)) = op2(h(e14),h(e16))
& h(op1(e14,e15)) = op2(h(e14),h(e15))
& h(op1(e14,e14)) = op2(h(e14),h(e14))
& h(op1(e14,e13)) = op2(h(e14),h(e13))
& h(op1(e14,e12)) = op2(h(e14),h(e12))
& h(op1(e14,e11)) = op2(h(e14),h(e11))
& h(op1(e14,e10)) = op2(h(e14),h(e10))
& h(op1(e13,e16)) = op2(h(e13),h(e16))
& h(op1(e13,e15)) = op2(h(e13),h(e15))
& h(op1(e13,e14)) = op2(h(e13),h(e14))
& h(op1(e13,e13)) = op2(h(e13),h(e13))
& h(op1(e13,e12)) = op2(h(e13),h(e12))
& h(op1(e13,e11)) = op2(h(e13),h(e11))
& h(op1(e13,e10)) = op2(h(e13),h(e10))
& h(op1(e12,e16)) = op2(h(e12),h(e16))
& h(op1(e12,e15)) = op2(h(e12),h(e15))
& h(op1(e12,e14)) = op2(h(e12),h(e14))
& h(op1(e12,e13)) = op2(h(e12),h(e13))
& h(op1(e12,e12)) = op2(h(e12),h(e12))
& h(op1(e12,e11)) = op2(h(e12),h(e11))
& h(op1(e12,e10)) = op2(h(e12),h(e10))
& h(op1(e11,e16)) = op2(h(e11),h(e16))
& h(op1(e11,e15)) = op2(h(e11),h(e15))
& h(op1(e11,e14)) = op2(h(e11),h(e14))
& h(op1(e11,e13)) = op2(h(e11),h(e13))
& h(op1(e11,e12)) = op2(h(e11),h(e12))
& h(op1(e11,e11)) = op2(h(e11),h(e11))
& h(op1(e11,e10)) = op2(h(e11),h(e10))
& h(op1(e10,e16)) = op2(h(e10),h(e16))
& h(op1(e10,e15)) = op2(h(e10),h(e15))
& h(op1(e10,e14)) = op2(h(e10),h(e14))
& h(op1(e10,e13)) = op2(h(e10),h(e13))
& h(op1(e10,e12)) = op2(h(e10),h(e12))
& h(op1(e10,e11)) = op2(h(e10),h(e11))
& h(op1(e10,e10)) = op2(h(e10),h(e10)) ) ),
inference(assume_negation,[status(cth)],[co1]) ).
cnf(c_29,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_34,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_98,plain,
op1(e10,e10) = e10,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_106,plain,
op1(e11,e11) = e11,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_114,plain,
op1(e12,e12) = e12,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_122,plain,
op1(e13,e13) = e13,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_130,plain,
op1(e14,e14) = e14,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_138,plain,
op1(e15,e15) = e15,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_146,plain,
op1(e16,e16) = e16,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_147,plain,
op2(e20,e20) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_149,plain,
op2(e20,e22) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_154,plain,
op2(e21,e20) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_203,negated_conjecture,
( j(e20) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_210,negated_conjecture,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3997,negated_conjecture,
h(e10) = op2(h(e10),h(e10)),
inference(paramod,[status(thm)],[c_98,c_210]) ).
cnf(c_211,negated_conjecture,
op2(h(e10),h(e10)) = h(e10),
inference(copy,[status(thm)],[c_3997]) ).
cnf(c_226,negated_conjecture,
h(op1(e11,e11)) = op2(h(e11),h(e11)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3998,negated_conjecture,
h(e11) = op2(h(e11),h(e11)),
inference(paramod,[status(thm)],[c_106,c_226]) ).
cnf(c_227,negated_conjecture,
op2(h(e11),h(e11)) = h(e11),
inference(copy,[status(thm)],[c_3998]) ).
cnf(c_308,negated_conjecture,
j(op2(e20,e20)) = op1(j(e20),j(e20)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_309,negated_conjecture,
j(e22) = op1(j(e20),j(e20)),
inference(paramod,[status(thm)],[c_147,c_308]) ).
cnf(c_312,negated_conjecture,
j(op2(e20,e22)) = op1(j(e20),j(e22)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_3999,negated_conjecture,
j(e21) = op1(j(e20),j(e22)),
inference(paramod,[status(thm)],[c_149,c_312]) ).
cnf(c_313,negated_conjecture,
j(e21) = op1(j(e20),op1(j(e20),j(e20))),
inference(paramod,[status(thm)],[c_309,c_3999]) ).
cnf(c_322,negated_conjecture,
j(op2(e21,e20)) = op1(j(e21),j(e20)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_4000,negated_conjecture,
j(e20) = op1(j(e21),j(e20)),
inference(paramod,[status(thm)],[c_154,c_322]) ).
cnf(c_4001,negated_conjecture,
j(e20) = op1(op1(j(e20),op1(j(e20),j(e20))),j(e20)),
inference(paramod,[status(thm)],[c_313,c_4000]) ).
cnf(c_323,negated_conjecture,
op1(op1(j(e20),op1(j(e20),j(e20))),j(e20)) = j(e20),
inference(copy,[status(thm)],[c_4001]) ).
cnf(c_406,negated_conjecture,
h(j(e20)) = e20,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_407,negated_conjecture,
h(j(e21)) = e21,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_408,negated_conjecture,
h(op1(j(e20),op1(j(e20),j(e20)))) = e21,
inference(paramod,[status(thm)],[c_313,c_407]) ).
cnf(c_409,negated_conjecture,
h(j(e22)) = e22,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_410,negated_conjecture,
h(op1(j(e20),j(e20))) = e22,
inference(paramod,[status(thm)],[c_309,c_409]) ).
cnf(c_4002,plain,
( j(e22) = op1(e16,j(e20))
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_203,c_309]) ).
cnf(c_609,plain,
( op1(j(e20),j(e20)) = op1(e16,j(e20))
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_309,c_4002]) ).
cnf(c_614,plain,
( op1(op1(e16,op1(j(e20),j(e20))),j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_203,c_323]) ).
cnf(c_623,plain,
( h(op1(j(e20),op1(e16,j(e20)))) = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_203,c_408]) ).
cnf(c_4003,plain,
( op1(j(e20),j(e20)) = op1(e16,e16)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_203,c_609]) ).
cnf(c_4004,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_146,c_4003]) ).
cnf(c_4005,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4004]) ).
cnf(c_4006,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4005]) ).
cnf(c_4007,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4006]) ).
cnf(c_4008,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4007]) ).
cnf(c_4009,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4008]) ).
cnf(c_989,plain,
( op1(j(e20),j(e20)) = e16
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4009]) ).
cnf(c_4010,plain,
( op1(op1(e16,e16),j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_989,c_614]) ).
cnf(c_4011,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_146,c_4010]) ).
cnf(c_4012,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4011]) ).
cnf(c_4013,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4012]) ).
cnf(c_4014,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4013]) ).
cnf(c_4015,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4014]) ).
cnf(c_4016,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4015]) ).
cnf(c_2133,plain,
( op1(e16,j(e20)) = j(e20)
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4016]) ).
cnf(c_4017,plain,
( h(op1(j(e20),j(e20))) = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2133,c_623]) ).
cnf(c_4018,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_410,c_4017]) ).
cnf(c_4019,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4018]) ).
cnf(c_4020,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4019]) ).
cnf(c_4021,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4020]) ).
cnf(c_4022,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4021]) ).
cnf(c_4023,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4022]) ).
cnf(c_4024,plain,
( e22 = e21
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4023]) ).
cnf(c_2142,plain,
( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_34,c_4024]) ).
cnf(c_4025,plain,
( j(e22) = op1(e15,j(e20))
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2142,c_309]) ).
cnf(c_2143,plain,
( op1(j(e20),j(e20)) = op1(e15,j(e20))
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_309,c_4025]) ).
cnf(c_2160,plain,
( h(op1(j(e20),e15)) = e22
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2142,c_410]) ).
cnf(c_4026,plain,
( op1(j(e20),j(e20)) = op1(e15,e15)
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2142,c_2143]) ).
cnf(c_4027,plain,
( op1(j(e20),j(e20)) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_138,c_4026]) ).
cnf(c_4028,plain,
( op1(j(e20),j(e20)) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4027]) ).
cnf(c_4029,plain,
( op1(j(e20),j(e20)) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4028]) ).
cnf(c_4030,plain,
( op1(j(e20),j(e20)) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4029]) ).
cnf(c_4031,plain,
( op1(j(e20),j(e20)) = e15
| j(e20) = e14
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4030]) ).
cnf(c_2201,plain,
( op1(j(e20),j(e20)) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4031]) ).
cnf(c_2236,plain,
( h(op1(j(e20),e15)) = e21
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2201,c_408]) ).
cnf(c_4032,plain,
( e21 = e22
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2236,c_2160]) ).
cnf(c_4033,plain,
( e22 = e21
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4032]) ).
cnf(c_4034,plain,
( e22 = e21
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4033]) ).
cnf(c_4035,plain,
( e22 = e21
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4034]) ).
cnf(c_4036,plain,
( e22 = e21
| j(e20) = e14
| j(e20) = e13
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4035]) ).
cnf(c_4037,plain,
( e22 = e21
| j(e20) = e14
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4036]) ).
cnf(c_4038,plain,
( e22 = e21
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4037]) ).
cnf(c_2282,plain,
( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_34,c_4038]) ).
cnf(c_4039,plain,
( j(e22) = op1(e14,j(e20))
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2282,c_309]) ).
cnf(c_2283,plain,
( op1(j(e20),j(e20)) = op1(e14,j(e20))
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_309,c_4039]) ).
cnf(c_2300,plain,
( h(op1(j(e20),e14)) = e22
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2282,c_410]) ).
cnf(c_4040,plain,
( op1(j(e20),j(e20)) = op1(e14,e14)
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2282,c_2283]) ).
cnf(c_4041,plain,
( op1(j(e20),j(e20)) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_130,c_4040]) ).
cnf(c_4042,plain,
( op1(j(e20),j(e20)) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4041]) ).
cnf(c_4043,plain,
( op1(j(e20),j(e20)) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4042]) ).
cnf(c_4044,plain,
( op1(j(e20),j(e20)) = e14
| j(e20) = e13
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4043]) ).
cnf(c_2369,plain,
( op1(j(e20),j(e20)) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4044]) ).
cnf(c_2381,plain,
( h(op1(j(e20),e14)) = e21
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2369,c_408]) ).
cnf(c_4045,plain,
( e21 = e22
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2381,c_2300]) ).
cnf(c_4046,plain,
( e22 = e21
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4045]) ).
cnf(c_4047,plain,
( e22 = e21
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4046]) ).
cnf(c_4048,plain,
( e22 = e21
| j(e20) = e13
| j(e20) = e12
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4047]) ).
cnf(c_4049,plain,
( e22 = e21
| j(e20) = e13
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4048]) ).
cnf(c_4050,plain,
( e22 = e21
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4049]) ).
cnf(c_2429,plain,
( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_34,c_4050]) ).
cnf(c_4051,plain,
( j(e22) = op1(e13,j(e20))
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2429,c_309]) ).
cnf(c_2432,plain,
( op1(j(e20),j(e20)) = op1(e13,j(e20))
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_309,c_4051]) ).
cnf(c_2465,plain,
( h(op1(j(e20),e13)) = e22
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2429,c_410]) ).
cnf(c_4052,plain,
( op1(j(e20),j(e20)) = op1(e13,e13)
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2429,c_2432]) ).
cnf(c_4053,plain,
( op1(j(e20),j(e20)) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_122,c_4052]) ).
cnf(c_4054,plain,
( op1(j(e20),j(e20)) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4053]) ).
cnf(c_4055,plain,
( op1(j(e20),j(e20)) = e13
| j(e20) = e12
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4054]) ).
cnf(c_2655,plain,
( op1(j(e20),j(e20)) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4055]) ).
cnf(c_2667,plain,
( h(op1(j(e20),e13)) = e21
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2655,c_408]) ).
cnf(c_4056,plain,
( e21 = e22
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2667,c_2465]) ).
cnf(c_4057,plain,
( e22 = e21
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4056]) ).
cnf(c_4058,plain,
( e22 = e21
| j(e20) = e12
| j(e20) = e11
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4057]) ).
cnf(c_4059,plain,
( e22 = e21
| j(e20) = e12
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4058]) ).
cnf(c_4060,plain,
( e22 = e21
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4059]) ).
cnf(c_2815,plain,
( j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_34,c_4060]) ).
cnf(c_4061,plain,
( j(e22) = op1(e12,j(e20))
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2815,c_309]) ).
cnf(c_2822,plain,
( op1(j(e20),j(e20)) = op1(e12,j(e20))
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_309,c_4061]) ).
cnf(c_2855,plain,
( h(op1(j(e20),e12)) = e22
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2815,c_410]) ).
cnf(c_4062,plain,
( op1(j(e20),j(e20)) = op1(e12,e12)
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2815,c_2822]) ).
cnf(c_4063,plain,
( op1(j(e20),j(e20)) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_114,c_4062]) ).
cnf(c_4064,plain,
( op1(j(e20),j(e20)) = e12
| j(e20) = e11
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4063]) ).
cnf(c_2970,plain,
( op1(j(e20),j(e20)) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4064]) ).
cnf(c_2987,plain,
( h(op1(j(e20),e12)) = e21
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2970,c_408]) ).
cnf(c_4065,plain,
( e21 = e22
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_2987,c_2855]) ).
cnf(c_4066,plain,
( e22 = e21
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4065]) ).
cnf(c_4067,plain,
( e22 = e21
| j(e20) = e11
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4066]) ).
cnf(c_4068,plain,
( e22 = e21
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_4067]) ).
cnf(c_3049,plain,
( j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_34,c_4068]) ).
cnf(c_3078,plain,
( h(e11) = e20
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_3049,c_406]) ).
cnf(c_3253,plain,
( h(e10) = e20
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_3078,c_406]) ).
cnf(c_3412,plain,
( op2(e20,h(e11)) = h(e11)
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_3253,c_227]) ).
cnf(c_4069,plain,
( op2(e20,e20) = h(e11)
| h(e10) = e20
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_3253,c_3412]) ).
cnf(c_4070,plain,
( e22 = h(e11)
| h(e10) = e20
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_147,c_4069]) ).
cnf(c_4071,plain,
( h(e11) = e22
| h(e10) = e20
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_4070]) ).
cnf(c_3719,plain,
( h(e11) = e22
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_4071]) ).
cnf(c_4072,plain,
( h(e10) = e20
| e22 = e20
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_3719,c_3253]) ).
cnf(c_4073,plain,
( e22 = e20
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_4072]) ).
cnf(c_3857,plain,
h(e10) = e20,
inference(resolve,[status(thm)],[c_29,c_4073]) ).
cnf(c_4074,negated_conjecture,
op2(e20,h(e10)) = h(e10),
inference(paramod,[status(thm)],[c_3857,c_211]) ).
cnf(c_4075,negated_conjecture,
op2(e20,e20) = h(e10),
inference(paramod,[status(thm)],[c_3857,c_4074]) ).
cnf(c_4076,negated_conjecture,
e22 = h(e10),
inference(paramod,[status(thm)],[c_147,c_4075]) ).
cnf(c_4077,negated_conjecture,
e22 = e20,
inference(paramod,[status(thm)],[c_3857,c_4076]) ).
cnf(c_3996,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_29,c_4077]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG206+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 21:25:31 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1571166 was started by sandbox2 on n011,
% 0.08/0.36 % Sat Sep 26 21:25:31 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.38
% 0.08/0.38 % From the command line: assign(max_seconds, 300).
% 16.69/2.52
% 16.69/2.52 % SZS status Theorem for theBenchmark
% 16.69/2.52
% 16.69/2.52 % Proof 1 at 1.80 (+ 0.32) seconds.
% 16.69/2.52 % Length of proof is 64.
% 16.69/2.52 % Level of proof is 29.
% 16.69/2.52 % Maximum clause weight is 72.000.
% 16.69/2.52 % Given clauses 448.
% 16.69/2.52
% 16.69/2.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------