%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:21:13 AM UTC 2026
% Result : Theorem 0.19s 0.33s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 142
% Syntax : Number of formulae : 939 ( 157 unt; 136 def)
% Number of atoms : 2989 (1344 equ)
% Maximal formula atoms : 250 ( 3 avg)
% Number of connectives : 3401 (1351 ~;1520 |; 394 &)
% ( 136 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 161 ( 159 usr; 160 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
( 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
& op(unit,e4) = e4
& op(e4,unit) = e4
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3
| unit = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0
| op(e0,e4) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0
| op(e4,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1
| op(e0,e4) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1
| op(e4,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2
| op(e0,e4) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2
| op(e4,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3
| op(e0,e4) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3
| op(e4,e0) = e3 )
& ( op(e0,e0) = e4
| op(e0,e1) = e4
| op(e0,e2) = e4
| op(e0,e3) = e4
| op(e0,e4) = e4 )
& ( op(e0,e0) = e4
| op(e1,e0) = e4
| op(e2,e0) = e4
| op(e3,e0) = e4
| op(e4,e0) = e4 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0
| op(e1,e4) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0
| op(e4,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1
| op(e1,e4) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1
| op(e4,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2
| op(e1,e4) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2
| op(e4,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3
| op(e1,e4) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3
| op(e4,e1) = e3 )
& ( op(e1,e0) = e4
| op(e1,e1) = e4
| op(e1,e2) = e4
| op(e1,e3) = e4
| op(e1,e4) = e4 )
& ( op(e0,e1) = e4
| op(e1,e1) = e4
| op(e2,e1) = e4
| op(e3,e1) = e4
| op(e4,e1) = e4 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0
| op(e2,e4) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0
| op(e4,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1
| op(e2,e4) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1
| op(e4,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2
| op(e2,e4) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2
| op(e4,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3
| op(e2,e4) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3
| op(e4,e2) = e3 )
& ( op(e2,e0) = e4
| op(e2,e1) = e4
| op(e2,e2) = e4
| op(e2,e3) = e4
| op(e2,e4) = e4 )
& ( op(e0,e2) = e4
| op(e1,e2) = e4
| op(e2,e2) = e4
| op(e3,e2) = e4
| op(e4,e2) = e4 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0
| op(e3,e4) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0
| op(e4,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1
| op(e3,e4) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1
| op(e4,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2
| op(e3,e4) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2
| op(e4,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3
| op(e3,e4) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3
| op(e4,e3) = e3 )
& ( op(e3,e0) = e4
| op(e3,e1) = e4
| op(e3,e2) = e4
| op(e3,e3) = e4
| op(e3,e4) = e4 )
& ( op(e0,e3) = e4
| op(e1,e3) = e4
| op(e2,e3) = e4
| op(e3,e3) = e4
| op(e4,e3) = e4 )
& ( op(e4,e0) = e0
| op(e4,e1) = e0
| op(e4,e2) = e0
| op(e4,e3) = e0
| op(e4,e4) = e0 )
& ( op(e0,e4) = e0
| op(e1,e4) = e0
| op(e2,e4) = e0
| op(e3,e4) = e0
| op(e4,e4) = e0 )
& ( op(e4,e0) = e1
| op(e4,e1) = e1
| op(e4,e2) = e1
| op(e4,e3) = e1
| op(e4,e4) = e1 )
& ( op(e0,e4) = e1
| op(e1,e4) = e1
| op(e2,e4) = e1
| op(e3,e4) = e1
| op(e4,e4) = e1 )
& ( op(e4,e0) = e2
| op(e4,e1) = e2
| op(e4,e2) = e2
| op(e4,e3) = e2
| op(e4,e4) = e2 )
& ( op(e0,e4) = e2
| op(e1,e4) = e2
| op(e2,e4) = e2
| op(e3,e4) = e2
| op(e4,e4) = e2 )
& ( op(e4,e0) = e3
| op(e4,e1) = e3
| op(e4,e2) = e3
| op(e4,e3) = e3
| op(e4,e4) = e3 )
& ( op(e0,e4) = e3
| op(e1,e4) = e3
| op(e2,e4) = e3
| op(e3,e4) = e3
| op(e4,e4) = e3 )
& ( op(e4,e0) = e4
| op(e4,e1) = e4
| op(e4,e2) = e4
| op(e4,e3) = e4
| op(e4,e4) = e4 )
& ( op(e0,e4) = e4
| op(e1,e4) = e4
| op(e2,e4) = e4
| op(e3,e4) = e4
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e4,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e4,e0)
& op(e2,e0) != op(e3,e0)
& op(e2,e0) != op(e4,e0)
& op(e3,e0) != op(e4,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e4,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e4,e1)
& op(e2,e1) != op(e3,e1)
& op(e2,e1) != op(e4,e1)
& op(e3,e1) != op(e4,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e4,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e4,e2)
& op(e2,e2) != op(e3,e2)
& op(e2,e2) != op(e4,e2)
& op(e3,e2) != op(e4,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e4,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e4,e3)
& op(e2,e3) != op(e3,e3)
& op(e2,e3) != op(e4,e3)
& op(e3,e3) != op(e4,e3)
& op(e0,e4) != op(e1,e4)
& op(e0,e4) != op(e2,e4)
& op(e0,e4) != op(e3,e4)
& op(e0,e4) != op(e4,e4)
& op(e1,e4) != op(e2,e4)
& op(e1,e4) != op(e3,e4)
& op(e1,e4) != op(e4,e4)
& op(e2,e4) != op(e3,e4)
& op(e2,e4) != op(e4,e4)
& op(e3,e4) != op(e4,e4)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e4)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e4)
& op(e0,e2) != op(e0,e3)
& op(e0,e2) != op(e0,e4)
& op(e0,e3) != op(e0,e4)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e4)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e4)
& op(e1,e2) != op(e1,e3)
& op(e1,e2) != op(e1,e4)
& op(e1,e3) != op(e1,e4)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e4)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e4)
& op(e2,e2) != op(e2,e3)
& op(e2,e2) != op(e2,e4)
& op(e2,e3) != op(e2,e4)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e4)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e4)
& op(e3,e2) != op(e3,e3)
& op(e3,e2) != op(e3,e4)
& op(e3,e3) != op(e3,e4)
& op(e4,e0) != op(e4,e1)
& op(e4,e0) != op(e4,e2)
& op(e4,e0) != op(e4,e3)
& op(e4,e0) != op(e4,e4)
& op(e4,e1) != op(e4,e2)
& op(e4,e1) != op(e4,e3)
& op(e4,e1) != op(e4,e4)
& op(e4,e2) != op(e4,e3)
& op(e4,e2) != op(e4,e4)
& op(e4,e3) != op(e4,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e0 != e4
& e1 != e2
& e1 != e3
& e1 != e4
& e2 != e3
& e2 != e4
& e3 != e4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( e0 = op(op(e4,e2),op(e4,e2))
& e1 = op(e4,e2)
& e3 = op(e2,e4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f8,negated_conjecture,
~ ~ ( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f9,plain,
( ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e0,e0) != e4
| op(e0,e4) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e1,e1) != e4
| op(e1,e4) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e2,e2) != e4
| op(e2,e4) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( op(e3,e3) != e4
| op(e3,e4) = e3 )
& ( op(e4,e4) != e0
| op(e4,e0) = e4 )
& ( op(e4,e4) != e1
| op(e4,e1) = e4 )
& ( op(e4,e4) != e2
| op(e4,e2) = e4 )
& ( op(e4,e4) != e3
| op(e4,e3) = e4 )
& ( op(e4,e4) != e4
| op(e4,e4) = e4 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f35,plain,
( e4 = unit
| e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f36,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f37,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f38,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f39,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f40,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f41,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f42,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f43,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f48,plain,
( e1 = op(e0,e4)
| e1 = op(e0,e3)
| e1 = op(e0,e2)
| e1 = op(e0,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f3]) ).
fof(f60,plain,
( e2 = op(e1,e4)
| e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f61,plain,
( e2 = op(e4,e1)
| e2 = op(e3,e1)
| e2 = op(e2,e1)
| e2 = op(e1,e1)
| e2 = op(e0,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f62,plain,
( e3 = op(e1,e4)
| e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f63,plain,
( e3 = op(e4,e1)
| e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f64,plain,
( e4 = op(e1,e4)
| e4 = op(e1,e3)
| e4 = op(e1,e2)
| e4 = op(e1,e1)
| e4 = op(e1,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f68,plain,
( e1 = op(e2,e4)
| e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f73,plain,
( e3 = op(e4,e2)
| e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f74,plain,
( e4 = op(e2,e4)
| e4 = op(e2,e3)
| e4 = op(e2,e2)
| e4 = op(e2,e1)
| e4 = op(e2,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f75,plain,
( e4 = op(e4,e2)
| e4 = op(e3,e2)
| e4 = op(e2,e2)
| e4 = op(e1,e2)
| e4 = op(e0,e2) ),
inference(cnf_transformation,[],[f3]) ).
fof(f76,plain,
( e0 = op(e3,e4)
| e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f78,plain,
( e1 = op(e3,e4)
| e1 = op(e3,e3)
| e1 = op(e3,e2)
| e1 = op(e3,e1)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f79,plain,
( e1 = op(e4,e3)
| e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f80,plain,
( e2 = op(e3,e4)
| e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f81,plain,
( e2 = op(e4,e3)
| e2 = op(e3,e3)
| e2 = op(e2,e3)
| e2 = op(e1,e3)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f85,plain,
( e4 = op(e4,e3)
| e4 = op(e3,e3)
| e4 = op(e2,e3)
| e4 = op(e1,e3)
| e4 = op(e0,e3) ),
inference(cnf_transformation,[],[f3]) ).
fof(f87,plain,
( e0 = op(e4,e4)
| e0 = op(e3,e4)
| e0 = op(e2,e4)
| e0 = op(e1,e4)
| e0 = op(e0,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f89,plain,
( e1 = op(e4,e4)
| e1 = op(e3,e4)
| e1 = op(e2,e4)
| e1 = op(e1,e4)
| e1 = op(e0,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f90,plain,
( e2 = op(e4,e4)
| e2 = op(e4,e3)
| e2 = op(e4,e2)
| e2 = op(e4,e1)
| e2 = op(e4,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f91,plain,
( e2 = op(e4,e4)
| e2 = op(e3,e4)
| e2 = op(e2,e4)
| e2 = op(e1,e4)
| e2 = op(e0,e4) ),
inference(cnf_transformation,[],[f3]) ).
fof(f92,plain,
( e3 = op(e4,e4)
| e3 = op(e4,e3)
| e3 = op(e4,e2)
| e3 = op(e4,e1)
| e3 = op(e4,e0) ),
inference(cnf_transformation,[],[f3]) ).
fof(f97,plain,
op(e4,e2) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f98,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f116,plain,
op(e2,e3) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f117,plain,
op(e2,e2) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f119,plain,
op(e2,e1) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f147,plain,
op(e2,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f148,plain,
op(e2,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
op(e1,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f166,plain,
op(e3,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f167,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f169,plain,
op(e1,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f172,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f196,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
e2 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
e2 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f204,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
e0 != e1,
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
e3 = op(e2,e4),
inference(cnf_transformation,[],[f6]) ).
fof(f207,plain,
e1 = op(e4,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f208,plain,
e0 = op(op(e4,e2),op(e4,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f211,plain,
( op(e0,e0) != op(e0,e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f9]) ).
fof(f214,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP21 ),
inference(cnf_transformation,[],[f9]) ).
fof(f215,plain,
( e2 != op(op(e0,e2),e0)
| ~ sP20 ),
inference(cnf_transformation,[],[f9]) ).
fof(f218,plain,
( e3 != op(op(e0,e3),e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f9]) ).
fof(f221,plain,
( e4 != op(op(e0,e4),e0)
| ~ sP18 ),
inference(cnf_transformation,[],[f9]) ).
fof(f226,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP17 ),
inference(cnf_transformation,[],[f9]) ).
fof(f229,plain,
( op(e1,e1) != op(e1,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f9]) ).
fof(f231,plain,
( e1 = op(op(e1,e2),e2)
| ~ sP15 ),
inference(cnf_transformation,[],[f9]) ).
fof(f234,plain,
( e1 = op(op(e1,e3),e3)
| ~ sP14 ),
inference(cnf_transformation,[],[f9]) ).
fof(f236,plain,
( e4 != op(op(e1,e4),e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f9]) ).
fof(f241,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP12 ),
inference(cnf_transformation,[],[f9]) ).
fof(f242,plain,
( e1 != op(op(e2,e1),e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f9]) ).
fof(f247,plain,
( op(e2,e2) != op(e2,e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f9]) ).
fof(f249,plain,
( e2 = op(op(e2,e3),e3)
| ~ sP9 ),
inference(cnf_transformation,[],[f9]) ).
fof(f252,plain,
( e2 = op(op(e2,e4),e4)
| ~ sP8 ),
inference(cnf_transformation,[],[f9]) ).
fof(f256,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP7 ),
inference(cnf_transformation,[],[f9]) ).
fof(f257,plain,
( e1 != op(op(e3,e1),e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f9]) ).
fof(f260,plain,
( e2 != op(op(e3,e2),e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f9]) ).
fof(f265,plain,
( op(e3,e3) != op(e3,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f9]) ).
fof(f267,plain,
( e3 = op(op(e3,e4),e4)
| ~ sP3 ),
inference(cnf_transformation,[],[f9]) ).
fof(f271,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP2 ),
inference(cnf_transformation,[],[f9]) ).
fof(f272,plain,
( e1 != op(op(e4,e1),e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f275,plain,
( e2 != op(op(e4,e2),e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f9]) ).
fof(f279,plain,
( op(e4,e4) != op(e4,e4)
| e4 = op(op(e4,e3),e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22 ),
inference(cnf_transformation,[],[f9]) ).
fof(f287,plain,
( e0 = op(e0,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f9]) ).
fof(f291,plain,
( e1 = op(e1,e0)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f292,plain,
( e1 = op(e1,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f298,plain,
( e2 = op(e2,e4)
| e4 != op(e2,e2) ),
inference(cnf_transformation,[],[f9]) ).
fof(f300,plain,
( e3 = op(e3,e1)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f9]) ).
fof(f301,plain,
( e3 = op(e3,e2)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f9]) ).
fof(f302,plain,
( e3 = op(e3,e4)
| e4 != op(e3,e3) ),
inference(cnf_transformation,[],[f9]) ).
fof(f303,plain,
( e4 = op(e4,e0)
| e0 != op(e4,e4) ),
inference(cnf_transformation,[],[f9]) ).
fof(f305,plain,
( e4 = op(e4,e2)
| e2 != op(e4,e4) ),
inference(cnf_transformation,[],[f9]) ).
fof(f307,plain,
~ sP22,
inference(trivial_inequality_removal,[],[f211]) ).
fof(f308,plain,
~ sP16,
inference(trivial_inequality_removal,[],[f229]) ).
fof(f309,plain,
~ sP10,
inference(trivial_inequality_removal,[],[f247]) ).
fof(f310,plain,
~ sP4,
inference(trivial_inequality_removal,[],[f265]) ).
fof(f312,plain,
( e4 = op(op(e4,e3),e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22 ),
inference(trivial_inequality_removal,[],[f279]) ).
fof(f315,definition,
( spl23_1
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition]) ).
fof(f324,plain,
~ spl23_1,
inference(avatar_split_clause,[],[f307,f315]) ).
fof(f326,definition,
( spl23_3
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition]) ).
fof(f340,definition,
( spl23_6
<=> op(e0,e1) = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition]) ).
fof(f342,plain,
( op(e0,e1) != op(e1,e0)
| spl23_6 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f343,plain,
( ~ spl23_3
| ~ spl23_6 ),
inference(avatar_split_clause,[],[f214,f340,f326]) ).
fof(f345,definition,
( spl23_7
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl23_7])],[avatar_definition]) ).
fof(f349,definition,
( spl23_8
<=> e2 = op(op(e0,e2),e0) ),
introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition]) ).
fof(f351,plain,
( e2 != op(op(e0,e2),e0)
| spl23_8 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f352,plain,
( ~ spl23_7
| ~ spl23_8 ),
inference(avatar_split_clause,[],[f215,f349,f345]) ).
fof(f359,definition,
( spl23_10
<=> op(e0,e2) = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl23_10])],[avatar_definition]) ).
fof(f361,plain,
( op(e0,e2) != op(e2,e0)
| spl23_10 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f364,definition,
( spl23_11
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition]) ).
fof(f368,definition,
( spl23_12
<=> e3 = op(op(e0,e3),e0) ),
introduced(definition,[new_symbols(definition,[spl23_12])],[avatar_definition]) ).
fof(f370,plain,
( e3 != op(op(e0,e3),e0)
| spl23_12 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f371,plain,
( ~ spl23_11
| ~ spl23_12 ),
inference(avatar_split_clause,[],[f218,f368,f364]) ).
fof(f378,definition,
( spl23_14
<=> op(e0,e3) = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl23_14])],[avatar_definition]) ).
fof(f380,plain,
( op(e0,e3) != op(e3,e0)
| spl23_14 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f383,definition,
( spl23_15
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl23_15])],[avatar_definition]) ).
fof(f387,definition,
( spl23_16
<=> e4 = op(op(e0,e4),e0) ),
introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition]) ).
fof(f389,plain,
( e4 != op(op(e0,e4),e0)
| spl23_16 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f390,plain,
( ~ spl23_15
| ~ spl23_16 ),
inference(avatar_split_clause,[],[f221,f387,f383]) ).
fof(f397,definition,
( spl23_18
<=> op(e0,e4) = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl23_18])],[avatar_definition]) ).
fof(f399,plain,
( op(e0,e4) != op(e4,e0)
| spl23_18 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f402,definition,
( spl23_19
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition]) ).
fof(f415,plain,
( ~ spl23_19
| ~ spl23_6 ),
inference(avatar_split_clause,[],[f226,f340,f402]) ).
fof(f417,definition,
( spl23_22
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl23_22])],[avatar_definition]) ).
fof(f426,plain,
~ spl23_22,
inference(avatar_split_clause,[],[f308,f417]) ).
fof(f428,definition,
( spl23_24
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl23_24])],[avatar_definition]) ).
fof(f437,definition,
( spl23_26
<=> e1 = op(op(e1,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition]) ).
fof(f439,plain,
( e1 = op(op(e1,e2),e2)
| ~ spl23_26 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f440,plain,
( ~ spl23_24
| spl23_26 ),
inference(avatar_split_clause,[],[f231,f437,f428]) ).
fof(f447,definition,
( spl23_28
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl23_28])],[avatar_definition]) ).
fof(f456,definition,
( spl23_30
<=> e1 = op(op(e1,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl23_30])],[avatar_definition]) ).
fof(f458,plain,
( e1 = op(op(e1,e3),e3)
| ~ spl23_30 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f459,plain,
( ~ spl23_28
| spl23_30 ),
inference(avatar_split_clause,[],[f234,f456,f447]) ).
fof(f466,definition,
( spl23_32
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl23_32])],[avatar_definition]) ).
fof(f470,definition,
( spl23_33
<=> e4 = op(op(e1,e4),e1) ),
introduced(definition,[new_symbols(definition,[spl23_33])],[avatar_definition]) ).
fof(f472,plain,
( e4 != op(op(e1,e4),e1)
| spl23_33 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f473,plain,
( ~ spl23_32
| ~ spl23_33 ),
inference(avatar_split_clause,[],[f236,f470,f466]) ).
fof(f485,definition,
( spl23_36
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl23_36])],[avatar_definition]) ).
fof(f498,plain,
( ~ spl23_36
| ~ spl23_10 ),
inference(avatar_split_clause,[],[f241,f359,f485]) ).
fof(f500,definition,
( spl23_39
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl23_39])],[avatar_definition]) ).
fof(f504,definition,
( spl23_40
<=> e1 = op(op(e2,e1),e2) ),
introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition]) ).
fof(f506,plain,
( e1 != op(op(e2,e1),e2)
| spl23_40 ),
inference(avatar_component_clause,[],[f504]) ).
fof(f507,plain,
( ~ spl23_39
| ~ spl23_40 ),
inference(avatar_split_clause,[],[f242,f504,f500]) ).
fof(f515,definition,
( spl23_42
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl23_42])],[avatar_definition]) ).
fof(f524,plain,
~ spl23_42,
inference(avatar_split_clause,[],[f309,f515]) ).
fof(f526,definition,
( spl23_44
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl23_44])],[avatar_definition]) ).
fof(f535,definition,
( spl23_46
<=> e2 = op(op(e2,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl23_46])],[avatar_definition]) ).
fof(f537,plain,
( e2 = op(op(e2,e3),e3)
| ~ spl23_46 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f538,plain,
( ~ spl23_44
| spl23_46 ),
inference(avatar_split_clause,[],[f249,f535,f526]) ).
fof(f545,definition,
( spl23_48
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl23_48])],[avatar_definition]) ).
fof(f554,definition,
( spl23_50
<=> e2 = op(op(e2,e4),e4) ),
introduced(definition,[new_symbols(definition,[spl23_50])],[avatar_definition]) ).
fof(f556,plain,
( e2 = op(op(e2,e4),e4)
| ~ spl23_50 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f557,plain,
( ~ spl23_48
| spl23_50 ),
inference(avatar_split_clause,[],[f252,f554,f545]) ).
fof(f564,definition,
( spl23_52
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl23_52])],[avatar_definition]) ).
fof(f577,plain,
( ~ spl23_52
| ~ spl23_14 ),
inference(avatar_split_clause,[],[f256,f378,f564]) ).
fof(f579,definition,
( spl23_55
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl23_55])],[avatar_definition]) ).
fof(f583,definition,
( spl23_56
<=> e1 = op(op(e3,e1),e3) ),
introduced(definition,[new_symbols(definition,[spl23_56])],[avatar_definition]) ).
fof(f585,plain,
( e1 != op(op(e3,e1),e3)
| spl23_56 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f586,plain,
( ~ spl23_55
| ~ spl23_56 ),
inference(avatar_split_clause,[],[f257,f583,f579]) ).
fof(f594,definition,
( spl23_58
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl23_58])],[avatar_definition]) ).
fof(f598,definition,
( spl23_59
<=> e2 = op(op(e3,e2),e3) ),
introduced(definition,[new_symbols(definition,[spl23_59])],[avatar_definition]) ).
fof(f599,plain,
( e2 = op(op(e3,e2),e3)
| ~ spl23_59 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f600,plain,
( e2 != op(op(e3,e2),e3)
| spl23_59 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f601,plain,
( ~ spl23_58
| ~ spl23_59 ),
inference(avatar_split_clause,[],[f260,f598,f594]) ).
fof(f609,definition,
( spl23_61
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl23_61])],[avatar_definition]) ).
fof(f618,plain,
~ spl23_61,
inference(avatar_split_clause,[],[f310,f609]) ).
fof(f620,definition,
( spl23_63
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl23_63])],[avatar_definition]) ).
fof(f629,definition,
( spl23_65
<=> e3 = op(op(e3,e4),e4) ),
introduced(definition,[new_symbols(definition,[spl23_65])],[avatar_definition]) ).
fof(f631,plain,
( e3 = op(op(e3,e4),e4)
| ~ spl23_65 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f632,plain,
( ~ spl23_63
| spl23_65 ),
inference(avatar_split_clause,[],[f267,f629,f620]) ).
fof(f639,definition,
( spl23_67
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl23_67])],[avatar_definition]) ).
fof(f652,plain,
( ~ spl23_67
| ~ spl23_18 ),
inference(avatar_split_clause,[],[f271,f397,f639]) ).
fof(f654,definition,
( spl23_70
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl23_70])],[avatar_definition]) ).
fof(f658,definition,
( spl23_71
<=> e1 = op(op(e4,e1),e4) ),
introduced(definition,[new_symbols(definition,[spl23_71])],[avatar_definition]) ).
fof(f660,plain,
( e1 != op(op(e4,e1),e4)
| spl23_71 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f661,plain,
( ~ spl23_70
| ~ spl23_71 ),
inference(avatar_split_clause,[],[f272,f658,f654]) ).
fof(f669,definition,
( spl23_73
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl23_73])],[avatar_definition]) ).
fof(f673,definition,
( spl23_74
<=> e2 = op(op(e4,e2),e4) ),
introduced(definition,[new_symbols(definition,[spl23_74])],[avatar_definition]) ).
fof(f675,plain,
( e2 != op(op(e4,e2),e4)
| spl23_74 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f676,plain,
( ~ spl23_73
| ~ spl23_74 ),
inference(avatar_split_clause,[],[f275,f673,f669]) ).
fof(f689,definition,
( spl23_77
<=> e4 = op(op(e4,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl23_77])],[avatar_definition]) ).
fof(f691,plain,
( e4 = op(op(e4,e3),e3)
| ~ spl23_77 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f692,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_22
| spl23_24
| spl23_28
| spl23_32
| spl23_36
| spl23_39
| spl23_42
| spl23_44
| spl23_48
| spl23_52
| spl23_55
| spl23_58
| spl23_61
| spl23_63
| spl23_67
| spl23_70
| spl23_73
| spl23_77 ),
inference(avatar_split_clause,[],[f312,f689,f669,f654,f639,f620,f609,f594,f579,f564,f545,f526,f515,f500,f485,f466,f447,f428,f417,f402,f383,f364,f345,f326,f315]) ).
fof(f705,definition,
( spl23_79
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl23_79])],[avatar_definition]) ).
fof(f709,definition,
( spl23_80
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl23_80])],[avatar_definition]) ).
fof(f711,plain,
( e0 = op(e0,e1)
| ~ spl23_80 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f712,plain,
( ~ spl23_79
| spl23_80 ),
inference(avatar_split_clause,[],[f287,f709,f705]) ).
fof(f736,definition,
( spl23_86
<=> e0 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl23_86])],[avatar_definition]) ).
fof(f738,plain,
( e0 = op(e0,e4)
| ~ spl23_86 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f741,definition,
( spl23_87
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_87])],[avatar_definition]) ).
fof(f742,plain,
( e0 = op(e1,e1)
| ~ spl23_87 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f745,definition,
( spl23_88
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl23_88])],[avatar_definition]) ).
fof(f747,plain,
( e1 = op(e1,e0)
| ~ spl23_88 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f748,plain,
( ~ spl23_87
| spl23_88 ),
inference(avatar_split_clause,[],[f291,f745,f741]) ).
fof(f750,definition,
( spl23_89
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_89])],[avatar_definition]) ).
fof(f754,definition,
( spl23_90
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl23_90])],[avatar_definition]) ).
fof(f757,plain,
( ~ spl23_89
| spl23_90 ),
inference(avatar_split_clause,[],[f292,f754,f750]) ).
fof(f759,definition,
( spl23_91
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_91])],[avatar_definition]) ).
fof(f760,plain,
( e3 = op(e1,e1)
| ~ spl23_91 ),
inference(avatar_component_clause,[],[f759]) ).
fof(f763,definition,
( spl23_92
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl23_92])],[avatar_definition]) ).
fof(f764,plain,
( e1 != op(e1,e3)
| spl23_92 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f765,plain,
( e1 = op(e1,e3)
| ~ spl23_92 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f768,definition,
( spl23_93
<=> e4 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl23_93])],[avatar_definition]) ).
fof(f769,plain,
( e4 = op(e1,e1)
| ~ spl23_93 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f772,definition,
( spl23_94
<=> e1 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl23_94])],[avatar_definition]) ).
fof(f774,plain,
( e1 = op(e1,e4)
| ~ spl23_94 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f781,definition,
( spl23_96
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl23_96])],[avatar_definition]) ).
fof(f782,plain,
( e2 != op(e2,e0)
| spl23_96 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f783,plain,
( e2 = op(e2,e0)
| ~ spl23_96 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f786,definition,
( spl23_97
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_97])],[avatar_definition]) ).
fof(f790,definition,
( spl23_98
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl23_98])],[avatar_definition]) ).
fof(f792,plain,
( e2 = op(e2,e1)
| ~ spl23_98 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f795,definition,
( spl23_99
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_99])],[avatar_definition]) ).
fof(f799,definition,
( spl23_100
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl23_100])],[avatar_definition]) ).
fof(f800,plain,
( e2 != op(e2,e3)
| spl23_100 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f801,plain,
( e2 = op(e2,e3)
| ~ spl23_100 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f804,definition,
( spl23_101
<=> e4 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl23_101])],[avatar_definition]) ).
fof(f808,definition,
( spl23_102
<=> e2 = op(e2,e4) ),
introduced(definition,[new_symbols(definition,[spl23_102])],[avatar_definition]) ).
fof(f810,plain,
( e2 = op(e2,e4)
| ~ spl23_102 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f811,plain,
( ~ spl23_101
| spl23_102 ),
inference(avatar_split_clause,[],[f298,f808,f804]) ).
fof(f813,definition,
( spl23_103
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_103])],[avatar_definition]) ).
fof(f814,plain,
( e0 = op(e3,e3)
| ~ spl23_103 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f817,definition,
( spl23_104
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl23_104])],[avatar_definition]) ).
fof(f819,plain,
( e3 = op(e3,e0)
| ~ spl23_104 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f822,definition,
( spl23_105
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_105])],[avatar_definition]) ).
fof(f823,plain,
( e1 = op(e3,e3)
| ~ spl23_105 ),
inference(avatar_component_clause,[],[f822]) ).
fof(f826,definition,
( spl23_106
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl23_106])],[avatar_definition]) ).
fof(f828,plain,
( e3 = op(e3,e1)
| ~ spl23_106 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f829,plain,
( ~ spl23_105
| spl23_106 ),
inference(avatar_split_clause,[],[f300,f826,f822]) ).
fof(f831,definition,
( spl23_107
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_107])],[avatar_definition]) ).
fof(f835,definition,
( spl23_108
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl23_108])],[avatar_definition]) ).
fof(f837,plain,
( e3 = op(e3,e2)
| ~ spl23_108 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f838,plain,
( ~ spl23_107
| spl23_108 ),
inference(avatar_split_clause,[],[f301,f835,f831]) ).
fof(f840,definition,
( spl23_109
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl23_109])],[avatar_definition]) ).
fof(f844,definition,
( spl23_110
<=> e3 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl23_110])],[avatar_definition]) ).
fof(f847,plain,
( ~ spl23_109
| spl23_110 ),
inference(avatar_split_clause,[],[f302,f844,f840]) ).
fof(f849,definition,
( spl23_111
<=> e0 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_111])],[avatar_definition]) ).
fof(f853,definition,
( spl23_112
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl23_112])],[avatar_definition]) ).
fof(f854,plain,
( e4 != op(e4,e0)
| spl23_112 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f855,plain,
( e4 = op(e4,e0)
| ~ spl23_112 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f856,plain,
( ~ spl23_111
| spl23_112 ),
inference(avatar_split_clause,[],[f303,f853,f849]) ).
fof(f858,definition,
( spl23_113
<=> e1 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_113])],[avatar_definition]) ).
fof(f862,definition,
( spl23_114
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl23_114])],[avatar_definition]) ).
fof(f863,plain,
( e4 != op(e4,e1)
| spl23_114 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f864,plain,
( e4 = op(e4,e1)
| ~ spl23_114 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f867,definition,
( spl23_115
<=> e2 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_115])],[avatar_definition]) ).
fof(f871,definition,
( spl23_116
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl23_116])],[avatar_definition]) ).
fof(f873,plain,
( e4 = op(e4,e2)
| ~ spl23_116 ),
inference(avatar_component_clause,[],[f871]) ).
fof(f874,plain,
( ~ spl23_115
| spl23_116 ),
inference(avatar_split_clause,[],[f305,f871,f867]) ).
fof(f876,definition,
( spl23_117
<=> e3 = op(e4,e4) ),
introduced(definition,[new_symbols(definition,[spl23_117])],[avatar_definition]) ).
fof(f880,definition,
( spl23_118
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl23_118])],[avatar_definition]) ).
fof(f882,plain,
( e4 = op(e4,e3)
| ~ spl23_118 ),
inference(avatar_component_clause,[],[f880]) ).
fof(f884,plain,
e0 = op(e1,e1),
inference(forward_demodulation,[],[f208,f207]) ).
fof(f885,plain,
e1 != op(e4,e4),
inference(forward_demodulation,[],[f97,f207]) ).
fof(f886,plain,
e1 != op(e4,e3),
inference(forward_demodulation,[],[f98,f207]) ).
fof(f889,plain,
e3 != op(e2,e3),
inference(forward_demodulation,[],[f116,f206]) ).
fof(f890,plain,
e3 != op(e2,e2),
inference(forward_demodulation,[],[f117,f206]) ).
fof(f891,plain,
e3 != op(e2,e1),
inference(forward_demodulation,[],[f119,f206]) ).
fof(f893,plain,
e3 != op(e4,e4),
inference(forward_demodulation,[],[f147,f206]) ).
fof(f894,plain,
e3 != op(e3,e4),
inference(forward_demodulation,[],[f148,f206]) ).
fof(f895,plain,
e3 != op(e1,e4),
inference(forward_demodulation,[],[f151,f206]) ).
fof(f897,plain,
e1 != op(e3,e2),
inference(forward_demodulation,[],[f166,f207]) ).
fof(f898,plain,
e1 != op(e2,e2),
inference(forward_demodulation,[],[f167,f207]) ).
fof(f899,plain,
e1 != op(e1,e2),
inference(forward_demodulation,[],[f169,f207]) ).
fof(f900,plain,
e1 != op(e0,e2),
inference(forward_demodulation,[],[f172,f207]) ).
fof(f915,definition,
( spl23_122
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl23_122])],[avatar_definition]) ).
fof(f917,plain,
( e0 = op(e3,e0)
| ~ spl23_122 ),
inference(avatar_component_clause,[],[f915]) ).
fof(f924,definition,
( spl23_124
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl23_124])],[avatar_definition]) ).
fof(f926,plain,
( e1 = op(e0,e1)
| ~ spl23_124 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f928,definition,
( spl23_125
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl23_125])],[avatar_definition]) ).
fof(f932,definition,
( spl23_126
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl23_126])],[avatar_definition]) ).
fof(f934,plain,
( e1 = op(e0,e3)
| ~ spl23_126 ),
inference(avatar_component_clause,[],[f932]) ).
fof(f936,definition,
( spl23_127
<=> e1 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl23_127])],[avatar_definition]) ).
fof(f938,plain,
( e1 = op(e0,e4)
| ~ spl23_127 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f939,plain,
( spl23_79
| spl23_124
| spl23_125
| spl23_126
| spl23_127 ),
inference(avatar_split_clause,[],[f48,f936,f932,f928,f924,f705]) ).
fof(f941,definition,
( spl23_128
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl23_128])],[avatar_definition]) ).
fof(f943,plain,
( e1 = op(e2,e0)
| ~ spl23_128 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f945,definition,
( spl23_129
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl23_129])],[avatar_definition]) ).
fof(f947,plain,
( e1 = op(e3,e0)
| ~ spl23_129 ),
inference(avatar_component_clause,[],[f945]) ).
fof(f954,definition,
( spl23_131
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl23_131])],[avatar_definition]) ).
fof(f956,plain,
( e2 = op(e0,e1)
| ~ spl23_131 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f958,definition,
( spl23_132
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl23_132])],[avatar_definition]) ).
fof(f960,plain,
( e2 = op(e0,e2)
| ~ spl23_132 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f962,definition,
( spl23_133
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl23_133])],[avatar_definition]) ).
fof(f964,plain,
( e2 = op(e0,e3)
| ~ spl23_133 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f966,definition,
( spl23_134
<=> e2 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl23_134])],[avatar_definition]) ).
fof(f968,plain,
( e2 = op(e0,e4)
| ~ spl23_134 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f971,definition,
( spl23_135
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl23_135])],[avatar_definition]) ).
fof(f973,plain,
( e2 = op(e1,e0)
| ~ spl23_135 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f975,definition,
( spl23_136
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl23_136])],[avatar_definition]) ).
fof(f977,plain,
( e2 = op(e3,e0)
| ~ spl23_136 ),
inference(avatar_component_clause,[],[f975]) ).
fof(f979,definition,
( spl23_137
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl23_137])],[avatar_definition]) ).
fof(f981,plain,
( e2 = op(e4,e0)
| ~ spl23_137 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f984,definition,
( spl23_138
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl23_138])],[avatar_definition]) ).
fof(f986,plain,
( e3 = op(e0,e1)
| ~ spl23_138 ),
inference(avatar_component_clause,[],[f984]) ).
fof(f988,definition,
( spl23_139
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl23_139])],[avatar_definition]) ).
fof(f990,plain,
( e3 = op(e0,e2)
| ~ spl23_139 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f992,definition,
( spl23_140
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl23_140])],[avatar_definition]) ).
fof(f994,plain,
( e3 = op(e0,e3)
| ~ spl23_140 ),
inference(avatar_component_clause,[],[f992]) ).
fof(f1001,definition,
( spl23_142
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl23_142])],[avatar_definition]) ).
fof(f1003,plain,
( e3 = op(e1,e0)
| ~ spl23_142 ),
inference(avatar_component_clause,[],[f1001]) ).
fof(f1009,definition,
( spl23_144
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl23_144])],[avatar_definition]) ).
fof(f1011,plain,
( e3 = op(e4,e0)
| ~ spl23_144 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1018,definition,
( spl23_146
<=> e4 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl23_146])],[avatar_definition]) ).
fof(f1020,plain,
( e4 = op(e0,e2)
| ~ spl23_146 ),
inference(avatar_component_clause,[],[f1018]) ).
fof(f1022,definition,
( spl23_147
<=> e4 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl23_147])],[avatar_definition]) ).
fof(f1024,plain,
( e4 = op(e0,e3)
| ~ spl23_147 ),
inference(avatar_component_clause,[],[f1022]) ).
fof(f1026,definition,
( spl23_148
<=> e4 = op(e0,e4) ),
introduced(definition,[new_symbols(definition,[spl23_148])],[avatar_definition]) ).
fof(f1028,plain,
( e4 = op(e0,e4)
| ~ spl23_148 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1031,definition,
( spl23_149
<=> e4 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl23_149])],[avatar_definition]) ).
fof(f1033,plain,
( e4 = op(e1,e0)
| ~ spl23_149 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1035,definition,
( spl23_150
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl23_150])],[avatar_definition]) ).
fof(f1037,plain,
( e4 = op(e2,e0)
| ~ spl23_150 ),
inference(avatar_component_clause,[],[f1035]) ).
fof(f1052,definition,
( spl23_154
<=> e0 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl23_154])],[avatar_definition]) ).
fof(f1054,plain,
( e0 = op(e1,e4)
| ~ spl23_154 ),
inference(avatar_component_clause,[],[f1052]) ).
fof(f1061,definition,
( spl23_156
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl23_156])],[avatar_definition]) ).
fof(f1063,plain,
( e0 = op(e3,e1)
| ~ spl23_156 ),
inference(avatar_component_clause,[],[f1061]) ).
fof(f1075,definition,
( spl23_159
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl23_159])],[avatar_definition]) ).
fof(f1077,plain,
( e1 = op(e2,e1)
| ~ spl23_159 ),
inference(avatar_component_clause,[],[f1075]) ).
fof(f1079,definition,
( spl23_160
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl23_160])],[avatar_definition]) ).
fof(f1081,plain,
( e1 = op(e3,e1)
| ~ spl23_160 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1088,definition,
( spl23_162
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl23_162])],[avatar_definition]) ).
fof(f1090,plain,
( e2 = op(e1,e2)
| ~ spl23_162 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1092,definition,
( spl23_163
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl23_163])],[avatar_definition]) ).
fof(f1094,plain,
( e2 = op(e1,e3)
| ~ spl23_163 ),
inference(avatar_component_clause,[],[f1092]) ).
fof(f1096,definition,
( spl23_164
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl23_164])],[avatar_definition]) ).
fof(f1098,plain,
( e2 = op(e1,e4)
| ~ spl23_164 ),
inference(avatar_component_clause,[],[f1096]) ).
fof(f1099,plain,
( spl23_135
| spl23_89
| spl23_162
| spl23_163
| spl23_164 ),
inference(avatar_split_clause,[],[f60,f1096,f1092,f1088,f750,f971]) ).
fof(f1101,definition,
( spl23_165
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl23_165])],[avatar_definition]) ).
fof(f1103,plain,
( e2 = op(e3,e1)
| ~ spl23_165 ),
inference(avatar_component_clause,[],[f1101]) ).
fof(f1105,definition,
( spl23_166
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl23_166])],[avatar_definition]) ).
fof(f1107,plain,
( e2 = op(e4,e1)
| ~ spl23_166 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1108,plain,
( spl23_131
| spl23_89
| spl23_98
| spl23_165
| spl23_166 ),
inference(avatar_split_clause,[],[f61,f1105,f1101,f790,f750,f954]) ).
fof(f1110,definition,
( spl23_167
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl23_167])],[avatar_definition]) ).
fof(f1112,plain,
( e3 = op(e1,e2)
| ~ spl23_167 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1114,definition,
( spl23_168
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl23_168])],[avatar_definition]) ).
fof(f1116,plain,
( e3 = op(e1,e3)
| ~ spl23_168 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1118,definition,
( spl23_169
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl23_169])],[avatar_definition]) ).
fof(f1121,plain,
( spl23_142
| spl23_91
| spl23_167
| spl23_168
| spl23_169 ),
inference(avatar_split_clause,[],[f62,f1118,f1114,f1110,f759,f1001]) ).
fof(f1123,definition,
( spl23_170
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl23_170])],[avatar_definition]) ).
fof(f1127,definition,
( spl23_171
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl23_171])],[avatar_definition]) ).
fof(f1129,plain,
( e3 = op(e4,e1)
| ~ spl23_171 ),
inference(avatar_component_clause,[],[f1127]) ).
fof(f1130,plain,
( spl23_138
| spl23_91
| spl23_170
| spl23_106
| spl23_171 ),
inference(avatar_split_clause,[],[f63,f1127,f826,f1123,f759,f984]) ).
fof(f1132,definition,
( spl23_172
<=> e4 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl23_172])],[avatar_definition]) ).
fof(f1134,plain,
( e4 = op(e1,e2)
| ~ spl23_172 ),
inference(avatar_component_clause,[],[f1132]) ).
fof(f1136,definition,
( spl23_173
<=> e4 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl23_173])],[avatar_definition]) ).
fof(f1138,plain,
( e4 = op(e1,e3)
| ~ spl23_173 ),
inference(avatar_component_clause,[],[f1136]) ).
fof(f1140,definition,
( spl23_174
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl23_174])],[avatar_definition]) ).
fof(f1142,plain,
( e4 = op(e1,e4)
| ~ spl23_174 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1143,plain,
( spl23_149
| spl23_93
| spl23_172
| spl23_173
| spl23_174 ),
inference(avatar_split_clause,[],[f64,f1140,f1136,f1132,f768,f1031]) ).
fof(f1145,definition,
( spl23_175
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl23_175])],[avatar_definition]) ).
fof(f1147,plain,
( e4 = op(e2,e1)
| ~ spl23_175 ),
inference(avatar_component_clause,[],[f1145]) ).
fof(f1155,plain,
( e1 = e3
| e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) ),
inference(forward_demodulation,[],[f68,f206]) ).
fof(f1158,plain,
( e1 = e3
| e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
inference(forward_demodulation,[],[f73,f207]) ).
fof(f1159,plain,
( e3 = e4
| e4 = op(e2,e3)
| e4 = op(e2,e2)
| e4 = op(e2,e1)
| e4 = op(e2,e0) ),
inference(forward_demodulation,[],[f74,f206]) ).
fof(f1160,plain,
( e1 = e4
| e4 = op(e3,e2)
| e4 = op(e2,e2)
| e4 = op(e1,e2)
| e4 = op(e0,e2) ),
inference(forward_demodulation,[],[f75,f207]) ).
fof(f1162,definition,
( spl23_177
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl23_177])],[avatar_definition]) ).
fof(f1164,plain,
( e0 = op(e3,e2)
| ~ spl23_177 ),
inference(avatar_component_clause,[],[f1162]) ).
fof(f1166,definition,
( spl23_178
<=> e0 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl23_178])],[avatar_definition]) ).
fof(f1168,plain,
( e0 = op(e3,e4)
| ~ spl23_178 ),
inference(avatar_component_clause,[],[f1166]) ).
fof(f1169,plain,
( spl23_122
| spl23_156
| spl23_177
| spl23_103
| spl23_178 ),
inference(avatar_split_clause,[],[f76,f1166,f813,f1162,f1061,f915]) ).
fof(f1180,definition,
( spl23_181
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl23_181])],[avatar_definition]) ).
fof(f1184,definition,
( spl23_182
<=> e1 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl23_182])],[avatar_definition]) ).
fof(f1186,plain,
( e1 = op(e3,e4)
| ~ spl23_182 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1187,plain,
( spl23_129
| spl23_160
| spl23_181
| spl23_105
| spl23_182 ),
inference(avatar_split_clause,[],[f78,f1184,f822,f1180,f1079,f945]) ).
fof(f1189,definition,
( spl23_183
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl23_183])],[avatar_definition]) ).
fof(f1191,plain,
( e1 = op(e2,e3)
| ~ spl23_183 ),
inference(avatar_component_clause,[],[f1189]) ).
fof(f1193,definition,
( spl23_184
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl23_184])],[avatar_definition]) ).
fof(f1194,plain,
( e1 != op(e4,e3)
| spl23_184 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1196,plain,
( spl23_126
| spl23_92
| spl23_183
| spl23_105
| spl23_184 ),
inference(avatar_split_clause,[],[f79,f1193,f822,f1189,f763,f932]) ).
fof(f1198,definition,
( spl23_185
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl23_185])],[avatar_definition]) ).
fof(f1200,plain,
( e2 = op(e3,e2)
| ~ spl23_185 ),
inference(avatar_component_clause,[],[f1198]) ).
fof(f1202,definition,
( spl23_186
<=> e2 = op(e3,e4) ),
introduced(definition,[new_symbols(definition,[spl23_186])],[avatar_definition]) ).
fof(f1203,plain,
( e2 != op(e3,e4)
| spl23_186 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1204,plain,
( e2 = op(e3,e4)
| ~ spl23_186 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1205,plain,
( spl23_136
| spl23_165
| spl23_185
| spl23_107
| spl23_186 ),
inference(avatar_split_clause,[],[f80,f1202,f831,f1198,f1101,f975]) ).
fof(f1207,definition,
( spl23_187
<=> e2 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl23_187])],[avatar_definition]) ).
fof(f1209,plain,
( e2 = op(e4,e3)
| ~ spl23_187 ),
inference(avatar_component_clause,[],[f1207]) ).
fof(f1210,plain,
( spl23_133
| spl23_163
| spl23_100
| spl23_107
| spl23_187 ),
inference(avatar_split_clause,[],[f81,f1207,f831,f799,f1092,f962]) ).
fof(f1217,definition,
( spl23_189
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl23_189])],[avatar_definition]) ).
fof(f1221,definition,
( spl23_190
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl23_190])],[avatar_definition]) ).
fof(f1223,plain,
( e3 = op(e4,e3)
| ~ spl23_190 ),
inference(avatar_component_clause,[],[f1221]) ).
fof(f1226,definition,
( spl23_191
<=> e4 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl23_191])],[avatar_definition]) ).
fof(f1228,plain,
( e4 = op(e3,e2)
| ~ spl23_191 ),
inference(avatar_component_clause,[],[f1226]) ).
fof(f1235,definition,
( spl23_193
<=> e4 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl23_193])],[avatar_definition]) ).
fof(f1236,plain,
( e4 != op(e2,e3)
| spl23_193 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1237,plain,
( e4 = op(e2,e3)
| ~ spl23_193 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1238,plain,
( spl23_147
| spl23_173
| spl23_193
| spl23_109
| spl23_118 ),
inference(avatar_split_clause,[],[f85,f880,f840,f1235,f1136,f1022]) ).
fof(f1240,plain,
( e0 = e3
| e0 = op(e4,e4)
| e0 = op(e3,e4)
| e0 = op(e1,e4)
| e0 = op(e0,e4) ),
inference(forward_demodulation,[],[f87,f206]) ).
fof(f1241,plain,
( e1 = e3
| e1 = op(e4,e4)
| e1 = op(e3,e4)
| e1 = op(e1,e4)
| e1 = op(e0,e4) ),
inference(forward_demodulation,[],[f89,f206]) ).
fof(f1242,plain,
( e1 = e2
| e2 = op(e4,e4)
| e2 = op(e4,e3)
| e2 = op(e4,e1)
| e2 = op(e4,e0) ),
inference(forward_demodulation,[],[f90,f207]) ).
fof(f1243,plain,
( e2 = e3
| e2 = op(e4,e4)
| e2 = op(e3,e4)
| e2 = op(e1,e4)
| e2 = op(e0,e4) ),
inference(forward_demodulation,[],[f91,f206]) ).
fof(f1244,plain,
( e1 = e3
| e3 = op(e4,e4)
| e3 = op(e4,e3)
| e3 = op(e4,e1)
| e3 = op(e4,e0) ),
inference(forward_demodulation,[],[f92,f207]) ).
fof(f1248,definition,
( spl23_194
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl23_194])],[avatar_definition]) ).
fof(f1250,plain,
( e0 = unit
| ~ spl23_194 ),
inference(avatar_component_clause,[],[f1248]) ).
fof(f1252,definition,
( spl23_195
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl23_195])],[avatar_definition]) ).
fof(f1254,plain,
( e1 = unit
| ~ spl23_195 ),
inference(avatar_component_clause,[],[f1252]) ).
fof(f1256,definition,
( spl23_196
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl23_196])],[avatar_definition]) ).
fof(f1258,plain,
( e2 = unit
| ~ spl23_196 ),
inference(avatar_component_clause,[],[f1256]) ).
fof(f1260,definition,
( spl23_197
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl23_197])],[avatar_definition]) ).
fof(f1262,plain,
( e3 = unit
| ~ spl23_197 ),
inference(avatar_component_clause,[],[f1260]) ).
fof(f1264,definition,
( spl23_198
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl23_198])],[avatar_definition]) ).
fof(f1266,plain,
( e4 = unit
| ~ spl23_198 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1267,plain,
( spl23_194
| spl23_195
| spl23_196
| spl23_197
| spl23_198 ),
inference(avatar_split_clause,[],[f35,f1264,f1260,f1256,f1252,f1248]) ).
fof(f1299,plain,
spl23_87,
inference(avatar_split_clause,[],[f884,f741]) ).
fof(f1300,plain,
~ spl23_113,
inference(avatar_split_clause,[],[f885,f858]) ).
fof(f1301,plain,
~ spl23_184,
inference(avatar_split_clause,[],[f886,f1193]) ).
fof(f1304,plain,
~ spl23_189,
inference(avatar_split_clause,[],[f889,f1217]) ).
fof(f1305,plain,
~ spl23_99,
inference(avatar_split_clause,[],[f890,f795]) ).
fof(f1306,plain,
~ spl23_170,
inference(avatar_split_clause,[],[f891,f1123]) ).
fof(f1308,plain,
~ spl23_117,
inference(avatar_split_clause,[],[f893,f876]) ).
fof(f1309,plain,
~ spl23_110,
inference(avatar_split_clause,[],[f894,f844]) ).
fof(f1310,plain,
~ spl23_169,
inference(avatar_split_clause,[],[f895,f1118]) ).
fof(f1312,plain,
~ spl23_181,
inference(avatar_split_clause,[],[f897,f1180]) ).
fof(f1313,plain,
~ spl23_97,
inference(avatar_split_clause,[],[f898,f786]) ).
fof(f1314,plain,
~ spl23_90,
inference(avatar_split_clause,[],[f899,f754]) ).
fof(f1315,plain,
~ spl23_125,
inference(avatar_split_clause,[],[f900,f928]) ).
fof(f1318,plain,
( e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) ),
inference(forward_subsumption_resolution,[],[f1155,f200]) ).
fof(f1321,plain,
( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
inference(forward_subsumption_resolution,[],[f1158,f200]) ).
fof(f1322,plain,
( e4 = op(e2,e3)
| e4 = op(e2,e2)
| e4 = op(e2,e1)
| e4 = op(e2,e0) ),
inference(forward_subsumption_resolution,[],[f1159,f196]) ).
fof(f1323,plain,
( e4 = op(e3,e2)
| e4 = op(e2,e2)
| e4 = op(e1,e2)
| e4 = op(e0,e2) ),
inference(forward_subsumption_resolution,[],[f1160,f199]) ).
fof(f1325,plain,
( e0 = op(e4,e4)
| e0 = op(e3,e4)
| e0 = op(e1,e4)
| e0 = op(e0,e4) ),
inference(forward_subsumption_resolution,[],[f1240,f203]) ).
fof(f1326,plain,
( e1 = op(e4,e4)
| e1 = op(e3,e4)
| e1 = op(e1,e4)
| e1 = op(e0,e4) ),
inference(forward_subsumption_resolution,[],[f1241,f200]) ).
fof(f1327,plain,
( e2 = op(e4,e4)
| e2 = op(e4,e3)
| e2 = op(e4,e1)
| e2 = op(e4,e0) ),
inference(forward_subsumption_resolution,[],[f1242,f201]) ).
fof(f1328,plain,
( e2 = op(e4,e4)
| e2 = op(e3,e4)
| e2 = op(e1,e4)
| e2 = op(e0,e4) ),
inference(forward_subsumption_resolution,[],[f1243,f198]) ).
fof(f1329,plain,
( e3 = op(e4,e4)
| e3 = op(e4,e3)
| e3 = op(e4,e1)
| e3 = op(e4,e0) ),
inference(forward_subsumption_resolution,[],[f1244,f200]) ).
fof(f1334,plain,
( spl23_128
| spl23_159
| spl23_97
| spl23_183 ),
inference(avatar_split_clause,[],[f1318,f1189,f786,f1075,f941]) ).
fof(f1337,plain,
( spl23_139
| spl23_167
| spl23_99
| spl23_108 ),
inference(avatar_split_clause,[],[f1321,f835,f795,f1110,f988]) ).
fof(f1338,plain,
( spl23_150
| spl23_175
| spl23_101
| spl23_193 ),
inference(avatar_split_clause,[],[f1322,f1235,f804,f1145,f1035]) ).
fof(f1339,plain,
( spl23_146
| spl23_172
| spl23_101
| spl23_191 ),
inference(avatar_split_clause,[],[f1323,f1226,f804,f1132,f1018]) ).
fof(f1341,plain,
( spl23_86
| spl23_154
| spl23_178
| spl23_111 ),
inference(avatar_split_clause,[],[f1325,f849,f1166,f1052,f736]) ).
fof(f1342,plain,
( spl23_127
| spl23_94
| spl23_182
| spl23_113 ),
inference(avatar_split_clause,[],[f1326,f858,f1184,f772,f936]) ).
fof(f1343,plain,
( spl23_137
| spl23_166
| spl23_187
| spl23_115 ),
inference(avatar_split_clause,[],[f1327,f867,f1207,f1105,f979]) ).
fof(f1344,plain,
( spl23_134
| spl23_164
| spl23_186
| spl23_115 ),
inference(avatar_split_clause,[],[f1328,f867,f1202,f1096,f966]) ).
fof(f1345,plain,
( spl23_144
| spl23_171
| spl23_190
| spl23_117 ),
inference(avatar_split_clause,[],[f1329,f876,f1221,f1127,f1009]) ).
fof(f1351,plain,
( e2 = e3
| ~ spl23_102 ),
inference(forward_demodulation,[],[f810,f206]) ).
fof(f1355,plain,
( e1 = e2
| ~ spl23_96
| ~ spl23_128 ),
inference(forward_demodulation,[],[f943,f783]) ).
fof(f1358,plain,
( e3 = e4
| ~ spl23_112
| ~ spl23_144 ),
inference(forward_demodulation,[],[f1011,f855]) ).
fof(f1365,plain,
( $false
| ~ spl23_102 ),
inference(forward_subsumption_resolution,[],[f1351,f198]) ).
fof(f1366,plain,
~ spl23_102,
inference(avatar_contradiction_clause,[],[f1365]) ).
fof(f1367,plain,
( $false
| ~ spl23_96
| ~ spl23_128 ),
inference(forward_subsumption_resolution,[],[f1355,f201]) ).
fof(f1368,plain,
( ~ spl23_96
| ~ spl23_128 ),
inference(avatar_contradiction_clause,[],[f1367]) ).
fof(f1369,plain,
( $false
| ~ spl23_112
| ~ spl23_144 ),
inference(forward_subsumption_resolution,[],[f1358,f196]) ).
fof(f1370,plain,
( ~ spl23_112
| ~ spl23_144 ),
inference(avatar_contradiction_clause,[],[f1369]) ).
fof(f1375,plain,
( e1 = e2
| ~ spl23_98
| ~ spl23_159 ),
inference(forward_demodulation,[],[f1077,f792]) ).
fof(f1379,plain,
( $false
| ~ spl23_98
| ~ spl23_159 ),
inference(forward_subsumption_resolution,[],[f1375,f201]) ).
fof(f1380,plain,
( ~ spl23_98
| ~ spl23_159 ),
inference(avatar_contradiction_clause,[],[f1379]) ).
fof(f1381,plain,
( e0 = e3
| ~ spl23_87
| ~ spl23_91 ),
inference(superposition,[],[f760,f742]) ).
fof(f1385,plain,
( $false
| ~ spl23_87
| ~ spl23_91 ),
inference(forward_subsumption_resolution,[],[f1381,f203]) ).
fof(f1386,plain,
( ~ spl23_87
| ~ spl23_91 ),
inference(avatar_contradiction_clause,[],[f1385]) ).
fof(f1388,plain,
( e0 = e4
| ~ spl23_87
| ~ spl23_93 ),
inference(superposition,[],[f769,f742]) ).
fof(f1392,plain,
( $false
| ~ spl23_87
| ~ spl23_93 ),
inference(forward_subsumption_resolution,[],[f1388,f202]) ).
fof(f1393,plain,
( ~ spl23_87
| ~ spl23_93 ),
inference(avatar_contradiction_clause,[],[f1392]) ).
fof(f1415,plain,
( e1 = e3
| ~ spl23_106
| ~ spl23_160 ),
inference(forward_demodulation,[],[f1081,f828]) ).
fof(f1417,plain,
( $false
| ~ spl23_106
| ~ spl23_160 ),
inference(forward_subsumption_resolution,[],[f1415,f200]) ).
fof(f1418,plain,
( ~ spl23_106
| ~ spl23_160 ),
inference(avatar_contradiction_clause,[],[f1417]) ).
fof(f1421,plain,
( e1 != op(e0,e1)
| spl23_6
| ~ spl23_88 ),
inference(superposition,[],[f342,f747]) ).
fof(f1422,plain,
( $false
| spl23_6
| ~ spl23_88
| ~ spl23_124 ),
inference(forward_subsumption_resolution,[],[f1421,f926]) ).
fof(f1423,plain,
( spl23_6
| ~ spl23_88
| ~ spl23_124 ),
inference(avatar_contradiction_clause,[],[f1422]) ).
fof(f1441,plain,
( e1 = e3
| ~ spl23_126
| ~ spl23_140 ),
inference(forward_demodulation,[],[f934,f994]) ).
fof(f1446,plain,
( $false
| ~ spl23_126
| ~ spl23_140 ),
inference(forward_subsumption_resolution,[],[f1441,f200]) ).
fof(f1447,plain,
( ~ spl23_126
| ~ spl23_140 ),
inference(avatar_contradiction_clause,[],[f1446]) ).
fof(f1452,plain,
( e1 = e4
| ~ spl23_127
| ~ spl23_148 ),
inference(forward_demodulation,[],[f938,f1028]) ).
fof(f1455,plain,
( $false
| ~ spl23_127
| ~ spl23_148 ),
inference(forward_subsumption_resolution,[],[f1452,f199]) ).
fof(f1456,plain,
( ~ spl23_127
| ~ spl23_148 ),
inference(avatar_contradiction_clause,[],[f1455]) ).
fof(f1517,plain,
( e4 = op(e4,e0)
| ~ spl23_194 ),
inference(superposition,[],[f36,f1250]) ).
fof(f1518,plain,
( $false
| spl23_112
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1517,f854]) ).
fof(f1519,plain,
( spl23_112
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1518]) ).
fof(f1521,plain,
( e3 = e4
| ~ spl23_114
| ~ spl23_171 ),
inference(forward_demodulation,[],[f1129,f864]) ).
fof(f1522,plain,
( $false
| ~ spl23_114
| ~ spl23_171 ),
inference(forward_subsumption_resolution,[],[f1521,f196]) ).
fof(f1523,plain,
( ~ spl23_114
| ~ spl23_171 ),
inference(avatar_contradiction_clause,[],[f1522]) ).
fof(f1524,plain,
( e4 = op(e0,e4)
| ~ spl23_194 ),
inference(superposition,[],[f37,f1250]) ).
fof(f1525,plain,
( spl23_148
| ~ spl23_194 ),
inference(avatar_split_clause,[],[f1524,f1248,f1026]) ).
fof(f1527,plain,
( e4 = op(e1,e4)
| ~ spl23_195 ),
inference(superposition,[],[f37,f1254]) ).
fof(f1528,plain,
( e4 = op(e4,e1)
| ~ spl23_195 ),
inference(superposition,[],[f36,f1254]) ).
fof(f1529,plain,
( $false
| spl23_114
| ~ spl23_195 ),
inference(forward_subsumption_resolution,[],[f1528,f863]) ).
fof(f1530,plain,
( spl23_114
| ~ spl23_195 ),
inference(avatar_contradiction_clause,[],[f1529]) ).
fof(f1531,plain,
( spl23_174
| ~ spl23_195 ),
inference(avatar_split_clause,[],[f1527,f1252,f1140]) ).
fof(f1533,plain,
( e3 = e4
| ~ spl23_118
| ~ spl23_190 ),
inference(forward_demodulation,[],[f1223,f882]) ).
fof(f1534,plain,
( $false
| ~ spl23_118
| ~ spl23_190 ),
inference(forward_subsumption_resolution,[],[f1533,f196]) ).
fof(f1535,plain,
( ~ spl23_118
| ~ spl23_190 ),
inference(avatar_contradiction_clause,[],[f1534]) ).
fof(f1543,plain,
( e1 = e2
| ~ spl23_100
| ~ spl23_183 ),
inference(forward_demodulation,[],[f1191,f801]) ).
fof(f1546,plain,
( $false
| ~ spl23_100
| ~ spl23_183 ),
inference(forward_subsumption_resolution,[],[f1543,f201]) ).
fof(f1547,plain,
( ~ spl23_100
| ~ spl23_183 ),
inference(avatar_contradiction_clause,[],[f1546]) ).
fof(f1553,plain,
( e3 = op(e2,e3)
| ~ spl23_196 ),
inference(superposition,[],[f39,f1258]) ).
fof(f1557,plain,
( spl23_189
| ~ spl23_196 ),
inference(avatar_split_clause,[],[f1553,f1256,f1217]) ).
fof(f1574,plain,
( e2 = op(e2,e4)
| ~ spl23_198 ),
inference(superposition,[],[f40,f1266]) ).
fof(f1579,plain,
( e2 = e3
| ~ spl23_198 ),
inference(forward_demodulation,[],[f1574,f206]) ).
fof(f1582,plain,
( $false
| ~ spl23_198 ),
inference(forward_subsumption_resolution,[],[f1579,f198]) ).
fof(f1583,plain,
~ spl23_198,
inference(avatar_contradiction_clause,[],[f1582]) ).
fof(f1611,plain,
( e2 = e4
| ~ spl23_114
| ~ spl23_166 ),
inference(forward_demodulation,[],[f1107,f864]) ).
fof(f1614,plain,
( $false
| ~ spl23_114
| ~ spl23_166 ),
inference(forward_subsumption_resolution,[],[f1611,f197]) ).
fof(f1615,plain,
( ~ spl23_114
| ~ spl23_166 ),
inference(avatar_contradiction_clause,[],[f1614]) ).
fof(f1622,plain,
( e2 = e3
| ~ spl23_166
| ~ spl23_171 ),
inference(forward_demodulation,[],[f1107,f1129]) ).
fof(f1629,plain,
( $false
| ~ spl23_166
| ~ spl23_171 ),
inference(forward_subsumption_resolution,[],[f1622,f198]) ).
fof(f1630,plain,
( ~ spl23_166
| ~ spl23_171 ),
inference(avatar_contradiction_clause,[],[f1629]) ).
fof(f1655,plain,
( e3 = op(e3,e0)
| ~ spl23_194 ),
inference(superposition,[],[f38,f1250]) ).
fof(f1656,plain,
( e3 = op(e0,e3)
| ~ spl23_194 ),
inference(superposition,[],[f39,f1250]) ).
fof(f1658,plain,
( e2 = op(e0,e2)
| ~ spl23_194 ),
inference(superposition,[],[f41,f1250]) ).
fof(f1660,plain,
( e1 = op(e0,e1)
| ~ spl23_194 ),
inference(superposition,[],[f43,f1250]) ).
fof(f1663,plain,
( e1 = e2
| ~ spl23_131
| ~ spl23_194 ),
inference(forward_demodulation,[],[f1660,f956]) ).
fof(f1664,plain,
( e2 = e3
| ~ spl23_139
| ~ spl23_194 ),
inference(forward_demodulation,[],[f1658,f990]) ).
fof(f1665,plain,
( e3 = e4
| ~ spl23_147
| ~ spl23_194 ),
inference(forward_demodulation,[],[f1656,f1024]) ).
fof(f1666,plain,
( spl23_104
| ~ spl23_194 ),
inference(avatar_split_clause,[],[f1655,f1248,f817]) ).
fof(f1667,plain,
( $false
| ~ spl23_131
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1663,f201]) ).
fof(f1668,plain,
( ~ spl23_131
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1667]) ).
fof(f1669,plain,
( $false
| ~ spl23_139
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1664,f198]) ).
fof(f1670,plain,
( ~ spl23_139
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1669]) ).
fof(f1671,plain,
( $false
| ~ spl23_147
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1665,f196]) ).
fof(f1672,plain,
( ~ spl23_147
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1671]) ).
fof(f1674,plain,
( spl23_140
| ~ spl23_194 ),
inference(avatar_split_clause,[],[f1656,f1248,f992]) ).
fof(f1677,plain,
( e2 = e4
| ~ spl23_146
| ~ spl23_194 ),
inference(forward_demodulation,[],[f1658,f1020]) ).
fof(f1680,plain,
( e1 = e3
| ~ spl23_138
| ~ spl23_194 ),
inference(forward_demodulation,[],[f1660,f986]) ).
fof(f1681,plain,
( $false
| ~ spl23_146
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1677,f197]) ).
fof(f1682,plain,
( ~ spl23_146
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1681]) ).
fof(f1683,plain,
( $false
| ~ spl23_138
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1680,f200]) ).
fof(f1684,plain,
( ~ spl23_138
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1683]) ).
fof(f1695,plain,
( e0 = e1
| ~ spl23_80
| ~ spl23_194 ),
inference(forward_demodulation,[],[f1660,f711]) ).
fof(f1702,plain,
( $false
| ~ spl23_80
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f1695,f205]) ).
fof(f1703,plain,
( ~ spl23_80
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f1702]) ).
fof(f1714,plain,
( e1 = e4
| ~ spl23_116 ),
inference(superposition,[],[f207,f873]) ).
fof(f1718,plain,
( $false
| ~ spl23_116 ),
inference(forward_subsumption_resolution,[],[f1714,f199]) ).
fof(f1719,plain,
~ spl23_116,
inference(avatar_contradiction_clause,[],[f1718]) ).
fof(f1723,plain,
( e2 = e4
| ~ spl23_118
| ~ spl23_187 ),
inference(forward_demodulation,[],[f1209,f882]) ).
fof(f1729,plain,
( $false
| ~ spl23_118
| ~ spl23_187 ),
inference(forward_subsumption_resolution,[],[f1723,f197]) ).
fof(f1730,plain,
( ~ spl23_118
| ~ spl23_187 ),
inference(avatar_contradiction_clause,[],[f1729]) ).
fof(f1731,plain,
( e2 = e4
| ~ spl23_134
| ~ spl23_148 ),
inference(forward_demodulation,[],[f968,f1028]) ).
fof(f1733,plain,
( $false
| ~ spl23_134
| ~ spl23_148 ),
inference(forward_subsumption_resolution,[],[f1731,f197]) ).
fof(f1734,plain,
( ~ spl23_134
| ~ spl23_148 ),
inference(avatar_contradiction_clause,[],[f1733]) ).
fof(f1736,plain,
( e2 = e4
| ~ spl23_164
| ~ spl23_174 ),
inference(forward_demodulation,[],[f1098,f1142]) ).
fof(f1737,plain,
( $false
| ~ spl23_164
| ~ spl23_174 ),
inference(forward_subsumption_resolution,[],[f1736,f197]) ).
fof(f1738,plain,
( ~ spl23_164
| ~ spl23_174 ),
inference(avatar_contradiction_clause,[],[f1737]) ).
fof(f1765,plain,
( e1 = e3
| ~ spl23_104
| ~ spl23_129 ),
inference(superposition,[],[f947,f819]) ).
fof(f1769,plain,
( $false
| ~ spl23_104
| ~ spl23_129 ),
inference(forward_subsumption_resolution,[],[f1765,f200]) ).
fof(f1770,plain,
( ~ spl23_104
| ~ spl23_129 ),
inference(avatar_contradiction_clause,[],[f1769]) ).
fof(f1772,plain,
( e0 = e1
| ~ spl23_178
| ~ spl23_182 ),
inference(forward_demodulation,[],[f1186,f1168]) ).
fof(f1775,plain,
( $false
| ~ spl23_178
| ~ spl23_182 ),
inference(forward_subsumption_resolution,[],[f1772,f205]) ).
fof(f1776,plain,
( ~ spl23_178
| ~ spl23_182 ),
inference(avatar_contradiction_clause,[],[f1775]) ).
fof(f1786,plain,
( e0 = e3
| ~ spl23_104
| ~ spl23_122 ),
inference(forward_demodulation,[],[f917,f819]) ).
fof(f1787,plain,
( $false
| ~ spl23_104
| ~ spl23_122 ),
inference(forward_subsumption_resolution,[],[f1786,f203]) ).
fof(f1788,plain,
( ~ spl23_104
| ~ spl23_122 ),
inference(avatar_contradiction_clause,[],[f1787]) ).
fof(f1796,plain,
( e1 = e2
| ~ spl23_88
| ~ spl23_135 ),
inference(superposition,[],[f973,f747]) ).
fof(f1800,plain,
( $false
| ~ spl23_88
| ~ spl23_135 ),
inference(forward_subsumption_resolution,[],[f1796,f201]) ).
fof(f1801,plain,
( ~ spl23_88
| ~ spl23_135 ),
inference(avatar_contradiction_clause,[],[f1800]) ).
fof(f1804,plain,
( e2 = e3
| ~ spl23_133
| ~ spl23_140 ),
inference(superposition,[],[f994,f964]) ).
fof(f1808,plain,
( $false
| ~ spl23_133
| ~ spl23_140 ),
inference(forward_subsumption_resolution,[],[f1804,f198]) ).
fof(f1809,plain,
( ~ spl23_133
| ~ spl23_140 ),
inference(avatar_contradiction_clause,[],[f1808]) ).
fof(f1814,plain,
( e1 = e3
| ~ spl23_88
| ~ spl23_142 ),
inference(superposition,[],[f1003,f747]) ).
fof(f1818,plain,
( $false
| ~ spl23_88
| ~ spl23_142 ),
inference(forward_subsumption_resolution,[],[f1814,f200]) ).
fof(f1819,plain,
( ~ spl23_88
| ~ spl23_142 ),
inference(avatar_contradiction_clause,[],[f1818]) ).
fof(f1823,plain,
( e1 = e4
| ~ spl23_88
| ~ spl23_149 ),
inference(superposition,[],[f1033,f747]) ).
fof(f1827,plain,
( $false
| ~ spl23_88
| ~ spl23_149 ),
inference(forward_subsumption_resolution,[],[f1823,f199]) ).
fof(f1828,plain,
( ~ spl23_88
| ~ spl23_149 ),
inference(avatar_contradiction_clause,[],[f1827]) ).
fof(f1830,plain,
( e2 = e4
| ~ spl23_96
| ~ spl23_150 ),
inference(superposition,[],[f1037,f783]) ).
fof(f1834,plain,
( $false
| ~ spl23_96
| ~ spl23_150 ),
inference(forward_subsumption_resolution,[],[f1830,f197]) ).
fof(f1835,plain,
( ~ spl23_96
| ~ spl23_150 ),
inference(avatar_contradiction_clause,[],[f1834]) ).
fof(f1846,plain,
( e1 = e4
| ~ spl23_183
| ~ spl23_193 ),
inference(forward_demodulation,[],[f1191,f1237]) ).
fof(f1851,plain,
( $false
| ~ spl23_183
| ~ spl23_193 ),
inference(forward_subsumption_resolution,[],[f1846,f199]) ).
fof(f1852,plain,
( ~ spl23_183
| ~ spl23_193 ),
inference(avatar_contradiction_clause,[],[f1851]) ).
fof(f1862,plain,
( e1 = e3
| ~ spl23_92
| ~ spl23_168 ),
inference(forward_demodulation,[],[f765,f1116]) ).
fof(f1868,plain,
( $false
| ~ spl23_92
| ~ spl23_168 ),
inference(forward_subsumption_resolution,[],[f1862,f200]) ).
fof(f1869,plain,
( ~ spl23_92
| ~ spl23_168 ),
inference(avatar_contradiction_clause,[],[f1868]) ).
fof(f1871,plain,
( e3 = e4
| ~ spl23_167
| ~ spl23_172 ),
inference(forward_demodulation,[],[f1112,f1134]) ).
fof(f1878,plain,
( e2 = op(e1,e3)
| ~ spl23_46
| ~ spl23_183 ),
inference(forward_demodulation,[],[f537,f1191]) ).
fof(f1881,plain,
( $false
| ~ spl23_167
| ~ spl23_172 ),
inference(forward_subsumption_resolution,[],[f1871,f196]) ).
fof(f1882,plain,
( ~ spl23_167
| ~ spl23_172 ),
inference(avatar_contradiction_clause,[],[f1881]) ).
fof(f1886,plain,
( e2 = e4
| ~ spl23_46
| ~ spl23_173
| ~ spl23_183 ),
inference(forward_demodulation,[],[f1878,f1138]) ).
fof(f1887,plain,
( $false
| ~ spl23_46
| ~ spl23_173
| ~ spl23_183 ),
inference(forward_subsumption_resolution,[],[f1886,f197]) ).
fof(f1888,plain,
( ~ spl23_46
| ~ spl23_173
| ~ spl23_183 ),
inference(avatar_contradiction_clause,[],[f1887]) ).
fof(f1889,plain,
( e2 = e4
| ~ spl23_112
| ~ spl23_137 ),
inference(forward_demodulation,[],[f981,f855]) ).
fof(f1896,plain,
( $false
| ~ spl23_112
| ~ spl23_137 ),
inference(forward_subsumption_resolution,[],[f1889,f197]) ).
fof(f1897,plain,
( ~ spl23_112
| ~ spl23_137 ),
inference(avatar_contradiction_clause,[],[f1896]) ).
fof(f1898,plain,
( e1 = e2
| ~ spl23_92
| ~ spl23_163 ),
inference(forward_demodulation,[],[f765,f1094]) ).
fof(f1904,plain,
( $false
| ~ spl23_92
| ~ spl23_163 ),
inference(forward_subsumption_resolution,[],[f1898,f201]) ).
fof(f1905,plain,
( ~ spl23_92
| ~ spl23_163 ),
inference(avatar_contradiction_clause,[],[f1904]) ).
fof(f1907,plain,
( e2 = e3
| ~ spl23_162
| ~ spl23_167 ),
inference(forward_demodulation,[],[f1090,f1112]) ).
fof(f1908,plain,
( $false
| ~ spl23_162
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f1907,f198]) ).
fof(f1909,plain,
( ~ spl23_162
| ~ spl23_167 ),
inference(avatar_contradiction_clause,[],[f1908]) ).
fof(f1915,plain,
( e1 = e2
| ~ spl23_94
| ~ spl23_164 ),
inference(superposition,[],[f1098,f774]) ).
fof(f1919,plain,
( $false
| ~ spl23_94
| ~ spl23_164 ),
inference(forward_subsumption_resolution,[],[f1915,f201]) ).
fof(f1920,plain,
( ~ spl23_94
| ~ spl23_164 ),
inference(avatar_contradiction_clause,[],[f1919]) ).
fof(f1940,plain,
( e1 = e4
| ~ spl23_92
| ~ spl23_173 ),
inference(superposition,[],[f1138,f765]) ).
fof(f1947,plain,
( $false
| ~ spl23_92
| ~ spl23_173 ),
inference(forward_subsumption_resolution,[],[f1940,f199]) ).
fof(f1948,plain,
( ~ spl23_92
| ~ spl23_173 ),
inference(avatar_contradiction_clause,[],[f1947]) ).
fof(f1949,plain,
( e0 = e1
| ~ spl23_103
| ~ spl23_105 ),
inference(forward_demodulation,[],[f823,f814]) ).
fof(f1952,plain,
( $false
| ~ spl23_103
| ~ spl23_105 ),
inference(forward_subsumption_resolution,[],[f1949,f205]) ).
fof(f1953,plain,
( ~ spl23_103
| ~ spl23_105 ),
inference(avatar_contradiction_clause,[],[f1952]) ).
fof(f1954,plain,
( e0 = e3
| ~ spl23_108
| ~ spl23_177 ),
inference(forward_demodulation,[],[f1164,f837]) ).
fof(f1956,plain,
( $false
| ~ spl23_108
| ~ spl23_177 ),
inference(forward_subsumption_resolution,[],[f1954,f203]) ).
fof(f1957,plain,
( ~ spl23_108
| ~ spl23_177 ),
inference(avatar_contradiction_clause,[],[f1956]) ).
fof(f1973,plain,
( e0 = e4
| ~ spl23_177
| ~ spl23_191 ),
inference(forward_demodulation,[],[f1164,f1228]) ).
fof(f1978,plain,
( $false
| ~ spl23_177
| ~ spl23_191 ),
inference(forward_subsumption_resolution,[],[f1973,f202]) ).
fof(f1979,plain,
( ~ spl23_177
| ~ spl23_191 ),
inference(avatar_contradiction_clause,[],[f1978]) ).
fof(f1984,plain,
( e1 = e4
| ~ spl23_94
| ~ spl23_174 ),
inference(forward_demodulation,[],[f774,f1142]) ).
fof(f1986,plain,
( e0 = e2
| ~ spl23_178
| ~ spl23_186 ),
inference(forward_demodulation,[],[f1168,f1204]) ).
fof(f1990,plain,
( e2 = e3
| ~ spl23_187
| ~ spl23_190 ),
inference(forward_demodulation,[],[f1209,f1223]) ).
fof(f1996,plain,
( $false
| ~ spl23_94
| ~ spl23_174 ),
inference(forward_subsumption_resolution,[],[f1984,f199]) ).
fof(f1997,plain,
( ~ spl23_94
| ~ spl23_174 ),
inference(avatar_contradiction_clause,[],[f1996]) ).
fof(f1998,plain,
( $false
| ~ spl23_178
| ~ spl23_186 ),
inference(forward_subsumption_resolution,[],[f1986,f204]) ).
fof(f1999,plain,
( ~ spl23_178
| ~ spl23_186 ),
inference(avatar_contradiction_clause,[],[f1998]) ).
fof(f2002,plain,
( $false
| ~ spl23_187
| ~ spl23_190 ),
inference(forward_subsumption_resolution,[],[f1990,f198]) ).
fof(f2003,plain,
( ~ spl23_187
| ~ spl23_190 ),
inference(avatar_contradiction_clause,[],[f2002]) ).
fof(f2015,plain,
( e1 = e2
| ~ spl23_182
| ~ spl23_186 ),
inference(forward_demodulation,[],[f1186,f1204]) ).
fof(f2022,plain,
( $false
| ~ spl23_182
| ~ spl23_186 ),
inference(forward_subsumption_resolution,[],[f2015,f201]) ).
fof(f2023,plain,
( ~ spl23_182
| ~ spl23_186 ),
inference(avatar_contradiction_clause,[],[f2022]) ).
fof(f2027,plain,
( e2 = e4
| ~ spl23_98
| ~ spl23_175 ),
inference(forward_demodulation,[],[f792,f1147]) ).
fof(f2030,plain,
( e0 = e4
| ~ spl23_154
| ~ spl23_174 ),
inference(forward_demodulation,[],[f1054,f1142]) ).
fof(f2057,plain,
( $false
| ~ spl23_98
| ~ spl23_175 ),
inference(forward_subsumption_resolution,[],[f2027,f197]) ).
fof(f2058,plain,
( ~ spl23_98
| ~ spl23_175 ),
inference(avatar_contradiction_clause,[],[f2057]) ).
fof(f2059,plain,
( $false
| ~ spl23_154
| ~ spl23_174 ),
inference(forward_subsumption_resolution,[],[f2030,f202]) ).
fof(f2060,plain,
( ~ spl23_154
| ~ spl23_174 ),
inference(avatar_contradiction_clause,[],[f2059]) ).
fof(f2064,plain,
( e0 = e2
| ~ spl23_86
| ~ spl23_134 ),
inference(forward_demodulation,[],[f738,f968]) ).
fof(f2076,plain,
( $false
| ~ spl23_86
| ~ spl23_134 ),
inference(forward_subsumption_resolution,[],[f2064,f204]) ).
fof(f2077,plain,
( ~ spl23_86
| ~ spl23_134 ),
inference(avatar_contradiction_clause,[],[f2076]) ).
fof(f2082,plain,
( e2 = op(e3,e4)
| ~ spl23_50 ),
inference(forward_demodulation,[],[f556,f206]) ).
fof(f2085,plain,
( e1 = e2
| ~ spl23_127
| ~ spl23_134 ),
inference(forward_demodulation,[],[f938,f968]) ).
fof(f2103,plain,
( $false
| ~ spl23_50
| spl23_186 ),
inference(forward_subsumption_resolution,[],[f2082,f1203]) ).
fof(f2104,plain,
( ~ spl23_50
| spl23_186 ),
inference(avatar_contradiction_clause,[],[f2103]) ).
fof(f2106,plain,
( $false
| ~ spl23_127
| ~ spl23_134 ),
inference(forward_subsumption_resolution,[],[f2085,f201]) ).
fof(f2107,plain,
( ~ spl23_127
| ~ spl23_134 ),
inference(avatar_contradiction_clause,[],[f2106]) ).
fof(f2131,plain,
( e0 = e1
| ~ spl23_86
| ~ spl23_127 ),
inference(forward_demodulation,[],[f938,f738]) ).
fof(f2138,plain,
( $false
| ~ spl23_86
| ~ spl23_127 ),
inference(forward_subsumption_resolution,[],[f2131,f205]) ).
fof(f2139,plain,
( ~ spl23_86
| ~ spl23_127 ),
inference(avatar_contradiction_clause,[],[f2138]) ).
fof(f2147,plain,
( e0 = e3
| ~ spl23_106
| ~ spl23_156 ),
inference(forward_demodulation,[],[f1063,f828]) ).
fof(f2171,plain,
( $false
| ~ spl23_106
| ~ spl23_156 ),
inference(forward_subsumption_resolution,[],[f2147,f203]) ).
fof(f2172,plain,
( ~ spl23_106
| ~ spl23_156 ),
inference(avatar_contradiction_clause,[],[f2171]) ).
fof(f2217,plain,
( e2 = e4
| ~ spl23_163
| ~ spl23_173 ),
inference(forward_demodulation,[],[f1094,f1138]) ).
fof(f2224,plain,
( $false
| ~ spl23_163
| ~ spl23_173 ),
inference(forward_subsumption_resolution,[],[f2217,f197]) ).
fof(f2225,plain,
( ~ spl23_163
| ~ spl23_173 ),
inference(avatar_contradiction_clause,[],[f2224]) ).
fof(f2234,plain,
( e3 = e4
| ~ spl23_168
| ~ spl23_173 ),
inference(forward_demodulation,[],[f1116,f1138]) ).
fof(f2258,plain,
( $false
| ~ spl23_168
| ~ spl23_173 ),
inference(forward_subsumption_resolution,[],[f2234,f196]) ).
fof(f2259,plain,
( ~ spl23_168
| ~ spl23_173 ),
inference(avatar_contradiction_clause,[],[f2258]) ).
fof(f2297,plain,
( e2 = op(e2,e0)
| ~ spl23_194 ),
inference(superposition,[],[f40,f1250]) ).
fof(f2298,plain,
( e2 = op(e0,e2)
| ~ spl23_194 ),
inference(superposition,[],[f41,f1250]) ).
fof(f2314,plain,
( e2 = e3
| ~ spl23_104
| ~ spl23_136 ),
inference(superposition,[],[f977,f819]) ).
fof(f2318,plain,
( $false
| ~ spl23_104
| ~ spl23_136 ),
inference(forward_subsumption_resolution,[],[f2314,f198]) ).
fof(f2319,plain,
( ~ spl23_104
| ~ spl23_136 ),
inference(avatar_contradiction_clause,[],[f2318]) ).
fof(f2324,plain,
( e3 != op(e0,e3)
| spl23_14
| ~ spl23_104 ),
inference(forward_demodulation,[],[f380,f819]) ).
fof(f2325,plain,
( $false
| spl23_14
| ~ spl23_104
| ~ spl23_140 ),
inference(forward_subsumption_resolution,[],[f2324,f994]) ).
fof(f2326,plain,
( spl23_14
| ~ spl23_104
| ~ spl23_140 ),
inference(avatar_contradiction_clause,[],[f2325]) ).
fof(f2328,plain,
( e4 != op(e4,e0)
| spl23_16
| ~ spl23_148 ),
inference(forward_demodulation,[],[f389,f1028]) ).
fof(f2330,plain,
( e4 != op(e0,e4)
| spl23_18
| ~ spl23_112 ),
inference(forward_demodulation,[],[f399,f855]) ).
fof(f2331,plain,
( $false
| spl23_16
| ~ spl23_112
| ~ spl23_148 ),
inference(forward_subsumption_resolution,[],[f2328,f855]) ).
fof(f2332,plain,
( spl23_16
| ~ spl23_112
| ~ spl23_148 ),
inference(avatar_contradiction_clause,[],[f2331]) ).
fof(f2333,plain,
( $false
| spl23_18
| ~ spl23_112
| ~ spl23_148 ),
inference(forward_subsumption_resolution,[],[f2330,f1028]) ).
fof(f2334,plain,
( spl23_18
| ~ spl23_112
| ~ spl23_148 ),
inference(avatar_contradiction_clause,[],[f2333]) ).
fof(f2346,plain,
( e2 != op(e1,e4)
| spl23_74 ),
inference(forward_demodulation,[],[f675,f207]) ).
fof(f2350,plain,
( $false
| spl23_74
| ~ spl23_164 ),
inference(forward_subsumption_resolution,[],[f2346,f1098]) ).
fof(f2351,plain,
( spl23_74
| ~ spl23_164 ),
inference(avatar_contradiction_clause,[],[f2350]) ).
fof(f2361,plain,
( e1 != op(e3,e4)
| spl23_71
| ~ spl23_171 ),
inference(forward_demodulation,[],[f660,f1129]) ).
fof(f2364,plain,
( $false
| spl23_71
| ~ spl23_171
| ~ spl23_182 ),
inference(forward_subsumption_resolution,[],[f2361,f1186]) ).
fof(f2365,plain,
( spl23_71
| ~ spl23_171
| ~ spl23_182 ),
inference(avatar_contradiction_clause,[],[f2364]) ).
fof(f2367,plain,
( e2 != op(e2,e0)
| spl23_8
| ~ spl23_132 ),
inference(forward_demodulation,[],[f351,f960]) ).
fof(f2369,plain,
( e2 != op(e0,e2)
| spl23_10
| ~ spl23_96 ),
inference(forward_demodulation,[],[f361,f783]) ).
fof(f2372,plain,
( $false
| spl23_8
| ~ spl23_96
| ~ spl23_132 ),
inference(forward_subsumption_resolution,[],[f2367,f783]) ).
fof(f2373,plain,
( spl23_8
| ~ spl23_96
| ~ spl23_132 ),
inference(avatar_contradiction_clause,[],[f2372]) ).
fof(f2374,plain,
( $false
| spl23_10
| ~ spl23_96
| ~ spl23_132 ),
inference(forward_subsumption_resolution,[],[f2369,f960]) ).
fof(f2375,plain,
( spl23_10
| ~ spl23_96
| ~ spl23_132 ),
inference(avatar_contradiction_clause,[],[f2374]) ).
fof(f2380,plain,
( e3 = op(e1,e4)
| ~ spl23_65
| ~ spl23_182 ),
inference(forward_demodulation,[],[f631,f1186]) ).
fof(f2383,plain,
( spl23_169
| ~ spl23_65
| ~ spl23_182 ),
inference(avatar_split_clause,[],[f2380,f1184,f629,f1118]) ).
fof(f2386,plain,
( e4 = op(e2,e3)
| ~ spl23_77
| ~ spl23_187 ),
inference(forward_demodulation,[],[f691,f1209]) ).
fof(f2388,plain,
( $false
| ~ spl23_77
| ~ spl23_187
| spl23_193 ),
inference(forward_subsumption_resolution,[],[f2386,f1236]) ).
fof(f2389,plain,
( ~ spl23_77
| ~ spl23_187
| spl23_193 ),
inference(avatar_contradiction_clause,[],[f2388]) ).
fof(f2396,plain,
( e3 != op(e3,e0)
| spl23_12
| ~ spl23_140 ),
inference(superposition,[],[f370,f994]) ).
fof(f2398,plain,
( $false
| spl23_12
| ~ spl23_104
| ~ spl23_140 ),
inference(forward_subsumption_resolution,[],[f2396,f819]) ).
fof(f2399,plain,
( spl23_12
| ~ spl23_104
| ~ spl23_140 ),
inference(avatar_contradiction_clause,[],[f2398]) ).
fof(f2417,plain,
( e4 != op(e2,e1)
| spl23_33
| ~ spl23_164 ),
inference(forward_demodulation,[],[f472,f1098]) ).
fof(f2425,plain,
( e1 = e2
| ~ spl23_160
| ~ spl23_165 ),
inference(superposition,[],[f1103,f1081]) ).
fof(f2431,plain,
( $false
| ~ spl23_160
| ~ spl23_165 ),
inference(forward_subsumption_resolution,[],[f2425,f201]) ).
fof(f2432,plain,
( ~ spl23_160
| ~ spl23_165 ),
inference(avatar_contradiction_clause,[],[f2431]) ).
fof(f2442,plain,
( spl23_132
| ~ spl23_194 ),
inference(avatar_split_clause,[],[f2298,f1248,f958]) ).
fof(f2445,plain,
( $false
| spl23_96
| ~ spl23_194 ),
inference(forward_subsumption_resolution,[],[f2297,f782]) ).
fof(f2446,plain,
( spl23_96
| ~ spl23_194 ),
inference(avatar_contradiction_clause,[],[f2445]) ).
fof(f2463,plain,
( e1 != op(e2,e3)
| spl23_56
| ~ spl23_165 ),
inference(forward_demodulation,[],[f585,f1103]) ).
fof(f2476,plain,
( $false
| spl23_56
| ~ spl23_165
| ~ spl23_183 ),
inference(forward_subsumption_resolution,[],[f2463,f1191]) ).
fof(f2477,plain,
( spl23_56
| ~ spl23_165
| ~ spl23_183 ),
inference(avatar_contradiction_clause,[],[f2476]) ).
fof(f2527,plain,
( e3 = e4
| ~ spl23_108
| ~ spl23_191 ),
inference(superposition,[],[f1228,f837]) ).
fof(f2531,plain,
( $false
| ~ spl23_108
| ~ spl23_191 ),
inference(forward_subsumption_resolution,[],[f2527,f196]) ).
fof(f2532,plain,
( ~ spl23_108
| ~ spl23_191 ),
inference(avatar_contradiction_clause,[],[f2531]) ).
fof(f2537,plain,
( e2 != op(e4,e3)
| spl23_59
| ~ spl23_191 ),
inference(forward_demodulation,[],[f600,f1228]) ).
fof(f2540,plain,
( $false
| spl23_59
| ~ spl23_187
| ~ spl23_191 ),
inference(forward_subsumption_resolution,[],[f2537,f1209]) ).
fof(f2541,plain,
( spl23_59
| ~ spl23_187
| ~ spl23_191 ),
inference(avatar_contradiction_clause,[],[f2540]) ).
fof(f2543,plain,
( e1 = op(e3,e2)
| ~ spl23_26
| ~ spl23_167 ),
inference(forward_demodulation,[],[f439,f1112]) ).
fof(f2548,plain,
( e1 = e4
| ~ spl23_26
| ~ spl23_167
| ~ spl23_191 ),
inference(forward_demodulation,[],[f2543,f1228]) ).
fof(f2550,plain,
( $false
| ~ spl23_26
| ~ spl23_167
| ~ spl23_191 ),
inference(forward_subsumption_resolution,[],[f2548,f199]) ).
fof(f2551,plain,
( ~ spl23_26
| ~ spl23_167
| ~ spl23_191 ),
inference(avatar_contradiction_clause,[],[f2550]) ).
fof(f2554,plain,
( e1 != op(e4,e2)
| spl23_40
| ~ spl23_175 ),
inference(forward_demodulation,[],[f506,f1147]) ).
fof(f2557,plain,
( $false
| spl23_40
| ~ spl23_175 ),
inference(forward_subsumption_resolution,[],[f2554,f207]) ).
fof(f2558,plain,
( spl23_40
| ~ spl23_175 ),
inference(avatar_contradiction_clause,[],[f2557]) ).
fof(f2562,plain,
( e1 = op(e4,e3)
| ~ spl23_30
| ~ spl23_173 ),
inference(forward_demodulation,[],[f458,f1138]) ).
fof(f2567,plain,
( $false
| ~ spl23_30
| ~ spl23_173
| spl23_184 ),
inference(forward_subsumption_resolution,[],[f2562,f1194]) ).
fof(f2568,plain,
( ~ spl23_30
| ~ spl23_173
| spl23_184 ),
inference(avatar_contradiction_clause,[],[f2567]) ).
fof(f2572,plain,
( ~ spl23_175
| spl23_33
| ~ spl23_164 ),
inference(avatar_split_clause,[],[f2417,f1096,f470,f1145]) ).
fof(f2593,plain,
( e2 = op(e2,e3)
| ~ spl23_59
| ~ spl23_185 ),
inference(forward_demodulation,[],[f599,f1200]) ).
fof(f2635,plain,
( $false
| ~ spl23_59
| spl23_100
| ~ spl23_185 ),
inference(forward_subsumption_resolution,[],[f2593,f800]) ).
fof(f2636,plain,
( ~ spl23_59
| spl23_100
| ~ spl23_185 ),
inference(avatar_contradiction_clause,[],[f2635]) ).
fof(f2722,plain,
( e1 = op(e1,e3)
| ~ spl23_197 ),
inference(superposition,[],[f42,f1262]) ).
fof(f2729,plain,
( $false
| spl23_92
| ~ spl23_197 ),
inference(forward_subsumption_resolution,[],[f2722,f764]) ).
fof(f2730,plain,
( spl23_92
| ~ spl23_197 ),
inference(avatar_contradiction_clause,[],[f2729]) ).
cnf(s3,plain,
~ spl23_1,
inference(sat_conversion,[],[f324]) ).
cnf(s6,plain,
( ~ spl23_3
| ~ spl23_6 ),
inference(sat_conversion,[],[f343]) ).
cnf(s7,plain,
( ~ spl23_7
| ~ spl23_8 ),
inference(sat_conversion,[],[f352]) ).
cnf(s10,plain,
( ~ spl23_11
| ~ spl23_12 ),
inference(sat_conversion,[],[f371]) ).
cnf(s13,plain,
( ~ spl23_15
| ~ spl23_16 ),
inference(sat_conversion,[],[f390]) ).
cnf(s18,plain,
( ~ spl23_6
| ~ spl23_19 ),
inference(sat_conversion,[],[f415]) ).
cnf(s21,plain,
~ spl23_22,
inference(sat_conversion,[],[f426]) ).
cnf(s23,plain,
( ~ spl23_24
| spl23_26 ),
inference(sat_conversion,[],[f440]) ).
cnf(s26,plain,
( ~ spl23_28
| spl23_30 ),
inference(sat_conversion,[],[f459]) ).
cnf(s28,plain,
( ~ spl23_32
| ~ spl23_33 ),
inference(sat_conversion,[],[f473]) ).
cnf(s33,plain,
( ~ spl23_10
| ~ spl23_36 ),
inference(sat_conversion,[],[f498]) ).
cnf(s34,plain,
( ~ spl23_39
| ~ spl23_40 ),
inference(sat_conversion,[],[f507]) ).
cnf(s39,plain,
~ spl23_42,
inference(sat_conversion,[],[f524]) ).
cnf(s41,plain,
( ~ spl23_44
| spl23_46 ),
inference(sat_conversion,[],[f538]) ).
cnf(s44,plain,
( ~ spl23_48
| spl23_50 ),
inference(sat_conversion,[],[f557]) ).
cnf(s48,plain,
( ~ spl23_14
| ~ spl23_52 ),
inference(sat_conversion,[],[f577]) ).
cnf(s49,plain,
( ~ spl23_55
| ~ spl23_56 ),
inference(sat_conversion,[],[f586]) ).
cnf(s52,plain,
( ~ spl23_58
| ~ spl23_59 ),
inference(sat_conversion,[],[f601]) ).
cnf(s57,plain,
~ spl23_61,
inference(sat_conversion,[],[f618]) ).
cnf(s59,plain,
( ~ spl23_63
| spl23_65 ),
inference(sat_conversion,[],[f632]) ).
cnf(s63,plain,
( ~ spl23_18
| ~ spl23_67 ),
inference(sat_conversion,[],[f652]) ).
cnf(s64,plain,
( ~ spl23_70
| ~ spl23_71 ),
inference(sat_conversion,[],[f661]) ).
cnf(s67,plain,
( ~ spl23_73
| ~ spl23_74 ),
inference(sat_conversion,[],[f676]) ).
cnf(s71,plain,
( spl23_1
| spl23_3
| spl23_7
| spl23_11
| spl23_15
| spl23_19
| spl23_22
| spl23_24
| spl23_28
| spl23_32
| spl23_36
| spl23_39
| spl23_42
| spl23_44
| spl23_48
| spl23_52
| spl23_55
| spl23_58
| spl23_61
| spl23_63
| spl23_67
| spl23_70
| spl23_73
| spl23_77 ),
inference(sat_conversion,[],[f692]) ).
cnf(s79,plain,
( ~ spl23_79
| spl23_80 ),
inference(sat_conversion,[],[f712]) ).
cnf(s83,plain,
( ~ spl23_87
| spl23_88 ),
inference(sat_conversion,[],[f748]) ).
cnf(s84,plain,
( ~ spl23_89
| spl23_90 ),
inference(sat_conversion,[],[f757]) ).
cnf(s90,plain,
( ~ spl23_101
| spl23_102 ),
inference(sat_conversion,[],[f811]) ).
cnf(s92,plain,
( ~ spl23_105
| spl23_106 ),
inference(sat_conversion,[],[f829]) ).
cnf(s93,plain,
( ~ spl23_107
| spl23_108 ),
inference(sat_conversion,[],[f838]) ).
cnf(s94,plain,
( ~ spl23_109
| spl23_110 ),
inference(sat_conversion,[],[f847]) ).
cnf(s95,plain,
( ~ spl23_111
| spl23_112 ),
inference(sat_conversion,[],[f856]) ).
cnf(s97,plain,
( ~ spl23_115
| spl23_116 ),
inference(sat_conversion,[],[f874]) ).
cnf(s101,plain,
( spl23_79
| spl23_124
| spl23_125
| spl23_126
| spl23_127 ),
inference(sat_conversion,[],[f939]) ).
cnf(s113,plain,
( spl23_89
| spl23_135
| spl23_162
| spl23_163
| spl23_164 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s114,plain,
( spl23_89
| spl23_98
| spl23_131
| spl23_165
| spl23_166 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s115,plain,
( spl23_91
| spl23_142
| spl23_167
| spl23_168
| spl23_169 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s116,plain,
( spl23_91
| spl23_106
| spl23_138
| spl23_170
| spl23_171 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s117,plain,
( spl23_93
| spl23_149
| spl23_172
| spl23_173
| spl23_174 ),
inference(sat_conversion,[],[f1143]) ).
cnf(s119,plain,
( spl23_103
| spl23_122
| spl23_156
| spl23_177
| spl23_178 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s121,plain,
( spl23_105
| spl23_129
| spl23_160
| spl23_181
| spl23_182 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s122,plain,
( spl23_92
| spl23_105
| spl23_126
| spl23_183
| spl23_184 ),
inference(sat_conversion,[],[f1196]) ).
cnf(s123,plain,
( spl23_107
| spl23_136
| spl23_165
| spl23_185
| spl23_186 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s124,plain,
( spl23_100
| spl23_107
| spl23_133
| spl23_163
| spl23_187 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s128,plain,
( spl23_109
| spl23_118
| spl23_147
| spl23_173
| spl23_193 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s129,plain,
( spl23_194
| spl23_195
| spl23_196
| spl23_197
| spl23_198 ),
inference(sat_conversion,[],[f1267]) ).
cnf(s153,plain,
spl23_87,
inference(sat_conversion,[],[f1299]) ).
cnf(s154,plain,
~ spl23_113,
inference(sat_conversion,[],[f1300]) ).
cnf(s155,plain,
~ spl23_184,
inference(sat_conversion,[],[f1301]) ).
cnf(s158,plain,
~ spl23_189,
inference(sat_conversion,[],[f1304]) ).
cnf(s159,plain,
~ spl23_99,
inference(sat_conversion,[],[f1305]) ).
cnf(s160,plain,
~ spl23_170,
inference(sat_conversion,[],[f1306]) ).
cnf(s162,plain,
~ spl23_117,
inference(sat_conversion,[],[f1308]) ).
cnf(s163,plain,
~ spl23_110,
inference(sat_conversion,[],[f1309]) ).
cnf(s164,plain,
~ spl23_169,
inference(sat_conversion,[],[f1310]) ).
cnf(s166,plain,
~ spl23_181,
inference(sat_conversion,[],[f1312]) ).
cnf(s167,plain,
~ spl23_97,
inference(sat_conversion,[],[f1313]) ).
cnf(s168,plain,
~ spl23_90,
inference(sat_conversion,[],[f1314]) ).
cnf(s169,plain,
~ spl23_125,
inference(sat_conversion,[],[f1315]) ).
cnf(s172,plain,
( spl23_97
| spl23_128
| spl23_159
| spl23_183 ),
inference(sat_conversion,[],[f1334]) ).
cnf(s175,plain,
( spl23_99
| spl23_108
| spl23_139
| spl23_167 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s176,plain,
( spl23_101
| spl23_150
| spl23_175
| spl23_193 ),
inference(sat_conversion,[],[f1338]) ).
cnf(s177,plain,
( spl23_101
| spl23_146
| spl23_172
| spl23_191 ),
inference(sat_conversion,[],[f1339]) ).
cnf(s179,plain,
( spl23_86
| spl23_111
| spl23_154
| spl23_178 ),
inference(sat_conversion,[],[f1341]) ).
cnf(s180,plain,
( spl23_94
| spl23_113
| spl23_127
| spl23_182 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s181,plain,
( spl23_115
| spl23_137
| spl23_166
| spl23_187 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s182,plain,
( spl23_115
| spl23_134
| spl23_164
| spl23_186 ),
inference(sat_conversion,[],[f1344]) ).
cnf(s183,plain,
( spl23_117
| spl23_144
| spl23_171
| spl23_190 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s186,plain,
~ spl23_102,
inference(sat_conversion,[],[f1366]) ).
cnf(s187,plain,
( ~ spl23_96
| ~ spl23_128 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s188,plain,
( ~ spl23_112
| ~ spl23_144 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s189,plain,
( ~ spl23_98
| ~ spl23_159 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s191,plain,
( ~ spl23_87
| ~ spl23_91 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s193,plain,
( ~ spl23_87
| ~ spl23_93 ),
inference(sat_conversion,[],[f1393]) ).
cnf(s198,plain,
( ~ spl23_106
| ~ spl23_160 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s199,plain,
( spl23_6
| ~ spl23_88
| ~ spl23_124 ),
inference(sat_conversion,[],[f1423]) ).
cnf(s205,plain,
( ~ spl23_126
| ~ spl23_140 ),
inference(sat_conversion,[],[f1447]) ).
cnf(s207,plain,
( ~ spl23_127
| ~ spl23_148 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s215,plain,
( spl23_112
| ~ spl23_194 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s216,plain,
( ~ spl23_114
| ~ spl23_171 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s217,plain,
( spl23_148
| ~ spl23_194 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s218,plain,
( spl23_114
| ~ spl23_195 ),
inference(sat_conversion,[],[f1530]) ).
cnf(s219,plain,
( spl23_174
| ~ spl23_195 ),
inference(sat_conversion,[],[f1531]) ).
cnf(s220,plain,
( ~ spl23_118
| ~ spl23_190 ),
inference(sat_conversion,[],[f1535]) ).
cnf(s223,plain,
( ~ spl23_100
| ~ spl23_183 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s224,plain,
( spl23_189
| ~ spl23_196 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s230,plain,
~ spl23_198,
inference(sat_conversion,[],[f1583]) ).
cnf(s234,plain,
( ~ spl23_114
| ~ spl23_166 ),
inference(sat_conversion,[],[f1615]) ).
cnf(s236,plain,
( ~ spl23_166
| ~ spl23_171 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s240,plain,
( spl23_104
| ~ spl23_194 ),
inference(sat_conversion,[],[f1666]) ).
cnf(s241,plain,
( ~ spl23_131
| ~ spl23_194 ),
inference(sat_conversion,[],[f1668]) ).
cnf(s242,plain,
( ~ spl23_139
| ~ spl23_194 ),
inference(sat_conversion,[],[f1670]) ).
cnf(s243,plain,
( ~ spl23_147
| ~ spl23_194 ),
inference(sat_conversion,[],[f1672]) ).
cnf(s244,plain,
( spl23_140
| ~ spl23_194 ),
inference(sat_conversion,[],[f1674]) ).
cnf(s245,plain,
( ~ spl23_146
| ~ spl23_194 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s246,plain,
( ~ spl23_138
| ~ spl23_194 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s248,plain,
( ~ spl23_80
| ~ spl23_194 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s250,plain,
~ spl23_116,
inference(sat_conversion,[],[f1719]) ).
cnf(s252,plain,
( ~ spl23_118
| ~ spl23_187 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s253,plain,
( ~ spl23_134
| ~ spl23_148 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s254,plain,
( ~ spl23_164
| ~ spl23_174 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s260,plain,
( ~ spl23_104
| ~ spl23_129 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s261,plain,
( ~ spl23_178
| ~ spl23_182 ),
inference(sat_conversion,[],[f1776]) ).
cnf(s264,plain,
( ~ spl23_104
| ~ spl23_122 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s266,plain,
( ~ spl23_88
| ~ spl23_135 ),
inference(sat_conversion,[],[f1801]) ).
cnf(s268,plain,
( ~ spl23_133
| ~ spl23_140 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s270,plain,
( ~ spl23_88
| ~ spl23_142 ),
inference(sat_conversion,[],[f1819]) ).
cnf(s272,plain,
( ~ spl23_88
| ~ spl23_149 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s274,plain,
( ~ spl23_96
| ~ spl23_150 ),
inference(sat_conversion,[],[f1835]) ).
cnf(s277,plain,
( ~ spl23_183
| ~ spl23_193 ),
inference(sat_conversion,[],[f1852]) ).
cnf(s279,plain,
( ~ spl23_92
| ~ spl23_168 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s280,plain,
( ~ spl23_167
| ~ spl23_172 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s282,plain,
( ~ spl23_46
| ~ spl23_173
| ~ spl23_183 ),
inference(sat_conversion,[],[f1888]) ).
cnf(s283,plain,
( ~ spl23_112
| ~ spl23_137 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s284,plain,
( ~ spl23_92
| ~ spl23_163 ),
inference(sat_conversion,[],[f1905]) ).
cnf(s285,plain,
( ~ spl23_162
| ~ spl23_167 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s287,plain,
( ~ spl23_94
| ~ spl23_164 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s291,plain,
( ~ spl23_92
| ~ spl23_173 ),
inference(sat_conversion,[],[f1948]) ).
cnf(s292,plain,
( ~ spl23_103
| ~ spl23_105 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s293,plain,
( ~ spl23_108
| ~ spl23_177 ),
inference(sat_conversion,[],[f1957]) ).
cnf(s300,plain,
( ~ spl23_177
| ~ spl23_191 ),
inference(sat_conversion,[],[f1979]) ).
cnf(s302,plain,
( ~ spl23_94
| ~ spl23_174 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s303,plain,
( ~ spl23_178
| ~ spl23_186 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s305,plain,
( ~ spl23_187
| ~ spl23_190 ),
inference(sat_conversion,[],[f2003]) ).
cnf(s311,plain,
( ~ spl23_182
| ~ spl23_186 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s313,plain,
( ~ spl23_98
| ~ spl23_175 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s314,plain,
( ~ spl23_154
| ~ spl23_174 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s316,plain,
( ~ spl23_86
| ~ spl23_134 ),
inference(sat_conversion,[],[f2077]) ).
cnf(s318,plain,
( ~ spl23_50
| spl23_186 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s319,plain,
( ~ spl23_127
| ~ spl23_134 ),
inference(sat_conversion,[],[f2107]) ).
cnf(s325,plain,
( ~ spl23_86
| ~ spl23_127 ),
inference(sat_conversion,[],[f2139]) ).
cnf(s327,plain,
( ~ spl23_106
| ~ spl23_156 ),
inference(sat_conversion,[],[f2172]) ).
cnf(s337,plain,
( ~ spl23_163
| ~ spl23_173 ),
inference(sat_conversion,[],[f2225]) ).
cnf(s340,plain,
( ~ spl23_168
| ~ spl23_173 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s350,plain,
( ~ spl23_104
| ~ spl23_136 ),
inference(sat_conversion,[],[f2319]) ).
cnf(s351,plain,
( spl23_14
| ~ spl23_104
| ~ spl23_140 ),
inference(sat_conversion,[],[f2326]) ).
cnf(s352,plain,
( spl23_16
| ~ spl23_112
| ~ spl23_148 ),
inference(sat_conversion,[],[f2332]) ).
cnf(s353,plain,
( spl23_18
| ~ spl23_112
| ~ spl23_148 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s356,plain,
( spl23_74
| ~ spl23_164 ),
inference(sat_conversion,[],[f2351]) ).
cnf(s359,plain,
( spl23_71
| ~ spl23_171
| ~ spl23_182 ),
inference(sat_conversion,[],[f2365]) ).
cnf(s361,plain,
( spl23_8
| ~ spl23_96
| ~ spl23_132 ),
inference(sat_conversion,[],[f2373]) ).
cnf(s362,plain,
( spl23_10
| ~ spl23_96
| ~ spl23_132 ),
inference(sat_conversion,[],[f2375]) ).
cnf(s364,plain,
( ~ spl23_65
| spl23_169
| ~ spl23_182 ),
inference(sat_conversion,[],[f2383]) ).
cnf(s365,plain,
( ~ spl23_77
| ~ spl23_187
| spl23_193 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s366,plain,
( spl23_12
| ~ spl23_104
| ~ spl23_140 ),
inference(sat_conversion,[],[f2399]) ).
cnf(s371,plain,
( ~ spl23_160
| ~ spl23_165 ),
inference(sat_conversion,[],[f2432]) ).
cnf(s373,plain,
( spl23_132
| ~ spl23_194 ),
inference(sat_conversion,[],[f2442]) ).
cnf(s374,plain,
( spl23_96
| ~ spl23_194 ),
inference(sat_conversion,[],[f2446]) ).
cnf(s379,plain,
( spl23_56
| ~ spl23_165
| ~ spl23_183 ),
inference(sat_conversion,[],[f2477]) ).
cnf(s386,plain,
( ~ spl23_108
| ~ spl23_191 ),
inference(sat_conversion,[],[f2532]) ).
cnf(s387,plain,
( spl23_59
| ~ spl23_187
| ~ spl23_191 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s389,plain,
( ~ spl23_26
| ~ spl23_167
| ~ spl23_191 ),
inference(sat_conversion,[],[f2551]) ).
cnf(s390,plain,
( spl23_40
| ~ spl23_175 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s393,plain,
( ~ spl23_30
| ~ spl23_173
| spl23_184 ),
inference(sat_conversion,[],[f2568]) ).
cnf(s394,plain,
( spl23_33
| ~ spl23_164
| ~ spl23_175 ),
inference(sat_conversion,[],[f2572]) ).
cnf(s402,plain,
( ~ spl23_59
| spl23_100
| ~ spl23_185 ),
inference(sat_conversion,[],[f2636]) ).
cnf(s418,plain,
( spl23_92
| ~ spl23_197 ),
inference(sat_conversion,[],[f2730]) ).
cnf(s421,plain,
~ spl23_196,
inference(rat,[],[s224,s158]) ).
cnf(s423,plain,
~ spl23_93,
inference(rat,[],[s193,s153]) ).
cnf(s424,plain,
~ spl23_91,
inference(rat,[],[s191,s153]) ).
cnf(s439,plain,
( spl23_194
| spl23_195
| spl23_197 ),
inference(rat,[],[s129,s230,s421]) ).
cnf(s442,plain,
( spl23_92
| spl23_105
| spl23_126
| spl23_183 ),
inference(rat,[],[s122,s155]) ).
cnf(s443,plain,
( spl23_105
| spl23_129
| spl23_160
| spl23_182 ),
inference(rat,[],[s121,s166]) ).
cnf(s445,plain,
( spl23_149
| spl23_172
| spl23_173
| spl23_174 ),
inference(rat,[],[s117,s423]) ).
cnf(s446,plain,
( spl23_106
| spl23_138
| spl23_171 ),
inference(rat,[],[s116,s160,s424]) ).
cnf(s447,plain,
( spl23_142
| spl23_167
| spl23_168 ),
inference(rat,[],[s115,s164,s424]) ).
cnf(s453,plain,
( spl23_79
| spl23_124
| spl23_126
| spl23_127 ),
inference(rat,[],[s101,s169]) ).
cnf(s454,plain,
~ spl23_115,
inference(rat,[],[s97,s250]) ).
cnf(s455,plain,
~ spl23_109,
inference(rat,[],[s94,s163]) ).
cnf(s456,plain,
~ spl23_101,
inference(rat,[],[s90,s186]) ).
cnf(s457,plain,
~ spl23_89,
inference(rat,[],[s84,s168]) ).
cnf(s458,plain,
spl23_88,
inference(rat,[],[s83,s153]) ).
cnf(s459,plain,
~ spl23_149,
inference(rat,[],[s272,s458]) ).
cnf(s460,plain,
~ spl23_142,
inference(rat,[],[s270,s458]) ).
cnf(s461,plain,
~ spl23_135,
inference(rat,[],[s266,s458]) ).
cnf(s463,plain,
( ~ spl23_194
| spl23_8 ),
inference(rat,[],[s361,s373,s374]) ).
cnf(s464,plain,
~ spl23_92,
inference(rat,[],[s254,s445,s113,s280,s285,s447,s279,s284,s291,s459,s457,s461,s460]) ).
cnf(s465,plain,
~ spl23_197,
inference(rat,[],[s418,s464]) ).
cnf(s466,plain,
( ~ spl23_134
| spl23_111
| ~ spl23_174 ),
inference(rat,[],[s261,s179,s180,s316,s319,s314,s302,s154]) ).
cnf(s467,plain,
( spl23_111
| ~ spl23_174 ),
inference(rat,[],[s325,s179,s180,s303,s311,s182,s466,s314,s302,s254,s154,s454]) ).
cnf(s468,plain,
~ spl23_195,
inference(rat,[],[s305,s183,s181,s188,s283,s95,s467,s216,s234,s218,s219,s162,s454]) ).
cnf(s469,plain,
spl23_194,
inference(rat,[],[s439,s465,s468]) ).
cnf(s470,plain,
spl23_96,
inference(rat,[],[s374,s469]) ).
cnf(s471,plain,
spl23_132,
inference(rat,[],[s373,s469]) ).
cnf(s472,plain,
~ spl23_80,
inference(rat,[],[s248,s469]) ).
cnf(s473,plain,
~ spl23_138,
inference(rat,[],[s246,s469]) ).
cnf(s474,plain,
~ spl23_146,
inference(rat,[],[s245,s469]) ).
cnf(s475,plain,
spl23_140,
inference(rat,[],[s244,s469]) ).
cnf(s476,plain,
~ spl23_147,
inference(rat,[],[s243,s469]) ).
cnf(s477,plain,
~ spl23_139,
inference(rat,[],[s242,s469]) ).
cnf(s478,plain,
~ spl23_131,
inference(rat,[],[s241,s469]) ).
cnf(s479,plain,
spl23_104,
inference(rat,[],[s240,s469]) ).
cnf(s480,plain,
spl23_148,
inference(rat,[],[s217,s469]) ).
cnf(s481,plain,
spl23_112,
inference(rat,[],[s215,s469]) ).
cnf(s482,plain,
spl23_8,
inference(rat,[],[s463,s469]) ).
cnf(s484,plain,
~ spl23_150,
inference(rat,[],[s274,s470]) ).
cnf(s485,plain,
~ spl23_128,
inference(rat,[],[s187,s470]) ).
cnf(s487,plain,
spl23_10,
inference(rat,[],[s362,s470,s471]) ).
cnf(s488,plain,
~ spl23_79,
inference(rat,[],[s79,s472]) ).
cnf(s489,plain,
~ spl23_133,
inference(rat,[],[s268,s475]) ).
cnf(s491,plain,
~ spl23_126,
inference(rat,[],[s205,s475]) ).
cnf(s492,plain,
spl23_12,
inference(rat,[],[s366,s475,s479]) ).
cnf(s493,plain,
spl23_14,
inference(rat,[],[s351,s475,s479]) ).
cnf(s494,plain,
~ spl23_136,
inference(rat,[],[s350,s479]) ).
cnf(s495,plain,
~ spl23_122,
inference(rat,[],[s264,s479]) ).
cnf(s496,plain,
~ spl23_129,
inference(rat,[],[s260,s479]) ).
cnf(s498,plain,
~ spl23_134,
inference(rat,[],[s253,s480]) ).
cnf(s500,plain,
~ spl23_127,
inference(rat,[],[s207,s480]) ).
cnf(s501,plain,
~ spl23_137,
inference(rat,[],[s283,s481]) ).
cnf(s503,plain,
~ spl23_144,
inference(rat,[],[s188,s481]) ).
cnf(s504,plain,
spl23_16,
inference(rat,[],[s352,s480,s481]) ).
cnf(s505,plain,
spl23_18,
inference(rat,[],[s353,s480,s481]) ).
cnf(s507,plain,
~ spl23_36,
inference(rat,[],[s33,s487]) ).
cnf(s510,plain,
spl23_124,
inference(rat,[],[s453,s488,s491,s500]) ).
cnf(s511,plain,
~ spl23_7,
inference(rat,[],[s7,s482]) ).
cnf(s512,plain,
~ spl23_11,
inference(rat,[],[s10,s492]) ).
cnf(s513,plain,
~ spl23_52,
inference(rat,[],[s48,s493]) ).
cnf(s515,plain,
~ spl23_15,
inference(rat,[],[s13,s504]) ).
cnf(s516,plain,
~ spl23_67,
inference(rat,[],[s63,s505]) ).
cnf(s518,plain,
spl23_6,
inference(rat,[],[s199,s458,s510]) ).
cnf(s519,plain,
~ spl23_19,
inference(rat,[],[s18,s518]) ).
cnf(s520,plain,
~ spl23_98,
inference(rat,[],[s277,s172,s176,s189,s313,s167,s485,s456,s484]) ).
cnf(s521,plain,
~ spl23_118,
inference(rat,[],[s236,s183,s181,s220,s252,s162,s503,s454,s501]) ).
cnf(s522,plain,
~ spl23_177,
inference(rat,[],[s280,s175,s177,s293,s300,s159,s477,s456,s474]) ).
cnf(s523,plain,
( ~ spl23_105
| spl23_178 ),
inference(rat,[],[s327,s119,s92,s292,s522,s495]) ).
cnf(s524,plain,
( ~ spl23_182
| spl23_3 ),
inference(rat,[],[s49,s71,s379,s64,s123,s359,s52,s402,s183,s387,s365,s305,s124,s23,s93,s389,s386,s177,s280,s41,s447,s26,s28,s34,s282,s337,s340,s393,s394,s390,s128,s176,s223,s277,s442,s523,s67,s356,s44,s59,s182,s318,s364,s261,s311,s3,s511,s512,s21,s515,s519,s39,s507,s513,s57,s516,s494,s162,s503,s489,s456,s474,s460,s155,s455,s476,s521,s484,s491,s464,s454,s498,s164]) ).
cnf(s525,plain,
~ spl23_160,
inference(rat,[],[s236,s446,s114,s198,s371,s473,s457,s478,s520]) ).
cnf(s526,plain,
~ spl23_3,
inference(rat,[],[s6,s518]) ).
cnf(s527,plain,
~ spl23_182,
inference(rat,[],[s524,s526]) ).
cnf(s528,plain,
spl23_94,
inference(rat,[],[s180,s500,s154,s527]) ).
cnf(s529,plain,
spl23_105,
inference(rat,[],[s443,s525,s496,s527]) ).
cnf(s531,plain,
~ spl23_164,
inference(rat,[],[s287,s528]) ).
cnf(s535,plain,
spl23_178,
inference(rat,[],[s523,s529]) ).
cnf(s536,plain,
spl23_186,
inference(rat,[],[s182,s498,s454,s531]) ).
cnf(s538,plain,
$false,
inference(rat,[],[s303,s536,s535]) ).
fof(f2735,plain,
$false,
inference(avatar_sat_refutation,[],[s538]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG068+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n010.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 19:24:47 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.23 Running first-order model finding
% 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.33 % (2235127)Will run a generic schedule for satisfiability detection.
% 0.19/0.33 % (2235132)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1938396623_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.33 % (2235133)% WARNING: option uhcvi not known.
% 0.19/0.33 % (2235133)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2371690510:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.33 % (2235134)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2246388180:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.33 % (2235135)dis+10_1_sil=32000:sp=arity:random_seed=3166766785:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.33 % (2235136)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=137001780:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.33 % (2235137)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4122906789:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.33 % (2235138)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3530255565:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.33 % Detected minimum model sizes of [5]
% 0.19/0.33 % Detected maximum model sizes of [max]
% 0.19/0.33 % TRYING [5]
% 0.19/0.33 % TRYING [6]
% 0.19/0.33 % TRYING [7]
% 0.19/0.33 % (2235136) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2235127-2235136"...
% 0.19/0.33 % (2235136)...printing done.
% 0.19/0.33 % (2235136)Refutation found. Thanks to Tanya!
% 0.19/0.33 % SZS status Theorem for theBenchmark
% 0.19/0.33 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.35 % (2235136)------------------------------
% 0.19/0.35 % (2235136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (2235136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (2235136)CaDiCaL version: 2.1.3
% 0.19/0.35 % (2235136)Termination reason: Refutation
% 0.19/0.35 % (2235136)Time elapsed: 0.050 s
% 0.19/0.35 % (2235136)Peak memory usage: 13 MB
% 0.19/0.35 % (2235136)Instructions burned: 97 (million)
% 0.19/0.35 % (2235127)Success in time 0.096 s
% 0.19/0.35 % Vampire exiting
%------------------------------------------------------------------------------