%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG080+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:26 AM UTC 2026
% Result : Theorem 3.14s 0.81s
% Output : CNFRefutation 3.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 5
% Syntax : Number of formulae : 294 ( 93 unt; 0 def)
% Number of atoms : 1209 (1208 equ)
% Maximal formula atoms : 110 ( 4 avg)
% Number of connectives : 951 ( 36 ~; 711 |; 202 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( e13 != e14
& e12 != e14
& e12 != e13
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('theBenchmark.p',ax1) ).
fof(ax2,axiom,
( e23 != e24
& e22 != e24
& e22 != e23
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('theBenchmark.p',ax2) ).
fof(ax4,axiom,
( op1(e14,e14) = e12
& op1(e14,e13) = e11
& op1(e14,e12) = e10
& op1(e14,e11) = e13
& op1(e14,e10) = e14
& op1(e13,e14) = e10
& op1(e13,e13) = e14
& op1(e13,e12) = e11
& op1(e13,e11) = e12
& op1(e13,e10) = e13
& op1(e12,e14) = e11
& op1(e12,e13) = e10
& op1(e12,e12) = e13
& op1(e12,e11) = e14
& op1(e12,e10) = e12
& op1(e11,e14) = e13
& op1(e11,e13) = e12
& op1(e11,e12) = e14
& op1(e11,e11) = e10
& op1(e11,e10) = e11
& op1(e10,e14) = e14
& op1(e10,e13) = e13
& op1(e10,e12) = e12
& op1(e10,e11) = e11
& op1(e10,e10) = e10 ),
file('theBenchmark.p',ax4) ).
fof(ax5,axiom,
( op2(e24,e24) = e20
& op2(e24,e23) = e22
& op2(e24,e22) = e21
& op2(e24,e21) = e23
& op2(e24,e20) = e24
& op2(e23,e24) = e22
& op2(e23,e23) = e21
& op2(e23,e22) = e20
& op2(e23,e21) = e24
& op2(e23,e20) = e23
& op2(e22,e24) = e21
& op2(e22,e23) = e24
& op2(e22,e22) = e23
& op2(e22,e21) = e20
& op2(e22,e20) = e22
& op2(e21,e24) = e23
& op2(e21,e23) = e20
& op2(e21,e22) = e24
& op2(e21,e21) = e22
& op2(e21,e20) = e21
& op2(e20,e24) = e24
& op2(e20,e23) = e23
& op2(e20,e22) = e22
& op2(e20,e21) = e21
& op2(e20,e20) = e20 ),
file('theBenchmark.p',ax5) ).
fof(co1,conjecture,
( ( ( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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,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(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,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,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,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,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(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 )
& ( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 )
& ( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 )
& ( j(e21) = e14
| j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10 )
& ( j(e20) = e14
| j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10 )
& ( h(e14) = e24
| h(e14) = e23
| h(e14) = e22
| h(e14) = e21
| h(e14) = e20 )
& ( h(e13) = e24
| h(e13) = e23
| h(e13) = e22
| h(e13) = e21
| h(e13) = e20 )
& ( h(e12) = e24
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 )
& ( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 )
& ( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ) )
=> ~ ( j(h(e14)) = e14
& j(h(e13)) = e13
& j(h(e12)) = e12
& j(h(e11)) = e11
& j(h(e10)) = e10
& h(j(e24)) = e24
& h(j(e23)) = e23
& h(j(e22)) = e22
& h(j(e21)) = e21
& h(j(e20)) = e20
& 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,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,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,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,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(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,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,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,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,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_7,plain,
e11 != e10,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_8,plain,
e12 != e10,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_9,plain,
e13 != e10,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_10,plain,
e14 != e10,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_15,plain,
e14 != e12,
inference(clausify,[status(thm)],[ax1]) ).
cnf(c_18,plain,
e22 != e20,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_19,plain,
e23 != e20,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_20,plain,
e24 != e20,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_21,plain,
e22 != e21,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_23,plain,
e24 != e21,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_24,plain,
e23 != e22,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_25,plain,
e24 != e22,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_26,plain,
e24 != e23,
inference(clausify,[status(thm)],[ax2]) ).
cnf(c_52,plain,
op1(e10,e10) = e10,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_59,plain,
op1(e11,e12) = e14,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_60,plain,
op1(e11,e13) = e12,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_61,plain,
op1(e11,e14) = e13,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_64,plain,
op1(e12,e12) = e13,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_68,plain,
op1(e13,e11) = e12,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_69,plain,
op1(e13,e12) = e11,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_70,plain,
op1(e13,e13) = e14,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_71,plain,
op1(e13,e14) = e10,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_72,plain,
op1(e14,e10) = e14,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_75,plain,
op1(e14,e13) = e11,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_76,plain,
op1(e14,e14) = e12,
inference(clausify,[status(thm)],[ax4]) ).
cnf(c_83,plain,
op2(e21,e21) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_85,plain,
op2(e21,e23) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_87,plain,
op2(e22,e20) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_89,plain,
op2(e22,e22) = e23,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_93,plain,
op2(e23,e21) = e24,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_94,plain,
op2(e23,e22) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_95,plain,
op2(e23,e23) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_96,plain,
op2(e23,e24) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_98,plain,
op2(e24,e21) = e23,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_99,plain,
op2(e24,e22) = e21,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_100,plain,
op2(e24,e23) = e22,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_101,plain,
op2(e24,e24) = e20,
inference(clausify,[status(thm)],[ax5]) ).
cnf(c_102,negated_conjecture,
( h(e10) = e24
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_103,negated_conjecture,
( h(e11) = e24
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_109,negated_conjecture,
( j(e22) = e14
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_110,negated_conjecture,
( j(e23) = e14
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_111,negated_conjecture,
( j(e24) = e14
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_112,negated_conjecture,
h(op1(e10,e10)) = op2(h(e10),h(e10)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1825,negated_conjecture,
h(e10) = op2(h(e10),h(e10)),
inference(paramod,[status(thm)],[c_52,c_112]) ).
cnf(c_113,negated_conjecture,
op2(h(e10),h(e10)) = h(e10),
inference(copy,[status(thm)],[c_1825]) ).
cnf(c_130,negated_conjecture,
h(op1(e11,e14)) = op2(h(e11),h(e14)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1826,negated_conjecture,
h(e13) = op2(h(e11),h(e14)),
inference(paramod,[status(thm)],[c_61,c_130]) ).
cnf(c_131,negated_conjecture,
op2(h(e11),h(e14)) = h(e13),
inference(copy,[status(thm)],[c_1826]) ).
cnf(c_144,negated_conjecture,
h(op1(e13,e11)) = op2(h(e13),h(e11)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1827,negated_conjecture,
h(e12) = op2(h(e13),h(e11)),
inference(paramod,[status(thm)],[c_68,c_144]) ).
cnf(c_145,negated_conjecture,
op2(h(e13),h(e11)) = h(e12),
inference(copy,[status(thm)],[c_1827]) ).
cnf(c_146,negated_conjecture,
h(op1(e13,e12)) = op2(h(e13),h(e12)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1828,negated_conjecture,
h(e11) = op2(h(e13),h(e12)),
inference(paramod,[status(thm)],[c_69,c_146]) ).
cnf(c_147,negated_conjecture,
op2(h(e13),h(e12)) = h(e11),
inference(copy,[status(thm)],[c_1828]) ).
cnf(c_150,negated_conjecture,
h(op1(e13,e14)) = op2(h(e13),h(e14)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1829,negated_conjecture,
h(e10) = op2(h(e13),h(e14)),
inference(paramod,[status(thm)],[c_71,c_150]) ).
cnf(c_151,negated_conjecture,
op2(h(e13),h(e14)) = h(e10),
inference(copy,[status(thm)],[c_1829]) ).
cnf(c_152,negated_conjecture,
h(op1(e14,e10)) = op2(h(e14),h(e10)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1830,negated_conjecture,
h(e14) = op2(h(e14),h(e10)),
inference(paramod,[status(thm)],[c_72,c_152]) ).
cnf(c_153,negated_conjecture,
op2(h(e14),h(e10)) = h(e14),
inference(copy,[status(thm)],[c_1830]) ).
cnf(c_196,negated_conjecture,
j(op2(e23,e22)) = op1(j(e23),j(e22)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1831,negated_conjecture,
j(e20) = op1(j(e23),j(e22)),
inference(paramod,[status(thm)],[c_94,c_196]) ).
cnf(c_197,negated_conjecture,
op1(j(e23),j(e22)) = j(e20),
inference(copy,[status(thm)],[c_1831]) ).
cnf(c_204,negated_conjecture,
j(op2(e24,e21)) = op1(j(e24),j(e21)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1832,negated_conjecture,
j(e23) = op1(j(e24),j(e21)),
inference(paramod,[status(thm)],[c_98,c_204]) ).
cnf(c_205,negated_conjecture,
op1(j(e24),j(e21)) = j(e23),
inference(copy,[status(thm)],[c_1832]) ).
cnf(c_206,negated_conjecture,
j(op2(e24,e22)) = op1(j(e24),j(e22)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1833,negated_conjecture,
j(e21) = op1(j(e24),j(e22)),
inference(paramod,[status(thm)],[c_99,c_206]) ).
cnf(c_207,negated_conjecture,
op1(j(e24),j(e22)) = j(e21),
inference(copy,[status(thm)],[c_1833]) ).
cnf(c_208,negated_conjecture,
j(op2(e24,e23)) = op1(j(e24),j(e23)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1834,negated_conjecture,
j(e22) = op1(j(e24),j(e23)),
inference(paramod,[status(thm)],[c_100,c_208]) ).
cnf(c_209,negated_conjecture,
op1(j(e24),j(e23)) = j(e22),
inference(copy,[status(thm)],[c_1834]) ).
cnf(c_210,negated_conjecture,
j(op2(e24,e24)) = op1(j(e24),j(e24)),
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_1835,negated_conjecture,
j(e20) = op1(j(e24),j(e24)),
inference(paramod,[status(thm)],[c_101,c_210]) ).
cnf(c_211,negated_conjecture,
op1(j(e24),j(e24)) = j(e20),
inference(copy,[status(thm)],[c_1835]) ).
cnf(c_213,negated_conjecture,
h(j(e21)) = e21,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_214,negated_conjecture,
h(j(e22)) = e22,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_215,negated_conjecture,
h(j(e23)) = e23,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_216,negated_conjecture,
h(j(e24)) = e24,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_217,negated_conjecture,
j(h(e10)) = e10,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_218,negated_conjecture,
j(h(e11)) = e11,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_219,negated_conjecture,
j(h(e12)) = e12,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_220,negated_conjecture,
j(h(e13)) = e13,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_221,negated_conjecture,
j(h(e14)) = e14,
inference(clausify,[status(thm)],[co1_neg]) ).
cnf(c_222,plain,
( op2(e24,h(e10)) = h(e10)
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_102,c_113]) ).
cnf(c_240,plain,
( op2(e24,h(e14)) = h(e13)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_103,c_131]) ).
cnf(c_254,plain,
( op2(h(e13),e24) = h(e12)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_103,c_145]) ).
cnf(c_324,plain,
( h(e14) = e22
| j(e22) = e13
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(paramod,[status(thm)],[c_109,c_214]) ).
cnf(c_325,plain,
( h(e14) = e23
| j(e23) = e13
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 ),
inference(paramod,[status(thm)],[c_110,c_215]) ).
cnf(c_326,plain,
( h(e14) = e24
| j(e24) = e13
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_111,c_216]) ).
cnf(c_328,plain,
( j(e24) = e11
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_103,c_218]) ).
cnf(c_1836,plain,
( op2(e24,e24) = h(e10)
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_102,c_222]) ).
cnf(c_1837,plain,
( e20 = h(e10)
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_101,c_1836]) ).
cnf(c_1838,plain,
( h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1837]) ).
cnf(c_1839,plain,
( h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1838]) ).
cnf(c_1840,plain,
( h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1839]) ).
cnf(c_1841,plain,
( h(e10) = e20
| h(e10) = e23
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1840]) ).
cnf(c_1842,plain,
( h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1841]) ).
cnf(c_332,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1842]) ).
cnf(c_333,plain,
( op2(e23,h(e10)) = h(e10)
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_332,c_113]) ).
cnf(c_386,plain,
( h(e13) = e22
| h(e14) = e22
| j(e22) = e12
| j(e22) = e11
| j(e22) = e10 ),
inference(paramod,[status(thm)],[c_324,c_214]) ).
cnf(c_397,plain,
( h(e13) = e23
| h(e14) = e23
| j(e23) = e12
| j(e23) = e11
| j(e23) = e10 ),
inference(paramod,[status(thm)],[c_325,c_215]) ).
cnf(c_410,plain,
( h(e13) = e24
| h(e14) = e24
| j(e24) = e12
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_326,c_216]) ).
cnf(c_416,plain,
( op1(e11,j(e21)) = j(e23)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_328,c_205]) ).
cnf(c_417,plain,
( op1(e11,j(e22)) = j(e21)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_328,c_207]) ).
cnf(c_418,plain,
( op1(e11,j(e23)) = j(e22)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20 ),
inference(paramod,[status(thm)],[c_328,c_209]) ).
cnf(c_491,plain,
( h(e12) = e22
| h(e13) = e22
| h(e14) = e22
| j(e22) = e11
| j(e22) = e10 ),
inference(paramod,[status(thm)],[c_386,c_214]) ).
cnf(c_502,plain,
( h(e12) = e23
| h(e13) = e23
| h(e14) = e23
| j(e23) = e11
| j(e23) = e10 ),
inference(paramod,[status(thm)],[c_397,c_215]) ).
cnf(c_513,plain,
( h(e12) = e24
| h(e13) = e24
| h(e14) = e24
| j(e24) = e11
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_410,c_216]) ).
cnf(c_548,plain,
( h(e11) = e22
| h(e12) = e22
| h(e13) = e22
| h(e14) = e22
| j(e22) = e10 ),
inference(paramod,[status(thm)],[c_491,c_214]) ).
cnf(c_559,plain,
( h(e11) = e23
| h(e12) = e23
| h(e13) = e23
| h(e14) = e23
| j(e23) = e10 ),
inference(paramod,[status(thm)],[c_502,c_215]) ).
cnf(c_570,plain,
( h(e11) = e24
| h(e12) = e24
| h(e13) = e24
| h(e14) = e24
| j(e24) = e10 ),
inference(paramod,[status(thm)],[c_513,c_216]) ).
cnf(c_603,plain,
( h(e10) = e22
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22
| h(e14) = e22 ),
inference(paramod,[status(thm)],[c_548,c_214]) ).
cnf(c_616,plain,
( h(e10) = e23
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23
| h(e14) = e23 ),
inference(paramod,[status(thm)],[c_559,c_215]) ).
cnf(c_627,plain,
( h(e10) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24
| h(e14) = e24 ),
inference(paramod,[status(thm)],[c_570,c_216]) ).
cnf(c_655,plain,
( op2(e22,h(e10)) = h(e14)
| h(e10) = e22
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_603,c_153]) ).
cnf(c_674,plain,
( j(e23) = e14
| h(e10) = e23
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_616,c_221]) ).
cnf(c_689,plain,
( j(e24) = e14
| h(e10) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_627,c_221]) ).
cnf(c_729,plain,
( op1(e14,j(e22)) = j(e20)
| h(e10) = e23
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_674,c_197]) ).
cnf(c_733,plain,
( op1(j(e24),e14) = j(e22)
| h(e10) = e23
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_674,c_209]) ).
cnf(c_742,plain,
( op1(e14,j(e24)) = j(e20)
| h(e10) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_689,c_211]) ).
cnf(c_1843,plain,
( op2(e23,e23) = h(e10)
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_332,c_333]) ).
cnf(c_1844,plain,
( e21 = h(e10)
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_95,c_1843]) ).
cnf(c_1845,plain,
( h(e10) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1844]) ).
cnf(c_1846,plain,
( h(e10) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1845]) ).
cnf(c_1847,plain,
( h(e10) = e21
| h(e10) = e22
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1846]) ).
cnf(c_1848,plain,
( h(e10) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1847]) ).
cnf(c_767,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1848]) ).
cnf(c_768,plain,
( op2(e22,h(e10)) = h(e10)
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_767,c_113]) ).
cnf(c_1849,plain,
( op2(e22,e22) = h(e10)
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_767,c_768]) ).
cnf(c_1850,plain,
( e23 = h(e10)
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_89,c_1849]) ).
cnf(c_1851,plain,
( h(e10) = e23
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1850]) ).
cnf(c_1852,plain,
( h(e10) = e23
| h(e10) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1851]) ).
cnf(c_792,plain,
( h(e10) = e23
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1852]) ).
cnf(c_1853,plain,
( e23 = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_792,c_767]) ).
cnf(c_1854,plain,
( e23 = e22
| h(e10) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1853]) ).
cnf(c_1855,plain,
( e23 = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1854]) ).
cnf(c_805,plain,
( h(e10) = e21
| h(e10) = e20 ),
inference(resolve,[status(thm)],[c_24,c_1855]) ).
cnf(c_806,plain,
( op2(e21,h(e10)) = h(e10)
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_805,c_113]) ).
cnf(c_1856,plain,
( op2(e21,e21) = h(e10)
| h(e10) = e20
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_805,c_806]) ).
cnf(c_1857,plain,
( e22 = h(e10)
| h(e10) = e20
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_83,c_1856]) ).
cnf(c_1858,plain,
( h(e10) = e22
| h(e10) = e20
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1857]) ).
cnf(c_830,plain,
( h(e10) = e22
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1858]) ).
cnf(c_1859,plain,
( e22 = e21
| h(e10) = e20
| h(e10) = e20 ),
inference(paramod,[status(thm)],[c_830,c_805]) ).
cnf(c_1860,plain,
( e22 = e21
| h(e10) = e20 ),
inference(copy,[status(thm)],[c_1859]) ).
cnf(c_843,plain,
h(e10) = e20,
inference(resolve,[status(thm)],[c_21,c_1860]) ).
cnf(c_1861,plain,
( op1(e14,j(e24)) = j(e20)
| e20 = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_843,c_742]) ).
cnf(c_1862,plain,
( op1(e14,j(e24)) = j(e20)
| e24 = e20
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(copy,[status(thm)],[c_1861]) ).
cnf(c_845,plain,
( op1(e14,j(e24)) = j(e20)
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(resolve,[status(thm)],[c_20,c_1862]) ).
cnf(c_1863,plain,
( op1(j(e24),e14) = j(e22)
| e20 = e23
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_843,c_733]) ).
cnf(c_1864,plain,
( op1(j(e24),e14) = j(e22)
| e23 = e20
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(copy,[status(thm)],[c_1863]) ).
cnf(c_854,plain,
( op1(j(e24),e14) = j(e22)
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(resolve,[status(thm)],[c_19,c_1864]) ).
cnf(c_1865,plain,
( op1(e14,j(e22)) = j(e20)
| e20 = e23
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_843,c_729]) ).
cnf(c_1866,plain,
( op1(e14,j(e22)) = j(e20)
| e23 = e20
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(copy,[status(thm)],[c_1865]) ).
cnf(c_858,plain,
( op1(e14,j(e22)) = j(e20)
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(resolve,[status(thm)],[c_19,c_1866]) ).
cnf(c_1867,plain,
( j(e24) = e14
| e20 = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_843,c_689]) ).
cnf(c_1868,plain,
( j(e24) = e14
| e24 = e20
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(copy,[status(thm)],[c_1867]) ).
cnf(c_887,plain,
( j(e24) = e14
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(resolve,[status(thm)],[c_20,c_1868]) ).
cnf(c_1869,plain,
( op2(e22,h(e10)) = h(e14)
| e20 = e22
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_843,c_655]) ).
cnf(c_1870,plain,
( op2(e22,e20) = h(e14)
| e20 = e22
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_843,c_1869]) ).
cnf(c_1871,plain,
( e22 = h(e14)
| e20 = e22
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_87,c_1870]) ).
cnf(c_1872,plain,
( e22 = h(e14)
| e22 = e20
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(copy,[status(thm)],[c_1871]) ).
cnf(c_1873,plain,
( h(e14) = e22
| e22 = e20
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(copy,[status(thm)],[c_1872]) ).
cnf(c_916,plain,
( h(e14) = e22
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(resolve,[status(thm)],[c_18,c_1873]) ).
cnf(c_938,negated_conjecture,
j(e20) = e10,
inference(paramod,[status(thm)],[c_843,c_217]) ).
cnf(c_941,negated_conjecture,
op2(h(e13),h(e14)) = e20,
inference(paramod,[status(thm)],[c_843,c_151]) ).
cnf(c_956,plain,
( op1(e14,j(e22)) = e10
| h(e11) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_938,c_858]) ).
cnf(c_957,plain,
( op1(e14,j(e24)) = e10
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_938,c_845]) ).
cnf(c_999,negated_conjecture,
op1(j(e24),j(e24)) = e10,
inference(paramod,[status(thm)],[c_938,c_211]) ).
cnf(c_1874,plain,
( op2(e24,e22) = h(e13)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_916,c_240]) ).
cnf(c_1875,plain,
( e21 = h(e13)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_99,c_1874]) ).
cnf(c_1876,plain,
( h(e13) = e21
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| h(e11) = e20
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(copy,[status(thm)],[c_1875]) ).
cnf(c_1016,plain,
( h(e13) = e21
| h(e11) = e23
| h(e11) = e21
| h(e11) = e20
| h(e11) = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(copy,[status(thm)],[c_1876]) ).
cnf(c_1877,plain,
( op1(e14,e14) = e10
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_887,c_957]) ).
cnf(c_1878,plain,
( e12 = e10
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(paramod,[status(thm)],[c_76,c_1877]) ).
cnf(c_1879,plain,
( e12 = e10
| h(e11) = e24
| h(e12) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(copy,[status(thm)],[c_1878]) ).
cnf(c_1880,plain,
( e12 = e10
| h(e11) = e24
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(copy,[status(thm)],[c_1879]) ).
cnf(c_1881,plain,
( e12 = e10
| h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(copy,[status(thm)],[c_1880]) ).
cnf(c_1049,plain,
( h(e11) = e24
| h(e12) = e24
| h(e13) = e24 ),
inference(resolve,[status(thm)],[c_8,c_1881]) ).
cnf(c_1057,plain,
( j(e24) = e13
| h(e11) = e24
| h(e12) = e24 ),
inference(paramod,[status(thm)],[c_1049,c_220]) ).
cnf(c_1071,plain,
( op1(e13,j(e24)) = e10
| h(e11) = e24
| h(e12) = e24 ),
inference(paramod,[status(thm)],[c_1057,c_999]) ).
cnf(c_1882,plain,
( op1(e13,e13) = e10
| h(e11) = e24
| h(e12) = e24
| h(e11) = e24
| h(e12) = e24 ),
inference(paramod,[status(thm)],[c_1057,c_1071]) ).
cnf(c_1883,plain,
( e14 = e10
| h(e11) = e24
| h(e12) = e24
| h(e11) = e24
| h(e12) = e24 ),
inference(paramod,[status(thm)],[c_70,c_1882]) ).
cnf(c_1884,plain,
( e14 = e10
| h(e11) = e24
| h(e11) = e24
| h(e12) = e24 ),
inference(copy,[status(thm)],[c_1883]) ).
cnf(c_1885,plain,
( e14 = e10
| h(e11) = e24
| h(e12) = e24 ),
inference(copy,[status(thm)],[c_1884]) ).
cnf(c_1075,plain,
( h(e11) = e24
| h(e12) = e24 ),
inference(resolve,[status(thm)],[c_10,c_1885]) ).
cnf(c_1082,plain,
( j(e24) = e12
| h(e11) = e24 ),
inference(paramod,[status(thm)],[c_1075,c_219]) ).
cnf(c_1097,plain,
( op1(e12,j(e24)) = e10
| h(e11) = e24 ),
inference(paramod,[status(thm)],[c_1082,c_999]) ).
cnf(c_1886,plain,
( op1(e12,e12) = e10
| h(e11) = e24
| h(e11) = e24 ),
inference(paramod,[status(thm)],[c_1082,c_1097]) ).
cnf(c_1887,plain,
( e13 = e10
| h(e11) = e24
| h(e11) = e24 ),
inference(paramod,[status(thm)],[c_64,c_1886]) ).
cnf(c_1888,plain,
( e13 = e10
| h(e11) = e24 ),
inference(copy,[status(thm)],[c_1887]) ).
cnf(c_1101,plain,
h(e11) = e24,
inference(resolve,[status(thm)],[c_9,c_1888]) ).
cnf(c_1889,plain,
( h(e13) = e21
| h(e11) = e23
| h(e11) = e21
| h(e11) = e20
| e24 = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_1101,c_1016]) ).
cnf(c_1890,plain,
( h(e13) = e21
| h(e11) = e23
| h(e11) = e21
| e24 = e20
| e24 = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_1101,c_1889]) ).
cnf(c_1891,plain,
( h(e13) = e21
| h(e11) = e23
| e24 = e21
| e24 = e20
| e24 = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_1101,c_1890]) ).
cnf(c_1892,plain,
( h(e13) = e21
| e24 = e23
| e24 = e21
| e24 = e20
| e24 = e22
| h(e12) = e22
| h(e13) = e22 ),
inference(paramod,[status(thm)],[c_1101,c_1891]) ).
cnf(c_1893,plain,
( h(e13) = e21
| e24 = e23
| e24 = e21
| e24 = e20
| h(e12) = e22
| h(e13) = e22 ),
inference(resolve,[status(thm)],[c_25,c_1892]) ).
cnf(c_1894,plain,
( h(e13) = e21
| e24 = e23
| e24 = e21
| h(e12) = e22
| h(e13) = e22 ),
inference(resolve,[status(thm)],[c_20,c_1893]) ).
cnf(c_1895,plain,
( h(e13) = e21
| e24 = e23
| h(e12) = e22
| h(e13) = e22 ),
inference(resolve,[status(thm)],[c_23,c_1894]) ).
cnf(c_1131,plain,
( h(e13) = e21
| h(e12) = e22
| h(e13) = e22 ),
inference(resolve,[status(thm)],[c_26,c_1895]) ).
cnf(c_1896,plain,
( op1(e14,j(e22)) = e10
| e24 = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_1101,c_956]) ).
cnf(c_1137,plain,
( op1(e14,j(e22)) = e10
| h(e12) = e23
| h(e13) = e23 ),
inference(resolve,[status(thm)],[c_26,c_1896]) ).
cnf(c_1897,plain,
( op1(j(e24),e14) = j(e22)
| e24 = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_1101,c_854]) ).
cnf(c_1184,plain,
( op1(j(e24),e14) = j(e22)
| h(e12) = e23
| h(e13) = e23 ),
inference(resolve,[status(thm)],[c_26,c_1897]) ).
cnf(c_1898,plain,
( op1(e11,j(e23)) = j(e22)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_418]) ).
cnf(c_1899,plain,
( op1(e11,j(e23)) = j(e22)
| h(e11) = e23
| h(e11) = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1898]) ).
cnf(c_1900,plain,
( op1(e11,j(e23)) = j(e22)
| h(e11) = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1899]) ).
cnf(c_1901,plain,
( op1(e11,j(e23)) = j(e22)
| e24 = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1900]) ).
cnf(c_1902,plain,
( op1(e11,j(e23)) = j(e22)
| e24 = e23
| e24 = e22
| e24 = e21 ),
inference(resolve,[status(thm)],[c_20,c_1901]) ).
cnf(c_1903,plain,
( op1(e11,j(e23)) = j(e22)
| e24 = e23
| e24 = e22 ),
inference(resolve,[status(thm)],[c_23,c_1902]) ).
cnf(c_1904,plain,
( op1(e11,j(e23)) = j(e22)
| e24 = e23 ),
inference(resolve,[status(thm)],[c_25,c_1903]) ).
cnf(c_1188,plain,
op1(e11,j(e23)) = j(e22),
inference(resolve,[status(thm)],[c_26,c_1904]) ).
cnf(c_1905,plain,
( op1(e11,j(e22)) = j(e21)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_417]) ).
cnf(c_1906,plain,
( op1(e11,j(e22)) = j(e21)
| h(e11) = e23
| h(e11) = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1905]) ).
cnf(c_1907,plain,
( op1(e11,j(e22)) = j(e21)
| h(e11) = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1906]) ).
cnf(c_1908,plain,
( op1(e11,j(e22)) = j(e21)
| e24 = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1907]) ).
cnf(c_1909,plain,
( op1(e11,j(e22)) = j(e21)
| e24 = e23
| e24 = e22
| e24 = e21 ),
inference(resolve,[status(thm)],[c_20,c_1908]) ).
cnf(c_1910,plain,
( op1(e11,j(e22)) = j(e21)
| e24 = e23
| e24 = e22 ),
inference(resolve,[status(thm)],[c_23,c_1909]) ).
cnf(c_1911,plain,
( op1(e11,j(e22)) = j(e21)
| e24 = e23 ),
inference(resolve,[status(thm)],[c_25,c_1910]) ).
cnf(c_1189,plain,
op1(e11,j(e22)) = j(e21),
inference(resolve,[status(thm)],[c_26,c_1911]) ).
cnf(c_1912,plain,
( op1(e11,j(e21)) = j(e23)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_416]) ).
cnf(c_1913,plain,
( op1(e11,j(e21)) = j(e23)
| h(e11) = e23
| h(e11) = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1912]) ).
cnf(c_1914,plain,
( op1(e11,j(e21)) = j(e23)
| h(e11) = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1913]) ).
cnf(c_1915,plain,
( op1(e11,j(e21)) = j(e23)
| e24 = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1914]) ).
cnf(c_1916,plain,
( op1(e11,j(e21)) = j(e23)
| e24 = e23
| e24 = e22
| e24 = e21 ),
inference(resolve,[status(thm)],[c_20,c_1915]) ).
cnf(c_1917,plain,
( op1(e11,j(e21)) = j(e23)
| e24 = e23
| e24 = e22 ),
inference(resolve,[status(thm)],[c_23,c_1916]) ).
cnf(c_1918,plain,
( op1(e11,j(e21)) = j(e23)
| e24 = e23 ),
inference(resolve,[status(thm)],[c_25,c_1917]) ).
cnf(c_1190,plain,
op1(e11,j(e21)) = j(e23),
inference(resolve,[status(thm)],[c_26,c_1918]) ).
cnf(c_1919,plain,
( j(e24) = e11
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_328]) ).
cnf(c_1920,plain,
( j(e24) = e11
| h(e11) = e23
| h(e11) = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1919]) ).
cnf(c_1921,plain,
( j(e24) = e11
| h(e11) = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1920]) ).
cnf(c_1922,plain,
( j(e24) = e11
| e24 = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1921]) ).
cnf(c_1923,plain,
( j(e24) = e11
| e24 = e23
| e24 = e22
| e24 = e21 ),
inference(resolve,[status(thm)],[c_20,c_1922]) ).
cnf(c_1924,plain,
( j(e24) = e11
| e24 = e23
| e24 = e22 ),
inference(resolve,[status(thm)],[c_23,c_1923]) ).
cnf(c_1925,plain,
( j(e24) = e11
| e24 = e23 ),
inference(resolve,[status(thm)],[c_25,c_1924]) ).
cnf(c_1194,plain,
j(e24) = e11,
inference(resolve,[status(thm)],[c_26,c_1925]) ).
cnf(c_1926,plain,
( op2(h(e13),e24) = h(e12)
| h(e11) = e23
| h(e11) = e22
| h(e11) = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_254]) ).
cnf(c_1927,plain,
( op2(h(e13),e24) = h(e12)
| h(e11) = e23
| h(e11) = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1926]) ).
cnf(c_1928,plain,
( op2(h(e13),e24) = h(e12)
| h(e11) = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1927]) ).
cnf(c_1929,plain,
( op2(h(e13),e24) = h(e12)
| e24 = e23
| e24 = e22
| e24 = e21
| e24 = e20 ),
inference(paramod,[status(thm)],[c_1101,c_1928]) ).
cnf(c_1930,plain,
( op2(h(e13),e24) = h(e12)
| e24 = e23
| e24 = e22
| e24 = e21 ),
inference(resolve,[status(thm)],[c_20,c_1929]) ).
cnf(c_1931,plain,
( op2(h(e13),e24) = h(e12)
| e24 = e23
| e24 = e22 ),
inference(resolve,[status(thm)],[c_23,c_1930]) ).
cnf(c_1932,plain,
( op2(h(e13),e24) = h(e12)
| e24 = e23 ),
inference(resolve,[status(thm)],[c_25,c_1931]) ).
cnf(c_1196,plain,
op2(h(e13),e24) = h(e12),
inference(resolve,[status(thm)],[c_26,c_1932]) ).
cnf(c_1202,negated_conjecture,
op2(h(e13),h(e12)) = e24,
inference(paramod,[status(thm)],[c_1101,c_147]) ).
cnf(c_1933,plain,
( op1(e11,e14) = j(e22)
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_1194,c_1184]) ).
cnf(c_1934,plain,
( e13 = j(e22)
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_61,c_1933]) ).
cnf(c_1204,plain,
( j(e22) = e13
| h(e12) = e23
| h(e13) = e23 ),
inference(copy,[status(thm)],[c_1934]) ).
cnf(c_1251,plain,
( j(e22) = e13
| h(e13) = e21
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_1131,c_220]) ).
cnf(c_1935,plain,
( op1(e11,e13) = j(e21)
| h(e13) = e21
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_1251,c_1189]) ).
cnf(c_1936,plain,
( e12 = j(e21)
| h(e13) = e21
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_60,c_1935]) ).
cnf(c_1301,plain,
( j(e21) = e12
| h(e13) = e21
| h(e12) = e22 ),
inference(copy,[status(thm)],[c_1936]) ).
cnf(c_1937,plain,
( op1(e11,e12) = j(e23)
| h(e13) = e21
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_1301,c_1190]) ).
cnf(c_1938,plain,
( e14 = j(e23)
| h(e13) = e21
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_59,c_1937]) ).
cnf(c_1358,plain,
( j(e23) = e14
| h(e13) = e21
| h(e12) = e22 ),
inference(copy,[status(thm)],[c_1938]) ).
cnf(c_1939,plain,
( op1(e14,e13) = e10
| h(e12) = e23
| h(e13) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_1204,c_1137]) ).
cnf(c_1940,plain,
( e11 = e10
| h(e12) = e23
| h(e13) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(paramod,[status(thm)],[c_75,c_1939]) ).
cnf(c_1941,plain,
( e11 = e10
| h(e12) = e23
| h(e12) = e23
| h(e13) = e23 ),
inference(copy,[status(thm)],[c_1940]) ).
cnf(c_1942,plain,
( e11 = e10
| h(e12) = e23
| h(e13) = e23 ),
inference(copy,[status(thm)],[c_1941]) ).
cnf(c_1712,plain,
( h(e12) = e23
| h(e13) = e23 ),
inference(resolve,[status(thm)],[c_7,c_1942]) ).
cnf(c_1715,plain,
( j(e23) = e13
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1712,c_220]) ).
cnf(c_1716,plain,
( op2(e23,h(e14)) = e20
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1712,c_941]) ).
cnf(c_1943,plain,
( op2(e23,e24) = h(e12)
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1712,c_1196]) ).
cnf(c_1944,plain,
( e22 = h(e12)
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_96,c_1943]) ).
cnf(c_1719,plain,
( h(e12) = e22
| h(e12) = e23 ),
inference(copy,[status(thm)],[c_1944]) ).
cnf(c_1945,plain,
( op1(e11,e13) = j(e22)
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1715,c_1188]) ).
cnf(c_1946,plain,
( e12 = j(e22)
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_60,c_1945]) ).
cnf(c_1726,plain,
( j(e22) = e12
| h(e12) = e23 ),
inference(copy,[status(thm)],[c_1946]) ).
cnf(c_1732,plain,
( j(e23) = e12
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_1719,c_219]) ).
cnf(c_1947,plain,
( op1(e11,e12) = j(e21)
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1726,c_1189]) ).
cnf(c_1948,plain,
( e14 = j(e21)
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_59,c_1947]) ).
cnf(c_1750,plain,
( j(e21) = e14
| h(e12) = e23 ),
inference(copy,[status(thm)],[c_1948]) ).
cnf(c_1949,plain,
( e12 = e14
| h(e13) = e21
| h(e12) = e22
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_1732,c_1358]) ).
cnf(c_1950,plain,
( e14 = e12
| h(e13) = e21
| h(e12) = e22
| h(e12) = e22 ),
inference(copy,[status(thm)],[c_1949]) ).
cnf(c_1951,plain,
( e14 = e12
| h(e13) = e21
| h(e12) = e22 ),
inference(copy,[status(thm)],[c_1950]) ).
cnf(c_1766,plain,
( h(e13) = e21
| h(e12) = e22 ),
inference(resolve,[status(thm)],[c_15,c_1951]) ).
cnf(c_1775,plain,
( h(e14) = e21
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1750,c_213]) ).
cnf(c_1798,plain,
( op2(e21,h(e12)) = e24
| h(e12) = e22 ),
inference(paramod,[status(thm)],[c_1766,c_1202]) ).
cnf(c_1952,plain,
( op2(e23,e21) = e20
| h(e12) = e23
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_1775,c_1716]) ).
cnf(c_1953,plain,
( e24 = e20
| h(e12) = e23
| h(e12) = e23 ),
inference(paramod,[status(thm)],[c_93,c_1952]) ).
cnf(c_1954,plain,
( e24 = e20
| h(e12) = e23 ),
inference(copy,[status(thm)],[c_1953]) ).
cnf(c_1817,plain,
h(e12) = e23,
inference(resolve,[status(thm)],[c_20,c_1954]) ).
cnf(c_1955,plain,
( op2(e21,h(e12)) = e24
| e23 = e22 ),
inference(paramod,[status(thm)],[c_1817,c_1798]) ).
cnf(c_1956,plain,
( op2(e21,e23) = e24
| e23 = e22 ),
inference(paramod,[status(thm)],[c_1817,c_1955]) ).
cnf(c_1957,plain,
( e20 = e24
| e23 = e22 ),
inference(paramod,[status(thm)],[c_85,c_1956]) ).
cnf(c_1958,plain,
( e24 = e20
| e23 = e22 ),
inference(copy,[status(thm)],[c_1957]) ).
cnf(c_1959,plain,
e24 = e20,
inference(resolve,[status(thm)],[c_24,c_1958]) ).
cnf(c_1824,plain,
$false,
inference(resolve,[status(thm)],[c_20,c_1959]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG080+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.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 21:08:39 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3769999 was started by sandbox2 on n003,
% 0.09/0.37 % Sat Sep 26 21:08:39 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 3.14/0.81
% 3.14/0.81 % SZS status Theorem for theBenchmark
% 3.14/0.81
% 3.14/0.81 % Proof 1 at 0.34 (+ 0.08) seconds.
% 3.14/0.81 % Length of proof is 158.
% 3.14/0.81 % Level of proof is 30.
% 3.14/0.81 % Maximum clause weight is 38.000.
% 3.14/0.81 % Given clauses 400.
% 3.14/0.81
% 3.14/0.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------