%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG204+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 3.02s 16.34s
% Output : CNFRefutation 3.02s
% 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) = e26
& op2(e26,e25) = e22
& op2(e26,e24) = e23
& op2(e26,e23) = e21
& op2(e26,e22) = e20
& op2(e26,e21) = e24
& op2(e26,e20) = e25
& op2(e25,e26) = e22
& op2(e25,e25) = e25
& op2(e25,e24) = e21
& op2(e25,e23) = e26
& op2(e25,e22) = e23
& op2(e25,e21) = e20
& op2(e25,e20) = e24
& op2(e24,e26) = e23
& op2(e24,e25) = e21
& op2(e24,e24) = e24
& op2(e24,e23) = e20
& op2(e24,e22) = e25
& op2(e24,e21) = e22
& op2(e24,e20) = e26
& op2(e23,e26) = e21
& op2(e23,e25) = e26
& op2(e23,e24) = e20
& op2(e23,e23) = e23
& op2(e23,e22) = e24
& op2(e23,e21) = e25
& op2(e23,e20) = e22
& op2(e22,e26) = e20
& op2(e22,e25) = e23
& op2(e22,e24) = e25
& op2(e22,e23) = e24
& op2(e22,e22) = e22
& op2(e22,e21) = e26
& op2(e22,e20) = e21
& op2(e21,e26) = e24
& op2(e21,e25) = e20
& op2(e21,e24) = e22
& op2(e21,e23) = e25
& op2(e21,e22) = e26
& op2(e21,e21) = e21
& op2(e21,e20) = e23
& op2(e20,e26) = e25
& op2(e20,e25) = e24
& op2(e20,e24) = e26
& op2(e20,e23) = e22
& op2(e20,e22) = e21
& op2(e20,e21) = e23
& op2(e20,e20) = e20 ),
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_147,plain,
op2(e20,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_308,negated_conjecture,
j(op2(e20,e20)) = op1(j(e20),j(e20)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1858,negated_conjecture,
j(e20) = op1(j(e20),j(e20)),
inference(paramod,[status(thm)],[c_147,c_308]) ).
cnf(c_309,negated_conjecture,
op1(j(e20),j(e20)) = j(e20),
inference(copy,[status(thm)],[c_1858]) ).
cnf(c_666,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(paramod,[status(thm)],[c_203,c_309]) ).
cnf(c_1859,plain,
( op1(e16,e16) = 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_203,c_666]) ).
cnf(c_1860,plain,
( e10 = 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_1859]) ).
cnf(c_1861,plain,
( j(e20) = e10
| 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(copy,[status(thm)],[c_1860]) ).
cnf(c_1862,plain,
( j(e20) = e10
| 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_1861]) ).
cnf(c_1863,plain,
( j(e20) = e10
| 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_1862]) ).
cnf(c_1864,plain,
( j(e20) = e10
| 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_1863]) ).
cnf(c_1865,plain,
( j(e20) = e10
| 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_1864]) ).
cnf(c_1866,plain,
( j(e20) = e10
| 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_1865]) ).
cnf(c_1867,plain,
( j(e20) = e10
| j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1866]) ).
cnf(c_861,plain,
( j(e20) = e15
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1867]) ).
cnf(c_862,plain,
( op1(e15,j(e20)) = j(e20)
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_861,c_309]) ).
cnf(c_1868,plain,
( op1(e15,e15) = j(e20)
| 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_861,c_862]) ).
cnf(c_1869,plain,
( e11 = j(e20)
| 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_1868]) ).
cnf(c_1870,plain,
( j(e20) = e11
| 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_1869]) ).
cnf(c_1871,plain,
( j(e20) = e11
| 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_1870]) ).
cnf(c_1872,plain,
( j(e20) = e11
| 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_1871]) ).
cnf(c_1873,plain,
( j(e20) = e11
| 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_1872]) ).
cnf(c_1874,plain,
( j(e20) = e11
| j(e20) = e14
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1873]) ).
cnf(c_1875,plain,
( j(e20) = e11
| j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1874]) ).
cnf(c_935,plain,
( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1875]) ).
cnf(c_936,plain,
( op1(e14,j(e20)) = j(e20)
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_935,c_309]) ).
cnf(c_1876,plain,
( op1(e14,e14) = j(e20)
| 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_935,c_936]) ).
cnf(c_1877,plain,
( e12 = j(e20)
| 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_1876]) ).
cnf(c_1878,plain,
( j(e20) = e12
| 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_1877]) ).
cnf(c_1879,plain,
( j(e20) = e12
| 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_1878]) ).
cnf(c_1880,plain,
( j(e20) = e12
| j(e20) = e13
| j(e20) = e12
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1879]) ).
cnf(c_1881,plain,
( j(e20) = e12
| j(e20) = e13
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1880]) ).
cnf(c_1882,plain,
( j(e20) = e12
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1881]) ).
cnf(c_1017,plain,
( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1882]) ).
cnf(c_1018,plain,
( op1(e13,j(e20)) = j(e20)
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1017,c_309]) ).
cnf(c_1883,plain,
( op1(e13,e13) = j(e20)
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1017,c_1018]) ).
cnf(c_1884,plain,
( e14 = j(e20)
| 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_1883]) ).
cnf(c_1885,plain,
( j(e20) = e14
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1884]) ).
cnf(c_1886,plain,
( j(e20) = e14
| j(e20) = e12
| j(e20) = e11
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1885]) ).
cnf(c_1887,plain,
( j(e20) = e14
| j(e20) = e12
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1886]) ).
cnf(c_1132,plain,
( j(e20) = e14
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1887]) ).
cnf(c_1888,plain,
( e14 = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1132,c_1017]) ).
cnf(c_1889,plain,
( e14 = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1888]) ).
cnf(c_1890,plain,
( e14 = e13
| j(e20) = e12
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1889]) ).
cnf(c_1891,plain,
( e14 = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1890]) ).
cnf(c_1241,plain,
( j(e20) = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_22,c_1891]) ).
cnf(c_1242,plain,
( op1(e12,j(e20)) = j(e20)
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1241,c_309]) ).
cnf(c_1892,plain,
( op1(e12,e12) = j(e20)
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1241,c_1242]) ).
cnf(c_1893,plain,
( e15 = j(e20)
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_114,c_1892]) ).
cnf(c_1894,plain,
( j(e20) = e15
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1893]) ).
cnf(c_1895,plain,
( j(e20) = e15
| j(e20) = e11
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1894]) ).
cnf(c_1359,plain,
( j(e20) = e15
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1895]) ).
cnf(c_1896,plain,
( e15 = e12
| j(e20) = e11
| j(e20) = e10
| j(e20) = e11
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1359,c_1241]) ).
cnf(c_1897,plain,
( e15 = e12
| j(e20) = e11
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1896]) ).
cnf(c_1898,plain,
( e15 = e12
| j(e20) = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1897]) ).
cnf(c_1478,plain,
( j(e20) = e11
| j(e20) = e10 ),
inference(resolve,[status(thm)],[c_20,c_1898]) ).
cnf(c_1479,plain,
( op1(e11,j(e20)) = j(e20)
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1478,c_309]) ).
cnf(c_1899,plain,
( op1(e11,e11) = j(e20)
| j(e20) = e10
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1478,c_1479]) ).
cnf(c_1900,plain,
( e16 = j(e20)
| j(e20) = e10
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_106,c_1899]) ).
cnf(c_1901,plain,
( j(e20) = e16
| j(e20) = e10
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1900]) ).
cnf(c_1609,plain,
( j(e20) = e16
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1901]) ).
cnf(c_1902,plain,
( e16 = e11
| j(e20) = e10
| j(e20) = e10 ),
inference(paramod,[status(thm)],[c_1609,c_1478]) ).
cnf(c_1903,plain,
( e16 = e11
| j(e20) = e10 ),
inference(copy,[status(thm)],[c_1902]) ).
cnf(c_1734,plain,
j(e20) = e10,
inference(resolve,[status(thm)],[c_17,c_1903]) ).
cnf(c_1904,negated_conjecture,
op1(e10,j(e20)) = j(e20),
inference(paramod,[status(thm)],[c_1734,c_309]) ).
cnf(c_1905,negated_conjecture,
op1(e10,e10) = j(e20),
inference(paramod,[status(thm)],[c_1734,c_1904]) ).
cnf(c_1906,negated_conjecture,
e13 = j(e20),
inference(paramod,[status(thm)],[c_98,c_1905]) ).
cnf(c_1907,negated_conjecture,
e13 = e10,
inference(paramod,[status(thm)],[c_1734,c_1906]) ).
cnf(c_1857,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_9,c_1907]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG204+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.04/15.46 % CPULimit : 300
% 0.04/15.46 % WCLimit : 300
% 0.04/15.46 % DateTime : Sat Sep 26 21:28:06 UTC 2026
% 0.04/15.46 % CPUTime :
% 0.04/15.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.04/15.46 % Process 2714353 was started by sandbox on n002,
% 0.04/15.46 % Sat Sep 26 21:28:06 2026
% 0.04/15.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.04/15.47
% 0.04/15.47 % From the command line: assign(max_seconds, 300).
% 3.02/16.34
% 3.02/16.34 % SZS status Theorem for theBenchmark
% 3.02/16.34
% 3.02/16.34 % Proof 1 at 0.36 (+ 0.05) seconds.
% 3.02/16.34 % Length of proof is 35.
% 3.02/16.34 % Level of proof is 18.
% 3.02/16.34 % Maximum clause weight is 46.000.
% 3.02/16.34 % Given clauses 338.
% 3.02/16.34
% 3.02/16.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------