%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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:10 PM UTC 2026
% Result : Theorem 1.04s 0.96s
% Output : CNFRefutation 1.04s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f49ERROR: Could not build tree for root c_4167ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op1(e13,e13) = e13
| op1(e13,e13) = e12
| op1(e13,e13) = e11
| op1(e13,e13) = e10 )
& ( op1(e13,e12) = e13
| op1(e13,e12) = e12
| op1(e13,e12) = e11
| op1(e13,e12) = e10 )
& ( op1(e13,e11) = e13
| op1(e13,e11) = e12
| op1(e13,e11) = e11
| op1(e13,e11) = e10 )
& ( op1(e13,e10) = e13
| op1(e13,e10) = e12
| op1(e13,e10) = e11
| op1(e13,e10) = e10 )
& ( op1(e12,e13) = e13
| op1(e12,e13) = e12
| op1(e12,e13) = e11
| op1(e12,e13) = e10 )
& ( op1(e12,e12) = e13
| op1(e12,e12) = e12
| op1(e12,e12) = e11
| op1(e12,e12) = e10 )
& ( op1(e12,e11) = e13
| op1(e12,e11) = e12
| op1(e12,e11) = e11
| op1(e12,e11) = e10 )
& ( op1(e12,e10) = e13
| op1(e12,e10) = e12
| op1(e12,e10) = e11
| op1(e12,e10) = e10 )
& ( op1(e11,e13) = e13
| op1(e11,e13) = e12
| op1(e11,e13) = e11
| op1(e11,e13) = e10 )
& ( op1(e11,e12) = e13
| op1(e11,e12) = e12
| op1(e11,e12) = e11
| op1(e11,e12) = e10 )
& ( op1(e11,e11) = e13
| op1(e11,e11) = e12
| op1(e11,e11) = e11
| op1(e11,e11) = e10 )
& ( op1(e11,e10) = e13
| op1(e11,e10) = e12
| op1(e11,e10) = e11
| op1(e11,e10) = e10 )
& ( op1(e10,e13) = e13
| op1(e10,e13) = e12
| op1(e10,e13) = e11
| op1(e10,e13) = e10 )
& ( op1(e10,e12) = e13
| op1(e10,e12) = e12
| op1(e10,e12) = e11
| op1(e10,e12) = e10 )
& ( op1(e10,e11) = e13
| op1(e10,e11) = e12
| op1(e10,e11) = e11
| op1(e10,e11) = e10 )
& ( op1(e10,e10) = e13
| op1(e10,e10) = e12
| op1(e10,e10) = e11
| op1(e10,e10) = e10 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( 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),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),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),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,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),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),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),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,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),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),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),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,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),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),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),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/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f5,axiom,
( ( op2(e23,e23) = e23
| op2(e23,e23) = e22
| op2(e23,e23) = e21
| op2(e23,e23) = e20 )
& ( op2(e23,e22) = e23
| op2(e23,e22) = e22
| op2(e23,e22) = e21
| op2(e23,e22) = e20 )
& ( op2(e23,e21) = e23
| op2(e23,e21) = e22
| op2(e23,e21) = e21
| op2(e23,e21) = e20 )
& ( op2(e23,e20) = e23
| op2(e23,e20) = e22
| op2(e23,e20) = e21
| op2(e23,e20) = e20 )
& ( op2(e22,e23) = e23
| op2(e22,e23) = e22
| op2(e22,e23) = e21
| op2(e22,e23) = e20 )
& ( op2(e22,e22) = e23
| op2(e22,e22) = e22
| op2(e22,e22) = e21
| op2(e22,e22) = e20 )
& ( op2(e22,e21) = e23
| op2(e22,e21) = e22
| op2(e22,e21) = e21
| op2(e22,e21) = e20 )
& ( op2(e22,e20) = e23
| op2(e22,e20) = e22
| op2(e22,e20) = e21
| op2(e22,e20) = e20 )
& ( op2(e21,e23) = e23
| op2(e21,e23) = e22
| op2(e21,e23) = e21
| op2(e21,e23) = e20 )
& ( op2(e21,e22) = e23
| op2(e21,e22) = e22
| op2(e21,e22) = e21
| op2(e21,e22) = e20 )
& ( op2(e21,e21) = e23
| op2(e21,e21) = e22
| op2(e21,e21) = e21
| op2(e21,e21) = e20 )
& ( op2(e21,e20) = e23
| op2(e21,e20) = e22
| op2(e21,e20) = e21
| op2(e21,e20) = e20 )
& ( op2(e20,e23) = e23
| op2(e20,e23) = e22
| op2(e20,e23) = e21
| op2(e20,e23) = e20 )
& ( op2(e20,e22) = e23
| op2(e20,e22) = e22
| op2(e20,e22) = e21
| op2(e20,e22) = e20 )
& ( op2(e20,e21) = e23
| op2(e20,e21) = e22
| op2(e20,e21) = e21
| op2(e20,e21) = e20 )
& ( op2(e20,e20) = e23
| op2(e20,e20) = e22
| op2(e20,e20) = e21
| op2(e20,e20) = e20 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( 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),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),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),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,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),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),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),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,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),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),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),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,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),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),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),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/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f17,axiom,
( op1(e13,e12) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e13)
& op1(e13,e11) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e13)
& op1(e13,e10) != op1(e13,e12)
& op1(e13,e10) != op1(e13,e11)
& op1(e12,e12) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e13)
& op1(e12,e11) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e13)
& op1(e12,e10) != op1(e12,e12)
& op1(e12,e10) != op1(e12,e11)
& op1(e11,e12) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e13)
& op1(e11,e11) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e13)
& op1(e11,e10) != op1(e11,e12)
& op1(e11,e10) != op1(e11,e11)
& op1(e10,e12) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e13)
& op1(e10,e11) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e13)
& op1(e10,e10) != op1(e10,e12)
& op1(e10,e10) != op1(e10,e11)
& op1(e12,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e13,e13)
& op1(e11,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e13,e13)
& op1(e10,e13) != op1(e12,e13)
& op1(e10,e13) != op1(e11,e13)
& op1(e12,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e13,e12)
& op1(e11,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e13,e12)
& op1(e10,e12) != op1(e12,e12)
& op1(e10,e12) != op1(e11,e12)
& op1(e12,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e13,e11)
& op1(e11,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e13,e11)
& op1(e10,e11) != op1(e12,e11)
& op1(e10,e11) != op1(e11,e11)
& op1(e12,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e13,e10)
& op1(e11,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e13,e10)
& op1(e10,e10) != op1(e12,e10)
& op1(e10,e10) != op1(e11,e10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
( op2(e23,e22) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e23)
& op2(e23,e21) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e23)
& op2(e23,e20) != op2(e23,e22)
& op2(e23,e20) != op2(e23,e21)
& op2(e22,e22) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e23)
& op2(e22,e21) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e23)
& op2(e22,e20) != op2(e22,e22)
& op2(e22,e20) != op2(e22,e21)
& op2(e21,e22) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e23)
& op2(e21,e21) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e23)
& op2(e21,e20) != op2(e21,e22)
& op2(e21,e20) != op2(e21,e21)
& op2(e20,e22) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e23)
& op2(e20,e21) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e23)
& op2(e20,e20) != op2(e20,e22)
& op2(e20,e20) != op2(e20,e21)
& op2(e22,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e23,e23)
& op2(e21,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e23,e23)
& op2(e20,e23) != op2(e22,e23)
& op2(e20,e23) != op2(e21,e23)
& op2(e22,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e23,e22)
& op2(e21,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e23,e22)
& op2(e20,e22) != op2(e22,e22)
& op2(e20,e22) != op2(e21,e22)
& op2(e22,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e23,e21)
& op2(e21,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e23,e21)
& op2(e20,e21) != op2(e22,e21)
& op2(e20,e21) != op2(e21,e21)
& op2(e22,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e23,e20)
& op2(e21,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e23,e20)
& op2(e20,e20) != op2(e22,e20)
& op2(e20,e20) != op2(e21,e20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f24,axiom,
( e13 = op1(e12,e12)
& e11 = op1(e12,op1(e12,e12))
& e10 = op1(op1(e12,op1(e12,e12)),e12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
( e23 = op2(e22,e22)
& e21 = op2(e22,op2(e22,e22))
& e20 = op2(op2(e22,op2(e22,e22)),e22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
( h1(e13) = op2(e20,e20)
& h1(e11) = op2(e20,op2(e20,e20))
& h1(e10) = op2(op2(e20,op2(e20,e20)),e20)
& h1(e12) = e20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f27,axiom,
( h2(e13) = op2(e21,e21)
& h2(e11) = op2(e21,op2(e21,e21))
& h2(e10) = op2(op2(e21,op2(e21,e21)),e21)
& h2(e12) = e21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f29,axiom,
( h4(e13) = op2(e23,e23)
& h4(e11) = op2(e23,op2(e23,e23))
& h4(e10) = op2(op2(e23,op2(e23,e23)),e23)
& h4(e12) = e23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f53,plain,
( ~ sP8
| ( e21 != h2(e13)
& e21 != h2(e12)
& e21 != h2(e11)
& e21 != h2(e10) ) ),
inference(nnf_transformation,[],[f45]) ).
fof(f54,plain,
( ~ sP7
| ( e22 != h2(e13)
& e22 != h2(e12)
& e22 != h2(e11)
& e22 != h2(e10) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f55,plain,
( ~ sP6
| ( e23 != h2(e13)
& e23 != h2(e12)
& e23 != h2(e11)
& e23 != h2(e10) ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f64,plain,
( e13 = op1(e13,e11)
| e12 = op1(e13,e11)
| e11 = op1(e13,e11)
| e10 = op1(e13,e11) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e13 = op1(e12,e12)
| e12 = op1(e12,e12)
| e11 = op1(e12,e12)
| e10 = op1(e12,e12) ),
inference(cnf_transformation,[],[f1]) ).
fof(f78,plain,
op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f80,plain,
op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11)),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10)),
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
( e23 = op2(e23,e21)
| e22 = op2(e23,e21)
| e21 = op2(e23,e21)
| e20 = op2(e23,e21) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( e23 = op2(e22,e22)
| e22 = op2(e22,e22)
| e21 = op2(e22,e22)
| e20 = op2(e22,e22) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f180,plain,
op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f181,plain,
op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f182,plain,
op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f183,plain,
op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f184,plain,
op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f185,plain,
op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f186,plain,
op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f190,plain,
op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f191,plain,
op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f192,plain,
op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f193,plain,
op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f195,plain,
op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f197,plain,
op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f199,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(cnf_transformation,[],[f6]) ).
fof(f200,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f210,plain,
op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f214,plain,
op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20)),
inference(cnf_transformation,[],[f6]) ).
fof(f229,plain,
op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21)),
inference(cnf_transformation,[],[f6]) ).
fof(f240,plain,
op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22)),
inference(cnf_transformation,[],[f6]) ).
fof(f327,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f17]) ).
fof(f328,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f17]) ).
fof(f329,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f17]) ).
fof(f375,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f376,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f18]) ).
fof(f378,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[],[f18]) ).
fof(f450,plain,
e13 = op1(e12,e12),
inference(cnf_transformation,[],[f24]) ).
fof(f451,plain,
e11 = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f24]) ).
fof(f452,plain,
e10 = op1(op1(e12,op1(e12,e12)),e12),
inference(cnf_transformation,[],[f24]) ).
fof(f453,plain,
e23 = op2(e22,e22),
inference(cnf_transformation,[],[f25]) ).
fof(f454,plain,
e21 = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f25]) ).
fof(f455,plain,
e20 = op2(op2(e22,op2(e22,e22)),e22),
inference(cnf_transformation,[],[f25]) ).
fof(f456,plain,
op2(e20,e20) = h1(e13),
inference(cnf_transformation,[],[f26]) ).
fof(f460,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f27]) ).
fof(f461,plain,
op2(e21,op2(e21,e21)) = h2(e11),
inference(cnf_transformation,[],[f27]) ).
fof(f462,plain,
h2(e10) = op2(op2(e21,op2(e21,e21)),e21),
inference(cnf_transformation,[],[f27]) ).
fof(f463,plain,
e21 = h2(e12),
inference(cnf_transformation,[],[f27]) ).
fof(f468,plain,
op2(e23,e23) = h4(e13),
inference(cnf_transformation,[],[f29]) ).
fof(f469,plain,
op2(e23,op2(e23,e23)) = h4(e11),
inference(cnf_transformation,[],[f29]) ).
fof(f470,plain,
h4(e10) = op2(op2(e23,op2(e23,e23)),e23),
inference(cnf_transformation,[],[f29]) ).
fof(f485,plain,
( ~ sP8
| e21 != h2(e12) ),
inference(cnf_transformation,[],[f53]) ).
fof(f490,plain,
( ~ sP7
| e22 != h2(e11) ),
inference(cnf_transformation,[],[f54]) ).
fof(f492,plain,
( ~ sP6
| e23 != h2(e13) ),
inference(cnf_transformation,[],[f55]) ).
fof(f531,plain,
( sP6
| sP7
| sP8
| e20 != h2(e10)
| h2(op1(e13,e13)) != op2(h2(e13),h2(e13))
| h2(op1(e13,e12)) != op2(h2(e13),h2(e12))
| h2(op1(e13,e11)) != op2(h2(e13),h2(e11))
| h2(op1(e13,e10)) != op2(h2(e13),h2(e10))
| h2(op1(e12,e13)) != op2(h2(e12),h2(e13))
| h2(op1(e12,e12)) != op2(h2(e12),h2(e12))
| h2(op1(e12,e11)) != op2(h2(e12),h2(e11))
| h2(op1(e12,e10)) != op2(h2(e12),h2(e10))
| h2(op1(e11,e13)) != op2(h2(e11),h2(e13))
| h2(op1(e11,e12)) != op2(h2(e11),h2(e12))
| h2(op1(e11,e11)) != op2(h2(e11),h2(e11))
| h2(op1(e11,e10)) != op2(h2(e11),h2(e10))
| h2(op1(e10,e13)) != op2(h2(e10),h2(e13))
| h2(op1(e10,e12)) != op2(h2(e10),h2(e12))
| h2(op1(e10,e11)) != op2(h2(e10),h2(e11))
| h2(op1(e10,e10)) != op2(h2(e10),h2(e10)) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_59,plain,
( ( op1(e12,e12) = e13 )
| ( op1(e12,e12) = e12 )
| ( op1(e12,e12) = e11 )
| ( op1(e12,e12) = e10 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_62,plain,
( ( op1(e13,e11) = e13 )
| ( op1(e13,e11) = e12 )
| ( op1(e13,e11) = e11 )
| ( op1(e13,e11) = e10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_101,plain,
op1(op1(e12,e11),e10) = op1(e12,op1(e11,e10)),
inference(cnf_transformation,[],[f105]) ).
tcf(c_107,plain,
op1(op1(e12,e12),e12) = op1(e12,op1(e12,e12)),
inference(cnf_transformation,[],[f99]) ).
tcf(c_108,plain,
op1(op1(e12,e12),e13) = op1(e12,op1(e12,e13)),
inference(cnf_transformation,[],[f98]) ).
tcf(c_110,plain,
op1(op1(e12,e13),e11) = op1(e12,op1(e13,e11)),
inference(cnf_transformation,[],[f96]) ).
tcf(c_111,plain,
op1(op1(e12,e13),e12) = op1(e12,op1(e13,e12)),
inference(cnf_transformation,[],[f95]) ).
tcf(c_112,plain,
op1(op1(e12,e13),e13) = op1(e12,op1(e13,e13)),
inference(cnf_transformation,[],[f94]) ).
tcf(c_121,plain,
op1(op1(e13,e12),e10) = op1(e13,op1(e12,e10)),
inference(cnf_transformation,[],[f85]) ).
tcf(c_122,plain,
op1(op1(e13,e12),e11) = op1(e13,op1(e12,e11)),
inference(cnf_transformation,[],[f84]) ).
tcf(c_124,plain,
op1(op1(e13,e12),e13) = op1(e13,op1(e12,e13)),
inference(cnf_transformation,[],[f82]) ).
tcf(c_126,plain,
op1(op1(e13,e13),e11) = op1(e13,op1(e13,e11)),
inference(cnf_transformation,[],[f80]) ).
tcf(c_127,plain,
op1(op1(e13,e13),e12) = op1(e13,op1(e13,e12)),
inference(cnf_transformation,[],[f79]) ).
tcf(c_128,plain,
op1(op1(e13,e13),e13) = op1(e13,op1(e13,e13)),
inference(cnf_transformation,[],[f78]) ).
tcf(c_160,plain,
( ( op2(e22,e22) = e23 )
| ( op2(e22,e22) = e22 )
| ( op2(e22,e22) = e21 )
| ( op2(e22,e22) = e20 ) ),
inference(cnf_transformation,[],[f168]) ).
tcf(c_163,plain,
( ( op2(e23,e21) = e23 )
| ( op2(e23,e21) = e22 )
| ( op2(e23,e21) = e21 )
| ( op2(e23,e21) = e20 ) ),
inference(cnf_transformation,[],[f165]) ).
tcf(c_168,plain,
op2(op2(e20,e20),e22) = op2(e20,op2(e20,e22)),
inference(cnf_transformation,[],[f240]) ).
tcf(c_179,plain,
op2(op2(e20,e23),e21) = op2(e20,op2(e23,e21)),
inference(cnf_transformation,[],[f229]) ).
tcf(c_194,plain,
op2(op2(e21,e23),e20) = op2(e21,op2(e23,e20)),
inference(cnf_transformation,[],[f214]) ).
tcf(c_198,plain,
op2(op2(e22,e20),e20) = op2(e22,op2(e20,e20)),
inference(cnf_transformation,[],[f210]) ).
tcf(c_208,plain,
op2(op2(e22,e22),e22) = op2(e22,op2(e22,e22)),
inference(cnf_transformation,[],[f200]) ).
tcf(c_209,plain,
op2(op2(e22,e22),e23) = op2(e22,op2(e22,e23)),
inference(cnf_transformation,[],[f199]) ).
tcf(c_211,plain,
op2(op2(e22,e23),e21) = op2(e22,op2(e23,e21)),
inference(cnf_transformation,[],[f197]) ).
tcf(c_213,plain,
op2(op2(e22,e23),e23) = op2(e22,op2(e23,e23)),
inference(cnf_transformation,[],[f195]) ).
tcf(c_215,plain,
op2(op2(e23,e20),e21) = op2(e23,op2(e20,e21)),
inference(cnf_transformation,[],[f193]) ).
tcf(c_216,plain,
op2(op2(e23,e20),e22) = op2(e23,op2(e20,e22)),
inference(cnf_transformation,[],[f192]) ).
tcf(c_217,plain,
op2(op2(e23,e20),e23) = op2(e23,op2(e20,e23)),
inference(cnf_transformation,[],[f191]) ).
tcf(c_218,plain,
op2(op2(e23,e21),e20) = op2(e23,op2(e21,e20)),
inference(cnf_transformation,[],[f190]) ).
tcf(c_222,plain,
op2(op2(e23,e22),e20) = op2(e23,op2(e22,e20)),
inference(cnf_transformation,[],[f186]) ).
tcf(c_223,plain,
op2(op2(e23,e22),e21) = op2(e23,op2(e22,e21)),
inference(cnf_transformation,[],[f185]) ).
tcf(c_224,plain,
op2(op2(e23,e22),e22) = op2(e23,op2(e22,e22)),
inference(cnf_transformation,[],[f184]) ).
tcf(c_225,plain,
op2(op2(e23,e22),e23) = op2(e23,op2(e22,e23)),
inference(cnf_transformation,[],[f183]) ).
tcf(c_226,plain,
op2(op2(e23,e23),e20) = op2(e23,op2(e23,e20)),
inference(cnf_transformation,[],[f182]) ).
tcf(c_227,plain,
op2(op2(e23,e23),e21) = op2(e23,op2(e23,e21)),
inference(cnf_transformation,[],[f181]) ).
tcf(c_228,plain,
op2(op2(e23,e23),e22) = op2(e23,op2(e23,e22)),
inference(cnf_transformation,[],[f180]) ).
tcf(c_229,plain,
op2(op2(e23,e23),e23) = op2(e23,op2(e23,e23)),
inference(cnf_transformation,[],[f179]) ).
tcf(c_333,plain,
op1(e12,e10) != op1(e12,e11),
inference(cnf_transformation,[],[f329]) ).
tcf(c_334,plain,
op1(e12,e10) != op1(e12,e12),
inference(cnf_transformation,[],[f328]) ).
tcf(c_335,plain,
op1(e12,e10) != op1(e12,e13),
inference(cnf_transformation,[],[f327]) ).
tcf(c_380,plain,
op2(e21,e22) != op2(e21,e23),
inference(cnf_transformation,[],[f378]) ).
tcf(c_382,plain,
op2(e22,e20) != op2(e22,e22),
inference(cnf_transformation,[],[f376]) ).
tcf(c_383,plain,
op2(e22,e20) != op2(e22,e23),
inference(cnf_transformation,[],[f375]) ).
tcf(c_429,plain,
op1(op1(e12,op1(e12,e12)),e12) = e10,
inference(cnf_transformation,[],[f452]) ).
tcf(c_430,plain,
op1(e12,op1(e12,e12)) = e11,
inference(cnf_transformation,[],[f451]) ).
tcf(c_431,plain,
op1(e12,e12) = e13,
inference(cnf_transformation,[],[f450]) ).
tcf(c_432,plain,
op2(op2(e22,op2(e22,e22)),e22) = e20,
inference(cnf_transformation,[],[f455]) ).
tcf(c_433,plain,
op2(e22,op2(e22,e22)) = e21,
inference(cnf_transformation,[],[f454]) ).
tcf(c_434,plain,
op2(e22,e22) = e23,
inference(cnf_transformation,[],[f453]) ).
tcf(c_438,plain,
op2(e20,e20) = h1(e13),
inference(cnf_transformation,[],[f456]) ).
tcf(c_439,plain,
h2(e12) = e21,
inference(cnf_transformation,[],[f463]) ).
tcf(c_440,plain,
op2(op2(e21,op2(e21,e21)),e21) = h2(e10),
inference(cnf_transformation,[],[f462]) ).
tcf(c_441,plain,
op2(e21,op2(e21,e21)) = h2(e11),
inference(cnf_transformation,[],[f461]) ).
tcf(c_442,plain,
op2(e21,e21) = h2(e13),
inference(cnf_transformation,[],[f460]) ).
tcf(c_448,plain,
op2(op2(e23,op2(e23,e23)),e23) = h4(e10),
inference(cnf_transformation,[],[f470]) ).
tcf(c_449,plain,
op2(e23,op2(e23,e23)) = h4(e11),
inference(cnf_transformation,[],[f469]) ).
tcf(c_450,plain,
op2(e23,e23) = h4(e13),
inference(cnf_transformation,[],[f468]) ).
tcf(c_465,plain,
( ~ sP8
| ( h2(e12) != e21 ) ),
inference(cnf_transformation,[],[f485]) ).
tcf(c_468,plain,
( ~ sP7
| ( h2(e11) != e22 ) ),
inference(cnf_transformation,[],[f490]) ).
tcf(c_474,plain,
( ~ sP6
| ( h2(e13) != e23 ) ),
inference(cnf_transformation,[],[f492]) ).
tcf(c_503,negated_conjecture,
( sP6
| sP7
| sP8
| ( h2(e10) != e20 )
| ( op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) )
| ( op2(h2(e13),h2(e12)) != h2(op1(e13,e12)) )
| ( op2(h2(e13),h2(e11)) != h2(op1(e13,e11)) )
| ( op2(h2(e13),h2(e10)) != h2(op1(e13,e10)) )
| ( op2(h2(e12),h2(e13)) != h2(op1(e12,e13)) )
| ( op2(h2(e12),h2(e12)) != h2(op1(e12,e12)) )
| ( op2(h2(e12),h2(e11)) != h2(op1(e12,e11)) )
| ( op2(h2(e12),h2(e10)) != h2(op1(e12,e10)) )
| ( op2(h2(e11),h2(e13)) != h2(op1(e11,e13)) )
| ( op2(h2(e11),h2(e12)) != h2(op1(e11,e12)) )
| ( op2(h2(e11),h2(e11)) != h2(op1(e11,e11)) )
| ( op2(h2(e11),h2(e10)) != h2(op1(e11,e10)) )
| ( op2(h2(e10),h2(e13)) != h2(op1(e10,e13)) )
| ( op2(h2(e10),h2(e12)) != h2(op1(e10,e12)) )
| ( op2(h2(e10),h2(e11)) != h2(op1(e10,e11)) )
| ( op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ) ),
inference(cnf_transformation,[],[f531]) ).
tcf(c_539,plain,
op2(e22,e22) = e23,
inference(global_subsumption_just,[status(thm)],[c_160,c_434]) ).
tcf(c_541,plain,
op1(e12,e12) = e13,
inference(global_subsumption_just,[status(thm)],[c_59,c_431]) ).
tcf(c_569,plain,
( sP6
| sP7
| ( op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) )
| ( op2(h2(e10),h2(e11)) != h2(op1(e10,e11)) )
| ( op2(h2(e10),h2(e12)) != h2(op1(e10,e12)) )
| ( op2(h2(e10),h2(e13)) != h2(op1(e10,e13)) )
| ( op2(h2(e11),h2(e10)) != h2(op1(e11,e10)) )
| ( op2(h2(e11),h2(e11)) != h2(op1(e11,e11)) )
| ( op2(h2(e11),h2(e12)) != h2(op1(e11,e12)) )
| ( op2(h2(e11),h2(e13)) != h2(op1(e11,e13)) )
| ( op2(h2(e12),h2(e10)) != h2(op1(e12,e10)) )
| ( op2(h2(e12),h2(e11)) != h2(op1(e12,e11)) )
| ( op2(h2(e12),h2(e12)) != h2(op1(e12,e12)) )
| ( op2(h2(e12),h2(e13)) != h2(op1(e12,e13)) )
| ( op2(h2(e13),h2(e10)) != h2(op1(e13,e10)) )
| ( op2(h2(e13),h2(e11)) != h2(op1(e13,e11)) )
| ( op2(h2(e13),h2(e12)) != h2(op1(e13,e12)) )
| ( op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) )
| ( h2(e10) != e20 ) ),
inference(global_subsumption_just,[status(thm)],[c_503,c_439,c_465,c_503]) ).
tcf(c_570,negated_conjecture,
( sP6
| sP7
| ( h2(e10) != e20 )
| ( op2(h2(e13),h2(e13)) != h2(op1(e13,e13)) )
| ( op2(h2(e13),h2(e12)) != h2(op1(e13,e12)) )
| ( op2(h2(e13),h2(e11)) != h2(op1(e13,e11)) )
| ( op2(h2(e13),h2(e10)) != h2(op1(e13,e10)) )
| ( op2(h2(e12),h2(e13)) != h2(op1(e12,e13)) )
| ( op2(h2(e12),h2(e12)) != h2(op1(e12,e12)) )
| ( op2(h2(e12),h2(e11)) != h2(op1(e12,e11)) )
| ( op2(h2(e12),h2(e10)) != h2(op1(e12,e10)) )
| ( op2(h2(e11),h2(e13)) != h2(op1(e11,e13)) )
| ( op2(h2(e11),h2(e12)) != h2(op1(e11,e12)) )
| ( op2(h2(e11),h2(e11)) != h2(op1(e11,e11)) )
| ( op2(h2(e11),h2(e10)) != h2(op1(e11,e10)) )
| ( op2(h2(e10),h2(e13)) != h2(op1(e10,e13)) )
| ( op2(h2(e10),h2(e12)) != h2(op1(e10,e12)) )
| ( op2(h2(e10),h2(e11)) != h2(op1(e10,e11)) )
| ( op2(h2(e10),h2(e10)) != h2(op1(e10,e10)) ) ),
inference(renaming,[status(thm)],[c_569]) ).
tcf(c_677,plain,
( ( h2(e11) != e22 )
| ~ sP7 ),
inference(prop_impl_just,[status(thm)],[c_468]) ).
tcf(c_678,plain,
( ~ sP7
| ( h2(e11) != e22 ) ),
inference(renaming,[status(thm)],[c_677]) ).
tcf(c_697,plain,
( ( h2(e13) != e23 )
| ~ sP6 ),
inference(prop_impl_just,[status(thm)],[c_474]) ).
tcf(c_698,plain,
( ~ sP6
| ( h2(e13) != e23 ) ),
inference(renaming,[status(thm)],[c_697]) ).
tcf(c_3354,plain,
op2(e22,e23) = e21,
inference(light_normalisation,[status(thm)],[c_433,c_539]) ).
tcf(c_3355,plain,
op1(e12,e13) = e11,
inference(light_normalisation,[status(thm)],[c_430,c_541]) ).
tcf(c_3356,plain,
op2(e23,h4(e13)) = h4(e11),
inference(light_normalisation,[status(thm)],[c_449,c_450]) ).
tcf(c_3360,plain,
op2(e21,h2(e13)) = h2(e11),
inference(light_normalisation,[status(thm)],[c_441,c_442]) ).
tcf(c_3368,plain,
op2(e22,e20) != e21,
inference(light_normalisation,[status(thm)],[c_383,c_3354]) ).
tcf(c_3369,plain,
op2(e22,e20) != e23,
inference(light_normalisation,[status(thm)],[c_382,c_539]) ).
tcf(c_3393,plain,
op1(e12,e10) != e11,
inference(light_normalisation,[status(thm)],[c_335,c_3355]) ).
tcf(c_3394,plain,
op1(e12,e10) != e13,
inference(light_normalisation,[status(thm)],[c_334,c_541]) ).
tcf(c_3401,plain,
op2(e21,e22) = e20,
inference(light_normalisation,[status(thm)],[c_432,c_539,c_3354]) ).
tcf(c_3407,plain,
op2(e21,e23) != e20,
inference(demodulation,[status(thm)],[c_380,c_3401]) ).
tcf(c_3408,plain,
op1(e11,e12) = e10,
inference(light_normalisation,[status(thm)],[c_429,c_541,c_3355]) ).
tcf(c_3415,plain,
op2(h4(e11),e23) = h4(e10),
inference(light_normalisation,[status(thm)],[c_448,c_450,c_3356]) ).
tcf(c_3417,plain,
op2(h2(e11),e21) = h2(e10),
inference(light_normalisation,[status(thm)],[c_440,c_442,c_3360]) ).
tcf(c_3515,plain,
op2(h4(e13),e23) = h4(e11),
inference(light_normalisation,[status(thm)],[c_229,c_450,c_3356]) ).
tcf(c_3516,plain,
op2(e23,op2(e23,e22)) = op2(h4(e13),e22),
inference(light_normalisation,[status(thm)],[c_228,c_450]) ).
tcf(c_3517,plain,
op2(e23,op2(e23,e21)) = op2(h4(e13),e21),
inference(light_normalisation,[status(thm)],[c_227,c_450]) ).
tcf(c_3518,plain,
op2(e23,op2(e23,e20)) = op2(h4(e13),e20),
inference(light_normalisation,[status(thm)],[c_226,c_450]) ).
tcf(c_3519,plain,
op2(op2(e23,e22),e23) = op2(e23,e21),
inference(light_normalisation,[status(thm)],[c_225,c_3354]) ).
tcf(c_3520,plain,
op2(op2(e23,e22),e22) = h4(e13),
inference(light_normalisation,[status(thm)],[c_224,c_539,c_450]) ).
tcf(c_3524,plain,
op2(e22,h4(e13)) = op2(e21,e23),
inference(light_normalisation,[status(thm)],[c_213,c_450,c_3354]) ).
tcf(c_3526,plain,
op2(e22,op2(e23,e21)) = h2(e13),
inference(light_normalisation,[status(thm)],[c_211,c_442,c_3354]) ).
tcf(c_3528,plain,
op2(e22,e21) = h4(e13),
inference(light_normalisation,[status(thm)],[c_209,c_539,c_450,c_3354]) ).
tcf(c_3529,plain,
op2(op2(e23,e22),e21) = op2(e23,h4(e13)),
inference(demodulation,[status(thm)],[c_223,c_3528]) ).
tcf(c_3536,plain,
op2(op2(e23,e22),e21) = h4(e11),
inference(light_normalisation,[status(thm)],[c_3529,c_3356]) ).
tcf(c_3537,plain,
op2(e23,e22) = e21,
inference(light_normalisation,[status(thm)],[c_208,c_539,c_3354]) ).
tcf(c_3538,plain,
op2(e21,e21) = h4(e11),
inference(demodulation,[status(thm)],[c_3536,c_3537]) ).
tcf(c_3540,plain,
op2(e23,op2(e22,e20)) = op2(e21,e20),
inference(demodulation,[status(thm)],[c_222,c_3537]) ).
tcf(c_3541,plain,
op2(e21,e22) = h4(e13),
inference(demodulation,[status(thm)],[c_3520,c_3537]) ).
tcf(c_3542,plain,
op2(e21,e23) = op2(e23,e21),
inference(demodulation,[status(thm)],[c_3519,c_3537]) ).
tcf(c_3543,plain,
op2(h4(e13),e22) = op2(e23,e21),
inference(demodulation,[status(thm)],[c_3516,c_3537]) ).
tcf(c_3550,plain,
op2(h4(e13),e22) = op2(e21,e23),
inference(demodulation,[status(thm)],[c_3543,c_3542]) ).
tcf(c_3552,plain,
op2(e22,op2(e21,e23)) = h2(e13),
inference(demodulation,[status(thm)],[c_3526,c_3542]) ).
tcf(c_3553,plain,
op2(op2(e21,e23),e20) = op2(e23,op2(e21,e20)),
inference(demodulation,[status(thm)],[c_218,c_3542]) ).
tcf(c_3557,plain,
op2(e23,op2(e21,e23)) = op2(h4(e13),e21),
inference(demodulation,[status(thm)],[c_3517,c_3542]) ).
tcf(c_3563,plain,
h4(e13) = e20,
inference(light_normalisation,[status(thm)],[c_3541,c_3401]) ).
tcf(c_3564,plain,
op2(e20,e22) = op2(e21,e23),
inference(demodulation,[status(thm)],[c_3550,c_3563]) ).
tcf(c_3566,plain,
op2(e23,op2(e21,e23)) = op2(e20,e21),
inference(demodulation,[status(thm)],[c_3557,c_3563]) ).
tcf(c_3571,plain,
op2(e22,e21) = e20,
inference(demodulation,[status(thm)],[c_3528,c_3563]) ).
tcf(c_3572,plain,
op2(e21,e23) = op2(e22,e20),
inference(demodulation,[status(thm)],[c_3524,c_3563]) ).
tcf(c_3573,plain,
op2(e23,op2(e23,e20)) = op2(e20,e20),
inference(demodulation,[status(thm)],[c_3518,c_3563]) ).
tcf(c_3574,plain,
op2(e20,e23) = h4(e11),
inference(demodulation,[status(thm)],[c_3515,c_3563]) ).
tcf(c_3579,plain,
op2(e23,e20) = h4(e11),
inference(demodulation,[status(thm)],[c_3356,c_3563]) ).
tcf(c_3581,plain,
op2(e23,e23) = e20,
inference(demodulation,[status(thm)],[c_450,c_3563]) ).
tcf(c_3587,plain,
op2(e23,op2(e20,e21)) = op2(h4(e11),e21),
inference(demodulation,[status(thm)],[c_215,c_3579]) ).
tcf(c_3588,plain,
op2(e23,op2(e20,e22)) = op2(h4(e11),e22),
inference(demodulation,[status(thm)],[c_216,c_3579]) ).
tcf(c_3589,plain,
op2(e23,op2(e20,e23)) = op2(h4(e11),e23),
inference(demodulation,[status(thm)],[c_217,c_3579]) ).
tcf(c_3593,plain,
op2(e23,op2(e20,e23)) = h4(e10),
inference(light_normalisation,[status(thm)],[c_3589,c_3415]) ).
tcf(c_3596,plain,
op2(e23,h4(e11)) = h4(e10),
inference(demodulation,[status(thm)],[c_3593,c_3574]) ).
tcf(c_3602,plain,
h1(e13) = h4(e10),
inference(light_normalisation,[status(thm)],[c_3573,c_438,c_3579,c_3596]) ).
tcf(c_3604,plain,
op2(h4(e11),e23) = h1(e13),
inference(demodulation,[status(thm)],[c_3415,c_3602]) ).
tcf(c_3617,plain,
op2(e22,op2(e22,e20)) = h2(e13),
inference(demodulation,[status(thm)],[c_3552,c_3572]) ).
tcf(c_3618,plain,
op2(op2(e22,e20),e20) = op2(e23,op2(e21,e20)),
inference(demodulation,[status(thm)],[c_3553,c_3572]) ).
tcf(c_3621,plain,
op2(e22,e20) = op2(e23,e21),
inference(demodulation,[status(thm)],[c_3542,c_3572]) ).
tcf(c_3622,plain,
op2(e22,e20) != e20,
inference(demodulation,[status(thm)],[c_3407,c_3572]) ).
tcf(c_3626,plain,
op2(e23,op2(e22,e20)) = op2(e20,e21),
inference(light_normalisation,[status(thm)],[c_3566,c_3572]) ).
tcf(c_3628,plain,
op2(e20,e22) = op2(e22,e20),
inference(light_normalisation,[status(thm)],[c_3564,c_3572]) ).
tcf(c_3630,plain,
op2(e23,op2(e22,e20)) = op2(h4(e11),e22),
inference(demodulation,[status(thm)],[c_3588,c_3628]) ).
tcf(c_3636,plain,
op2(h4(e11),e22) = op2(e20,e21),
inference(light_normalisation,[status(thm)],[c_3630,c_3626]) ).
tcf(c_3637,plain,
op2(e20,e21) = op2(e21,e20),
inference(light_normalisation,[status(thm)],[c_3540,c_3626]) ).
tcf(c_3638,plain,
op2(op2(e22,e20),e20) = op2(e23,op2(e20,e21)),
inference(demodulation,[status(thm)],[c_3618,c_3637]) ).
tcf(c_3645,plain,
op2(op2(e22,e20),e20) = op2(h4(e11),e21),
inference(light_normalisation,[status(thm)],[c_3638,c_3587]) ).
tcf(c_3646,plain,
h2(e13) = h4(e11),
inference(light_normalisation,[status(thm)],[c_3538,c_442]) ).
tcf(c_3647,plain,
op2(op2(e22,e20),e20) = op2(h2(e13),e21),
inference(demodulation,[status(thm)],[c_3645,c_3646]) ).
tcf(c_3649,plain,
op2(h2(e13),e22) = op2(e20,e21),
inference(demodulation,[status(thm)],[c_3636,c_3646]) ).
tcf(c_3652,plain,
op2(h2(e13),e23) = h1(e13),
inference(demodulation,[status(thm)],[c_3604,c_3646]) ).
tcf(c_3654,plain,
op2(e20,e23) = h2(e13),
inference(demodulation,[status(thm)],[c_3574,c_3646]) ).
tcf(c_3661,plain,
op2(e23,e20) = h2(e13),
inference(demodulation,[status(thm)],[c_3579,c_3646]) ).
tcf(c_3677,plain,
op2(h2(e13),e21) = op2(e22,h1(e13)),
inference(light_normalisation,[status(thm)],[c_198,c_438,c_3647]) ).
tcf(c_3678,plain,
op2(op2(e22,e20),e20) = op2(e22,h1(e13)),
inference(demodulation,[status(thm)],[c_3647,c_3677]) ).
tcf(c_3683,plain,
op2(e22,h1(e13)) = h2(e11),
inference(light_normalisation,[status(thm)],[c_194,c_3360,c_3572,c_3661,c_3678]) ).
tcf(c_3686,plain,
op2(h2(e13),e21) = h2(e11),
inference(demodulation,[status(thm)],[c_3677,c_3683]) ).
tcf(c_3701,plain,
op2(e20,op2(e22,e20)) = h2(e11),
inference(light_normalisation,[status(thm)],[c_179,c_3621,c_3654,c_3686]) ).
tcf(c_3715,plain,
op2(h1(e13),e22) = h2(e11),
inference(light_normalisation,[status(thm)],[c_168,c_438,c_3628,c_3701]) ).
tcf(c_3718,plain,
op1(op1(e13,e12),e13) = op1(e13,e11),
inference(light_normalisation,[status(thm)],[c_124,c_3355]) ).
tcf(c_3721,plain,
op1(e12,op1(e13,e13)) = op1(e11,e13),
inference(light_normalisation,[status(thm)],[c_112,c_3355]) ).
tcf(c_3722,plain,
op1(e12,op1(e13,e12)) = e10,
inference(light_normalisation,[status(thm)],[c_111,c_3355,c_3408]) ).
tcf(c_3723,plain,
op1(e12,op1(e13,e11)) = op1(e11,e11),
inference(light_normalisation,[status(thm)],[c_110,c_3355]) ).
tcf(c_3725,plain,
op1(e12,e11) = op1(e13,e13),
inference(light_normalisation,[status(thm)],[c_108,c_541,c_3355]) ).
tcf(c_3726,plain,
op1(e12,op1(e12,e11)) = op1(e11,e13),
inference(demodulation,[status(thm)],[c_3721,c_3725]) ).
tcf(c_3729,plain,
op1(op1(e12,e11),e11) = op1(e13,op1(e13,e11)),
inference(demodulation,[status(thm)],[c_126,c_3725]) ).
tcf(c_3730,plain,
op1(op1(e12,e11),e12) = op1(e13,op1(e13,e12)),
inference(demodulation,[status(thm)],[c_127,c_3725]) ).
tcf(c_3731,plain,
op1(op1(e12,e11),e13) = op1(e13,op1(e12,e11)),
inference(demodulation,[status(thm)],[c_128,c_3725]) ).
tcf(c_3738,plain,
op1(e13,e12) = e11,
inference(light_normalisation,[status(thm)],[c_107,c_541,c_3355]) ).
tcf(c_3740,plain,
op1(op1(e12,e11),e12) = op1(e13,e11),
inference(demodulation,[status(thm)],[c_3730,c_3738]) ).
tcf(c_3742,plain,
op1(e12,e11) = e10,
inference(demodulation,[status(thm)],[c_3722,c_3738]) ).
tcf(c_3743,plain,
op1(e13,op1(e12,e10)) = op1(e11,e10),
inference(demodulation,[status(thm)],[c_121,c_3738]) ).
tcf(c_3744,plain,
op1(e13,op1(e12,e11)) = op1(e11,e11),
inference(demodulation,[status(thm)],[c_122,c_3738]) ).
tcf(c_3745,plain,
op1(e11,e13) = op1(e13,e11),
inference(demodulation,[status(thm)],[c_3718,c_3738]) ).
tcf(c_3752,plain,
op1(op1(e12,e11),e11) = op1(e13,op1(e11,e13)),
inference(demodulation,[status(thm)],[c_3729,c_3745]) ).
tcf(c_3753,plain,
op1(e12,op1(e11,e13)) = op1(e11,e11),
inference(demodulation,[status(thm)],[c_3723,c_3745]) ).
tcf(c_3762,plain,
op1(op1(e12,e11),e13) = op1(e11,e11),
inference(demodulation,[status(thm)],[c_3731,c_3744]) ).
tcf(c_3763,plain,
op1(e10,e13) = op1(e11,e11),
inference(demodulation,[status(thm)],[c_3762,c_3742]) ).
tcf(c_3764,plain,
op1(e11,e11) = op1(e13,e10),
inference(demodulation,[status(thm)],[c_3744,c_3742]) ).
tcf(c_3765,plain,
op1(e13,op1(e11,e13)) = op1(e10,e11),
inference(demodulation,[status(thm)],[c_3752,c_3742]) ).
tcf(c_3766,plain,
op1(e11,e13) = op1(e12,e10),
inference(demodulation,[status(thm)],[c_3726,c_3742]) ).
tcf(c_3771,plain,
op1(e13,e13) = e10,
inference(demodulation,[status(thm)],[c_3725,c_3742]) ).
tcf(c_3774,plain,
op1(e12,e10) != e10,
inference(demodulation,[status(thm)],[c_333,c_3742]) ).
tcf(c_3777,plain,
op1(e12,op1(e12,e10)) = op1(e11,e11),
inference(demodulation,[status(thm)],[c_3753,c_3766]) ).
tcf(c_3784,plain,
op1(e12,e10) = op1(e13,e11),
inference(demodulation,[status(thm)],[c_3745,c_3766]) ).
tcf(c_3791,plain,
op1(e10,e11) = op1(e11,e10),
inference(light_normalisation,[status(thm)],[c_3765,c_3743,c_3766]) ).
tcf(c_3794,plain,
op1(e13,op1(e12,e10)) = op1(e10,e11),
inference(demodulation,[status(thm)],[c_3743,c_3791]) ).
tcf(c_3823,plain,
op1(e10,e13) = op1(e13,e10),
inference(demodulation,[status(thm)],[c_3764,c_3763]) ).
tcf(c_3824,plain,
op1(e12,op1(e12,e10)) = op1(e10,e13),
inference(demodulation,[status(thm)],[c_3777,c_3763]) ).
tcf(c_3829,plain,
op1(e10,e12) = op1(e12,e10),
inference(light_normalisation,[status(thm)],[c_3740,c_3742,c_3784]) ).
tcf(c_3844,plain,
op1(e12,op1(e10,e11)) = op1(e10,e10),
inference(light_normalisation,[status(thm)],[c_101,c_3742,c_3791]) ).
tcf(c_3966,plain,
( ( op2(e22,e20) = e23 )
| ( op2(e22,e20) = e22 )
| ( op2(e22,e20) = e21 )
| ( op2(e22,e20) = e20 ) ),
inference(light_normalisation,[status(thm)],[c_163,c_3621]) ).
tcf(c_3967,plain,
op2(e22,e20) = e22,
inference(forward_subsumption_resolution,[status(thm)],[c_3966,c_3369,c_3368,c_3622]) ).
tcf(c_3976,plain,
op2(e22,e22) = h2(e13),
inference(demodulation,[status(thm)],[c_3617,c_3967]) ).
tcf(c_3978,plain,
op2(e23,e21) = e22,
inference(demodulation,[status(thm)],[c_3621,c_3967]) ).
tcf(c_3981,plain,
op2(e21,e23) = e22,
inference(demodulation,[status(thm)],[c_3572,c_3967]) ).
tcf(c_3985,plain,
h2(e13) = e23,
inference(light_normalisation,[status(thm)],[c_3976,c_539]) ).
tcf(c_3994,plain,
op2(e20,e21) = op2(e23,e22),
inference(demodulation,[status(thm)],[c_3649,c_3985]) ).
tcf(c_3996,plain,
op2(e23,e23) = h1(e13),
inference(demodulation,[status(thm)],[c_3652,c_3985]) ).
tcf(c_3997,plain,
op2(e20,e23) = e23,
inference(demodulation,[status(thm)],[c_3654,c_3985]) ).
tcf(c_4000,plain,
op2(e23,e20) = e23,
inference(demodulation,[status(thm)],[c_3661,c_3985]) ).
tcf(c_4004,plain,
op2(e21,e23) = h2(e11),
inference(demodulation,[status(thm)],[c_3360,c_3985]) ).
tcf(c_4005,plain,
( ~ sP6
| ( e23 != e23 ) ),
inference(demodulation,[status(thm)],[c_698,c_3985]) ).
tcf(c_4006,plain,
op2(e21,e21) = e23,
inference(demodulation,[status(thm)],[c_442,c_3985]) ).
tcf(c_4007,plain,
~ sP6,
inference(equality_resolution_simp,[status(thm)],[c_4005]) ).
tcf(c_4008,plain,
h2(e11) = e22,
inference(light_normalisation,[status(thm)],[c_4004,c_3981]) ).
tcf(c_4009,plain,
op2(h1(e13),e22) = e22,
inference(demodulation,[status(thm)],[c_3715,c_4008]) ).
tcf(c_4013,plain,
op2(e22,e21) = h2(e10),
inference(demodulation,[status(thm)],[c_3417,c_4008]) ).
tcf(c_4014,plain,
( ~ sP7
| ( e22 != e22 ) ),
inference(demodulation,[status(thm)],[c_678,c_4008]) ).
tcf(c_4015,plain,
~ sP7,
inference(equality_resolution_simp,[status(thm)],[c_4014]) ).
tcf(c_4016,plain,
h2(e10) = e20,
inference(light_normalisation,[status(thm)],[c_4013,c_3571]) ).
tcf(c_4017,plain,
h1(e13) = e20,
inference(light_normalisation,[status(thm)],[c_3996,c_3581]) ).
tcf(c_4019,plain,
op2(e20,e22) = e22,
inference(demodulation,[status(thm)],[c_4009,c_4017]) ).
tcf(c_4033,plain,
op2(e20,e20) = e20,
inference(demodulation,[status(thm)],[c_438,c_4017]) ).
tcf(c_4045,plain,
op2(e20,e21) = e21,
inference(light_normalisation,[status(thm)],[c_3994,c_3537]) ).
tcf(c_4054,plain,
op2(e21,e20) = e21,
inference(demodulation,[status(thm)],[c_3637,c_4045]) ).
tcf(c_4067,plain,
( ( op1(e12,e10) = e13 )
| ( op1(e12,e10) = e12 )
| ( op1(e12,e10) = e11 )
| ( op1(e12,e10) = e10 ) ),
inference(light_normalisation,[status(thm)],[c_62,c_3784]) ).
tcf(c_4068,plain,
op1(e12,e10) = e12,
inference(forward_subsumption_resolution,[status(thm)],[c_4067,c_3394,c_3393,c_3774]) ).
tcf(c_4072,plain,
op1(e10,e12) = e12,
inference(demodulation,[status(thm)],[c_3829,c_4068]) ).
tcf(c_4074,plain,
op1(e10,e13) = op1(e12,e12),
inference(demodulation,[status(thm)],[c_3824,c_4068]) ).
tcf(c_4077,plain,
op1(e10,e11) = op1(e13,e12),
inference(demodulation,[status(thm)],[c_3794,c_4068]) ).
tcf(c_4079,plain,
op1(e13,e11) = e12,
inference(demodulation,[status(thm)],[c_3784,c_4068]) ).
tcf(c_4081,plain,
op1(e11,e13) = e12,
inference(demodulation,[status(thm)],[c_3766,c_4068]) ).
tcf(c_4086,plain,
op1(e10,e11) = e11,
inference(light_normalisation,[status(thm)],[c_4077,c_3738]) ).
tcf(c_4096,plain,
op1(e10,e10) = op1(e12,e11),
inference(demodulation,[status(thm)],[c_3844,c_4086]) ).
tcf(c_4099,plain,
op1(e11,e10) = e11,
inference(demodulation,[status(thm)],[c_3791,c_4086]) ).
tcf(c_4103,plain,
op1(e10,e10) = e10,
inference(light_normalisation,[status(thm)],[c_4096,c_3742]) ).
tcf(c_4126,plain,
op1(e10,e13) = e13,
inference(light_normalisation,[status(thm)],[c_4074,c_541]) ).
tcf(c_4136,plain,
op1(e13,e10) = e13,
inference(demodulation,[status(thm)],[c_3823,c_4126]) ).
tcf(c_4137,plain,
op1(e11,e11) = e13,
inference(demodulation,[status(thm)],[c_3763,c_4126]) ).
tcf(c_4163,plain,
( sP6
| sP7
| ( e23 != e23 )
| ( e22 != e22 )
| ( e21 != e21 )
| ( e20 != e20 )
| ( h2(e10) != e20 ) ),
inference(light_normalisation,[status(thm)],[c_570,c_541,c_539,c_439,c_3354,c_3355,c_3401,c_3408,c_3537,c_3571,c_3581,c_3738,c_3742,c_3771,c_3967,c_4019,c_3978,c_3981,c_3985,c_3997,c_4000,c_4006,c_4008,c_4016,c_4033,c_4045,c_4054,c_4068,c_4072,c_4079,c_4081,c_4086,c_4099,c_4103,c_4126,c_4136,c_4137]) ).
tcf(c_4164,plain,
( sP6
| sP7
| ( h2(e10) != e20 ) ),
inference(equality_resolution_simp,[status(thm)],[c_4163]) ).
tcf(c_4165,plain,
( sP6
| sP7
| ( e20 != e20 ) ),
inference(demodulation,[status(thm)],[c_4164,c_4016]) ).
tcf(c_4166,plain,
( sP6
| sP7 ),
inference(equality_resolution_simp,[status(thm)],[c_4165]) ).
tcf(c_4167,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_4166,c_4007,c_4015]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG016+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Fri Sep 25 04:32:05 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.03/0.32 Running first-order theorem proving
% 0.03/0.32 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.33
% 0.03/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.03/0.33
% 0.03/0.33 % Detected problem language: tptp
% 0.07/0.33 % Proving...
% 1.04/0.96 % SZS status Started for theBenchmark.p
% 1.04/0.96 % SZS status Theorem for theBenchmark.p
% 1.04/0.96
% 1.04/0.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.04/0.96
% 1.04/0.96 % ------ iProver source info
% 1.04/0.96
% 1.04/0.96 % git: date: 2026-07-19 20:42:38 +0200
% 1.04/0.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.04/0.96 % git: non_committed_changes: false
% 1.04/0.96
% 1.04/0.96 % ------ Parsing...
% 1.04/0.96 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.04/0.96
% 1.04/0.96 % ------ Preprocessing...%
% 1.04/0.96
% 1.04/0.96 % SZS status Theorem for theBenchmark.p
% 1.04/0.96
% 1.04/0.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.04/0.97
% 1.04/0.97
%------------------------------------------------------------------------------