%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG205+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 : n003.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 22.30s 3.27s
% Output : CNFRefutation 22.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 4
% Syntax : Number of formulae : 86 ( 21 unt; 0 def)
% Number of atoms : 944 ( 943 equ)
% Maximal formula atoms : 210 ( 10 avg)
% Number of connectives : 886 ( 28 ~; 492 |; 364 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 115 ( 9 avg)
% Maximal term depth : 3 ( 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(ax1,axiom,
( e15 != e16
& e14 != e16
& e14 != e15
& e13 != e16
& e13 != e15
& e13 != e14
& e12 != e16
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e16
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e16
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax1) ).
fof(ax4,axiom,
( op1(e16,e16) = e10
& op1(e16,e15) = e16
& op1(e16,e14) = e11
& op1(e16,e13) = e13
& op1(e16,e12) = e14
& op1(e16,e11) = e12
& op1(e16,e10) = e15
& op1(e15,e16) = e16
& op1(e15,e15) = e11
& op1(e15,e14) = e15
& op1(e15,e13) = e10
& op1(e15,e12) = e13
& op1(e15,e11) = e14
& op1(e15,e10) = e12
& op1(e14,e16) = e11
& op1(e14,e15) = e15
& op1(e14,e14) = e12
& op1(e14,e13) = e16
& op1(e14,e12) = e10
& op1(e14,e11) = e13
& op1(e14,e10) = e14
& op1(e13,e16) = e13
& op1(e13,e15) = e10
& op1(e13,e14) = e16
& op1(e13,e13) = e14
& op1(e13,e12) = e12
& op1(e13,e11) = e15
& op1(e13,e10) = e11
& op1(e12,e16) = e14
& op1(e12,e15) = e13
& op1(e12,e14) = e10
& op1(e12,e13) = e12
& op1(e12,e12) = e15
& op1(e12,e11) = e11
& op1(e12,e10) = e16
& op1(e11,e16) = e12
& op1(e11,e15) = e14
& op1(e11,e14) = e13
& op1(e11,e13) = e15
& op1(e11,e12) = e11
& op1(e11,e11) = e16
& op1(e11,e10) = e10
& op1(e10,e16) = e15
& op1(e10,e15) = e12
& op1(e10,e14) = e14
& op1(e10,e13) = e11
& op1(e10,e12) = e16
& op1(e10,e11) = e10
& op1(e10,e10) = e13 ),
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_9,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_17,plain,
e16 != e11,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_20,plain,
e15 != e12,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_22,plain,
e14 != e13,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_98,plain,
op1(e10,e10) = e13,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_106,plain,
op1(e11,e11) = e16,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_114,plain,
op1(e12,e12) = e15,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_122,plain,
op1(e13,e13) = e14,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_130,plain,
op1(e14,e14) = e12,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_138,plain,
op1(e15,e15) = e11,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_146,plain,
op1(e16,e16) = e10,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_179,plain,
op2(e24,e24) = e24,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_207,negated_conjecture,
( j(e24) = e16
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_372,negated_conjecture,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_7131,negated_conjecture,
j(e24) = op1(j(e24),j(e24)),
inference(paramod,[status(thm)],[c_179,c_372]) ).
cnf(c_373,negated_conjecture,
op1(j(e24),j(e24)) = j(e24),
inference(copy,[status(thm)],[c_7131]) ).
cnf(c_582,plain,
( op1(e16,j(e24)) = j(e24)
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_207,c_373]) ).
cnf(c_7132,plain,
( op1(e16,e16) = j(e24)
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_207,c_582]) ).
cnf(c_7133,plain,
( e10 = j(e24)
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_146,c_7132]) ).
cnf(c_7134,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7133]) ).
cnf(c_7135,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7134]) ).
cnf(c_7136,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7135]) ).
cnf(c_7137,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7136]) ).
cnf(c_7138,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7137]) ).
cnf(c_7139,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7138]) ).
cnf(c_7140,plain,
( j(e24) = e10
| j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7139]) ).
cnf(c_4424,plain,
( j(e24) = e15
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7140]) ).
cnf(c_4433,plain,
( op1(e15,j(e24)) = j(e24)
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_4424,c_373]) ).
cnf(c_7141,plain,
( op1(e15,e15) = j(e24)
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_4424,c_4433]) ).
cnf(c_7142,plain,
( e11 = j(e24)
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_138,c_7141]) ).
cnf(c_7143,plain,
( j(e24) = e11
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7142]) ).
cnf(c_7144,plain,
( j(e24) = e11
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7143]) ).
cnf(c_7145,plain,
( j(e24) = e11
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7144]) ).
cnf(c_7146,plain,
( j(e24) = e11
| j(e24) = e14
| j(e24) = e13
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7145]) ).
cnf(c_7147,plain,
( j(e24) = e11
| j(e24) = e14
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7146]) ).
cnf(c_7148,plain,
( j(e24) = e11
| j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7147]) ).
cnf(c_4918,plain,
( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7148]) ).
cnf(c_4927,plain,
( op1(e14,j(e24)) = j(e24)
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_4918,c_373]) ).
cnf(c_7149,plain,
( op1(e14,e14) = j(e24)
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_4918,c_4927]) ).
cnf(c_7150,plain,
( e12 = j(e24)
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_130,c_7149]) ).
cnf(c_7151,plain,
( j(e24) = e12
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7150]) ).
cnf(c_7152,plain,
( j(e24) = e12
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7151]) ).
cnf(c_7153,plain,
( j(e24) = e12
| j(e24) = e13
| j(e24) = e12
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7152]) ).
cnf(c_7154,plain,
( j(e24) = e12
| j(e24) = e13
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7153]) ).
cnf(c_7155,plain,
( j(e24) = e12
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7154]) ).
cnf(c_5397,plain,
( j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7155]) ).
cnf(c_5419,plain,
( op1(e13,j(e24)) = j(e24)
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_5397,c_373]) ).
cnf(c_7156,plain,
( op1(e13,e13) = j(e24)
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_5397,c_5419]) ).
cnf(c_7157,plain,
( e14 = j(e24)
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_122,c_7156]) ).
cnf(c_7158,plain,
( j(e24) = e14
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7157]) ).
cnf(c_7159,plain,
( j(e24) = e14
| j(e24) = e12
| j(e24) = e11
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7158]) ).
cnf(c_7160,plain,
( j(e24) = e14
| j(e24) = e12
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7159]) ).
cnf(c_5870,plain,
( j(e24) = e14
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7160]) ).
cnf(c_7161,plain,
( e14 = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_5870,c_5397]) ).
cnf(c_7162,plain,
( e14 = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7161]) ).
cnf(c_7163,plain,
( e14 = e13
| j(e24) = e12
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7162]) ).
cnf(c_7164,plain,
( e14 = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7163]) ).
cnf(c_5896,plain,
( j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(resolve,[status(thm)],[c_22,c_7164]) ).
cnf(c_5909,plain,
( op1(e12,j(e24)) = j(e24)
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_5896,c_373]) ).
cnf(c_7165,plain,
( op1(e12,e12) = j(e24)
| j(e24) = e11
| j(e24) = e10
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_5896,c_5909]) ).
cnf(c_7166,plain,
( e15 = j(e24)
| j(e24) = e11
| j(e24) = e10
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_114,c_7165]) ).
cnf(c_7167,plain,
( j(e24) = e15
| j(e24) = e11
| j(e24) = e10
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7166]) ).
cnf(c_7168,plain,
( j(e24) = e15
| j(e24) = e11
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7167]) ).
cnf(c_6311,plain,
( j(e24) = e15
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7168]) ).
cnf(c_7169,plain,
( e15 = e12
| j(e24) = e11
| j(e24) = e10
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_6311,c_5896]) ).
cnf(c_7170,plain,
( e15 = e12
| j(e24) = e11
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7169]) ).
cnf(c_7171,plain,
( e15 = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7170]) ).
cnf(c_6346,plain,
( j(e24) = e11
| j(e24) = e10 ),
inference(resolve,[status(thm)],[c_20,c_7171]) ).
cnf(c_6355,plain,
( op1(e11,j(e24)) = j(e24)
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_6346,c_373]) ).
cnf(c_7172,plain,
( op1(e11,e11) = j(e24)
| j(e24) = e10
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_6346,c_6355]) ).
cnf(c_7173,plain,
( e16 = j(e24)
| j(e24) = e10
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_106,c_7172]) ).
cnf(c_7174,plain,
( j(e24) = e16
| j(e24) = e10
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7173]) ).
cnf(c_6727,plain,
( j(e24) = e16
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7174]) ).
cnf(c_7175,plain,
( e16 = e11
| j(e24) = e10
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_6727,c_6346]) ).
cnf(c_7176,plain,
( e16 = e11
| j(e24) = e10 ),
inference(copy,[status(thm)],[c_7175]) ).
cnf(c_6758,plain,
j(e24) = e10,
inference(resolve,[status(thm)],[c_17,c_7176]) ).
cnf(c_7177,negated_conjecture,
op1(e10,j(e24)) = j(e24),
inference(paramod,[status(thm)],[c_6758,c_373]) ).
cnf(c_7178,negated_conjecture,
op1(e10,e10) = j(e24),
inference(paramod,[status(thm)],[c_6758,c_7177]) ).
cnf(c_7179,negated_conjecture,
e13 = j(e24),
inference(paramod,[status(thm)],[c_98,c_7178]) ).
cnf(c_7180,negated_conjecture,
e13 = e10,
inference(paramod,[status(thm)],[c_6758,c_7179]) ).
cnf(c_7130,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_9,c_7180]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG205+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 21:27:09 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3784695 was started by sandbox2 on n003,
% 0.10/0.36 % Sat Sep 26 21:27:09 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 22.30/3.27
% 22.30/3.27 % given #500 (T,wt=46): 498 h(e14) = e20 | h(e14) = e21 | h(e14) = e22 | h(e14) = e23 | h(e14) = e24 | h(e14) = e25 | op2(h(e15),e26) = h(e15). [para(200(g,1),289(a,1,2))].
% 22.30/3.27
% 22.30/3.27 % SZS status Theorem for theBenchmark
% 22.30/3.27
% 22.30/3.27 % Proof 1 at 2.46 (+ 0.34) seconds.
% 22.30/3.27 % Length of proof is 35.
% 22.30/3.27 % Level of proof is 18.
% 22.30/3.27 % Maximum clause weight is 46.000.
% 22.30/3.27 % Given clauses 776.
% 22.30/3.27
% 22.30/3.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------