%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/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:47:44 AM UTC 2026
% Result : Theorem 64.14s 9.95s
% Output : CNFRefutation 64.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( e13 != e14
& e12 != e14
& e12 != e13
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ) ).
fof(ax2,axiom,
( e23 != e24
& e22 != e24
& e22 != e23
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ) ).
fof(ax4,axiom,
( op1(e14,e14) = e14
& op1(e14,e13) = e10
& op1(e14,e12) = e11
& op1(e14,e11) = e12
& op1(e14,e10) = e13
& op1(e13,e14) = e11
& op1(e13,e13) = e13
& op1(e13,e12) = e10
& op1(e13,e11) = e14
& op1(e13,e10) = e12
& op1(e12,e14) = e13
& op1(e12,e13) = e14
& op1(e12,e12) = e12
& op1(e12,e11) = e10
& op1(e12,e10) = e11
& op1(e11,e14) = e10
& op1(e11,e13) = e12
& op1(e11,e12) = e13
& op1(e11,e11) = e11
& op1(e11,e10) = e14
& op1(e10,e14) = e12
& op1(e10,e13) = e11
& op1(e10,e12) = e14
& op1(e10,e11) = e13
& op1(e10,e10) = e10 ) ).
fof(ax5,axiom,
( op2(e24,e24) = e24
& op2(e24,e23) = e21
& op2(e24,e22) = e20
& op2(e24,e21) = e22
& op2(e24,e20) = e23
& op2(e23,e24) = e22
& op2(e23,e23) = e23
& op2(e23,e22) = e21
& op2(e23,e21) = e20
& op2(e23,e20) = e24
& op2(e22,e24) = e23
& op2(e22,e23) = e20
& op2(e22,e22) = e22
& op2(e22,e21) = e24
& op2(e22,e20) = e21
& op2(e21,e24) = e20
& op2(e21,e23) = e24
& op2(e21,e22) = e23
& op2(e21,e21) = e21
& op2(e21,e20) = e22
& op2(e20,e24) = e21
& op2(e20,e23) = e22
& op2(e20,e22) = e24
& op2(e20,e21) = e23
& op2(e20,e20) = e20 ) ).
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)) ) ) ).
fof(negated_conjecture,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(negate_conjecture,[status(cth)],[co1]) ).
cnf(c0,plain,
e10 != e11,
inference(clausification,[status(esa)],[ax1]) ).
cnf(c1,plain,
e10 != e12,
inference(clausification,[status(esa)],[ax1]) ).
cnf(c10,plain,
e20 != e21,
inference(clausification,[status(esa)],[ax2]) ).
cnf(c11,plain,
e20 != e22,
inference(clausification,[status(esa)],[ax2]) ).
cnf(c12,plain,
e20 != e23,
inference(clausification,[status(esa)],[ax2]) ).
cnf(c13,plain,
e20 != e24,
inference(clausification,[status(esa)],[ax2]) ).
cnf(c15,plain,
e21 != e23,
inference(clausification,[status(esa)],[ax2]) ).
cnf(c16,plain,
e21 != e24,
inference(clausification,[status(esa)],[ax2]) ).
cnf(c46,plain,
op1(e10,e11) = e13,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c47,plain,
op1(e10,e12) = e14,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c48,plain,
op1(e10,e13) = e11,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c49,plain,
op1(e10,e14) = e12,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c50,plain,
op1(e11,e10) = e14,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c52,plain,
op1(e11,e12) = e13,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c54,plain,
op1(e11,e14) = e10,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c55,plain,
op1(e12,e10) = e11,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c58,plain,
op1(e12,e13) = e14,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c59,plain,
op1(e12,e14) = e13,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c60,plain,
op1(e13,e10) = e12,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c62,plain,
op1(e13,e12) = e10,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c65,plain,
op1(e14,e10) = e13,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c67,plain,
op1(e14,e12) = e11,
inference(clausification,[status(esa)],[ax4]) ).
cnf(c71,plain,
op2(e20,e21) = e23,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c74,plain,
op2(e20,e24) = e21,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c75,plain,
op2(e21,e20) = e22,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c77,plain,
op2(e21,e22) = e23,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c78,plain,
op2(e21,e23) = e24,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c80,plain,
op2(e22,e20) = e21,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c81,plain,
op2(e22,e21) = e24,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c84,plain,
op2(e22,e24) = e23,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c85,plain,
op2(e23,e20) = e24,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c86,plain,
op2(e23,e21) = e20,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c87,plain,
op2(e23,e22) = e21,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c89,plain,
op2(e23,e24) = e22,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c91,plain,
op2(e24,e21) = e22,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c92,plain,
op2(e24,e22) = e20,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c93,plain,
op2(e24,e23) = e21,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c95,plain,
( h(e10) = e22
| h(e10) = e23
| h(e10) = e21
| h(e10) = e20
| h(e10) = e24 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c97,plain,
( h(e12) = e20
| h(e12) = e21
| h(e12) = e24
| h(e12) = e23
| h(e12) = e22 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c100,plain,
( j(e20) = e11
| j(e20) = e13
| j(e20) = e10
| j(e20) = e12
| j(e20) = e14 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c101,plain,
( j(e21) = e12
| j(e21) = e11
| j(e21) = e14
| j(e21) = e10
| j(e21) = e13 ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c106,plain,
h(op1(e10,e11)) = op2(h(e10),h(e11)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c107,plain,
h(op1(e10,e12)) = op2(h(e10),h(e12)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c108,plain,
h(op1(e10,e13)) = op2(h(e10),h(e13)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c109,plain,
h(op1(e10,e14)) = op2(h(e10),h(e14)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c110,plain,
h(op1(e11,e10)) = op2(h(e11),h(e10)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c114,plain,
h(op1(e11,e14)) = op2(h(e11),h(e14)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c115,plain,
h(op1(e12,e10)) = op2(h(e12),h(e10)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c118,plain,
h(op1(e12,e13)) = op2(h(e12),h(e13)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c119,plain,
h(op1(e12,e14)) = op2(h(e12),h(e14)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c120,plain,
h(op1(e13,e10)) = op2(h(e13),h(e10)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c122,plain,
h(op1(e13,e12)) = op2(h(e13),h(e12)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c125,plain,
h(op1(e14,e10)) = op2(h(e14),h(e10)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c131,plain,
j(op2(e20,e21)) = op1(j(e20),j(e21)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c138,plain,
j(op2(e21,e23)) = op1(j(e21),j(e23)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c146,plain,
j(op2(e23,e21)) = op1(j(e23),j(e21)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c153,plain,
j(op2(e24,e23)) = op1(j(e24),j(e23)),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c155,plain,
h(j(e20)) = e20,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c156,plain,
h(j(e21)) = e21,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c160,plain,
j(h(e10)) = e10,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c161,plain,
j(h(e11)) = e11,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c162,plain,
j(h(e12)) = e12,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(c164,plain,
j(h(e14)) = e14,
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
h(e13) = op2(h(e10),h(e11)),
inference(demodulation,[status(thm)],[c106,c46]) ).
cnf(d1,plain,
h(e11) = op2(h(e10),h(e13)),
inference(demodulation,[status(thm)],[c108,c48]) ).
cnf(d2,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(op1(e12,e10)) = op2(h(e12),e24) ),
inference(superposition,[status(thm)],[c95,c115]) ).
cnf(d3,plain,
( h(e11) = op2(h(e12),e24)
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d2,c55]) ).
cnf(d4,plain,
h(e13) = op2(h(e12),h(e14)),
inference(demodulation,[status(thm)],[c119,c59]) ).
cnf(d5,plain,
( j(e21) = e13
| j(e21) = e12
| j(e21) = e11
| j(e21) = e10
| h(e14) = e21 ),
inference(superposition,[status(thm)],[c101,c156]) ).
cnf(d6,plain,
( j(e21) = e12
| j(e21) = e11
| j(e21) = e10
| h(e14) = e21
| h(e13) = e21 ),
inference(superposition,[status(thm)],[d5,c156]) ).
cnf(d7,plain,
( j(e21) = e11
| j(e21) = e10
| h(e14) = e21
| h(e13) = e21
| h(e12) = e21 ),
inference(superposition,[status(thm)],[d6,c156]) ).
cnf(d8,plain,
( j(e21) = e10
| h(e14) = e21
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21 ),
inference(superposition,[status(thm)],[d7,c156]) ).
cnf(d9,plain,
( h(e14) = e21
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21 ),
inference(superposition,[status(thm)],[d8,c156]) ).
cnf(d10,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(op1(e12,e13)) = op2(e24,h(e13)) ),
inference(superposition,[status(thm)],[c97,c118]) ).
cnf(d11,plain,
( h(e14) = op2(e24,h(e13))
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 ),
inference(demodulation,[status(thm)],[d10,c58]) ).
cnf(d12,plain,
( h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| h(op1(e12,e14)) = op2(h(e12),e21) ),
inference(superposition,[status(thm)],[d9,c119]) ).
cnf(d13,plain,
( h(e13) = op2(h(e12),e21)
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d12,c59]) ).
cnf(d14,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| h(e13) = op2(e24,e21) ),
inference(superposition,[status(thm)],[c97,d13]) ).
cnf(d15,plain,
( h(e13) = e22
| h(e13) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d14,c91]) ).
cnf(d16,plain,
( h(e13) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e14) = op2(e24,e22) ),
inference(superposition,[status(thm)],[d15,d11]) ).
cnf(d17,plain,
( h(e14) = e20
| h(e13) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d16,c92]) ).
cnf(d18,plain,
( h(e13) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| e20 = e21 ),
inference(superposition,[status(thm)],[d17,d9]) ).
cnf(d19,plain,
( h(e13) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(resolution,[status(thm)],[c10,d18]) ).
cnf(d20,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(op1(e12,e14)) = op2(e24,h(e14)) ),
inference(superposition,[status(thm)],[c97,c119]) ).
cnf(d21,plain,
( h(e13) = op2(e24,h(e14))
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20 ),
inference(demodulation,[status(thm)],[d20,c59]) ).
cnf(d22,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e14) = op2(e24,e21) ),
inference(superposition,[status(thm)],[d19,d11]) ).
cnf(d23,plain,
( h(e14) = e22
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d22,c91]) ).
cnf(d24,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e13) = op2(e24,e22) ),
inference(superposition,[status(thm)],[d23,d21]) ).
cnf(d25,plain,
( h(e13) = e20
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d24,c92]) ).
cnf(d26,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| e20 = e21 ),
inference(superposition,[status(thm)],[d25,d19]) ).
cnf(d27,plain,
( h(e12) = e23
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(resolution,[status(thm)],[c10,d26]) ).
cnf(d28,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = op2(e23,h(e14)) ),
inference(superposition,[status(thm)],[d27,d4]) ).
cnf(d29,plain,
h(e14) = op2(h(e12),h(e13)),
inference(demodulation,[status(thm)],[c118,c58]) ).
cnf(d30,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e23,h(e13)) ),
inference(superposition,[status(thm)],[d27,d29]) ).
cnf(d31,plain,
j(e21) = op1(j(e24),j(e23)),
inference(demodulation,[status(thm)],[c153,c93]) ).
cnf(d32,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| j(e23) = e12 ),
inference(superposition,[status(thm)],[d27,c162]) ).
cnf(d33,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| j(e21) = op1(j(e24),e12) ),
inference(superposition,[status(thm)],[d32,d31]) ).
cnf(d34,plain,
( h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| j(e21) = e14 ),
inference(superposition,[status(thm)],[d9,c164]) ).
cnf(d35,plain,
( h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| j(op2(e21,e23)) = op1(e14,j(e23)) ),
inference(superposition,[status(thm)],[d34,c138]) ).
cnf(d36,plain,
( j(e24) = op1(e14,j(e23))
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d35,c78]) ).
cnf(d37,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| j(e24) = op1(e14,e12) ),
inference(superposition,[status(thm)],[d32,d36]) ).
cnf(d38,plain,
( j(e24) = e11
| h(e13) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d37,c67]) ).
cnf(d39,plain,
( h(e13) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| j(e21) = op1(e11,e12) ),
inference(superposition,[status(thm)],[d38,d33]) ).
cnf(d40,plain,
( j(e21) = e13
| h(e13) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d39,c52]) ).
cnf(d41,plain,
( h(e13) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = e21 ),
inference(superposition,[status(thm)],[d40,c156]) ).
cnf(d42,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d41,d30]) ).
cnf(d43,plain,
( h(e14) = e20
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d42,c86]) ).
cnf(d44,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = op2(e23,e20) ),
inference(superposition,[status(thm)],[d43,d28]) ).
cnf(d45,plain,
( h(e13) = e24
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d44,c85]) ).
cnf(d46,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| e21 = e24 ),
inference(superposition,[status(thm)],[d41,d45]) ).
cnf(d47,plain,
( h(e12) = e22
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(resolution,[status(thm)],[c16,d46]) ).
cnf(d48,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = op2(e22,h(e14)) ),
inference(superposition,[status(thm)],[d47,d4]) ).
cnf(d49,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e22,h(e13)) ),
inference(superposition,[status(thm)],[d47,d29]) ).
cnf(d50,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| h(e13) = op2(e22,e21) ),
inference(superposition,[status(thm)],[d47,d13]) ).
cnf(d51,plain,
( h(e13) = e24
| h(e13) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d50,c81]) ).
cnf(d52,plain,
( h(e13) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e22,e24) ),
inference(superposition,[status(thm)],[d51,d49]) ).
cnf(d53,plain,
( h(e14) = e23
| h(e13) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d52,c84]) ).
cnf(d54,plain,
( h(e13) = e21
| h(e12) = e21
| h(e11) = e21
| h(e10) = e21
| h(e13) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| e21 = e23 ),
inference(superposition,[status(thm)],[d9,d53]) ).
cnf(d55,plain,
( h(e13) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(resolution,[status(thm)],[c15,d54]) ).
cnf(d56,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e22,e21) ),
inference(superposition,[status(thm)],[d55,d49]) ).
cnf(d57,plain,
( h(e14) = e24
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d56,c81]) ).
cnf(d58,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e13) = op2(e22,e24) ),
inference(superposition,[status(thm)],[d57,d48]) ).
cnf(d59,plain,
( h(e13) = e23
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d58,c84]) ).
cnf(d60,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| e21 = e23 ),
inference(superposition,[status(thm)],[d55,d59]) ).
cnf(d61,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21 ),
inference(resolution,[status(thm)],[c15,d60]) ).
cnf(d62,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(op1(e10,e14)) = op2(e24,h(e14)) ),
inference(superposition,[status(thm)],[c95,c109]) ).
cnf(d63,plain,
( h(e12) = op2(e24,h(e14))
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d62,c49]) ).
cnf(d64,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(op1(e10,e12)) = op2(e24,h(e12)) ),
inference(superposition,[status(thm)],[c95,c107]) ).
cnf(d65,plain,
( h(e14) = op2(e24,h(e12))
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d64,c47]) ).
cnf(d66,plain,
h(e10) = op2(h(e13),h(e12)),
inference(demodulation,[status(thm)],[c122,c62]) ).
cnf(d67,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = op2(h(e13),e22) ),
inference(superposition,[status(thm)],[d47,d66]) ).
cnf(d68,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = op2(e21,e22) ),
inference(superposition,[status(thm)],[d55,d67]) ).
cnf(d69,plain,
( h(e12) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e21 ),
inference(demodulation,[status(thm)],[d68,c77]) ).
cnf(d70,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e14) = op2(e24,e21) ),
inference(superposition,[status(thm)],[d69,d65]) ).
cnf(d71,plain,
( h(e14) = e22
| h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d70,c91]) ).
cnf(d72,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e24,e22) ),
inference(superposition,[status(thm)],[d71,d63]) ).
cnf(d73,plain,
( h(e12) = e20
| h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d72,c92]) ).
cnf(d74,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| e20 = e21 ),
inference(superposition,[status(thm)],[d73,d61]) ).
cnf(d75,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c10,d74]) ).
cnf(d76,plain,
( h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e11) = op2(e20,e24) ),
inference(superposition,[status(thm)],[d75,d3]) ).
cnf(d77,plain,
( h(e11) = e21
| h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d76,c74]) ).
cnf(d78,plain,
( h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| j(e21) = e11 ),
inference(superposition,[status(thm)],[d77,c161]) ).
cnf(d79,plain,
( h(e11) = e21
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e11) = e21 ),
inference(superposition,[status(thm)],[d78,c156]) ).
cnf(d80,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(op1(e10,e13)) = op2(e24,h(e13)) ),
inference(superposition,[status(thm)],[c95,c108]) ).
cnf(d81,plain,
( h(e11) = op2(e24,h(e13))
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d80,c48]) ).
cnf(d82,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(op1(e10,e11)) = op2(e24,h(e11)) ),
inference(superposition,[status(thm)],[c95,c106]) ).
cnf(d83,plain,
( h(e13) = op2(e24,h(e11))
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d82,c46]) ).
cnf(d84,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e13) = op2(e24,e21) ),
inference(superposition,[status(thm)],[d79,d83]) ).
cnf(d85,plain,
( h(e13) = e22
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d84,c91]) ).
cnf(d86,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e11) = op2(e24,e22) ),
inference(superposition,[status(thm)],[d85,d81]) ).
cnf(d87,plain,
( h(e11) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d86,c92]) ).
cnf(d88,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| e20 = e21 ),
inference(superposition,[status(thm)],[d87,d79]) ).
cnf(d89,plain,
( h(e10) = e23
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c10,d88]) ).
cnf(d90,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e11) = op2(e23,h(e13)) ),
inference(superposition,[status(thm)],[d89,d1]) ).
cnf(d91,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e13) = op2(e23,h(e11)) ),
inference(superposition,[status(thm)],[d89,d0]) ).
cnf(d92,plain,
h(e12) = op2(h(e10),h(e14)),
inference(demodulation,[status(thm)],[c109,c49]) ).
cnf(d93,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e23,h(e14)) ),
inference(superposition,[status(thm)],[d89,d92]) ).
cnf(d94,plain,
h(e14) = op2(h(e10),h(e12)),
inference(demodulation,[status(thm)],[c107,c47]) ).
cnf(d95,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e14) = op2(e23,h(e12)) ),
inference(superposition,[status(thm)],[d89,d94]) ).
cnf(d96,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(h(e10),e21) ),
inference(superposition,[status(thm)],[d61,d94]) ).
cnf(d97,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d89,d96]) ).
cnf(d98,plain,
( h(e14) = e20
| h(e12) = e20
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d97,c86]) ).
cnf(d99,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e23,e20) ),
inference(superposition,[status(thm)],[d98,d93]) ).
cnf(d100,plain,
( h(e12) = e24
| h(e12) = e20
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d99,c85]) ).
cnf(d101,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| e21 = e24 ),
inference(superposition,[status(thm)],[d61,d100]) ).
cnf(d102,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c16,d101]) ).
cnf(d103,plain,
( h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e14) = op2(e23,e20) ),
inference(superposition,[status(thm)],[d102,d95]) ).
cnf(d104,plain,
( h(e14) = e24
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d103,c85]) ).
cnf(d105,plain,
( h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e23,e24) ),
inference(superposition,[status(thm)],[d104,d93]) ).
cnf(d106,plain,
( h(e12) = e22
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d105,c89]) ).
cnf(d107,plain,
( h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| e20 = e22 ),
inference(superposition,[status(thm)],[d102,d106]) ).
cnf(d108,plain,
( h(e11) = e21
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c11,d107]) ).
cnf(d109,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e13) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d108,d91]) ).
cnf(d110,plain,
( h(e13) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d109,c86]) ).
cnf(d111,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e11) = op2(e23,e20) ),
inference(superposition,[status(thm)],[d110,d90]) ).
cnf(d112,plain,
( h(e11) = e24
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d111,c85]) ).
cnf(d113,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| h(e10) = e22
| h(e10) = e21
| h(e10) = e20
| e21 = e24 ),
inference(superposition,[status(thm)],[d108,d112]) ).
cnf(d114,plain,
( h(e10) = e22
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c16,d113]) ).
cnf(d115,plain,
( h(e10) = e21
| h(e10) = e20
| h(e13) = op2(e22,h(e11)) ),
inference(superposition,[status(thm)],[d114,d0]) ).
cnf(d116,plain,
( h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e22,h(e14)) ),
inference(superposition,[status(thm)],[d114,d92]) ).
cnf(d117,plain,
( h(e10) = e21
| h(e10) = e20
| h(e14) = op2(e22,h(e12)) ),
inference(superposition,[status(thm)],[d114,d94]) ).
cnf(d118,plain,
( h(e10) = e21
| h(e10) = e20
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e14) = op2(e22,e21) ),
inference(superposition,[status(thm)],[d114,d96]) ).
cnf(d119,plain,
( h(e14) = e24
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d118,c81]) ).
cnf(d120,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e22,e24) ),
inference(superposition,[status(thm)],[d119,d116]) ).
cnf(d121,plain,
( h(e12) = e23
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d120,c84]) ).
cnf(d122,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20
| e21 = e23 ),
inference(superposition,[status(thm)],[d61,d121]) ).
cnf(d123,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c15,d122]) ).
cnf(d124,plain,
( h(e11) = e21
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| h(e14) = op2(e22,e20) ),
inference(superposition,[status(thm)],[d123,d117]) ).
cnf(d125,plain,
( h(e14) = e21
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d124,c80]) ).
cnf(d126,plain,
( h(e11) = e21
| h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| h(e12) = op2(e22,e21) ),
inference(superposition,[status(thm)],[d125,d116]) ).
cnf(d127,plain,
( h(e12) = e24
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d126,c81]) ).
cnf(d128,plain,
( h(e11) = e21
| h(e10) = e21
| h(e10) = e20
| h(e11) = e21
| h(e10) = e21
| h(e10) = e20
| e20 = e24 ),
inference(superposition,[status(thm)],[d123,d127]) ).
cnf(d129,plain,
( h(e11) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c13,d128]) ).
cnf(d130,plain,
( h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| h(e13) = op2(e22,e21) ),
inference(superposition,[status(thm)],[d129,d115]) ).
cnf(d131,plain,
( h(e13) = e24
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d130,c81]) ).
cnf(d132,plain,
h(e13) = op2(h(e14),h(e10)),
inference(demodulation,[status(thm)],[c125,c65]) ).
cnf(d133,plain,
( h(e10) = e21
| h(e10) = e20
| h(e13) = op2(h(e14),e22) ),
inference(superposition,[status(thm)],[d114,d132]) ).
cnf(d134,plain,
h(e14) = op2(h(e11),h(e10)),
inference(demodulation,[status(thm)],[c110,c50]) ).
cnf(d135,plain,
( h(e10) = e21
| h(e10) = e20
| h(e14) = op2(h(e11),e22) ),
inference(superposition,[status(thm)],[d114,d134]) ).
cnf(d136,plain,
( h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| h(e14) = op2(e21,e22) ),
inference(superposition,[status(thm)],[d129,d135]) ).
cnf(d137,plain,
( h(e14) = e23
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d136,c77]) ).
cnf(d138,plain,
( h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| h(e13) = op2(e23,e22) ),
inference(superposition,[status(thm)],[d137,d133]) ).
cnf(d139,plain,
( h(e13) = e21
| h(e10) = e21
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d138,c87]) ).
cnf(d140,plain,
( h(e10) = e21
| h(e10) = e20
| h(e10) = e21
| h(e10) = e20
| e21 = e24 ),
inference(superposition,[status(thm)],[d139,d131]) ).
cnf(d141,plain,
( h(e10) = e21
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c16,d140]) ).
cnf(d142,plain,
( h(e10) = e20
| h(e13) = op2(e21,h(e11)) ),
inference(superposition,[status(thm)],[d141,d0]) ).
cnf(d143,plain,
( h(e10) = e20
| h(e14) = op2(e21,h(e12)) ),
inference(superposition,[status(thm)],[d141,d94]) ).
cnf(d144,plain,
h(e11) = op2(h(e12),h(e10)),
inference(demodulation,[status(thm)],[c115,c55]) ).
cnf(d145,plain,
( h(e10) = e20
| h(e11) = op2(h(e12),e21) ),
inference(superposition,[status(thm)],[d141,d144]) ).
cnf(d146,plain,
h(e12) = op2(h(e13),h(e10)),
inference(demodulation,[status(thm)],[c120,c60]) ).
cnf(d147,plain,
( h(e10) = e20
| h(e12) = op2(h(e13),e21) ),
inference(superposition,[status(thm)],[d141,d146]) ).
cnf(d148,plain,
( j(e20) = e13
| j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| h(e14) = e20 ),
inference(superposition,[status(thm)],[c100,c155]) ).
cnf(d149,plain,
( j(e20) = e12
| j(e20) = e11
| j(e20) = e10
| h(e14) = e20
| h(e13) = e20 ),
inference(superposition,[status(thm)],[d148,c155]) ).
cnf(d150,plain,
( j(e20) = e11
| j(e20) = e10
| h(e14) = e20
| h(e13) = e20
| h(e12) = e20 ),
inference(superposition,[status(thm)],[d149,c155]) ).
cnf(d151,plain,
( j(e20) = e10
| h(e14) = e20
| h(e13) = e20
| h(e12) = e20
| h(e11) = e20 ),
inference(superposition,[status(thm)],[d150,c155]) ).
cnf(d152,plain,
( h(e14) = e20
| h(e13) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(superposition,[status(thm)],[d151,c155]) ).
cnf(d153,plain,
( h(e13) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20
| h(op1(e14,e10)) = op2(e20,h(e10)) ),
inference(superposition,[status(thm)],[d152,c125]) ).
cnf(d154,plain,
( h(e13) = op2(e20,h(e10))
| h(e13) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d153,c65]) ).
cnf(d155,plain,
( h(e10) = e20
| h(e13) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20
| h(e13) = op2(e20,e21) ),
inference(superposition,[status(thm)],[d141,d154]) ).
cnf(d156,plain,
( h(e13) = e23
| h(e13) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d155,c71]) ).
cnf(d157,plain,
( h(e13) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20
| h(e10) = e20
| h(e12) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d156,d147]) ).
cnf(d158,plain,
( h(e13) = e20
| h(e12) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d157,c86]) ).
cnf(d159,plain,
( h(e12) = e20
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20
| h(e10) = e20
| h(e12) = op2(e20,e21) ),
inference(superposition,[status(thm)],[d158,d147]) ).
cnf(d160,plain,
( h(e12) = e23
| h(e12) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d159,c71]) ).
cnf(d161,plain,
( h(e12) = e20
| h(e11) = e20
| h(e10) = e20
| h(e10) = e20
| h(e11) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d160,d145]) ).
cnf(d162,plain,
( h(e12) = e20
| h(e11) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d161,c86]) ).
cnf(d163,plain,
( h(e11) = e20
| h(e11) = e20
| h(e10) = e20
| h(e10) = e20
| h(e14) = op2(e21,e20) ),
inference(superposition,[status(thm)],[d162,d143]) ).
cnf(d164,plain,
( h(e14) = e22
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d163,c75]) ).
cnf(d165,plain,
( h(e10) = e20
| h(e14) = op2(h(e11),e21) ),
inference(superposition,[status(thm)],[d141,d134]) ).
cnf(d166,plain,
( h(e11) = e20
| h(e11) = e20
| h(e10) = e20
| h(e10) = e20
| h(e11) = op2(e20,e21) ),
inference(superposition,[status(thm)],[d162,d145]) ).
cnf(d167,plain,
( h(e11) = e23
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d166,c71]) ).
cnf(d168,plain,
( h(e11) = e20
| h(e10) = e20
| h(e10) = e20
| h(e14) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d167,d165]) ).
cnf(d169,plain,
( h(e14) = e20
| h(e11) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d168,c86]) ).
cnf(d170,plain,
( h(e11) = e20
| h(e10) = e20
| h(e11) = e20
| h(e10) = e20
| e20 = e22 ),
inference(superposition,[status(thm)],[d169,d164]) ).
cnf(d171,plain,
( h(e11) = e20
| h(e10) = e20 ),
inference(resolution,[status(thm)],[c11,d170]) ).
cnf(d172,plain,
( h(e10) = e20
| h(e10) = e20
| h(e13) = op2(e21,e20) ),
inference(superposition,[status(thm)],[d171,d142]) ).
cnf(d173,plain,
( h(e13) = e22
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d172,c75]) ).
cnf(d174,plain,
( h(e10) = e20
| h(e13) = op2(h(e14),e21) ),
inference(superposition,[status(thm)],[d141,d132]) ).
cnf(d175,plain,
( h(e10) = e20
| h(e10) = e20
| h(e14) = op2(e20,e21) ),
inference(superposition,[status(thm)],[d171,d165]) ).
cnf(d176,plain,
( h(e14) = e23
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d175,c71]) ).
cnf(d177,plain,
( h(e10) = e20
| h(e10) = e20
| h(e13) = op2(e23,e21) ),
inference(superposition,[status(thm)],[d176,d174]) ).
cnf(d178,plain,
( h(e13) = e20
| h(e10) = e20 ),
inference(demodulation,[status(thm)],[d177,c86]) ).
cnf(d179,plain,
( h(e10) = e20
| h(e10) = e20
| e20 = e22 ),
inference(superposition,[status(thm)],[d178,d173]) ).
cnf(d180,plain,
h(e10) = e20,
inference(resolution,[status(thm)],[c11,d179]) ).
cnf(d181,plain,
j(e20) = e10,
inference(demodulation,[status(thm)],[c160,d180]) ).
cnf(d182,plain,
j(e20) = op1(j(e23),j(e21)),
inference(demodulation,[status(thm)],[c146,c86]) ).
cnf(d183,plain,
e10 = op1(j(e23),j(e21)),
inference(demodulation,[status(thm)],[d182,d181]) ).
cnf(d184,plain,
( h(e12) = e20
| h(e11) = e21
| h(e10) = e21
| j(e21) = e12 ),
inference(superposition,[status(thm)],[d61,c162]) ).
cnf(d185,plain,
( j(e21) = e12
| h(e12) = e20
| h(e11) = e21
| e20 = e21 ),
inference(demodulation,[status(thm)],[d184,d180]) ).
cnf(d186,plain,
( j(e21) = e12
| h(e12) = e20
| h(e11) = e21 ),
inference(resolution,[status(thm)],[c10,d185]) ).
cnf(d187,plain,
( h(e12) = e20
| h(e11) = e21
| e10 = op1(j(e23),e12) ),
inference(superposition,[status(thm)],[d186,d183]) ).
cnf(d188,plain,
j(e23) = op1(j(e20),j(e21)),
inference(demodulation,[status(thm)],[c131,c71]) ).
cnf(d189,plain,
j(e23) = op1(e10,j(e21)),
inference(demodulation,[status(thm)],[d188,d181]) ).
cnf(d190,plain,
( h(e12) = e20
| h(e11) = e21
| j(e23) = op1(e10,e12) ),
inference(superposition,[status(thm)],[d186,d189]) ).
cnf(d191,plain,
( j(e23) = e14
| h(e12) = e20
| h(e11) = e21 ),
inference(demodulation,[status(thm)],[d190,c47]) ).
cnf(d192,plain,
( h(e12) = e20
| h(e11) = e21
| h(e12) = e20
| h(e11) = e21
| e10 = op1(e14,e12) ),
inference(superposition,[status(thm)],[d191,d187]) ).
cnf(d193,plain,
( h(e12) = e20
| h(e11) = e21
| e10 = e11 ),
inference(demodulation,[status(thm)],[d192,c67]) ).
cnf(d194,plain,
( h(e12) = e20
| h(e11) = e21 ),
inference(resolution,[status(thm)],[c0,d193]) ).
cnf(d195,plain,
( h(e11) = e21
| j(e20) = e12 ),
inference(superposition,[status(thm)],[d194,c162]) ).
cnf(d196,plain,
( e10 = e12
| h(e11) = e21 ),
inference(demodulation,[status(thm)],[d195,d181]) ).
cnf(d197,plain,
h(e11) = e21,
inference(resolution,[status(thm)],[c1,d196]) ).
cnf(d198,plain,
h(e14) = op2(h(e11),e20),
inference(demodulation,[status(thm)],[d134,d180]) ).
cnf(d199,plain,
h(e14) = op2(e21,e20),
inference(demodulation,[status(thm)],[d198,d197]) ).
cnf(d200,plain,
h(e14) = e22,
inference(demodulation,[status(thm)],[d199,c75]) ).
cnf(d201,plain,
h(e10) = op2(h(e11),h(e14)),
inference(demodulation,[status(thm)],[c114,c54]) ).
cnf(d202,plain,
e20 = op2(h(e11),h(e14)),
inference(demodulation,[status(thm)],[d201,d180]) ).
cnf(d203,plain,
e20 = op2(e21,h(e14)),
inference(demodulation,[status(thm)],[d202,d197]) ).
cnf(d204,plain,
e20 = op2(e21,e22),
inference(demodulation,[status(thm)],[d203,d200]) ).
cnf(d205,plain,
e20 = e23,
inference(demodulation,[status(thm)],[c77,d204]) ).
cnf(d206,plain,
$false,
inference(resolution,[status(thm)],[c12,d205]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG185+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 26 21:25:24 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 64.14/9.95 % SZS status Theorem for theBenchmark.p
% 64.14/9.95 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------