%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : ALG192+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:47:55 AM UTC 2026
% Result : Unsatisfiable 29.71s 13.57s
% Output : CNFRefutation 29.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 122
% Number of leaves : 12
% Syntax : Number of formulae : 291 ( 66 unt; 0 def)
% Number of atoms : 1553 (1552 equ)
% Maximal formula atoms : 250 ( 5 avg)
% Number of connectives : 1562 ( 300 ~;1021 |; 241 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax1,axiom,
( ( op(e4,e4) = e4
| op(e4,e4) = e3
| op(e4,e4) = e2
| op(e4,e4) = e1
| op(e4,e4) = e0 )
& ( op(e4,e3) = e4
| op(e4,e3) = e3
| op(e4,e3) = e2
| op(e4,e3) = e1
| op(e4,e3) = e0 )
& ( op(e4,e2) = e4
| op(e4,e2) = e3
| op(e4,e2) = e2
| op(e4,e2) = e1
| op(e4,e2) = e0 )
& ( op(e4,e1) = e4
| op(e4,e1) = e3
| op(e4,e1) = e2
| op(e4,e1) = e1
| op(e4,e1) = e0 )
& ( op(e4,e0) = e4
| op(e4,e0) = e3
| op(e4,e0) = e2
| op(e4,e0) = e1
| op(e4,e0) = e0 )
& ( op(e3,e4) = e4
| op(e3,e4) = e3
| op(e3,e4) = e2
| op(e3,e4) = e1
| op(e3,e4) = e0 )
& ( op(e3,e3) = e4
| op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e4
| op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e4
| op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e4
| op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e4) = e4
| op(e2,e4) = e3
| op(e2,e4) = e2
| op(e2,e4) = e1
| op(e2,e4) = e0 )
& ( op(e2,e3) = e4
| op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e4
| op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e4
| op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e4
| op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e4) = e4
| op(e1,e4) = e3
| op(e1,e4) = e2
| op(e1,e4) = e1
| op(e1,e4) = e0 )
& ( op(e1,e3) = e4
| op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e4
| op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e4
| op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e4
| op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e4) = e2
| op(e0,e4) = e1
| op(e0,e4) = e0 )
& ( op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e4
| op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ) ).
fof(ax2,axiom,
( ( op(e4,e4) = e4
| op(e3,e4) = e4
| op(e2,e4) = e4
| op(e1,e4) = e4
| op(e0,e4) = e4 )
& ( op(e4,e4) = e4
| op(e4,e3) = e4
| op(e4,e2) = e4
| op(e4,e1) = e4
| op(e4,e0) = e4 )
& ( op(e4,e4) = e3
| op(e3,e4) = e3
| op(e2,e4) = e3
| op(e1,e4) = e3
| op(e0,e4) = e3 )
& ( op(e4,e4) = e3
| op(e4,e3) = e3
| op(e4,e2) = e3
| op(e4,e1) = e3
| op(e4,e0) = e3 )
& ( op(e4,e4) = e2
| op(e3,e4) = e2
| op(e2,e4) = e2
| op(e1,e4) = e2
| op(e0,e4) = e2 )
& ( op(e4,e4) = e2
| op(e4,e3) = e2
| op(e4,e2) = e2
| op(e4,e1) = e2
| op(e4,e0) = e2 )
& ( op(e4,e4) = e1
| op(e3,e4) = e1
| op(e2,e4) = e1
| op(e1,e4) = e1
| op(e0,e4) = e1 )
& ( op(e4,e4) = e1
| op(e4,e3) = e1
| op(e4,e2) = e1
| op(e4,e1) = e1
| op(e4,e0) = e1 )
& ( op(e4,e4) = e0
| op(e3,e4) = e0
| op(e2,e4) = e0
| op(e1,e4) = e0
| op(e0,e4) = e0 )
& ( op(e4,e4) = e0
| op(e4,e3) = e0
| op(e4,e2) = e0
| op(e4,e1) = e0
| op(e4,e0) = e0 )
& ( op(e4,e3) = e4
| op(e3,e3) = e4
| op(e2,e3) = e4
| op(e1,e3) = e4
| op(e0,e3) = e4 )
& ( op(e3,e4) = e4
| op(e3,e3) = e4
| op(e3,e2) = e4
| op(e3,e1) = e4
| op(e3,e0) = e4 )
& ( op(e4,e3) = e3
| op(e3,e3) = e3
| op(e2,e3) = e3
| op(e1,e3) = e3
| op(e0,e3) = e3 )
& ( op(e3,e4) = e3
| op(e3,e3) = e3
| op(e3,e2) = e3
| op(e3,e1) = e3
| op(e3,e0) = e3 )
& ( op(e4,e3) = e2
| op(e3,e3) = e2
| op(e2,e3) = e2
| op(e1,e3) = e2
| op(e0,e3) = e2 )
& ( op(e3,e4) = e2
| op(e3,e3) = e2
| op(e3,e2) = e2
| op(e3,e1) = e2
| op(e3,e0) = e2 )
& ( op(e4,e3) = e1
| op(e3,e3) = e1
| op(e2,e3) = e1
| op(e1,e3) = e1
| op(e0,e3) = e1 )
& ( op(e3,e4) = e1
| op(e3,e3) = e1
| op(e3,e2) = e1
| op(e3,e1) = e1
| op(e3,e0) = e1 )
& ( op(e4,e3) = e0
| op(e3,e3) = e0
| op(e2,e3) = e0
| op(e1,e3) = e0
| op(e0,e3) = e0 )
& ( op(e3,e4) = e0
| op(e3,e3) = e0
| op(e3,e2) = e0
| op(e3,e1) = e0
| op(e3,e0) = e0 )
& ( op(e4,e2) = e4
| op(e3,e2) = e4
| op(e2,e2) = e4
| op(e1,e2) = e4
| op(e0,e2) = e4 )
& ( op(e2,e4) = e4
| op(e2,e3) = e4
| op(e2,e2) = e4
| op(e2,e1) = e4
| op(e2,e0) = e4 )
& ( op(e4,e2) = e3
| op(e3,e2) = e3
| op(e2,e2) = e3
| op(e1,e2) = e3
| op(e0,e2) = e3 )
& ( op(e2,e4) = e3
| op(e2,e3) = e3
| op(e2,e2) = e3
| op(e2,e1) = e3
| op(e2,e0) = e3 )
& ( op(e4,e2) = e2
| op(e3,e2) = e2
| op(e2,e2) = e2
| op(e1,e2) = e2
| op(e0,e2) = e2 )
& ( op(e2,e4) = e2
| op(e2,e3) = e2
| op(e2,e2) = e2
| op(e2,e1) = e2
| op(e2,e0) = e2 )
& ( op(e4,e2) = e1
| op(e3,e2) = e1
| op(e2,e2) = e1
| op(e1,e2) = e1
| op(e0,e2) = e1 )
& ( op(e2,e4) = e1
| op(e2,e3) = e1
| op(e2,e2) = e1
| op(e2,e1) = e1
| op(e2,e0) = e1 )
& ( op(e4,e2) = e0
| op(e3,e2) = e0
| op(e2,e2) = e0
| op(e1,e2) = e0
| op(e0,e2) = e0 )
& ( op(e2,e4) = e0
| op(e2,e3) = e0
| op(e2,e2) = e0
| op(e2,e1) = e0
| op(e2,e0) = e0 )
& ( op(e4,e1) = e4
| op(e3,e1) = e4
| op(e2,e1) = e4
| op(e1,e1) = e4
| op(e0,e1) = e4 )
& ( op(e1,e4) = e4
| op(e1,e3) = e4
| op(e1,e2) = e4
| op(e1,e1) = e4
| op(e1,e0) = e4 )
& ( op(e4,e1) = e3
| op(e3,e1) = e3
| op(e2,e1) = e3
| op(e1,e1) = e3
| op(e0,e1) = e3 )
& ( op(e1,e4) = e3
| op(e1,e3) = e3
| op(e1,e2) = e3
| op(e1,e1) = e3
| op(e1,e0) = e3 )
& ( op(e4,e1) = e2
| op(e3,e1) = e2
| op(e2,e1) = e2
| op(e1,e1) = e2
| op(e0,e1) = e2 )
& ( op(e1,e4) = e2
| op(e1,e3) = e2
| op(e1,e2) = e2
| op(e1,e1) = e2
| op(e1,e0) = e2 )
& ( op(e4,e1) = e1
| op(e3,e1) = e1
| op(e2,e1) = e1
| op(e1,e1) = e1
| op(e0,e1) = e1 )
& ( op(e1,e4) = e1
| op(e1,e3) = e1
| op(e1,e2) = e1
| op(e1,e1) = e1
| op(e1,e0) = e1 )
& ( op(e4,e1) = e0
| op(e3,e1) = e0
| op(e2,e1) = e0
| op(e1,e1) = e0
| op(e0,e1) = e0 )
& ( op(e1,e4) = e0
| op(e1,e3) = e0
| op(e1,e2) = e0
| op(e1,e1) = e0
| op(e1,e0) = e0 )
& ( op(e4,e0) = e4
| op(e3,e0) = e4
| op(e2,e0) = e4
| op(e1,e0) = e4
| op(e0,e0) = e4 )
& ( op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4
| op(e0,e0) = e4 )
& ( op(e4,e0) = e3
| op(e3,e0) = e3
| op(e2,e0) = e3
| op(e1,e0) = e3
| op(e0,e0) = e3 )
& ( op(e0,e4) = e3
| op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 )
& ( op(e4,e0) = e2
| op(e3,e0) = e2
| op(e2,e0) = e2
| op(e1,e0) = e2
| op(e0,e0) = e2 )
& ( op(e0,e4) = e2
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e1) = e2
| op(e0,e0) = e2 )
& ( op(e4,e0) = e1
| op(e3,e0) = e1
| op(e2,e0) = e1
| op(e1,e0) = e1
| op(e0,e0) = e1 )
& ( op(e0,e4) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e1) = e1
| op(e0,e0) = e1 )
& ( op(e4,e0) = e0
| op(e3,e0) = e0
| op(e2,e0) = e0
| op(e1,e0) = e0
| op(e0,e0) = e0 )
& ( op(e0,e4) = e0
| op(e0,e3) = e0
| op(e0,e2) = e0
| op(e0,e1) = e0
| op(e0,e0) = e0 ) ) ).
fof(ax3,axiom,
( op(op(e4,e4),op(e4,e4)) = e4
& op(op(e3,e4),op(e4,e3)) = e4
& op(op(e2,e4),op(e4,e2)) = e4
& op(op(e1,e4),op(e4,e1)) = e4
& op(op(e0,e4),op(e4,e0)) = e4
& op(op(e4,e3),op(e3,e4)) = e3
& op(op(e3,e3),op(e3,e3)) = e3
& op(op(e2,e3),op(e3,e2)) = e3
& op(op(e1,e3),op(e3,e1)) = e3
& op(op(e0,e3),op(e3,e0)) = e3
& op(op(e4,e2),op(e2,e4)) = e2
& op(op(e3,e2),op(e2,e3)) = e2
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e1,e2),op(e2,e1)) = e2
& op(op(e0,e2),op(e2,e0)) = e2
& op(op(e4,e1),op(e1,e4)) = e1
& op(op(e3,e1),op(e1,e3)) = e1
& op(op(e2,e1),op(e1,e2)) = e1
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e0,e1),op(e1,e0)) = e1
& op(op(e4,e0),op(e0,e4)) = e0
& op(op(e3,e0),op(e0,e3)) = e0
& op(op(e2,e0),op(e0,e2)) = e0
& op(op(e1,e0),op(e0,e1)) = e0
& op(op(e0,e0),op(e0,e0)) = e0 ) ).
fof(ax4,axiom,
( op(e4,e3) != op(e4,e4)
& op(e4,e2) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e2)
& op(e4,e0) != op(e4,e4)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e1)
& op(e3,e3) != op(e3,e4)
& op(e3,e2) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e4)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e3) != op(e2,e4)
& op(e2,e2) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e4)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e3) != op(e1,e4)
& op(e1,e2) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e4)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e3) != op(e0,e4)
& op(e0,e2) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e4)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e3,e4) != op(e4,e4)
& op(e2,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e2,e4)
& op(e0,e4) != op(e4,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e1,e4)
& op(e3,e3) != op(e4,e3)
& op(e2,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e4,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e3,e2) != op(e4,e2)
& op(e2,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e4,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e3,e1) != op(e4,e1)
& op(e2,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e4,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e3,e0) != op(e4,e0)
& op(e2,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e4,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ) ).
fof(ax5,axiom,
( e3 != e4
& e2 != e4
& e2 != e3
& e1 != e4
& e1 != e3
& e1 != e2
& e0 != e4
& e0 != e3
& e0 != e2
& e0 != e1 ) ).
fof(ax6,axiom,
( op(e4,op(e4,e4)) = e4
& op(e4,op(e4,e3)) = e3
& op(e4,op(e4,e2)) = e2
& op(e4,op(e4,e1)) = e1
& op(e4,op(e4,e0)) = e0
& op(e3,op(e3,e4)) = e4
& op(e3,op(e3,e3)) = e3
& op(e3,op(e3,e2)) = e2
& op(e3,op(e3,e1)) = e1
& op(e3,op(e3,e0)) = e0
& op(e2,op(e2,e4)) = e4
& op(e2,op(e2,e3)) = e3
& op(e2,op(e2,e2)) = e2
& op(e2,op(e2,e1)) = e1
& op(e2,op(e2,e0)) = e0
& op(e1,op(e1,e4)) = e4
& op(e1,op(e1,e3)) = e3
& op(e1,op(e1,e2)) = e2
& op(e1,op(e1,e1)) = e1
& op(e1,op(e1,e0)) = e0
& op(e0,op(e0,e4)) = e4
& op(e0,op(e0,e3)) = e3
& op(e0,op(e0,e2)) = e2
& op(e0,op(e0,e1)) = e1
& op(e0,op(e0,e0)) = e0 ) ).
fof(ax41,axiom,
~ ( e3 = op(e0,e2)
& e4 = op(e0,op(op(e0,e2),e0))
& e1 = op(op(e0,e2),e0) ) ).
fof(ax51,axiom,
~ ( e3 = op(e0,e4)
& e2 = op(e0,op(op(e0,e4),e0))
& e1 = op(op(e0,e4),e0) ) ).
fof(ax53,axiom,
~ ( e2 = op(e0,e4)
& e3 = op(e0,op(op(e0,e4),e0))
& e1 = op(op(e0,e4),e0) ) ).
fof(ax101,axiom,
~ ( e1 = op(e0,e4)
& e2 = op(e0,op(op(e0,e4),e0))
& e3 = op(op(e0,e4),e0) ) ).
fof(ax111,axiom,
~ ( e3 = op(e0,e1)
& e2 = op(e0,op(op(e0,e1),e0))
& e4 = op(op(e0,e1),e0) ) ).
fof(ax113,axiom,
~ ( e2 = op(e0,e1)
& e3 = op(e0,op(op(e0,e1),e0))
& e4 = op(op(e0,e1),e0) ) ).
cnf(c0,plain,
( op(e0,e0) = e1
| op(e0,e0) = e0
| op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3 ),
inference(clausification,[status(esa)],[ax1]) ).
cnf(c1,plain,
( op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0
| op(e0,e1) = e3
| op(e0,e1) = e4 ),
inference(clausification,[status(esa)],[ax1]) ).
cnf(c28,plain,
( op(e3,e0) = e1
| op(e0,e0) = e1
| op(e1,e0) = e1
| op(e4,e0) = e1
| op(e2,e0) = e1 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c29,plain,
( op(e0,e1) = e2
| op(e0,e0) = e2
| op(e0,e4) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c31,plain,
( op(e0,e3) = e3
| op(e0,e2) = e3
| op(e0,e4) = e3
| op(e0,e1) = e3
| op(e0,e0) = e3 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c33,plain,
( op(e0,e0) = e4
| op(e0,e4) = e4
| op(e0,e3) = e4
| op(e0,e2) = e4
| op(e0,e1) = e4 ),
inference(clausification,[status(esa)],[ax2]) ).
cnf(c75,plain,
op(op(e0,e0),op(e0,e0)) = e0,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c76,plain,
op(op(e1,e0),op(e0,e1)) = e0,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c77,plain,
op(op(e2,e0),op(e0,e2)) = e0,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c78,plain,
op(op(e3,e0),op(e0,e3)) = e0,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c79,plain,
op(op(e4,e0),op(e0,e4)) = e0,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c80,plain,
op(op(e0,e1),op(e1,e0)) = e1,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c81,plain,
op(op(e1,e1),op(e1,e1)) = e1,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c85,plain,
op(op(e0,e2),op(e2,e0)) = e2,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c90,plain,
op(op(e0,e3),op(e3,e0)) = e3,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c95,plain,
op(op(e0,e4),op(e4,e0)) = e4,
inference(clausification,[status(esa)],[ax3]) ).
cnf(c110,plain,
op(e0,e1) != op(e1,e1),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c121,plain,
op(e0,e2) != op(e2,e2),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c132,plain,
op(e0,e3) != op(e3,e3),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c143,plain,
op(e0,e4) != op(e4,e4),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c150,plain,
op(e0,e0) != op(e0,e1),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c154,plain,
op(e0,e1) != op(e0,e2),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c155,plain,
op(e0,e1) != op(e0,e3),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c156,plain,
op(e0,e1) != op(e0,e4),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c158,plain,
op(e0,e2) != op(e0,e4),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c159,plain,
op(e0,e3) != op(e0,e4),
inference(clausification,[status(esa)],[ax4]) ).
cnf(c200,plain,
e0 != e1,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c201,plain,
e0 != e2,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c202,plain,
e0 != e3,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c203,plain,
e0 != e4,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c204,plain,
e1 != e2,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c206,plain,
e1 != e4,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c207,plain,
e2 != e3,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c208,plain,
e2 != e4,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c209,plain,
e3 != e4,
inference(clausification,[status(esa)],[ax5]) ).
cnf(c210,plain,
op(e0,op(e0,e0)) = e0,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c211,plain,
op(e0,op(e0,e1)) = e1,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c212,plain,
op(e0,op(e0,e2)) = e2,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c213,plain,
op(e0,op(e0,e3)) = e3,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c214,plain,
op(e0,op(e0,e4)) = e4,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c215,plain,
op(e1,op(e1,e0)) = e0,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c217,plain,
op(e1,op(e1,e2)) = e2,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c218,plain,
op(e1,op(e1,e3)) = e3,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c219,plain,
op(e1,op(e1,e4)) = e4,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c220,plain,
op(e2,op(e2,e0)) = e0,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c221,plain,
op(e2,op(e2,e1)) = e1,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c223,plain,
op(e2,op(e2,e3)) = e3,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c224,plain,
op(e2,op(e2,e4)) = e4,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c227,plain,
op(e3,op(e3,e2)) = e2,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c229,plain,
op(e3,op(e3,e4)) = e4,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c230,plain,
op(e4,op(e4,e0)) = e0,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c233,plain,
op(e4,op(e4,e3)) = e3,
inference(clausification,[status(esa)],[ax6]) ).
cnf(c269,plain,
( e3 != op(e0,e2)
| e4 != op(e0,op(op(e0,e2),e0))
| e1 != op(op(e0,e2),e0) ),
inference(clausification,[status(esa)],[ax41]) ).
cnf(c279,plain,
( e3 != op(e0,e4)
| e2 != op(e0,op(op(e0,e4),e0))
| e1 != op(op(e0,e4),e0) ),
inference(clausification,[status(esa)],[ax51]) ).
cnf(c281,plain,
( e2 != op(e0,e4)
| e3 != op(e0,op(op(e0,e4),e0))
| e1 != op(op(e0,e4),e0) ),
inference(clausification,[status(esa)],[ax53]) ).
cnf(c329,plain,
( e1 != op(e0,e4)
| e2 != op(e0,op(op(e0,e4),e0))
| e3 != op(op(e0,e4),e0) ),
inference(clausification,[status(esa)],[ax101]) ).
cnf(c339,plain,
( e3 != op(e0,e1)
| e2 != op(e0,op(op(e0,e1),e0))
| e4 != op(op(e0,e1),e0) ),
inference(clausification,[status(esa)],[ax111]) ).
cnf(c341,plain,
( e2 != op(e0,e1)
| e3 != op(e0,op(op(e0,e1),e0))
| e4 != op(op(e0,e1),e0) ),
inference(clausification,[status(esa)],[ax113]) ).
cnf(d0,plain,
( op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e1,op(e0,e0)) = e0 ),
inference(superposition,[status(thm)],[c0,c75]) ).
cnf(d1,plain,
( op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[c0,d0]) ).
cnf(d2,plain,
( op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e1) != e0 ),
inference(superposition,[status(thm)],[d1,c110]) ).
cnf(d3,plain,
( op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e1) = e0 ),
inference(superposition,[status(thm)],[c0,c210]) ).
cnf(d4,plain,
( op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| e0 != e0 ),
inference(superposition,[status(thm)],[d3,d2]) ).
cnf(d5,plain,
( op(e0,e0) = e4
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0 ),
inference(equality_resolution,[status(thm)],[d4]) ).
cnf(d6,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(op(e0,e0),e4) = e0 ),
inference(superposition,[status(thm)],[d5,c75]) ).
cnf(d7,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e4,e4) = e0 ),
inference(superposition,[status(thm)],[d5,d6]) ).
cnf(d8,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e4) != e0 ),
inference(superposition,[status(thm)],[d7,c143]) ).
cnf(d9,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e4) = e0 ),
inference(superposition,[status(thm)],[d5,c210]) ).
cnf(d10,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0
| e0 != e0 ),
inference(superposition,[status(thm)],[d9,d8]) ).
cnf(d11,plain,
( op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e0 ),
inference(equality_resolution,[status(thm)],[d10]) ).
cnf(d12,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0
| op(op(e0,e0),e2) = e0 ),
inference(superposition,[status(thm)],[d11,c75]) ).
cnf(d13,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e3
| op(e0,e0) = e0
| op(e2,e2) = e0 ),
inference(superposition,[status(thm)],[d11,d12]) ).
cnf(d14,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e2) != e0 ),
inference(superposition,[status(thm)],[d13,c121]) ).
cnf(d15,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e2) = e0 ),
inference(superposition,[status(thm)],[d11,c210]) ).
cnf(d16,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0
| op(e0,e0) = e3
| op(e0,e0) = e0
| e0 != e0 ),
inference(superposition,[status(thm)],[d15,d14]) ).
cnf(d17,plain,
( op(e0,e0) = e3
| op(e0,e0) = e0 ),
inference(equality_resolution,[status(thm)],[d16]) ).
cnf(d18,plain,
( op(e0,e0) = e0
| op(op(e0,e0),e3) = e0 ),
inference(superposition,[status(thm)],[d17,c75]) ).
cnf(d19,plain,
( op(e0,e0) = e0
| op(e0,e0) = e0
| op(e3,e3) = e0 ),
inference(superposition,[status(thm)],[d17,d18]) ).
cnf(d20,plain,
( op(e0,e0) = e0
| op(e0,e3) != e0 ),
inference(superposition,[status(thm)],[d19,c132]) ).
cnf(d21,plain,
( op(e0,e0) = e0
| op(e0,e3) = e0 ),
inference(superposition,[status(thm)],[d17,c210]) ).
cnf(d22,plain,
( op(e0,e0) = e0
| op(e0,e0) = e0
| e0 != e0 ),
inference(superposition,[status(thm)],[d21,d20]) ).
cnf(d23,plain,
op(e0,e0) = e0,
inference(equality_resolution,[status(thm)],[d22]) ).
cnf(d24,plain,
e0 != op(e0,e1),
inference(demodulation,[status(thm)],[c150,d23]) ).
cnf(d25,plain,
( op(e0,e1) = e4
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0
| op(e1,op(e1,e0)) = e1 ),
inference(superposition,[status(thm)],[c1,c80]) ).
cnf(d26,plain,
( e0 = e1
| op(e0,e1) = e4
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0 ),
inference(demodulation,[status(thm)],[d25,c215]) ).
cnf(d27,plain,
( op(e0,e1) = e4
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0 ),
inference(resolution,[status(thm)],[c200,d26]) ).
cnf(d28,plain,
( op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0
| e4 != op(e0,e3) ),
inference(superposition,[status(thm)],[d27,c155]) ).
cnf(d29,plain,
( op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e0) = e4
| op(e0,e4) = e1 ),
inference(superposition,[status(thm)],[c33,c211]) ).
cnf(d30,plain,
( op(e0,e4) = e1
| op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| e0 = e4 ),
inference(demodulation,[status(thm)],[d29,d23]) ).
cnf(d31,plain,
( op(e0,e4) = e1
| op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4 ),
inference(resolution,[status(thm)],[c203,d30]) ).
cnf(d32,plain,
( op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e3) != e1 ),
inference(superposition,[status(thm)],[d31,c159]) ).
cnf(d33,plain,
( op(e0,e4) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e0) = e2
| op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e0) = e4
| e2 = e4 ),
inference(superposition,[status(thm)],[c29,c33]) ).
cnf(d34,plain,
( op(e0,e4) = e4
| op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e0) = e4
| op(e0,e0) = e2 ),
inference(resolution,[status(thm)],[c208,d33]) ).
cnf(d35,plain,
( op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e0) = e4
| op(e0,e0) = e2
| op(e4,op(e4,e0)) = e4 ),
inference(superposition,[status(thm)],[d34,c95]) ).
cnf(d36,plain,
( op(e4,op(e4,e0)) = e4
| op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e0) = e4
| e0 = e2 ),
inference(demodulation,[status(thm)],[d35,d23]) ).
cnf(d37,plain,
( op(e4,op(e4,e0)) = e4
| op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e0 = e4
| e0 = e2 ),
inference(demodulation,[status(thm)],[d36,d23]) ).
cnf(d38,plain,
( e0 = e4
| op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e0 = e4
| e0 = e2 ),
inference(demodulation,[status(thm)],[d37,c230]) ).
cnf(d39,plain,
( e0 = e4
| op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e0 = e4 ),
inference(resolution,[status(thm)],[c201,d38]) ).
cnf(d40,plain,
( op(e0,e4) = e2
| op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c203,d39]) ).
cnf(d41,plain,
( op(e0,e2) = e4
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e2) = e4 ),
inference(superposition,[status(thm)],[d40,c214]) ).
cnf(d42,plain,
( op(e0,e1) = e2
| op(e0,e4) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| e0 = e2 ),
inference(demodulation,[status(thm)],[c29,d23]) ).
cnf(d43,plain,
( op(e0,e1) = e2
| op(e0,e4) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c201,d42]) ).
cnf(d44,plain,
( op(e0,e4) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e2) = e1 ),
inference(superposition,[status(thm)],[d43,c211]) ).
cnf(d45,plain,
( op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0
| op(e0,e4) = e1 ),
inference(superposition,[status(thm)],[d27,c211]) ).
cnf(d46,plain,
( op(e0,e1) = e3
| op(e0,e1) = e0
| op(e0,e4) = e1
| op(e0,e2) = e1 ),
inference(superposition,[status(thm)],[d45,c211]) ).
cnf(d47,plain,
( op(e0,e1) = e0
| op(e0,e4) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 ),
inference(superposition,[status(thm)],[d46,c211]) ).
cnf(d48,plain,
( op(e0,e4) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e0) != e0 ),
inference(superposition,[status(thm)],[d47,c150]) ).
cnf(d49,plain,
( op(e0,e4) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 ),
inference(resolution,[status(thm)],[d23,d48]) ).
cnf(d50,plain,
( op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e3) = e2
| e1 = e2 ),
inference(superposition,[status(thm)],[d49,d44]) ).
cnf(d51,plain,
( op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e3) = e1
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c204,d50]) ).
cnf(d52,plain,
( op(e0,e2) = e2
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e2) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e1 = e4 ),
inference(superposition,[status(thm)],[d51,d41]) ).
cnf(d53,plain,
( op(e0,e2) = e2
| op(e0,e3) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c206,d52]) ).
cnf(d54,plain,
( op(e0,e3) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e2,op(e2,e0)) = e2 ),
inference(superposition,[status(thm)],[d53,c85]) ).
cnf(d55,plain,
( e0 = e2
| op(e0,e3) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(demodulation,[status(thm)],[d54,c220]) ).
cnf(d56,plain,
( op(e0,e3) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c201,d55]) ).
cnf(d57,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| e1 != e1 ),
inference(superposition,[status(thm)],[d56,d32]) ).
cnf(d58,plain,
( op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d57]) ).
cnf(d59,plain,
( op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e4,op(e4,e0)) = e4 ),
inference(superposition,[status(thm)],[d58,c95]) ).
cnf(d60,plain,
( e0 = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(demodulation,[status(thm)],[d59,c230]) ).
cnf(d61,plain,
( op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c203,d60]) ).
cnf(d62,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e4) = e2 ),
inference(superposition,[status(thm)],[d61,c212]) ).
cnf(d63,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e1 != op(op(e0,e4),e0)
| e2 != op(e0,e4)
| e3 != op(e0,op(e2,e0)) ),
inference(superposition,[status(thm)],[d62,c281]) ).
cnf(d64,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != op(e0,e4)
| e3 != op(e0,op(e2,e0))
| op(e0,e3) = e4
| op(e0,e3) = e2
| e1 != op(e2,e0) ),
inference(superposition,[status(thm)],[d62,d63]) ).
cnf(d65,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(op(e3,e0),e1) = e0 ),
inference(superposition,[status(thm)],[d56,c78]) ).
cnf(d66,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e1) = e3 ),
inference(superposition,[status(thm)],[d56,c213]) ).
cnf(d67,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e4 != op(op(e0,e1),e0)
| e3 != op(e0,e1)
| e2 != op(e0,op(e3,e0)) ),
inference(superposition,[status(thm)],[d66,c339]) ).
cnf(d68,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != op(e0,op(e3,e0))
| e3 != op(e0,e1)
| op(e0,e3) = e4
| op(e0,e3) = e2
| e4 != op(e3,e0) ),
inference(superposition,[status(thm)],[d66,d67]) ).
cnf(d69,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e1,op(e3,e0)) = e3 ),
inference(superposition,[status(thm)],[d56,c90]) ).
cnf(d70,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(op(e2,e0),e4) = e0 ),
inference(superposition,[status(thm)],[d61,c77]) ).
cnf(d71,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(op(e4,e0),e2) = e0 ),
inference(superposition,[status(thm)],[d62,c79]) ).
cnf(d72,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(op(e1,e0),e3) = e0 ),
inference(superposition,[status(thm)],[d66,c76]) ).
cnf(d73,plain,
( op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[c28,c215]) ).
cnf(d74,plain,
( op(e1,e1) = e0
| op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| e0 = e1 ),
inference(demodulation,[status(thm)],[d73,d23]) ).
cnf(d75,plain,
( op(e1,e1) = e0
| op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 ),
inference(resolution,[status(thm)],[c200,d74]) ).
cnf(d76,plain,
( op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(op(e1,e1),e0) = e1 ),
inference(superposition,[status(thm)],[d75,c81]) ).
cnf(d77,plain,
( op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e0) = e1 ),
inference(superposition,[status(thm)],[d75,d76]) ).
cnf(d78,plain,
( op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| e0 = e1 ),
inference(demodulation,[status(thm)],[d77,d23]) ).
cnf(d79,plain,
( op(e4,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 ),
inference(resolution,[status(thm)],[c200,d78]) ).
cnf(d80,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e1,op(e0,e4)) = e0 ),
inference(superposition,[status(thm)],[d79,c79]) ).
cnf(d81,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e1,e2) = e0 ),
inference(superposition,[status(thm)],[d62,d80]) ).
cnf(d82,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e1,e0) = e2 ),
inference(superposition,[status(thm)],[d81,c217]) ).
cnf(d83,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e2,e3) = e0 ),
inference(superposition,[status(thm)],[d82,d72]) ).
cnf(d84,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e2,e0) = e3 ),
inference(superposition,[status(thm)],[d83,c223]) ).
cnf(d85,plain,
( op(e2,e0) = e3
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e1,e4) = e0 ),
inference(superposition,[status(thm)],[d84,d70]) ).
cnf(d86,plain,
( op(e2,e0) = e3
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e1,e0) = e4 ),
inference(superposition,[status(thm)],[d85,c219]) ).
cnf(d87,plain,
( op(e2,e0) = e3
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e4,e3) = e0 ),
inference(superposition,[status(thm)],[d86,d72]) ).
cnf(d88,plain,
( op(e2,e0) = e3
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e4,e0) = e3 ),
inference(superposition,[status(thm)],[d87,c233]) ).
cnf(d89,plain,
( op(e2,e0) = e3
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e3,e2) = e0 ),
inference(superposition,[status(thm)],[d88,d71]) ).
cnf(d90,plain,
( op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e3,e4) = e0 ),
inference(superposition,[status(thm)],[d89,d70]) ).
cnf(d91,plain,
( op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e3,e0) = e4 ),
inference(superposition,[status(thm)],[d90,c229]) ).
cnf(d92,plain,
( op(e3,e0) = e1
| op(e3,e0) = e4
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e3,e0) = e2 ),
inference(superposition,[status(thm)],[d91,c227]) ).
cnf(d93,plain,
( op(e3,e0) = e4
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e1,e1) = e3 ),
inference(superposition,[status(thm)],[d92,d69]) ).
cnf(d94,plain,
( op(e3,e0) = e4
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[d92,d65]) ).
cnf(d95,plain,
( op(e3,e0) = e4
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e3,e0) = e4
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e0 = e3 ),
inference(superposition,[status(thm)],[d94,d93]) ).
cnf(d96,plain,
( op(e3,e0) = e4
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c202,d95]) ).
cnf(d97,plain,
( op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e4 != op(e3,e0)
| e3 != op(e0,e1)
| op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != op(e0,e4) ),
inference(superposition,[status(thm)],[d96,d68]) ).
cnf(d98,plain,
( op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != op(e0,e4)
| e3 != op(e0,e1)
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e4 != e4 ),
inference(superposition,[status(thm)],[d96,d97]) ).
cnf(d99,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e4 != e4
| e3 != op(e0,e1)
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != e2 ),
inference(superposition,[status(thm)],[d62,d98]) ).
cnf(d100,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e4 != e4
| e2 != e2
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e3 != e3 ),
inference(superposition,[status(thm)],[d66,d99]) ).
cnf(d101,plain,
( e2 != e2
| e3 != e3
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d100]) ).
cnf(d102,plain,
( e3 != e3
| op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d101]) ).
cnf(d103,plain,
( op(e3,e0) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d102]) ).
cnf(d104,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| op(e2,e1) = e0 ),
inference(superposition,[status(thm)],[d103,d65]) ).
cnf(d105,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| op(e2,e0) = e1 ),
inference(superposition,[status(thm)],[d104,c221]) ).
cnf(d106,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e1 != op(e2,e0)
| e2 != op(e0,e4)
| op(e0,e3) = e4
| op(e0,e3) = e2
| e3 != op(e0,e1) ),
inference(superposition,[status(thm)],[d105,d64]) ).
cnf(d107,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != op(e0,e4)
| e3 != op(e0,e1)
| op(e0,e3) = e4
| op(e0,e3) = e2
| e1 != e1 ),
inference(superposition,[status(thm)],[d105,d106]) ).
cnf(d108,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e1 != e1
| e3 != op(e0,e1)
| op(e0,e3) = e4
| op(e0,e3) = e2
| e2 != e2 ),
inference(superposition,[status(thm)],[d62,d107]) ).
cnf(d109,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2
| e1 != e1
| e2 != e2
| op(e0,e3) = e4
| op(e0,e3) = e2
| e3 != e3 ),
inference(superposition,[status(thm)],[d66,d108]) ).
cnf(d110,plain,
( e2 != e2
| e3 != e3
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d109]) ).
cnf(d111,plain,
( e3 != e3
| op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d110]) ).
cnf(d112,plain,
( op(e0,e3) = e4
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d111]) ).
cnf(d113,plain,
( op(e0,e3) = e2
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0
| e4 != e4 ),
inference(superposition,[status(thm)],[d112,d28]) ).
cnf(d114,plain,
( op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e0
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d113]) ).
cnf(d115,plain,
( op(e0,e1) = e3
| op(e0,e1) = e0
| op(e0,e3) = e2
| op(e0,e2) = e1 ),
inference(superposition,[status(thm)],[d114,c211]) ).
cnf(d116,plain,
( op(e0,e1) = e0
| op(e0,e2) = e1
| op(e0,e3) = e2
| e3 != op(e0,e4) ),
inference(superposition,[status(thm)],[d115,c156]) ).
cnf(d117,plain,
( op(e0,e3) = e2
| op(e0,e4) = e3 ),
inference(superposition,[status(thm)],[d112,c213]) ).
cnf(d118,plain,
( op(e0,e3) = e2
| op(e0,e1) = e0
| op(e0,e2) = e1
| op(e0,e3) = e2
| e3 != e3 ),
inference(superposition,[status(thm)],[d117,d116]) ).
cnf(d119,plain,
( op(e0,e1) = e0
| op(e0,e2) = e1
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d118]) ).
cnf(d120,plain,
( op(e0,e2) = e1
| op(e0,e3) = e2
| e0 != e0 ),
inference(superposition,[status(thm)],[d119,d24]) ).
cnf(d121,plain,
( op(e0,e2) = e1
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d120]) ).
cnf(d122,plain,
( op(e0,e3) = e2
| op(e0,e1) = e2 ),
inference(superposition,[status(thm)],[d121,c212]) ).
cnf(d123,plain,
( op(e0,e3) = e2
| e4 != op(op(e0,e1),e0)
| e2 != op(e0,e1)
| e3 != op(e0,op(e2,e0)) ),
inference(superposition,[status(thm)],[d122,c341]) ).
cnf(d124,plain,
( op(e0,e3) = e2
| e2 != op(e0,e1)
| e3 != op(e0,op(e2,e0))
| op(e0,e3) = e2
| e4 != op(e2,e0) ),
inference(superposition,[status(thm)],[d122,d123]) ).
cnf(d125,plain,
( op(e0,e3) = e2
| op(op(e3,e0),e4) = e0 ),
inference(superposition,[status(thm)],[d112,c78]) ).
cnf(d126,plain,
( op(e0,e3) = e2
| e1 != op(op(e0,e4),e0)
| e3 != op(e0,e4)
| e2 != op(e0,op(e3,e0)) ),
inference(superposition,[status(thm)],[d117,c279]) ).
cnf(d127,plain,
( op(e0,e3) = e2
| e2 != op(e0,op(e3,e0))
| e3 != op(e0,e4)
| op(e0,e3) = e2
| e1 != op(e3,e0) ),
inference(superposition,[status(thm)],[d117,d126]) ).
cnf(d128,plain,
( op(e0,e3) = e2
| op(e1,op(e2,e0)) = e2 ),
inference(superposition,[status(thm)],[d121,c85]) ).
cnf(d129,plain,
( op(e0,e3) = e2
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e1,e3) = e0 ),
inference(superposition,[status(thm)],[d117,d80]) ).
cnf(d130,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e3) = e2
| op(e1,e0) = e3 ),
inference(superposition,[status(thm)],[d129,c218]) ).
cnf(d131,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e3) = e2
| op(e3,op(e0,e1)) = e0 ),
inference(superposition,[status(thm)],[d130,c76]) ).
cnf(d132,plain,
( op(e0,e3) = e2
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e0,e3) = e2
| op(e3,e2) = e0 ),
inference(superposition,[status(thm)],[d122,d131]) ).
cnf(d133,plain,
( op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e2
| op(e0,e3) = e2
| op(e1,e1) = e2 ),
inference(superposition,[status(thm)],[d132,d128]) ).
cnf(d134,plain,
( op(e0,e3) = e2
| op(op(e2,e0),e1) = e0 ),
inference(superposition,[status(thm)],[d121,c77]) ).
cnf(d135,plain,
( op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e2
| op(e0,e3) = e2
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[d132,d134]) ).
cnf(d136,plain,
( op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e2
| op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e2
| e0 = e2 ),
inference(superposition,[status(thm)],[d135,d133]) ).
cnf(d137,plain,
( op(e3,e2) = e0
| op(e3,e0) = e1
| op(e0,e3) = e2 ),
inference(resolution,[status(thm)],[c201,d136]) ).
cnf(d138,plain,
( op(e3,e0) = e1
| op(e0,e3) = e2
| op(e3,e0) = e2 ),
inference(superposition,[status(thm)],[d137,c227]) ).
cnf(d139,plain,
( op(e3,e0) = e2
| op(e0,e3) = e2
| e1 != op(e3,e0)
| e3 != op(e0,e4)
| op(e0,e3) = e2
| e2 != op(e0,e1) ),
inference(superposition,[status(thm)],[d138,d127]) ).
cnf(d140,plain,
( op(e3,e0) = e2
| op(e0,e3) = e2
| e2 != op(e0,e1)
| e3 != op(e0,e4)
| op(e3,e0) = e2
| op(e0,e3) = e2
| e1 != e1 ),
inference(superposition,[status(thm)],[d138,d139]) ).
cnf(d141,plain,
( op(e0,e3) = e2
| e1 != e1
| e3 != op(e0,e4)
| op(e3,e0) = e2
| op(e0,e3) = e2
| e2 != e2 ),
inference(superposition,[status(thm)],[d122,d140]) ).
cnf(d142,plain,
( op(e0,e3) = e2
| e1 != e1
| e2 != e2
| op(e3,e0) = e2
| op(e0,e3) = e2
| e3 != e3 ),
inference(superposition,[status(thm)],[d117,d141]) ).
cnf(d143,plain,
( e2 != e2
| e3 != e3
| op(e3,e0) = e2
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d142]) ).
cnf(d144,plain,
( e3 != e3
| op(e3,e0) = e2
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d143]) ).
cnf(d145,plain,
( op(e3,e0) = e2
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d144]) ).
cnf(d146,plain,
( op(e0,e3) = e2
| op(e0,e3) = e2
| op(e2,e4) = e0 ),
inference(superposition,[status(thm)],[d145,d125]) ).
cnf(d147,plain,
( op(e0,e3) = e2
| op(e2,e0) = e4 ),
inference(superposition,[status(thm)],[d146,c224]) ).
cnf(d148,plain,
( op(e0,e3) = e2
| e4 != op(e2,e0)
| e2 != op(e0,e1)
| op(e0,e3) = e2
| e3 != op(e0,e4) ),
inference(superposition,[status(thm)],[d147,d124]) ).
cnf(d149,plain,
( op(e0,e3) = e2
| e2 != op(e0,e1)
| e3 != op(e0,e4)
| op(e0,e3) = e2
| e4 != e4 ),
inference(superposition,[status(thm)],[d147,d148]) ).
cnf(d150,plain,
( op(e0,e3) = e2
| e4 != e4
| e3 != op(e0,e4)
| op(e0,e3) = e2
| e2 != e2 ),
inference(superposition,[status(thm)],[d122,d149]) ).
cnf(d151,plain,
( op(e0,e3) = e2
| e4 != e4
| e2 != e2
| op(e0,e3) = e2
| e3 != e3 ),
inference(superposition,[status(thm)],[d117,d150]) ).
cnf(d152,plain,
( e2 != e2
| e3 != e3
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d151]) ).
cnf(d153,plain,
( e3 != e3
| op(e0,e3) = e2 ),
inference(equality_resolution,[status(thm)],[d152]) ).
cnf(d154,plain,
op(e0,e3) = e2,
inference(equality_resolution,[status(thm)],[d153]) ).
cnf(d155,plain,
op(e0,e1) != e2,
inference(demodulation,[status(thm)],[c155,d154]) ).
cnf(d156,plain,
( op(e0,e1) = e4
| op(e0,e1) = e3
| op(e0,e1) = e0 ),
inference(resolution,[status(thm)],[d155,d27]) ).
cnf(d157,plain,
op(e0,e2) = e3,
inference(demodulation,[status(thm)],[c213,d154]) ).
cnf(d158,plain,
op(e0,e1) != e3,
inference(demodulation,[status(thm)],[c154,d157]) ).
cnf(d159,plain,
( op(e0,e1) = e4
| op(e0,e1) = e0 ),
inference(resolution,[status(thm)],[d158,d156]) ).
cnf(d160,plain,
( op(e0,e1) = e0
| op(e0,e4) = e1 ),
inference(superposition,[status(thm)],[d159,c211]) ).
cnf(d161,plain,
( op(e0,e4) = e1
| e0 != e0 ),
inference(superposition,[status(thm)],[d160,d24]) ).
cnf(d162,plain,
op(e0,e4) = e1,
inference(equality_resolution,[status(thm)],[d161]) ).
cnf(d163,plain,
op(e0,e1) = e4,
inference(demodulation,[status(thm)],[c214,d162]) ).
cnf(d164,plain,
( e1 != op(e0,e4)
| e2 != op(e0,op(op(e0,e4),e0))
| e3 != op(e1,e0) ),
inference(demodulation,[status(thm)],[c329,d162]) ).
cnf(d165,plain,
( e1 != op(e0,e4)
| e2 != op(e0,op(e1,e0))
| e3 != op(e1,e0) ),
inference(demodulation,[status(thm)],[d164,d162]) ).
cnf(d166,plain,
( e1 != e1
| e2 != op(e0,op(e1,e0))
| e3 != op(e1,e0) ),
inference(demodulation,[status(thm)],[d165,d162]) ).
cnf(d167,plain,
( op(e0,e4) = e1
| op(e0,e0) = e1 ),
inference(superposition,[status(thm)],[d160,c211]) ).
cnf(d168,plain,
( op(e0,e4) = e1
| e0 = e1 ),
inference(demodulation,[status(thm)],[d167,d23]) ).
cnf(d169,plain,
( e1 = e1
| e0 = e1 ),
inference(demodulation,[status(thm)],[d168,d162]) ).
cnf(d170,plain,
e1 = e1,
inference(resolution,[status(thm)],[c200,d169]) ).
cnf(d171,plain,
( e2 != op(e0,op(e1,e0))
| e3 != op(e1,e0) ),
inference(resolution,[status(thm)],[d170,d166]) ).
cnf(d172,plain,
op(op(e2,e0),e3) = e0,
inference(demodulation,[status(thm)],[c77,d157]) ).
cnf(d173,plain,
e4 != op(e1,e1),
inference(demodulation,[status(thm)],[c110,d163]) ).
cnf(d174,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(op(e0,e4),e1) = e4 ),
inference(superposition,[status(thm)],[d79,c95]) ).
cnf(d175,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| op(e1,e1) = e4 ),
inference(demodulation,[status(thm)],[d174,d162]) ).
cnf(d176,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1
| e4 != e4 ),
inference(superposition,[status(thm)],[d175,d173]) ).
cnf(d177,plain,
( op(e0,e4) = e1
| op(e0,e2) = e1
| e2 = e1 ),
inference(demodulation,[status(thm)],[d49,d154]) ).
cnf(d178,plain,
( e2 = e1
| op(e0,e4) = e1
| e3 = e1 ),
inference(demodulation,[status(thm)],[d177,d157]) ).
cnf(d179,plain,
( e2 = e1
| e3 = e1
| op(e0,e1) = e4 ),
inference(superposition,[status(thm)],[d178,c214]) ).
cnf(d180,plain,
e3 != op(e0,e4),
inference(demodulation,[status(thm)],[c158,d157]) ).
cnf(d181,plain,
e3 != e1,
inference(demodulation,[status(thm)],[d180,d162]) ).
cnf(d182,plain,
( e2 = e1
| op(e0,e1) = e4 ),
inference(resolution,[status(thm)],[d181,d179]) ).
cnf(d183,plain,
( e2 = e1
| e4 = e4 ),
inference(demodulation,[status(thm)],[d182,d163]) ).
cnf(d184,plain,
e2 != op(e0,e4),
inference(demodulation,[status(thm)],[c159,d154]) ).
cnf(d185,plain,
e2 != e1,
inference(demodulation,[status(thm)],[d184,d162]) ).
cnf(d186,plain,
e4 = e4,
inference(resolution,[status(thm)],[d185,d183]) ).
cnf(d187,plain,
( op(e2,e0) = e1
| op(e3,e0) = e1 ),
inference(resolution,[status(thm)],[d186,d176]) ).
cnf(d188,plain,
( op(e3,e0) = e1
| op(e1,e3) = e0 ),
inference(superposition,[status(thm)],[d187,d172]) ).
cnf(d189,plain,
( op(e3,e0) = e1
| op(e1,e0) = e3 ),
inference(superposition,[status(thm)],[d188,c218]) ).
cnf(d190,plain,
( op(e3,e0) = e1
| e3 != op(e1,e0)
| e2 != op(e0,e3) ),
inference(superposition,[status(thm)],[d189,d171]) ).
cnf(d191,plain,
( e2 != e2
| e3 != op(e1,e0)
| op(e3,e0) = e1 ),
inference(demodulation,[status(thm)],[d190,d154]) ).
cnf(d192,plain,
( op(e3,e0) = e1
| e2 != e2
| op(e3,e0) = e1
| e3 != e3 ),
inference(superposition,[status(thm)],[d189,d191]) ).
cnf(d193,plain,
( op(e0,e4) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e0) = e3
| op(e0,e4) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e0) = e4
| e3 = e4 ),
inference(superposition,[status(thm)],[c31,c33]) ).
cnf(d194,plain,
( op(e0,e4) = e4
| op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e0) = e4
| op(e0,e0) = e3 ),
inference(resolution,[status(thm)],[c209,d193]) ).
cnf(d195,plain,
( op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e0) = e4
| op(e0,e0) = e3
| op(e4,op(e4,e0)) = e4 ),
inference(superposition,[status(thm)],[d194,c95]) ).
cnf(d196,plain,
( op(e4,op(e4,e0)) = e4
| op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e0) = e4
| e0 = e3 ),
inference(demodulation,[status(thm)],[d195,d23]) ).
cnf(d197,plain,
( op(e4,op(e4,e0)) = e4
| op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| e0 = e4
| e0 = e3 ),
inference(demodulation,[status(thm)],[d196,d23]) ).
cnf(d198,plain,
( e0 = e4
| op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| e0 = e4
| e0 = e3 ),
inference(demodulation,[status(thm)],[d197,c230]) ).
cnf(d199,plain,
( e0 = e4
| op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| e0 = e4 ),
inference(resolution,[status(thm)],[c202,d198]) ).
cnf(d200,plain,
( op(e0,e4) = e3
| op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3 ),
inference(resolution,[status(thm)],[c203,d199]) ).
cnf(d201,plain,
( op(e0,e2) = e4
| op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) = e4 ),
inference(superposition,[status(thm)],[d200,c214]) ).
cnf(d202,plain,
( op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e4) = e2 ),
inference(superposition,[status(thm)],[d201,c212]) ).
cnf(d203,plain,
( op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3
| op(e0,e3) != e2 ),
inference(superposition,[status(thm)],[d202,c159]) ).
cnf(d204,plain,
( op(e0,e2) = e3
| op(e0,e3) = e4
| op(e0,e3) = e3 ),
inference(resolution,[status(thm)],[d154,d203]) ).
cnf(d205,plain,
( op(e0,e2) = e3
| op(e0,e3) = e4
| e2 = e3 ),
inference(demodulation,[status(thm)],[d204,d154]) ).
cnf(d206,plain,
( op(e0,e2) = e3
| e2 = e4
| e2 = e3 ),
inference(demodulation,[status(thm)],[d205,d154]) ).
cnf(d207,plain,
( e3 = e3
| e2 = e4
| e2 = e3 ),
inference(demodulation,[status(thm)],[d206,d157]) ).
cnf(d208,plain,
( e3 = e3
| e2 = e4 ),
inference(resolution,[status(thm)],[c207,d207]) ).
cnf(d209,plain,
e3 = e3,
inference(resolution,[status(thm)],[c208,d208]) ).
cnf(d210,plain,
( e2 != e2
| op(e3,e0) = e1 ),
inference(resolution,[status(thm)],[d209,d192]) ).
cnf(d211,plain,
op(e3,e0) = e1,
inference(equality_resolution,[status(thm)],[d210]) ).
cnf(d212,plain,
( e1 != op(op(e0,e2),e0)
| e4 != op(e0,op(op(e0,e2),e0))
| e3 != e3 ),
inference(demodulation,[status(thm)],[c269,d157]) ).
cnf(d213,plain,
( e1 != op(op(e0,e2),e0)
| e4 != op(e0,op(e3,e0))
| e3 != e3 ),
inference(demodulation,[status(thm)],[d212,d157]) ).
cnf(d214,plain,
( e1 != op(e3,e0)
| e4 != op(e0,op(e3,e0))
| e3 != e3 ),
inference(demodulation,[status(thm)],[d213,d157]) ).
cnf(d215,plain,
( e1 != op(e3,e0)
| e4 != op(e0,op(e3,e0)) ),
inference(resolution,[status(thm)],[d209,d214]) ).
cnf(d216,plain,
( e1 != op(e3,e0)
| e4 != op(e0,e1) ),
inference(demodulation,[status(thm)],[d215,d211]) ).
cnf(d217,plain,
( e1 != e1
| e4 != op(e0,e1) ),
inference(demodulation,[status(thm)],[d216,d211]) ).
cnf(d218,plain,
( e1 != e1
| e4 != e4 ),
inference(demodulation,[status(thm)],[d217,d163]) ).
cnf(d219,plain,
e1 != e1,
inference(resolution,[status(thm)],[d186,d218]) ).
cnf(d220,plain,
$false,
inference(resolution,[status(thm)],[d170,d219]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG192+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n002.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 21:27:05 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.71/13.57 % SZS status Unsatisfiable for theBenchmark.p
% 29.71/13.57 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------