%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG021+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:20:06 AM UTC 2026
% Result : Theorem 0.22s 0.27s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 138
% Syntax : Number of formulae : 882 ( 170 unt; 134 def)
% Number of atoms : 3671 (1492 equ)
% Maximal formula atoms : 180 ( 4 avg)
% Number of connectives : 5040 (2251 ~;2237 |; 439 &)
% ( 113 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 109 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 136 ( 134 usr; 135 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( op(e0,e0) = e0
& op(e0,e1) = e1
& op(e0,e2) = e2
& op(e0,e3) = e3
& op(e1,e0) = e1
& op(e1,e1) = e0
& op(e1,e2) = e3
& op(e1,e3) = e2
& op(e2,e0) = e2
& op(e2,e1) = e3
& op(e2,e2) = e0
& op(e2,e3) = e1
& op(e3,e0) = e3
& op(e3,e1) = e2
& op(e3,e2) = e1
& op(e3,e3) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
unit = e0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( inv(e0) = e0
& inv(e1) = e1
& inv(e2) = e2
& inv(e3) = e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,conjecture,
( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 )
& op(op(e0,e0),e0) = op(e0,op(e0,e0))
& op(op(e0,e0),e1) = op(e0,op(e0,e1))
& op(op(e0,e0),e2) = op(e0,op(e0,e2))
& op(op(e0,e0),e3) = op(e0,op(e0,e3))
& op(op(e0,e1),e0) = op(e0,op(e1,e0))
& op(op(e0,e1),e1) = op(e0,op(e1,e1))
& op(op(e0,e1),e2) = op(e0,op(e1,e2))
& op(op(e0,e1),e3) = op(e0,op(e1,e3))
& op(op(e0,e2),e0) = op(e0,op(e2,e0))
& op(op(e0,e2),e1) = op(e0,op(e2,e1))
& op(op(e0,e2),e2) = op(e0,op(e2,e2))
& op(op(e0,e2),e3) = op(e0,op(e2,e3))
& op(op(e0,e3),e0) = op(e0,op(e3,e0))
& op(op(e0,e3),e1) = op(e0,op(e3,e1))
& op(op(e0,e3),e2) = op(e0,op(e3,e2))
& op(op(e0,e3),e3) = op(e0,op(e3,e3))
& op(op(e1,e0),e0) = op(e1,op(e0,e0))
& op(op(e1,e0),e1) = op(e1,op(e0,e1))
& op(op(e1,e0),e2) = op(e1,op(e0,e2))
& op(op(e1,e0),e3) = op(e1,op(e0,e3))
& op(op(e1,e1),e0) = op(e1,op(e1,e0))
& op(op(e1,e1),e1) = op(e1,op(e1,e1))
& op(op(e1,e1),e2) = op(e1,op(e1,e2))
& op(op(e1,e1),e3) = op(e1,op(e1,e3))
& op(op(e1,e2),e0) = op(e1,op(e2,e0))
& op(op(e1,e2),e1) = op(e1,op(e2,e1))
& op(op(e1,e2),e2) = op(e1,op(e2,e2))
& op(op(e1,e2),e3) = op(e1,op(e2,e3))
& op(op(e1,e3),e0) = op(e1,op(e3,e0))
& op(op(e1,e3),e1) = op(e1,op(e3,e1))
& op(op(e1,e3),e2) = op(e1,op(e3,e2))
& op(op(e1,e3),e3) = op(e1,op(e3,e3))
& op(op(e2,e0),e0) = op(e2,op(e0,e0))
& op(op(e2,e0),e1) = op(e2,op(e0,e1))
& op(op(e2,e0),e2) = op(e2,op(e0,e2))
& op(op(e2,e0),e3) = op(e2,op(e0,e3))
& op(op(e2,e1),e0) = op(e2,op(e1,e0))
& op(op(e2,e1),e1) = op(e2,op(e1,e1))
& op(op(e2,e1),e2) = op(e2,op(e1,e2))
& op(op(e2,e1),e3) = op(e2,op(e1,e3))
& op(op(e2,e2),e0) = op(e2,op(e2,e0))
& op(op(e2,e2),e1) = op(e2,op(e2,e1))
& op(op(e2,e2),e2) = op(e2,op(e2,e2))
& op(op(e2,e2),e3) = op(e2,op(e2,e3))
& op(op(e2,e3),e0) = op(e2,op(e3,e0))
& op(op(e2,e3),e1) = op(e2,op(e3,e1))
& op(op(e2,e3),e2) = op(e2,op(e3,e2))
& op(op(e2,e3),e3) = op(e2,op(e3,e3))
& op(op(e3,e0),e0) = op(e3,op(e0,e0))
& op(op(e3,e0),e1) = op(e3,op(e0,e1))
& op(op(e3,e0),e2) = op(e3,op(e0,e2))
& op(op(e3,e0),e3) = op(e3,op(e0,e3))
& op(op(e3,e1),e0) = op(e3,op(e1,e0))
& op(op(e3,e1),e1) = op(e3,op(e1,e1))
& op(op(e3,e1),e2) = op(e3,op(e1,e2))
& op(op(e3,e1),e3) = op(e3,op(e1,e3))
& op(op(e3,e2),e0) = op(e3,op(e2,e0))
& op(op(e3,e2),e1) = op(e3,op(e2,e1))
& op(op(e3,e2),e2) = op(e3,op(e2,e2))
& op(op(e3,e2),e3) = op(e3,op(e2,e3))
& op(op(e3,e3),e0) = op(e3,op(e3,e0))
& op(op(e3,e3),e1) = op(e3,op(e3,e1))
& op(op(e3,e3),e2) = op(e3,op(e3,e2))
& op(op(e3,e3),e3) = op(e3,op(e3,e3))
& op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 )
& op(e0,inv(e0)) = unit
& op(inv(e0),e0) = unit
& op(e1,inv(e1)) = unit
& op(inv(e1),e1) = unit
& op(e2,inv(e2)) = unit
& op(inv(e2),e2) = unit
& op(e3,inv(e3)) = unit
& op(inv(e3),e3) = unit
& ( inv(e0) = e0
| inv(e0) = e1
| inv(e0) = e2
| inv(e0) = e3 )
& ( inv(e1) = e0
| inv(e1) = e1
| inv(e1) = e2
| inv(e1) = e3 )
& ( inv(e2) = e0
| inv(e2) = e1
| inv(e2) = e2
| inv(e2) = e3 )
& ( inv(e3) = e0
| inv(e3) = e1
| inv(e3) = e2
| inv(e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f6,negated_conjecture,
~ ( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 )
& op(op(e0,e0),e0) = op(e0,op(e0,e0))
& op(op(e0,e0),e1) = op(e0,op(e0,e1))
& op(op(e0,e0),e2) = op(e0,op(e0,e2))
& op(op(e0,e0),e3) = op(e0,op(e0,e3))
& op(op(e0,e1),e0) = op(e0,op(e1,e0))
& op(op(e0,e1),e1) = op(e0,op(e1,e1))
& op(op(e0,e1),e2) = op(e0,op(e1,e2))
& op(op(e0,e1),e3) = op(e0,op(e1,e3))
& op(op(e0,e2),e0) = op(e0,op(e2,e0))
& op(op(e0,e2),e1) = op(e0,op(e2,e1))
& op(op(e0,e2),e2) = op(e0,op(e2,e2))
& op(op(e0,e2),e3) = op(e0,op(e2,e3))
& op(op(e0,e3),e0) = op(e0,op(e3,e0))
& op(op(e0,e3),e1) = op(e0,op(e3,e1))
& op(op(e0,e3),e2) = op(e0,op(e3,e2))
& op(op(e0,e3),e3) = op(e0,op(e3,e3))
& op(op(e1,e0),e0) = op(e1,op(e0,e0))
& op(op(e1,e0),e1) = op(e1,op(e0,e1))
& op(op(e1,e0),e2) = op(e1,op(e0,e2))
& op(op(e1,e0),e3) = op(e1,op(e0,e3))
& op(op(e1,e1),e0) = op(e1,op(e1,e0))
& op(op(e1,e1),e1) = op(e1,op(e1,e1))
& op(op(e1,e1),e2) = op(e1,op(e1,e2))
& op(op(e1,e1),e3) = op(e1,op(e1,e3))
& op(op(e1,e2),e0) = op(e1,op(e2,e0))
& op(op(e1,e2),e1) = op(e1,op(e2,e1))
& op(op(e1,e2),e2) = op(e1,op(e2,e2))
& op(op(e1,e2),e3) = op(e1,op(e2,e3))
& op(op(e1,e3),e0) = op(e1,op(e3,e0))
& op(op(e1,e3),e1) = op(e1,op(e3,e1))
& op(op(e1,e3),e2) = op(e1,op(e3,e2))
& op(op(e1,e3),e3) = op(e1,op(e3,e3))
& op(op(e2,e0),e0) = op(e2,op(e0,e0))
& op(op(e2,e0),e1) = op(e2,op(e0,e1))
& op(op(e2,e0),e2) = op(e2,op(e0,e2))
& op(op(e2,e0),e3) = op(e2,op(e0,e3))
& op(op(e2,e1),e0) = op(e2,op(e1,e0))
& op(op(e2,e1),e1) = op(e2,op(e1,e1))
& op(op(e2,e1),e2) = op(e2,op(e1,e2))
& op(op(e2,e1),e3) = op(e2,op(e1,e3))
& op(op(e2,e2),e0) = op(e2,op(e2,e0))
& op(op(e2,e2),e1) = op(e2,op(e2,e1))
& op(op(e2,e2),e2) = op(e2,op(e2,e2))
& op(op(e2,e2),e3) = op(e2,op(e2,e3))
& op(op(e2,e3),e0) = op(e2,op(e3,e0))
& op(op(e2,e3),e1) = op(e2,op(e3,e1))
& op(op(e2,e3),e2) = op(e2,op(e3,e2))
& op(op(e2,e3),e3) = op(e2,op(e3,e3))
& op(op(e3,e0),e0) = op(e3,op(e0,e0))
& op(op(e3,e0),e1) = op(e3,op(e0,e1))
& op(op(e3,e0),e2) = op(e3,op(e0,e2))
& op(op(e3,e0),e3) = op(e3,op(e0,e3))
& op(op(e3,e1),e0) = op(e3,op(e1,e0))
& op(op(e3,e1),e1) = op(e3,op(e1,e1))
& op(op(e3,e1),e2) = op(e3,op(e1,e2))
& op(op(e3,e1),e3) = op(e3,op(e1,e3))
& op(op(e3,e2),e0) = op(e3,op(e2,e0))
& op(op(e3,e2),e1) = op(e3,op(e2,e1))
& op(op(e3,e2),e2) = op(e3,op(e2,e2))
& op(op(e3,e2),e3) = op(e3,op(e2,e3))
& op(op(e3,e3),e0) = op(e3,op(e3,e0))
& op(op(e3,e3),e1) = op(e3,op(e3,e1))
& op(op(e3,e3),e2) = op(e3,op(e3,e2))
& op(op(e3,e3),e3) = op(e3,op(e3,e3))
& op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 )
& op(e0,inv(e0)) = unit
& op(inv(e0),e0) = unit
& op(e1,inv(e1)) = unit
& op(inv(e1),e1) = unit
& op(e2,inv(e2)) = unit
& op(inv(e2),e2) = unit
& op(e3,inv(e3)) = unit
& op(inv(e3),e3) = unit
& ( inv(e0) = e0
| inv(e0) = e1
| inv(e0) = e2
| inv(e0) = e3 )
& ( inv(e1) = e0
| inv(e1) = e1
| inv(e1) = e2
| inv(e1) = e3 )
& ( inv(e2) = e0
| inv(e2) = e1
| inv(e2) = e2
| inv(e2) = e3 )
& ( inv(e3) = e0
| inv(e3) = e1
| inv(e3) = e2
| inv(e3) = e3 ) ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f7,plain,
( ( ( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) )
& ( e1 != op(e0,e0)
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) )
& ( e2 != op(e0,e0)
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) )
& ( e3 != op(e0,e0)
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ) )
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3) )
| op(op(e0,e0),e0) != op(e0,op(e0,e0))
| op(op(e0,e0),e1) != op(e0,op(e0,e1))
| op(op(e0,e0),e2) != op(e0,op(e0,e2))
| op(op(e0,e0),e3) != op(e0,op(e0,e3))
| op(op(e0,e1),e0) != op(e0,op(e1,e0))
| op(op(e0,e1),e1) != op(e0,op(e1,e1))
| op(op(e0,e1),e2) != op(e0,op(e1,e2))
| op(op(e0,e1),e3) != op(e0,op(e1,e3))
| op(op(e0,e2),e0) != op(e0,op(e2,e0))
| op(op(e0,e2),e1) != op(e0,op(e2,e1))
| op(op(e0,e2),e2) != op(e0,op(e2,e2))
| op(op(e0,e2),e3) != op(e0,op(e2,e3))
| op(op(e0,e3),e0) != op(e0,op(e3,e0))
| op(op(e0,e3),e1) != op(e0,op(e3,e1))
| op(op(e0,e3),e2) != op(e0,op(e3,e2))
| op(op(e0,e3),e3) != op(e0,op(e3,e3))
| op(op(e1,e0),e0) != op(e1,op(e0,e0))
| op(op(e1,e0),e1) != op(e1,op(e0,e1))
| op(op(e1,e0),e2) != op(e1,op(e0,e2))
| op(op(e1,e0),e3) != op(e1,op(e0,e3))
| op(op(e1,e1),e0) != op(e1,op(e1,e0))
| op(op(e1,e1),e1) != op(e1,op(e1,e1))
| op(op(e1,e1),e2) != op(e1,op(e1,e2))
| op(op(e1,e1),e3) != op(e1,op(e1,e3))
| op(op(e1,e2),e0) != op(e1,op(e2,e0))
| op(op(e1,e2),e1) != op(e1,op(e2,e1))
| op(op(e1,e2),e2) != op(e1,op(e2,e2))
| op(op(e1,e2),e3) != op(e1,op(e2,e3))
| op(op(e1,e3),e0) != op(e1,op(e3,e0))
| op(op(e1,e3),e1) != op(e1,op(e3,e1))
| op(op(e1,e3),e2) != op(e1,op(e3,e2))
| op(op(e1,e3),e3) != op(e1,op(e3,e3))
| op(op(e2,e0),e0) != op(e2,op(e0,e0))
| op(op(e2,e0),e1) != op(e2,op(e0,e1))
| op(op(e2,e0),e2) != op(e2,op(e0,e2))
| op(op(e2,e0),e3) != op(e2,op(e0,e3))
| op(op(e2,e1),e0) != op(e2,op(e1,e0))
| op(op(e2,e1),e1) != op(e2,op(e1,e1))
| op(op(e2,e1),e2) != op(e2,op(e1,e2))
| op(op(e2,e1),e3) != op(e2,op(e1,e3))
| op(op(e2,e2),e0) != op(e2,op(e2,e0))
| op(op(e2,e2),e1) != op(e2,op(e2,e1))
| op(op(e2,e2),e2) != op(e2,op(e2,e2))
| op(op(e2,e2),e3) != op(e2,op(e2,e3))
| op(op(e2,e3),e0) != op(e2,op(e3,e0))
| op(op(e2,e3),e1) != op(e2,op(e3,e1))
| op(op(e2,e3),e2) != op(e2,op(e3,e2))
| op(op(e2,e3),e3) != op(e2,op(e3,e3))
| op(op(e3,e0),e0) != op(e3,op(e0,e0))
| op(op(e3,e0),e1) != op(e3,op(e0,e1))
| op(op(e3,e0),e2) != op(e3,op(e0,e2))
| op(op(e3,e0),e3) != op(e3,op(e0,e3))
| op(op(e3,e1),e0) != op(e3,op(e1,e0))
| op(op(e3,e1),e1) != op(e3,op(e1,e1))
| op(op(e3,e1),e2) != op(e3,op(e1,e2))
| op(op(e3,e1),e3) != op(e3,op(e1,e3))
| op(op(e3,e2),e0) != op(e3,op(e2,e0))
| op(op(e3,e2),e1) != op(e3,op(e2,e1))
| op(op(e3,e2),e2) != op(e3,op(e2,e2))
| op(op(e3,e2),e3) != op(e3,op(e2,e3))
| op(op(e3,e3),e0) != op(e3,op(e3,e0))
| op(op(e3,e3),e1) != op(e3,op(e3,e1))
| op(op(e3,e3),e2) != op(e3,op(e3,e2))
| op(op(e3,e3),e3) != op(e3,op(e3,e3))
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit )
| unit != op(e0,inv(e0))
| unit != op(inv(e0),e0)
| unit != op(e1,inv(e1))
| unit != op(inv(e1),e1)
| unit != op(e2,inv(e2))
| unit != op(inv(e2),e2)
| unit != op(e3,inv(e3))
| unit != op(inv(e3),e3)
| ( e0 != inv(e0)
& e1 != inv(e0)
& e2 != inv(e0)
& e3 != inv(e0) )
| ( e0 != inv(e1)
& e1 != inv(e1)
& e2 != inv(e1)
& e3 != inv(e1) )
| ( e0 != inv(e2)
& e1 != inv(e2)
& e2 != inv(e2)
& e3 != inv(e2) )
| ( e0 != inv(e3)
& e1 != inv(e3)
& e2 != inv(e3)
& e3 != inv(e3) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f8,definition,
( ( e0 != inv(e3)
& e1 != inv(e3)
& e2 != inv(e3)
& e3 != inv(e3) )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f9,definition,
( ( e0 != inv(e2)
& e1 != inv(e2)
& e2 != inv(e2)
& e3 != inv(e2) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f10,definition,
( ( e0 != inv(e1)
& e1 != inv(e1)
& e2 != inv(e1)
& e3 != inv(e1) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( e0 != inv(e0)
& e1 != inv(e0)
& e2 != inv(e0)
& e3 != inv(e0) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3) )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2) )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1) )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0) )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3) )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2) )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1) )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0) )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3) )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2) )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1) )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0) )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3) )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2) )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1) )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0) )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f29,plain,
( ( ( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) )
& ( e1 != op(e0,e0)
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) )
& ( e2 != op(e0,e0)
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) )
& ( e3 != op(e0,e0)
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ) )
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| op(op(e0,e0),e0) != op(e0,op(e0,e0))
| op(op(e0,e0),e1) != op(e0,op(e0,e1))
| op(op(e0,e0),e2) != op(e0,op(e0,e2))
| op(op(e0,e0),e3) != op(e0,op(e0,e3))
| op(op(e0,e1),e0) != op(e0,op(e1,e0))
| op(op(e0,e1),e1) != op(e0,op(e1,e1))
| op(op(e0,e1),e2) != op(e0,op(e1,e2))
| op(op(e0,e1),e3) != op(e0,op(e1,e3))
| op(op(e0,e2),e0) != op(e0,op(e2,e0))
| op(op(e0,e2),e1) != op(e0,op(e2,e1))
| op(op(e0,e2),e2) != op(e0,op(e2,e2))
| op(op(e0,e2),e3) != op(e0,op(e2,e3))
| op(op(e0,e3),e0) != op(e0,op(e3,e0))
| op(op(e0,e3),e1) != op(e0,op(e3,e1))
| op(op(e0,e3),e2) != op(e0,op(e3,e2))
| op(op(e0,e3),e3) != op(e0,op(e3,e3))
| op(op(e1,e0),e0) != op(e1,op(e0,e0))
| op(op(e1,e0),e1) != op(e1,op(e0,e1))
| op(op(e1,e0),e2) != op(e1,op(e0,e2))
| op(op(e1,e0),e3) != op(e1,op(e0,e3))
| op(op(e1,e1),e0) != op(e1,op(e1,e0))
| op(op(e1,e1),e1) != op(e1,op(e1,e1))
| op(op(e1,e1),e2) != op(e1,op(e1,e2))
| op(op(e1,e1),e3) != op(e1,op(e1,e3))
| op(op(e1,e2),e0) != op(e1,op(e2,e0))
| op(op(e1,e2),e1) != op(e1,op(e2,e1))
| op(op(e1,e2),e2) != op(e1,op(e2,e2))
| op(op(e1,e2),e3) != op(e1,op(e2,e3))
| op(op(e1,e3),e0) != op(e1,op(e3,e0))
| op(op(e1,e3),e1) != op(e1,op(e3,e1))
| op(op(e1,e3),e2) != op(e1,op(e3,e2))
| op(op(e1,e3),e3) != op(e1,op(e3,e3))
| op(op(e2,e0),e0) != op(e2,op(e0,e0))
| op(op(e2,e0),e1) != op(e2,op(e0,e1))
| op(op(e2,e0),e2) != op(e2,op(e0,e2))
| op(op(e2,e0),e3) != op(e2,op(e0,e3))
| op(op(e2,e1),e0) != op(e2,op(e1,e0))
| op(op(e2,e1),e1) != op(e2,op(e1,e1))
| op(op(e2,e1),e2) != op(e2,op(e1,e2))
| op(op(e2,e1),e3) != op(e2,op(e1,e3))
| op(op(e2,e2),e0) != op(e2,op(e2,e0))
| op(op(e2,e2),e1) != op(e2,op(e2,e1))
| op(op(e2,e2),e2) != op(e2,op(e2,e2))
| op(op(e2,e2),e3) != op(e2,op(e2,e3))
| op(op(e2,e3),e0) != op(e2,op(e3,e0))
| op(op(e2,e3),e1) != op(e2,op(e3,e1))
| op(op(e2,e3),e2) != op(e2,op(e3,e2))
| op(op(e2,e3),e3) != op(e2,op(e3,e3))
| op(op(e3,e0),e0) != op(e3,op(e0,e0))
| op(op(e3,e0),e1) != op(e3,op(e0,e1))
| op(op(e3,e0),e2) != op(e3,op(e0,e2))
| op(op(e3,e0),e3) != op(e3,op(e0,e3))
| op(op(e3,e1),e0) != op(e3,op(e1,e0))
| op(op(e3,e1),e1) != op(e3,op(e1,e1))
| op(op(e3,e1),e2) != op(e3,op(e1,e2))
| op(op(e3,e1),e3) != op(e3,op(e1,e3))
| op(op(e3,e2),e0) != op(e3,op(e2,e0))
| op(op(e3,e2),e1) != op(e3,op(e2,e1))
| op(op(e3,e2),e2) != op(e3,op(e2,e2))
| op(op(e3,e2),e3) != op(e3,op(e2,e3))
| op(op(e3,e3),e0) != op(e3,op(e3,e0))
| op(op(e3,e3),e1) != op(e3,op(e3,e1))
| op(op(e3,e3),e2) != op(e3,op(e3,e2))
| op(op(e3,e3),e3) != op(e3,op(e3,e3))
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| sP4
| unit != op(e0,inv(e0))
| unit != op(inv(e0),e0)
| unit != op(e1,inv(e1))
| unit != op(inv(e1),e1)
| unit != op(e2,inv(e2))
| unit != op(inv(e2),e2)
| unit != op(e3,inv(e3))
| unit != op(inv(e3),e3)
| sP3
| sP2
| sP1
| sP0 ),
inference(definition_folding,[],[f7,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8]) ).
fof(f30,plain,
( ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0) )
| ~ sP20 ),
inference(nnf_transformation,[],[f28]) ).
fof(f31,plain,
( ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1) )
| ~ sP19 ),
inference(nnf_transformation,[],[f27]) ).
fof(f32,plain,
( ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2) )
| ~ sP18 ),
inference(nnf_transformation,[],[f26]) ).
fof(f33,plain,
( ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3) )
| ~ sP17 ),
inference(nnf_transformation,[],[f25]) ).
fof(f34,plain,
( ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0) )
| ~ sP16 ),
inference(nnf_transformation,[],[f24]) ).
fof(f35,plain,
( ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1) )
| ~ sP15 ),
inference(nnf_transformation,[],[f23]) ).
fof(f36,plain,
( ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2) )
| ~ sP14 ),
inference(nnf_transformation,[],[f22]) ).
fof(f37,plain,
( ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3) )
| ~ sP13 ),
inference(nnf_transformation,[],[f21]) ).
fof(f38,plain,
( ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0) )
| ~ sP12 ),
inference(nnf_transformation,[],[f20]) ).
fof(f39,plain,
( ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1) )
| ~ sP11 ),
inference(nnf_transformation,[],[f19]) ).
fof(f40,plain,
( ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2) )
| ~ sP10 ),
inference(nnf_transformation,[],[f18]) ).
fof(f41,plain,
( ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3) )
| ~ sP9 ),
inference(nnf_transformation,[],[f17]) ).
fof(f42,plain,
( ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0) )
| ~ sP8 ),
inference(nnf_transformation,[],[f16]) ).
fof(f43,plain,
( ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1) )
| ~ sP7 ),
inference(nnf_transformation,[],[f15]) ).
fof(f44,plain,
( ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2) )
| ~ sP6 ),
inference(nnf_transformation,[],[f14]) ).
fof(f45,plain,
( ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3) )
| ~ sP5 ),
inference(nnf_transformation,[],[f13]) ).
fof(f46,plain,
( ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit )
| ~ sP4 ),
inference(nnf_transformation,[],[f12]) ).
fof(f47,plain,
( ( e0 != inv(e0)
& e1 != inv(e0)
& e2 != inv(e0)
& e3 != inv(e0) )
| ~ sP3 ),
inference(nnf_transformation,[],[f11]) ).
fof(f48,plain,
( ( e0 != inv(e1)
& e1 != inv(e1)
& e2 != inv(e1)
& e3 != inv(e1) )
| ~ sP2 ),
inference(nnf_transformation,[],[f10]) ).
fof(f49,plain,
( ( e0 != inv(e2)
& e1 != inv(e2)
& e2 != inv(e2)
& e3 != inv(e2) )
| ~ sP1 ),
inference(nnf_transformation,[],[f9]) ).
fof(f50,plain,
( ( e0 != inv(e3)
& e1 != inv(e3)
& e2 != inv(e3)
& e3 != inv(e3) )
| ~ sP0 ),
inference(nnf_transformation,[],[f8]) ).
fof(f57,plain,
e0 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f58,plain,
e1 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f59,plain,
e2 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f60,plain,
e3 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f61,plain,
e1 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f62,plain,
e0 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f63,plain,
e3 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f64,plain,
e2 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f65,plain,
e2 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f66,plain,
e3 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f67,plain,
e0 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f68,plain,
e1 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f69,plain,
e3 = op(e0,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f70,plain,
e2 = op(e0,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f71,plain,
e1 = op(e0,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
e0 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
e0 = unit,
inference(cnf_transformation,[],[f3]) ).
fof(f74,plain,
e3 = inv(e3),
inference(cnf_transformation,[],[f4]) ).
fof(f75,plain,
e2 = inv(e2),
inference(cnf_transformation,[],[f4]) ).
fof(f76,plain,
e1 = inv(e1),
inference(cnf_transformation,[],[f4]) ).
fof(f77,plain,
e0 = inv(e0),
inference(cnf_transformation,[],[f4]) ).
fof(f81,plain,
( e0 != op(e0,e0)
| ~ sP20 ),
inference(cnf_transformation,[],[f30]) ).
fof(f84,plain,
( e1 != op(e0,e1)
| ~ sP19 ),
inference(cnf_transformation,[],[f31]) ).
fof(f87,plain,
( e2 != op(e0,e2)
| ~ sP18 ),
inference(cnf_transformation,[],[f32]) ).
fof(f90,plain,
( e3 != op(e0,e3)
| ~ sP17 ),
inference(cnf_transformation,[],[f33]) ).
fof(f96,plain,
( e1 != op(e1,e0)
| ~ sP16 ),
inference(cnf_transformation,[],[f34]) ).
fof(f101,plain,
( e0 != op(e1,e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f35]) ).
fof(f102,plain,
( e3 != op(e1,e2)
| ~ sP14 ),
inference(cnf_transformation,[],[f36]) ).
fof(f107,plain,
( e2 != op(e1,e3)
| ~ sP13 ),
inference(cnf_transformation,[],[f37]) ).
fof(f111,plain,
( e2 != op(e2,e0)
| ~ sP12 ),
inference(cnf_transformation,[],[f38]) ).
fof(f114,plain,
( e3 != op(e2,e1)
| ~ sP11 ),
inference(cnf_transformation,[],[f39]) ).
fof(f121,plain,
( e0 != op(e2,e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f40]) ).
fof(f124,plain,
( e1 != op(e2,e3)
| ~ sP9 ),
inference(cnf_transformation,[],[f41]) ).
fof(f126,plain,
( e3 != op(e3,e0)
| ~ sP8 ),
inference(cnf_transformation,[],[f42]) ).
fof(f131,plain,
( e2 != op(e3,e1)
| ~ sP7 ),
inference(cnf_transformation,[],[f43]) ).
fof(f136,plain,
( e1 != op(e3,e2)
| ~ sP6 ),
inference(cnf_transformation,[],[f44]) ).
fof(f141,plain,
( e0 != op(e3,e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f45]) ).
fof(f145,plain,
( e0 != unit
| ~ sP4 ),
inference(cnf_transformation,[],[f46]) ).
fof(f149,plain,
( e0 != inv(e0)
| ~ sP3 ),
inference(cnf_transformation,[],[f47]) ).
fof(f152,plain,
( e1 != inv(e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f48]) ).
fof(f155,plain,
( e2 != inv(e2)
| ~ sP1 ),
inference(cnf_transformation,[],[f49]) ).
fof(f158,plain,
( e3 != inv(e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f50]) ).
fof(f165,plain,
( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3)
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| op(op(e0,e0),e0) != op(e0,op(e0,e0))
| op(op(e0,e0),e1) != op(e0,op(e0,e1))
| op(op(e0,e0),e2) != op(e0,op(e0,e2))
| op(op(e0,e0),e3) != op(e0,op(e0,e3))
| op(op(e0,e1),e0) != op(e0,op(e1,e0))
| op(op(e0,e1),e1) != op(e0,op(e1,e1))
| op(op(e0,e1),e2) != op(e0,op(e1,e2))
| op(op(e0,e1),e3) != op(e0,op(e1,e3))
| op(op(e0,e2),e0) != op(e0,op(e2,e0))
| op(op(e0,e2),e1) != op(e0,op(e2,e1))
| op(op(e0,e2),e2) != op(e0,op(e2,e2))
| op(op(e0,e2),e3) != op(e0,op(e2,e3))
| op(op(e0,e3),e0) != op(e0,op(e3,e0))
| op(op(e0,e3),e1) != op(e0,op(e3,e1))
| op(op(e0,e3),e2) != op(e0,op(e3,e2))
| op(op(e0,e3),e3) != op(e0,op(e3,e3))
| op(op(e1,e0),e0) != op(e1,op(e0,e0))
| op(op(e1,e0),e1) != op(e1,op(e0,e1))
| op(op(e1,e0),e2) != op(e1,op(e0,e2))
| op(op(e1,e0),e3) != op(e1,op(e0,e3))
| op(op(e1,e1),e0) != op(e1,op(e1,e0))
| op(op(e1,e1),e1) != op(e1,op(e1,e1))
| op(op(e1,e1),e2) != op(e1,op(e1,e2))
| op(op(e1,e1),e3) != op(e1,op(e1,e3))
| op(op(e1,e2),e0) != op(e1,op(e2,e0))
| op(op(e1,e2),e1) != op(e1,op(e2,e1))
| op(op(e1,e2),e2) != op(e1,op(e2,e2))
| op(op(e1,e2),e3) != op(e1,op(e2,e3))
| op(op(e1,e3),e0) != op(e1,op(e3,e0))
| op(op(e1,e3),e1) != op(e1,op(e3,e1))
| op(op(e1,e3),e2) != op(e1,op(e3,e2))
| op(op(e1,e3),e3) != op(e1,op(e3,e3))
| op(op(e2,e0),e0) != op(e2,op(e0,e0))
| op(op(e2,e0),e1) != op(e2,op(e0,e1))
| op(op(e2,e0),e2) != op(e2,op(e0,e2))
| op(op(e2,e0),e3) != op(e2,op(e0,e3))
| op(op(e2,e1),e0) != op(e2,op(e1,e0))
| op(op(e2,e1),e1) != op(e2,op(e1,e1))
| op(op(e2,e1),e2) != op(e2,op(e1,e2))
| op(op(e2,e1),e3) != op(e2,op(e1,e3))
| op(op(e2,e2),e0) != op(e2,op(e2,e0))
| op(op(e2,e2),e1) != op(e2,op(e2,e1))
| op(op(e2,e2),e2) != op(e2,op(e2,e2))
| op(op(e2,e2),e3) != op(e2,op(e2,e3))
| op(op(e2,e3),e0) != op(e2,op(e3,e0))
| op(op(e2,e3),e1) != op(e2,op(e3,e1))
| op(op(e2,e3),e2) != op(e2,op(e3,e2))
| op(op(e2,e3),e3) != op(e2,op(e3,e3))
| op(op(e3,e0),e0) != op(e3,op(e0,e0))
| op(op(e3,e0),e1) != op(e3,op(e0,e1))
| op(op(e3,e0),e2) != op(e3,op(e0,e2))
| op(op(e3,e0),e3) != op(e3,op(e0,e3))
| op(op(e3,e1),e0) != op(e3,op(e1,e0))
| op(op(e3,e1),e1) != op(e3,op(e1,e1))
| op(op(e3,e1),e2) != op(e3,op(e1,e2))
| op(op(e3,e1),e3) != op(e3,op(e1,e3))
| op(op(e3,e2),e0) != op(e3,op(e2,e0))
| op(op(e3,e2),e1) != op(e3,op(e2,e1))
| op(op(e3,e2),e2) != op(e3,op(e2,e2))
| op(op(e3,e2),e3) != op(e3,op(e2,e3))
| op(op(e3,e3),e0) != op(e3,op(e3,e0))
| op(op(e3,e3),e1) != op(e3,op(e3,e1))
| op(op(e3,e3),e2) != op(e3,op(e3,e2))
| op(op(e3,e3),e3) != op(e3,op(e3,e3))
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| sP4
| unit != op(e0,inv(e0))
| unit != op(inv(e0),e0)
| unit != op(e1,inv(e1))
| unit != op(inv(e1),e1)
| unit != op(e2,inv(e2))
| unit != op(inv(e2),e2)
| unit != op(e3,inv(e3))
| unit != op(inv(e3),e3)
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f29]) ).
fof(f169,plain,
unit = op(unit,unit),
inference(definition_unfolding,[],[f72,f73,f73,f73]) ).
fof(f170,plain,
e1 = op(unit,e1),
inference(definition_unfolding,[],[f71,f73]) ).
fof(f171,plain,
e2 = op(unit,e2),
inference(definition_unfolding,[],[f70,f73]) ).
fof(f172,plain,
e3 = op(unit,e3),
inference(definition_unfolding,[],[f69,f73]) ).
fof(f173,plain,
e1 = op(e1,unit),
inference(definition_unfolding,[],[f68,f73]) ).
fof(f174,plain,
op(e1,e1) = unit,
inference(definition_unfolding,[],[f67,f73]) ).
fof(f175,plain,
e2 = op(e2,unit),
inference(definition_unfolding,[],[f64,f73]) ).
fof(f176,plain,
op(e2,e2) = unit,
inference(definition_unfolding,[],[f62,f73]) ).
fof(f177,plain,
e3 = op(e3,unit),
inference(definition_unfolding,[],[f60,f73]) ).
fof(f178,plain,
op(e3,e3) = unit,
inference(definition_unfolding,[],[f57,f73]) ).
fof(f179,plain,
unit = inv(unit),
inference(definition_unfolding,[],[f77,f73,f73]) ).
fof(f180,plain,
( unit != op(unit,unit)
| ~ sP20 ),
inference(definition_unfolding,[],[f81,f73,f73,f73]) ).
fof(f185,plain,
( e1 != op(unit,e1)
| ~ sP19 ),
inference(definition_unfolding,[],[f84,f73]) ).
fof(f190,plain,
( e2 != op(unit,e2)
| ~ sP18 ),
inference(definition_unfolding,[],[f87,f73]) ).
fof(f195,plain,
( e3 != op(unit,e3)
| ~ sP17 ),
inference(definition_unfolding,[],[f90,f73]) ).
fof(f197,plain,
( e1 != op(e1,unit)
| ~ sP16 ),
inference(definition_unfolding,[],[f96,f73]) ).
fof(f200,plain,
( op(e1,e1) != unit
| ~ sP15 ),
inference(definition_unfolding,[],[f101,f73]) ).
fof(f205,plain,
( e2 != op(e2,unit)
| ~ sP12 ),
inference(definition_unfolding,[],[f111,f73]) ).
fof(f208,plain,
( op(e2,e2) != unit
| ~ sP10 ),
inference(definition_unfolding,[],[f121,f73]) ).
fof(f213,plain,
( e3 != op(e3,unit)
| ~ sP8 ),
inference(definition_unfolding,[],[f126,f73]) ).
fof(f216,plain,
( op(e3,e3) != unit
| ~ sP5 ),
inference(definition_unfolding,[],[f141,f73]) ).
fof(f217,plain,
( unit != unit
| ~ sP4 ),
inference(definition_unfolding,[],[f145,f73]) ).
fof(f218,plain,
( unit != inv(unit)
| ~ sP3 ),
inference(definition_unfolding,[],[f149,f73,f73]) ).
fof(f225,plain,
( unit != op(unit,unit)
| op(e1,e1) != unit
| op(e2,e2) != unit
| op(e3,e3) != unit
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| op(op(unit,unit),unit) != op(unit,op(unit,unit))
| op(op(unit,unit),e1) != op(unit,op(unit,e1))
| op(op(unit,unit),e2) != op(unit,op(unit,e2))
| op(op(unit,unit),e3) != op(unit,op(unit,e3))
| op(op(unit,e1),unit) != op(unit,op(e1,unit))
| op(op(unit,e1),e1) != op(unit,op(e1,e1))
| op(op(unit,e1),e2) != op(unit,op(e1,e2))
| op(op(unit,e1),e3) != op(unit,op(e1,e3))
| op(op(unit,e2),unit) != op(unit,op(e2,unit))
| op(op(unit,e2),e1) != op(unit,op(e2,e1))
| op(op(unit,e2),e2) != op(unit,op(e2,e2))
| op(op(unit,e2),e3) != op(unit,op(e2,e3))
| op(op(unit,e3),unit) != op(unit,op(e3,unit))
| op(op(unit,e3),e1) != op(unit,op(e3,e1))
| op(op(unit,e3),e2) != op(unit,op(e3,e2))
| op(op(unit,e3),e3) != op(unit,op(e3,e3))
| op(op(e1,unit),unit) != op(e1,op(unit,unit))
| op(op(e1,unit),e1) != op(e1,op(unit,e1))
| op(op(e1,unit),e2) != op(e1,op(unit,e2))
| op(op(e1,unit),e3) != op(e1,op(unit,e3))
| op(op(e1,e1),unit) != op(e1,op(e1,unit))
| op(op(e1,e1),e1) != op(e1,op(e1,e1))
| op(op(e1,e1),e2) != op(e1,op(e1,e2))
| op(op(e1,e1),e3) != op(e1,op(e1,e3))
| op(op(e1,e2),unit) != op(e1,op(e2,unit))
| op(op(e1,e2),e1) != op(e1,op(e2,e1))
| op(op(e1,e2),e2) != op(e1,op(e2,e2))
| op(op(e1,e2),e3) != op(e1,op(e2,e3))
| op(op(e1,e3),unit) != op(e1,op(e3,unit))
| op(op(e1,e3),e1) != op(e1,op(e3,e1))
| op(op(e1,e3),e2) != op(e1,op(e3,e2))
| op(op(e1,e3),e3) != op(e1,op(e3,e3))
| op(op(e2,unit),unit) != op(e2,op(unit,unit))
| op(op(e2,unit),e1) != op(e2,op(unit,e1))
| op(op(e2,unit),e2) != op(e2,op(unit,e2))
| op(op(e2,unit),e3) != op(e2,op(unit,e3))
| op(op(e2,e1),unit) != op(e2,op(e1,unit))
| op(op(e2,e1),e1) != op(e2,op(e1,e1))
| op(op(e2,e1),e2) != op(e2,op(e1,e2))
| op(op(e2,e1),e3) != op(e2,op(e1,e3))
| op(op(e2,e2),unit) != op(e2,op(e2,unit))
| op(op(e2,e2),e1) != op(e2,op(e2,e1))
| op(op(e2,e2),e2) != op(e2,op(e2,e2))
| op(op(e2,e2),e3) != op(e2,op(e2,e3))
| op(op(e2,e3),unit) != op(e2,op(e3,unit))
| op(op(e2,e3),e1) != op(e2,op(e3,e1))
| op(op(e2,e3),e2) != op(e2,op(e3,e2))
| op(op(e2,e3),e3) != op(e2,op(e3,e3))
| op(op(e3,unit),unit) != op(e3,op(unit,unit))
| op(op(e3,unit),e1) != op(e3,op(unit,e1))
| op(op(e3,unit),e2) != op(e3,op(unit,e2))
| op(op(e3,unit),e3) != op(e3,op(unit,e3))
| op(op(e3,e1),unit) != op(e3,op(e1,unit))
| op(op(e3,e1),e1) != op(e3,op(e1,e1))
| op(op(e3,e1),e2) != op(e3,op(e1,e2))
| op(op(e3,e1),e3) != op(e3,op(e1,e3))
| op(op(e3,e2),unit) != op(e3,op(e2,unit))
| op(op(e3,e2),e1) != op(e3,op(e2,e1))
| op(op(e3,e2),e2) != op(e3,op(e2,e2))
| op(op(e3,e2),e3) != op(e3,op(e2,e3))
| op(op(e3,e3),unit) != op(e3,op(e3,unit))
| op(op(e3,e3),e1) != op(e3,op(e3,e1))
| op(op(e3,e3),e2) != op(e3,op(e3,e2))
| op(op(e3,e3),e3) != op(e3,op(e3,e3))
| unit != op(unit,unit)
| unit != op(unit,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| sP4
| unit != op(unit,inv(unit))
| unit != op(inv(unit),unit)
| unit != op(e1,inv(e1))
| unit != op(inv(e1),e1)
| unit != op(e2,inv(e2))
| unit != op(inv(e2),e2)
| unit != op(e3,inv(e3))
| unit != op(inv(e3),e3)
| sP3
| sP2
| sP1
| sP0 ),
inference(definition_unfolding,[],[f165,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73,f73]) ).
fof(f232,plain,
( unit != op(unit,unit)
| op(e1,e1) != unit
| op(e2,e2) != unit
| op(e3,e3) != unit
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| op(op(unit,unit),unit) != op(unit,op(unit,unit))
| op(op(unit,unit),e1) != op(unit,op(unit,e1))
| op(op(unit,unit),e2) != op(unit,op(unit,e2))
| op(op(unit,unit),e3) != op(unit,op(unit,e3))
| op(op(unit,e1),unit) != op(unit,op(e1,unit))
| op(op(unit,e1),e1) != op(unit,op(e1,e1))
| op(op(unit,e1),e2) != op(unit,op(e1,e2))
| op(op(unit,e1),e3) != op(unit,op(e1,e3))
| op(op(unit,e2),unit) != op(unit,op(e2,unit))
| op(op(unit,e2),e1) != op(unit,op(e2,e1))
| op(op(unit,e2),e2) != op(unit,op(e2,e2))
| op(op(unit,e2),e3) != op(unit,op(e2,e3))
| op(op(unit,e3),unit) != op(unit,op(e3,unit))
| op(op(unit,e3),e1) != op(unit,op(e3,e1))
| op(op(unit,e3),e2) != op(unit,op(e3,e2))
| op(op(unit,e3),e3) != op(unit,op(e3,e3))
| op(op(e1,unit),unit) != op(e1,op(unit,unit))
| op(op(e1,unit),e1) != op(e1,op(unit,e1))
| op(op(e1,unit),e2) != op(e1,op(unit,e2))
| op(op(e1,unit),e3) != op(e1,op(unit,e3))
| op(op(e1,e1),unit) != op(e1,op(e1,unit))
| op(op(e1,e1),e1) != op(e1,op(e1,e1))
| op(op(e1,e1),e2) != op(e1,op(e1,e2))
| op(op(e1,e1),e3) != op(e1,op(e1,e3))
| op(op(e1,e2),unit) != op(e1,op(e2,unit))
| op(op(e1,e2),e1) != op(e1,op(e2,e1))
| op(op(e1,e2),e2) != op(e1,op(e2,e2))
| op(op(e1,e2),e3) != op(e1,op(e2,e3))
| op(op(e1,e3),unit) != op(e1,op(e3,unit))
| op(op(e1,e3),e1) != op(e1,op(e3,e1))
| op(op(e1,e3),e2) != op(e1,op(e3,e2))
| op(op(e1,e3),e3) != op(e1,op(e3,e3))
| op(op(e2,unit),unit) != op(e2,op(unit,unit))
| op(op(e2,unit),e1) != op(e2,op(unit,e1))
| op(op(e2,unit),e2) != op(e2,op(unit,e2))
| op(op(e2,unit),e3) != op(e2,op(unit,e3))
| op(op(e2,e1),unit) != op(e2,op(e1,unit))
| op(op(e2,e1),e1) != op(e2,op(e1,e1))
| op(op(e2,e1),e2) != op(e2,op(e1,e2))
| op(op(e2,e1),e3) != op(e2,op(e1,e3))
| op(op(e2,e2),unit) != op(e2,op(e2,unit))
| op(op(e2,e2),e1) != op(e2,op(e2,e1))
| op(op(e2,e2),e2) != op(e2,op(e2,e2))
| op(op(e2,e2),e3) != op(e2,op(e2,e3))
| op(op(e2,e3),unit) != op(e2,op(e3,unit))
| op(op(e2,e3),e1) != op(e2,op(e3,e1))
| op(op(e2,e3),e2) != op(e2,op(e3,e2))
| op(op(e2,e3),e3) != op(e2,op(e3,e3))
| op(op(e3,unit),unit) != op(e3,op(unit,unit))
| op(op(e3,unit),e1) != op(e3,op(unit,e1))
| op(op(e3,unit),e2) != op(e3,op(unit,e2))
| op(op(e3,unit),e3) != op(e3,op(unit,e3))
| op(op(e3,e1),unit) != op(e3,op(e1,unit))
| op(op(e3,e1),e1) != op(e3,op(e1,e1))
| op(op(e3,e1),e2) != op(e3,op(e1,e2))
| op(op(e3,e1),e3) != op(e3,op(e1,e3))
| op(op(e3,e2),unit) != op(e3,op(e2,unit))
| op(op(e3,e2),e1) != op(e3,op(e2,e1))
| op(op(e3,e2),e2) != op(e3,op(e2,e2))
| op(op(e3,e2),e3) != op(e3,op(e2,e3))
| op(op(e3,e3),unit) != op(e3,op(e3,unit))
| op(op(e3,e3),e1) != op(e3,op(e3,e1))
| op(op(e3,e3),e2) != op(e3,op(e3,e2))
| op(op(e3,e3),e3) != op(e3,op(e3,e3))
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| sP4
| unit != op(unit,inv(unit))
| unit != op(inv(unit),unit)
| unit != op(e1,inv(e1))
| unit != op(inv(e1),e1)
| unit != op(e2,inv(e2))
| unit != op(inv(e2),e2)
| unit != op(e3,inv(e3))
| unit != op(inv(e3),e3)
| sP3
| sP2
| sP1
| sP0 ),
inference(duplicate_literal_removal,[],[f225]) ).
fof(f233,plain,
~ sP4,
inference(trivial_inequality_removal,[],[f217]) ).
fof(f235,definition,
( spl21_1
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition]) ).
fof(f239,definition,
( spl21_2
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition]) ).
fof(f243,definition,
( spl21_3
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
fof(f247,definition,
( spl21_4
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl21_4])],[avatar_definition]) ).
fof(f251,definition,
( spl21_5
<=> unit = op(inv(e3),e3) ),
introduced(definition,[new_symbols(definition,[spl21_5])],[avatar_definition]) ).
fof(f253,plain,
( unit != op(inv(e3),e3)
| spl21_5 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f255,definition,
( spl21_6
<=> unit = op(e3,inv(e3)) ),
introduced(definition,[new_symbols(definition,[spl21_6])],[avatar_definition]) ).
fof(f257,plain,
( unit != op(e3,inv(e3))
| spl21_6 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f259,definition,
( spl21_7
<=> unit = op(inv(e2),e2) ),
introduced(definition,[new_symbols(definition,[spl21_7])],[avatar_definition]) ).
fof(f261,plain,
( unit != op(inv(e2),e2)
| spl21_7 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f263,definition,
( spl21_8
<=> unit = op(e2,inv(e2)) ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
fof(f265,plain,
( unit != op(e2,inv(e2))
| spl21_8 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f267,definition,
( spl21_9
<=> unit = op(inv(e1),e1) ),
introduced(definition,[new_symbols(definition,[spl21_9])],[avatar_definition]) ).
fof(f269,plain,
( unit != op(inv(e1),e1)
| spl21_9 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl21_10
<=> unit = op(e1,inv(e1)) ),
introduced(definition,[new_symbols(definition,[spl21_10])],[avatar_definition]) ).
fof(f273,plain,
( unit != op(e1,inv(e1))
| spl21_10 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f275,definition,
( spl21_11
<=> unit = op(inv(unit),unit) ),
introduced(definition,[new_symbols(definition,[spl21_11])],[avatar_definition]) ).
fof(f277,plain,
( unit != op(inv(unit),unit)
| spl21_11 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl21_12
<=> unit = op(unit,inv(unit)) ),
introduced(definition,[new_symbols(definition,[spl21_12])],[avatar_definition]) ).
fof(f281,plain,
( unit != op(unit,inv(unit))
| spl21_12 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f283,definition,
( spl21_13
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl21_13])],[avatar_definition]) ).
fof(f287,definition,
( spl21_14
<=> e3 = op(e3,unit) ),
introduced(definition,[new_symbols(definition,[spl21_14])],[avatar_definition]) ).
fof(f288,plain,
( e3 = op(e3,unit)
| ~ spl21_14 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f291,definition,
( spl21_15
<=> e3 = op(unit,e3) ),
introduced(definition,[new_symbols(definition,[spl21_15])],[avatar_definition]) ).
fof(f292,plain,
( e3 = op(unit,e3)
| ~ spl21_15 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f295,definition,
( spl21_16
<=> e2 = op(e2,unit) ),
introduced(definition,[new_symbols(definition,[spl21_16])],[avatar_definition]) ).
fof(f296,plain,
( e2 = op(e2,unit)
| ~ spl21_16 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl21_17
<=> e2 = op(unit,e2) ),
introduced(definition,[new_symbols(definition,[spl21_17])],[avatar_definition]) ).
fof(f300,plain,
( e2 = op(unit,e2)
| ~ spl21_17 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f303,definition,
( spl21_18
<=> e1 = op(e1,unit) ),
introduced(definition,[new_symbols(definition,[spl21_18])],[avatar_definition]) ).
fof(f304,plain,
( e1 = op(e1,unit)
| ~ spl21_18 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl21_19
<=> e1 = op(unit,e1) ),
introduced(definition,[new_symbols(definition,[spl21_19])],[avatar_definition]) ).
fof(f308,plain,
( e1 = op(unit,e1)
| ~ spl21_19 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl21_20
<=> unit = op(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl21_20])],[avatar_definition]) ).
fof(f312,plain,
( unit = op(unit,unit)
| ~ spl21_20 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl21_21
<=> op(op(e3,e3),e3) = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_21])],[avatar_definition]) ).
fof(f317,plain,
( op(op(e3,e3),e3) != op(e3,op(e3,e3))
| spl21_21 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl21_22
<=> op(op(e3,e3),e2) = op(e3,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_22])],[avatar_definition]) ).
fof(f321,plain,
( op(op(e3,e3),e2) != op(e3,op(e3,e2))
| spl21_22 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f323,definition,
( spl21_23
<=> op(op(e3,e3),e1) = op(e3,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_23])],[avatar_definition]) ).
fof(f325,plain,
( op(op(e3,e3),e1) != op(e3,op(e3,e1))
| spl21_23 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f327,definition,
( spl21_24
<=> op(op(e3,e3),unit) = op(e3,op(e3,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_24])],[avatar_definition]) ).
fof(f329,plain,
( op(op(e3,e3),unit) != op(e3,op(e3,unit))
| spl21_24 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f331,definition,
( spl21_25
<=> op(op(e3,e2),e3) = op(e3,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_25])],[avatar_definition]) ).
fof(f333,plain,
( op(op(e3,e2),e3) != op(e3,op(e2,e3))
| spl21_25 ),
inference(avatar_component_clause,[],[f331]) ).
fof(f335,definition,
( spl21_26
<=> op(op(e3,e2),e2) = op(e3,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_26])],[avatar_definition]) ).
fof(f337,plain,
( op(op(e3,e2),e2) != op(e3,op(e2,e2))
| spl21_26 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl21_27
<=> op(op(e3,e2),e1) = op(e3,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_27])],[avatar_definition]) ).
fof(f341,plain,
( op(op(e3,e2),e1) != op(e3,op(e2,e1))
| spl21_27 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f343,definition,
( spl21_28
<=> op(op(e3,e2),unit) = op(e3,op(e2,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_28])],[avatar_definition]) ).
fof(f345,plain,
( op(op(e3,e2),unit) != op(e3,op(e2,unit))
| spl21_28 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f347,definition,
( spl21_29
<=> op(op(e3,e1),e3) = op(e3,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_29])],[avatar_definition]) ).
fof(f349,plain,
( op(op(e3,e1),e3) != op(e3,op(e1,e3))
| spl21_29 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f351,definition,
( spl21_30
<=> op(op(e3,e1),e2) = op(e3,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_30])],[avatar_definition]) ).
fof(f353,plain,
( op(op(e3,e1),e2) != op(e3,op(e1,e2))
| spl21_30 ),
inference(avatar_component_clause,[],[f351]) ).
fof(f355,definition,
( spl21_31
<=> op(op(e3,e1),e1) = op(e3,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_31])],[avatar_definition]) ).
fof(f357,plain,
( op(op(e3,e1),e1) != op(e3,op(e1,e1))
| spl21_31 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f359,definition,
( spl21_32
<=> op(op(e3,e1),unit) = op(e3,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_32])],[avatar_definition]) ).
fof(f361,plain,
( op(op(e3,e1),unit) != op(e3,op(e1,unit))
| spl21_32 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f363,definition,
( spl21_33
<=> op(op(e3,unit),e3) = op(e3,op(unit,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_33])],[avatar_definition]) ).
fof(f365,plain,
( op(op(e3,unit),e3) != op(e3,op(unit,e3))
| spl21_33 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f367,definition,
( spl21_34
<=> op(op(e3,unit),e2) = op(e3,op(unit,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_34])],[avatar_definition]) ).
fof(f369,plain,
( op(op(e3,unit),e2) != op(e3,op(unit,e2))
| spl21_34 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f371,definition,
( spl21_35
<=> op(op(e3,unit),e1) = op(e3,op(unit,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_35])],[avatar_definition]) ).
fof(f373,plain,
( op(op(e3,unit),e1) != op(e3,op(unit,e1))
| spl21_35 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f375,definition,
( spl21_36
<=> op(op(e3,unit),unit) = op(e3,op(unit,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_36])],[avatar_definition]) ).
fof(f377,plain,
( op(op(e3,unit),unit) != op(e3,op(unit,unit))
| spl21_36 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f379,definition,
( spl21_37
<=> op(op(e2,e3),e3) = op(e2,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_37])],[avatar_definition]) ).
fof(f381,plain,
( op(op(e2,e3),e3) != op(e2,op(e3,e3))
| spl21_37 ),
inference(avatar_component_clause,[],[f379]) ).
fof(f383,definition,
( spl21_38
<=> op(op(e2,e3),e2) = op(e2,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_38])],[avatar_definition]) ).
fof(f385,plain,
( op(op(e2,e3),e2) != op(e2,op(e3,e2))
| spl21_38 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f387,definition,
( spl21_39
<=> op(op(e2,e3),e1) = op(e2,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_39])],[avatar_definition]) ).
fof(f389,plain,
( op(op(e2,e3),e1) != op(e2,op(e3,e1))
| spl21_39 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f391,definition,
( spl21_40
<=> op(op(e2,e3),unit) = op(e2,op(e3,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_40])],[avatar_definition]) ).
fof(f393,plain,
( op(op(e2,e3),unit) != op(e2,op(e3,unit))
| spl21_40 ),
inference(avatar_component_clause,[],[f391]) ).
fof(f395,definition,
( spl21_41
<=> op(op(e2,e2),e3) = op(e2,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_41])],[avatar_definition]) ).
fof(f397,plain,
( op(op(e2,e2),e3) != op(e2,op(e2,e3))
| spl21_41 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f399,definition,
( spl21_42
<=> op(op(e2,e2),e2) = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_42])],[avatar_definition]) ).
fof(f401,plain,
( op(op(e2,e2),e2) != op(e2,op(e2,e2))
| spl21_42 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f403,definition,
( spl21_43
<=> op(op(e2,e2),e1) = op(e2,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_43])],[avatar_definition]) ).
fof(f405,plain,
( op(op(e2,e2),e1) != op(e2,op(e2,e1))
| spl21_43 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f407,definition,
( spl21_44
<=> op(op(e2,e2),unit) = op(e2,op(e2,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_44])],[avatar_definition]) ).
fof(f409,plain,
( op(op(e2,e2),unit) != op(e2,op(e2,unit))
| spl21_44 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f411,definition,
( spl21_45
<=> op(op(e2,e1),e3) = op(e2,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_45])],[avatar_definition]) ).
fof(f413,plain,
( op(op(e2,e1),e3) != op(e2,op(e1,e3))
| spl21_45 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f415,definition,
( spl21_46
<=> op(op(e2,e1),e2) = op(e2,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_46])],[avatar_definition]) ).
fof(f417,plain,
( op(op(e2,e1),e2) != op(e2,op(e1,e2))
| spl21_46 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f419,definition,
( spl21_47
<=> op(op(e2,e1),e1) = op(e2,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_47])],[avatar_definition]) ).
fof(f421,plain,
( op(op(e2,e1),e1) != op(e2,op(e1,e1))
| spl21_47 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f423,definition,
( spl21_48
<=> op(op(e2,e1),unit) = op(e2,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_48])],[avatar_definition]) ).
fof(f425,plain,
( op(op(e2,e1),unit) != op(e2,op(e1,unit))
| spl21_48 ),
inference(avatar_component_clause,[],[f423]) ).
fof(f427,definition,
( spl21_49
<=> op(op(e2,unit),e3) = op(e2,op(unit,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_49])],[avatar_definition]) ).
fof(f429,plain,
( op(op(e2,unit),e3) != op(e2,op(unit,e3))
| spl21_49 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f431,definition,
( spl21_50
<=> op(op(e2,unit),e2) = op(e2,op(unit,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_50])],[avatar_definition]) ).
fof(f433,plain,
( op(op(e2,unit),e2) != op(e2,op(unit,e2))
| spl21_50 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f435,definition,
( spl21_51
<=> op(op(e2,unit),e1) = op(e2,op(unit,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_51])],[avatar_definition]) ).
fof(f437,plain,
( op(op(e2,unit),e1) != op(e2,op(unit,e1))
| spl21_51 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f439,definition,
( spl21_52
<=> op(op(e2,unit),unit) = op(e2,op(unit,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_52])],[avatar_definition]) ).
fof(f441,plain,
( op(op(e2,unit),unit) != op(e2,op(unit,unit))
| spl21_52 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f443,definition,
( spl21_53
<=> op(op(e1,e3),e3) = op(e1,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_53])],[avatar_definition]) ).
fof(f445,plain,
( op(op(e1,e3),e3) != op(e1,op(e3,e3))
| spl21_53 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl21_54
<=> op(op(e1,e3),e2) = op(e1,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_54])],[avatar_definition]) ).
fof(f449,plain,
( op(op(e1,e3),e2) != op(e1,op(e3,e2))
| spl21_54 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f451,definition,
( spl21_55
<=> op(op(e1,e3),e1) = op(e1,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_55])],[avatar_definition]) ).
fof(f453,plain,
( op(op(e1,e3),e1) != op(e1,op(e3,e1))
| spl21_55 ),
inference(avatar_component_clause,[],[f451]) ).
fof(f455,definition,
( spl21_56
<=> op(op(e1,e3),unit) = op(e1,op(e3,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_56])],[avatar_definition]) ).
fof(f457,plain,
( op(op(e1,e3),unit) != op(e1,op(e3,unit))
| spl21_56 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl21_57
<=> op(op(e1,e2),e3) = op(e1,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_57])],[avatar_definition]) ).
fof(f461,plain,
( op(op(e1,e2),e3) != op(e1,op(e2,e3))
| spl21_57 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f463,definition,
( spl21_58
<=> op(op(e1,e2),e2) = op(e1,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_58])],[avatar_definition]) ).
fof(f465,plain,
( op(op(e1,e2),e2) != op(e1,op(e2,e2))
| spl21_58 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f467,definition,
( spl21_59
<=> op(op(e1,e2),e1) = op(e1,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_59])],[avatar_definition]) ).
fof(f469,plain,
( op(op(e1,e2),e1) != op(e1,op(e2,e1))
| spl21_59 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f471,definition,
( spl21_60
<=> op(op(e1,e2),unit) = op(e1,op(e2,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_60])],[avatar_definition]) ).
fof(f473,plain,
( op(op(e1,e2),unit) != op(e1,op(e2,unit))
| spl21_60 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f475,definition,
( spl21_61
<=> op(op(e1,e1),e3) = op(e1,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_61])],[avatar_definition]) ).
fof(f477,plain,
( op(op(e1,e1),e3) != op(e1,op(e1,e3))
| spl21_61 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl21_62
<=> op(op(e1,e1),e2) = op(e1,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_62])],[avatar_definition]) ).
fof(f481,plain,
( op(op(e1,e1),e2) != op(e1,op(e1,e2))
| spl21_62 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f483,definition,
( spl21_63
<=> op(op(e1,e1),e1) = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_63])],[avatar_definition]) ).
fof(f485,plain,
( op(op(e1,e1),e1) != op(e1,op(e1,e1))
| spl21_63 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f487,definition,
( spl21_64
<=> op(op(e1,e1),unit) = op(e1,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_64])],[avatar_definition]) ).
fof(f489,plain,
( op(op(e1,e1),unit) != op(e1,op(e1,unit))
| spl21_64 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f491,definition,
( spl21_65
<=> op(op(e1,unit),e3) = op(e1,op(unit,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_65])],[avatar_definition]) ).
fof(f493,plain,
( op(op(e1,unit),e3) != op(e1,op(unit,e3))
| spl21_65 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f495,definition,
( spl21_66
<=> op(op(e1,unit),e2) = op(e1,op(unit,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_66])],[avatar_definition]) ).
fof(f497,plain,
( op(op(e1,unit),e2) != op(e1,op(unit,e2))
| spl21_66 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f499,definition,
( spl21_67
<=> op(op(e1,unit),e1) = op(e1,op(unit,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_67])],[avatar_definition]) ).
fof(f501,plain,
( op(op(e1,unit),e1) != op(e1,op(unit,e1))
| spl21_67 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f503,definition,
( spl21_68
<=> op(op(e1,unit),unit) = op(e1,op(unit,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_68])],[avatar_definition]) ).
fof(f505,plain,
( op(op(e1,unit),unit) != op(e1,op(unit,unit))
| spl21_68 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f507,definition,
( spl21_69
<=> op(op(unit,e3),e3) = op(unit,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_69])],[avatar_definition]) ).
fof(f509,plain,
( op(op(unit,e3),e3) != op(unit,op(e3,e3))
| spl21_69 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,definition,
( spl21_70
<=> op(op(unit,e3),e2) = op(unit,op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_70])],[avatar_definition]) ).
fof(f513,plain,
( op(op(unit,e3),e2) != op(unit,op(e3,e2))
| spl21_70 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f515,definition,
( spl21_71
<=> op(op(unit,e3),e1) = op(unit,op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_71])],[avatar_definition]) ).
fof(f517,plain,
( op(op(unit,e3),e1) != op(unit,op(e3,e1))
| spl21_71 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f519,definition,
( spl21_72
<=> op(op(unit,e3),unit) = op(unit,op(e3,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_72])],[avatar_definition]) ).
fof(f521,plain,
( op(op(unit,e3),unit) != op(unit,op(e3,unit))
| spl21_72 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f523,definition,
( spl21_73
<=> op(op(unit,e2),e3) = op(unit,op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_73])],[avatar_definition]) ).
fof(f525,plain,
( op(op(unit,e2),e3) != op(unit,op(e2,e3))
| spl21_73 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl21_74
<=> op(op(unit,e2),e2) = op(unit,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_74])],[avatar_definition]) ).
fof(f529,plain,
( op(op(unit,e2),e2) != op(unit,op(e2,e2))
| spl21_74 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f531,definition,
( spl21_75
<=> op(op(unit,e2),e1) = op(unit,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_75])],[avatar_definition]) ).
fof(f533,plain,
( op(op(unit,e2),e1) != op(unit,op(e2,e1))
| spl21_75 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f535,definition,
( spl21_76
<=> op(op(unit,e2),unit) = op(unit,op(e2,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_76])],[avatar_definition]) ).
fof(f537,plain,
( op(op(unit,e2),unit) != op(unit,op(e2,unit))
| spl21_76 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f539,definition,
( spl21_77
<=> op(op(unit,e1),e3) = op(unit,op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_77])],[avatar_definition]) ).
fof(f541,plain,
( op(op(unit,e1),e3) != op(unit,op(e1,e3))
| spl21_77 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f543,definition,
( spl21_78
<=> op(op(unit,e1),e2) = op(unit,op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_78])],[avatar_definition]) ).
fof(f545,plain,
( op(op(unit,e1),e2) != op(unit,op(e1,e2))
| spl21_78 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f547,definition,
( spl21_79
<=> op(op(unit,e1),e1) = op(unit,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_79])],[avatar_definition]) ).
fof(f549,plain,
( op(op(unit,e1),e1) != op(unit,op(e1,e1))
| spl21_79 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f551,definition,
( spl21_80
<=> op(op(unit,e1),unit) = op(unit,op(e1,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_80])],[avatar_definition]) ).
fof(f553,plain,
( op(op(unit,e1),unit) != op(unit,op(e1,unit))
| spl21_80 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f555,definition,
( spl21_81
<=> op(op(unit,unit),e3) = op(unit,op(unit,e3)) ),
introduced(definition,[new_symbols(definition,[spl21_81])],[avatar_definition]) ).
fof(f557,plain,
( op(op(unit,unit),e3) != op(unit,op(unit,e3))
| spl21_81 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f559,definition,
( spl21_82
<=> op(op(unit,unit),e2) = op(unit,op(unit,e2)) ),
introduced(definition,[new_symbols(definition,[spl21_82])],[avatar_definition]) ).
fof(f561,plain,
( op(op(unit,unit),e2) != op(unit,op(unit,e2))
| spl21_82 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl21_83
<=> op(op(unit,unit),e1) = op(unit,op(unit,e1)) ),
introduced(definition,[new_symbols(definition,[spl21_83])],[avatar_definition]) ).
fof(f565,plain,
( op(op(unit,unit),e1) != op(unit,op(unit,e1))
| spl21_83 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl21_84
<=> op(op(unit,unit),unit) = op(unit,op(unit,unit)) ),
introduced(definition,[new_symbols(definition,[spl21_84])],[avatar_definition]) ).
fof(f569,plain,
( op(op(unit,unit),unit) != op(unit,op(unit,unit))
| spl21_84 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl21_85
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl21_85])],[avatar_definition]) ).
fof(f575,definition,
( spl21_86
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl21_86])],[avatar_definition]) ).
fof(f579,definition,
( spl21_87
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl21_87])],[avatar_definition]) ).
fof(f583,definition,
( spl21_88
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl21_88])],[avatar_definition]) ).
fof(f587,definition,
( spl21_89
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl21_89])],[avatar_definition]) ).
fof(f591,definition,
( spl21_90
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl21_90])],[avatar_definition]) ).
fof(f595,definition,
( spl21_91
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl21_91])],[avatar_definition]) ).
fof(f599,definition,
( spl21_92
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl21_92])],[avatar_definition]) ).
fof(f603,definition,
( spl21_93
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl21_93])],[avatar_definition]) ).
fof(f607,definition,
( spl21_94
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl21_94])],[avatar_definition]) ).
fof(f611,definition,
( spl21_95
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl21_95])],[avatar_definition]) ).
fof(f615,definition,
( spl21_96
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl21_96])],[avatar_definition]) ).
fof(f619,definition,
( spl21_97
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl21_97])],[avatar_definition]) ).
fof(f623,definition,
( spl21_98
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl21_98])],[avatar_definition]) ).
fof(f627,definition,
( spl21_99
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl21_99])],[avatar_definition]) ).
fof(f631,definition,
( spl21_100
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl21_100])],[avatar_definition]) ).
fof(f686,definition,
( spl21_113
<=> op(e3,e3) = unit ),
introduced(definition,[new_symbols(definition,[spl21_113])],[avatar_definition]) ).
fof(f687,plain,
( op(e3,e3) = unit
| ~ spl21_113 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f690,definition,
( spl21_114
<=> op(e2,e2) = unit ),
introduced(definition,[new_symbols(definition,[spl21_114])],[avatar_definition]) ).
fof(f691,plain,
( op(e2,e2) = unit
| ~ spl21_114 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f694,definition,
( spl21_115
<=> op(e1,e1) = unit ),
introduced(definition,[new_symbols(definition,[spl21_115])],[avatar_definition]) ).
fof(f695,plain,
( op(e1,e1) = unit
| ~ spl21_115 ),
inference(avatar_component_clause,[],[f694]) ).
fof(f697,plain,
( spl21_1
| spl21_2
| spl21_3
| spl21_4
| ~ spl21_5
| ~ spl21_6
| ~ spl21_7
| ~ spl21_8
| ~ spl21_9
| ~ spl21_10
| ~ spl21_11
| ~ spl21_12
| spl21_13
| ~ spl21_14
| ~ spl21_15
| ~ spl21_16
| ~ spl21_17
| ~ spl21_18
| ~ spl21_19
| ~ spl21_21
| ~ spl21_22
| ~ spl21_23
| ~ spl21_24
| ~ spl21_25
| ~ spl21_26
| ~ spl21_27
| ~ spl21_28
| ~ spl21_29
| ~ spl21_30
| ~ spl21_31
| ~ spl21_32
| ~ spl21_33
| ~ spl21_34
| ~ spl21_35
| ~ spl21_36
| ~ spl21_37
| ~ spl21_38
| ~ spl21_39
| ~ spl21_40
| ~ spl21_41
| ~ spl21_42
| ~ spl21_43
| ~ spl21_44
| ~ spl21_45
| ~ spl21_46
| ~ spl21_47
| ~ spl21_48
| ~ spl21_49
| ~ spl21_50
| ~ spl21_51
| ~ spl21_52
| ~ spl21_53
| ~ spl21_54
| ~ spl21_55
| ~ spl21_56
| ~ spl21_57
| ~ spl21_58
| ~ spl21_59
| ~ spl21_60
| ~ spl21_61
| ~ spl21_62
| ~ spl21_63
| ~ spl21_64
| ~ spl21_65
| ~ spl21_66
| ~ spl21_67
| ~ spl21_68
| ~ spl21_69
| ~ spl21_70
| ~ spl21_71
| ~ spl21_72
| ~ spl21_73
| ~ spl21_74
| ~ spl21_75
| ~ spl21_76
| ~ spl21_77
| ~ spl21_78
| ~ spl21_79
| ~ spl21_80
| ~ spl21_81
| ~ spl21_82
| ~ spl21_83
| ~ spl21_84
| spl21_85
| spl21_86
| spl21_87
| spl21_88
| spl21_89
| spl21_90
| spl21_91
| spl21_92
| spl21_93
| spl21_94
| spl21_95
| spl21_96
| spl21_97
| spl21_98
| spl21_99
| spl21_100
| ~ spl21_113
| ~ spl21_114
| ~ spl21_115
| ~ spl21_20 ),
inference(avatar_split_clause,[],[f232,f311,f694,f690,f686,f631,f627,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f563,f559,f555,f551,f547,f543,f539,f535,f531,f527,f523,f519,f515,f511,f507,f503,f499,f495,f491,f487,f483,f479,f475,f471,f467,f463,f459,f455,f451,f447,f443,f439,f435,f431,f427,f423,f419,f415,f411,f407,f403,f399,f395,f391,f387,f383,f379,f375,f371,f367,f363,f359,f355,f351,f347,f343,f339,f335,f331,f327,f323,f319,f315,f307,f303,f299,f295,f291,f287,f283,f279,f275,f271,f267,f263,f259,f255,f251,f247,f243,f239,f235]) ).
fof(f699,definition,
( spl21_116
<=> e3 = inv(e3) ),
introduced(definition,[new_symbols(definition,[spl21_116])],[avatar_definition]) ).
fof(f700,plain,
( e3 = inv(e3)
| ~ spl21_116 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f702,plain,
( ~ spl21_1
| ~ spl21_116 ),
inference(avatar_split_clause,[],[f158,f699,f235]) ).
fof(f724,definition,
( spl21_121
<=> e2 = inv(e2) ),
introduced(definition,[new_symbols(definition,[spl21_121])],[avatar_definition]) ).
fof(f725,plain,
( e2 = inv(e2)
| ~ spl21_121 ),
inference(avatar_component_clause,[],[f724]) ).
fof(f727,plain,
( ~ spl21_2
| ~ spl21_121 ),
inference(avatar_split_clause,[],[f155,f724,f239]) ).
fof(f749,definition,
( spl21_126
<=> e1 = inv(e1) ),
introduced(definition,[new_symbols(definition,[spl21_126])],[avatar_definition]) ).
fof(f750,plain,
( e1 = inv(e1)
| ~ spl21_126 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f752,plain,
( ~ spl21_3
| ~ spl21_126 ),
inference(avatar_split_clause,[],[f152,f749,f243]) ).
fof(f774,definition,
( spl21_131
<=> unit = inv(unit) ),
introduced(definition,[new_symbols(definition,[spl21_131])],[avatar_definition]) ).
fof(f775,plain,
( unit = inv(unit)
| ~ spl21_131 ),
inference(avatar_component_clause,[],[f774]) ).
fof(f777,plain,
( ~ spl21_4
| ~ spl21_131 ),
inference(avatar_split_clause,[],[f218,f774,f247]) ).
fof(f793,plain,
~ spl21_13,
inference(avatar_split_clause,[],[f233,f283]) ).
fof(f797,plain,
( ~ spl21_85
| ~ spl21_113 ),
inference(avatar_split_clause,[],[f216,f686,f571]) ).
fof(f809,definition,
( spl21_137
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl21_137])],[avatar_definition]) ).
fof(f810,plain,
( e1 = op(e3,e2)
| ~ spl21_137 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f812,plain,
( ~ spl21_86
| ~ spl21_137 ),
inference(avatar_split_clause,[],[f136,f809,f575]) ).
fof(f824,definition,
( spl21_140
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl21_140])],[avatar_definition]) ).
fof(f825,plain,
( e2 = op(e3,e1)
| ~ spl21_140 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f827,plain,
( ~ spl21_87
| ~ spl21_140 ),
inference(avatar_split_clause,[],[f131,f824,f579]) ).
fof(f838,plain,
( ~ spl21_88
| ~ spl21_14 ),
inference(avatar_split_clause,[],[f213,f287,f583]) ).
fof(f865,definition,
( spl21_148
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl21_148])],[avatar_definition]) ).
fof(f866,plain,
( e1 = op(e2,e3)
| ~ spl21_148 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f868,plain,
( ~ spl21_89
| ~ spl21_148 ),
inference(avatar_split_clause,[],[f124,f865,f587]) ).
fof(f877,plain,
( ~ spl21_90
| ~ spl21_114 ),
inference(avatar_split_clause,[],[f208,f690,f591]) ).
fof(f879,definition,
( spl21_150
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl21_150])],[avatar_definition]) ).
fof(f880,plain,
( e3 = op(e2,e1)
| ~ spl21_150 ),
inference(avatar_component_clause,[],[f879]) ).
fof(f882,plain,
( ~ spl21_91
| ~ spl21_150 ),
inference(avatar_split_clause,[],[f114,f879,f595]) ).
fof(f903,plain,
( ~ spl21_92
| ~ spl21_16 ),
inference(avatar_split_clause,[],[f205,f295,f599]) ).
fof(f920,definition,
( spl21_158
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl21_158])],[avatar_definition]) ).
fof(f921,plain,
( e2 = op(e1,e3)
| ~ spl21_158 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f923,plain,
( ~ spl21_93
| ~ spl21_158 ),
inference(avatar_split_clause,[],[f107,f920,f603]) ).
fof(f935,definition,
( spl21_161
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl21_161])],[avatar_definition]) ).
fof(f936,plain,
( e3 = op(e1,e2)
| ~ spl21_161 ),
inference(avatar_component_clause,[],[f935]) ).
fof(f938,plain,
( ~ spl21_94
| ~ spl21_161 ),
inference(avatar_split_clause,[],[f102,f935,f607]) ).
fof(f957,plain,
( ~ spl21_95
| ~ spl21_115 ),
inference(avatar_split_clause,[],[f200,f694,f611]) ).
fof(f968,plain,
( ~ spl21_96
| ~ spl21_18 ),
inference(avatar_split_clause,[],[f197,f303,f615]) ).
fof(f974,plain,
( ~ spl21_97
| ~ spl21_15 ),
inference(avatar_split_clause,[],[f195,f291,f619]) ).
fof(f995,plain,
( ~ spl21_98
| ~ spl21_17 ),
inference(avatar_split_clause,[],[f190,f299,f623]) ).
fof(f1016,plain,
( ~ spl21_99
| ~ spl21_19 ),
inference(avatar_split_clause,[],[f185,f307,f627]) ).
fof(f1025,plain,
( ~ spl21_100
| ~ spl21_20 ),
inference(avatar_split_clause,[],[f180,f311,f631]) ).
fof(f1026,plain,
spl21_116,
inference(avatar_split_clause,[],[f74,f699]) ).
fof(f1027,plain,
spl21_121,
inference(avatar_split_clause,[],[f75,f724]) ).
fof(f1028,plain,
spl21_126,
inference(avatar_split_clause,[],[f76,f749]) ).
fof(f1029,plain,
spl21_131,
inference(avatar_split_clause,[],[f179,f774]) ).
fof(f1030,plain,
spl21_113,
inference(avatar_split_clause,[],[f178,f686]) ).
fof(f1031,plain,
spl21_137,
inference(avatar_split_clause,[],[f58,f809]) ).
fof(f1032,plain,
spl21_140,
inference(avatar_split_clause,[],[f59,f824]) ).
fof(f1033,plain,
spl21_14,
inference(avatar_split_clause,[],[f177,f287]) ).
fof(f1034,plain,
spl21_148,
inference(avatar_split_clause,[],[f61,f865]) ).
fof(f1035,plain,
spl21_114,
inference(avatar_split_clause,[],[f176,f690]) ).
fof(f1036,plain,
spl21_150,
inference(avatar_split_clause,[],[f63,f879]) ).
fof(f1037,plain,
spl21_16,
inference(avatar_split_clause,[],[f175,f295]) ).
fof(f1038,plain,
spl21_158,
inference(avatar_split_clause,[],[f65,f920]) ).
fof(f1039,plain,
spl21_161,
inference(avatar_split_clause,[],[f66,f935]) ).
fof(f1040,plain,
spl21_115,
inference(avatar_split_clause,[],[f174,f694]) ).
fof(f1041,plain,
spl21_18,
inference(avatar_split_clause,[],[f173,f303]) ).
fof(f1042,plain,
spl21_15,
inference(avatar_split_clause,[],[f172,f291]) ).
fof(f1043,plain,
spl21_17,
inference(avatar_split_clause,[],[f171,f299]) ).
fof(f1044,plain,
spl21_19,
inference(avatar_split_clause,[],[f170,f307]) ).
fof(f1045,plain,
spl21_20,
inference(avatar_split_clause,[],[f169,f311]) ).
fof(f1049,plain,
( op(e3,e3) != unit
| spl21_5
| ~ spl21_116 ),
inference(superposition,[],[f253,f700]) ).
fof(f1050,plain,
( $false
| spl21_5
| ~ spl21_113
| ~ spl21_116 ),
inference(forward_subsumption_resolution,[],[f1049,f687]) ).
fof(f1051,plain,
( spl21_5
| ~ spl21_113
| ~ spl21_116 ),
inference(avatar_contradiction_clause,[],[f1050]) ).
fof(f1053,plain,
( op(e3,e3) != unit
| spl21_6
| ~ spl21_116 ),
inference(forward_demodulation,[],[f257,f700]) ).
fof(f1054,plain,
( $false
| spl21_6
| ~ spl21_113
| ~ spl21_116 ),
inference(forward_subsumption_resolution,[],[f1053,f687]) ).
fof(f1055,plain,
( spl21_6
| ~ spl21_113
| ~ spl21_116 ),
inference(avatar_contradiction_clause,[],[f1054]) ).
fof(f1057,plain,
( op(e2,e2) != unit
| spl21_7
| ~ spl21_121 ),
inference(superposition,[],[f261,f725]) ).
fof(f1058,plain,
( $false
| spl21_7
| ~ spl21_114
| ~ spl21_121 ),
inference(forward_subsumption_resolution,[],[f1057,f691]) ).
fof(f1059,plain,
( spl21_7
| ~ spl21_114
| ~ spl21_121 ),
inference(avatar_contradiction_clause,[],[f1058]) ).
fof(f1061,plain,
( op(e2,e2) != unit
| spl21_8
| ~ spl21_121 ),
inference(forward_demodulation,[],[f265,f725]) ).
fof(f1062,plain,
( $false
| spl21_8
| ~ spl21_114
| ~ spl21_121 ),
inference(forward_subsumption_resolution,[],[f1061,f691]) ).
fof(f1063,plain,
( spl21_8
| ~ spl21_114
| ~ spl21_121 ),
inference(avatar_contradiction_clause,[],[f1062]) ).
fof(f1065,plain,
( op(e1,e1) != unit
| spl21_9
| ~ spl21_126 ),
inference(superposition,[],[f269,f750]) ).
fof(f1066,plain,
( $false
| spl21_9
| ~ spl21_115
| ~ spl21_126 ),
inference(forward_subsumption_resolution,[],[f1065,f695]) ).
fof(f1067,plain,
( spl21_9
| ~ spl21_115
| ~ spl21_126 ),
inference(avatar_contradiction_clause,[],[f1066]) ).
fof(f1069,plain,
( op(e1,e1) != unit
| spl21_10
| ~ spl21_126 ),
inference(forward_demodulation,[],[f273,f750]) ).
fof(f1070,plain,
( $false
| spl21_10
| ~ spl21_115
| ~ spl21_126 ),
inference(forward_subsumption_resolution,[],[f1069,f695]) ).
fof(f1071,plain,
( spl21_10
| ~ spl21_115
| ~ spl21_126 ),
inference(avatar_contradiction_clause,[],[f1070]) ).
fof(f1073,plain,
( unit != op(unit,unit)
| spl21_11
| ~ spl21_131 ),
inference(superposition,[],[f277,f775]) ).
fof(f1074,plain,
( $false
| spl21_11
| ~ spl21_20
| ~ spl21_131 ),
inference(forward_subsumption_resolution,[],[f1073,f312]) ).
fof(f1075,plain,
( spl21_11
| ~ spl21_20
| ~ spl21_131 ),
inference(avatar_contradiction_clause,[],[f1074]) ).
fof(f1077,plain,
( unit != op(unit,unit)
| spl21_12
| ~ spl21_131 ),
inference(forward_demodulation,[],[f281,f775]) ).
fof(f1078,plain,
( $false
| spl21_12
| ~ spl21_20
| ~ spl21_131 ),
inference(forward_subsumption_resolution,[],[f1077,f312]) ).
fof(f1079,plain,
( spl21_12
| ~ spl21_20
| ~ spl21_131 ),
inference(avatar_contradiction_clause,[],[f1078]) ).
fof(f1081,plain,
( op(unit,e3) != op(e3,unit)
| spl21_21
| ~ spl21_113 ),
inference(forward_demodulation,[],[f317,f687]) ).
fof(f1082,plain,
( e3 != op(unit,e3)
| ~ spl21_14
| spl21_21
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1081,f288]) ).
fof(f1083,plain,
( $false
| ~ spl21_14
| ~ spl21_15
| spl21_21
| ~ spl21_113 ),
inference(forward_subsumption_resolution,[],[f1082,f292]) ).
fof(f1084,plain,
( ~ spl21_14
| ~ spl21_15
| spl21_21
| ~ spl21_113 ),
inference(avatar_contradiction_clause,[],[f1083]) ).
fof(f1086,plain,
( op(e3,op(e3,e2)) != op(unit,e2)
| spl21_22
| ~ spl21_113 ),
inference(forward_demodulation,[],[f321,f687]) ).
fof(f1088,plain,
( e2 != op(e3,op(e3,e2))
| ~ spl21_17
| spl21_22
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1086,f300]) ).
fof(f1089,plain,
( e2 != op(e3,e1)
| ~ spl21_17
| spl21_22
| ~ spl21_113
| ~ spl21_137 ),
inference(superposition,[],[f1088,f810]) ).
fof(f1090,plain,
( ~ spl21_140
| ~ spl21_17
| spl21_22
| ~ spl21_113
| ~ spl21_137 ),
inference(avatar_split_clause,[],[f1089,f809,f686,f319,f299,f824]) ).
fof(f1092,plain,
( op(e3,op(e3,e1)) != op(unit,e1)
| spl21_23
| ~ spl21_113 ),
inference(forward_demodulation,[],[f325,f687]) ).
fof(f1094,plain,
( e1 != op(e3,op(e3,e1))
| ~ spl21_19
| spl21_23
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1092,f308]) ).
fof(f1097,plain,
( e1 != op(e3,e2)
| ~ spl21_19
| spl21_23
| ~ spl21_113
| ~ spl21_140 ),
inference(superposition,[],[f1094,f825]) ).
fof(f1098,plain,
( $false
| ~ spl21_19
| spl21_23
| ~ spl21_113
| ~ spl21_137
| ~ spl21_140 ),
inference(forward_subsumption_resolution,[],[f1097,f810]) ).
fof(f1099,plain,
( ~ spl21_19
| spl21_23
| ~ spl21_113
| ~ spl21_137
| ~ spl21_140 ),
inference(avatar_contradiction_clause,[],[f1098]) ).
fof(f1101,plain,
( op(e3,e3) != op(op(e3,e3),unit)
| ~ spl21_14
| spl21_24 ),
inference(forward_demodulation,[],[f329,f288]) ).
fof(f1103,plain,
( unit != op(unit,unit)
| ~ spl21_14
| spl21_24
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1101,f687]) ).
fof(f1105,plain,
( $false
| ~ spl21_14
| ~ spl21_20
| spl21_24
| ~ spl21_113 ),
inference(forward_subsumption_resolution,[],[f1103,f312]) ).
fof(f1106,plain,
( ~ spl21_14
| ~ spl21_20
| spl21_24
| ~ spl21_113 ),
inference(avatar_contradiction_clause,[],[f1105]) ).
fof(f1108,plain,
( op(e1,e3) != op(e3,op(e2,e3))
| spl21_25
| ~ spl21_137 ),
inference(forward_demodulation,[],[f333,f810]) ).
fof(f1110,plain,
( op(e1,e3) != op(e3,e1)
| spl21_25
| ~ spl21_137
| ~ spl21_148 ),
inference(superposition,[],[f1108,f866]) ).
fof(f1111,plain,
( e2 != op(e1,e3)
| spl21_25
| ~ spl21_137
| ~ spl21_140
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1110,f825]) ).
fof(f1112,plain,
( ~ spl21_158
| spl21_25
| ~ spl21_137
| ~ spl21_140
| ~ spl21_148 ),
inference(avatar_split_clause,[],[f1111,f865,f824,f809,f331,f920]) ).
fof(f1114,plain,
( op(op(e3,e2),e2) != op(e3,unit)
| spl21_26
| ~ spl21_114 ),
inference(forward_demodulation,[],[f337,f691]) ).
fof(f1116,plain,
( e3 != op(op(e3,e2),e2)
| ~ spl21_14
| spl21_26
| ~ spl21_114 ),
inference(forward_demodulation,[],[f1114,f288]) ).
fof(f1118,plain,
( e3 != op(e1,e2)
| ~ spl21_14
| spl21_26
| ~ spl21_114
| ~ spl21_137 ),
inference(forward_demodulation,[],[f1116,f810]) ).
fof(f1120,plain,
( ~ spl21_161
| ~ spl21_14
| spl21_26
| ~ spl21_114
| ~ spl21_137 ),
inference(avatar_split_clause,[],[f1118,f809,f690,f335,f287,f935]) ).
fof(f1122,plain,
( op(e1,e1) != op(e3,op(e2,e1))
| spl21_27
| ~ spl21_137 ),
inference(forward_demodulation,[],[f341,f810]) ).
fof(f1124,plain,
( unit != op(e3,op(e2,e1))
| spl21_27
| ~ spl21_115
| ~ spl21_137 ),
inference(forward_demodulation,[],[f1122,f695]) ).
fof(f1127,plain,
( op(e3,e3) != unit
| spl21_27
| ~ spl21_115
| ~ spl21_137
| ~ spl21_150 ),
inference(superposition,[],[f1124,f880]) ).
fof(f1128,plain,
( $false
| spl21_27
| ~ spl21_113
| ~ spl21_115
| ~ spl21_137
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1127,f687]) ).
fof(f1129,plain,
( spl21_27
| ~ spl21_113
| ~ spl21_115
| ~ spl21_137
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1128]) ).
fof(f1131,plain,
( op(e3,e2) != op(op(e3,e2),unit)
| ~ spl21_16
| spl21_28 ),
inference(forward_demodulation,[],[f345,f296]) ).
fof(f1133,plain,
( e1 != op(e1,unit)
| ~ spl21_16
| spl21_28
| ~ spl21_137 ),
inference(forward_demodulation,[],[f1131,f810]) ).
fof(f1135,plain,
( $false
| ~ spl21_16
| ~ spl21_18
| spl21_28
| ~ spl21_137 ),
inference(forward_subsumption_resolution,[],[f1133,f304]) ).
fof(f1136,plain,
( ~ spl21_16
| ~ spl21_18
| spl21_28
| ~ spl21_137 ),
inference(avatar_contradiction_clause,[],[f1135]) ).
fof(f1138,plain,
( op(e2,e3) != op(e3,op(e1,e3))
| spl21_29
| ~ spl21_140 ),
inference(forward_demodulation,[],[f349,f825]) ).
fof(f1140,plain,
( e1 != op(e3,op(e1,e3))
| spl21_29
| ~ spl21_140
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1138,f866]) ).
fof(f1141,plain,
( e1 != op(e3,e2)
| spl21_29
| ~ spl21_140
| ~ spl21_148
| ~ spl21_158 ),
inference(superposition,[],[f1140,f921]) ).
fof(f1142,plain,
( $false
| spl21_29
| ~ spl21_137
| ~ spl21_140
| ~ spl21_148
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1141,f810]) ).
fof(f1143,plain,
( spl21_29
| ~ spl21_137
| ~ spl21_140
| ~ spl21_148
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1142]) ).
fof(f1145,plain,
( op(e2,e2) != op(e3,op(e1,e2))
| spl21_30
| ~ spl21_140 ),
inference(forward_demodulation,[],[f353,f825]) ).
fof(f1147,plain,
( unit != op(e3,op(e1,e2))
| spl21_30
| ~ spl21_114
| ~ spl21_140 ),
inference(forward_demodulation,[],[f1145,f691]) ).
fof(f1149,plain,
( op(e3,e3) != unit
| spl21_30
| ~ spl21_114
| ~ spl21_140
| ~ spl21_161 ),
inference(superposition,[],[f1147,f936]) ).
fof(f1150,plain,
( $false
| spl21_30
| ~ spl21_113
| ~ spl21_114
| ~ spl21_140
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1149,f687]) ).
fof(f1151,plain,
( spl21_30
| ~ spl21_113
| ~ spl21_114
| ~ spl21_140
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1150]) ).
fof(f1153,plain,
( op(op(e3,e1),e1) != op(e3,unit)
| spl21_31
| ~ spl21_115 ),
inference(forward_demodulation,[],[f357,f695]) ).
fof(f1155,plain,
( e3 != op(op(e3,e1),e1)
| ~ spl21_14
| spl21_31
| ~ spl21_115 ),
inference(forward_demodulation,[],[f1153,f288]) ).
fof(f1157,plain,
( e3 != op(e2,e1)
| ~ spl21_14
| spl21_31
| ~ spl21_115
| ~ spl21_140 ),
inference(forward_demodulation,[],[f1155,f825]) ).
fof(f1158,plain,
( $false
| ~ spl21_14
| spl21_31
| ~ spl21_115
| ~ spl21_140
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1157,f880]) ).
fof(f1159,plain,
( ~ spl21_14
| spl21_31
| ~ spl21_115
| ~ spl21_140
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1158]) ).
fof(f1161,plain,
( op(e3,e1) != op(op(e3,e1),unit)
| ~ spl21_18
| spl21_32 ),
inference(forward_demodulation,[],[f361,f304]) ).
fof(f1163,plain,
( e2 != op(e2,unit)
| ~ spl21_18
| spl21_32
| ~ spl21_140 ),
inference(forward_demodulation,[],[f1161,f825]) ).
fof(f1165,plain,
( $false
| ~ spl21_16
| ~ spl21_18
| spl21_32
| ~ spl21_140 ),
inference(forward_subsumption_resolution,[],[f1163,f296]) ).
fof(f1166,plain,
( ~ spl21_16
| ~ spl21_18
| spl21_32
| ~ spl21_140 ),
inference(avatar_contradiction_clause,[],[f1165]) ).
fof(f1168,plain,
( op(e3,e3) != op(op(e3,unit),e3)
| ~ spl21_15
| spl21_33 ),
inference(forward_demodulation,[],[f365,f292]) ).
fof(f1170,plain,
( op(e3,e3) != op(e3,e3)
| ~ spl21_14
| ~ spl21_15
| spl21_33 ),
inference(forward_demodulation,[],[f1168,f288]) ).
fof(f1171,plain,
( $false
| ~ spl21_14
| ~ spl21_15
| spl21_33 ),
inference(trivial_inequality_removal,[],[f1170]) ).
fof(f1172,plain,
( ~ spl21_14
| ~ spl21_15
| spl21_33 ),
inference(avatar_contradiction_clause,[],[f1171]) ).
fof(f1174,plain,
( op(e3,e2) != op(op(e3,unit),e2)
| ~ spl21_17
| spl21_34 ),
inference(forward_demodulation,[],[f369,f300]) ).
fof(f1175,plain,
( op(e3,e2) != op(e3,e2)
| ~ spl21_14
| ~ spl21_17
| spl21_34 ),
inference(forward_demodulation,[],[f1174,f288]) ).
fof(f1176,plain,
( $false
| ~ spl21_14
| ~ spl21_17
| spl21_34 ),
inference(trivial_inequality_removal,[],[f1175]) ).
fof(f1177,plain,
( ~ spl21_14
| ~ spl21_17
| spl21_34 ),
inference(avatar_contradiction_clause,[],[f1176]) ).
fof(f1179,plain,
( op(e3,e1) != op(op(e3,unit),e1)
| ~ spl21_19
| spl21_35 ),
inference(forward_demodulation,[],[f373,f308]) ).
fof(f1180,plain,
( op(e3,e1) != op(e3,e1)
| ~ spl21_14
| ~ spl21_19
| spl21_35 ),
inference(forward_demodulation,[],[f1179,f288]) ).
fof(f1181,plain,
( $false
| ~ spl21_14
| ~ spl21_19
| spl21_35 ),
inference(trivial_inequality_removal,[],[f1180]) ).
fof(f1182,plain,
( ~ spl21_14
| ~ spl21_19
| spl21_35 ),
inference(avatar_contradiction_clause,[],[f1181]) ).
fof(f1184,plain,
( op(e3,unit) != op(op(e3,unit),unit)
| ~ spl21_20
| spl21_36 ),
inference(forward_demodulation,[],[f377,f312]) ).
fof(f1185,plain,
( e3 != op(e3,unit)
| ~ spl21_14
| ~ spl21_20
| spl21_36 ),
inference(forward_demodulation,[],[f1184,f288]) ).
fof(f1186,plain,
( $false
| ~ spl21_14
| ~ spl21_20
| spl21_36 ),
inference(forward_subsumption_resolution,[],[f1185,f288]) ).
fof(f1187,plain,
( ~ spl21_14
| ~ spl21_20
| spl21_36 ),
inference(avatar_contradiction_clause,[],[f1186]) ).
fof(f1189,plain,
( op(op(e2,e3),e3) != op(e2,unit)
| spl21_37
| ~ spl21_113 ),
inference(forward_demodulation,[],[f381,f687]) ).
fof(f1191,plain,
( e2 != op(op(e2,e3),e3)
| ~ spl21_16
| spl21_37
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1189,f296]) ).
fof(f1192,plain,
( e2 != op(e1,e3)
| ~ spl21_16
| spl21_37
| ~ spl21_113
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1191,f866]) ).
fof(f1193,plain,
( $false
| ~ spl21_16
| spl21_37
| ~ spl21_113
| ~ spl21_148
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1192,f921]) ).
fof(f1194,plain,
( ~ spl21_16
| spl21_37
| ~ spl21_113
| ~ spl21_148
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1193]) ).
fof(f1196,plain,
( op(e2,e1) != op(op(e2,e3),e2)
| spl21_38
| ~ spl21_137 ),
inference(forward_demodulation,[],[f385,f810]) ).
fof(f1198,plain,
( op(e1,e2) != op(e2,e1)
| spl21_38
| ~ spl21_137
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1196,f866]) ).
fof(f1200,plain,
( e3 != op(e1,e2)
| spl21_38
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1198,f880]) ).
fof(f1201,plain,
( $false
| spl21_38
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1200,f936]) ).
fof(f1202,plain,
( spl21_38
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1201]) ).
fof(f1204,plain,
( op(e2,e2) != op(op(e2,e3),e1)
| spl21_39
| ~ spl21_140 ),
inference(forward_demodulation,[],[f389,f825]) ).
fof(f1206,plain,
( op(e1,e1) != op(e2,e2)
| spl21_39
| ~ spl21_140
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1204,f866]) ).
fof(f1208,plain,
( op(e1,e1) != unit
| spl21_39
| ~ spl21_114
| ~ spl21_140
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1206,f691]) ).
fof(f1209,plain,
( $false
| spl21_39
| ~ spl21_114
| ~ spl21_115
| ~ spl21_140
| ~ spl21_148 ),
inference(forward_subsumption_resolution,[],[f1208,f695]) ).
fof(f1210,plain,
( spl21_39
| ~ spl21_114
| ~ spl21_115
| ~ spl21_140
| ~ spl21_148 ),
inference(avatar_contradiction_clause,[],[f1209]) ).
fof(f1212,plain,
( op(e2,e3) != op(op(e2,e3),unit)
| ~ spl21_14
| spl21_40 ),
inference(forward_demodulation,[],[f393,f288]) ).
fof(f1214,plain,
( e1 != op(e1,unit)
| ~ spl21_14
| spl21_40
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1212,f866]) ).
fof(f1216,plain,
( $false
| ~ spl21_14
| ~ spl21_18
| spl21_40
| ~ spl21_148 ),
inference(forward_subsumption_resolution,[],[f1214,f304]) ).
fof(f1217,plain,
( ~ spl21_14
| ~ spl21_18
| spl21_40
| ~ spl21_148 ),
inference(avatar_contradiction_clause,[],[f1216]) ).
fof(f1219,plain,
( op(e2,e1) != op(op(e2,e2),e3)
| spl21_41
| ~ spl21_148 ),
inference(forward_demodulation,[],[f397,f866]) ).
fof(f1221,plain,
( op(e2,e1) != op(unit,e3)
| spl21_41
| ~ spl21_114
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1219,f691]) ).
fof(f1222,plain,
( e3 != op(e2,e1)
| ~ spl21_15
| spl21_41
| ~ spl21_114
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1221,f292]) ).
fof(f1223,plain,
( $false
| ~ spl21_15
| spl21_41
| ~ spl21_114
| ~ spl21_148
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1222,f880]) ).
fof(f1224,plain,
( ~ spl21_15
| spl21_41
| ~ spl21_114
| ~ spl21_148
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1223]) ).
fof(f1226,plain,
( op(unit,e2) != op(e2,unit)
| spl21_42
| ~ spl21_114 ),
inference(forward_demodulation,[],[f401,f691]) ).
fof(f1228,plain,
( e2 != op(unit,e2)
| ~ spl21_16
| spl21_42
| ~ spl21_114 ),
inference(forward_demodulation,[],[f1226,f296]) ).
fof(f1230,plain,
( $false
| ~ spl21_16
| ~ spl21_17
| spl21_42
| ~ spl21_114 ),
inference(forward_subsumption_resolution,[],[f1228,f300]) ).
fof(f1231,plain,
( ~ spl21_16
| ~ spl21_17
| spl21_42
| ~ spl21_114 ),
inference(avatar_contradiction_clause,[],[f1230]) ).
fof(f1233,plain,
( op(e2,e3) != op(op(e2,e2),e1)
| spl21_43
| ~ spl21_150 ),
inference(forward_demodulation,[],[f405,f880]) ).
fof(f1235,plain,
( op(e2,e3) != op(unit,e1)
| spl21_43
| ~ spl21_114
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1233,f691]) ).
fof(f1236,plain,
( e1 != op(e2,e3)
| ~ spl21_19
| spl21_43
| ~ spl21_114
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1235,f308]) ).
fof(f1237,plain,
( $false
| ~ spl21_19
| spl21_43
| ~ spl21_114
| ~ spl21_148
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1236,f866]) ).
fof(f1238,plain,
( ~ spl21_19
| spl21_43
| ~ spl21_114
| ~ spl21_148
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1237]) ).
fof(f1240,plain,
( op(e2,e2) != op(op(e2,e2),unit)
| ~ spl21_16
| spl21_44 ),
inference(forward_demodulation,[],[f409,f296]) ).
fof(f1242,plain,
( unit != op(unit,unit)
| ~ spl21_16
| spl21_44
| ~ spl21_114 ),
inference(forward_demodulation,[],[f1240,f691]) ).
fof(f1244,plain,
( $false
| ~ spl21_16
| ~ spl21_20
| spl21_44
| ~ spl21_114 ),
inference(forward_subsumption_resolution,[],[f1242,f312]) ).
fof(f1245,plain,
( ~ spl21_16
| ~ spl21_20
| spl21_44
| ~ spl21_114 ),
inference(avatar_contradiction_clause,[],[f1244]) ).
fof(f1247,plain,
( op(e2,e2) != op(op(e2,e1),e3)
| spl21_45
| ~ spl21_158 ),
inference(forward_demodulation,[],[f413,f921]) ).
fof(f1249,plain,
( op(e2,e2) != op(e3,e3)
| spl21_45
| ~ spl21_150
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1247,f880]) ).
fof(f1250,plain,
( op(e2,e2) != unit
| spl21_45
| ~ spl21_113
| ~ spl21_150
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1249,f687]) ).
fof(f1251,plain,
( $false
| spl21_45
| ~ spl21_113
| ~ spl21_114
| ~ spl21_150
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1250,f691]) ).
fof(f1252,plain,
( spl21_45
| ~ spl21_113
| ~ spl21_114
| ~ spl21_150
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1251]) ).
fof(f1254,plain,
( op(e2,e3) != op(op(e2,e1),e2)
| spl21_46
| ~ spl21_161 ),
inference(forward_demodulation,[],[f417,f936]) ).
fof(f1256,plain,
( op(e2,e3) != op(e3,e2)
| spl21_46
| ~ spl21_150
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1254,f880]) ).
fof(f1258,plain,
( e1 != op(e2,e3)
| spl21_46
| ~ spl21_137
| ~ spl21_150
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1256,f810]) ).
fof(f1259,plain,
( $false
| spl21_46
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1258,f866]) ).
fof(f1260,plain,
( spl21_46
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1259]) ).
fof(f1262,plain,
( op(op(e2,e1),e1) != op(e2,unit)
| spl21_47
| ~ spl21_115 ),
inference(forward_demodulation,[],[f421,f695]) ).
fof(f1264,plain,
( e2 != op(op(e2,e1),e1)
| ~ spl21_16
| spl21_47
| ~ spl21_115 ),
inference(forward_demodulation,[],[f1262,f296]) ).
fof(f1266,plain,
( e2 != op(e3,e1)
| ~ spl21_16
| spl21_47
| ~ spl21_115
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1264,f880]) ).
fof(f1267,plain,
( $false
| ~ spl21_16
| spl21_47
| ~ spl21_115
| ~ spl21_140
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1266,f825]) ).
fof(f1268,plain,
( ~ spl21_16
| spl21_47
| ~ spl21_115
| ~ spl21_140
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1267]) ).
fof(f1270,plain,
( op(e2,e1) != op(op(e2,e1),unit)
| ~ spl21_18
| spl21_48 ),
inference(forward_demodulation,[],[f425,f304]) ).
fof(f1272,plain,
( e3 != op(e3,unit)
| ~ spl21_18
| spl21_48
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1270,f880]) ).
fof(f1274,plain,
( $false
| ~ spl21_14
| ~ spl21_18
| spl21_48
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1272,f288]) ).
fof(f1275,plain,
( ~ spl21_14
| ~ spl21_18
| spl21_48
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1274]) ).
fof(f1277,plain,
( op(e2,e3) != op(op(e2,unit),e3)
| ~ spl21_15
| spl21_49 ),
inference(forward_demodulation,[],[f429,f292]) ).
fof(f1279,plain,
( op(e2,e3) != op(e2,e3)
| ~ spl21_15
| ~ spl21_16
| spl21_49 ),
inference(forward_demodulation,[],[f1277,f296]) ).
fof(f1280,plain,
( $false
| ~ spl21_15
| ~ spl21_16
| spl21_49 ),
inference(trivial_inequality_removal,[],[f1279]) ).
fof(f1281,plain,
( ~ spl21_15
| ~ spl21_16
| spl21_49 ),
inference(avatar_contradiction_clause,[],[f1280]) ).
fof(f1283,plain,
( op(e2,e2) != op(op(e2,unit),e2)
| ~ spl21_17
| spl21_50 ),
inference(forward_demodulation,[],[f433,f300]) ).
fof(f1284,plain,
( op(e2,e2) != op(e2,e2)
| ~ spl21_16
| ~ spl21_17
| spl21_50 ),
inference(forward_demodulation,[],[f1283,f296]) ).
fof(f1285,plain,
( $false
| ~ spl21_16
| ~ spl21_17
| spl21_50 ),
inference(trivial_inequality_removal,[],[f1284]) ).
fof(f1286,plain,
( ~ spl21_16
| ~ spl21_17
| spl21_50 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
fof(f1288,plain,
( op(e2,e1) != op(op(e2,unit),e1)
| ~ spl21_19
| spl21_51 ),
inference(forward_demodulation,[],[f437,f308]) ).
fof(f1289,plain,
( op(e2,e1) != op(e2,e1)
| ~ spl21_16
| ~ spl21_19
| spl21_51 ),
inference(forward_demodulation,[],[f1288,f296]) ).
fof(f1290,plain,
( $false
| ~ spl21_16
| ~ spl21_19
| spl21_51 ),
inference(trivial_inequality_removal,[],[f1289]) ).
fof(f1291,plain,
( ~ spl21_16
| ~ spl21_19
| spl21_51 ),
inference(avatar_contradiction_clause,[],[f1290]) ).
fof(f1293,plain,
( op(e2,unit) != op(op(e2,unit),unit)
| ~ spl21_20
| spl21_52 ),
inference(forward_demodulation,[],[f441,f312]) ).
fof(f1294,plain,
( e2 != op(e2,unit)
| ~ spl21_16
| ~ spl21_20
| spl21_52 ),
inference(forward_demodulation,[],[f1293,f296]) ).
fof(f1295,plain,
( $false
| ~ spl21_16
| ~ spl21_20
| spl21_52 ),
inference(forward_subsumption_resolution,[],[f1294,f296]) ).
fof(f1296,plain,
( ~ spl21_16
| ~ spl21_20
| spl21_52 ),
inference(avatar_contradiction_clause,[],[f1295]) ).
fof(f1298,plain,
( op(op(e1,e3),e3) != op(e1,unit)
| spl21_53
| ~ spl21_113 ),
inference(forward_demodulation,[],[f445,f687]) ).
fof(f1300,plain,
( e1 != op(op(e1,e3),e3)
| ~ spl21_18
| spl21_53
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1298,f304]) ).
fof(f1301,plain,
( e1 != op(e2,e3)
| ~ spl21_18
| spl21_53
| ~ spl21_113
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1300,f921]) ).
fof(f1302,plain,
( $false
| ~ spl21_18
| spl21_53
| ~ spl21_113
| ~ spl21_148
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1301,f866]) ).
fof(f1303,plain,
( ~ spl21_18
| spl21_53
| ~ spl21_113
| ~ spl21_148
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1302]) ).
fof(f1305,plain,
( op(e1,e1) != op(op(e1,e3),e2)
| spl21_54
| ~ spl21_137 ),
inference(forward_demodulation,[],[f449,f810]) ).
fof(f1307,plain,
( op(e1,e1) != op(e2,e2)
| spl21_54
| ~ spl21_137
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1305,f921]) ).
fof(f1309,plain,
( op(e1,e1) != unit
| spl21_54
| ~ spl21_114
| ~ spl21_137
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1307,f691]) ).
fof(f1310,plain,
( $false
| spl21_54
| ~ spl21_114
| ~ spl21_115
| ~ spl21_137
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1309,f695]) ).
fof(f1311,plain,
( spl21_54
| ~ spl21_114
| ~ spl21_115
| ~ spl21_137
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1310]) ).
fof(f1313,plain,
( op(e1,e2) != op(op(e1,e3),e1)
| spl21_55
| ~ spl21_140 ),
inference(forward_demodulation,[],[f453,f825]) ).
fof(f1315,plain,
( op(e1,e2) != op(e2,e1)
| spl21_55
| ~ spl21_140
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1313,f921]) ).
fof(f1317,plain,
( e3 != op(e1,e2)
| spl21_55
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1315,f880]) ).
fof(f1318,plain,
( $false
| spl21_55
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1317,f936]) ).
fof(f1319,plain,
( spl21_55
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1318]) ).
fof(f1321,plain,
( op(e1,e3) != op(op(e1,e3),unit)
| ~ spl21_14
| spl21_56 ),
inference(forward_demodulation,[],[f457,f288]) ).
fof(f1323,plain,
( e2 != op(e2,unit)
| ~ spl21_14
| spl21_56
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1321,f921]) ).
fof(f1325,plain,
( $false
| ~ spl21_14
| ~ spl21_16
| spl21_56
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1323,f296]) ).
fof(f1326,plain,
( ~ spl21_14
| ~ spl21_16
| spl21_56
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1325]) ).
fof(f1328,plain,
( op(e1,e1) != op(op(e1,e2),e3)
| spl21_57
| ~ spl21_148 ),
inference(forward_demodulation,[],[f461,f866]) ).
fof(f1330,plain,
( op(e1,e1) != op(e3,e3)
| spl21_57
| ~ spl21_148
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1328,f936]) ).
fof(f1331,plain,
( op(e1,e1) != unit
| spl21_57
| ~ spl21_113
| ~ spl21_148
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1330,f687]) ).
fof(f1332,plain,
( $false
| spl21_57
| ~ spl21_113
| ~ spl21_115
| ~ spl21_148
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1331,f695]) ).
fof(f1333,plain,
( spl21_57
| ~ spl21_113
| ~ spl21_115
| ~ spl21_148
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1332]) ).
fof(f1335,plain,
( op(op(e1,e2),e2) != op(e1,unit)
| spl21_58
| ~ spl21_114 ),
inference(forward_demodulation,[],[f465,f691]) ).
fof(f1337,plain,
( e1 != op(op(e1,e2),e2)
| ~ spl21_18
| spl21_58
| ~ spl21_114 ),
inference(forward_demodulation,[],[f1335,f304]) ).
fof(f1339,plain,
( e1 != op(e3,e2)
| ~ spl21_18
| spl21_58
| ~ spl21_114
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1337,f936]) ).
fof(f1340,plain,
( $false
| ~ spl21_18
| spl21_58
| ~ spl21_114
| ~ spl21_137
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1339,f810]) ).
fof(f1341,plain,
( ~ spl21_18
| spl21_58
| ~ spl21_114
| ~ spl21_137
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1340]) ).
fof(f1343,plain,
( op(e1,e3) != op(op(e1,e2),e1)
| spl21_59
| ~ spl21_150 ),
inference(forward_demodulation,[],[f469,f880]) ).
fof(f1345,plain,
( op(e1,e3) != op(e3,e1)
| spl21_59
| ~ spl21_150
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1343,f936]) ).
fof(f1347,plain,
( e2 != op(e1,e3)
| spl21_59
| ~ spl21_140
| ~ spl21_150
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1345,f825]) ).
fof(f1348,plain,
( $false
| spl21_59
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1347,f921]) ).
fof(f1349,plain,
( spl21_59
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1348]) ).
fof(f1351,plain,
( op(e1,e2) != op(op(e1,e2),unit)
| ~ spl21_16
| spl21_60 ),
inference(forward_demodulation,[],[f473,f296]) ).
fof(f1353,plain,
( e3 != op(e3,unit)
| ~ spl21_16
| spl21_60
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1351,f936]) ).
fof(f1355,plain,
( $false
| ~ spl21_14
| ~ spl21_16
| spl21_60
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1353,f288]) ).
fof(f1356,plain,
( ~ spl21_14
| ~ spl21_16
| spl21_60
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1358,plain,
( op(e1,e2) != op(op(e1,e1),e3)
| spl21_61
| ~ spl21_158 ),
inference(forward_demodulation,[],[f477,f921]) ).
fof(f1360,plain,
( op(e1,e2) != op(unit,e3)
| spl21_61
| ~ spl21_115
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1358,f695]) ).
fof(f1361,plain,
( e3 != op(e1,e2)
| ~ spl21_15
| spl21_61
| ~ spl21_115
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1360,f292]) ).
fof(f1362,plain,
( $false
| ~ spl21_15
| spl21_61
| ~ spl21_115
| ~ spl21_158
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1361,f936]) ).
fof(f1363,plain,
( ~ spl21_15
| spl21_61
| ~ spl21_115
| ~ spl21_158
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1362]) ).
fof(f1365,plain,
( op(e1,e3) != op(op(e1,e1),e2)
| spl21_62
| ~ spl21_161 ),
inference(forward_demodulation,[],[f481,f936]) ).
fof(f1367,plain,
( op(e1,e3) != op(unit,e2)
| spl21_62
| ~ spl21_115
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1365,f695]) ).
fof(f1369,plain,
( e2 != op(e1,e3)
| ~ spl21_17
| spl21_62
| ~ spl21_115
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1367,f300]) ).
fof(f1370,plain,
( $false
| ~ spl21_17
| spl21_62
| ~ spl21_115
| ~ spl21_158
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1369,f921]) ).
fof(f1371,plain,
( ~ spl21_17
| spl21_62
| ~ spl21_115
| ~ spl21_158
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1370]) ).
fof(f1373,plain,
( op(unit,e1) != op(e1,unit)
| spl21_63
| ~ spl21_115 ),
inference(forward_demodulation,[],[f485,f695]) ).
fof(f1375,plain,
( e1 != op(unit,e1)
| ~ spl21_18
| spl21_63
| ~ spl21_115 ),
inference(forward_demodulation,[],[f1373,f304]) ).
fof(f1377,plain,
( $false
| ~ spl21_18
| ~ spl21_19
| spl21_63
| ~ spl21_115 ),
inference(forward_subsumption_resolution,[],[f1375,f308]) ).
fof(f1378,plain,
( ~ spl21_18
| ~ spl21_19
| spl21_63
| ~ spl21_115 ),
inference(avatar_contradiction_clause,[],[f1377]) ).
fof(f1380,plain,
( op(e1,e1) != op(op(e1,e1),unit)
| ~ spl21_18
| spl21_64 ),
inference(forward_demodulation,[],[f489,f304]) ).
fof(f1382,plain,
( unit != op(unit,unit)
| ~ spl21_18
| spl21_64
| ~ spl21_115 ),
inference(forward_demodulation,[],[f1380,f695]) ).
fof(f1383,plain,
( $false
| ~ spl21_18
| ~ spl21_20
| spl21_64
| ~ spl21_115 ),
inference(forward_subsumption_resolution,[],[f1382,f312]) ).
fof(f1384,plain,
( ~ spl21_18
| ~ spl21_20
| spl21_64
| ~ spl21_115 ),
inference(avatar_contradiction_clause,[],[f1383]) ).
fof(f1386,plain,
( op(e1,e3) != op(op(e1,unit),e3)
| ~ spl21_15
| spl21_65 ),
inference(forward_demodulation,[],[f493,f292]) ).
fof(f1388,plain,
( op(e1,e3) != op(e1,e3)
| ~ spl21_15
| ~ spl21_18
| spl21_65 ),
inference(forward_demodulation,[],[f1386,f304]) ).
fof(f1389,plain,
( $false
| ~ spl21_15
| ~ spl21_18
| spl21_65 ),
inference(trivial_inequality_removal,[],[f1388]) ).
fof(f1390,plain,
( ~ spl21_15
| ~ spl21_18
| spl21_65 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1392,plain,
( op(e1,e2) != op(op(e1,unit),e2)
| ~ spl21_17
| spl21_66 ),
inference(forward_demodulation,[],[f497,f300]) ).
fof(f1393,plain,
( op(e1,e2) != op(e1,e2)
| ~ spl21_17
| ~ spl21_18
| spl21_66 ),
inference(forward_demodulation,[],[f1392,f304]) ).
fof(f1394,plain,
( $false
| ~ spl21_17
| ~ spl21_18
| spl21_66 ),
inference(trivial_inequality_removal,[],[f1393]) ).
fof(f1395,plain,
( ~ spl21_17
| ~ spl21_18
| spl21_66 ),
inference(avatar_contradiction_clause,[],[f1394]) ).
fof(f1397,plain,
( op(e1,e1) != op(op(e1,unit),e1)
| ~ spl21_19
| spl21_67 ),
inference(forward_demodulation,[],[f501,f308]) ).
fof(f1398,plain,
( op(e1,e1) != op(e1,e1)
| ~ spl21_18
| ~ spl21_19
| spl21_67 ),
inference(forward_demodulation,[],[f1397,f304]) ).
fof(f1399,plain,
( $false
| ~ spl21_18
| ~ spl21_19
| spl21_67 ),
inference(trivial_inequality_removal,[],[f1398]) ).
fof(f1400,plain,
( ~ spl21_18
| ~ spl21_19
| spl21_67 ),
inference(avatar_contradiction_clause,[],[f1399]) ).
fof(f1402,plain,
( op(e1,unit) != op(op(e1,unit),unit)
| ~ spl21_20
| spl21_68 ),
inference(forward_demodulation,[],[f505,f312]) ).
fof(f1403,plain,
( e1 != op(e1,unit)
| ~ spl21_18
| ~ spl21_20
| spl21_68 ),
inference(forward_demodulation,[],[f1402,f304]) ).
fof(f1404,plain,
( $false
| ~ spl21_18
| ~ spl21_20
| spl21_68 ),
inference(forward_subsumption_resolution,[],[f1403,f304]) ).
fof(f1405,plain,
( ~ spl21_18
| ~ spl21_20
| spl21_68 ),
inference(avatar_contradiction_clause,[],[f1404]) ).
fof(f1407,plain,
( op(unit,unit) != op(op(unit,e3),e3)
| spl21_69
| ~ spl21_113 ),
inference(forward_demodulation,[],[f509,f687]) ).
fof(f1409,plain,
( op(e3,e3) != op(unit,unit)
| ~ spl21_15
| spl21_69
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1407,f292]) ).
fof(f1410,plain,
( op(e3,e3) != unit
| ~ spl21_15
| ~ spl21_20
| spl21_69
| ~ spl21_113 ),
inference(forward_demodulation,[],[f1409,f312]) ).
fof(f1411,plain,
( $false
| ~ spl21_15
| ~ spl21_20
| spl21_69
| ~ spl21_113 ),
inference(forward_subsumption_resolution,[],[f1410,f687]) ).
fof(f1412,plain,
( ~ spl21_15
| ~ spl21_20
| spl21_69
| ~ spl21_113 ),
inference(avatar_contradiction_clause,[],[f1411]) ).
fof(f1414,plain,
( op(unit,e1) != op(op(unit,e3),e2)
| spl21_70
| ~ spl21_137 ),
inference(forward_demodulation,[],[f513,f810]) ).
fof(f1416,plain,
( op(e3,e2) != op(unit,e1)
| ~ spl21_15
| spl21_70
| ~ spl21_137 ),
inference(forward_demodulation,[],[f1414,f292]) ).
fof(f1418,plain,
( e1 != op(e3,e2)
| ~ spl21_15
| ~ spl21_19
| spl21_70
| ~ spl21_137 ),
inference(forward_demodulation,[],[f1416,f308]) ).
fof(f1419,plain,
( $false
| ~ spl21_15
| ~ spl21_19
| spl21_70
| ~ spl21_137 ),
inference(forward_subsumption_resolution,[],[f1418,f810]) ).
fof(f1420,plain,
( ~ spl21_15
| ~ spl21_19
| spl21_70
| ~ spl21_137 ),
inference(avatar_contradiction_clause,[],[f1419]) ).
fof(f1422,plain,
( op(unit,e2) != op(op(unit,e3),e1)
| spl21_71
| ~ spl21_140 ),
inference(forward_demodulation,[],[f517,f825]) ).
fof(f1424,plain,
( op(e3,e1) != op(unit,e2)
| ~ spl21_15
| spl21_71
| ~ spl21_140 ),
inference(forward_demodulation,[],[f1422,f292]) ).
fof(f1426,plain,
( e2 != op(e3,e1)
| ~ spl21_15
| ~ spl21_17
| spl21_71
| ~ spl21_140 ),
inference(forward_demodulation,[],[f1424,f300]) ).
fof(f1427,plain,
( $false
| ~ spl21_15
| ~ spl21_17
| spl21_71
| ~ spl21_140 ),
inference(forward_subsumption_resolution,[],[f1426,f825]) ).
fof(f1428,plain,
( ~ spl21_15
| ~ spl21_17
| spl21_71
| ~ spl21_140 ),
inference(avatar_contradiction_clause,[],[f1427]) ).
fof(f1430,plain,
( op(unit,e3) != op(op(unit,e3),unit)
| ~ spl21_14
| spl21_72 ),
inference(forward_demodulation,[],[f521,f288]) ).
fof(f1432,plain,
( e3 != op(e3,unit)
| ~ spl21_14
| ~ spl21_15
| spl21_72 ),
inference(forward_demodulation,[],[f1430,f292]) ).
fof(f1434,plain,
( $false
| ~ spl21_14
| ~ spl21_15
| spl21_72 ),
inference(forward_subsumption_resolution,[],[f1432,f288]) ).
fof(f1435,plain,
( ~ spl21_14
| ~ spl21_15
| spl21_72 ),
inference(avatar_contradiction_clause,[],[f1434]) ).
fof(f1437,plain,
( op(unit,e1) != op(op(unit,e2),e3)
| spl21_73
| ~ spl21_148 ),
inference(forward_demodulation,[],[f525,f866]) ).
fof(f1439,plain,
( op(e2,e3) != op(unit,e1)
| ~ spl21_17
| spl21_73
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1437,f300]) ).
fof(f1440,plain,
( e1 != op(e2,e3)
| ~ spl21_17
| ~ spl21_19
| spl21_73
| ~ spl21_148 ),
inference(forward_demodulation,[],[f1439,f308]) ).
fof(f1441,plain,
( $false
| ~ spl21_17
| ~ spl21_19
| spl21_73
| ~ spl21_148 ),
inference(forward_subsumption_resolution,[],[f1440,f866]) ).
fof(f1442,plain,
( ~ spl21_17
| ~ spl21_19
| spl21_73
| ~ spl21_148 ),
inference(avatar_contradiction_clause,[],[f1441]) ).
fof(f1444,plain,
( op(unit,unit) != op(op(unit,e2),e2)
| spl21_74
| ~ spl21_114 ),
inference(forward_demodulation,[],[f529,f691]) ).
fof(f1446,plain,
( op(e2,e2) != op(unit,unit)
| ~ spl21_17
| spl21_74
| ~ spl21_114 ),
inference(forward_demodulation,[],[f1444,f300]) ).
fof(f1448,plain,
( op(e2,e2) != unit
| ~ spl21_17
| ~ spl21_20
| spl21_74
| ~ spl21_114 ),
inference(forward_demodulation,[],[f1446,f312]) ).
fof(f1449,plain,
( $false
| ~ spl21_17
| ~ spl21_20
| spl21_74
| ~ spl21_114 ),
inference(forward_subsumption_resolution,[],[f1448,f691]) ).
fof(f1450,plain,
( ~ spl21_17
| ~ spl21_20
| spl21_74
| ~ spl21_114 ),
inference(avatar_contradiction_clause,[],[f1449]) ).
fof(f1452,plain,
( op(unit,e3) != op(op(unit,e2),e1)
| spl21_75
| ~ spl21_150 ),
inference(forward_demodulation,[],[f533,f880]) ).
fof(f1454,plain,
( op(e2,e1) != op(unit,e3)
| ~ spl21_17
| spl21_75
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1452,f300]) ).
fof(f1456,plain,
( e3 != op(e2,e1)
| ~ spl21_15
| ~ spl21_17
| spl21_75
| ~ spl21_150 ),
inference(forward_demodulation,[],[f1454,f292]) ).
fof(f1457,plain,
( $false
| ~ spl21_15
| ~ spl21_17
| spl21_75
| ~ spl21_150 ),
inference(forward_subsumption_resolution,[],[f1456,f880]) ).
fof(f1458,plain,
( ~ spl21_15
| ~ spl21_17
| spl21_75
| ~ spl21_150 ),
inference(avatar_contradiction_clause,[],[f1457]) ).
fof(f1460,plain,
( op(unit,e2) != op(op(unit,e2),unit)
| ~ spl21_16
| spl21_76 ),
inference(forward_demodulation,[],[f537,f296]) ).
fof(f1462,plain,
( e2 != op(e2,unit)
| ~ spl21_16
| ~ spl21_17
| spl21_76 ),
inference(forward_demodulation,[],[f1460,f300]) ).
fof(f1464,plain,
( $false
| ~ spl21_16
| ~ spl21_17
| spl21_76 ),
inference(forward_subsumption_resolution,[],[f1462,f296]) ).
fof(f1465,plain,
( ~ spl21_16
| ~ spl21_17
| spl21_76 ),
inference(avatar_contradiction_clause,[],[f1464]) ).
fof(f1467,plain,
( op(unit,e2) != op(op(unit,e1),e3)
| spl21_77
| ~ spl21_158 ),
inference(forward_demodulation,[],[f541,f921]) ).
fof(f1469,plain,
( op(e1,e3) != op(unit,e2)
| ~ spl21_19
| spl21_77
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1467,f308]) ).
fof(f1470,plain,
( e2 != op(e1,e3)
| ~ spl21_17
| ~ spl21_19
| spl21_77
| ~ spl21_158 ),
inference(forward_demodulation,[],[f1469,f300]) ).
fof(f1471,plain,
( $false
| ~ spl21_17
| ~ spl21_19
| spl21_77
| ~ spl21_158 ),
inference(forward_subsumption_resolution,[],[f1470,f921]) ).
fof(f1472,plain,
( ~ spl21_17
| ~ spl21_19
| spl21_77
| ~ spl21_158 ),
inference(avatar_contradiction_clause,[],[f1471]) ).
fof(f1474,plain,
( op(unit,e3) != op(op(unit,e1),e2)
| spl21_78
| ~ spl21_161 ),
inference(forward_demodulation,[],[f545,f936]) ).
fof(f1476,plain,
( op(e1,e2) != op(unit,e3)
| ~ spl21_19
| spl21_78
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1474,f308]) ).
fof(f1478,plain,
( e3 != op(e1,e2)
| ~ spl21_15
| ~ spl21_19
| spl21_78
| ~ spl21_161 ),
inference(forward_demodulation,[],[f1476,f292]) ).
fof(f1479,plain,
( $false
| ~ spl21_15
| ~ spl21_19
| spl21_78
| ~ spl21_161 ),
inference(forward_subsumption_resolution,[],[f1478,f936]) ).
fof(f1480,plain,
( ~ spl21_15
| ~ spl21_19
| spl21_78
| ~ spl21_161 ),
inference(avatar_contradiction_clause,[],[f1479]) ).
fof(f1482,plain,
( op(unit,unit) != op(op(unit,e1),e1)
| spl21_79
| ~ spl21_115 ),
inference(forward_demodulation,[],[f549,f695]) ).
fof(f1484,plain,
( op(e1,e1) != op(unit,unit)
| ~ spl21_19
| spl21_79
| ~ spl21_115 ),
inference(forward_demodulation,[],[f1482,f308]) ).
fof(f1486,plain,
( op(e1,e1) != unit
| ~ spl21_19
| ~ spl21_20
| spl21_79
| ~ spl21_115 ),
inference(forward_demodulation,[],[f1484,f312]) ).
fof(f1487,plain,
( $false
| ~ spl21_19
| ~ spl21_20
| spl21_79
| ~ spl21_115 ),
inference(forward_subsumption_resolution,[],[f1486,f695]) ).
fof(f1488,plain,
( ~ spl21_19
| ~ spl21_20
| spl21_79
| ~ spl21_115 ),
inference(avatar_contradiction_clause,[],[f1487]) ).
fof(f1490,plain,
( op(unit,e1) != op(op(unit,e1),unit)
| ~ spl21_18
| spl21_80 ),
inference(forward_demodulation,[],[f553,f304]) ).
fof(f1492,plain,
( e1 != op(e1,unit)
| ~ spl21_18
| ~ spl21_19
| spl21_80 ),
inference(forward_demodulation,[],[f1490,f308]) ).
fof(f1494,plain,
( $false
| ~ spl21_18
| ~ spl21_19
| spl21_80 ),
inference(forward_subsumption_resolution,[],[f1492,f304]) ).
fof(f1495,plain,
( ~ spl21_18
| ~ spl21_19
| spl21_80 ),
inference(avatar_contradiction_clause,[],[f1494]) ).
fof(f1497,plain,
( op(unit,e3) != op(op(unit,unit),e3)
| ~ spl21_15
| spl21_81 ),
inference(forward_demodulation,[],[f557,f292]) ).
fof(f1499,plain,
( op(unit,e3) != op(unit,e3)
| ~ spl21_15
| ~ spl21_20
| spl21_81 ),
inference(forward_demodulation,[],[f1497,f312]) ).
fof(f1500,plain,
( $false
| ~ spl21_15
| ~ spl21_20
| spl21_81 ),
inference(trivial_inequality_removal,[],[f1499]) ).
fof(f1501,plain,
( ~ spl21_15
| ~ spl21_20
| spl21_81 ),
inference(avatar_contradiction_clause,[],[f1500]) ).
fof(f1503,plain,
( op(unit,e2) != op(op(unit,unit),e2)
| ~ spl21_17
| spl21_82 ),
inference(forward_demodulation,[],[f561,f300]) ).
fof(f1504,plain,
( op(unit,e2) != op(unit,e2)
| ~ spl21_17
| ~ spl21_20
| spl21_82 ),
inference(forward_demodulation,[],[f1503,f312]) ).
fof(f1505,plain,
( $false
| ~ spl21_17
| ~ spl21_20
| spl21_82 ),
inference(trivial_inequality_removal,[],[f1504]) ).
fof(f1506,plain,
( ~ spl21_17
| ~ spl21_20
| spl21_82 ),
inference(avatar_contradiction_clause,[],[f1505]) ).
fof(f1508,plain,
( op(unit,e1) != op(op(unit,unit),e1)
| ~ spl21_19
| spl21_83 ),
inference(forward_demodulation,[],[f565,f308]) ).
fof(f1509,plain,
( op(unit,e1) != op(unit,e1)
| ~ spl21_19
| ~ spl21_20
| spl21_83 ),
inference(forward_demodulation,[],[f1508,f312]) ).
fof(f1510,plain,
( $false
| ~ spl21_19
| ~ spl21_20
| spl21_83 ),
inference(trivial_inequality_removal,[],[f1509]) ).
fof(f1511,plain,
( ~ spl21_19
| ~ spl21_20
| spl21_83 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1513,plain,
( op(unit,unit) != op(unit,unit)
| ~ spl21_20
| spl21_84 ),
inference(forward_demodulation,[],[f569,f312]) ).
fof(f1514,plain,
( $false
| ~ spl21_20
| spl21_84 ),
inference(trivial_inequality_removal,[],[f1513]) ).
fof(f1515,plain,
( ~ spl21_20
| spl21_84 ),
inference(avatar_contradiction_clause,[],[f1514]) ).
cnf(s4,plain,
( spl21_1
| spl21_2
| spl21_3
| spl21_4
| ~ spl21_5
| ~ spl21_6
| ~ spl21_7
| ~ spl21_8
| ~ spl21_9
| ~ spl21_10
| ~ spl21_11
| ~ spl21_12
| spl21_13
| ~ spl21_14
| ~ spl21_15
| ~ spl21_16
| ~ spl21_17
| ~ spl21_18
| ~ spl21_19
| ~ spl21_20
| ~ spl21_21
| ~ spl21_22
| ~ spl21_23
| ~ spl21_24
| ~ spl21_25
| ~ spl21_26
| ~ spl21_27
| ~ spl21_28
| ~ spl21_29
| ~ spl21_30
| ~ spl21_31
| ~ spl21_32
| ~ spl21_33
| ~ spl21_34
| ~ spl21_35
| ~ spl21_36
| ~ spl21_37
| ~ spl21_38
| ~ spl21_39
| ~ spl21_40
| ~ spl21_41
| ~ spl21_42
| ~ spl21_43
| ~ spl21_44
| ~ spl21_45
| ~ spl21_46
| ~ spl21_47
| ~ spl21_48
| ~ spl21_49
| ~ spl21_50
| ~ spl21_51
| ~ spl21_52
| ~ spl21_53
| ~ spl21_54
| ~ spl21_55
| ~ spl21_56
| ~ spl21_57
| ~ spl21_58
| ~ spl21_59
| ~ spl21_60
| ~ spl21_61
| ~ spl21_62
| ~ spl21_63
| ~ spl21_64
| ~ spl21_65
| ~ spl21_66
| ~ spl21_67
| ~ spl21_68
| ~ spl21_69
| ~ spl21_70
| ~ spl21_71
| ~ spl21_72
| ~ spl21_73
| ~ spl21_74
| ~ spl21_75
| ~ spl21_76
| ~ spl21_77
| ~ spl21_78
| ~ spl21_79
| ~ spl21_80
| ~ spl21_81
| ~ spl21_82
| ~ spl21_83
| ~ spl21_84
| spl21_85
| spl21_86
| spl21_87
| spl21_88
| spl21_89
| spl21_90
| spl21_91
| spl21_92
| spl21_93
| spl21_94
| spl21_95
| spl21_96
| spl21_97
| spl21_98
| spl21_99
| spl21_100
| ~ spl21_113
| ~ spl21_114
| ~ spl21_115 ),
inference(sat_conversion,[],[f697]) ).
cnf(s5,plain,
( ~ spl21_1
| ~ spl21_116 ),
inference(sat_conversion,[],[f702]) ).
cnf(s10,plain,
( ~ spl21_2
| ~ spl21_121 ),
inference(sat_conversion,[],[f727]) ).
cnf(s15,plain,
( ~ spl21_3
| ~ spl21_126 ),
inference(sat_conversion,[],[f752]) ).
cnf(s20,plain,
( ~ spl21_4
| ~ spl21_131 ),
inference(sat_conversion,[],[f777]) ).
cnf(s24,plain,
~ spl21_13,
inference(sat_conversion,[],[f793]) ).
cnf(s28,plain,
( ~ spl21_85
| ~ spl21_113 ),
inference(sat_conversion,[],[f797]) ).
cnf(s31,plain,
( ~ spl21_86
| ~ spl21_137 ),
inference(sat_conversion,[],[f812]) ).
cnf(s34,plain,
( ~ spl21_87
| ~ spl21_140 ),
inference(sat_conversion,[],[f827]) ).
cnf(s37,plain,
( ~ spl21_14
| ~ spl21_88 ),
inference(sat_conversion,[],[f838]) ).
cnf(s43,plain,
( ~ spl21_89
| ~ spl21_148 ),
inference(sat_conversion,[],[f868]) ).
cnf(s48,plain,
( ~ spl21_90
| ~ spl21_114 ),
inference(sat_conversion,[],[f877]) ).
cnf(s49,plain,
( ~ spl21_91
| ~ spl21_150 ),
inference(sat_conversion,[],[f882]) ).
cnf(s54,plain,
( ~ spl21_16
| ~ spl21_92 ),
inference(sat_conversion,[],[f903]) ).
cnf(s58,plain,
( ~ spl21_93
| ~ spl21_158 ),
inference(sat_conversion,[],[f923]) ).
cnf(s61,plain,
( ~ spl21_94
| ~ spl21_161 ),
inference(sat_conversion,[],[f938]) ).
cnf(s68,plain,
( ~ spl21_95
| ~ spl21_115 ),
inference(sat_conversion,[],[f957]) ).
cnf(s71,plain,
( ~ spl21_18
| ~ spl21_96 ),
inference(sat_conversion,[],[f968]) ).
cnf(s73,plain,
( ~ spl21_15
| ~ spl21_97 ),
inference(sat_conversion,[],[f974]) ).
cnf(s78,plain,
( ~ spl21_17
| ~ spl21_98 ),
inference(sat_conversion,[],[f995]) ).
cnf(s83,plain,
( ~ spl21_19
| ~ spl21_99 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s88,plain,
( ~ spl21_20
| ~ spl21_100 ),
inference(sat_conversion,[],[f1025]) ).
cnf(s89,plain,
spl21_116,
inference(sat_conversion,[],[f1026]) ).
cnf(s90,plain,
spl21_121,
inference(sat_conversion,[],[f1027]) ).
cnf(s91,plain,
spl21_126,
inference(sat_conversion,[],[f1028]) ).
cnf(s92,plain,
spl21_131,
inference(sat_conversion,[],[f1029]) ).
cnf(s93,plain,
spl21_113,
inference(sat_conversion,[],[f1030]) ).
cnf(s94,plain,
spl21_137,
inference(sat_conversion,[],[f1031]) ).
cnf(s95,plain,
spl21_140,
inference(sat_conversion,[],[f1032]) ).
cnf(s96,plain,
spl21_14,
inference(sat_conversion,[],[f1033]) ).
cnf(s97,plain,
spl21_148,
inference(sat_conversion,[],[f1034]) ).
cnf(s98,plain,
spl21_114,
inference(sat_conversion,[],[f1035]) ).
cnf(s99,plain,
spl21_150,
inference(sat_conversion,[],[f1036]) ).
cnf(s100,plain,
spl21_16,
inference(sat_conversion,[],[f1037]) ).
cnf(s101,plain,
spl21_158,
inference(sat_conversion,[],[f1038]) ).
cnf(s102,plain,
spl21_161,
inference(sat_conversion,[],[f1039]) ).
cnf(s103,plain,
spl21_115,
inference(sat_conversion,[],[f1040]) ).
cnf(s104,plain,
spl21_18,
inference(sat_conversion,[],[f1041]) ).
cnf(s105,plain,
spl21_15,
inference(sat_conversion,[],[f1042]) ).
cnf(s106,plain,
spl21_17,
inference(sat_conversion,[],[f1043]) ).
cnf(s107,plain,
spl21_19,
inference(sat_conversion,[],[f1044]) ).
cnf(s108,plain,
spl21_20,
inference(sat_conversion,[],[f1045]) ).
cnf(s112,plain,
( spl21_5
| ~ spl21_113
| ~ spl21_116 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s113,plain,
( spl21_6
| ~ spl21_113
| ~ spl21_116 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s114,plain,
( spl21_7
| ~ spl21_114
| ~ spl21_121 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s115,plain,
( spl21_8
| ~ spl21_114
| ~ spl21_121 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s116,plain,
( spl21_9
| ~ spl21_115
| ~ spl21_126 ),
inference(sat_conversion,[],[f1067]) ).
cnf(s117,plain,
( spl21_10
| ~ spl21_115
| ~ spl21_126 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s118,plain,
( spl21_11
| ~ spl21_20
| ~ spl21_131 ),
inference(sat_conversion,[],[f1075]) ).
cnf(s119,plain,
( spl21_12
| ~ spl21_20
| ~ spl21_131 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s120,plain,
( ~ spl21_14
| ~ spl21_15
| spl21_21
| ~ spl21_113 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s121,plain,
( ~ spl21_17
| spl21_22
| ~ spl21_113
| ~ spl21_137
| ~ spl21_140 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s123,plain,
( ~ spl21_19
| spl21_23
| ~ spl21_113
| ~ spl21_137
| ~ spl21_140 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s124,plain,
( ~ spl21_14
| ~ spl21_20
| spl21_24
| ~ spl21_113 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s125,plain,
( spl21_25
| ~ spl21_137
| ~ spl21_140
| ~ spl21_148
| ~ spl21_158 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s127,plain,
( ~ spl21_14
| spl21_26
| ~ spl21_114
| ~ spl21_137
| ~ spl21_161 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s129,plain,
( spl21_27
| ~ spl21_113
| ~ spl21_115
| ~ spl21_137
| ~ spl21_150 ),
inference(sat_conversion,[],[f1129]) ).
cnf(s130,plain,
( ~ spl21_16
| ~ spl21_18
| spl21_28
| ~ spl21_137 ),
inference(sat_conversion,[],[f1136]) ).
cnf(s131,plain,
( spl21_29
| ~ spl21_137
| ~ spl21_140
| ~ spl21_148
| ~ spl21_158 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s132,plain,
( spl21_30
| ~ spl21_113
| ~ spl21_114
| ~ spl21_140
| ~ spl21_161 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s133,plain,
( ~ spl21_14
| spl21_31
| ~ spl21_115
| ~ spl21_140
| ~ spl21_150 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s134,plain,
( ~ spl21_16
| ~ spl21_18
| spl21_32
| ~ spl21_140 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s135,plain,
( ~ spl21_14
| ~ spl21_15
| spl21_33 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s136,plain,
( ~ spl21_14
| ~ spl21_17
| spl21_34 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s137,plain,
( ~ spl21_14
| ~ spl21_19
| spl21_35 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s138,plain,
( ~ spl21_14
| ~ spl21_20
| spl21_36 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s139,plain,
( ~ spl21_16
| spl21_37
| ~ spl21_113
| ~ spl21_148
| ~ spl21_158 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s140,plain,
( spl21_38
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150
| ~ spl21_161 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s141,plain,
( spl21_39
| ~ spl21_114
| ~ spl21_115
| ~ spl21_140
| ~ spl21_148 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s142,plain,
( ~ spl21_14
| ~ spl21_18
| spl21_40
| ~ spl21_148 ),
inference(sat_conversion,[],[f1217]) ).
cnf(s143,plain,
( ~ spl21_15
| spl21_41
| ~ spl21_114
| ~ spl21_148
| ~ spl21_150 ),
inference(sat_conversion,[],[f1224]) ).
cnf(s144,plain,
( ~ spl21_16
| ~ spl21_17
| spl21_42
| ~ spl21_114 ),
inference(sat_conversion,[],[f1231]) ).
cnf(s145,plain,
( ~ spl21_19
| spl21_43
| ~ spl21_114
| ~ spl21_148
| ~ spl21_150 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s146,plain,
( ~ spl21_16
| ~ spl21_20
| spl21_44
| ~ spl21_114 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s147,plain,
( spl21_45
| ~ spl21_113
| ~ spl21_114
| ~ spl21_150
| ~ spl21_158 ),
inference(sat_conversion,[],[f1252]) ).
cnf(s148,plain,
( spl21_46
| ~ spl21_137
| ~ spl21_148
| ~ spl21_150
| ~ spl21_161 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s149,plain,
( ~ spl21_16
| spl21_47
| ~ spl21_115
| ~ spl21_140
| ~ spl21_150 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s150,plain,
( ~ spl21_14
| ~ spl21_18
| spl21_48
| ~ spl21_150 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s151,plain,
( ~ spl21_15
| ~ spl21_16
| spl21_49 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s152,plain,
( ~ spl21_16
| ~ spl21_17
| spl21_50 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s153,plain,
( ~ spl21_16
| ~ spl21_19
| spl21_51 ),
inference(sat_conversion,[],[f1291]) ).
cnf(s154,plain,
( ~ spl21_16
| ~ spl21_20
| spl21_52 ),
inference(sat_conversion,[],[f1296]) ).
cnf(s155,plain,
( ~ spl21_18
| spl21_53
| ~ spl21_113
| ~ spl21_148
| ~ spl21_158 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s156,plain,
( spl21_54
| ~ spl21_114
| ~ spl21_115
| ~ spl21_137
| ~ spl21_158 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s157,plain,
( spl21_55
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158
| ~ spl21_161 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s158,plain,
( ~ spl21_14
| ~ spl21_16
| spl21_56
| ~ spl21_158 ),
inference(sat_conversion,[],[f1326]) ).
cnf(s159,plain,
( spl21_57
| ~ spl21_113
| ~ spl21_115
| ~ spl21_148
| ~ spl21_161 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s160,plain,
( ~ spl21_18
| spl21_58
| ~ spl21_114
| ~ spl21_137
| ~ spl21_161 ),
inference(sat_conversion,[],[f1341]) ).
cnf(s161,plain,
( spl21_59
| ~ spl21_140
| ~ spl21_150
| ~ spl21_158
| ~ spl21_161 ),
inference(sat_conversion,[],[f1349]) ).
cnf(s162,plain,
( ~ spl21_14
| ~ spl21_16
| spl21_60
| ~ spl21_161 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s163,plain,
( ~ spl21_15
| spl21_61
| ~ spl21_115
| ~ spl21_158
| ~ spl21_161 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s164,plain,
( ~ spl21_17
| spl21_62
| ~ spl21_115
| ~ spl21_158
| ~ spl21_161 ),
inference(sat_conversion,[],[f1371]) ).
cnf(s165,plain,
( ~ spl21_18
| ~ spl21_19
| spl21_63
| ~ spl21_115 ),
inference(sat_conversion,[],[f1378]) ).
cnf(s166,plain,
( ~ spl21_18
| ~ spl21_20
| spl21_64
| ~ spl21_115 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s167,plain,
( ~ spl21_15
| ~ spl21_18
| spl21_65 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s168,plain,
( ~ spl21_17
| ~ spl21_18
| spl21_66 ),
inference(sat_conversion,[],[f1395]) ).
cnf(s169,plain,
( ~ spl21_18
| ~ spl21_19
| spl21_67 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s170,plain,
( ~ spl21_18
| ~ spl21_20
| spl21_68 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s171,plain,
( ~ spl21_15
| ~ spl21_20
| spl21_69
| ~ spl21_113 ),
inference(sat_conversion,[],[f1412]) ).
cnf(s172,plain,
( ~ spl21_15
| ~ spl21_19
| spl21_70
| ~ spl21_137 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s173,plain,
( ~ spl21_15
| ~ spl21_17
| spl21_71
| ~ spl21_140 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s174,plain,
( ~ spl21_14
| ~ spl21_15
| spl21_72 ),
inference(sat_conversion,[],[f1435]) ).
cnf(s175,plain,
( ~ spl21_17
| ~ spl21_19
| spl21_73
| ~ spl21_148 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s176,plain,
( ~ spl21_17
| ~ spl21_20
| spl21_74
| ~ spl21_114 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s177,plain,
( ~ spl21_15
| ~ spl21_17
| spl21_75
| ~ spl21_150 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s178,plain,
( ~ spl21_16
| ~ spl21_17
| spl21_76 ),
inference(sat_conversion,[],[f1465]) ).
cnf(s179,plain,
( ~ spl21_17
| ~ spl21_19
| spl21_77
| ~ spl21_158 ),
inference(sat_conversion,[],[f1472]) ).
cnf(s180,plain,
( ~ spl21_15
| ~ spl21_19
| spl21_78
| ~ spl21_161 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s181,plain,
( ~ spl21_19
| ~ spl21_20
| spl21_79
| ~ spl21_115 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s182,plain,
( ~ spl21_18
| ~ spl21_19
| spl21_80 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s183,plain,
( ~ spl21_15
| ~ spl21_20
| spl21_81 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s184,plain,
( ~ spl21_17
| ~ spl21_20
| spl21_82 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s185,plain,
( ~ spl21_19
| ~ spl21_20
| spl21_83 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s186,plain,
( ~ spl21_20
| spl21_84 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s187,plain,
spl21_84,
inference(rat,[],[s186,s108]) ).
cnf(s188,plain,
spl21_83,
inference(rat,[],[s185,s108,s107]) ).
cnf(s189,plain,
spl21_82,
inference(rat,[],[s184,s108,s106]) ).
cnf(s190,plain,
spl21_81,
inference(rat,[],[s183,s108,s105]) ).
cnf(s191,plain,
spl21_80,
inference(rat,[],[s182,s107,s104]) ).
cnf(s192,plain,
spl21_68,
inference(rat,[],[s170,s108,s104]) ).
cnf(s193,plain,
spl21_67,
inference(rat,[],[s169,s107,s104]) ).
cnf(s194,plain,
spl21_66,
inference(rat,[],[s168,s106,s104]) ).
cnf(s195,plain,
spl21_65,
inference(rat,[],[s167,s105,s104]) ).
cnf(s196,plain,
spl21_79,
inference(rat,[],[s181,s107,s108,s103]) ).
cnf(s197,plain,
spl21_64,
inference(rat,[],[s166,s104,s108,s103]) ).
cnf(s198,plain,
spl21_63,
inference(rat,[],[s165,s104,s107,s103]) ).
cnf(s199,plain,
spl21_78,
inference(rat,[],[s180,s105,s107,s102]) ).
cnf(s200,plain,
spl21_77,
inference(rat,[],[s179,s106,s107,s101]) ).
cnf(s201,plain,
spl21_62,
inference(rat,[],[s164,s102,s103,s106,s101]) ).
cnf(s202,plain,
spl21_61,
inference(rat,[],[s163,s102,s103,s105,s101]) ).
cnf(s203,plain,
spl21_76,
inference(rat,[],[s178,s106,s100]) ).
cnf(s204,plain,
spl21_52,
inference(rat,[],[s154,s108,s100]) ).
cnf(s205,plain,
spl21_51,
inference(rat,[],[s153,s107,s100]) ).
cnf(s206,plain,
spl21_50,
inference(rat,[],[s152,s106,s100]) ).
cnf(s207,plain,
spl21_49,
inference(rat,[],[s151,s105,s100]) ).
cnf(s208,plain,
spl21_75,
inference(rat,[],[s177,s105,s106,s99]) ).
cnf(s209,plain,
spl21_74,
inference(rat,[],[s176,s106,s108,s98]) ).
cnf(s210,plain,
spl21_44,
inference(rat,[],[s146,s100,s108,s98]) ).
cnf(s211,plain,
spl21_42,
inference(rat,[],[s144,s100,s106,s98]) ).
cnf(s212,plain,
spl21_73,
inference(rat,[],[s175,s106,s107,s97]) ).
cnf(s213,plain,
spl21_43,
inference(rat,[],[s145,s99,s98,s107,s97]) ).
cnf(s214,plain,
spl21_41,
inference(rat,[],[s143,s99,s98,s105,s97]) ).
cnf(s215,plain,
spl21_72,
inference(rat,[],[s174,s105,s96]) ).
cnf(s216,plain,
spl21_60,
inference(rat,[],[s162,s102,s100,s96]) ).
cnf(s217,plain,
spl21_56,
inference(rat,[],[s158,s101,s100,s96]) ).
cnf(s218,plain,
spl21_48,
inference(rat,[],[s150,s99,s104,s96]) ).
cnf(s219,plain,
spl21_40,
inference(rat,[],[s142,s97,s104,s96]) ).
cnf(s220,plain,
spl21_36,
inference(rat,[],[s138,s108,s96]) ).
cnf(s221,plain,
spl21_35,
inference(rat,[],[s137,s107,s96]) ).
cnf(s222,plain,
spl21_34,
inference(rat,[],[s136,s106,s96]) ).
cnf(s223,plain,
spl21_33,
inference(rat,[],[s135,s105,s96]) ).
cnf(s224,plain,
spl21_59,
inference(rat,[],[s161,s102,s101,s99,s95]) ).
cnf(s225,plain,
spl21_55,
inference(rat,[],[s157,s102,s101,s99,s95]) ).
cnf(s226,plain,
spl21_71,
inference(rat,[],[s173,s105,s106,s95]) ).
cnf(s227,plain,
spl21_47,
inference(rat,[],[s149,s99,s100,s103,s95]) ).
cnf(s228,plain,
spl21_32,
inference(rat,[],[s134,s100,s104,s95]) ).
cnf(s229,plain,
spl21_39,
inference(rat,[],[s141,s97,s98,s103,s95]) ).
cnf(s230,plain,
spl21_31,
inference(rat,[],[s133,s99,s96,s103,s95]) ).
cnf(s231,plain,
spl21_46,
inference(rat,[],[s148,s102,s99,s97,s94]) ).
cnf(s232,plain,
spl21_38,
inference(rat,[],[s140,s102,s99,s97,s94]) ).
cnf(s233,plain,
spl21_29,
inference(rat,[],[s131,s101,s97,s95,s94]) ).
cnf(s234,plain,
spl21_25,
inference(rat,[],[s125,s101,s97,s95,s94]) ).
cnf(s235,plain,
spl21_70,
inference(rat,[],[s172,s105,s107,s94]) ).
cnf(s236,plain,
spl21_28,
inference(rat,[],[s130,s100,s104,s94]) ).
cnf(s237,plain,
spl21_54,
inference(rat,[],[s156,s101,s98,s103,s94]) ).
cnf(s238,plain,
spl21_58,
inference(rat,[],[s160,s102,s98,s104,s94]) ).
cnf(s239,plain,
spl21_26,
inference(rat,[],[s127,s102,s96,s98,s94]) ).
cnf(s240,plain,
spl21_57,
inference(rat,[],[s159,s102,s97,s103,s93]) ).
cnf(s241,plain,
spl21_45,
inference(rat,[],[s147,s101,s99,s98,s93]) ).
cnf(s242,plain,
spl21_30,
inference(rat,[],[s132,s102,s95,s98,s93]) ).
cnf(s243,plain,
spl21_27,
inference(rat,[],[s129,s99,s94,s103,s93]) ).
cnf(s244,plain,
spl21_23,
inference(rat,[],[s123,s95,s94,s107,s93]) ).
cnf(s245,plain,
spl21_22,
inference(rat,[],[s121,s95,s94,s106,s93]) ).
cnf(s246,plain,
spl21_69,
inference(rat,[],[s171,s105,s108,s93]) ).
cnf(s247,plain,
spl21_53,
inference(rat,[],[s155,s101,s97,s104,s93]) ).
cnf(s248,plain,
spl21_37,
inference(rat,[],[s139,s101,s97,s100,s93]) ).
cnf(s249,plain,
spl21_24,
inference(rat,[],[s124,s96,s108,s93]) ).
cnf(s250,plain,
spl21_21,
inference(rat,[],[s120,s96,s105,s93]) ).
cnf(s251,plain,
spl21_12,
inference(rat,[],[s119,s108,s92]) ).
cnf(s252,plain,
spl21_11,
inference(rat,[],[s118,s108,s92]) ).
cnf(s253,plain,
spl21_10,
inference(rat,[],[s117,s103,s91]) ).
cnf(s254,plain,
spl21_9,
inference(rat,[],[s116,s103,s91]) ).
cnf(s255,plain,
spl21_8,
inference(rat,[],[s115,s98,s90]) ).
cnf(s256,plain,
spl21_7,
inference(rat,[],[s114,s98,s90]) ).
cnf(s257,plain,
spl21_6,
inference(rat,[],[s113,s93,s89]) ).
cnf(s258,plain,
spl21_5,
inference(rat,[],[s112,s93,s89]) ).
cnf(s259,plain,
~ spl21_100,
inference(rat,[],[s88,s108]) ).
cnf(s260,plain,
~ spl21_99,
inference(rat,[],[s83,s107]) ).
cnf(s261,plain,
~ spl21_98,
inference(rat,[],[s78,s106]) ).
cnf(s262,plain,
~ spl21_97,
inference(rat,[],[s73,s105]) ).
cnf(s263,plain,
~ spl21_96,
inference(rat,[],[s71,s104]) ).
cnf(s264,plain,
~ spl21_95,
inference(rat,[],[s68,s103]) ).
cnf(s265,plain,
~ spl21_94,
inference(rat,[],[s61,s102]) ).
cnf(s266,plain,
~ spl21_93,
inference(rat,[],[s58,s101]) ).
cnf(s267,plain,
~ spl21_92,
inference(rat,[],[s54,s100]) ).
cnf(s268,plain,
~ spl21_91,
inference(rat,[],[s49,s99]) ).
cnf(s269,plain,
~ spl21_90,
inference(rat,[],[s48,s98]) ).
cnf(s270,plain,
~ spl21_89,
inference(rat,[],[s43,s97]) ).
cnf(s271,plain,
~ spl21_88,
inference(rat,[],[s37,s96]) ).
cnf(s272,plain,
~ spl21_87,
inference(rat,[],[s34,s95]) ).
cnf(s273,plain,
~ spl21_86,
inference(rat,[],[s31,s94]) ).
cnf(s274,plain,
~ spl21_85,
inference(rat,[],[s28,s93]) ).
cnf(s275,plain,
~ spl21_4,
inference(rat,[],[s20,s92]) ).
cnf(s276,plain,
~ spl21_3,
inference(rat,[],[s15,s91]) ).
cnf(s277,plain,
~ spl21_2,
inference(rat,[],[s10,s90]) ).
cnf(s278,plain,
~ spl21_1,
inference(rat,[],[s5,s89]) ).
cnf(s279,plain,
$false,
inference(rat,[],[s4,s103,s98,s93,s259,s260,s261,s262,s263,s264,s265,s266,s267,s268,s269,s270,s271,s272,s273,s274,s187,s188,s189,s190,s191,s196,s199,s200,s203,s208,s209,s212,s215,s226,s235,s246,s192,s193,s194,s195,s197,s198,s201,s202,s216,s224,s238,s240,s217,s225,s237,s247,s204,s205,s206,s207,s218,s227,s231,s241,s210,s213,s211,s214,s219,s229,s232,s248,s220,s221,s222,s223,s228,s230,s242,s233,s236,s243,s239,s234,s249,s244,s245,s250,s108,s107,s104,s106,s100,s105,s96,s24,s251,s252,s253,s254,s255,s256,s257,s258,s275,s276,s277,s278]) ).
fof(f1516,plain,
$false,
inference(avatar_sat_refutation,[],[s279]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG021+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:18:45 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.27 % (3364724)Will run a generic schedule for satisfiability detection.
% 0.22/0.27 % (3364732)dis+10_1_sil=32000:sp=arity:random_seed=946733722:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.22/0.27 % (3364730)% WARNING: option uhcvi not known.
% 0.22/0.27 % (3364729)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1592009125_2999 on theBenchmark for (2999ds/0Mi)
% 0.22/0.27 % (3364731)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1821872371:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.22/0.27 % (3364730)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=189137540:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.22/0.27 % (3364733)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2132360921:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.22/0.27 % (3364735)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2140978365:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.22/0.27 % (3364734)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2966569183:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.22/0.27 % (3364732) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3364724-3364732"...
% 0.22/0.27 % (3364732)...printing done.
% 0.22/0.27 % (3364732)Refutation found. Thanks to Tanya!
% 0.22/0.27 % SZS status Theorem for theBenchmark
% 0.22/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/0.28 % (3364732)------------------------------
% 0.22/0.28 % (3364732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.28 % (3364732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.28 % (3364732)CaDiCaL version: 2.1.3
% 0.22/0.28 % (3364732)Termination reason: Refutation
% 0.22/0.28 % (3364732)Time elapsed: 0.016 s
% 0.22/0.28 % (3364732)Peak memory usage: 13 MB
% 0.22/0.28 % (3364732)Instructions burned: 64 (million)
% 0.22/0.28 % (3364724)Success in time 0.043 s
% 0.22/0.28 % Vampire exiting
%------------------------------------------------------------------------------