%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG168+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n009.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 : Fri Sep 25 12:53:40 PM UTC 2026
% Result : Theorem 1.09s 1.74s
% Output : CNFRefutation 1.09s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f119ERROR: Could not build tree for root c_1150ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e14,e14) = e14
| op1(e14,e14) = e13
| op1(e14,e14) = e12
| op1(e14,e14) = e11
| op1(e14,e14) = e10 )
& ( op1(e14,e13) = e14
| op1(e14,e13) = e13
| op1(e14,e13) = e12
| op1(e14,e13) = e11
| op1(e14,e13) = e10 )
& ( op1(e14,e12) = e14
| op1(e14,e12) = e13
| op1(e14,e12) = e12
| op1(e14,e12) = e11
| op1(e14,e12) = e10 )
& ( op1(e14,e11) = e14
| op1(e14,e11) = e13
| op1(e14,e11) = e12
| op1(e14,e11) = e11
| op1(e14,e11) = e10 )
& ( op1(e14,e10) = e14
| op1(e14,e10) = e13
| op1(e14,e10) = e12
| op1(e14,e10) = e11
| op1(e14,e10) = e10 )
& ( op1(e13,e14) = e14
| op1(e13,e14) = e13
| op1(e13,e14) = e12
| op1(e13,e14) = e11
| op1(e13,e14) = e10 )
& ( op1(e13,e13) = e14
| op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e14
| op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e14
| op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e14
| op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e14) = e14
| op1(e12,e14) = e13
| op1(e12,e14) = e12
| op1(e12,e14) = e11
| op1(e12,e14) = e10 )
& ( op1(e12,e13) = e14
| op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e14
| op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e14
| op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e14
| op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e14) = e14
| op1(e11,e14) = e13
| op1(e11,e14) = e12
| op1(e11,e14) = e11
| op1(e11,e14) = e10 )
& ( op1(e11,e13) = e14
| op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e14
| op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e14
| op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e14
| op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e14) = e14
| op1(e10,e14) = e13
| op1(e10,e14) = e12
| op1(e10,e14) = e11
| op1(e10,e14) = e10 )
& ( op1(e10,e13) = e14
| op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e14
| op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e14
| op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e14
| op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op1(e14,e14) = e14
| op1(e13,e14) = e14
| op1(e12,e14) = e14
| op1(e11,e14) = e14
| op1(e10,e14) = e14 )
& ( op1(e14,e14) = e14
| op1(e14,e13) = e14
| op1(e14,e12) = e14
| op1(e14,e11) = e14
| op1(e14,e10) = e14 )
& ( op1(e14,e14) = e13
| op1(e13,e14) = e13
| op1(e12,e14) = e13
| op1(e11,e14) = e13
| op1(e10,e14) = e13 )
& ( op1(e14,e14) = e13
| op1(e14,e13) = e13
| op1(e14,e12) = e13
| op1(e14,e11) = e13
| op1(e14,e10) = e13 )
& ( op1(e14,e14) = e12
| op1(e13,e14) = e12
| op1(e12,e14) = e12
| op1(e11,e14) = e12
| op1(e10,e14) = e12 )
& ( op1(e14,e14) = e12
| op1(e14,e13) = e12
| op1(e14,e12) = e12
| op1(e14,e11) = e12
| op1(e14,e10) = e12 )
& ( op1(e14,e14) = e11
| op1(e13,e14) = e11
| op1(e12,e14) = e11
| op1(e11,e14) = e11
| op1(e10,e14) = e11 )
& ( op1(e14,e14) = e11
| op1(e14,e13) = e11
| op1(e14,e12) = e11
| op1(e14,e11) = e11
| op1(e14,e10) = e11 )
& ( op1(e14,e14) = e10
| op1(e13,e14) = e10
| op1(e12,e14) = e10
| op1(e11,e14) = e10
| op1(e10,e14) = e10 )
& ( op1(e14,e14) = e10
| op1(e14,e13) = e10
| op1(e14,e12) = e10
| op1(e14,e11) = e10
| op1(e14,e10) = e10 )
& ( op1(e14,e13) = e14
| op1(e13,e13) = e14
| op1(e12,e13) = e14
| op1(e11,e13) = e14
| op1(e10,e13) = e14 )
& ( op1(e13,e14) = e14
| op1(e13,e13) = e14
| op1(e13,e12) = e14
| op1(e13,e11) = e14
| op1(e13,e10) = e14 )
& ( op1(e14,e13) = e13
| op1(e13,e13) = e13
| op1(e12,e13) = e13
| op1(e11,e13) = e13
| op1(e10,e13) = e13 )
& ( op1(e13,e14) = e13
| op1(e13,e13) = e13
| op1(e13,e12) = e13
| op1(e13,e11) = e13
| op1(e13,e10) = e13 )
& ( op1(e14,e13) = e12
| op1(e13,e13) = e12
| op1(e12,e13) = e12
| op1(e11,e13) = e12
| op1(e10,e13) = e12 )
& ( op1(e13,e14) = e12
| op1(e13,e13) = e12
| op1(e13,e12) = e12
| op1(e13,e11) = e12
| op1(e13,e10) = e12 )
& ( op1(e14,e13) = e11
| op1(e13,e13) = e11
| op1(e12,e13) = e11
| op1(e11,e13) = e11
| op1(e10,e13) = e11 )
& ( op1(e13,e14) = e11
| op1(e13,e13) = e11
| op1(e13,e12) = e11
| op1(e13,e11) = e11
| op1(e13,e10) = e11 )
& ( op1(e14,e13) = e10
| op1(e13,e13) = e10
| op1(e12,e13) = e10
| op1(e11,e13) = e10
| op1(e10,e13) = e10 )
& ( op1(e13,e14) = e10
| op1(e13,e13) = e10
| op1(e13,e12) = e10
| op1(e13,e11) = e10
| op1(e13,e10) = e10 )
& ( op1(e14,e12) = e14
| op1(e13,e12) = e14
| op1(e12,e12) = e14
| op1(e11,e12) = e14
| op1(e10,e12) = e14 )
& ( op1(e12,e14) = e14
| op1(e12,e13) = e14
| op1(e12,e12) = e14
| op1(e12,e11) = e14
| op1(e12,e10) = e14 )
& ( op1(e14,e12) = e13
| op1(e13,e12) = e13
| op1(e12,e12) = e13
| op1(e11,e12) = e13
| op1(e10,e12) = e13 )
& ( op1(e12,e14) = e13
| op1(e12,e13) = e13
| op1(e12,e12) = e13
| op1(e12,e11) = e13
| op1(e12,e10) = e13 )
& ( op1(e14,e12) = e12
| op1(e13,e12) = e12
| op1(e12,e12) = e12
| op1(e11,e12) = e12
| op1(e10,e12) = e12 )
& ( op1(e12,e14) = e12
| op1(e12,e13) = e12
| op1(e12,e12) = e12
| op1(e12,e11) = e12
| op1(e12,e10) = e12 )
& ( op1(e14,e12) = e11
| op1(e13,e12) = e11
| op1(e12,e12) = e11
| op1(e11,e12) = e11
| op1(e10,e12) = e11 )
& ( op1(e12,e14) = e11
| op1(e12,e13) = e11
| op1(e12,e12) = e11
| op1(e12,e11) = e11
| op1(e12,e10) = e11 )
& ( op1(e14,e12) = e10
| op1(e13,e12) = e10
| op1(e12,e12) = e10
| op1(e11,e12) = e10
| op1(e10,e12) = e10 )
& ( op1(e12,e14) = e10
| op1(e12,e13) = e10
| op1(e12,e12) = e10
| op1(e12,e11) = e10
| op1(e12,e10) = e10 )
& ( op1(e14,e11) = e14
| op1(e13,e11) = e14
| op1(e12,e11) = e14
| op1(e11,e11) = e14
| op1(e10,e11) = e14 )
& ( op1(e11,e14) = e14
| op1(e11,e13) = e14
| op1(e11,e12) = e14
| op1(e11,e11) = e14
| op1(e11,e10) = e14 )
& ( op1(e14,e11) = e13
| op1(e13,e11) = e13
| op1(e12,e11) = e13
| op1(e11,e11) = e13
| op1(e10,e11) = e13 )
& ( op1(e11,e14) = e13
| op1(e11,e13) = e13
| op1(e11,e12) = e13
| op1(e11,e11) = e13
| op1(e11,e10) = e13 )
& ( op1(e14,e11) = e12
| op1(e13,e11) = e12
| op1(e12,e11) = e12
| op1(e11,e11) = e12
| op1(e10,e11) = e12 )
& ( op1(e11,e14) = e12
| op1(e11,e13) = e12
| op1(e11,e12) = e12
| op1(e11,e11) = e12
| op1(e11,e10) = e12 )
& ( op1(e14,e11) = e11
| op1(e13,e11) = e11
| op1(e12,e11) = e11
| op1(e11,e11) = e11
| op1(e10,e11) = e11 )
& ( op1(e11,e14) = e11
| op1(e11,e13) = e11
| op1(e11,e12) = e11
| op1(e11,e11) = e11
| op1(e11,e10) = e11 )
& ( op1(e14,e11) = e10
| op1(e13,e11) = e10
| op1(e12,e11) = e10
| op1(e11,e11) = e10
| op1(e10,e11) = e10 )
& ( op1(e11,e14) = e10
| op1(e11,e13) = e10
| op1(e11,e12) = e10
| op1(e11,e11) = e10
| op1(e11,e10) = e10 )
& ( op1(e14,e10) = e14
| op1(e13,e10) = e14
| op1(e12,e10) = e14
| op1(e11,e10) = e14
| op1(e10,e10) = e14 )
& ( op1(e10,e14) = e14
| op1(e10,e13) = e14
| op1(e10,e12) = e14
| op1(e10,e11) = e14
| op1(e10,e10) = e14 )
& ( op1(e14,e10) = e13
| op1(e13,e10) = e13
| op1(e12,e10) = e13
| op1(e11,e10) = e13
| op1(e10,e10) = e13 )
& ( op1(e10,e14) = e13
| op1(e10,e13) = e13
| op1(e10,e12) = e13
| op1(e10,e11) = e13
| op1(e10,e10) = e13 )
& ( op1(e14,e10) = e12
| op1(e13,e10) = e12
| op1(e12,e10) = e12
| op1(e11,e10) = e12
| op1(e10,e10) = e12 )
& ( op1(e10,e14) = e12
| op1(e10,e13) = e12
| op1(e10,e12) = e12
| op1(e10,e11) = e12
| op1(e10,e10) = e12 )
& ( op1(e14,e10) = e11
| op1(e13,e10) = e11
| op1(e12,e10) = e11
| op1(e11,e10) = e11
| op1(e10,e10) = e11 )
& ( op1(e10,e14) = e11
| op1(e10,e13) = e11
| op1(e10,e12) = e11
| op1(e10,e11) = e11
| op1(e10,e10) = e11 )
& ( op1(e14,e10) = e10
| op1(e13,e10) = e10
| op1(e12,e10) = e10
| op1(e11,e10) = e10
| op1(e10,e10) = e10 )
& ( op1(e10,e14) = e10
| op1(e10,e13) = e10
| op1(e10,e12) = e10
| op1(e10,e11) = e10
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op1(op1(e14,e14),op1(e14,e14)) = e14
& op1(op1(e13,e14),op1(e14,e13)) = e14
& op1(op1(e12,e14),op1(e14,e12)) = e14
& op1(op1(e11,e14),op1(e14,e11)) = e14
& op1(op1(e10,e14),op1(e14,e10)) = e14
& op1(op1(e14,e13),op1(e13,e14)) = e13
& op1(op1(e13,e13),op1(e13,e13)) = e13
& op1(op1(e12,e13),op1(e13,e12)) = e13
& op1(op1(e11,e13),op1(e13,e11)) = e13
& op1(op1(e10,e13),op1(e13,e10)) = e13
& op1(op1(e14,e12),op1(e12,e14)) = e12
& op1(op1(e13,e12),op1(e12,e13)) = e12
& op1(op1(e12,e12),op1(e12,e12)) = e12
& op1(op1(e11,e12),op1(e12,e11)) = e12
& op1(op1(e10,e12),op1(e12,e10)) = e12
& op1(op1(e14,e11),op1(e11,e14)) = e11
& op1(op1(e13,e11),op1(e11,e13)) = e11
& op1(op1(e12,e11),op1(e11,e12)) = e11
& op1(op1(e11,e11),op1(e11,e11)) = e11
& op1(op1(e10,e11),op1(e11,e10)) = e11
& op1(op1(e14,e10),op1(e10,e14)) = e10
& op1(op1(e13,e10),op1(e10,e13)) = e10
& op1(op1(e12,e10),op1(e10,e12)) = e10
& op1(op1(e11,e10),op1(e10,e11)) = e10
& op1(op1(e10,e10),op1(e10,e10)) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( ( op2(e24,e24) = e24
| op2(e24,e24) = e23
| op2(e24,e24) = e22
| op2(e24,e24) = e21
| op2(e24,e24) = e20 )
& ( op2(e24,e23) = e24
| op2(e24,e23) = e23
| op2(e24,e23) = e22
| op2(e24,e23) = e21
| op2(e24,e23) = e20 )
& ( op2(e24,e22) = e24
| op2(e24,e22) = e23
| op2(e24,e22) = e22
| op2(e24,e22) = e21
| op2(e24,e22) = e20 )
& ( op2(e24,e21) = e24
| op2(e24,e21) = e23
| op2(e24,e21) = e22
| op2(e24,e21) = e21
| op2(e24,e21) = e20 )
& ( op2(e24,e20) = e24
| op2(e24,e20) = e23
| op2(e24,e20) = e22
| op2(e24,e20) = e21
| op2(e24,e20) = e20 )
& ( op2(e23,e24) = e24
| op2(e23,e24) = e23
| op2(e23,e24) = e22
| op2(e23,e24) = e21
| op2(e23,e24) = e20 )
& ( op2(e23,e23) = e24
| op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e24
| op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e24
| op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e24
| op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e24) = e24
| op2(e22,e24) = e23
| op2(e22,e24) = e22
| op2(e22,e24) = e21
| op2(e22,e24) = e20 )
& ( op2(e22,e23) = e24
| op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e24
| op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e24
| op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e24
| op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e24) = e24
| op2(e21,e24) = e23
| op2(e21,e24) = e22
| op2(e21,e24) = e21
| op2(e21,e24) = e20 )
& ( op2(e21,e23) = e24
| op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e24
| op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e24
| op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e24
| op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e24) = e24
| op2(e20,e24) = e23
| op2(e20,e24) = e22
| op2(e20,e24) = e21
| op2(e20,e24) = e20 )
& ( op2(e20,e23) = e24
| op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e24
| op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e24
| op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e24
| op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op2(e24,e24) = e24
| op2(e23,e24) = e24
| op2(e22,e24) = e24
| op2(e21,e24) = e24
| op2(e20,e24) = e24 )
& ( op2(e24,e24) = e24
| op2(e24,e23) = e24
| op2(e24,e22) = e24
| op2(e24,e21) = e24
| op2(e24,e20) = e24 )
& ( op2(e24,e24) = e23
| op2(e23,e24) = e23
| op2(e22,e24) = e23
| op2(e21,e24) = e23
| op2(e20,e24) = e23 )
& ( op2(e24,e24) = e23
| op2(e24,e23) = e23
| op2(e24,e22) = e23
| op2(e24,e21) = e23
| op2(e24,e20) = e23 )
& ( op2(e24,e24) = e22
| op2(e23,e24) = e22
| op2(e22,e24) = e22
| op2(e21,e24) = e22
| op2(e20,e24) = e22 )
& ( op2(e24,e24) = e22
| op2(e24,e23) = e22
| op2(e24,e22) = e22
| op2(e24,e21) = e22
| op2(e24,e20) = e22 )
& ( op2(e24,e24) = e21
| op2(e23,e24) = e21
| op2(e22,e24) = e21
| op2(e21,e24) = e21
| op2(e20,e24) = e21 )
& ( op2(e24,e24) = e21
| op2(e24,e23) = e21
| op2(e24,e22) = e21
| op2(e24,e21) = e21
| op2(e24,e20) = e21 )
& ( op2(e24,e24) = e20
| op2(e23,e24) = e20
| op2(e22,e24) = e20
| op2(e21,e24) = e20
| op2(e20,e24) = e20 )
& ( op2(e24,e24) = e20
| op2(e24,e23) = e20
| op2(e24,e22) = e20
| op2(e24,e21) = e20
| op2(e24,e20) = e20 )
& ( op2(e24,e23) = e24
| op2(e23,e23) = e24
| op2(e22,e23) = e24
| op2(e21,e23) = e24
| op2(e20,e23) = e24 )
& ( op2(e23,e24) = e24
| op2(e23,e23) = e24
| op2(e23,e22) = e24
| op2(e23,e21) = e24
| op2(e23,e20) = e24 )
& ( op2(e24,e23) = e23
| op2(e23,e23) = e23
| op2(e22,e23) = e23
| op2(e21,e23) = e23
| op2(e20,e23) = e23 )
& ( op2(e23,e24) = e23
| op2(e23,e23) = e23
| op2(e23,e22) = e23
| op2(e23,e21) = e23
| op2(e23,e20) = e23 )
& ( op2(e24,e23) = e22
| op2(e23,e23) = e22
| op2(e22,e23) = e22
| op2(e21,e23) = e22
| op2(e20,e23) = e22 )
& ( op2(e23,e24) = e22
| op2(e23,e23) = e22
| op2(e23,e22) = e22
| op2(e23,e21) = e22
| op2(e23,e20) = e22 )
& ( op2(e24,e23) = e21
| op2(e23,e23) = e21
| op2(e22,e23) = e21
| op2(e21,e23) = e21
| op2(e20,e23) = e21 )
& ( op2(e23,e24) = e21
| op2(e23,e23) = e21
| op2(e23,e22) = e21
| op2(e23,e21) = e21
| op2(e23,e20) = e21 )
& ( op2(e24,e23) = e20
| op2(e23,e23) = e20
| op2(e22,e23) = e20
| op2(e21,e23) = e20
| op2(e20,e23) = e20 )
& ( op2(e23,e24) = e20
| op2(e23,e23) = e20
| op2(e23,e22) = e20
| op2(e23,e21) = e20
| op2(e23,e20) = e20 )
& ( op2(e24,e22) = e24
| op2(e23,e22) = e24
| op2(e22,e22) = e24
| op2(e21,e22) = e24
| op2(e20,e22) = e24 )
& ( op2(e22,e24) = e24
| op2(e22,e23) = e24
| op2(e22,e22) = e24
| op2(e22,e21) = e24
| op2(e22,e20) = e24 )
& ( op2(e24,e22) = e23
| op2(e23,e22) = e23
| op2(e22,e22) = e23
| op2(e21,e22) = e23
| op2(e20,e22) = e23 )
& ( op2(e22,e24) = e23
| op2(e22,e23) = e23
| op2(e22,e22) = e23
| op2(e22,e21) = e23
| op2(e22,e20) = e23 )
& ( op2(e24,e22) = e22
| op2(e23,e22) = e22
| op2(e22,e22) = e22
| op2(e21,e22) = e22
| op2(e20,e22) = e22 )
& ( op2(e22,e24) = e22
| op2(e22,e23) = e22
| op2(e22,e22) = e22
| op2(e22,e21) = e22
| op2(e22,e20) = e22 )
& ( op2(e24,e22) = e21
| op2(e23,e22) = e21
| op2(e22,e22) = e21
| op2(e21,e22) = e21
| op2(e20,e22) = e21 )
& ( op2(e22,e24) = e21
| op2(e22,e23) = e21
| op2(e22,e22) = e21
| op2(e22,e21) = e21
| op2(e22,e20) = e21 )
& ( op2(e24,e22) = e20
| op2(e23,e22) = e20
| op2(e22,e22) = e20
| op2(e21,e22) = e20
| op2(e20,e22) = e20 )
& ( op2(e22,e24) = e20
| op2(e22,e23) = e20
| op2(e22,e22) = e20
| op2(e22,e21) = e20
| op2(e22,e20) = e20 )
& ( op2(e24,e21) = e24
| op2(e23,e21) = e24
| op2(e22,e21) = e24
| op2(e21,e21) = e24
| op2(e20,e21) = e24 )
& ( op2(e21,e24) = e24
| op2(e21,e23) = e24
| op2(e21,e22) = e24
| op2(e21,e21) = e24
| op2(e21,e20) = e24 )
& ( op2(e24,e21) = e23
| op2(e23,e21) = e23
| op2(e22,e21) = e23
| op2(e21,e21) = e23
| op2(e20,e21) = e23 )
& ( op2(e21,e24) = e23
| op2(e21,e23) = e23
| op2(e21,e22) = e23
| op2(e21,e21) = e23
| op2(e21,e20) = e23 )
& ( op2(e24,e21) = e22
| op2(e23,e21) = e22
| op2(e22,e21) = e22
| op2(e21,e21) = e22
| op2(e20,e21) = e22 )
& ( op2(e21,e24) = e22
| op2(e21,e23) = e22
| op2(e21,e22) = e22
| op2(e21,e21) = e22
| op2(e21,e20) = e22 )
& ( op2(e24,e21) = e21
| op2(e23,e21) = e21
| op2(e22,e21) = e21
| op2(e21,e21) = e21
| op2(e20,e21) = e21 )
& ( op2(e21,e24) = e21
| op2(e21,e23) = e21
| op2(e21,e22) = e21
| op2(e21,e21) = e21
| op2(e21,e20) = e21 )
& ( op2(e24,e21) = e20
| op2(e23,e21) = e20
| op2(e22,e21) = e20
| op2(e21,e21) = e20
| op2(e20,e21) = e20 )
& ( op2(e21,e24) = e20
| op2(e21,e23) = e20
| op2(e21,e22) = e20
| op2(e21,e21) = e20
| op2(e21,e20) = e20 )
& ( op2(e24,e20) = e24
| op2(e23,e20) = e24
| op2(e22,e20) = e24
| op2(e21,e20) = e24
| op2(e20,e20) = e24 )
& ( op2(e20,e24) = e24
| op2(e20,e23) = e24
| op2(e20,e22) = e24
| op2(e20,e21) = e24
| op2(e20,e20) = e24 )
& ( op2(e24,e20) = e23
| op2(e23,e20) = e23
| op2(e22,e20) = e23
| op2(e21,e20) = e23
| op2(e20,e20) = e23 )
& ( op2(e20,e24) = e23
| op2(e20,e23) = e23
| op2(e20,e22) = e23
| op2(e20,e21) = e23
| op2(e20,e20) = e23 )
& ( op2(e24,e20) = e22
| op2(e23,e20) = e22
| op2(e22,e20) = e22
| op2(e21,e20) = e22
| op2(e20,e20) = e22 )
& ( op2(e20,e24) = e22
| op2(e20,e23) = e22
| op2(e20,e22) = e22
| op2(e20,e21) = e22
| op2(e20,e20) = e22 )
& ( op2(e24,e20) = e21
| op2(e23,e20) = e21
| op2(e22,e20) = e21
| op2(e21,e20) = e21
| op2(e20,e20) = e21 )
& ( op2(e20,e24) = e21
| op2(e20,e23) = e21
| op2(e20,e22) = e21
| op2(e20,e21) = e21
| op2(e20,e20) = e21 )
& ( op2(e24,e20) = e20
| op2(e23,e20) = e20
| op2(e22,e20) = e20
| op2(e21,e20) = e20
| op2(e20,e20) = e20 )
& ( op2(e20,e24) = e20
| op2(e20,e23) = e20
| op2(e20,e22) = e20
| op2(e20,e21) = e20
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( op2(op2(e24,e24),op2(e24,e24)) = e24
& op2(op2(e23,e24),op2(e24,e23)) = e24
& op2(op2(e22,e24),op2(e24,e22)) = e24
& op2(op2(e21,e24),op2(e24,e21)) = e24
& op2(op2(e20,e24),op2(e24,e20)) = e24
& op2(op2(e24,e23),op2(e23,e24)) = e23
& op2(op2(e23,e23),op2(e23,e23)) = e23
& op2(op2(e22,e23),op2(e23,e22)) = e23
& op2(op2(e21,e23),op2(e23,e21)) = e23
& op2(op2(e20,e23),op2(e23,e20)) = e23
& op2(op2(e24,e22),op2(e22,e24)) = e22
& op2(op2(e23,e22),op2(e22,e23)) = e22
& op2(op2(e22,e22),op2(e22,e22)) = e22
& op2(op2(e21,e22),op2(e22,e21)) = e22
& op2(op2(e20,e22),op2(e22,e20)) = e22
& op2(op2(e24,e21),op2(e21,e24)) = e21
& op2(op2(e23,e21),op2(e21,e23)) = e21
& op2(op2(e22,e21),op2(e21,e22)) = e21
& op2(op2(e21,e21),op2(e21,e21)) = e21
& op2(op2(e20,e21),op2(e21,e20)) = e21
& op2(op2(e24,e20),op2(e20,e24)) = e20
& op2(op2(e23,e20),op2(e20,e23)) = e20
& op2(op2(e22,e20),op2(e20,e22)) = e20
& op2(op2(e21,e20),op2(e20,e21)) = e20
& op2(op2(e20,e20),op2(e20,e20)) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
( op1(e14,e13) != op1(e14,e14)
& op1(e14,e12) != op1(e14,e14)
& op1(e14,e12) != op1(e14,e13)
& op1(e14,e11) != op1(e14,e14)
& op1(e14,e11) != op1(e14,e13)
& op1(e14,e11) != op1(e14,e12)
& op1(e14,e10) != op1(e14,e14)
& op1(e14,e10) != op1(e14,e13)
& op1(e14,e10) != op1(e14,e12)
& op1(e14,e10) != op1(e14,e11)
& op1(e13,e13) != op1(e13,e14)
& op1(e13,e12) != op1(e13,e14)
& op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e14)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e14)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e13) != op1(e12,e14)
& op1(e12,e12) != op1(e12,e14)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e14)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e14)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e13) != op1(e11,e14)
& op1(e11,e12) != op1(e11,e14)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e14)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e14)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e13) != op1(e10,e14)
& op1(e10,e12) != op1(e10,e14)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e14)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e14)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e13,e14) != op1(e14,e14)
& op1(e12,e14) != op1(e14,e14)
& op1(e12,e14) != op1(e13,e14)
& op1(e11,e14) != op1(e14,e14)
& op1(e11,e14) != op1(e13,e14)
& op1(e11,e14) != op1(e12,e14)
& op1(e10,e14) != op1(e14,e14)
& op1(e10,e14) != op1(e13,e14)
& op1(e10,e14) != op1(e12,e14)
& op1(e10,e14) != op1(e11,e14)
& op1(e13,e13) != op1(e14,e13)
& op1(e12,e13) != op1(e14,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e14,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e14,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e13,e12) != op1(e14,e12)
& op1(e12,e12) != op1(e14,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e14,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e14,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e13,e11) != op1(e14,e11)
& op1(e12,e11) != op1(e14,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e14,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e14,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e13,e10) != op1(e14,e10)
& op1(e12,e10) != op1(e14,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e14,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e14,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
( op2(e24,e23) != op2(e24,e24)
& op2(e24,e22) != op2(e24,e24)
& op2(e24,e22) != op2(e24,e23)
& op2(e24,e21) != op2(e24,e24)
& op2(e24,e21) != op2(e24,e23)
& op2(e24,e21) != op2(e24,e22)
& op2(e24,e20) != op2(e24,e24)
& op2(e24,e20) != op2(e24,e23)
& op2(e24,e20) != op2(e24,e22)
& op2(e24,e20) != op2(e24,e21)
& op2(e23,e23) != op2(e23,e24)
& op2(e23,e22) != op2(e23,e24)
& op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e24)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e24)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e23) != op2(e22,e24)
& op2(e22,e22) != op2(e22,e24)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e24)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e24)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e23) != op2(e21,e24)
& op2(e21,e22) != op2(e21,e24)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e24)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e24)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e23) != op2(e20,e24)
& op2(e20,e22) != op2(e20,e24)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e24)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e24)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e23,e24) != op2(e24,e24)
& op2(e22,e24) != op2(e24,e24)
& op2(e22,e24) != op2(e23,e24)
& op2(e21,e24) != op2(e24,e24)
& op2(e21,e24) != op2(e23,e24)
& op2(e21,e24) != op2(e22,e24)
& op2(e20,e24) != op2(e24,e24)
& op2(e20,e24) != op2(e23,e24)
& op2(e20,e24) != op2(e22,e24)
& op2(e20,e24) != op2(e21,e24)
& op2(e23,e23) != op2(e24,e23)
& op2(e22,e23) != op2(e24,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e24,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e24,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e23,e22) != op2(e24,e22)
& op2(e22,e22) != op2(e24,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e24,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e24,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e23,e21) != op2(e24,e21)
& op2(e22,e21) != op2(e24,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e24,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e24,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e23,e20) != op2(e24,e20)
& op2(e22,e20) != op2(e24,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e24,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e24,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
fof(f9,axiom,
( e13 != e14
& e12 != e14
& e12 != e13
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( e23 != e24
& e22 != e24
& e22 != e23
& e21 != e24
& e21 != e23
& e21 != e22
& e20 != e24
& e20 != e23
& e20 != e22
& e20 != e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax10) ).
fof(f12,axiom,
( op1(e14,op1(e14,e14)) = e14
& op1(e14,op1(e14,e13)) = e13
& op1(e14,op1(e14,e12)) = e12
& op1(e14,op1(e14,e11)) = e11
& op1(e14,op1(e14,e10)) = e10
& op1(e13,op1(e13,e14)) = e14
& op1(e13,op1(e13,e13)) = e13
& op1(e13,op1(e13,e12)) = e12
& op1(e13,op1(e13,e11)) = e11
& op1(e13,op1(e13,e10)) = e10
& op1(e12,op1(e12,e14)) = e14
& op1(e12,op1(e12,e13)) = e13
& op1(e12,op1(e12,e12)) = e12
& op1(e12,op1(e12,e11)) = e11
& op1(e12,op1(e12,e10)) = e10
& op1(e11,op1(e11,e14)) = e14
& op1(e11,op1(e11,e13)) = e13
& op1(e11,op1(e11,e12)) = e12
& op1(e11,op1(e11,e11)) = e11
& op1(e11,op1(e11,e10)) = e10
& op1(e10,op1(e10,e14)) = e14
& op1(e10,op1(e10,e13)) = e13
& op1(e10,op1(e10,e12)) = e12
& op1(e10,op1(e10,e11)) = e11
& op1(e10,op1(e10,e10)) = e10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
( op2(e24,op2(e24,e24)) = e24
& op2(e24,op2(e24,e23)) = e23
& op2(e24,op2(e24,e22)) = e22
& op2(e24,op2(e24,e21)) = e21
& op2(e24,op2(e24,e20)) = e20
& op2(e23,op2(e23,e24)) = e24
& op2(e23,op2(e23,e23)) = e23
& op2(e23,op2(e23,e22)) = e22
& op2(e23,op2(e23,e21)) = e21
& op2(e23,op2(e23,e20)) = e20
& op2(e22,op2(e22,e24)) = e24
& op2(e22,op2(e22,e23)) = e23
& op2(e22,op2(e22,e22)) = e22
& op2(e22,op2(e22,e21)) = e21
& op2(e22,op2(e22,e20)) = e20
& op2(e21,op2(e21,e24)) = e24
& op2(e21,op2(e21,e23)) = e23
& op2(e21,op2(e21,e22)) = e22
& op2(e21,op2(e21,e21)) = e21
& op2(e21,op2(e21,e20)) = e20
& op2(e20,op2(e20,e24)) = e24
& op2(e20,op2(e20,e23)) = e23
& op2(e20,op2(e20,e22)) = e22
& op2(e20,op2(e20,e21)) = e21
& op2(e20,op2(e20,e20)) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
( e14 = op1(e13,e11)
& e12 = op1(e13,op1(op1(e13,e11),e13))
& e10 = op1(op1(e13,e11),e13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
( e24 = op2(e23,e21)
& e22 = op2(e23,op2(op2(e23,e21),e23))
& e20 = op2(op2(e23,e21),e23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
( h1(e14) = op2(e21,e20)
& h1(e12) = op2(e21,op2(op2(e21,e20),e21))
& h1(e10) = op2(op2(e21,e20),e21)
& h1(e13) = e21
& h1(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
( h2(e14) = op2(e22,e20)
& h2(e12) = op2(e22,op2(op2(e22,e20),e22))
& h2(e10) = op2(op2(e22,e20),e22)
& h2(e13) = e22
& h2(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
( h3(e14) = op2(e23,e20)
& h3(e12) = op2(e23,op2(op2(e23,e20),e23))
& h3(e10) = op2(op2(e23,e20),e23)
& h3(e13) = e23
& h3(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax18) ).
fof(f19,axiom,
( h4(e14) = op2(e24,e20)
& h4(e12) = op2(e24,op2(op2(e24,e20),e24))
& h4(e10) = op2(op2(e24,e20),e24)
& h4(e13) = e24
& h4(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f21,axiom,
( h6(e14) = op2(e22,e21)
& h6(e12) = op2(e22,op2(op2(e22,e21),e22))
& h6(e10) = op2(op2(e22,e21),e22)
& h6(e13) = e22
& h6(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
fof(f23,axiom,
( h8(e14) = op2(e24,e21)
& h8(e12) = op2(e24,op2(op2(e24,e21),e24))
& h8(e10) = op2(op2(e24,e21),e24)
& h8(e13) = e24
& h8(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
( h9(e14) = op2(e20,e22)
& h9(e12) = op2(e20,op2(op2(e20,e22),e20))
& h9(e10) = op2(op2(e20,e22),e20)
& h9(e13) = e20
& h9(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( h10(e14) = op2(e21,e22)
& h10(e12) = op2(e21,op2(op2(e21,e22),e21))
& h10(e10) = op2(op2(e21,e22),e21)
& h10(e13) = e21
& h10(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f27,axiom,
( h12(e14) = op2(e24,e22)
& h12(e12) = op2(e24,op2(op2(e24,e22),e24))
& h12(e10) = op2(op2(e24,e22),e24)
& h12(e13) = e24
& h12(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27) ).
fof(f30,axiom,
( h15(e14) = op2(e22,e23)
& h15(e12) = op2(e22,op2(op2(e22,e23),e22))
& h15(e10) = op2(op2(e22,e23),e22)
& h15(e13) = e22
& h15(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax30) ).
fof(f31,axiom,
( h16(e14) = op2(e24,e23)
& h16(e12) = op2(e24,op2(op2(e24,e23),e24))
& h16(e10) = op2(op2(e24,e23),e24)
& h16(e13) = e24
& h16(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax31) ).
fof(f32,axiom,
( h17(e14) = op2(e20,e24)
& h17(e12) = op2(e20,op2(op2(e20,e24),e20))
& h17(e10) = op2(op2(e20,e24),e20)
& h17(e13) = e20
& h17(e11) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax32) ).
fof(f34,axiom,
( h19(e14) = op2(e22,e24)
& h19(e12) = op2(e22,op2(op2(e22,e24),e22))
& h19(e10) = op2(op2(e22,e24),e22)
& h19(e13) = e22
& h19(e11) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax34) ).
fof(f156,plain,
( ~ sP43
| ( e21 != h10(e14)
& e21 != h10(e13)
& e21 != h10(e12)
& e21 != h10(e11)
& e21 != h10(e10) ) ),
inference(nnf_transformation,[],[f82]) ).
fof(f157,plain,
( ~ sP42
| ( e22 != h10(e14)
& e22 != h10(e13)
& e22 != h10(e12)
& e22 != h10(e11)
& e22 != h10(e10) ) ),
inference(nnf_transformation,[],[f81]) ).
fof(f158,plain,
( ~ sP41
| ( e23 != h10(e14)
& e23 != h10(e13)
& e23 != h10(e12)
& e23 != h10(e11)
& e23 != h10(e10) ) ),
inference(nnf_transformation,[],[f80]) ).
fof(f159,plain,
( ~ sP40
| ( e24 != h10(e14)
& e24 != h10(e13)
& e24 != h10(e12)
& e24 != h10(e11)
& e24 != h10(e10) ) ),
inference(nnf_transformation,[],[f79]) ).
fof(f200,plain,
( e14 = op1(e14,e14)
| e13 = op1(e14,e14)
| e12 = op1(e14,e14)
| e11 = op1(e14,e14)
| e10 = op1(e14,e14) ),
inference(cnf_transformation,[],[f1]) ).
fof(f206,plain,
( e14 = op1(e13,e13)
| e13 = op1(e13,e13)
| e12 = op1(e13,e13)
| e11 = op1(e13,e13)
| e10 = op1(e13,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f218,plain,
( e14 = op1(e11,e11)
| e13 = op1(e11,e11)
| e12 = op1(e11,e11)
| e11 = op1(e11,e11)
| e10 = op1(e11,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f250,plain,
( e12 = op1(e12,e14)
| e12 = op1(e12,e13)
| e12 = op1(e12,e12)
| e12 = op1(e12,e11)
| e12 = op1(e12,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f273,plain,
( e10 = op1(e14,e10)
| e10 = op1(e13,e10)
| e10 = op1(e12,e10)
| e10 = op1(e11,e10)
| e10 = op1(e10,e10) ),
inference(cnf_transformation,[],[f2]) ).
fof(f276,plain,
e14 = op1(op1(e13,e14),op1(e14,e13)),
inference(cnf_transformation,[],[f3]) ).
fof(f278,plain,
e14 = op1(op1(e11,e14),op1(e14,e11)),
inference(cnf_transformation,[],[f3]) ).
fof(f280,plain,
e13 = op1(op1(e14,e13),op1(e13,e14)),
inference(cnf_transformation,[],[f3]) ).
fof(f283,plain,
e13 = op1(op1(e11,e13),op1(e13,e11)),
inference(cnf_transformation,[],[f3]) ).
fof(f284,plain,
e13 = op1(op1(e10,e13),op1(e13,e10)),
inference(cnf_transformation,[],[f3]) ).
fof(f286,plain,
e12 = op1(op1(e13,e12),op1(e12,e13)),
inference(cnf_transformation,[],[f3]) ).
fof(f291,plain,
e11 = op1(op1(e13,e11),op1(e11,e13)),
inference(cnf_transformation,[],[f3]) ).
fof(f296,plain,
e10 = op1(op1(e13,e10),op1(e10,e13)),
inference(cnf_transformation,[],[f3]) ).
fof(f306,plain,
( e24 = op2(e23,e23)
| e23 = op2(e23,e23)
| e22 = op2(e23,e23)
| e21 = op2(e23,e23)
| e20 = op2(e23,e23) ),
inference(cnf_transformation,[],[f4]) ).
fof(f318,plain,
( e24 = op2(e21,e21)
| e23 = op2(e21,e21)
| e22 = op2(e21,e21)
| e21 = op2(e21,e21)
| e20 = op2(e21,e21) ),
inference(cnf_transformation,[],[f4]) ).
fof(f326,plain,
( e24 = op2(e24,e24)
| e24 = op2(e24,e23)
| e24 = op2(e24,e22)
| e24 = op2(e24,e21)
| e24 = op2(e24,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f350,plain,
( e22 = op2(e22,e24)
| e22 = op2(e22,e23)
| e22 = op2(e22,e22)
| e22 = op2(e22,e21)
| e22 = op2(e22,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f373,plain,
( e20 = op2(e24,e20)
| e20 = op2(e23,e20)
| e20 = op2(e22,e20)
| e20 = op2(e21,e20)
| e20 = op2(e20,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f376,plain,
e24 = op2(op2(e23,e24),op2(e24,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f378,plain,
e24 = op2(op2(e21,e24),op2(e24,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f380,plain,
e23 = op2(op2(e24,e23),op2(e23,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f383,plain,
e23 = op2(op2(e21,e23),op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f384,plain,
e23 = op2(op2(e20,e23),op2(e23,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f386,plain,
e22 = op2(op2(e23,e22),op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f391,plain,
e21 = op2(op2(e23,e21),op2(e21,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f396,plain,
e20 = op2(op2(e23,e20),op2(e20,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f400,plain,
op1(e14,e13) != op1(e14,e14),
inference(cnf_transformation,[],[f7]) ).
fof(f403,plain,
op1(e14,e11) != op1(e14,e14),
inference(cnf_transformation,[],[f7]) ).
fof(f406,plain,
op1(e14,e10) != op1(e14,e14),
inference(cnf_transformation,[],[f7]) ).
fof(f407,plain,
op1(e14,e10) != op1(e14,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f410,plain,
op1(e13,e13) != op1(e13,e14),
inference(cnf_transformation,[],[f7]) ).
fof(f414,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f417,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f429,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f433,plain,
op1(e11,e11) != op1(e11,e14),
inference(cnf_transformation,[],[f7]) ).
fof(f434,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f450,plain,
op1(e13,e14) != op1(e14,e14),
inference(cnf_transformation,[],[f7]) ).
fof(f460,plain,
op1(e13,e13) != op1(e14,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f465,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f7]) ).
fof(f484,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f489,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f7]) ).
fof(f492,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f7]) ).
fof(f507,plain,
op2(e24,e20) != op2(e24,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f510,plain,
op2(e23,e23) != op2(e23,e24),
inference(cnf_transformation,[],[f8]) ).
fof(f514,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f517,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f529,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f8]) ).
fof(f533,plain,
op2(e21,e21) != op2(e21,e24),
inference(cnf_transformation,[],[f8]) ).
fof(f534,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f560,plain,
op2(e23,e23) != op2(e24,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f565,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f8]) ).
fof(f580,plain,
op2(e23,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f8]) ).
fof(f584,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f8]) ).
fof(f589,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f8]) ).
fof(f592,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f8]) ).
fof(f602,plain,
e12 != e13,
inference(cnf_transformation,[],[f9]) ).
fof(f606,plain,
e10 != e14,
inference(cnf_transformation,[],[f9]) ).
fof(f608,plain,
e10 != e12,
inference(cnf_transformation,[],[f9]) ).
fof(f610,plain,
e23 != e24,
inference(cnf_transformation,[],[f10]) ).
fof(f612,plain,
e22 != e23,
inference(cnf_transformation,[],[f10]) ).
fof(f613,plain,
e21 != e24,
inference(cnf_transformation,[],[f10]) ).
fof(f616,plain,
e20 != e24,
inference(cnf_transformation,[],[f10]) ).
fof(f618,plain,
e20 != e22,
inference(cnf_transformation,[],[f10]) ).
fof(f646,plain,
e13 = op1(e14,op1(e14,e13)),
inference(cnf_transformation,[],[f12]) ).
fof(f647,plain,
e12 = op1(e14,op1(e14,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f653,plain,
e11 = op1(e13,op1(e13,e11)),
inference(cnf_transformation,[],[f12]) ).
fof(f654,plain,
e10 = op1(e13,op1(e13,e10)),
inference(cnf_transformation,[],[f12]) ).
fof(f655,plain,
e14 = op1(e12,op1(e12,e14)),
inference(cnf_transformation,[],[f12]) ).
fof(f658,plain,
e11 = op1(e12,op1(e12,e11)),
inference(cnf_transformation,[],[f12]) ).
fof(f662,plain,
e12 = op1(e11,op1(e11,e12)),
inference(cnf_transformation,[],[f12]) ).
fof(f664,plain,
e10 = op1(e11,op1(e11,e10)),
inference(cnf_transformation,[],[f12]) ).
fof(f668,plain,
e11 = op1(e10,op1(e10,e11)),
inference(cnf_transformation,[],[f12]) ).
fof(f671,plain,
e23 = op2(e24,op2(e24,e23)),
inference(cnf_transformation,[],[f13]) ).
fof(f672,plain,
e22 = op2(e24,op2(e24,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f678,plain,
e21 = op2(e23,op2(e23,e21)),
inference(cnf_transformation,[],[f13]) ).
fof(f679,plain,
e20 = op2(e23,op2(e23,e20)),
inference(cnf_transformation,[],[f13]) ).
fof(f680,plain,
e24 = op2(e22,op2(e22,e24)),
inference(cnf_transformation,[],[f13]) ).
fof(f683,plain,
e21 = op2(e22,op2(e22,e21)),
inference(cnf_transformation,[],[f13]) ).
fof(f687,plain,
e22 = op2(e21,op2(e21,e22)),
inference(cnf_transformation,[],[f13]) ).
fof(f689,plain,
e20 = op2(e21,op2(e21,e20)),
inference(cnf_transformation,[],[f13]) ).
fof(f693,plain,
e21 = op2(e20,op2(e20,e21)),
inference(cnf_transformation,[],[f13]) ).
fof(f695,plain,
e14 = op1(e13,e11),
inference(cnf_transformation,[],[f14]) ).
fof(f696,plain,
e12 = op1(e13,op1(op1(e13,e11),e13)),
inference(cnf_transformation,[],[f14]) ).
fof(f697,plain,
e10 = op1(op1(e13,e11),e13),
inference(cnf_transformation,[],[f14]) ).
fof(f698,plain,
e24 = op2(e23,e21),
inference(cnf_transformation,[],[f15]) ).
fof(f699,plain,
e22 = op2(e23,op2(op2(e23,e21),e23)),
inference(cnf_transformation,[],[f15]) ).
fof(f700,plain,
e20 = op2(op2(e23,e21),e23),
inference(cnf_transformation,[],[f15]) ).
fof(f701,plain,
op2(e21,e20) = h1(e14),
inference(cnf_transformation,[],[f16]) ).
fof(f703,plain,
h1(e10) = op2(op2(e21,e20),e21),
inference(cnf_transformation,[],[f16]) ).
fof(f705,plain,
e20 = h1(e11),
inference(cnf_transformation,[],[f16]) ).
fof(f706,plain,
op2(e22,e20) = h2(e14),
inference(cnf_transformation,[],[f17]) ).
fof(f711,plain,
op2(e23,e20) = h3(e14),
inference(cnf_transformation,[],[f18]) ).
fof(f713,plain,
h3(e10) = op2(op2(e23,e20),e23),
inference(cnf_transformation,[],[f18]) ).
fof(f715,plain,
e20 = h3(e11),
inference(cnf_transformation,[],[f18]) ).
fof(f716,plain,
op2(e24,e20) = h4(e14),
inference(cnf_transformation,[],[f19]) ).
fof(f726,plain,
op2(e22,e21) = h6(e14),
inference(cnf_transformation,[],[f21]) ).
fof(f736,plain,
op2(e24,e21) = h8(e14),
inference(cnf_transformation,[],[f23]) ).
fof(f741,plain,
op2(e20,e22) = h9(e14),
inference(cnf_transformation,[],[f24]) ).
fof(f746,plain,
op2(e21,e22) = h10(e14),
inference(cnf_transformation,[],[f25]) ).
fof(f747,plain,
h10(e12) = op2(e21,op2(op2(e21,e22),e21)),
inference(cnf_transformation,[],[f25]) ).
fof(f748,plain,
h10(e10) = op2(op2(e21,e22),e21),
inference(cnf_transformation,[],[f25]) ).
fof(f749,plain,
e21 = h10(e13),
inference(cnf_transformation,[],[f25]) ).
fof(f750,plain,
e22 = h10(e11),
inference(cnf_transformation,[],[f25]) ).
fof(f756,plain,
op2(e24,e22) = h12(e14),
inference(cnf_transformation,[],[f27]) ).
fof(f771,plain,
op2(e22,e23) = h15(e14),
inference(cnf_transformation,[],[f30]) ).
fof(f776,plain,
op2(e24,e23) = h16(e14),
inference(cnf_transformation,[],[f31]) ).
fof(f781,plain,
op2(e20,e24) = h17(e14),
inference(cnf_transformation,[],[f32]) ).
fof(f791,plain,
op2(e22,e24) = h19(e14),
inference(cnf_transformation,[],[f34]) ).
fof(f982,plain,
( ~ sP43
| e21 != h10(e13) ),
inference(cnf_transformation,[],[f156]) ).
fof(f989,plain,
( ~ sP42
| e22 != h10(e11) ),
inference(cnf_transformation,[],[f157]) ).
fof(f991,plain,
( ~ sP41
| e23 != h10(e14) ),
inference(cnf_transformation,[],[f158]) ).
fof(f1000,plain,
( ~ sP40
| e24 != h10(e10) ),
inference(cnf_transformation,[],[f159]) ).
fof(f1253,plain,
( sP40
| sP41
| sP42
| sP43
| e20 != h10(e12)
| h10(op1(e14,e14)) != op2(h10(e14),h10(e14))
| h10(op1(e14,e13)) != op2(h10(e14),h10(e13))
| h10(op1(e14,e12)) != op2(h10(e14),h10(e12))
| h10(op1(e14,e11)) != op2(h10(e14),h10(e11))
| h10(op1(e14,e10)) != op2(h10(e14),h10(e10))
| h10(op1(e13,e14)) != op2(h10(e13),h10(e14))
| h10(op1(e13,e13)) != op2(h10(e13),h10(e13))
| h10(op1(e13,e12)) != op2(h10(e13),h10(e12))
| h10(op1(e13,e11)) != op2(h10(e13),h10(e11))
| h10(op1(e13,e10)) != op2(h10(e13),h10(e10))
| h10(op1(e12,e14)) != op2(h10(e12),h10(e14))
| h10(op1(e12,e13)) != op2(h10(e12),h10(e13))
| h10(op1(e12,e12)) != op2(h10(e12),h10(e12))
| h10(op1(e12,e11)) != op2(h10(e12),h10(e11))
| h10(op1(e12,e10)) != op2(h10(e12),h10(e10))
| h10(op1(e11,e14)) != op2(h10(e11),h10(e14))
| h10(op1(e11,e13)) != op2(h10(e11),h10(e13))
| h10(op1(e11,e12)) != op2(h10(e11),h10(e12))
| h10(op1(e11,e11)) != op2(h10(e11),h10(e11))
| h10(op1(e11,e10)) != op2(h10(e11),h10(e10))
| h10(op1(e10,e14)) != op2(h10(e10),h10(e14))
| h10(op1(e10,e13)) != op2(h10(e10),h10(e13))
| h10(op1(e10,e12)) != op2(h10(e10),h10(e12))
| h10(op1(e10,e11)) != op2(h10(e10),h10(e11))
| h10(op1(e10,e10)) != op2(h10(e10),h10(e10)) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_55,plain,
( ( op1(e11,e11) = e14 )
| ( op1(e11,e11) = e13 )
| ( op1(e11,e11) = e12 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e11) = e10 ) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_67,plain,
( ( op1(e13,e13) = e14 )
| ( op1(e13,e13) = e13 )
| ( op1(e13,e13) = e12 )
| ( op1(e13,e13) = e11 )
| ( op1(e13,e13) = e10 ) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_73,plain,
( ( op1(e14,e14) = e14 )
| ( op1(e14,e14) = e13 )
| ( op1(e14,e14) = e12 )
| ( op1(e14,e14) = e11 )
| ( op1(e14,e14) = e10 ) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_75,plain,
( ( op1(e14,e10) = e10 )
| ( op1(e13,e10) = e10 )
| ( op1(e12,e10) = e10 )
| ( op1(e11,e10) = e10 )
| ( op1(e10,e10) = e10 ) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_98,plain,
( ( op1(e12,e14) = e12 )
| ( op1(e12,e13) = e12 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e10) = e12 ) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_127,plain,
op1(op1(e13,e10),op1(e10,e13)) = e10,
inference(cnf_transformation,[],[f296]) ).
tcf(c_132,plain,
op1(op1(e13,e11),op1(e11,e13)) = e11,
inference(cnf_transformation,[],[f291]) ).
tcf(c_137,plain,
op1(op1(e13,e12),op1(e12,e13)) = e12,
inference(cnf_transformation,[],[f286]) ).
tcf(c_139,plain,
op1(op1(e10,e13),op1(e13,e10)) = e13,
inference(cnf_transformation,[],[f284]) ).
tcf(c_140,plain,
op1(op1(e11,e13),op1(e13,e11)) = e13,
inference(cnf_transformation,[],[f283]) ).
tcf(c_143,plain,
op1(op1(e14,e13),op1(e13,e14)) = e13,
inference(cnf_transformation,[],[f280]) ).
tcf(c_145,plain,
op1(op1(e11,e14),op1(e14,e11)) = e14,
inference(cnf_transformation,[],[f278]) ).
tcf(c_147,plain,
op1(op1(e13,e14),op1(e14,e13)) = e14,
inference(cnf_transformation,[],[f276]) ).
tcf(c_155,plain,
( ( op2(e21,e21) = e24 )
| ( op2(e21,e21) = e23 )
| ( op2(e21,e21) = e22 )
| ( op2(e21,e21) = e21 )
| ( op2(e21,e21) = e20 ) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_167,plain,
( ( op2(e23,e23) = e24 )
| ( op2(e23,e23) = e23 )
| ( op2(e23,e23) = e22 )
| ( op2(e23,e23) = e21 )
| ( op2(e23,e23) = e20 ) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_175,plain,
( ( op2(e24,e20) = e20 )
| ( op2(e23,e20) = e20 )
| ( op2(e22,e20) = e20 )
| ( op2(e21,e20) = e20 )
| ( op2(e20,e20) = e20 ) ),
inference(cnf_transformation,[],[f373]) ).
tcf(c_198,plain,
( ( op2(e22,e24) = e22 )
| ( op2(e22,e23) = e22 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e20) = e22 ) ),
inference(cnf_transformation,[],[f350]) ).
tcf(c_222,plain,
( ( op2(e24,e24) = e24 )
| ( op2(e24,e23) = e24 )
| ( op2(e24,e22) = e24 )
| ( op2(e24,e21) = e24 )
| ( op2(e24,e20) = e24 ) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_227,plain,
op2(op2(e23,e20),op2(e20,e23)) = e20,
inference(cnf_transformation,[],[f396]) ).
tcf(c_232,plain,
op2(op2(e23,e21),op2(e21,e23)) = e21,
inference(cnf_transformation,[],[f391]) ).
tcf(c_237,plain,
op2(op2(e23,e22),op2(e22,e23)) = e22,
inference(cnf_transformation,[],[f386]) ).
tcf(c_239,plain,
op2(op2(e20,e23),op2(e23,e20)) = e23,
inference(cnf_transformation,[],[f384]) ).
tcf(c_240,plain,
op2(op2(e21,e23),op2(e23,e21)) = e23,
inference(cnf_transformation,[],[f383]) ).
tcf(c_243,plain,
op2(op2(e24,e23),op2(e23,e24)) = e23,
inference(cnf_transformation,[],[f380]) ).
tcf(c_245,plain,
op2(op2(e21,e24),op2(e24,e21)) = e24,
inference(cnf_transformation,[],[f378]) ).
tcf(c_247,plain,
op2(op2(e23,e24),op2(e24,e23)) = e24,
inference(cnf_transformation,[],[f376]) ).
tcf(c_256,plain,
op1(e12,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f492]) ).
tcf(c_259,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f489]) ).
tcf(c_264,plain,
op1(e11,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f484]) ).
tcf(c_283,plain,
op1(e11,e13) != op1(e12,e13),
inference(cnf_transformation,[],[f465]) ).
tcf(c_288,plain,
op1(e13,e13) != op1(e14,e13),
inference(cnf_transformation,[],[f460]) ).
tcf(c_298,plain,
op1(e13,e14) != op1(e14,e14),
inference(cnf_transformation,[],[f450]) ).
tcf(c_314,plain,
op1(e11,e11) != op1(e11,e13),
inference(cnf_transformation,[],[f434]) ).
tcf(c_315,plain,
op1(e11,e11) != op1(e11,e14),
inference(cnf_transformation,[],[f433]) ).
tcf(c_319,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f429]) ).
tcf(c_331,plain,
op1(e13,e10) != op1(e13,e13),
inference(cnf_transformation,[],[f417]) ).
tcf(c_334,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f414]) ).
tcf(c_338,plain,
op1(e13,e13) != op1(e13,e14),
inference(cnf_transformation,[],[f410]) ).
tcf(c_341,plain,
op1(e14,e10) != op1(e14,e13),
inference(cnf_transformation,[],[f407]) ).
tcf(c_342,plain,
op1(e14,e10) != op1(e14,e14),
inference(cnf_transformation,[],[f406]) ).
tcf(c_345,plain,
op1(e14,e11) != op1(e14,e14),
inference(cnf_transformation,[],[f403]) ).
tcf(c_348,plain,
op1(e14,e13) != op1(e14,e14),
inference(cnf_transformation,[],[f400]) ).
tcf(c_356,plain,
op2(e22,e20) != op2(e23,e20),
inference(cnf_transformation,[],[f592]) ).
tcf(c_359,plain,
op2(e20,e21) != op2(e21,e21),
inference(cnf_transformation,[],[f589]) ).
tcf(c_364,plain,
op2(e21,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f584]) ).
tcf(c_368,plain,
op2(e23,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f580]) ).
tcf(c_383,plain,
op2(e21,e23) != op2(e22,e23),
inference(cnf_transformation,[],[f565]) ).
tcf(c_388,plain,
op2(e23,e23) != op2(e24,e23),
inference(cnf_transformation,[],[f560]) ).
tcf(c_414,plain,
op2(e21,e21) != op2(e21,e23),
inference(cnf_transformation,[],[f534]) ).
tcf(c_415,plain,
op2(e21,e21) != op2(e21,e24),
inference(cnf_transformation,[],[f533]) ).
tcf(c_419,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f529]) ).
tcf(c_431,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f517]) ).
tcf(c_434,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f514]) ).
tcf(c_438,plain,
op2(e23,e23) != op2(e23,e24),
inference(cnf_transformation,[],[f510]) ).
tcf(c_441,plain,
op2(e24,e20) != op2(e24,e23),
inference(cnf_transformation,[],[f507]) ).
tcf(c_450,plain,
e10 != e12,
inference(cnf_transformation,[],[f608]) ).
tcf(c_452,plain,
e10 != e14,
inference(cnf_transformation,[],[f606]) ).
tcf(c_456,plain,
e12 != e13,
inference(cnf_transformation,[],[f602]) ).
tcf(c_460,plain,
e20 != e22,
inference(cnf_transformation,[],[f618]) ).
tcf(c_462,plain,
e20 != e24,
inference(cnf_transformation,[],[f616]) ).
tcf(c_465,plain,
e21 != e24,
inference(cnf_transformation,[],[f613]) ).
tcf(c_466,plain,
e22 != e23,
inference(cnf_transformation,[],[f612]) ).
tcf(c_468,plain,
e23 != e24,
inference(cnf_transformation,[],[f610]) ).
tcf(c_495,plain,
op1(e10,op1(e10,e11)) = e11,
inference(cnf_transformation,[],[f668]) ).
tcf(c_499,plain,
op1(e11,op1(e11,e10)) = e10,
inference(cnf_transformation,[],[f664]) ).
tcf(c_501,plain,
op1(e11,op1(e11,e12)) = e12,
inference(cnf_transformation,[],[f662]) ).
tcf(c_505,plain,
op1(e12,op1(e12,e11)) = e11,
inference(cnf_transformation,[],[f658]) ).
tcf(c_508,plain,
op1(e12,op1(e12,e14)) = e14,
inference(cnf_transformation,[],[f655]) ).
tcf(c_509,plain,
op1(e13,op1(e13,e10)) = e10,
inference(cnf_transformation,[],[f654]) ).
tcf(c_510,plain,
op1(e13,op1(e13,e11)) = e11,
inference(cnf_transformation,[],[f653]) ).
tcf(c_516,plain,
op1(e14,op1(e14,e12)) = e12,
inference(cnf_transformation,[],[f647]) ).
tcf(c_517,plain,
op1(e14,op1(e14,e13)) = e13,
inference(cnf_transformation,[],[f646]) ).
tcf(c_520,plain,
op2(e20,op2(e20,e21)) = e21,
inference(cnf_transformation,[],[f693]) ).
tcf(c_524,plain,
op2(e21,op2(e21,e20)) = e20,
inference(cnf_transformation,[],[f689]) ).
tcf(c_526,plain,
op2(e21,op2(e21,e22)) = e22,
inference(cnf_transformation,[],[f687]) ).
tcf(c_530,plain,
op2(e22,op2(e22,e21)) = e21,
inference(cnf_transformation,[],[f683]) ).
tcf(c_533,plain,
op2(e22,op2(e22,e24)) = e24,
inference(cnf_transformation,[],[f680]) ).
tcf(c_534,plain,
op2(e23,op2(e23,e20)) = e20,
inference(cnf_transformation,[],[f679]) ).
tcf(c_535,plain,
op2(e23,op2(e23,e21)) = e21,
inference(cnf_transformation,[],[f678]) ).
tcf(c_541,plain,
op2(e24,op2(e24,e22)) = e22,
inference(cnf_transformation,[],[f672]) ).
tcf(c_542,plain,
op2(e24,op2(e24,e23)) = e23,
inference(cnf_transformation,[],[f671]) ).
tcf(c_544,plain,
op1(op1(e13,e11),e13) = e10,
inference(cnf_transformation,[],[f697]) ).
tcf(c_545,plain,
op1(e13,op1(op1(e13,e11),e13)) = e12,
inference(cnf_transformation,[],[f696]) ).
tcf(c_546,plain,
op1(e13,e11) = e14,
inference(cnf_transformation,[],[f695]) ).
tcf(c_547,plain,
op2(op2(e23,e21),e23) = e20,
inference(cnf_transformation,[],[f700]) ).
tcf(c_548,plain,
op2(e23,op2(op2(e23,e21),e23)) = e22,
inference(cnf_transformation,[],[f699]) ).
tcf(c_549,plain,
op2(e23,e21) = e24,
inference(cnf_transformation,[],[f698]) ).
tcf(c_550,plain,
h1(e11) = e20,
inference(cnf_transformation,[],[f705]) ).
tcf(c_552,plain,
op2(op2(e21,e20),e21) = h1(e10),
inference(cnf_transformation,[],[f703]) ).
tcf(c_554,plain,
op2(e21,e20) = h1(e14),
inference(cnf_transformation,[],[f701]) ).
tcf(c_559,plain,
op2(e22,e20) = h2(e14),
inference(cnf_transformation,[],[f706]) ).
tcf(c_560,plain,
h3(e11) = e20,
inference(cnf_transformation,[],[f715]) ).
tcf(c_562,plain,
op2(op2(e23,e20),e23) = h3(e10),
inference(cnf_transformation,[],[f713]) ).
tcf(c_564,plain,
op2(e23,e20) = h3(e14),
inference(cnf_transformation,[],[f711]) ).
tcf(c_569,plain,
op2(e24,e20) = h4(e14),
inference(cnf_transformation,[],[f716]) ).
tcf(c_579,plain,
op2(e22,e21) = h6(e14),
inference(cnf_transformation,[],[f726]) ).
tcf(c_589,plain,
op2(e24,e21) = h8(e14),
inference(cnf_transformation,[],[f736]) ).
tcf(c_594,plain,
op2(e20,e22) = h9(e14),
inference(cnf_transformation,[],[f741]) ).
tcf(c_595,plain,
h10(e11) = e22,
inference(cnf_transformation,[],[f750]) ).
tcf(c_596,plain,
h10(e13) = e21,
inference(cnf_transformation,[],[f749]) ).
tcf(c_597,plain,
op2(op2(e21,e22),e21) = h10(e10),
inference(cnf_transformation,[],[f748]) ).
tcf(c_598,plain,
op2(e21,op2(op2(e21,e22),e21)) = h10(e12),
inference(cnf_transformation,[],[f747]) ).
tcf(c_599,plain,
op2(e21,e22) = h10(e14),
inference(cnf_transformation,[],[f746]) ).
tcf(c_609,plain,
op2(e24,e22) = h12(e14),
inference(cnf_transformation,[],[f756]) ).
tcf(c_624,plain,
op2(e22,e23) = h15(e14),
inference(cnf_transformation,[],[f771]) ).
tcf(c_629,plain,
op2(e24,e23) = h16(e14),
inference(cnf_transformation,[],[f776]) ).
tcf(c_634,plain,
op2(e20,e24) = h17(e14),
inference(cnf_transformation,[],[f781]) ).
tcf(c_644,plain,
op2(e22,e24) = h19(e14),
inference(cnf_transformation,[],[f791]) ).
tcf(c_833,plain,
( ~ sP43
| ( h10(e13) != e21 ) ),
inference(cnf_transformation,[],[f982]) ).
tcf(c_836,plain,
( ~ sP42
| ( h10(e11) != e22 ) ),
inference(cnf_transformation,[],[f989]) ).
tcf(c_844,plain,
( ~ sP41
| ( h10(e14) != e23 ) ),
inference(cnf_transformation,[],[f991]) ).
tcf(c_845,plain,
( ~ sP40
| ( h10(e10) != e24 ) ),
inference(cnf_transformation,[],[f1000]) ).
tcf(c_1097,negated_conjecture,
( sP40
| sP41
| sP42
| sP43
| ( h10(e12) != e20 )
| ( op2(h10(e14),h10(e14)) != h10(op1(e14,e14)) )
| ( op2(h10(e14),h10(e13)) != h10(op1(e14,e13)) )
| ( op2(h10(e14),h10(e12)) != h10(op1(e14,e12)) )
| ( op2(h10(e14),h10(e11)) != h10(op1(e14,e11)) )
| ( op2(h10(e14),h10(e10)) != h10(op1(e14,e10)) )
| ( op2(h10(e13),h10(e14)) != h10(op1(e13,e14)) )
| ( op2(h10(e13),h10(e13)) != h10(op1(e13,e13)) )
| ( op2(h10(e13),h10(e12)) != h10(op1(e13,e12)) )
| ( op2(h10(e13),h10(e11)) != h10(op1(e13,e11)) )
| ( op2(h10(e13),h10(e10)) != h10(op1(e13,e10)) )
| ( op2(h10(e12),h10(e14)) != h10(op1(e12,e14)) )
| ( op2(h10(e12),h10(e13)) != h10(op1(e12,e13)) )
| ( op2(h10(e12),h10(e12)) != h10(op1(e12,e12)) )
| ( op2(h10(e12),h10(e11)) != h10(op1(e12,e11)) )
| ( op2(h10(e12),h10(e10)) != h10(op1(e12,e10)) )
| ( op2(h10(e11),h10(e14)) != h10(op1(e11,e14)) )
| ( op2(h10(e11),h10(e13)) != h10(op1(e11,e13)) )
| ( op2(h10(e11),h10(e12)) != h10(op1(e11,e12)) )
| ( op2(h10(e11),h10(e11)) != h10(op1(e11,e11)) )
| ( op2(h10(e11),h10(e10)) != h10(op1(e11,e10)) )
| ( op2(h10(e10),h10(e14)) != h10(op1(e10,e14)) )
| ( op2(h10(e10),h10(e13)) != h10(op1(e10,e13)) )
| ( op2(h10(e10),h10(e12)) != h10(op1(e10,e12)) )
| ( op2(h10(e10),h10(e11)) != h10(op1(e10,e11)) )
| ( op2(h10(e10),h10(e10)) != h10(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f1253]) ).
tcf(c_1150,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_1097,c_845,c_844,c_836,c_833,c_644,c_634,c_629,c_624,c_609,c_599,c_598,c_597,c_596,c_595,c_594,c_589,c_579,c_569,c_564,c_562,c_560,c_559,c_554,c_552,c_550,c_549,c_548,c_547,c_546,c_545,c_544,c_542,c_541,c_535,c_534,c_533,c_530,c_526,c_524,c_520,c_517,c_516,c_510,c_509,c_508,c_505,c_501,c_499,c_495,c_468,c_466,c_465,c_462,c_460,c_456,c_452,c_450,c_441,c_438,c_434,c_431,c_419,c_415,c_414,c_388,c_383,c_368,c_364,c_359,c_356,c_348,c_345,c_342,c_341,c_338,c_334,c_331,c_319,c_315,c_314,c_298,c_288,c_283,c_264,c_259,c_256,c_247,c_245,c_243,c_240,c_239,c_237,c_232,c_227,c_222,c_198,c_175,c_167,c_155,c_147,c_145,c_143,c_140,c_139,c_137,c_132,c_127,c_98,c_75,c_73,c_67,c_55]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG168+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.38 % Computer : n009.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.39 % CPULimit : 300
% 0.09/0.39 % WCLimit : 300
% 0.09/0.39 % DateTime : Fri Sep 25 04:57:29 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.43 Running first-order theorem proving
% 0.09/0.43 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.44
% 0.09/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.44
% 0.09/0.44 % Detected problem language: tptp
% 0.09/0.45 % Proving...
% 1.09/1.74 % SZS status Started for theBenchmark.p
% 1.09/1.74 % SZS status Theorem for theBenchmark.p
% 1.09/1.74
% 1.09/1.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.09/1.74
% 1.09/1.74 % ------ iProver source info
% 1.09/1.74
% 1.09/1.74 % git: date: 2026-07-19 20:42:38 +0200
% 1.09/1.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.09/1.74 % git: non_committed_changes: false
% 1.09/1.74
% 1.09/1.74 % ------ Parsing...
% 1.09/1.74 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.09/1.74
% 1.09/1.74 % ------ Preprocessing...%
% 1.09/1.74
% 1.09/1.74 % ------ Preprocessing...%
% 1.09/1.74
% 1.09/1.74 % SZS status Theorem for theBenchmark.p
% 1.09/1.74
% 1.09/1.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.09/1.75
% 1.09/1.75
%------------------------------------------------------------------------------