%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG027+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 : n010.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:12 PM UTC 2026
% Result : Theorem 23.33s 8.82s
% Output : CNFRefutation 23.33s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f213ERROR: Could not build tree for root c_3453ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e15,e15) = e15
| op1(e15,e15) = e14
| op1(e15,e15) = e13
| op1(e15,e15) = e12
| op1(e15,e15) = e11
| op1(e15,e15) = e10 )
& ( op1(e15,e14) = e15
| op1(e15,e14) = e14
| op1(e15,e14) = e13
| op1(e15,e14) = e12
| op1(e15,e14) = e11
| op1(e15,e14) = e10 )
& ( op1(e15,e13) = e15
| op1(e15,e13) = e14
| op1(e15,e13) = e13
| op1(e15,e13) = e12
| op1(e15,e13) = e11
| op1(e15,e13) = e10 )
& ( op1(e15,e12) = e15
| op1(e15,e12) = e14
| op1(e15,e12) = e13
| op1(e15,e12) = e12
| op1(e15,e12) = e11
| op1(e15,e12) = e10 )
& ( op1(e15,e11) = e15
| op1(e15,e11) = e14
| op1(e15,e11) = e13
| op1(e15,e11) = e12
| op1(e15,e11) = e11
| op1(e15,e11) = e10 )
& ( op1(e15,e10) = e15
| op1(e15,e10) = e14
| op1(e15,e10) = e13
| op1(e15,e10) = e12
| op1(e15,e10) = e11
| op1(e15,e10) = e10 )
& ( op1(e14,e15) = e15
| op1(e14,e15) = e14
| op1(e14,e15) = e13
| op1(e14,e15) = e12
| op1(e14,e15) = e11
| op1(e14,e15) = e10 )
& ( op1(e14,e14) = e15
| op1(e14,e14) = e14
| op1(e14,e14) = e13
| op1(e14,e14) = e12
| op1(e14,e14) = e11
| op1(e14,e14) = e10 )
& ( op1(e14,e13) = e15
| op1(e14,e13) = e14
| op1(e14,e13) = e13
| op1(e14,e13) = e12
| op1(e14,e13) = e11
| op1(e14,e13) = e10 )
& ( op1(e14,e12) = e15
| op1(e14,e12) = e14
| op1(e14,e12) = e13
| op1(e14,e12) = e12
| op1(e14,e12) = e11
| op1(e14,e12) = e10 )
& ( op1(e14,e11) = e15
| op1(e14,e11) = e14
| op1(e14,e11) = e13
| op1(e14,e11) = e12
| op1(e14,e11) = e11
| op1(e14,e11) = e10 )
& ( op1(e14,e10) = e15
| op1(e14,e10) = e14
| op1(e14,e10) = e13
| op1(e14,e10) = e12
| op1(e14,e10) = e11
| op1(e14,e10) = e10 )
& ( op1(e13,e15) = e15
| op1(e13,e15) = e14
| op1(e13,e15) = e13
| op1(e13,e15) = e12
| op1(e13,e15) = e11
| op1(e13,e15) = e10 )
& ( op1(e13,e14) = e15
| op1(e13,e14) = e14
| op1(e13,e14) = e13
| op1(e13,e14) = e12
| op1(e13,e14) = e11
| op1(e13,e14) = e10 )
& ( op1(e13,e13) = e15
| op1(e13,e13) = e14
| op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e15
| op1(e13,e12) = e14
| op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e15
| op1(e13,e11) = e14
| op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e15
| op1(e13,e10) = e14
| op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e15) = e15
| op1(e12,e15) = e14
| op1(e12,e15) = e13
| op1(e12,e15) = e12
| op1(e12,e15) = e11
| op1(e12,e15) = e10 )
& ( op1(e12,e14) = e15
| op1(e12,e14) = e14
| op1(e12,e14) = e13
| op1(e12,e14) = e12
| op1(e12,e14) = e11
| op1(e12,e14) = e10 )
& ( op1(e12,e13) = e15
| op1(e12,e13) = e14
| op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e15
| op1(e12,e12) = e14
| op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e15
| op1(e12,e11) = e14
| op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e15
| op1(e12,e10) = e14
| op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e15) = e15
| op1(e11,e15) = e14
| op1(e11,e15) = e13
| op1(e11,e15) = e12
| op1(e11,e15) = e11
| op1(e11,e15) = e10 )
& ( op1(e11,e14) = e15
| op1(e11,e14) = e14
| op1(e11,e14) = e13
| op1(e11,e14) = e12
| op1(e11,e14) = e11
| op1(e11,e14) = e10 )
& ( op1(e11,e13) = e15
| op1(e11,e13) = e14
| op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e15
| op1(e11,e12) = e14
| op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e15
| op1(e11,e11) = e14
| op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e15
| op1(e11,e10) = e14
| op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e15) = e15
| op1(e10,e15) = e14
| op1(e10,e15) = e13
| op1(e10,e15) = e12
| op1(e10,e15) = e11
| op1(e10,e15) = e10 )
& ( op1(e10,e14) = e15
| op1(e10,e14) = e14
| op1(e10,e14) = e13
| op1(e10,e14) = e12
| op1(e10,e14) = e11
| op1(e10,e14) = e10 )
& ( op1(e10,e13) = e15
| op1(e10,e13) = e14
| op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e15
| op1(e10,e12) = e14
| op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e15
| op1(e10,e11) = e14
| op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e15
| 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(op1(e15,e15),e15) = op1(e15,op1(e15,e15))
& op1(op1(e15,e15),e14) = op1(e15,op1(e15,e14))
& op1(op1(e15,e15),e13) = op1(e15,op1(e15,e13))
& op1(op1(e15,e15),e12) = op1(e15,op1(e15,e12))
& op1(op1(e15,e15),e11) = op1(e15,op1(e15,e11))
& op1(op1(e15,e15),e10) = op1(e15,op1(e15,e10))
& op1(op1(e15,e14),e15) = op1(e15,op1(e14,e15))
& op1(op1(e15,e14),e14) = op1(e15,op1(e14,e14))
& op1(op1(e15,e14),e13) = op1(e15,op1(e14,e13))
& op1(op1(e15,e14),e12) = op1(e15,op1(e14,e12))
& op1(op1(e15,e14),e11) = op1(e15,op1(e14,e11))
& op1(op1(e15,e14),e10) = op1(e15,op1(e14,e10))
& op1(op1(e15,e13),e15) = op1(e15,op1(e13,e15))
& op1(op1(e15,e13),e14) = op1(e15,op1(e13,e14))
& op1(op1(e15,e13),e13) = op1(e15,op1(e13,e13))
& op1(op1(e15,e13),e12) = op1(e15,op1(e13,e12))
& op1(op1(e15,e13),e11) = op1(e15,op1(e13,e11))
& op1(op1(e15,e13),e10) = op1(e15,op1(e13,e10))
& op1(op1(e15,e12),e15) = op1(e15,op1(e12,e15))
& op1(op1(e15,e12),e14) = op1(e15,op1(e12,e14))
& op1(op1(e15,e12),e13) = op1(e15,op1(e12,e13))
& op1(op1(e15,e12),e12) = op1(e15,op1(e12,e12))
& op1(op1(e15,e12),e11) = op1(e15,op1(e12,e11))
& op1(op1(e15,e12),e10) = op1(e15,op1(e12,e10))
& op1(op1(e15,e11),e15) = op1(e15,op1(e11,e15))
& op1(op1(e15,e11),e14) = op1(e15,op1(e11,e14))
& op1(op1(e15,e11),e13) = op1(e15,op1(e11,e13))
& op1(op1(e15,e11),e12) = op1(e15,op1(e11,e12))
& op1(op1(e15,e11),e11) = op1(e15,op1(e11,e11))
& op1(op1(e15,e11),e10) = op1(e15,op1(e11,e10))
& op1(op1(e15,e10),e15) = op1(e15,op1(e10,e15))
& op1(op1(e15,e10),e14) = op1(e15,op1(e10,e14))
& op1(op1(e15,e10),e13) = op1(e15,op1(e10,e13))
& op1(op1(e15,e10),e12) = op1(e15,op1(e10,e12))
& op1(op1(e15,e10),e11) = op1(e15,op1(e10,e11))
& op1(op1(e15,e10),e10) = op1(e15,op1(e10,e10))
& op1(op1(e14,e15),e15) = op1(e14,op1(e15,e15))
& op1(op1(e14,e15),e14) = op1(e14,op1(e15,e14))
& op1(op1(e14,e15),e13) = op1(e14,op1(e15,e13))
& op1(op1(e14,e15),e12) = op1(e14,op1(e15,e12))
& op1(op1(e14,e15),e11) = op1(e14,op1(e15,e11))
& op1(op1(e14,e15),e10) = op1(e14,op1(e15,e10))
& op1(op1(e14,e14),e15) = op1(e14,op1(e14,e15))
& op1(op1(e14,e14),e14) = op1(e14,op1(e14,e14))
& op1(op1(e14,e14),e13) = op1(e14,op1(e14,e13))
& op1(op1(e14,e14),e12) = op1(e14,op1(e14,e12))
& op1(op1(e14,e14),e11) = op1(e14,op1(e14,e11))
& op1(op1(e14,e14),e10) = op1(e14,op1(e14,e10))
& op1(op1(e14,e13),e15) = op1(e14,op1(e13,e15))
& op1(op1(e14,e13),e14) = op1(e14,op1(e13,e14))
& op1(op1(e14,e13),e13) = op1(e14,op1(e13,e13))
& op1(op1(e14,e13),e12) = op1(e14,op1(e13,e12))
& op1(op1(e14,e13),e11) = op1(e14,op1(e13,e11))
& op1(op1(e14,e13),e10) = op1(e14,op1(e13,e10))
& op1(op1(e14,e12),e15) = op1(e14,op1(e12,e15))
& op1(op1(e14,e12),e14) = op1(e14,op1(e12,e14))
& op1(op1(e14,e12),e13) = op1(e14,op1(e12,e13))
& op1(op1(e14,e12),e12) = op1(e14,op1(e12,e12))
& op1(op1(e14,e12),e11) = op1(e14,op1(e12,e11))
& op1(op1(e14,e12),e10) = op1(e14,op1(e12,e10))
& op1(op1(e14,e11),e15) = op1(e14,op1(e11,e15))
& op1(op1(e14,e11),e14) = op1(e14,op1(e11,e14))
& op1(op1(e14,e11),e13) = op1(e14,op1(e11,e13))
& op1(op1(e14,e11),e12) = op1(e14,op1(e11,e12))
& op1(op1(e14,e11),e11) = op1(e14,op1(e11,e11))
& op1(op1(e14,e11),e10) = op1(e14,op1(e11,e10))
& op1(op1(e14,e10),e15) = op1(e14,op1(e10,e15))
& op1(op1(e14,e10),e14) = op1(e14,op1(e10,e14))
& op1(op1(e14,e10),e13) = op1(e14,op1(e10,e13))
& op1(op1(e14,e10),e12) = op1(e14,op1(e10,e12))
& op1(op1(e14,e10),e11) = op1(e14,op1(e10,e11))
& op1(op1(e14,e10),e10) = op1(e14,op1(e10,e10))
& op1(op1(e13,e15),e15) = op1(e13,op1(e15,e15))
& op1(op1(e13,e15),e14) = op1(e13,op1(e15,e14))
& op1(op1(e13,e15),e13) = op1(e13,op1(e15,e13))
& op1(op1(e13,e15),e12) = op1(e13,op1(e15,e12))
& op1(op1(e13,e15),e11) = op1(e13,op1(e15,e11))
& op1(op1(e13,e15),e10) = op1(e13,op1(e15,e10))
& op1(op1(e13,e14),e15) = op1(e13,op1(e14,e15))
& op1(op1(e13,e14),e14) = op1(e13,op1(e14,e14))
& op1(op1(e13,e14),e13) = op1(e13,op1(e14,e13))
& op1(op1(e13,e14),e12) = op1(e13,op1(e14,e12))
& op1(op1(e13,e14),e11) = op1(e13,op1(e14,e11))
& op1(op1(e13,e14),e10) = op1(e13,op1(e14,e10))
& op1(op1(e13,e13),e15) = op1(e13,op1(e13,e15))
& op1(op1(e13,e13),e14) = op1(e13,op1(e13,e14))
& op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13))
& op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12))
& op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11))
& op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10))
& op1(op1(e13,e12),e15) = op1(e13,op1(e12,e15))
& op1(op1(e13,e12),e14) = op1(e13,op1(e12,e14))
& op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13))
& op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12))
& op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11))
& op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10))
& op1(op1(e13,e11),e15) = op1(e13,op1(e11,e15))
& op1(op1(e13,e11),e14) = op1(e13,op1(e11,e14))
& op1(op1(e13,e11),e13) = op1(e13,op1(e11,e13))
& op1(op1(e13,e11),e12) = op1(e13,op1(e11,e12))
& op1(op1(e13,e11),e11) = op1(e13,op1(e11,e11))
& op1(op1(e13,e11),e10) = op1(e13,op1(e11,e10))
& op1(op1(e13,e10),e15) = op1(e13,op1(e10,e15))
& op1(op1(e13,e10),e14) = op1(e13,op1(e10,e14))
& op1(op1(e13,e10),e13) = op1(e13,op1(e10,e13))
& op1(op1(e13,e10),e12) = op1(e13,op1(e10,e12))
& op1(op1(e13,e10),e11) = op1(e13,op1(e10,e11))
& op1(op1(e13,e10),e10) = op1(e13,op1(e10,e10))
& op1(op1(e12,e15),e15) = op1(e12,op1(e15,e15))
& op1(op1(e12,e15),e14) = op1(e12,op1(e15,e14))
& op1(op1(e12,e15),e13) = op1(e12,op1(e15,e13))
& op1(op1(e12,e15),e12) = op1(e12,op1(e15,e12))
& op1(op1(e12,e15),e11) = op1(e12,op1(e15,e11))
& op1(op1(e12,e15),e10) = op1(e12,op1(e15,e10))
& op1(op1(e12,e14),e15) = op1(e12,op1(e14,e15))
& op1(op1(e12,e14),e14) = op1(e12,op1(e14,e14))
& op1(op1(e12,e14),e13) = op1(e12,op1(e14,e13))
& op1(op1(e12,e14),e12) = op1(e12,op1(e14,e12))
& op1(op1(e12,e14),e11) = op1(e12,op1(e14,e11))
& op1(op1(e12,e14),e10) = op1(e12,op1(e14,e10))
& op1(op1(e12,e13),e15) = op1(e12,op1(e13,e15))
& op1(op1(e12,e13),e14) = op1(e12,op1(e13,e14))
& op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13))
& op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12))
& op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11))
& op1(op1(e12,e13),e10) = op1(e12,op1(e13,e10))
& op1(op1(e12,e12),e15) = op1(e12,op1(e12,e15))
& op1(op1(e12,e12),e14) = op1(e12,op1(e12,e14))
& op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13))
& op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12))
& op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11))
& op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10))
& op1(op1(e12,e11),e15) = op1(e12,op1(e11,e15))
& op1(op1(e12,e11),e14) = op1(e12,op1(e11,e14))
& op1(op1(e12,e11),e13) = op1(e12,op1(e11,e13))
& op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12))
& op1(op1(e12,e11),e11) = op1(e12,op1(e11,e11))
& op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10))
& op1(op1(e12,e10),e15) = op1(e12,op1(e10,e15))
& op1(op1(e12,e10),e14) = op1(e12,op1(e10,e14))
& op1(op1(e12,e10),e13) = op1(e12,op1(e10,e13))
& op1(op1(e12,e10),e12) = op1(e12,op1(e10,e12))
& op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11))
& op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10))
& op1(op1(e11,e15),e15) = op1(e11,op1(e15,e15))
& op1(op1(e11,e15),e14) = op1(e11,op1(e15,e14))
& op1(op1(e11,e15),e13) = op1(e11,op1(e15,e13))
& op1(op1(e11,e15),e12) = op1(e11,op1(e15,e12))
& op1(op1(e11,e15),e11) = op1(e11,op1(e15,e11))
& op1(op1(e11,e15),e10) = op1(e11,op1(e15,e10))
& op1(op1(e11,e14),e15) = op1(e11,op1(e14,e15))
& op1(op1(e11,e14),e14) = op1(e11,op1(e14,e14))
& op1(op1(e11,e14),e13) = op1(e11,op1(e14,e13))
& op1(op1(e11,e14),e12) = op1(e11,op1(e14,e12))
& op1(op1(e11,e14),e11) = op1(e11,op1(e14,e11))
& op1(op1(e11,e14),e10) = op1(e11,op1(e14,e10))
& op1(op1(e11,e13),e15) = op1(e11,op1(e13,e15))
& op1(op1(e11,e13),e14) = op1(e11,op1(e13,e14))
& op1(op1(e11,e13),e13) = op1(e11,op1(e13,e13))
& op1(op1(e11,e13),e12) = op1(e11,op1(e13,e12))
& op1(op1(e11,e13),e11) = op1(e11,op1(e13,e11))
& op1(op1(e11,e13),e10) = op1(e11,op1(e13,e10))
& op1(op1(e11,e12),e15) = op1(e11,op1(e12,e15))
& op1(op1(e11,e12),e14) = op1(e11,op1(e12,e14))
& op1(op1(e11,e12),e13) = op1(e11,op1(e12,e13))
& op1(op1(e11,e12),e12) = op1(e11,op1(e12,e12))
& op1(op1(e11,e12),e11) = op1(e11,op1(e12,e11))
& op1(op1(e11,e12),e10) = op1(e11,op1(e12,e10))
& op1(op1(e11,e11),e15) = op1(e11,op1(e11,e15))
& op1(op1(e11,e11),e14) = op1(e11,op1(e11,e14))
& op1(op1(e11,e11),e13) = op1(e11,op1(e11,e13))
& op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12))
& op1(op1(e11,e11),e11) = op1(e11,op1(e11,e11))
& op1(op1(e11,e11),e10) = op1(e11,op1(e11,e10))
& op1(op1(e11,e10),e15) = op1(e11,op1(e10,e15))
& op1(op1(e11,e10),e14) = op1(e11,op1(e10,e14))
& op1(op1(e11,e10),e13) = op1(e11,op1(e10,e13))
& op1(op1(e11,e10),e12) = op1(e11,op1(e10,e12))
& op1(op1(e11,e10),e11) = op1(e11,op1(e10,e11))
& op1(op1(e11,e10),e10) = op1(e11,op1(e10,e10))
& op1(op1(e10,e15),e15) = op1(e10,op1(e15,e15))
& op1(op1(e10,e15),e14) = op1(e10,op1(e15,e14))
& op1(op1(e10,e15),e13) = op1(e10,op1(e15,e13))
& op1(op1(e10,e15),e12) = op1(e10,op1(e15,e12))
& op1(op1(e10,e15),e11) = op1(e10,op1(e15,e11))
& op1(op1(e10,e15),e10) = op1(e10,op1(e15,e10))
& op1(op1(e10,e14),e15) = op1(e10,op1(e14,e15))
& op1(op1(e10,e14),e14) = op1(e10,op1(e14,e14))
& op1(op1(e10,e14),e13) = op1(e10,op1(e14,e13))
& op1(op1(e10,e14),e12) = op1(e10,op1(e14,e12))
& op1(op1(e10,e14),e11) = op1(e10,op1(e14,e11))
& op1(op1(e10,e14),e10) = op1(e10,op1(e14,e10))
& op1(op1(e10,e13),e15) = op1(e10,op1(e13,e15))
& op1(op1(e10,e13),e14) = op1(e10,op1(e13,e14))
& op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13))
& op1(op1(e10,e13),e12) = op1(e10,op1(e13,e12))
& op1(op1(e10,e13),e11) = op1(e10,op1(e13,e11))
& op1(op1(e10,e13),e10) = op1(e10,op1(e13,e10))
& op1(op1(e10,e12),e15) = op1(e10,op1(e12,e15))
& op1(op1(e10,e12),e14) = op1(e10,op1(e12,e14))
& op1(op1(e10,e12),e13) = op1(e10,op1(e12,e13))
& op1(op1(e10,e12),e12) = op1(e10,op1(e12,e12))
& op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11))
& op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10))
& op1(op1(e10,e11),e15) = op1(e10,op1(e11,e15))
& op1(op1(e10,e11),e14) = op1(e10,op1(e11,e14))
& op1(op1(e10,e11),e13) = op1(e10,op1(e11,e13))
& op1(op1(e10,e11),e12) = op1(e10,op1(e11,e12))
& op1(op1(e10,e11),e11) = op1(e10,op1(e11,e11))
& op1(op1(e10,e11),e10) = op1(e10,op1(e11,e10))
& op1(op1(e10,e10),e15) = op1(e10,op1(e10,e15))
& op1(op1(e10,e10),e14) = op1(e10,op1(e10,e14))
& op1(op1(e10,e10),e13) = op1(e10,op1(e10,e13))
& op1(op1(e10,e10),e12) = op1(e10,op1(e10,e12))
& op1(op1(e10,e10),e11) = op1(e10,op1(e10,e11))
& op1(op1(e10,e10),e10) = op1(e10,op1(e10,e10)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f5,axiom,
( ( op2(e25,e25) = e25
| op2(e25,e25) = e24
| op2(e25,e25) = e23
| op2(e25,e25) = e22
| op2(e25,e25) = e21
| op2(e25,e25) = e20 )
& ( op2(e25,e24) = e25
| op2(e25,e24) = e24
| op2(e25,e24) = e23
| op2(e25,e24) = e22
| op2(e25,e24) = e21
| op2(e25,e24) = e20 )
& ( op2(e25,e23) = e25
| op2(e25,e23) = e24
| op2(e25,e23) = e23
| op2(e25,e23) = e22
| op2(e25,e23) = e21
| op2(e25,e23) = e20 )
& ( op2(e25,e22) = e25
| op2(e25,e22) = e24
| op2(e25,e22) = e23
| op2(e25,e22) = e22
| op2(e25,e22) = e21
| op2(e25,e22) = e20 )
& ( op2(e25,e21) = e25
| op2(e25,e21) = e24
| op2(e25,e21) = e23
| op2(e25,e21) = e22
| op2(e25,e21) = e21
| op2(e25,e21) = e20 )
& ( op2(e25,e20) = e25
| op2(e25,e20) = e24
| op2(e25,e20) = e23
| op2(e25,e20) = e22
| op2(e25,e20) = e21
| op2(e25,e20) = e20 )
& ( op2(e24,e25) = e25
| op2(e24,e25) = e24
| op2(e24,e25) = e23
| op2(e24,e25) = e22
| op2(e24,e25) = e21
| op2(e24,e25) = e20 )
& ( op2(e24,e24) = e25
| op2(e24,e24) = e24
| op2(e24,e24) = e23
| op2(e24,e24) = e22
| op2(e24,e24) = e21
| op2(e24,e24) = e20 )
& ( op2(e24,e23) = e25
| op2(e24,e23) = e24
| op2(e24,e23) = e23
| op2(e24,e23) = e22
| op2(e24,e23) = e21
| op2(e24,e23) = e20 )
& ( op2(e24,e22) = e25
| op2(e24,e22) = e24
| op2(e24,e22) = e23
| op2(e24,e22) = e22
| op2(e24,e22) = e21
| op2(e24,e22) = e20 )
& ( op2(e24,e21) = e25
| op2(e24,e21) = e24
| op2(e24,e21) = e23
| op2(e24,e21) = e22
| op2(e24,e21) = e21
| op2(e24,e21) = e20 )
& ( op2(e24,e20) = e25
| op2(e24,e20) = e24
| op2(e24,e20) = e23
| op2(e24,e20) = e22
| op2(e24,e20) = e21
| op2(e24,e20) = e20 )
& ( op2(e23,e25) = e25
| op2(e23,e25) = e24
| op2(e23,e25) = e23
| op2(e23,e25) = e22
| op2(e23,e25) = e21
| op2(e23,e25) = e20 )
& ( op2(e23,e24) = e25
| op2(e23,e24) = e24
| op2(e23,e24) = e23
| op2(e23,e24) = e22
| op2(e23,e24) = e21
| op2(e23,e24) = e20 )
& ( op2(e23,e23) = e25
| op2(e23,e23) = e24
| op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e25
| op2(e23,e22) = e24
| op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e25
| op2(e23,e21) = e24
| op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e25
| op2(e23,e20) = e24
| op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e25) = e25
| op2(e22,e25) = e24
| op2(e22,e25) = e23
| op2(e22,e25) = e22
| op2(e22,e25) = e21
| op2(e22,e25) = e20 )
& ( op2(e22,e24) = e25
| op2(e22,e24) = e24
| op2(e22,e24) = e23
| op2(e22,e24) = e22
| op2(e22,e24) = e21
| op2(e22,e24) = e20 )
& ( op2(e22,e23) = e25
| op2(e22,e23) = e24
| op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e25
| op2(e22,e22) = e24
| op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e25
| op2(e22,e21) = e24
| op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e25
| op2(e22,e20) = e24
| op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e25) = e25
| op2(e21,e25) = e24
| op2(e21,e25) = e23
| op2(e21,e25) = e22
| op2(e21,e25) = e21
| op2(e21,e25) = e20 )
& ( op2(e21,e24) = e25
| op2(e21,e24) = e24
| op2(e21,e24) = e23
| op2(e21,e24) = e22
| op2(e21,e24) = e21
| op2(e21,e24) = e20 )
& ( op2(e21,e23) = e25
| op2(e21,e23) = e24
| op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e25
| op2(e21,e22) = e24
| op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e25
| op2(e21,e21) = e24
| op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e25
| op2(e21,e20) = e24
| op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e25) = e25
| op2(e20,e25) = e24
| op2(e20,e25) = e23
| op2(e20,e25) = e22
| op2(e20,e25) = e21
| op2(e20,e25) = e20 )
& ( op2(e20,e24) = e25
| op2(e20,e24) = e24
| op2(e20,e24) = e23
| op2(e20,e24) = e22
| op2(e20,e24) = e21
| op2(e20,e24) = e20 )
& ( op2(e20,e23) = e25
| op2(e20,e23) = e24
| op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e25
| op2(e20,e22) = e24
| op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e25
| op2(e20,e21) = e24
| op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e25
| 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',ax5) ).
fof(f6,axiom,
( op2(op2(e25,e25),e25) = op2(e25,op2(e25,e25))
& op2(op2(e25,e25),e24) = op2(e25,op2(e25,e24))
& op2(op2(e25,e25),e23) = op2(e25,op2(e25,e23))
& op2(op2(e25,e25),e22) = op2(e25,op2(e25,e22))
& op2(op2(e25,e25),e21) = op2(e25,op2(e25,e21))
& op2(op2(e25,e25),e20) = op2(e25,op2(e25,e20))
& op2(op2(e25,e24),e25) = op2(e25,op2(e24,e25))
& op2(op2(e25,e24),e24) = op2(e25,op2(e24,e24))
& op2(op2(e25,e24),e23) = op2(e25,op2(e24,e23))
& op2(op2(e25,e24),e22) = op2(e25,op2(e24,e22))
& op2(op2(e25,e24),e21) = op2(e25,op2(e24,e21))
& op2(op2(e25,e24),e20) = op2(e25,op2(e24,e20))
& op2(op2(e25,e23),e25) = op2(e25,op2(e23,e25))
& op2(op2(e25,e23),e24) = op2(e25,op2(e23,e24))
& op2(op2(e25,e23),e23) = op2(e25,op2(e23,e23))
& op2(op2(e25,e23),e22) = op2(e25,op2(e23,e22))
& op2(op2(e25,e23),e21) = op2(e25,op2(e23,e21))
& op2(op2(e25,e23),e20) = op2(e25,op2(e23,e20))
& op2(op2(e25,e22),e25) = op2(e25,op2(e22,e25))
& op2(op2(e25,e22),e24) = op2(e25,op2(e22,e24))
& op2(op2(e25,e22),e23) = op2(e25,op2(e22,e23))
& op2(op2(e25,e22),e22) = op2(e25,op2(e22,e22))
& op2(op2(e25,e22),e21) = op2(e25,op2(e22,e21))
& op2(op2(e25,e22),e20) = op2(e25,op2(e22,e20))
& op2(op2(e25,e21),e25) = op2(e25,op2(e21,e25))
& op2(op2(e25,e21),e24) = op2(e25,op2(e21,e24))
& op2(op2(e25,e21),e23) = op2(e25,op2(e21,e23))
& op2(op2(e25,e21),e22) = op2(e25,op2(e21,e22))
& op2(op2(e25,e21),e21) = op2(e25,op2(e21,e21))
& op2(op2(e25,e21),e20) = op2(e25,op2(e21,e20))
& op2(op2(e25,e20),e25) = op2(e25,op2(e20,e25))
& op2(op2(e25,e20),e24) = op2(e25,op2(e20,e24))
& op2(op2(e25,e20),e23) = op2(e25,op2(e20,e23))
& op2(op2(e25,e20),e22) = op2(e25,op2(e20,e22))
& op2(op2(e25,e20),e21) = op2(e25,op2(e20,e21))
& op2(op2(e25,e20),e20) = op2(e25,op2(e20,e20))
& op2(op2(e24,e25),e25) = op2(e24,op2(e25,e25))
& op2(op2(e24,e25),e24) = op2(e24,op2(e25,e24))
& op2(op2(e24,e25),e23) = op2(e24,op2(e25,e23))
& op2(op2(e24,e25),e22) = op2(e24,op2(e25,e22))
& op2(op2(e24,e25),e21) = op2(e24,op2(e25,e21))
& op2(op2(e24,e25),e20) = op2(e24,op2(e25,e20))
& op2(op2(e24,e24),e25) = op2(e24,op2(e24,e25))
& op2(op2(e24,e24),e24) = op2(e24,op2(e24,e24))
& op2(op2(e24,e24),e23) = op2(e24,op2(e24,e23))
& op2(op2(e24,e24),e22) = op2(e24,op2(e24,e22))
& op2(op2(e24,e24),e21) = op2(e24,op2(e24,e21))
& op2(op2(e24,e24),e20) = op2(e24,op2(e24,e20))
& op2(op2(e24,e23),e25) = op2(e24,op2(e23,e25))
& op2(op2(e24,e23),e24) = op2(e24,op2(e23,e24))
& op2(op2(e24,e23),e23) = op2(e24,op2(e23,e23))
& op2(op2(e24,e23),e22) = op2(e24,op2(e23,e22))
& op2(op2(e24,e23),e21) = op2(e24,op2(e23,e21))
& op2(op2(e24,e23),e20) = op2(e24,op2(e23,e20))
& op2(op2(e24,e22),e25) = op2(e24,op2(e22,e25))
& op2(op2(e24,e22),e24) = op2(e24,op2(e22,e24))
& op2(op2(e24,e22),e23) = op2(e24,op2(e22,e23))
& op2(op2(e24,e22),e22) = op2(e24,op2(e22,e22))
& op2(op2(e24,e22),e21) = op2(e24,op2(e22,e21))
& op2(op2(e24,e22),e20) = op2(e24,op2(e22,e20))
& op2(op2(e24,e21),e25) = op2(e24,op2(e21,e25))
& op2(op2(e24,e21),e24) = op2(e24,op2(e21,e24))
& op2(op2(e24,e21),e23) = op2(e24,op2(e21,e23))
& op2(op2(e24,e21),e22) = op2(e24,op2(e21,e22))
& op2(op2(e24,e21),e21) = op2(e24,op2(e21,e21))
& op2(op2(e24,e21),e20) = op2(e24,op2(e21,e20))
& op2(op2(e24,e20),e25) = op2(e24,op2(e20,e25))
& op2(op2(e24,e20),e24) = op2(e24,op2(e20,e24))
& op2(op2(e24,e20),e23) = op2(e24,op2(e20,e23))
& op2(op2(e24,e20),e22) = op2(e24,op2(e20,e22))
& op2(op2(e24,e20),e21) = op2(e24,op2(e20,e21))
& op2(op2(e24,e20),e20) = op2(e24,op2(e20,e20))
& op2(op2(e23,e25),e25) = op2(e23,op2(e25,e25))
& op2(op2(e23,e25),e24) = op2(e23,op2(e25,e24))
& op2(op2(e23,e25),e23) = op2(e23,op2(e25,e23))
& op2(op2(e23,e25),e22) = op2(e23,op2(e25,e22))
& op2(op2(e23,e25),e21) = op2(e23,op2(e25,e21))
& op2(op2(e23,e25),e20) = op2(e23,op2(e25,e20))
& op2(op2(e23,e24),e25) = op2(e23,op2(e24,e25))
& op2(op2(e23,e24),e24) = op2(e23,op2(e24,e24))
& op2(op2(e23,e24),e23) = op2(e23,op2(e24,e23))
& op2(op2(e23,e24),e22) = op2(e23,op2(e24,e22))
& op2(op2(e23,e24),e21) = op2(e23,op2(e24,e21))
& op2(op2(e23,e24),e20) = op2(e23,op2(e24,e20))
& op2(op2(e23,e23),e25) = op2(e23,op2(e23,e25))
& op2(op2(e23,e23),e24) = op2(e23,op2(e23,e24))
& op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23))
& op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22))
& op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21))
& op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20))
& op2(op2(e23,e22),e25) = op2(e23,op2(e22,e25))
& op2(op2(e23,e22),e24) = op2(e23,op2(e22,e24))
& op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23))
& op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22))
& op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21))
& op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20))
& op2(op2(e23,e21),e25) = op2(e23,op2(e21,e25))
& op2(op2(e23,e21),e24) = op2(e23,op2(e21,e24))
& op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23))
& op2(op2(e23,e21),e22) = op2(e23,op2(e21,e22))
& op2(op2(e23,e21),e21) = op2(e23,op2(e21,e21))
& op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20))
& op2(op2(e23,e20),e25) = op2(e23,op2(e20,e25))
& op2(op2(e23,e20),e24) = op2(e23,op2(e20,e24))
& op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23))
& op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22))
& op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21))
& op2(op2(e23,e20),e20) = op2(e23,op2(e20,e20))
& op2(op2(e22,e25),e25) = op2(e22,op2(e25,e25))
& op2(op2(e22,e25),e24) = op2(e22,op2(e25,e24))
& op2(op2(e22,e25),e23) = op2(e22,op2(e25,e23))
& op2(op2(e22,e25),e22) = op2(e22,op2(e25,e22))
& op2(op2(e22,e25),e21) = op2(e22,op2(e25,e21))
& op2(op2(e22,e25),e20) = op2(e22,op2(e25,e20))
& op2(op2(e22,e24),e25) = op2(e22,op2(e24,e25))
& op2(op2(e22,e24),e24) = op2(e22,op2(e24,e24))
& op2(op2(e22,e24),e23) = op2(e22,op2(e24,e23))
& op2(op2(e22,e24),e22) = op2(e22,op2(e24,e22))
& op2(op2(e22,e24),e21) = op2(e22,op2(e24,e21))
& op2(op2(e22,e24),e20) = op2(e22,op2(e24,e20))
& op2(op2(e22,e23),e25) = op2(e22,op2(e23,e25))
& op2(op2(e22,e23),e24) = op2(e22,op2(e23,e24))
& op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23))
& op2(op2(e22,e23),e22) = op2(e22,op2(e23,e22))
& op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21))
& op2(op2(e22,e23),e20) = op2(e22,op2(e23,e20))
& op2(op2(e22,e22),e25) = op2(e22,op2(e22,e25))
& op2(op2(e22,e22),e24) = op2(e22,op2(e22,e24))
& op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23))
& op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22))
& op2(op2(e22,e22),e21) = op2(e22,op2(e22,e21))
& op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20))
& op2(op2(e22,e21),e25) = op2(e22,op2(e21,e25))
& op2(op2(e22,e21),e24) = op2(e22,op2(e21,e24))
& op2(op2(e22,e21),e23) = op2(e22,op2(e21,e23))
& op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22))
& op2(op2(e22,e21),e21) = op2(e22,op2(e21,e21))
& op2(op2(e22,e21),e20) = op2(e22,op2(e21,e20))
& op2(op2(e22,e20),e25) = op2(e22,op2(e20,e25))
& op2(op2(e22,e20),e24) = op2(e22,op2(e20,e24))
& op2(op2(e22,e20),e23) = op2(e22,op2(e20,e23))
& op2(op2(e22,e20),e22) = op2(e22,op2(e20,e22))
& op2(op2(e22,e20),e21) = op2(e22,op2(e20,e21))
& op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20))
& op2(op2(e21,e25),e25) = op2(e21,op2(e25,e25))
& op2(op2(e21,e25),e24) = op2(e21,op2(e25,e24))
& op2(op2(e21,e25),e23) = op2(e21,op2(e25,e23))
& op2(op2(e21,e25),e22) = op2(e21,op2(e25,e22))
& op2(op2(e21,e25),e21) = op2(e21,op2(e25,e21))
& op2(op2(e21,e25),e20) = op2(e21,op2(e25,e20))
& op2(op2(e21,e24),e25) = op2(e21,op2(e24,e25))
& op2(op2(e21,e24),e24) = op2(e21,op2(e24,e24))
& op2(op2(e21,e24),e23) = op2(e21,op2(e24,e23))
& op2(op2(e21,e24),e22) = op2(e21,op2(e24,e22))
& op2(op2(e21,e24),e21) = op2(e21,op2(e24,e21))
& op2(op2(e21,e24),e20) = op2(e21,op2(e24,e20))
& op2(op2(e21,e23),e25) = op2(e21,op2(e23,e25))
& op2(op2(e21,e23),e24) = op2(e21,op2(e23,e24))
& op2(op2(e21,e23),e23) = op2(e21,op2(e23,e23))
& op2(op2(e21,e23),e22) = op2(e21,op2(e23,e22))
& op2(op2(e21,e23),e21) = op2(e21,op2(e23,e21))
& op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20))
& op2(op2(e21,e22),e25) = op2(e21,op2(e22,e25))
& op2(op2(e21,e22),e24) = op2(e21,op2(e22,e24))
& op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23))
& op2(op2(e21,e22),e22) = op2(e21,op2(e22,e22))
& op2(op2(e21,e22),e21) = op2(e21,op2(e22,e21))
& op2(op2(e21,e22),e20) = op2(e21,op2(e22,e20))
& op2(op2(e21,e21),e25) = op2(e21,op2(e21,e25))
& op2(op2(e21,e21),e24) = op2(e21,op2(e21,e24))
& op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23))
& op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22))
& op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21))
& op2(op2(e21,e21),e20) = op2(e21,op2(e21,e20))
& op2(op2(e21,e20),e25) = op2(e21,op2(e20,e25))
& op2(op2(e21,e20),e24) = op2(e21,op2(e20,e24))
& op2(op2(e21,e20),e23) = op2(e21,op2(e20,e23))
& op2(op2(e21,e20),e22) = op2(e21,op2(e20,e22))
& op2(op2(e21,e20),e21) = op2(e21,op2(e20,e21))
& op2(op2(e21,e20),e20) = op2(e21,op2(e20,e20))
& op2(op2(e20,e25),e25) = op2(e20,op2(e25,e25))
& op2(op2(e20,e25),e24) = op2(e20,op2(e25,e24))
& op2(op2(e20,e25),e23) = op2(e20,op2(e25,e23))
& op2(op2(e20,e25),e22) = op2(e20,op2(e25,e22))
& op2(op2(e20,e25),e21) = op2(e20,op2(e25,e21))
& op2(op2(e20,e25),e20) = op2(e20,op2(e25,e20))
& op2(op2(e20,e24),e25) = op2(e20,op2(e24,e25))
& op2(op2(e20,e24),e24) = op2(e20,op2(e24,e24))
& op2(op2(e20,e24),e23) = op2(e20,op2(e24,e23))
& op2(op2(e20,e24),e22) = op2(e20,op2(e24,e22))
& op2(op2(e20,e24),e21) = op2(e20,op2(e24,e21))
& op2(op2(e20,e24),e20) = op2(e20,op2(e24,e20))
& op2(op2(e20,e23),e25) = op2(e20,op2(e23,e25))
& op2(op2(e20,e23),e24) = op2(e20,op2(e23,e24))
& op2(op2(e20,e23),e23) = op2(e20,op2(e23,e23))
& op2(op2(e20,e23),e22) = op2(e20,op2(e23,e22))
& op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21))
& op2(op2(e20,e23),e20) = op2(e20,op2(e23,e20))
& op2(op2(e20,e22),e25) = op2(e20,op2(e22,e25))
& op2(op2(e20,e22),e24) = op2(e20,op2(e22,e24))
& op2(op2(e20,e22),e23) = op2(e20,op2(e22,e23))
& op2(op2(e20,e22),e22) = op2(e20,op2(e22,e22))
& op2(op2(e20,e22),e21) = op2(e20,op2(e22,e21))
& op2(op2(e20,e22),e20) = op2(e20,op2(e22,e20))
& op2(op2(e20,e21),e25) = op2(e20,op2(e21,e25))
& op2(op2(e20,e21),e24) = op2(e20,op2(e21,e24))
& op2(op2(e20,e21),e23) = op2(e20,op2(e21,e23))
& op2(op2(e20,e21),e22) = op2(e20,op2(e21,e22))
& op2(op2(e20,e21),e21) = op2(e20,op2(e21,e21))
& op2(op2(e20,e21),e20) = op2(e20,op2(e21,e20))
& op2(op2(e20,e20),e25) = op2(e20,op2(e20,e25))
& op2(op2(e20,e20),e24) = op2(e20,op2(e20,e24))
& op2(op2(e20,e20),e23) = op2(e20,op2(e20,e23))
& op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22))
& op2(op2(e20,e20),e21) = op2(e20,op2(e20,e21))
& op2(op2(e20,e20),e20) = op2(e20,op2(e20,e20)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f17,axiom,
( op1(e15,e14) != op1(e15,e15)
& op1(e15,e13) != op1(e15,e15)
& op1(e15,e13) != op1(e15,e14)
& op1(e15,e12) != op1(e15,e15)
& op1(e15,e12) != op1(e15,e14)
& op1(e15,e12) != op1(e15,e13)
& op1(e15,e11) != op1(e15,e15)
& op1(e15,e11) != op1(e15,e14)
& op1(e15,e11) != op1(e15,e13)
& op1(e15,e11) != op1(e15,e12)
& op1(e15,e10) != op1(e15,e15)
& op1(e15,e10) != op1(e15,e14)
& op1(e15,e10) != op1(e15,e13)
& op1(e15,e10) != op1(e15,e12)
& op1(e15,e10) != op1(e15,e11)
& op1(e14,e14) != op1(e14,e15)
& op1(e14,e13) != op1(e14,e15)
& op1(e14,e13) != op1(e14,e14)
& op1(e14,e12) != op1(e14,e15)
& op1(e14,e12) != op1(e14,e14)
& op1(e14,e12) != op1(e14,e13)
& op1(e14,e11) != op1(e14,e15)
& op1(e14,e11) != op1(e14,e14)
& op1(e14,e11) != op1(e14,e13)
& op1(e14,e11) != op1(e14,e12)
& op1(e14,e10) != op1(e14,e15)
& 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,e14) != op1(e13,e15)
& op1(e13,e13) != op1(e13,e15)
& op1(e13,e13) != op1(e13,e14)
& op1(e13,e12) != op1(e13,e15)
& op1(e13,e12) != op1(e13,e14)
& op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e15)
& op1(e13,e11) != op1(e13,e14)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e15)
& 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,e14) != op1(e12,e15)
& op1(e12,e13) != op1(e12,e15)
& op1(e12,e13) != op1(e12,e14)
& op1(e12,e12) != op1(e12,e15)
& op1(e12,e12) != op1(e12,e14)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e15)
& op1(e12,e11) != op1(e12,e14)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e15)
& 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,e14) != op1(e11,e15)
& op1(e11,e13) != op1(e11,e15)
& op1(e11,e13) != op1(e11,e14)
& op1(e11,e12) != op1(e11,e15)
& op1(e11,e12) != op1(e11,e14)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e15)
& op1(e11,e11) != op1(e11,e14)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e15)
& 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,e14) != op1(e10,e15)
& op1(e10,e13) != op1(e10,e15)
& op1(e10,e13) != op1(e10,e14)
& op1(e10,e12) != op1(e10,e15)
& op1(e10,e12) != op1(e10,e14)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e15)
& op1(e10,e11) != op1(e10,e14)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e15)
& 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(e14,e15) != op1(e15,e15)
& op1(e13,e15) != op1(e15,e15)
& op1(e13,e15) != op1(e14,e15)
& op1(e12,e15) != op1(e15,e15)
& op1(e12,e15) != op1(e14,e15)
& op1(e12,e15) != op1(e13,e15)
& op1(e11,e15) != op1(e15,e15)
& op1(e11,e15) != op1(e14,e15)
& op1(e11,e15) != op1(e13,e15)
& op1(e11,e15) != op1(e12,e15)
& op1(e10,e15) != op1(e15,e15)
& op1(e10,e15) != op1(e14,e15)
& op1(e10,e15) != op1(e13,e15)
& op1(e10,e15) != op1(e12,e15)
& op1(e10,e15) != op1(e11,e15)
& op1(e14,e14) != op1(e15,e14)
& op1(e13,e14) != op1(e15,e14)
& op1(e13,e14) != op1(e14,e14)
& op1(e12,e14) != op1(e15,e14)
& op1(e12,e14) != op1(e14,e14)
& op1(e12,e14) != op1(e13,e14)
& op1(e11,e14) != op1(e15,e14)
& op1(e11,e14) != op1(e14,e14)
& op1(e11,e14) != op1(e13,e14)
& op1(e11,e14) != op1(e12,e14)
& op1(e10,e14) != op1(e15,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(e14,e13) != op1(e15,e13)
& op1(e13,e13) != op1(e15,e13)
& op1(e13,e13) != op1(e14,e13)
& op1(e12,e13) != op1(e15,e13)
& op1(e12,e13) != op1(e14,e13)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e15,e13)
& op1(e11,e13) != op1(e14,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e15,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(e14,e12) != op1(e15,e12)
& op1(e13,e12) != op1(e15,e12)
& op1(e13,e12) != op1(e14,e12)
& op1(e12,e12) != op1(e15,e12)
& op1(e12,e12) != op1(e14,e12)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e15,e12)
& op1(e11,e12) != op1(e14,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e15,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(e14,e11) != op1(e15,e11)
& op1(e13,e11) != op1(e15,e11)
& op1(e13,e11) != op1(e14,e11)
& op1(e12,e11) != op1(e15,e11)
& op1(e12,e11) != op1(e14,e11)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e15,e11)
& op1(e11,e11) != op1(e14,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e15,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(e14,e10) != op1(e15,e10)
& op1(e13,e10) != op1(e15,e10)
& op1(e13,e10) != op1(e14,e10)
& op1(e12,e10) != op1(e15,e10)
& op1(e12,e10) != op1(e14,e10)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e15,e10)
& op1(e11,e10) != op1(e14,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e15,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',ax17) ).
fof(f18,axiom,
( op2(e25,e24) != op2(e25,e25)
& op2(e25,e23) != op2(e25,e25)
& op2(e25,e23) != op2(e25,e24)
& op2(e25,e22) != op2(e25,e25)
& op2(e25,e22) != op2(e25,e24)
& op2(e25,e22) != op2(e25,e23)
& op2(e25,e21) != op2(e25,e25)
& op2(e25,e21) != op2(e25,e24)
& op2(e25,e21) != op2(e25,e23)
& op2(e25,e21) != op2(e25,e22)
& op2(e25,e20) != op2(e25,e25)
& op2(e25,e20) != op2(e25,e24)
& op2(e25,e20) != op2(e25,e23)
& op2(e25,e20) != op2(e25,e22)
& op2(e25,e20) != op2(e25,e21)
& op2(e24,e24) != op2(e24,e25)
& op2(e24,e23) != op2(e24,e25)
& op2(e24,e23) != op2(e24,e24)
& op2(e24,e22) != op2(e24,e25)
& op2(e24,e22) != op2(e24,e24)
& op2(e24,e22) != op2(e24,e23)
& op2(e24,e21) != op2(e24,e25)
& op2(e24,e21) != op2(e24,e24)
& op2(e24,e21) != op2(e24,e23)
& op2(e24,e21) != op2(e24,e22)
& op2(e24,e20) != op2(e24,e25)
& 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,e24) != op2(e23,e25)
& op2(e23,e23) != op2(e23,e25)
& op2(e23,e23) != op2(e23,e24)
& op2(e23,e22) != op2(e23,e25)
& op2(e23,e22) != op2(e23,e24)
& op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e25)
& op2(e23,e21) != op2(e23,e24)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e25)
& 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,e24) != op2(e22,e25)
& op2(e22,e23) != op2(e22,e25)
& op2(e22,e23) != op2(e22,e24)
& op2(e22,e22) != op2(e22,e25)
& op2(e22,e22) != op2(e22,e24)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e25)
& op2(e22,e21) != op2(e22,e24)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e25)
& 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,e24) != op2(e21,e25)
& op2(e21,e23) != op2(e21,e25)
& op2(e21,e23) != op2(e21,e24)
& op2(e21,e22) != op2(e21,e25)
& op2(e21,e22) != op2(e21,e24)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e25)
& op2(e21,e21) != op2(e21,e24)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e25)
& 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,e24) != op2(e20,e25)
& op2(e20,e23) != op2(e20,e25)
& op2(e20,e23) != op2(e20,e24)
& op2(e20,e22) != op2(e20,e25)
& op2(e20,e22) != op2(e20,e24)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e25)
& op2(e20,e21) != op2(e20,e24)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e25)
& 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(e24,e25) != op2(e25,e25)
& op2(e23,e25) != op2(e25,e25)
& op2(e23,e25) != op2(e24,e25)
& op2(e22,e25) != op2(e25,e25)
& op2(e22,e25) != op2(e24,e25)
& op2(e22,e25) != op2(e23,e25)
& op2(e21,e25) != op2(e25,e25)
& op2(e21,e25) != op2(e24,e25)
& op2(e21,e25) != op2(e23,e25)
& op2(e21,e25) != op2(e22,e25)
& op2(e20,e25) != op2(e25,e25)
& op2(e20,e25) != op2(e24,e25)
& op2(e20,e25) != op2(e23,e25)
& op2(e20,e25) != op2(e22,e25)
& op2(e20,e25) != op2(e21,e25)
& op2(e24,e24) != op2(e25,e24)
& op2(e23,e24) != op2(e25,e24)
& op2(e23,e24) != op2(e24,e24)
& op2(e22,e24) != op2(e25,e24)
& op2(e22,e24) != op2(e24,e24)
& op2(e22,e24) != op2(e23,e24)
& op2(e21,e24) != op2(e25,e24)
& op2(e21,e24) != op2(e24,e24)
& op2(e21,e24) != op2(e23,e24)
& op2(e21,e24) != op2(e22,e24)
& op2(e20,e24) != op2(e25,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(e24,e23) != op2(e25,e23)
& op2(e23,e23) != op2(e25,e23)
& op2(e23,e23) != op2(e24,e23)
& op2(e22,e23) != op2(e25,e23)
& op2(e22,e23) != op2(e24,e23)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e25,e23)
& op2(e21,e23) != op2(e24,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e25,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(e24,e22) != op2(e25,e22)
& op2(e23,e22) != op2(e25,e22)
& op2(e23,e22) != op2(e24,e22)
& op2(e22,e22) != op2(e25,e22)
& op2(e22,e22) != op2(e24,e22)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e25,e22)
& op2(e21,e22) != op2(e24,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e25,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(e24,e21) != op2(e25,e21)
& op2(e23,e21) != op2(e25,e21)
& op2(e23,e21) != op2(e24,e21)
& op2(e22,e21) != op2(e25,e21)
& op2(e22,e21) != op2(e24,e21)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e25,e21)
& op2(e21,e21) != op2(e24,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e25,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(e24,e20) != op2(e25,e20)
& op2(e23,e20) != op2(e25,e20)
& op2(e23,e20) != op2(e24,e20)
& op2(e22,e20) != op2(e25,e20)
& op2(e22,e20) != op2(e24,e20)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e25,e20)
& op2(e21,e20) != op2(e24,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e25,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',ax18) ).
fof(f19,axiom,
( e14 != e15
& e13 != e15
& e13 != e14
& e12 != e15
& e12 != e14
& e12 != e13
& e11 != e15
& e11 != e14
& e11 != e13
& e11 != e12
& e10 != e15
& e10 != e14
& e10 != e13
& e10 != e12
& e10 != e11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f24,axiom,
( e14 = op1(op1(e15,e11),op1(e15,e11))
& e13 = op1(e15,e11)
& e12 = op1(e15,op1(op1(e15,e11),op1(e15,e11)))
& e10 = op1(op1(e15,op1(op1(e15,e11),op1(e15,e11))),op1(e15,op1(op1(e15,e11),op1(e15,e11)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( e24 = op2(op2(e25,e21),op2(e25,e21))
& e23 = op2(e25,e21)
& e22 = op2(e25,op2(op2(e25,e21),op2(e25,e21)))
& e20 = op2(op2(e25,op2(op2(e25,e21),op2(e25,e21))),op2(e25,op2(op2(e25,e21),op2(e25,e21)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax25) ).
fof(f28,axiom,
( h3(e14) = op2(op2(e23,e20),op2(e23,e20))
& h3(e13) = op2(e23,e20)
& h3(e12) = op2(e23,op2(op2(e23,e20),op2(e23,e20)))
& h3(e10) = op2(op2(e23,op2(op2(e23,e20),op2(e23,e20))),op2(e23,op2(op2(e23,e20),op2(e23,e20))))
& h3(e15) = e23
& h3(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f30,axiom,
( h5(e14) = op2(op2(e25,e20),op2(e25,e20))
& h5(e13) = op2(e25,e20)
& h5(e12) = op2(e25,op2(op2(e25,e20),op2(e25,e20)))
& h5(e10) = op2(op2(e25,op2(op2(e25,e20),op2(e25,e20))),op2(e25,op2(op2(e25,e20),op2(e25,e20))))
& h5(e15) = e25
& h5(e11) = e20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax30) ).
fof(f32,axiom,
( h7(e14) = op2(op2(e22,e21),op2(e22,e21))
& h7(e13) = op2(e22,e21)
& h7(e12) = op2(e22,op2(op2(e22,e21),op2(e22,e21)))
& h7(e10) = op2(op2(e22,op2(op2(e22,e21),op2(e22,e21))),op2(e22,op2(op2(e22,e21),op2(e22,e21))))
& h7(e15) = e22
& h7(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax32) ).
fof(f33,axiom,
( h8(e14) = op2(op2(e23,e21),op2(e23,e21))
& h8(e13) = op2(e23,e21)
& h8(e12) = op2(e23,op2(op2(e23,e21),op2(e23,e21)))
& h8(e10) = op2(op2(e23,op2(op2(e23,e21),op2(e23,e21))),op2(e23,op2(op2(e23,e21),op2(e23,e21))))
& h8(e15) = e23
& h8(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax33) ).
fof(f34,axiom,
( h9(e14) = op2(op2(e24,e21),op2(e24,e21))
& h9(e13) = op2(e24,e21)
& h9(e12) = op2(e24,op2(op2(e24,e21),op2(e24,e21)))
& h9(e10) = op2(op2(e24,op2(op2(e24,e21),op2(e24,e21))),op2(e24,op2(op2(e24,e21),op2(e24,e21))))
& h9(e15) = e24
& h9(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax34) ).
fof(f35,axiom,
( h10(e14) = op2(op2(e25,e21),op2(e25,e21))
& h10(e13) = op2(e25,e21)
& h10(e12) = op2(e25,op2(op2(e25,e21),op2(e25,e21)))
& h10(e10) = op2(op2(e25,op2(op2(e25,e21),op2(e25,e21))),op2(e25,op2(op2(e25,e21),op2(e25,e21))))
& h10(e15) = e25
& h10(e11) = e21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax35) ).
fof(f37,axiom,
( h12(e14) = op2(op2(e21,e22),op2(e21,e22))
& h12(e13) = op2(e21,e22)
& h12(e12) = op2(e21,op2(op2(e21,e22),op2(e21,e22)))
& h12(e10) = op2(op2(e21,op2(op2(e21,e22),op2(e21,e22))),op2(e21,op2(op2(e21,e22),op2(e21,e22))))
& h12(e15) = e21
& h12(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax37) ).
fof(f38,axiom,
( h13(e14) = op2(op2(e23,e22),op2(e23,e22))
& h13(e13) = op2(e23,e22)
& h13(e12) = op2(e23,op2(op2(e23,e22),op2(e23,e22)))
& h13(e10) = op2(op2(e23,op2(op2(e23,e22),op2(e23,e22))),op2(e23,op2(op2(e23,e22),op2(e23,e22))))
& h13(e15) = e23
& h13(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax38) ).
fof(f39,axiom,
( h14(e14) = op2(op2(e24,e22),op2(e24,e22))
& h14(e13) = op2(e24,e22)
& h14(e12) = op2(e24,op2(op2(e24,e22),op2(e24,e22)))
& h14(e10) = op2(op2(e24,op2(op2(e24,e22),op2(e24,e22))),op2(e24,op2(op2(e24,e22),op2(e24,e22))))
& h14(e15) = e24
& h14(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax39) ).
fof(f40,axiom,
( h15(e14) = op2(op2(e25,e22),op2(e25,e22))
& h15(e13) = op2(e25,e22)
& h15(e12) = op2(e25,op2(op2(e25,e22),op2(e25,e22)))
& h15(e10) = op2(op2(e25,op2(op2(e25,e22),op2(e25,e22))),op2(e25,op2(op2(e25,e22),op2(e25,e22))))
& h15(e15) = e25
& h15(e11) = e22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax40) ).
fof(f42,axiom,
( h17(e14) = op2(op2(e21,e23),op2(e21,e23))
& h17(e13) = op2(e21,e23)
& h17(e12) = op2(e21,op2(op2(e21,e23),op2(e21,e23)))
& h17(e10) = op2(op2(e21,op2(op2(e21,e23),op2(e21,e23))),op2(e21,op2(op2(e21,e23),op2(e21,e23))))
& h17(e15) = e21
& h17(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax42) ).
fof(f43,axiom,
( h18(e14) = op2(op2(e22,e23),op2(e22,e23))
& h18(e13) = op2(e22,e23)
& h18(e12) = op2(e22,op2(op2(e22,e23),op2(e22,e23)))
& h18(e10) = op2(op2(e22,op2(op2(e22,e23),op2(e22,e23))),op2(e22,op2(op2(e22,e23),op2(e22,e23))))
& h18(e15) = e22
& h18(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax43) ).
fof(f44,axiom,
( h19(e14) = op2(op2(e24,e23),op2(e24,e23))
& h19(e13) = op2(e24,e23)
& h19(e12) = op2(e24,op2(op2(e24,e23),op2(e24,e23)))
& h19(e10) = op2(op2(e24,op2(op2(e24,e23),op2(e24,e23))),op2(e24,op2(op2(e24,e23),op2(e24,e23))))
& h19(e15) = e24
& h19(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax44) ).
fof(f45,axiom,
( h20(e14) = op2(op2(e25,e23),op2(e25,e23))
& h20(e13) = op2(e25,e23)
& h20(e12) = op2(e25,op2(op2(e25,e23),op2(e25,e23)))
& h20(e10) = op2(op2(e25,op2(op2(e25,e23),op2(e25,e23))),op2(e25,op2(op2(e25,e23),op2(e25,e23))))
& h20(e15) = e25
& h20(e11) = e23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax45) ).
fof(f47,axiom,
( h22(e14) = op2(op2(e21,e24),op2(e21,e24))
& h22(e13) = op2(e21,e24)
& h22(e12) = op2(e21,op2(op2(e21,e24),op2(e21,e24)))
& h22(e10) = op2(op2(e21,op2(op2(e21,e24),op2(e21,e24))),op2(e21,op2(op2(e21,e24),op2(e21,e24))))
& h22(e15) = e21
& h22(e11) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax47) ).
fof(f48,axiom,
( h23(e14) = op2(op2(e22,e24),op2(e22,e24))
& h23(e13) = op2(e22,e24)
& h23(e12) = op2(e22,op2(op2(e22,e24),op2(e22,e24)))
& h23(e10) = op2(op2(e22,op2(op2(e22,e24),op2(e22,e24))),op2(e22,op2(op2(e22,e24),op2(e22,e24))))
& h23(e15) = e22
& h23(e11) = e24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax48) ).
fof(f51,axiom,
( h26(e14) = op2(op2(e20,e25),op2(e20,e25))
& h26(e13) = op2(e20,e25)
& h26(e12) = op2(e20,op2(op2(e20,e25),op2(e20,e25)))
& h26(e10) = op2(op2(e20,op2(op2(e20,e25),op2(e20,e25))),op2(e20,op2(op2(e20,e25),op2(e20,e25))))
& h26(e15) = e20
& h26(e11) = e25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax51) ).
fof(f52,axiom,
( h27(e14) = op2(op2(e21,e25),op2(e21,e25))
& h27(e13) = op2(e21,e25)
& h27(e12) = op2(e21,op2(op2(e21,e25),op2(e21,e25)))
& h27(e10) = op2(op2(e21,op2(op2(e21,e25),op2(e21,e25))),op2(e21,op2(op2(e21,e25),op2(e21,e25))))
& h27(e15) = e21
& h27(e11) = e25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax52) ).
fof(f53,axiom,
( h28(e14) = op2(op2(e22,e25),op2(e22,e25))
& h28(e13) = op2(e22,e25)
& h28(e12) = op2(e22,op2(op2(e22,e25),op2(e22,e25)))
& h28(e10) = op2(op2(e22,op2(op2(e22,e25),op2(e22,e25))),op2(e22,op2(op2(e22,e25),op2(e22,e25))))
& h28(e15) = e22
& h28(e11) = e25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax53) ).
fof(f54,axiom,
( h29(e14) = op2(op2(e23,e25),op2(e23,e25))
& h29(e13) = op2(e23,e25)
& h29(e12) = op2(e23,op2(op2(e23,e25),op2(e23,e25)))
& h29(e10) = op2(op2(e23,op2(op2(e23,e25),op2(e23,e25))),op2(e23,op2(op2(e23,e25),op2(e23,e25))))
& h29(e15) = e23
& h29(e11) = e25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax54) ).
fof(f55,axiom,
( h30(e14) = op2(op2(e24,e25),op2(e24,e25))
& h30(e13) = op2(e24,e25)
& h30(e12) = op2(e24,op2(op2(e24,e25),op2(e24,e25)))
& h30(e10) = op2(op2(e24,op2(op2(e24,e25),op2(e24,e25))),op2(e24,op2(op2(e24,e25),op2(e24,e25))))
& h30(e15) = e24
& h30(e11) = e25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax55) ).
fof(f259,plain,
( ~ sP104
| ( e21 != h10(e15)
& e21 != h10(e14)
& e21 != h10(e13)
& e21 != h10(e12)
& e21 != h10(e11)
& e21 != h10(e10) ) ),
inference(nnf_transformation,[],[f167]) ).
fof(f260,plain,
( ~ sP103
| ( e22 != h10(e15)
& e22 != h10(e14)
& e22 != h10(e13)
& e22 != h10(e12)
& e22 != h10(e11)
& e22 != h10(e10) ) ),
inference(nnf_transformation,[],[f166]) ).
fof(f261,plain,
( ~ sP102
| ( e23 != h10(e15)
& e23 != h10(e14)
& e23 != h10(e13)
& e23 != h10(e12)
& e23 != h10(e11)
& e23 != h10(e10) ) ),
inference(nnf_transformation,[],[f165]) ).
fof(f262,plain,
( ~ sP101
| ( e24 != h10(e15)
& e24 != h10(e14)
& e24 != h10(e13)
& e24 != h10(e12)
& e24 != h10(e11)
& e24 != h10(e10) ) ),
inference(nnf_transformation,[],[f164]) ).
fof(f263,plain,
( ~ sP100
| ( e25 != h10(e15)
& e25 != h10(e14)
& e25 != h10(e13)
& e25 != h10(e12)
& e25 != h10(e11)
& e25 != h10(e10) ) ),
inference(nnf_transformation,[],[f163]) ).
fof(f367,plain,
( e15 = op1(e15,e12)
| e14 = op1(e15,e12)
| e13 = op1(e15,e12)
| e12 = op1(e15,e12)
| e11 = op1(e15,e12)
| e10 = op1(e15,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f369,plain,
( e15 = op1(e15,e10)
| e14 = op1(e15,e10)
| e13 = op1(e15,e10)
| e12 = op1(e15,e10)
| e11 = op1(e15,e10)
| e10 = op1(e15,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f370,plain,
( e15 = op1(e14,e15)
| e14 = op1(e14,e15)
| e13 = op1(e14,e15)
| e12 = op1(e14,e15)
| e11 = op1(e14,e15)
| e10 = op1(e14,e15) ),
inference(cnf_transformation,[],[f1]) ).
fof(f372,plain,
( e15 = op1(e14,e13)
| e14 = op1(e14,e13)
| e13 = op1(e14,e13)
| e12 = op1(e14,e13)
| e11 = op1(e14,e13)
| e10 = op1(e14,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f374,plain,
( e15 = op1(e14,e11)
| e14 = op1(e14,e11)
| e13 = op1(e14,e11)
| e12 = op1(e14,e11)
| e11 = op1(e14,e11)
| e10 = op1(e14,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f379,plain,
( e15 = op1(e13,e12)
| e14 = op1(e13,e12)
| e13 = op1(e13,e12)
| e12 = op1(e13,e12)
| e11 = op1(e13,e12)
| e10 = op1(e13,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f384,plain,
( e15 = op1(e12,e13)
| e14 = op1(e12,e13)
| e13 = op1(e12,e13)
| e12 = op1(e12,e13)
| e11 = op1(e12,e13)
| e10 = op1(e12,e13) ),
inference(cnf_transformation,[],[f1]) ).
fof(f386,plain,
( e15 = op1(e12,e11)
| e14 = op1(e12,e11)
| e13 = op1(e12,e11)
| e12 = op1(e12,e11)
| e11 = op1(e12,e11)
| e10 = op1(e12,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f392,plain,
( e15 = op1(e11,e11)
| 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(f393,plain,
( e15 = op1(e11,e10)
| e14 = op1(e11,e10)
| e13 = op1(e11,e10)
| e12 = op1(e11,e10)
| e11 = op1(e11,e10)
| e10 = op1(e11,e10) ),
inference(cnf_transformation,[],[f1]) ).
fof(f394,plain,
( e15 = op1(e10,e15)
| e14 = op1(e10,e15)
| e13 = op1(e10,e15)
| e12 = op1(e10,e15)
| e11 = op1(e10,e15)
| e10 = op1(e10,e15) ),
inference(cnf_transformation,[],[f1]) ).
fof(f398,plain,
( e15 = op1(e10,e11)
| e14 = op1(e10,e11)
| e13 = op1(e10,e11)
| e12 = op1(e10,e11)
| e11 = op1(e10,e11)
| e10 = op1(e10,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f400,plain,
op1(op1(e15,e15),e15) = op1(e15,op1(e15,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f406,plain,
op1(op1(e15,e14),e15) = op1(e15,op1(e14,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f408,plain,
op1(op1(e15,e14),e13) = op1(e15,op1(e14,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f409,plain,
op1(op1(e15,e14),e12) = op1(e15,op1(e14,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f410,plain,
op1(op1(e15,e14),e11) = op1(e15,op1(e14,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f411,plain,
op1(op1(e15,e14),e10) = op1(e15,op1(e14,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f419,plain,
op1(op1(e15,e12),e14) = op1(e15,op1(e12,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f421,plain,
op1(op1(e15,e12),e12) = op1(e15,op1(e12,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f422,plain,
op1(op1(e15,e12),e11) = op1(e15,op1(e12,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f423,plain,
op1(op1(e15,e12),e10) = op1(e15,op1(e12,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f424,plain,
op1(op1(e15,e11),e15) = op1(e15,op1(e11,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f425,plain,
op1(op1(e15,e11),e14) = op1(e15,op1(e11,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f427,plain,
op1(op1(e15,e11),e12) = op1(e15,op1(e11,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f428,plain,
op1(op1(e15,e11),e11) = op1(e15,op1(e11,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f429,plain,
op1(op1(e15,e11),e10) = op1(e15,op1(e11,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f430,plain,
op1(op1(e15,e10),e15) = op1(e15,op1(e10,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f433,plain,
op1(op1(e15,e10),e12) = op1(e15,op1(e10,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f434,plain,
op1(op1(e15,e10),e11) = op1(e15,op1(e10,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f437,plain,
op1(op1(e14,e15),e14) = op1(e14,op1(e15,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f439,plain,
op1(op1(e14,e15),e12) = op1(e14,op1(e15,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f440,plain,
op1(op1(e14,e15),e11) = op1(e14,op1(e15,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f441,plain,
op1(op1(e14,e15),e10) = op1(e14,op1(e15,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f445,plain,
op1(op1(e14,e14),e12) = op1(e14,op1(e14,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f446,plain,
op1(op1(e14,e14),e11) = op1(e14,op1(e14,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f447,plain,
op1(op1(e14,e14),e10) = op1(e14,op1(e14,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f457,plain,
op1(op1(e14,e12),e12) = op1(e14,op1(e12,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f458,plain,
op1(op1(e14,e12),e11) = op1(e14,op1(e12,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f470,plain,
op1(op1(e14,e10),e11) = op1(e14,op1(e10,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f473,plain,
op1(op1(e13,e15),e14) = op1(e13,op1(e15,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f484,plain,
op1(op1(e13,e13),e15) = op1(e13,op1(e13,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f486,plain,
op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f487,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f488,plain,
op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f489,plain,
op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f491,plain,
op1(op1(e13,e12),e14) = op1(e13,op1(e12,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f493,plain,
op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f494,plain,
op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f509,plain,
op1(op1(e12,e15),e14) = op1(e12,op1(e15,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f511,plain,
op1(op1(e12,e15),e12) = op1(e12,op1(e15,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f512,plain,
op1(op1(e12,e15),e11) = op1(e12,op1(e15,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f513,plain,
op1(op1(e12,e15),e10) = op1(e12,op1(e15,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f514,plain,
op1(op1(e12,e14),e15) = op1(e12,op1(e14,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f517,plain,
op1(op1(e12,e14),e12) = op1(e12,op1(e14,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f518,plain,
op1(op1(e12,e14),e11) = op1(e12,op1(e14,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f526,plain,
op1(op1(e12,e12),e15) = op1(e12,op1(e12,e15)),
inference(cnf_transformation,[],[f2]) ).
fof(f527,plain,
op1(op1(e12,e12),e14) = op1(e12,op1(e12,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f529,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f530,plain,
op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f531,plain,
op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f535,plain,
op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f542,plain,
op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f543,plain,
op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f548,plain,
op1(op1(e11,e15),e11) = op1(e11,op1(e15,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f553,plain,
op1(op1(e11,e14),e12) = op1(e11,op1(e14,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f569,plain,
op1(op1(e11,e11),e14) = op1(e11,op1(e11,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f571,plain,
op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f581,plain,
op1(op1(e10,e15),e14) = op1(e10,op1(e15,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f584,plain,
op1(op1(e10,e15),e11) = op1(e10,op1(e15,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f585,plain,
op1(op1(e10,e15),e10) = op1(e10,op1(e15,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f587,plain,
op1(op1(e10,e14),e14) = op1(e10,op1(e14,e14)),
inference(cnf_transformation,[],[f2]) ).
fof(f594,plain,
op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f602,plain,
op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f603,plain,
op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f650,plain,
( e25 = op2(e25,e22)
| e24 = op2(e25,e22)
| e23 = op2(e25,e22)
| e22 = op2(e25,e22)
| e21 = op2(e25,e22)
| e20 = op2(e25,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f652,plain,
( e25 = op2(e25,e20)
| e24 = op2(e25,e20)
| e23 = op2(e25,e20)
| e22 = op2(e25,e20)
| e21 = op2(e25,e20)
| e20 = op2(e25,e20) ),
inference(cnf_transformation,[],[f5]) ).
fof(f656,plain,
( e25 = op2(e24,e22)
| e24 = op2(e24,e22)
| e23 = op2(e24,e22)
| e22 = op2(e24,e22)
| e21 = op2(e24,e22)
| e20 = op2(e24,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f657,plain,
( e25 = op2(e24,e21)
| e24 = op2(e24,e21)
| e23 = op2(e24,e21)
| e22 = op2(e24,e21)
| e21 = op2(e24,e21)
| e20 = op2(e24,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f659,plain,
( e25 = op2(e23,e25)
| e24 = op2(e23,e25)
| e23 = op2(e23,e25)
| e22 = op2(e23,e25)
| e21 = op2(e23,e25)
| e20 = op2(e23,e25) ),
inference(cnf_transformation,[],[f5]) ).
fof(f662,plain,
( e25 = op2(e23,e22)
| e24 = op2(e23,e22)
| e23 = op2(e23,e22)
| e22 = op2(e23,e22)
| e21 = op2(e23,e22)
| e20 = op2(e23,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f663,plain,
( e25 = op2(e23,e21)
| e24 = op2(e23,e21)
| e23 = op2(e23,e21)
| e22 = op2(e23,e21)
| e21 = op2(e23,e21)
| e20 = op2(e23,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f669,plain,
( e25 = op2(e22,e21)
| e24 = op2(e22,e21)
| e23 = op2(e22,e21)
| e22 = op2(e22,e21)
| e21 = op2(e22,e21)
| e20 = op2(e22,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f672,plain,
( e25 = op2(e21,e24)
| e24 = op2(e21,e24)
| e23 = op2(e21,e24)
| e22 = op2(e21,e24)
| e21 = op2(e21,e24)
| e20 = op2(e21,e24) ),
inference(cnf_transformation,[],[f5]) ).
fof(f677,plain,
( e25 = op2(e20,e25)
| e24 = op2(e20,e25)
| e23 = op2(e20,e25)
| e22 = op2(e20,e25)
| e21 = op2(e20,e25)
| e20 = op2(e20,e25) ),
inference(cnf_transformation,[],[f5]) ).
fof(f684,plain,
op2(op2(e25,e25),e24) = op2(e25,op2(e25,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f689,plain,
op2(op2(e25,e24),e25) = op2(e25,op2(e24,e25)),
inference(cnf_transformation,[],[f6]) ).
fof(f691,plain,
op2(op2(e25,e24),e23) = op2(e25,op2(e24,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f692,plain,
op2(op2(e25,e24),e22) = op2(e25,op2(e24,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f693,plain,
op2(op2(e25,e24),e21) = op2(e25,op2(e24,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f696,plain,
op2(op2(e25,e23),e24) = op2(e25,op2(e23,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f697,plain,
op2(op2(e25,e23),e23) = op2(e25,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f699,plain,
op2(op2(e25,e23),e21) = op2(e25,op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f702,plain,
op2(op2(e25,e22),e24) = op2(e25,op2(e22,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f710,plain,
op2(op2(e25,e21),e22) = op2(e25,op2(e21,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f711,plain,
op2(op2(e25,e21),e21) = op2(e25,op2(e21,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f712,plain,
op2(op2(e25,e21),e20) = op2(e25,op2(e21,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f734,plain,
op2(op2(e24,e23),e22) = op2(e24,op2(e23,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f740,plain,
op2(op2(e24,e22),e22) = op2(e24,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f756,plain,
op2(op2(e23,e25),e24) = op2(e23,op2(e25,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f764,plain,
op2(op2(e23,e24),e22) = op2(e23,op2(e24,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f767,plain,
op2(op2(e23,e23),e25) = op2(e23,op2(e23,e25)),
inference(cnf_transformation,[],[f6]) ).
fof(f769,plain,
op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f770,plain,
op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f771,plain,
op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f772,plain,
op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f774,plain,
op2(op2(e23,e22),e24) = op2(e23,op2(e22,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f776,plain,
op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f777,plain,
op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f778,plain,
op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f781,plain,
op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f788,plain,
op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f797,plain,
op2(op2(e22,e24),e25) = op2(e22,op2(e24,e25)),
inference(cnf_transformation,[],[f6]) ).
fof(f805,plain,
op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f812,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f814,plain,
op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f818,plain,
op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f847,plain,
op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f852,plain,
op2(op2(e21,e21),e24) = op2(e21,op2(e21,e24)),
inference(cnf_transformation,[],[f6]) ).
fof(f853,plain,
op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f854,plain,
op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f855,plain,
op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f873,plain,
op2(op2(e20,e24),e21) = op2(e20,op2(e24,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f1046,plain,
op1(e15,e14) != op1(e15,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1050,plain,
op1(e15,e12) != op1(e15,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1052,plain,
op1(e15,e11) != op1(e15,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1055,plain,
op1(e15,e11) != op1(e15,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1057,plain,
op1(e15,e10) != op1(e15,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1059,plain,
op1(e15,e10) != op1(e15,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1060,plain,
op1(e15,e10) != op1(e15,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1061,plain,
op1(e14,e14) != op1(e14,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1064,plain,
op1(e14,e12) != op1(e14,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1065,plain,
op1(e14,e12) != op1(e14,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1066,plain,
op1(e14,e12) != op1(e14,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1067,plain,
op1(e14,e11) != op1(e14,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1069,plain,
op1(e14,e11) != op1(e14,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1071,plain,
op1(e14,e10) != op1(e14,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1075,plain,
op1(e14,e10) != op1(e14,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1081,plain,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1083,plain,
op1(e13,e11) != op1(e13,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1084,plain,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1092,plain,
op1(e12,e13) != op1(e12,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1094,plain,
op1(e12,e12) != op1(e12,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1095,plain,
op1(e12,e12) != op1(e12,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1096,plain,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1097,plain,
op1(e12,e11) != op1(e12,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1100,plain,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1103,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1121,plain,
op1(e10,e14) != op1(e10,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1124,plain,
op1(e10,e12) != op1(e10,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1127,plain,
op1(e10,e11) != op1(e10,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1128,plain,
op1(e10,e11) != op1(e10,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1130,plain,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1135,plain,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1136,plain,
op1(e14,e15) != op1(e15,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1139,plain,
op1(e12,e15) != op1(e15,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1146,plain,
op1(e10,e15) != op1(e15,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1147,plain,
op1(e10,e15) != op1(e14,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1149,plain,
op1(e10,e15) != op1(e12,e15),
inference(cnf_transformation,[],[f17]) ).
fof(f1152,plain,
op1(e13,e14) != op1(e15,e14),
inference(cnf_transformation,[],[f17]) ).
fof(f1168,plain,
op1(e13,e13) != op1(e14,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1170,plain,
op1(e12,e13) != op1(e14,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1171,plain,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f1183,plain,
op1(e13,e12) != op1(e14,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1184,plain,
op1(e12,e12) != op1(e15,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1185,plain,
op1(e12,e12) != op1(e14,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1186,plain,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1193,plain,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f1196,plain,
op1(e14,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1198,plain,
op1(e13,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1199,plain,
op1(e12,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1200,plain,
op1(e12,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1202,plain,
op1(e11,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1203,plain,
op1(e11,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1205,plain,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1206,plain,
op1(e10,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1207,plain,
op1(e10,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1208,plain,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1209,plain,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1210,plain,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f1215,plain,
op1(e12,e10) != op1(e14,e10),
inference(cnf_transformation,[],[f17]) ).
fof(f1217,plain,
op1(e11,e10) != op1(e15,e10),
inference(cnf_transformation,[],[f17]) ).
fof(f1218,plain,
op1(e11,e10) != op1(e14,e10),
inference(cnf_transformation,[],[f17]) ).
fof(f1219,plain,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f17]) ).
fof(f1220,plain,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f17]) ).
fof(f1225,plain,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f17]) ).
fof(f1230,plain,
op2(e25,e22) != op2(e25,e24),
inference(cnf_transformation,[],[f18]) ).
fof(f1235,plain,
op2(e25,e21) != op2(e25,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1237,plain,
op2(e25,e20) != op2(e25,e24),
inference(cnf_transformation,[],[f18]) ).
fof(f1240,plain,
op2(e25,e20) != op2(e25,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1250,plain,
op2(e24,e21) != op2(e24,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1255,plain,
op2(e24,e20) != op2(e24,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1257,plain,
op2(e23,e23) != op2(e23,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1259,plain,
op2(e23,e22) != op2(e23,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1260,plain,
op2(e23,e22) != op2(e23,e24),
inference(cnf_transformation,[],[f18]) ).
fof(f1261,plain,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f1264,plain,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f1265,plain,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1266,plain,
op2(e23,e20) != op2(e23,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1268,plain,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f1269,plain,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1276,plain,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f1280,plain,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1285,plain,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1290,plain,
op2(e21,e22) != op2(e21,e24),
inference(cnf_transformation,[],[f18]) ).
fof(f1297,plain,
op2(e21,e20) != op2(e21,e24),
inference(cnf_transformation,[],[f18]) ).
fof(f1301,plain,
op2(e20,e24) != op2(e20,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1302,plain,
op2(e20,e23) != op2(e20,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1304,plain,
op2(e20,e22) != op2(e20,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1307,plain,
op2(e20,e21) != op2(e20,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1311,plain,
op2(e20,e20) != op2(e20,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1317,plain,
op2(e23,e25) != op2(e25,e25),
inference(cnf_transformation,[],[f18]) ).
fof(f1337,plain,
op2(e21,e24) != op2(e25,e24),
inference(cnf_transformation,[],[f18]) ).
fof(f1351,plain,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f1361,plain,
op2(e24,e22) != op2(e25,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1362,plain,
op2(e23,e22) != op2(e25,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1363,plain,
op2(e23,e22) != op2(e24,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1364,plain,
op2(e22,e22) != op2(e25,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1365,plain,
op2(e22,e22) != op2(e24,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1366,plain,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f1376,plain,
op2(e24,e21) != op2(e25,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1377,plain,
op2(e23,e21) != op2(e25,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1378,plain,
op2(e23,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1379,plain,
op2(e22,e21) != op2(e25,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1381,plain,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1383,plain,
op2(e21,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1387,plain,
op2(e20,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1389,plain,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f18]) ).
fof(f1391,plain,
op2(e24,e20) != op2(e25,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f1397,plain,
op2(e21,e20) != op2(e25,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f1401,plain,
op2(e20,e20) != op2(e25,e20),
inference(cnf_transformation,[],[f18]) ).
fof(f1418,plain,
e10 != e13,
inference(cnf_transformation,[],[f19]) ).
fof(f1474,plain,
e14 = op1(op1(e15,e11),op1(e15,e11)),
inference(cnf_transformation,[],[f24]) ).
fof(f1475,plain,
e13 = op1(e15,e11),
inference(cnf_transformation,[],[f24]) ).
fof(f1476,plain,
e12 = op1(e15,op1(op1(e15,e11),op1(e15,e11))),
inference(cnf_transformation,[],[f24]) ).
fof(f1477,plain,
e10 = op1(op1(e15,op1(op1(e15,e11),op1(e15,e11))),op1(e15,op1(op1(e15,e11),op1(e15,e11)))),
inference(cnf_transformation,[],[f24]) ).
fof(f1478,plain,
e24 = op2(op2(e25,e21),op2(e25,e21)),
inference(cnf_transformation,[],[f25]) ).
fof(f1479,plain,
e23 = op2(e25,e21),
inference(cnf_transformation,[],[f25]) ).
fof(f1480,plain,
e22 = op2(e25,op2(op2(e25,e21),op2(e25,e21))),
inference(cnf_transformation,[],[f25]) ).
fof(f1481,plain,
e20 = op2(op2(e25,op2(op2(e25,e21),op2(e25,e21))),op2(e25,op2(op2(e25,e21),op2(e25,e21)))),
inference(cnf_transformation,[],[f25]) ).
fof(f1495,plain,
op2(e23,e20) = h3(e13),
inference(cnf_transformation,[],[f28]) ).
fof(f1507,plain,
op2(e25,e20) = h5(e13),
inference(cnf_transformation,[],[f30]) ).
fof(f1519,plain,
op2(e22,e21) = h7(e13),
inference(cnf_transformation,[],[f32]) ).
fof(f1525,plain,
op2(e23,e21) = h8(e13),
inference(cnf_transformation,[],[f33]) ).
fof(f1531,plain,
op2(e24,e21) = h9(e13),
inference(cnf_transformation,[],[f34]) ).
fof(f1536,plain,
op2(op2(e25,e21),op2(e25,e21)) = h10(e14),
inference(cnf_transformation,[],[f35]) ).
fof(f1537,plain,
op2(e25,e21) = h10(e13),
inference(cnf_transformation,[],[f35]) ).
fof(f1538,plain,
op2(e25,op2(op2(e25,e21),op2(e25,e21))) = h10(e12),
inference(cnf_transformation,[],[f35]) ).
fof(f1539,plain,
op2(op2(e25,op2(op2(e25,e21),op2(e25,e21))),op2(e25,op2(op2(e25,e21),op2(e25,e21)))) = h10(e10),
inference(cnf_transformation,[],[f35]) ).
fof(f1540,plain,
e25 = h10(e15),
inference(cnf_transformation,[],[f35]) ).
fof(f1541,plain,
e21 = h10(e11),
inference(cnf_transformation,[],[f35]) ).
fof(f1549,plain,
op2(e21,e22) = h12(e13),
inference(cnf_transformation,[],[f37]) ).
fof(f1555,plain,
op2(e23,e22) = h13(e13),
inference(cnf_transformation,[],[f38]) ).
fof(f1561,plain,
op2(e24,e22) = h14(e13),
inference(cnf_transformation,[],[f39]) ).
fof(f1567,plain,
op2(e25,e22) = h15(e13),
inference(cnf_transformation,[],[f40]) ).
fof(f1579,plain,
op2(e21,e23) = h17(e13),
inference(cnf_transformation,[],[f42]) ).
fof(f1585,plain,
op2(e22,e23) = h18(e13),
inference(cnf_transformation,[],[f43]) ).
fof(f1591,plain,
op2(e24,e23) = h19(e13),
inference(cnf_transformation,[],[f44]) ).
fof(f1597,plain,
op2(e25,e23) = h20(e13),
inference(cnf_transformation,[],[f45]) ).
fof(f1609,plain,
op2(e21,e24) = h22(e13),
inference(cnf_transformation,[],[f47]) ).
fof(f1615,plain,
op2(e22,e24) = h23(e13),
inference(cnf_transformation,[],[f48]) ).
fof(f1633,plain,
op2(e20,e25) = h26(e13),
inference(cnf_transformation,[],[f51]) ).
fof(f1639,plain,
op2(e21,e25) = h27(e13),
inference(cnf_transformation,[],[f52]) ).
fof(f1645,plain,
op2(e22,e25) = h28(e13),
inference(cnf_transformation,[],[f53]) ).
fof(f1651,plain,
op2(e23,e25) = h29(e13),
inference(cnf_transformation,[],[f54]) ).
fof(f1657,plain,
op2(e24,e25) = h30(e13),
inference(cnf_transformation,[],[f55]) ).
fof(f1936,plain,
( ~ sP104
| e21 != h10(e11) ),
inference(cnf_transformation,[],[f259]) ).
fof(f1941,plain,
( ~ sP103
| e22 != h10(e12) ),
inference(cnf_transformation,[],[f260]) ).
fof(f1946,plain,
( ~ sP102
| e23 != h10(e13) ),
inference(cnf_transformation,[],[f261]) ).
fof(f1951,plain,
( ~ sP101
| e24 != h10(e14) ),
inference(cnf_transformation,[],[f262]) ).
fof(f1956,plain,
( ~ sP100
| e25 != h10(e15) ),
inference(cnf_transformation,[],[f263]) ).
fof(f2687,plain,
( sP100
| sP101
| sP102
| sP103
| sP104
| e20 != h10(e10)
| h10(op1(e15,e15)) != op2(h10(e15),h10(e15))
| h10(op1(e15,e14)) != op2(h10(e15),h10(e14))
| h10(op1(e15,e13)) != op2(h10(e15),h10(e13))
| h10(op1(e15,e12)) != op2(h10(e15),h10(e12))
| h10(op1(e15,e11)) != op2(h10(e15),h10(e11))
| h10(op1(e15,e10)) != op2(h10(e15),h10(e10))
| h10(op1(e14,e15)) != op2(h10(e14),h10(e15))
| 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,e15)) != op2(h10(e13),h10(e15))
| 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,e15)) != op2(h10(e12),h10(e15))
| 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,e15)) != op2(h10(e11),h10(e15))
| 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,e15)) != op2(h10(e10),h10(e15))
| 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,[],[f213]) ).
tcf(c_50,plain,
( ( op1(e10,e11) = e15 )
| ( op1(e10,e11) = e14 )
| ( op1(e10,e11) = e13 )
| ( op1(e10,e11) = e12 )
| ( op1(e10,e11) = e11 )
| ( op1(e10,e11) = e10 ) ),
inference(cnf_transformation,[],[f398]) ).
tcf(c_54,plain,
( ( op1(e10,e15) = e15 )
| ( op1(e10,e15) = e14 )
| ( op1(e10,e15) = e13 )
| ( op1(e10,e15) = e12 )
| ( op1(e10,e15) = e11 )
| ( op1(e10,e15) = e10 ) ),
inference(cnf_transformation,[],[f394]) ).
tcf(c_55,plain,
( ( op1(e11,e10) = e15 )
| ( op1(e11,e10) = e14 )
| ( op1(e11,e10) = e13 )
| ( op1(e11,e10) = e12 )
| ( op1(e11,e10) = e11 )
| ( op1(e11,e10) = e10 ) ),
inference(cnf_transformation,[],[f393]) ).
tcf(c_56,plain,
( ( op1(e11,e11) = e15 )
| ( op1(e11,e11) = e14 )
| ( op1(e11,e11) = e13 )
| ( op1(e11,e11) = e12 )
| ( op1(e11,e11) = e11 )
| ( op1(e11,e11) = e10 ) ),
inference(cnf_transformation,[],[f392]) ).
tcf(c_62,plain,
( ( op1(e12,e11) = e15 )
| ( op1(e12,e11) = e14 )
| ( op1(e12,e11) = e13 )
| ( op1(e12,e11) = e12 )
| ( op1(e12,e11) = e11 )
| ( op1(e12,e11) = e10 ) ),
inference(cnf_transformation,[],[f386]) ).
tcf(c_64,plain,
( ( op1(e12,e13) = e15 )
| ( op1(e12,e13) = e14 )
| ( op1(e12,e13) = e13 )
| ( op1(e12,e13) = e12 )
| ( op1(e12,e13) = e11 )
| ( op1(e12,e13) = e10 ) ),
inference(cnf_transformation,[],[f384]) ).
tcf(c_69,plain,
( ( op1(e13,e12) = e15 )
| ( op1(e13,e12) = e14 )
| ( op1(e13,e12) = e13 )
| ( op1(e13,e12) = e12 )
| ( op1(e13,e12) = e11 )
| ( op1(e13,e12) = e10 ) ),
inference(cnf_transformation,[],[f379]) ).
tcf(c_74,plain,
( ( op1(e14,e11) = e15 )
| ( op1(e14,e11) = e14 )
| ( op1(e14,e11) = e13 )
| ( op1(e14,e11) = e12 )
| ( op1(e14,e11) = e11 )
| ( op1(e14,e11) = e10 ) ),
inference(cnf_transformation,[],[f374]) ).
tcf(c_76,plain,
( ( op1(e14,e13) = e15 )
| ( op1(e14,e13) = e14 )
| ( op1(e14,e13) = e13 )
| ( op1(e14,e13) = e12 )
| ( op1(e14,e13) = e11 )
| ( op1(e14,e13) = e10 ) ),
inference(cnf_transformation,[],[f372]) ).
tcf(c_78,plain,
( ( op1(e14,e15) = e15 )
| ( op1(e14,e15) = e14 )
| ( op1(e14,e15) = e13 )
| ( op1(e14,e15) = e12 )
| ( op1(e14,e15) = e11 )
| ( op1(e14,e15) = e10 ) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_79,plain,
( ( op1(e15,e10) = e15 )
| ( op1(e15,e10) = e14 )
| ( op1(e15,e10) = e13 )
| ( op1(e15,e10) = e12 )
| ( op1(e15,e10) = e11 )
| ( op1(e15,e10) = e10 ) ),
inference(cnf_transformation,[],[f369]) ).
tcf(c_81,plain,
( ( op1(e15,e12) = e15 )
| ( op1(e15,e12) = e14 )
| ( op1(e15,e12) = e13 )
| ( op1(e15,e12) = e12 )
| ( op1(e15,e12) = e11 )
| ( op1(e15,e12) = e10 ) ),
inference(cnf_transformation,[],[f367]) ).
tcf(c_97,plain,
op1(op1(e10,e12),e10) = op1(e10,op1(e12,e10)),
inference(cnf_transformation,[],[f603]) ).
tcf(c_98,plain,
op1(op1(e10,e12),e11) = op1(e10,op1(e12,e11)),
inference(cnf_transformation,[],[f602]) ).
tcf(c_106,plain,
op1(op1(e10,e13),e13) = op1(e10,op1(e13,e13)),
inference(cnf_transformation,[],[f594]) ).
tcf(c_113,plain,
op1(op1(e10,e14),e14) = op1(e10,op1(e14,e14)),
inference(cnf_transformation,[],[f587]) ).
tcf(c_115,plain,
op1(op1(e10,e15),e10) = op1(e10,op1(e15,e10)),
inference(cnf_transformation,[],[f585]) ).
tcf(c_116,plain,
op1(op1(e10,e15),e11) = op1(e10,op1(e15,e11)),
inference(cnf_transformation,[],[f584]) ).
tcf(c_119,plain,
op1(op1(e10,e15),e14) = op1(e10,op1(e15,e14)),
inference(cnf_transformation,[],[f581]) ).
tcf(c_129,plain,
op1(op1(e11,e11),e12) = op1(e11,op1(e11,e12)),
inference(cnf_transformation,[],[f571]) ).
tcf(c_131,plain,
op1(op1(e11,e11),e14) = op1(e11,op1(e11,e14)),
inference(cnf_transformation,[],[f569]) ).
tcf(c_147,plain,
op1(op1(e11,e14),e12) = op1(e11,op1(e14,e12)),
inference(cnf_transformation,[],[f553]) ).
tcf(c_152,plain,
op1(op1(e11,e15),e11) = op1(e11,op1(e15,e11)),
inference(cnf_transformation,[],[f548]) ).
tcf(c_157,plain,
op1(op1(e12,e10),e10) = op1(e12,op1(e10,e10)),
inference(cnf_transformation,[],[f543]) ).
tcf(c_158,plain,
op1(op1(e12,e10),e11) = op1(e12,op1(e10,e11)),
inference(cnf_transformation,[],[f542]) ).
tcf(c_165,plain,
op1(op1(e12,e11),e12) = op1(e12,op1(e11,e12)),
inference(cnf_transformation,[],[f535]) ).
tcf(c_169,plain,
op1(op1(e12,e12),e10) = op1(e12,op1(e12,e10)),
inference(cnf_transformation,[],[f531]) ).
tcf(c_170,plain,
op1(op1(e12,e12),e11) = op1(e12,op1(e12,e11)),
inference(cnf_transformation,[],[f530]) ).
tcf(c_171,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f529]) ).
tcf(c_173,plain,
op1(op1(e12,e12),e14) = op1(e12,op1(e12,e14)),
inference(cnf_transformation,[],[f527]) ).
tcf(c_174,plain,
op1(op1(e12,e12),e15) = op1(e12,op1(e12,e15)),
inference(cnf_transformation,[],[f526]) ).
tcf(c_182,plain,
op1(op1(e12,e14),e11) = op1(e12,op1(e14,e11)),
inference(cnf_transformation,[],[f518]) ).
tcf(c_183,plain,
op1(op1(e12,e14),e12) = op1(e12,op1(e14,e12)),
inference(cnf_transformation,[],[f517]) ).
tcf(c_186,plain,
op1(op1(e12,e14),e15) = op1(e12,op1(e14,e15)),
inference(cnf_transformation,[],[f514]) ).
tcf(c_187,plain,
op1(op1(e12,e15),e10) = op1(e12,op1(e15,e10)),
inference(cnf_transformation,[],[f513]) ).
tcf(c_188,plain,
op1(op1(e12,e15),e11) = op1(e12,op1(e15,e11)),
inference(cnf_transformation,[],[f512]) ).
tcf(c_189,plain,
op1(op1(e12,e15),e12) = op1(e12,op1(e15,e12)),
inference(cnf_transformation,[],[f511]) ).
tcf(c_191,plain,
op1(op1(e12,e15),e14) = op1(e12,op1(e15,e14)),
inference(cnf_transformation,[],[f509]) ).
tcf(c_206,plain,
op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)),
inference(cnf_transformation,[],[f494]) ).
tcf(c_207,plain,
op1(op1(e13,e12),e12) = op1(e13,op1(e12,e12)),
inference(cnf_transformation,[],[f493]) ).
tcf(c_209,plain,
op1(op1(e13,e12),e14) = op1(e13,op1(e12,e14)),
inference(cnf_transformation,[],[f491]) ).
tcf(c_211,plain,
op1(op1(e13,e13),e10) = op1(e13,op1(e13,e10)),
inference(cnf_transformation,[],[f489]) ).
tcf(c_212,plain,
op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11)),
inference(cnf_transformation,[],[f488]) ).
tcf(c_213,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(cnf_transformation,[],[f487]) ).
tcf(c_214,plain,
op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f486]) ).
tcf(c_216,plain,
op1(op1(e13,e13),e15) = op1(e13,op1(e13,e15)),
inference(cnf_transformation,[],[f484]) ).
tcf(c_227,plain,
op1(op1(e13,e15),e14) = op1(e13,op1(e15,e14)),
inference(cnf_transformation,[],[f473]) ).
tcf(c_230,plain,
op1(op1(e14,e10),e11) = op1(e14,op1(e10,e11)),
inference(cnf_transformation,[],[f470]) ).
tcf(c_242,plain,
op1(op1(e14,e12),e11) = op1(e14,op1(e12,e11)),
inference(cnf_transformation,[],[f458]) ).
tcf(c_243,plain,
op1(op1(e14,e12),e12) = op1(e14,op1(e12,e12)),
inference(cnf_transformation,[],[f457]) ).
tcf(c_253,plain,
op1(op1(e14,e14),e10) = op1(e14,op1(e14,e10)),
inference(cnf_transformation,[],[f447]) ).
tcf(c_254,plain,
op1(op1(e14,e14),e11) = op1(e14,op1(e14,e11)),
inference(cnf_transformation,[],[f446]) ).
tcf(c_255,plain,
op1(op1(e14,e14),e12) = op1(e14,op1(e14,e12)),
inference(cnf_transformation,[],[f445]) ).
tcf(c_259,plain,
op1(op1(e14,e15),e10) = op1(e14,op1(e15,e10)),
inference(cnf_transformation,[],[f441]) ).
tcf(c_260,plain,
op1(op1(e14,e15),e11) = op1(e14,op1(e15,e11)),
inference(cnf_transformation,[],[f440]) ).
tcf(c_261,plain,
op1(op1(e14,e15),e12) = op1(e14,op1(e15,e12)),
inference(cnf_transformation,[],[f439]) ).
tcf(c_263,plain,
op1(op1(e14,e15),e14) = op1(e14,op1(e15,e14)),
inference(cnf_transformation,[],[f437]) ).
tcf(c_266,plain,
op1(op1(e15,e10),e11) = op1(e15,op1(e10,e11)),
inference(cnf_transformation,[],[f434]) ).
tcf(c_267,plain,
op1(op1(e15,e10),e12) = op1(e15,op1(e10,e12)),
inference(cnf_transformation,[],[f433]) ).
tcf(c_270,plain,
op1(op1(e15,e10),e15) = op1(e15,op1(e10,e15)),
inference(cnf_transformation,[],[f430]) ).
tcf(c_271,plain,
op1(op1(e15,e11),e10) = op1(e15,op1(e11,e10)),
inference(cnf_transformation,[],[f429]) ).
tcf(c_272,plain,
op1(op1(e15,e11),e11) = op1(e15,op1(e11,e11)),
inference(cnf_transformation,[],[f428]) ).
tcf(c_273,plain,
op1(op1(e15,e11),e12) = op1(e15,op1(e11,e12)),
inference(cnf_transformation,[],[f427]) ).
tcf(c_275,plain,
op1(op1(e15,e11),e14) = op1(e15,op1(e11,e14)),
inference(cnf_transformation,[],[f425]) ).
tcf(c_276,plain,
op1(op1(e15,e11),e15) = op1(e15,op1(e11,e15)),
inference(cnf_transformation,[],[f424]) ).
tcf(c_277,plain,
op1(op1(e15,e12),e10) = op1(e15,op1(e12,e10)),
inference(cnf_transformation,[],[f423]) ).
tcf(c_278,plain,
op1(op1(e15,e12),e11) = op1(e15,op1(e12,e11)),
inference(cnf_transformation,[],[f422]) ).
tcf(c_279,plain,
op1(op1(e15,e12),e12) = op1(e15,op1(e12,e12)),
inference(cnf_transformation,[],[f421]) ).
tcf(c_281,plain,
op1(op1(e15,e12),e14) = op1(e15,op1(e12,e14)),
inference(cnf_transformation,[],[f419]) ).
tcf(c_289,plain,
op1(op1(e15,e14),e10) = op1(e15,op1(e14,e10)),
inference(cnf_transformation,[],[f411]) ).
tcf(c_290,plain,
op1(op1(e15,e14),e11) = op1(e15,op1(e14,e11)),
inference(cnf_transformation,[],[f410]) ).
tcf(c_291,plain,
op1(op1(e15,e14),e12) = op1(e15,op1(e14,e12)),
inference(cnf_transformation,[],[f409]) ).
tcf(c_292,plain,
op1(op1(e15,e14),e13) = op1(e15,op1(e14,e13)),
inference(cnf_transformation,[],[f408]) ).
tcf(c_294,plain,
op1(op1(e15,e14),e15) = op1(e15,op1(e14,e15)),
inference(cnf_transformation,[],[f406]) ).
tcf(c_300,plain,
op1(op1(e15,e15),e15) = op1(e15,op1(e15,e15)),
inference(cnf_transformation,[],[f400]) ).
tcf(c_337,plain,
( ( op2(e20,e25) = e25 )
| ( op2(e20,e25) = e24 )
| ( op2(e20,e25) = e23 )
| ( op2(e20,e25) = e22 )
| ( op2(e20,e25) = e21 )
| ( op2(e20,e25) = e20 ) ),
inference(cnf_transformation,[],[f677]) ).
tcf(c_342,plain,
( ( op2(e21,e24) = e25 )
| ( op2(e21,e24) = e24 )
| ( op2(e21,e24) = e23 )
| ( op2(e21,e24) = e22 )
| ( op2(e21,e24) = e21 )
| ( op2(e21,e24) = e20 ) ),
inference(cnf_transformation,[],[f672]) ).
tcf(c_345,plain,
( ( op2(e22,e21) = e25 )
| ( op2(e22,e21) = e24 )
| ( op2(e22,e21) = e23 )
| ( op2(e22,e21) = e22 )
| ( op2(e22,e21) = e21 )
| ( op2(e22,e21) = e20 ) ),
inference(cnf_transformation,[],[f669]) ).
tcf(c_351,plain,
( ( op2(e23,e21) = e25 )
| ( op2(e23,e21) = e24 )
| ( op2(e23,e21) = e23 )
| ( op2(e23,e21) = e22 )
| ( op2(e23,e21) = e21 )
| ( op2(e23,e21) = e20 ) ),
inference(cnf_transformation,[],[f663]) ).
tcf(c_352,plain,
( ( op2(e23,e22) = e25 )
| ( op2(e23,e22) = e24 )
| ( op2(e23,e22) = e23 )
| ( op2(e23,e22) = e22 )
| ( op2(e23,e22) = e21 )
| ( op2(e23,e22) = e20 ) ),
inference(cnf_transformation,[],[f662]) ).
tcf(c_355,plain,
( ( op2(e23,e25) = e25 )
| ( op2(e23,e25) = e24 )
| ( op2(e23,e25) = e23 )
| ( op2(e23,e25) = e22 )
| ( op2(e23,e25) = e21 )
| ( op2(e23,e25) = e20 ) ),
inference(cnf_transformation,[],[f659]) ).
tcf(c_357,plain,
( ( op2(e24,e21) = e25 )
| ( op2(e24,e21) = e24 )
| ( op2(e24,e21) = e23 )
| ( op2(e24,e21) = e22 )
| ( op2(e24,e21) = e21 )
| ( op2(e24,e21) = e20 ) ),
inference(cnf_transformation,[],[f657]) ).
tcf(c_358,plain,
( ( op2(e24,e22) = e25 )
| ( op2(e24,e22) = e24 )
| ( op2(e24,e22) = e23 )
| ( op2(e24,e22) = e22 )
| ( op2(e24,e22) = e21 )
| ( op2(e24,e22) = e20 ) ),
inference(cnf_transformation,[],[f656]) ).
tcf(c_362,plain,
( ( op2(e25,e20) = e25 )
| ( op2(e25,e20) = e24 )
| ( op2(e25,e20) = e23 )
| ( op2(e25,e20) = e22 )
| ( op2(e25,e20) = e21 )
| ( op2(e25,e20) = e20 ) ),
inference(cnf_transformation,[],[f652]) ).
tcf(c_364,plain,
( ( op2(e25,e22) = e25 )
| ( op2(e25,e22) = e24 )
| ( op2(e25,e22) = e23 )
| ( op2(e25,e22) = e22 )
| ( op2(e25,e22) = e21 )
| ( op2(e25,e22) = e20 ) ),
inference(cnf_transformation,[],[f650]) ).
tcf(c_393,plain,
op2(op2(e20,e24),e21) = op2(e20,op2(e24,e21)),
inference(cnf_transformation,[],[f873]) ).
tcf(c_411,plain,
op2(op2(e21,e21),e21) = op2(e21,op2(e21,e21)),
inference(cnf_transformation,[],[f855]) ).
tcf(c_412,plain,
op2(op2(e21,e21),e22) = op2(e21,op2(e21,e22)),
inference(cnf_transformation,[],[f854]) ).
tcf(c_413,plain,
op2(op2(e21,e21),e23) = op2(e21,op2(e21,e23)),
inference(cnf_transformation,[],[f853]) ).
tcf(c_414,plain,
op2(op2(e21,e21),e24) = op2(e21,op2(e21,e24)),
inference(cnf_transformation,[],[f852]) ).
tcf(c_419,plain,
op2(op2(e21,e22),e23) = op2(e21,op2(e22,e23)),
inference(cnf_transformation,[],[f847]) ).
tcf(c_448,plain,
op2(op2(e22,e21),e22) = op2(e22,op2(e21,e22)),
inference(cnf_transformation,[],[f818]) ).
tcf(c_452,plain,
op2(op2(e22,e22),e20) = op2(e22,op2(e22,e20)),
inference(cnf_transformation,[],[f814]) ).
tcf(c_454,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f812]) ).
tcf(c_461,plain,
op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)),
inference(cnf_transformation,[],[f805]) ).
tcf(c_469,plain,
op2(op2(e22,e24),e25) = op2(e22,op2(e24,e25)),
inference(cnf_transformation,[],[f797]) ).
tcf(c_478,plain,
op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22)),
inference(cnf_transformation,[],[f788]) ).
tcf(c_485,plain,
op2(op2(e23,e21),e23) = op2(e23,op2(e21,e23)),
inference(cnf_transformation,[],[f781]) ).
tcf(c_488,plain,
op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20)),
inference(cnf_transformation,[],[f778]) ).
tcf(c_489,plain,
op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21)),
inference(cnf_transformation,[],[f777]) ).
tcf(c_490,plain,
op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22)),
inference(cnf_transformation,[],[f776]) ).
tcf(c_492,plain,
op2(op2(e23,e22),e24) = op2(e23,op2(e22,e24)),
inference(cnf_transformation,[],[f774]) ).
tcf(c_494,plain,
op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20)),
inference(cnf_transformation,[],[f772]) ).
tcf(c_495,plain,
op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)),
inference(cnf_transformation,[],[f771]) ).
tcf(c_496,plain,
op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)),
inference(cnf_transformation,[],[f770]) ).
tcf(c_497,plain,
op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f769]) ).
tcf(c_499,plain,
op2(op2(e23,e23),e25) = op2(e23,op2(e23,e25)),
inference(cnf_transformation,[],[f767]) ).
tcf(c_502,plain,
op2(op2(e23,e24),e22) = op2(e23,op2(e24,e22)),
inference(cnf_transformation,[],[f764]) ).
tcf(c_510,plain,
op2(op2(e23,e25),e24) = op2(e23,op2(e25,e24)),
inference(cnf_transformation,[],[f756]) ).
tcf(c_526,plain,
op2(op2(e24,e22),e22) = op2(e24,op2(e22,e22)),
inference(cnf_transformation,[],[f740]) ).
tcf(c_532,plain,
op2(op2(e24,e23),e22) = op2(e24,op2(e23,e22)),
inference(cnf_transformation,[],[f734]) ).
tcf(c_554,plain,
op2(op2(e25,e21),e20) = op2(e25,op2(e21,e20)),
inference(cnf_transformation,[],[f712]) ).
tcf(c_555,plain,
op2(op2(e25,e21),e21) = op2(e25,op2(e21,e21)),
inference(cnf_transformation,[],[f711]) ).
tcf(c_556,plain,
op2(op2(e25,e21),e22) = op2(e25,op2(e21,e22)),
inference(cnf_transformation,[],[f710]) ).
tcf(c_564,plain,
op2(op2(e25,e22),e24) = op2(e25,op2(e22,e24)),
inference(cnf_transformation,[],[f702]) ).
tcf(c_567,plain,
op2(op2(e25,e23),e21) = op2(e25,op2(e23,e21)),
inference(cnf_transformation,[],[f699]) ).
tcf(c_569,plain,
op2(op2(e25,e23),e23) = op2(e25,op2(e23,e23)),
inference(cnf_transformation,[],[f697]) ).
tcf(c_570,plain,
op2(op2(e25,e23),e24) = op2(e25,op2(e23,e24)),
inference(cnf_transformation,[],[f696]) ).
tcf(c_573,plain,
op2(op2(e25,e24),e21) = op2(e25,op2(e24,e21)),
inference(cnf_transformation,[],[f693]) ).
tcf(c_574,plain,
op2(op2(e25,e24),e22) = op2(e25,op2(e24,e22)),
inference(cnf_transformation,[],[f692]) ).
tcf(c_575,plain,
op2(op2(e25,e24),e23) = op2(e25,op2(e24,e23)),
inference(cnf_transformation,[],[f691]) ).
tcf(c_577,plain,
op2(op2(e25,e24),e25) = op2(e25,op2(e24,e25)),
inference(cnf_transformation,[],[f689]) ).
tcf(c_582,plain,
op2(op2(e25,e25),e24) = op2(e25,op2(e25,e24)),
inference(cnf_transformation,[],[f684]) ).
tcf(c_719,negated_conjecture,
op1(e10,e10) != op1(e11,e10),
inference(cnf_transformation,[],[f1225]) ).
tcf(c_724,negated_conjecture,
op1(e11,e10) != op1(e12,e10),
inference(cnf_transformation,[],[f1220]) ).
tcf(c_725,negated_conjecture,
op1(e11,e10) != op1(e13,e10),
inference(cnf_transformation,[],[f1219]) ).
tcf(c_726,negated_conjecture,
op1(e11,e10) != op1(e14,e10),
inference(cnf_transformation,[],[f1218]) ).
tcf(c_727,negated_conjecture,
op1(e11,e10) != op1(e15,e10),
inference(cnf_transformation,[],[f1217]) ).
tcf(c_729,negated_conjecture,
op1(e12,e10) != op1(e14,e10),
inference(cnf_transformation,[],[f1215]) ).
tcf(c_734,negated_conjecture,
op1(e10,e11) != op1(e11,e11),
inference(cnf_transformation,[],[f1210]) ).
tcf(c_735,negated_conjecture,
op1(e10,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f1209]) ).
tcf(c_736,negated_conjecture,
op1(e10,e11) != op1(e13,e11),
inference(cnf_transformation,[],[f1208]) ).
tcf(c_737,negated_conjecture,
op1(e10,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f1207]) ).
tcf(c_738,negated_conjecture,
op1(e10,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f1206]) ).
tcf(c_739,negated_conjecture,
op1(e11,e11) != op1(e12,e11),
inference(cnf_transformation,[],[f1205]) ).
tcf(c_741,negated_conjecture,
op1(e11,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f1203]) ).
tcf(c_742,negated_conjecture,
op1(e11,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f1202]) ).
tcf(c_744,negated_conjecture,
op1(e12,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f1200]) ).
tcf(c_745,negated_conjecture,
op1(e12,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f1199]) ).
tcf(c_746,negated_conjecture,
op1(e13,e11) != op1(e14,e11),
inference(cnf_transformation,[],[f1198]) ).
tcf(c_748,negated_conjecture,
op1(e14,e11) != op1(e15,e11),
inference(cnf_transformation,[],[f1196]) ).
tcf(c_751,negated_conjecture,
op1(e10,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f1193]) ).
tcf(c_758,negated_conjecture,
op1(e12,e12) != op1(e13,e12),
inference(cnf_transformation,[],[f1186]) ).
tcf(c_759,negated_conjecture,
op1(e12,e12) != op1(e14,e12),
inference(cnf_transformation,[],[f1185]) ).
tcf(c_760,negated_conjecture,
op1(e12,e12) != op1(e15,e12),
inference(cnf_transformation,[],[f1184]) ).
tcf(c_761,negated_conjecture,
op1(e13,e12) != op1(e14,e12),
inference(cnf_transformation,[],[f1183]) ).
tcf(c_773,negated_conjecture,
op1(e12,e13) != op1(e13,e13),
inference(cnf_transformation,[],[f1171]) ).
tcf(c_774,negated_conjecture,
op1(e12,e13) != op1(e14,e13),
inference(cnf_transformation,[],[f1170]) ).
tcf(c_776,negated_conjecture,
op1(e13,e13) != op1(e14,e13),
inference(cnf_transformation,[],[f1168]) ).
tcf(c_792,negated_conjecture,
op1(e13,e14) != op1(e15,e14),
inference(cnf_transformation,[],[f1152]) ).
tcf(c_795,negated_conjecture,
op1(e10,e15) != op1(e12,e15),
inference(cnf_transformation,[],[f1149]) ).
tcf(c_797,negated_conjecture,
op1(e10,e15) != op1(e14,e15),
inference(cnf_transformation,[],[f1147]) ).
tcf(c_798,negated_conjecture,
op1(e10,e15) != op1(e15,e15),
inference(cnf_transformation,[],[f1146]) ).
tcf(c_805,negated_conjecture,
op1(e12,e15) != op1(e15,e15),
inference(cnf_transformation,[],[f1139]) ).
tcf(c_808,negated_conjecture,
op1(e14,e15) != op1(e15,e15),
inference(cnf_transformation,[],[f1136]) ).
tcf(c_809,negated_conjecture,
op1(e10,e10) != op1(e10,e11),
inference(cnf_transformation,[],[f1135]) ).
tcf(c_814,negated_conjecture,
op1(e10,e11) != op1(e10,e12),
inference(cnf_transformation,[],[f1130]) ).
tcf(c_816,negated_conjecture,
op1(e10,e11) != op1(e10,e14),
inference(cnf_transformation,[],[f1128]) ).
tcf(c_817,negated_conjecture,
op1(e10,e11) != op1(e10,e15),
inference(cnf_transformation,[],[f1127]) ).
tcf(c_820,negated_conjecture,
op1(e10,e12) != op1(e10,e15),
inference(cnf_transformation,[],[f1124]) ).
tcf(c_823,negated_conjecture,
op1(e10,e14) != op1(e10,e15),
inference(cnf_transformation,[],[f1121]) ).
tcf(c_841,negated_conjecture,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f1103]) ).
tcf(c_844,negated_conjecture,
op1(e12,e11) != op1(e12,e12),
inference(cnf_transformation,[],[f1100]) ).
tcf(c_847,negated_conjecture,
op1(e12,e11) != op1(e12,e15),
inference(cnf_transformation,[],[f1097]) ).
tcf(c_848,negated_conjecture,
op1(e12,e12) != op1(e12,e13),
inference(cnf_transformation,[],[f1096]) ).
tcf(c_849,negated_conjecture,
op1(e12,e12) != op1(e12,e14),
inference(cnf_transformation,[],[f1095]) ).
tcf(c_850,negated_conjecture,
op1(e12,e12) != op1(e12,e15),
inference(cnf_transformation,[],[f1094]) ).
tcf(c_852,negated_conjecture,
op1(e12,e13) != op1(e12,e15),
inference(cnf_transformation,[],[f1092]) ).
tcf(c_860,negated_conjecture,
op1(e13,e11) != op1(e13,e13),
inference(cnf_transformation,[],[f1084]) ).
tcf(c_861,negated_conjecture,
op1(e13,e11) != op1(e13,e14),
inference(cnf_transformation,[],[f1083]) ).
tcf(c_863,negated_conjecture,
op1(e13,e12) != op1(e13,e13),
inference(cnf_transformation,[],[f1081]) ).
tcf(c_869,negated_conjecture,
op1(e14,e10) != op1(e14,e11),
inference(cnf_transformation,[],[f1075]) ).
tcf(c_873,negated_conjecture,
op1(e14,e10) != op1(e14,e15),
inference(cnf_transformation,[],[f1071]) ).
tcf(c_875,negated_conjecture,
op1(e14,e11) != op1(e14,e13),
inference(cnf_transformation,[],[f1069]) ).
tcf(c_877,negated_conjecture,
op1(e14,e11) != op1(e14,e15),
inference(cnf_transformation,[],[f1067]) ).
tcf(c_878,negated_conjecture,
op1(e14,e12) != op1(e14,e13),
inference(cnf_transformation,[],[f1066]) ).
tcf(c_879,negated_conjecture,
op1(e14,e12) != op1(e14,e14),
inference(cnf_transformation,[],[f1065]) ).
tcf(c_880,negated_conjecture,
op1(e14,e12) != op1(e14,e15),
inference(cnf_transformation,[],[f1064]) ).
tcf(c_883,negated_conjecture,
op1(e14,e14) != op1(e14,e15),
inference(cnf_transformation,[],[f1061]) ).
tcf(c_884,negated_conjecture,
op1(e15,e10) != op1(e15,e11),
inference(cnf_transformation,[],[f1060]) ).
tcf(c_885,negated_conjecture,
op1(e15,e10) != op1(e15,e12),
inference(cnf_transformation,[],[f1059]) ).
tcf(c_887,negated_conjecture,
op1(e15,e10) != op1(e15,e14),
inference(cnf_transformation,[],[f1057]) ).
tcf(c_889,negated_conjecture,
op1(e15,e11) != op1(e15,e12),
inference(cnf_transformation,[],[f1055]) ).
tcf(c_892,negated_conjecture,
op1(e15,e11) != op1(e15,e15),
inference(cnf_transformation,[],[f1052]) ).
tcf(c_894,negated_conjecture,
op1(e15,e12) != op1(e15,e14),
inference(cnf_transformation,[],[f1050]) ).
tcf(c_898,negated_conjecture,
op1(e15,e14) != op1(e15,e15),
inference(cnf_transformation,[],[f1046]) ).
tcf(c_903,negated_conjecture,
op2(e20,e20) != op2(e25,e20),
inference(cnf_transformation,[],[f1401]) ).
tcf(c_907,negated_conjecture,
op2(e21,e20) != op2(e25,e20),
inference(cnf_transformation,[],[f1397]) ).
tcf(c_913,negated_conjecture,
op2(e24,e20) != op2(e25,e20),
inference(cnf_transformation,[],[f1391]) ).
tcf(c_915,negated_conjecture,
op2(e20,e21) != op2(e22,e21),
inference(cnf_transformation,[],[f1389]) ).
tcf(c_917,negated_conjecture,
op2(e20,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f1387]) ).
tcf(c_921,negated_conjecture,
op2(e21,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f1383]) ).
tcf(c_923,negated_conjecture,
op2(e22,e21) != op2(e23,e21),
inference(cnf_transformation,[],[f1381]) ).
tcf(c_925,negated_conjecture,
op2(e22,e21) != op2(e25,e21),
inference(cnf_transformation,[],[f1379]) ).
tcf(c_926,negated_conjecture,
op2(e23,e21) != op2(e24,e21),
inference(cnf_transformation,[],[f1378]) ).
tcf(c_927,negated_conjecture,
op2(e23,e21) != op2(e25,e21),
inference(cnf_transformation,[],[f1377]) ).
tcf(c_928,negated_conjecture,
op2(e24,e21) != op2(e25,e21),
inference(cnf_transformation,[],[f1376]) ).
tcf(c_938,negated_conjecture,
op2(e22,e22) != op2(e23,e22),
inference(cnf_transformation,[],[f1366]) ).
tcf(c_939,negated_conjecture,
op2(e22,e22) != op2(e24,e22),
inference(cnf_transformation,[],[f1365]) ).
tcf(c_940,negated_conjecture,
op2(e22,e22) != op2(e25,e22),
inference(cnf_transformation,[],[f1364]) ).
tcf(c_941,negated_conjecture,
op2(e23,e22) != op2(e24,e22),
inference(cnf_transformation,[],[f1363]) ).
tcf(c_942,negated_conjecture,
op2(e23,e22) != op2(e25,e22),
inference(cnf_transformation,[],[f1362]) ).
tcf(c_943,negated_conjecture,
op2(e24,e22) != op2(e25,e22),
inference(cnf_transformation,[],[f1361]) ).
tcf(c_953,negated_conjecture,
op2(e22,e23) != op2(e23,e23),
inference(cnf_transformation,[],[f1351]) ).
tcf(c_967,negated_conjecture,
op2(e21,e24) != op2(e25,e24),
inference(cnf_transformation,[],[f1337]) ).
tcf(c_987,negated_conjecture,
op2(e23,e25) != op2(e25,e25),
inference(cnf_transformation,[],[f1317]) ).
tcf(c_993,negated_conjecture,
op2(e20,e20) != op2(e20,e25),
inference(cnf_transformation,[],[f1311]) ).
tcf(c_997,negated_conjecture,
op2(e20,e21) != op2(e20,e25),
inference(cnf_transformation,[],[f1307]) ).
tcf(c_1000,negated_conjecture,
op2(e20,e22) != op2(e20,e25),
inference(cnf_transformation,[],[f1304]) ).
tcf(c_1002,negated_conjecture,
op2(e20,e23) != op2(e20,e25),
inference(cnf_transformation,[],[f1302]) ).
tcf(c_1003,negated_conjecture,
op2(e20,e24) != op2(e20,e25),
inference(cnf_transformation,[],[f1301]) ).
tcf(c_1007,negated_conjecture,
op2(e21,e20) != op2(e21,e24),
inference(cnf_transformation,[],[f1297]) ).
tcf(c_1014,negated_conjecture,
op2(e21,e22) != op2(e21,e24),
inference(cnf_transformation,[],[f1290]) ).
tcf(c_1019,negated_conjecture,
op2(e22,e20) != op2(e22,e21),
inference(cnf_transformation,[],[f1285]) ).
tcf(c_1024,negated_conjecture,
op2(e22,e21) != op2(e22,e22),
inference(cnf_transformation,[],[f1280]) ).
tcf(c_1028,negated_conjecture,
op2(e22,e22) != op2(e22,e23),
inference(cnf_transformation,[],[f1276]) ).
tcf(c_1035,negated_conjecture,
op2(e23,e20) != op2(e23,e22),
inference(cnf_transformation,[],[f1269]) ).
tcf(c_1036,negated_conjecture,
op2(e23,e20) != op2(e23,e23),
inference(cnf_transformation,[],[f1268]) ).
tcf(c_1038,negated_conjecture,
op2(e23,e20) != op2(e23,e25),
inference(cnf_transformation,[],[f1266]) ).
tcf(c_1039,negated_conjecture,
op2(e23,e21) != op2(e23,e22),
inference(cnf_transformation,[],[f1265]) ).
tcf(c_1040,negated_conjecture,
op2(e23,e21) != op2(e23,e23),
inference(cnf_transformation,[],[f1264]) ).
tcf(c_1043,negated_conjecture,
op2(e23,e22) != op2(e23,e23),
inference(cnf_transformation,[],[f1261]) ).
tcf(c_1044,negated_conjecture,
op2(e23,e22) != op2(e23,e24),
inference(cnf_transformation,[],[f1260]) ).
tcf(c_1045,negated_conjecture,
op2(e23,e22) != op2(e23,e25),
inference(cnf_transformation,[],[f1259]) ).
tcf(c_1047,negated_conjecture,
op2(e23,e23) != op2(e23,e25),
inference(cnf_transformation,[],[f1257]) ).
tcf(c_1049,negated_conjecture,
op2(e24,e20) != op2(e24,e21),
inference(cnf_transformation,[],[f1255]) ).
tcf(c_1054,negated_conjecture,
op2(e24,e21) != op2(e24,e22),
inference(cnf_transformation,[],[f1250]) ).
tcf(c_1064,negated_conjecture,
op2(e25,e20) != op2(e25,e21),
inference(cnf_transformation,[],[f1240]) ).
tcf(c_1067,negated_conjecture,
op2(e25,e20) != op2(e25,e24),
inference(cnf_transformation,[],[f1237]) ).
tcf(c_1069,negated_conjecture,
op2(e25,e21) != op2(e25,e22),
inference(cnf_transformation,[],[f1235]) ).
tcf(c_1074,negated_conjecture,
op2(e25,e22) != op2(e25,e24),
inference(cnf_transformation,[],[f1230]) ).
tcf(c_1081,negated_conjecture,
e10 != e13,
inference(cnf_transformation,[],[f1418]) ).
tcf(c_1145,negated_conjecture,
( ( op1(e15,e15) != op1(e15,e15) )
| ( op1(e14,e15) != op1(e15,e14) )
| ( op1(e14,e14) != op1(e14,e14) )
| ( op1(e13,e15) != op1(e15,e13) )
| ( op1(e13,e14) != op1(e14,e13) )
| ( op1(e13,e13) != op1(e13,e13) )
| ( op1(e12,e15) != op1(e15,e12) )
| ( op1(e12,e14) != op1(e14,e12) )
| ( op1(e12,e13) != op1(e13,e12) )
| ( op1(e12,e12) != op1(e12,e12) )
| ( op1(e11,e15) != op1(e15,e11) )
| ( op1(e11,e14) != op1(e14,e11) )
| ( op1(e11,e13) != op1(e13,e11) )
| ( op1(e11,e12) != op1(e12,e11) )
| ( op1(e11,e11) != op1(e11,e11) )
| ( op1(e10,e15) != op1(e15,e10) )
| ( op1(e10,e14) != op1(e14,e10) )
| ( op1(e10,e13) != op1(e13,e10) )
| ( op1(e10,e12) != op1(e12,e10) )
| ( op1(e10,e11) != op1(e11,e10) )
| ( op1(e10,e10) != op1(e10,e10) ) ),
inference(cnf_transformation,[],[f2742]) ).
tcf(c_1147,plain,
op1(op1(e15,op1(op1(e15,e11),op1(e15,e11))),op1(e15,op1(op1(e15,e11),op1(e15,e11)))) = e10,
inference(cnf_transformation,[],[f1477]) ).
tcf(c_1148,plain,
op1(e15,op1(op1(e15,e11),op1(e15,e11))) = e12,
inference(cnf_transformation,[],[f1476]) ).
tcf(c_1149,plain,
op1(e15,e11) = e13,
inference(cnf_transformation,[],[f1475]) ).
tcf(c_1150,plain,
op1(op1(e15,e11),op1(e15,e11)) = e14,
inference(cnf_transformation,[],[f1474]) ).
tcf(c_1151,plain,
op2(op2(e25,op2(op2(e25,e21),op2(e25,e21))),op2(e25,op2(op2(e25,e21),op2(e25,e21)))) = e20,
inference(cnf_transformation,[],[f1481]) ).
tcf(c_1152,plain,
op2(e25,op2(op2(e25,e21),op2(e25,e21))) = e22,
inference(cnf_transformation,[],[f1480]) ).
tcf(c_1153,plain,
op2(e25,e21) = e23,
inference(cnf_transformation,[],[f1479]) ).
tcf(c_1154,plain,
op2(op2(e25,e21),op2(e25,e21)) = e24,
inference(cnf_transformation,[],[f1478]) ).
tcf(c_1171,plain,
op2(e23,e20) = h3(e13),
inference(cnf_transformation,[],[f1495]) ).
tcf(c_1183,plain,
op2(e25,e20) = h5(e13),
inference(cnf_transformation,[],[f1507]) ).
tcf(c_1195,plain,
op2(e22,e21) = h7(e13),
inference(cnf_transformation,[],[f1519]) ).
tcf(c_1201,plain,
op2(e23,e21) = h8(e13),
inference(cnf_transformation,[],[f1525]) ).
tcf(c_1207,plain,
op2(e24,e21) = h9(e13),
inference(cnf_transformation,[],[f1531]) ).
tcf(c_1209,plain,
h10(e11) = e21,
inference(cnf_transformation,[],[f1541]) ).
tcf(c_1210,plain,
h10(e15) = e25,
inference(cnf_transformation,[],[f1540]) ).
tcf(c_1211,plain,
op2(op2(e25,op2(op2(e25,e21),op2(e25,e21))),op2(e25,op2(op2(e25,e21),op2(e25,e21)))) = h10(e10),
inference(cnf_transformation,[],[f1539]) ).
tcf(c_1212,plain,
op2(e25,op2(op2(e25,e21),op2(e25,e21))) = h10(e12),
inference(cnf_transformation,[],[f1538]) ).
tcf(c_1213,plain,
op2(e25,e21) = h10(e13),
inference(cnf_transformation,[],[f1537]) ).
tcf(c_1214,plain,
op2(op2(e25,e21),op2(e25,e21)) = h10(e14),
inference(cnf_transformation,[],[f1536]) ).
tcf(c_1225,plain,
op2(e21,e22) = h12(e13),
inference(cnf_transformation,[],[f1549]) ).
tcf(c_1231,plain,
op2(e23,e22) = h13(e13),
inference(cnf_transformation,[],[f1555]) ).
tcf(c_1237,plain,
op2(e24,e22) = h14(e13),
inference(cnf_transformation,[],[f1561]) ).
tcf(c_1243,plain,
op2(e25,e22) = h15(e13),
inference(cnf_transformation,[],[f1567]) ).
tcf(c_1255,plain,
op2(e21,e23) = h17(e13),
inference(cnf_transformation,[],[f1579]) ).
tcf(c_1261,plain,
op2(e22,e23) = h18(e13),
inference(cnf_transformation,[],[f1585]) ).
tcf(c_1267,plain,
op2(e24,e23) = h19(e13),
inference(cnf_transformation,[],[f1591]) ).
tcf(c_1273,plain,
op2(e25,e23) = h20(e13),
inference(cnf_transformation,[],[f1597]) ).
tcf(c_1285,plain,
op2(e21,e24) = h22(e13),
inference(cnf_transformation,[],[f1609]) ).
tcf(c_1291,plain,
op2(e22,e24) = h23(e13),
inference(cnf_transformation,[],[f1615]) ).
tcf(c_1309,plain,
op2(e20,e25) = h26(e13),
inference(cnf_transformation,[],[f1633]) ).
tcf(c_1315,plain,
op2(e21,e25) = h27(e13),
inference(cnf_transformation,[],[f1639]) ).
tcf(c_1321,plain,
op2(e22,e25) = h28(e13),
inference(cnf_transformation,[],[f1645]) ).
tcf(c_1327,plain,
op2(e23,e25) = h29(e13),
inference(cnf_transformation,[],[f1651]) ).
tcf(c_1333,plain,
op2(e24,e25) = h30(e13),
inference(cnf_transformation,[],[f1657]) ).
tcf(c_1606,negated_conjecture,
( ~ sP104
| ( h10(e11) != e21 ) ),
inference(cnf_transformation,[],[f1936]) ).
tcf(c_1613,negated_conjecture,
( ~ sP103
| ( h10(e12) != e22 ) ),
inference(cnf_transformation,[],[f1941]) ).
tcf(c_1620,negated_conjecture,
( ~ sP102
| ( h10(e13) != e23 ) ),
inference(cnf_transformation,[],[f1946]) ).
tcf(c_1627,negated_conjecture,
( ~ sP101
| ( h10(e14) != e24 ) ),
inference(cnf_transformation,[],[f1951]) ).
tcf(c_1634,negated_conjecture,
( ~ sP100
| ( h10(e15) != e25 ) ),
inference(cnf_transformation,[],[f1956]) ).
tcf(c_2289,negated_conjecture,
( sP100
| sP101
| sP102
| sP103
| sP104
| ( h10(e10) != e20 )
| ( op2(h10(e15),h10(e15)) != h10(op1(e15,e15)) )
| ( op2(h10(e15),h10(e14)) != h10(op1(e15,e14)) )
| ( op2(h10(e15),h10(e13)) != h10(op1(e15,e13)) )
| ( op2(h10(e15),h10(e12)) != h10(op1(e15,e12)) )
| ( op2(h10(e15),h10(e11)) != h10(op1(e15,e11)) )
| ( op2(h10(e15),h10(e10)) != h10(op1(e15,e10)) )
| ( op2(h10(e14),h10(e15)) != h10(op1(e14,e15)) )
| ( 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(e15)) != h10(op1(e13,e15)) )
| ( 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(e15)) != h10(op1(e12,e15)) )
| ( 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(e15)) != h10(op1(e11,e15)) )
| ( 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(e15)) != h10(op1(e10,e15)) )
| ( 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,[],[f2687]) ).
tcf(c_3020,plain,
( ( op1(e14,e15) != op1(e15,e14) )
| ( op1(e13,e15) != op1(e15,e13) )
| ( op1(e13,e14) != op1(e14,e13) )
| ( op1(e12,e15) != op1(e15,e12) )
| ( op1(e12,e14) != op1(e14,e12) )
| ( op1(e12,e13) != op1(e13,e12) )
| ( op1(e11,e15) != op1(e15,e11) )
| ( op1(e11,e14) != op1(e14,e11) )
| ( op1(e11,e13) != op1(e13,e11) )
| ( op1(e11,e12) != op1(e12,e11) )
| ( op1(e10,e15) != op1(e15,e10) )
| ( op1(e10,e14) != op1(e14,e10) )
| ( op1(e10,e13) != op1(e13,e10) )
| ( op1(e10,e12) != op1(e12,e10) )
| ( op1(e10,e11) != op1(e11,e10) ) ),
inference(equality_resolution_simp,[status(thm)],[c_1145]) ).
tcf(c_3271,plain,
( ( h10(e10) != e20 )
| ( op2(h10(e15),h10(e15)) != h10(op1(e15,e15)) )
| ( op2(h10(e15),h10(e14)) != h10(op1(e15,e14)) )
| ( op2(h10(e15),h10(e13)) != h10(op1(e15,e13)) )
| ( op2(h10(e15),h10(e12)) != h10(op1(e15,e12)) )
| ( op2(h10(e15),h10(e11)) != h10(op1(e15,e11)) )
| ( op2(h10(e15),h10(e10)) != h10(op1(e15,e10)) )
| ( op2(h10(e14),h10(e15)) != h10(op1(e14,e15)) )
| ( 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(e15)) != h10(op1(e13,e15)) )
| ( 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(e15)) != h10(op1(e12,e15)) )
| ( 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(e15)) != h10(op1(e11,e15)) )
| ( 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(e15)) != h10(op1(e10,e15)) )
| ( 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)) )
| sP103
| sP102
| sP101 ),
inference(global_subsumption_just,[status(thm)],[c_2289,c_1210,c_1209,c_1634,c_1606,c_2289]) ).
tcf(c_3272,negated_conjecture,
( sP101
| sP102
| sP103
| ( h10(e10) != e20 )
| ( op2(h10(e15),h10(e15)) != h10(op1(e15,e15)) )
| ( op2(h10(e15),h10(e14)) != h10(op1(e15,e14)) )
| ( op2(h10(e15),h10(e13)) != h10(op1(e15,e13)) )
| ( op2(h10(e15),h10(e12)) != h10(op1(e15,e12)) )
| ( op2(h10(e15),h10(e11)) != h10(op1(e15,e11)) )
| ( op2(h10(e15),h10(e10)) != h10(op1(e15,e10)) )
| ( op2(h10(e14),h10(e15)) != h10(op1(e14,e15)) )
| ( 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(e15)) != h10(op1(e13,e15)) )
| ( 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(e15)) != h10(op1(e12,e15)) )
| ( 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(e15)) != h10(op1(e11,e15)) )
| ( 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(e15)) != h10(op1(e10,e15)) )
| ( 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(renaming,[status(thm)],[c_3271]) ).
tcf(c_3453,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_3272,c_3020,c_1627,c_1620,c_1613,c_1333,c_1327,c_1321,c_1315,c_1309,c_1291,c_1285,c_1273,c_1267,c_1261,c_1255,c_1243,c_1237,c_1231,c_1225,c_1214,c_1213,c_1212,c_1211,c_1210,c_1209,c_1207,c_1201,c_1195,c_1183,c_1171,c_1154,c_1153,c_1152,c_1151,c_1150,c_1149,c_1148,c_1147,c_1081,c_1074,c_1069,c_1067,c_1064,c_1054,c_1049,c_1047,c_1045,c_1044,c_1043,c_1040,c_1039,c_1038,c_1036,c_1035,c_1028,c_1024,c_1019,c_1014,c_1007,c_1003,c_1002,c_1000,c_997,c_993,c_987,c_967,c_953,c_943,c_942,c_941,c_940,c_939,c_938,c_928,c_927,c_926,c_925,c_923,c_921,c_917,c_915,c_913,c_907,c_903,c_898,c_894,c_892,c_889,c_887,c_885,c_884,c_883,c_880,c_879,c_878,c_877,c_875,c_873,c_869,c_863,c_861,c_860,c_852,c_850,c_849,c_848,c_847,c_844,c_841,c_823,c_820,c_817,c_816,c_814,c_809,c_808,c_805,c_798,c_797,c_795,c_792,c_776,c_774,c_773,c_761,c_760,c_759,c_758,c_751,c_748,c_746,c_745,c_744,c_742,c_741,c_739,c_738,c_737,c_736,c_735,c_734,c_729,c_727,c_726,c_725,c_724,c_719,c_582,c_577,c_575,c_574,c_573,c_570,c_569,c_567,c_564,c_556,c_555,c_554,c_532,c_526,c_510,c_502,c_499,c_497,c_496,c_495,c_494,c_492,c_490,c_489,c_488,c_485,c_478,c_469,c_461,c_454,c_452,c_448,c_419,c_414,c_413,c_412,c_411,c_393,c_364,c_362,c_358,c_357,c_355,c_352,c_351,c_345,c_342,c_337,c_300,c_294,c_292,c_291,c_290,c_289,c_281,c_279,c_278,c_277,c_276,c_275,c_273,c_272,c_271,c_270,c_267,c_266,c_263,c_261,c_260,c_259,c_255,c_254,c_253,c_243,c_242,c_230,c_227,c_216,c_214,c_213,c_212,c_211,c_209,c_207,c_206,c_191,c_189,c_188,c_187,c_186,c_183,c_182,c_174,c_173,c_171,c_170,c_169,c_165,c_158,c_157,c_152,c_147,c_131,c_129,c_119,c_116,c_115,c_113,c_106,c_98,c_97,c_81,c_79,c_78,c_76,c_74,c_69,c_64,c_62,c_56,c_55,c_54,c_50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG027+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/5.38 % Computer : n010.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Fri Sep 25 04:33:51 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/5.42 Running first-order theorem proving
% 0.16/5.42 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.16/5.43
% 0.16/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.16/5.43
% 0.16/5.43 % Detected problem language: tptp
% 0.16/5.45 % Proving...
% 23.33/8.82 % SZS status Started for theBenchmark.p
% 23.33/8.82 ERROR - "ProverProcess:heur/409474:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 4 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution false --res_forward_subs subset_subsumption --res_forward_subs_resolution true --res_lit_sel pos_max --res_lit_sel_side num_var --res_ordering kbo_pred --res_passive_queue_type priority_queues --res_passive_queues "[[-num_lits];[-conj_symb;-num_symb;+num_symb]]" --res_passive_queues_freq "[15;3]" --res_prop_simpl_given false --res_prop_simpl_new true --res_sim_input true --res_time_limit 202.80 --res_to_prop_solver passive --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/ji94s8sl 2>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/ji94s8sl_error
% 23.33/8.82 ERROR - "ProverProcess:heur/469571:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 6 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3.0 --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 32 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp false --inst_learning_factor 10 --inst_learning_loop_flag true --inst_learning_start 256 --inst_lit_activity_flag true --inst_lit_sel "[+sign;-ground;-non_prol_conj_symb;-num_var]" --inst_lit_sel_side num_lit --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-ground;-epr]]" --inst_passive_queues_freq "[2]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given true --inst_sel_renew solver --inst_solver_calls_frac 0.6939020527068606 --inst_solver_per_active 8 --inst_sos_flag false --inst_start_prop_sim_after_learn 9 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 128 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[DemodLightNormLoopTriv;ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 640 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/jjfswqsi 2>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/jjfswqsi_error
% 23.33/8.82 ERROR - "ProverProcess:heur/381325:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 1 --comb_sup_mult 3 --conj_cone_tolerance 3. --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[Demod;DemodLoopTriv;LightNorm;ACNormalisation]" --sup_full_triv "[]" --sup_fun_splitting true --sup_immed_bw_immed "[]" --sup_immed_bw_main "[SubsumptionRes;UnitSubsAndRes]" --sup_immed_fw_immed "[Subsumption;UnitSubsAndRes;Demod;DemodLoopTriv;LightNorm;DemodLightNormLoopTriv]" --sup_immed_fw_main "[Subsumption;SubsumptionRes;LightNorm;DemodLightNormLoopTriv]" --sup_immed_triv "[PropSubs]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;FwDemod]" --sup_input_bw "[UnitSubsAndRes]" --sup_input_fw "[]" --sup_input_triv "[PropSubs]" --sup_iter_deepening 0 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_symb;-max_atom_input_occur];[+horn];[+bc_imp_inh;+ground;-conj_dist]]" --sup_passive_queues_freq "[3;1;25]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 8 --sup_score sim_d_gen --sup_share_max_num_cl 40 --sup_share_score_frac 0.1 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver active --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/qm2531aa 2>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/qm2531aa_error
% 23.33/8.82 ERROR - "ProverProcess:heur/346297:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref_under "[]" --comb_inst_mult 3 --comb_mode time_based --comb_sup_deep_mult 6 --comb_sup_mult 32 --conj_cone_tolerance 2.7380125131254 --demod_completeness_check full --demod_use_ground true --eq_ax_congr_red false --extra_neg_conj none --inst_activity_threshold 16 --inst_dismatching false --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 6 --inst_learning_loop_flag true --inst_learning_start 1024 --inst_lit_activity_flag true --inst_lit_sel "[+depth;+sign;+num_symb;-split;-eq]" --inst_lit_sel_side cnt --inst_orphan_elimination true --inst_passive_queue_type list --inst_passive_queues "[[-num_lits];[-max_atom_input_occur;-ground]]" --inst_passive_queues_freq "[8;50]" --inst_prop_sim_given false --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.21724605765256222 --inst_solver_per_active 256 --inst_sos_flag true --inst_sos_phase true --inst_sos_sth_lit_sel "[-depth;+non_prol_conj_symb;-split;-ground;+num_var]" --inst_start_prop_sim_after_learn 8 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd false --prep_def_merge_prop_impl true --prep_def_merge_tr_cl true --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim false --prep_sem_filter none --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten false --prep_upred true --preprocessing_flag true --prolific_symb_bound 2048 --prop_solver_per_cl 32 --pure_diseq_elim false --resolution_flag false --schedule none --share_sel_clauses false --smt_ac_axioms full --smt_preprocessing true --splitting_cvd true --splitting_cvd_svl false --splitting_grd true --splitting_mode full --splitting_nvd 128 --stats_out none --sub_typing true --subs_bck_mult 0 --sup_full_bw "[Demod]" --sup_full_fw "[Subsumption;SubsumptionRes;UnitSubsAndRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_full_triv "[PropSubs;Unflattening]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[Subsumption;SubsumptionRes;UnitSubsAndRes;Demod;ACJoinability]" --sup_immed_fw_main "[SubsumptionRes;DemodLoopTriv;DemodLightNormLoopTriv;ACJoinability;ACNormalisation]" --sup_immed_triv "[]" --sup_indices_passive "[UnitSubsumption;NonunitSubsumption;Subsumption;FwDemod;BwDemod;LightNorm]" --sup_input_bw "[]" --sup_input_fw "[]" --sup_input_triv "[PropSubs;Unflattening]" --sup_iter_deepening 4 --sup_passive_queue_type queue --sup_passive_queues "[[+num_symb]]" --sup_passive_queues_freq "[5]" --sup_prop_simpl_given true --sup_prop_simpl_new false --sup_restarts_mult 4 --sup_smt_interval 10000 --sup_symb_ordering arity_random --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.4432297345384799 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/ugrasjcp 2>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/ugrasjcp_error
% 23.33/8.82 ERROR - "ProverProcess:heur/397442:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 64 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 4 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp true --inst_learning_factor 8 --inst_learning_loop_flag true --inst_learning_start 2 --inst_lit_activity_flag false --inst_lit_sel "[-split]" --inst_lit_sel_side num_lit --inst_orphan_elimination false --inst_passive_queue_type priority_queues --inst_passive_queues "[[+conj_symb]]" --inst_passive_queues_freq "[50]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 0.8199321230744955 --inst_solver_per_active 4 --inst_sos_flag false --inst_start_prop_sim_after_learn 7 --inst_subs_given false --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/p65frzc3 2>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/p65frzc3_error
% 23.33/8.82 ERROR - "ProverProcess:heur/421498:1.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 Fatal error: exception Failure("Clausification error: res/vclausify_rel exits with an error status: 1")
% 23.33/8.82 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_under "[]" --comb_inst_mult 8 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --inst_activity_threshold 512 --inst_dismatching true --inst_eager_unprocessed_to_passive false --inst_eq_res_simp true --inst_learning_factor 8 --inst_learning_loop_flag true --inst_learning_start 128 --inst_lit_activity_flag false --inst_lit_sel "[+sign;+prop]" --inst_lit_sel_side none --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[+num_symb;-age;-age];[+num_symb;+conj_non_prolific_symb]]" --inst_passive_queues_freq "[512;10]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew model --inst_solver_calls_frac 0.006221608720445637 --inst_solver_per_active 32768 --inst_sos_flag true --inst_sos_phase false --inst_sos_sth_lit_sel "[+non_prol_conj_symb;+sign;-depth;-prop]" --inst_start_prop_sim_after_learn 9 --inst_subs_given true --inst_subs_new false --instantiation_flag true --out_options none --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessing_flag true --prolific_symb_bound 256 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300.00 --res_to_prop_solver active --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[]" --sup_full_fw "[]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[]" --sup_immed_bw_main "[]" --sup_immed_fw_immed "[ACNormalisation]" --sup_immed_fw_main "[]" --sup_immed_triv "[]" --sup_indices_passive "[]" --sup_input_bw "[]" --sup_input_fw "[ACNormalisation]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 0.33" --time_out_real 1.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/g48n9drn 2>> /export/starexec/sandbox2/tmp/iprover_out_dwd6kvo2/g48n9drn_error
% 23.33/8.82 % SZS status Theorem for theBenchmark.p
% 23.33/8.82
% 23.33/8.82 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 23.33/8.82
% 23.33/8.82 % ------ iProver source info
% 23.33/8.82
% 23.33/8.82 % git: date: 2026-07-19 20:42:38 +0200
% 23.33/8.82 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 23.33/8.82 % git: non_committed_changes: false
% 23.33/8.82
% 23.33/8.82 % ------ Parsing...
% 23.33/8.82 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 23.33/8.82
% 23.33/8.82 % ------ Preprocessing... sup_sim: 0 sf_s rm: 50 0s sf_e sup_sim: 0 sf_s rm: 0 0s sf_e %
% 23.33/8.82
% 23.33/8.82 % ------ Preprocessing...%
% 23.33/8.82
% 23.33/8.82 % SZS status Theorem for theBenchmark.p
% 23.33/8.82
% 23.33/8.82 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 23.33/8.84
% 23.33/8.84
%------------------------------------------------------------------------------