%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG057+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 : n005.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:01 AM UTC 2026
% Result : Theorem 0.87s 0.44s
% Output : Refutation 0.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 122
% Syntax : Number of formulae : 954 ( 150 unt; 116 def)
% Number of atoms : 3570 (1481 equ)
% Maximal formula atoms : 125 ( 3 avg)
% Number of connectives : 4316 (1700 ~;2017 |; 517 &)
% ( 82 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 118 ( 116 usr; 117 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(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3
| op(e0,e0) = e4 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3
| op(e0,e1) = e4 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3
| op(e0,e2) = e4 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3
| op(e0,e3) = e4 )
& ( op(e0,e4) = e0
| op(e0,e4) = e1
| op(e0,e4) = e2
| op(e0,e4) = e3
| op(e0,e4) = e4 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3
| op(e1,e0) = e4 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e4 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3
| op(e1,e2) = e4 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3
| op(e1,e3) = e4 )
& ( op(e1,e4) = e0
| op(e1,e4) = e1
| op(e1,e4) = e2
| op(e1,e4) = e3
| op(e1,e4) = e4 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3
| op(e2,e0) = e4 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3
| op(e2,e1) = e4 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3
| op(e2,e2) = e4 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3
| op(e2,e3) = e4 )
& ( op(e2,e4) = e0
| op(e2,e4) = e1
| op(e2,e4) = e2
| op(e2,e4) = e3
| op(e2,e4) = e4 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3
| op(e3,e0) = e4 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3
| op(e3,e1) = e4 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3
| op(e3,e2) = e4 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3
| op(e3,e3) = e4 )
& ( op(e3,e4) = e0
| op(e3,e4) = e1
| op(e3,e4) = e2
| op(e3,e4) = e3
| op(e3,e4) = e4 )
& ( op(e4,e0) = e0
| op(e4,e0) = e1
| op(e4,e0) = e2
| op(e4,e0) = e3
| op(e4,e0) = e4 )
& ( op(e4,e1) = e0
| op(e4,e1) = e1
| op(e4,e1) = e2
| op(e4,e1) = e3
| op(e4,e1) = e4 )
& ( op(e4,e2) = e0
| op(e4,e2) = e1
| op(e4,e2) = e2
| op(e4,e2) = e3
| op(e4,e2) = e4 )
& ( op(e4,e3) = e0
| op(e4,e3) = e1
| op(e4,e3) = e2
| op(e4,e3) = e3
| op(e4,e3) = e4 )
& ( op(e4,e4) = e0
| op(e4,e4) = e1
| op(e4,e4) = e2
| op(e4,e4) = e3
| op(e4,e4) = e4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
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(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(e2,e2),op(e2,e2))
& e1 = op(op(e2,op(e2,e2)),op(e2,e2))
& e3 = op(e2,op(e2,e2))
& e4 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
fof(f7,conjecture,
~ ( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(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,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(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,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 ) )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 ) )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 ) )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 ) )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ( op(e4,op(e4,e4)) != e4
& op(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(f10,definition,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f34,definition,
( ( op(e4,op(e4,e4)) != e4
& op(e4,op(e4,e4)) = e4 )
| ~ sP24 ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f35,definition,
( ( op(e3,op(e3,e4)) != e4
& op(e4,op(e3,e4)) = e3 )
| ~ sP25 ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f36,definition,
( ( op(e4,op(e4,e3)) != e3
& op(e3,op(e4,e3)) = e4 )
| ~ sP26 ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f37,definition,
( ( op(e3,op(e3,e3)) != e3
& op(e3,op(e3,e3)) = e3 )
| ~ sP27 ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f38,definition,
( ( op(e4,op(e4,e2)) != e2
& op(e2,op(e4,e2)) = e4 )
| ~ sP28 ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f39,definition,
( ( op(e3,op(e3,e2)) != e2
& op(e2,op(e3,e2)) = e3 )
| ~ sP29 ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f40,definition,
( ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 )
| ~ sP30 ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f41,definition,
( ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ~ sP31 ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f42,definition,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP32 ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f43,definition,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP33 ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f44,plain,
( ( ( op(e0,op(e0,e0)) != e0
& op(e0,op(e0,e0)) = e0 )
| ( op(e1,op(e1,e0)) != e0
& op(e0,op(e1,e0)) = e1 )
| ( op(e2,op(e2,e0)) != e0
& op(e0,op(e2,e0)) = e2 )
| sP33
| sP32 )
& ( ( op(e0,op(e0,e1)) != e1
& op(e1,op(e0,e1)) = e0 )
| ( op(e1,op(e1,e1)) != e1
& op(e1,op(e1,e1)) = e1 )
| ( op(e2,op(e2,e1)) != e1
& op(e1,op(e2,e1)) = e2 )
| sP31
| sP30 )
& ( ( op(e0,op(e0,e2)) != e2
& op(e2,op(e0,e2)) = e0 )
| ( op(e1,op(e1,e2)) != e2
& op(e2,op(e1,e2)) = e1 )
| ( op(e2,op(e2,e2)) != e2
& op(e2,op(e2,e2)) = e2 )
| sP29
| sP28 )
& ( ( op(e0,op(e0,e3)) != e3
& op(e3,op(e0,e3)) = e0 )
| ( op(e1,op(e1,e3)) != e3
& op(e3,op(e1,e3)) = e1 )
| ( op(e2,op(e2,e3)) != e3
& op(e3,op(e2,e3)) = e2 )
| sP27
| sP26 )
& ( ( op(e0,op(e0,e4)) != e4
& op(e4,op(e0,e4)) = e0 )
| ( op(e1,op(e1,e4)) != e4
& op(e4,op(e1,e4)) = e1 )
| ( op(e2,op(e2,e4)) != e4
& op(e4,op(e2,e4)) = e2 )
| sP25
| sP24 )
& ( ( op(e0,e0) != op(e0,e0)
& op(op(e0,e0),e0) = e0
& op(op(e0,e0),e0) != e0 )
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ) ),
inference(definition_folding,[],[f9,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10]) ).
fof(f45,plain,
( ( op(e3,op(e3,e0)) != e0
& op(e0,op(e3,e0)) = e3 )
| ~ sP33 ),
inference(nnf_transformation,[],[f43]) ).
fof(f46,plain,
( ( op(e4,op(e4,e0)) != e0
& op(e0,op(e4,e0)) = e4 )
| ~ sP32 ),
inference(nnf_transformation,[],[f42]) ).
fof(f47,plain,
( ( op(e3,op(e3,e1)) != e1
& op(e1,op(e3,e1)) = e3 )
| ~ sP31 ),
inference(nnf_transformation,[],[f41]) ).
fof(f48,plain,
( ( op(e4,op(e4,e1)) != e1
& op(e1,op(e4,e1)) = e4 )
| ~ sP30 ),
inference(nnf_transformation,[],[f40]) ).
fof(f55,plain,
( ( op(e1,e0) != op(e0,e1)
& op(op(e0,e1),e1) = e0
& op(op(e0,e1),e0) != e1 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f56,plain,
( ( op(e2,e0) != op(e0,e2)
& op(op(e0,e2),e2) = e0
& op(op(e0,e2),e0) != e2 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f57,plain,
( ( op(e3,e0) != op(e0,e3)
& op(op(e0,e3),e3) = e0
& op(op(e0,e3),e0) != e3 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f58,plain,
( ( op(e4,e0) != op(e0,e4)
& op(op(e0,e4),e4) = e0
& op(op(e0,e4),e0) != e4 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f59,plain,
( ( op(e0,e1) != op(e1,e0)
& op(op(e1,e0),e0) = e1
& op(op(e1,e0),e1) != e0 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f60,plain,
( ( op(e1,e1) != op(e1,e1)
& op(op(e1,e1),e1) = e1
& op(op(e1,e1),e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f61,plain,
( ( op(e2,e1) != op(e1,e2)
& op(op(e1,e2),e2) = e1
& op(op(e1,e2),e1) != e2 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f62,plain,
( ( op(e3,e1) != op(e1,e3)
& op(op(e1,e3),e3) = e1
& op(op(e1,e3),e1) != e3 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f63,plain,
( ( op(e4,e1) != op(e1,e4)
& op(op(e1,e4),e4) = e1
& op(op(e1,e4),e1) != e4 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f64,plain,
( ( op(e0,e2) != op(e2,e0)
& op(op(e2,e0),e0) = e2
& op(op(e2,e0),e2) != e0 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f65,plain,
( ( op(e1,e2) != op(e2,e1)
& op(op(e2,e1),e1) = e2
& op(op(e2,e1),e2) != e1 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f66,plain,
( ( op(e2,e2) != op(e2,e2)
& op(op(e2,e2),e2) = e2
& op(op(e2,e2),e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f67,plain,
( ( op(e3,e2) != op(e2,e3)
& op(op(e2,e3),e3) = e2
& op(op(e2,e3),e2) != e3 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f68,plain,
( ( op(e4,e2) != op(e2,e4)
& op(op(e2,e4),e4) = e2
& op(op(e2,e4),e2) != e4 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f69,plain,
( ( op(e0,e3) != op(e3,e0)
& op(op(e3,e0),e0) = e3
& op(op(e3,e0),e3) != e0 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f70,plain,
( ( op(e1,e3) != op(e3,e1)
& op(op(e3,e1),e1) = e3
& op(op(e3,e1),e3) != e1 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f71,plain,
( ( op(e2,e3) != op(e3,e2)
& op(op(e3,e2),e2) = e3
& op(op(e3,e2),e3) != e2 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f72,plain,
( ( op(e3,e3) != op(e3,e3)
& op(op(e3,e3),e3) = e3
& op(op(e3,e3),e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f73,plain,
( ( op(e4,e3) != op(e3,e4)
& op(op(e3,e4),e4) = e3
& op(op(e3,e4),e3) != e4 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f74,plain,
( ( op(e0,e4) != op(e4,e0)
& op(op(e4,e0),e0) = e4
& op(op(e4,e0),e4) != e0 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f75,plain,
( ( op(e1,e4) != op(e4,e1)
& op(op(e4,e1),e1) = e4
& op(op(e4,e1),e4) != e1 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f76,plain,
( ( op(e2,e4) != op(e4,e2)
& op(op(e4,e2),e2) = e4
& op(op(e4,e2),e4) != e2 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f77,plain,
( ( op(e3,e4) != op(e4,e3)
& op(op(e4,e3),e3) = e4
& op(op(e4,e3),e4) != e3 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f78,plain,
( ( op(e4,e4) != op(e4,e4)
& op(op(e4,e4),e4) = e4
& op(op(e4,e4),e4) != e4 )
| ~ sP0 ),
inference(nnf_transformation,[],[f10]) ).
fof(f80,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f81,plain,
( e0 = op(e4,e2)
| e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f82,plain,
( e0 = op(e4,e1)
| e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f83,plain,
( e0 = op(e4,e0)
| e1 = op(e4,e0)
| e2 = op(e4,e0)
| e3 = op(e4,e0)
| e4 = op(e4,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f85,plain,
( e0 = op(e3,e3)
| e1 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f86,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f87,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1)
| e4 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f88,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0)
| e4 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f90,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f92,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| e4 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f93,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0)
| e4 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f94,plain,
( e0 = op(e1,e4)
| e1 = op(e1,e4)
| e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4) ),
inference(cnf_transformation,[],[f1]) ).
fof(f95,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f104,plain,
( e0 = unit
| e1 = unit
| e2 = unit
| e3 = unit
| e4 = unit ),
inference(cnf_transformation,[],[f2]) ).
fof(f105,plain,
e4 = op(e4,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
e4 = op(unit,e4),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f110,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f111,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f112,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f113,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f2]) ).
fof(f114,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f165,plain,
op(e4,e3) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f166,plain,
op(e4,e2) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f167,plain,
op(e4,e2) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f168,plain,
op(e4,e1) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f169,plain,
op(e4,e1) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f170,plain,
op(e4,e1) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f171,plain,
op(e4,e0) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f172,plain,
op(e4,e0) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f173,plain,
op(e4,e0) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f174,plain,
op(e4,e0) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f175,plain,
op(e3,e3) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f176,plain,
op(e3,e2) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f177,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f178,plain,
op(e3,e1) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f179,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f180,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f181,plain,
op(e3,e0) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f182,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f183,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f184,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f185,plain,
op(e2,e3) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f187,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f188,plain,
op(e2,e1) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f189,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f190,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f191,plain,
op(e2,e0) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f192,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f193,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f194,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f202,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f207,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f209,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f218,plain,
op(e1,e4) != op(e4,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f219,plain,
op(e1,e4) != op(e3,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f220,plain,
op(e1,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f223,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f224,plain,
op(e0,e4) != op(e1,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f225,plain,
op(e3,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f226,plain,
op(e2,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f228,plain,
op(e1,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f229,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f231,plain,
op(e0,e3) != op(e4,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f232,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f234,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f4]) ).
fof(f236,plain,
op(e2,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f237,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f238,plain,
op(e1,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f239,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f241,plain,
op(e0,e2) != op(e4,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f242,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f243,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f4]) ).
fof(f245,plain,
op(e3,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f246,plain,
op(e2,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f247,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f251,plain,
op(e0,e1) != op(e4,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f253,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f4]) ).
fof(f256,plain,
op(e2,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f260,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f265,plain,
e3 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f268,plain,
e1 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f269,plain,
e1 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f270,plain,
e1 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f271,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f275,plain,
e4 = op(e2,e2),
inference(cnf_transformation,[],[f6]) ).
fof(f276,plain,
e3 = op(e2,op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f277,plain,
e1 = op(op(e2,op(e2,e2)),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f278,plain,
e0 = op(op(e2,e2),op(e2,e2)),
inference(cnf_transformation,[],[f6]) ).
fof(f279,plain,
( e3 = op(e0,op(e3,e0))
| ~ sP33 ),
inference(cnf_transformation,[],[f45]) ).
fof(f280,plain,
( e0 != op(e3,op(e3,e0))
| ~ sP33 ),
inference(cnf_transformation,[],[f45]) ).
fof(f281,plain,
( e4 = op(e0,op(e4,e0))
| ~ sP32 ),
inference(cnf_transformation,[],[f46]) ).
fof(f282,plain,
( e0 != op(e4,op(e4,e0))
| ~ sP32 ),
inference(cnf_transformation,[],[f46]) ).
fof(f283,plain,
( e3 = op(e1,op(e3,e1))
| ~ sP31 ),
inference(cnf_transformation,[],[f47]) ).
fof(f285,plain,
( e4 = op(e1,op(e4,e1))
| ~ sP30 ),
inference(cnf_transformation,[],[f48]) ).
fof(f299,plain,
( e1 != op(op(e0,e1),e0)
| ~ sP23 ),
inference(cnf_transformation,[],[f55]) ).
fof(f302,plain,
( e2 != op(op(e0,e2),e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f56]) ).
fof(f307,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP21 ),
inference(cnf_transformation,[],[f57]) ).
fof(f310,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP20 ),
inference(cnf_transformation,[],[f58]) ).
fof(f313,plain,
( op(e0,e1) != op(e1,e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f59]) ).
fof(f316,plain,
( op(e1,e1) != op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f60]) ).
fof(f318,plain,
( e1 = op(op(e1,e2),e2)
| ~ sP17 ),
inference(cnf_transformation,[],[f61]) ).
fof(f321,plain,
( e1 = op(op(e1,e3),e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f62]) ).
fof(f324,plain,
( e1 = op(op(e1,e4),e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f63]) ).
fof(f328,plain,
( op(e0,e2) != op(e2,e0)
| ~ sP14 ),
inference(cnf_transformation,[],[f64]) ).
fof(f330,plain,
( e2 = op(op(e2,e1),e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f65]) ).
fof(f334,plain,
( op(e2,e2) != op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f66]) ).
fof(f336,plain,
( e2 = op(op(e2,e3),e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f67]) ).
fof(f339,plain,
( e2 = op(op(e2,e4),e4)
| ~ sP10 ),
inference(cnf_transformation,[],[f68]) ).
fof(f343,plain,
( op(e0,e3) != op(e3,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f69]) ).
fof(f345,plain,
( e3 = op(op(e3,e1),e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f70]) ).
fof(f348,plain,
( e3 = op(op(e3,e2),e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f71]) ).
fof(f352,plain,
( op(e3,e3) != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f72]) ).
fof(f354,plain,
( e3 = op(op(e3,e4),e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f73]) ).
fof(f358,plain,
( op(e0,e4) != op(e4,e0)
| ~ sP4 ),
inference(cnf_transformation,[],[f74]) ).
fof(f360,plain,
( e4 = op(op(e4,e1),e1)
| ~ sP3 ),
inference(cnf_transformation,[],[f75]) ).
fof(f362,plain,
( e2 != op(op(e4,e2),e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f76]) ).
fof(f365,plain,
( e3 != op(op(e4,e3),e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f77]) ).
fof(f370,plain,
( op(e4,e4) != op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f371,plain,
( e0 != op(op(e0,e0),e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f44]) ).
fof(f372,plain,
( e0 = op(op(e0,e0),e0)
| sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f44]) ).
fof(f402,plain,
( e1 != op(e0,op(e0,e1))
| e1 = op(e1,op(e1,e1))
| e2 = op(e1,op(e2,e1))
| sP31
| sP30 ),
inference(cnf_transformation,[],[f44]) ).
fof(f404,plain,
( e1 != op(e0,op(e0,e1))
| e1 != op(e1,op(e1,e1))
| e2 = op(e1,op(e2,e1))
| sP31
| sP30 ),
inference(cnf_transformation,[],[f44]) ).
fof(f406,plain,
( e0 = op(e0,op(e0,e0))
| e1 = op(e0,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(cnf_transformation,[],[f44]) ).
fof(f408,plain,
( e0 = op(e0,op(e0,e0))
| e0 != op(e1,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(cnf_transformation,[],[f44]) ).
fof(f410,plain,
( e0 != op(e0,op(e0,e0))
| e1 = op(e0,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(cnf_transformation,[],[f44]) ).
fof(f412,plain,
( e0 != op(e0,op(e0,e0))
| e0 != op(e1,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(cnf_transformation,[],[f44]) ).
fof(f415,plain,
~ sP0,
inference(trivial_inequality_removal,[],[f370]) ).
fof(f416,plain,
~ sP6,
inference(trivial_inequality_removal,[],[f352]) ).
fof(f417,plain,
~ sP12,
inference(trivial_inequality_removal,[],[f334]) ).
fof(f418,plain,
~ sP18,
inference(trivial_inequality_removal,[],[f316]) ).
fof(f419,plain,
( sP23
| sP22
| sP21
| sP20
| sP19
| sP18
| sP17
| sP16
| sP15
| sP14
| sP13
| sP12
| sP11
| sP10
| sP9
| sP8
| sP7
| sP6
| sP5
| sP4
| sP3
| sP2
| sP1
| sP0 ),
inference(global_subsumption,[],[f372,f371]) ).
fof(f420,plain,
( e1 = op(e0,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(global_subsumption,[],[f410,f406]) ).
fof(f422,plain,
( e0 != op(e1,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| sP32 ),
inference(global_subsumption,[],[f412,f408]) ).
fof(f430,plain,
e4 = op(e2,e2),
inference(global_subsumption,[],[f275]) ).
fof(f433,plain,
( sP23
| sP22
| sP21
| sP20
| sP19
| sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1 ),
inference(global_subsumption,[],[f419,f418,f417,f416,f415]) ).
fof(f435,definition,
( spl34_1
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl34_1])],[avatar_definition]) ).
fof(f436,plain,
( ~ sP32
| spl34_1 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f437,plain,
( sP32
| ~ spl34_1 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f439,definition,
( spl34_2
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl34_2])],[avatar_definition]) ).
fof(f443,definition,
( spl34_3
<=> e2 = op(e0,op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_3])],[avatar_definition]) ).
fof(f445,plain,
( e2 = op(e0,op(e2,e0))
| ~ spl34_3 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl34_4
<=> e1 = op(e0,op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_4])],[avatar_definition]) ).
fof(f448,plain,
( e1 != op(e0,op(e1,e0))
| spl34_4 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f449,plain,
( e1 = op(e0,op(e1,e0))
| ~ spl34_4 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl34_1
| spl34_2
| spl34_3
| spl34_4 ),
inference(avatar_split_clause,[],[f420,f447,f443,f439,f435]) ).
fof(f452,definition,
( spl34_5
<=> e0 = op(e3,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_5])],[avatar_definition]) ).
fof(f454,plain,
( e0 != op(e3,op(e3,e0))
| spl34_5 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( ~ spl34_2
| ~ spl34_5 ),
inference(avatar_split_clause,[],[f280,f452,f439]) ).
fof(f458,definition,
( spl34_6
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl34_6])],[avatar_definition]) ).
fof(f460,plain,
( ~ sP31
| spl34_6 ),
inference(avatar_component_clause,[],[f458]) ).
fof(f467,definition,
( spl34_8
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl34_8])],[avatar_definition]) ).
fof(f512,definition,
( spl34_18
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl34_18])],[avatar_definition]) ).
fof(f514,plain,
( ~ sP23
| spl34_18 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f516,definition,
( spl34_19
<=> e1 = op(op(e0,e1),e0) ),
introduced(definition,[new_symbols(definition,[spl34_19])],[avatar_definition]) ).
fof(f518,plain,
( e1 != op(op(e0,e1),e0)
| spl34_19 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f519,plain,
( ~ spl34_18
| ~ spl34_19 ),
inference(avatar_split_clause,[],[f299,f516,f512]) ).
fof(f521,definition,
( spl34_20
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl34_20])],[avatar_definition]) ).
fof(f523,plain,
( ~ sP22
| spl34_20 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f525,definition,
( spl34_21
<=> e2 = op(op(e0,e2),e0) ),
introduced(definition,[new_symbols(definition,[spl34_21])],[avatar_definition]) ).
fof(f527,plain,
( e2 != op(op(e0,e2),e0)
| spl34_21 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f528,plain,
( ~ spl34_20
| ~ spl34_21 ),
inference(avatar_split_clause,[],[f302,f525,f521]) ).
fof(f530,definition,
( spl34_22
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl34_22])],[avatar_definition]) ).
fof(f532,plain,
( ~ sP21
| spl34_22 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f539,definition,
( spl34_24
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl34_24])],[avatar_definition]) ).
fof(f541,plain,
( ~ sP20
| spl34_24 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f548,definition,
( spl34_26
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl34_26])],[avatar_definition]) ).
fof(f550,plain,
( ~ sP19
| spl34_26 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f557,definition,
( spl34_28
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl34_28])],[avatar_definition]) ).
fof(f566,definition,
( spl34_30
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl34_30])],[avatar_definition]) ).
fof(f567,plain,
( sP16
| ~ spl34_30 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f568,plain,
( ~ sP16
| spl34_30 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f575,definition,
( spl34_32
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl34_32])],[avatar_definition]) ).
fof(f577,plain,
( ~ sP15
| spl34_32 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f584,definition,
( spl34_34
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl34_34])],[avatar_definition]) ).
fof(f593,definition,
( spl34_36
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl34_36])],[avatar_definition]) ).
fof(f595,plain,
( ~ sP13
| spl34_36 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f602,definition,
( spl34_38
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl34_38])],[avatar_definition]) ).
fof(f604,plain,
( ~ sP11
| spl34_38 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f606,definition,
( spl34_39
<=> e3 = op(op(e2,e3),e2) ),
introduced(definition,[new_symbols(definition,[spl34_39])],[avatar_definition]) ).
fof(f607,plain,
( e3 = op(op(e2,e3),e2)
| ~ spl34_39 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f608,plain,
( e3 != op(op(e2,e3),e2)
| spl34_39 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f611,definition,
( spl34_40
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl34_40])],[avatar_definition]) ).
fof(f613,plain,
( ~ sP10
| spl34_40 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f620,definition,
( spl34_42
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl34_42])],[avatar_definition]) ).
fof(f622,plain,
( ~ sP9
| spl34_42 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f629,definition,
( spl34_44
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl34_44])],[avatar_definition]) ).
fof(f631,plain,
( ~ sP8
| spl34_44 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f638,definition,
( spl34_46
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl34_46])],[avatar_definition]) ).
fof(f640,plain,
( ~ sP7
| spl34_46 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f647,definition,
( spl34_48
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl34_48])],[avatar_definition]) ).
fof(f649,plain,
( ~ sP5
| spl34_48 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f656,definition,
( spl34_50
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl34_50])],[avatar_definition]) ).
fof(f658,plain,
( ~ sP4
| spl34_50 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f665,definition,
( spl34_52
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl34_52])],[avatar_definition]) ).
fof(f667,plain,
( ~ sP3
| spl34_52 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f674,definition,
( spl34_54
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl34_54])],[avatar_definition]) ).
fof(f676,plain,
( ~ sP2
| spl34_54 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f678,definition,
( spl34_55
<=> e2 = op(op(e4,e2),e4) ),
introduced(definition,[new_symbols(definition,[spl34_55])],[avatar_definition]) ).
fof(f680,plain,
( e2 != op(op(e4,e2),e4)
| spl34_55 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,plain,
( ~ spl34_54
| ~ spl34_55 ),
inference(avatar_split_clause,[],[f362,f678,f674]) ).
fof(f683,definition,
( spl34_56
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl34_56])],[avatar_definition]) ).
fof(f685,plain,
( ~ sP1
| spl34_56 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,definition,
( spl34_57
<=> e3 = op(op(e4,e3),e4) ),
introduced(definition,[new_symbols(definition,[spl34_57])],[avatar_definition]) ).
fof(f689,plain,
( e3 != op(op(e4,e3),e4)
| spl34_57 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( ~ spl34_56
| ~ spl34_57 ),
inference(avatar_split_clause,[],[f365,f687,f683]) ).
fof(f730,definition,
( spl34_58
<=> op(e0,e3) = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_58])],[avatar_definition]) ).
fof(f731,plain,
( op(e0,e3) = op(e3,e0)
| ~ spl34_58 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f732,plain,
( op(e0,e3) != op(e3,e0)
| spl34_58 ),
inference(avatar_component_clause,[],[f730]) ).
fof(f733,plain,
( ~ spl34_22
| ~ spl34_58 ),
inference(avatar_split_clause,[],[f307,f730,f530]) ).
fof(f738,definition,
( spl34_59
<=> e2 = op(e4,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_59])],[avatar_definition]) ).
fof(f739,plain,
( e2 != op(e4,op(e2,e4))
| spl34_59 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f740,plain,
( e2 = op(e4,op(e2,e4))
| ~ spl34_59 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f753,definition,
( spl34_62
<=> e4 = op(e2,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_62])],[avatar_definition]) ).
fof(f754,plain,
( e4 = op(e2,op(e2,e4))
| ~ spl34_62 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f755,plain,
( e4 != op(e2,op(e2,e4))
| spl34_62 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f845,definition,
( spl34_76
<=> e2 = op(e1,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl34_76])],[avatar_definition]) ).
fof(f846,plain,
( e2 != op(e1,op(e2,e1))
| spl34_76 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f847,plain,
( e2 = op(e1,op(e2,e1))
| ~ spl34_76 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f853,definition,
( spl34_78
<=> e0 = op(e1,op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl34_78])],[avatar_definition]) ).
fof(f854,plain,
( e0 != op(e1,op(e0,e1))
| spl34_78 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f855,plain,
( e0 = op(e1,op(e0,e1))
| ~ spl34_78 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f896,plain,
e3 = op(e2,e4),
inference(forward_demodulation,[],[f276,f430]) ).
fof(f897,plain,
e3 != op(e2,e3),
inference(superposition,[],[f185,f896]) ).
fof(f899,plain,
e3 != op(e2,e1),
inference(superposition,[],[f188,f896]) ).
fof(f900,plain,
e3 != op(e2,e0),
inference(superposition,[],[f191,f896]) ).
fof(f901,plain,
( e2 = op(e4,e3)
| ~ spl34_59 ),
inference(superposition,[],[f740,f896]) ).
fof(f902,plain,
( e4 = op(e2,e3)
| ~ spl34_62 ),
inference(superposition,[],[f754,f896]) ).
fof(f906,plain,
( e2 != op(e4,e1)
| ~ spl34_59 ),
inference(superposition,[],[f169,f901]) ).
fof(f908,plain,
( e2 != op(e3,e3)
| ~ spl34_59 ),
inference(superposition,[],[f225,f901]) ).
fof(f912,plain,
( e4 != op(e2,e2)
| ~ spl34_62 ),
inference(superposition,[],[f187,f902]) ).
fof(f921,plain,
( $false
| ~ spl34_62 ),
inference(forward_subsumption_resolution,[],[f912,f430]) ).
fof(f922,plain,
~ spl34_62,
inference(avatar_contradiction_clause,[],[f921]) ).
fof(f923,plain,
( e4 != op(e2,e3)
| spl34_62 ),
inference(forward_demodulation,[],[f755,f896]) ).
fof(f925,definition,
( spl34_81
<=> e3 = op(e0,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_81])],[avatar_definition]) ).
fof(f927,plain,
( e3 = op(e0,op(e3,e0))
| ~ spl34_81 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f928,plain,
( ~ spl34_2
| spl34_81 ),
inference(avatar_split_clause,[],[f279,f925,f439]) ).
fof(f929,plain,
( e4 = op(e0,op(e4,e0))
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f281,f437]) ).
fof(f931,plain,
e0 = op(e4,e4),
inference(forward_demodulation,[],[f278,f430]) ).
fof(f932,plain,
e0 != op(e4,e3),
inference(superposition,[],[f165,f931]) ).
fof(f933,plain,
e0 != op(e4,e2),
inference(superposition,[],[f166,f931]) ).
fof(f934,plain,
e0 != op(e4,e1),
inference(superposition,[],[f168,f931]) ).
fof(f935,plain,
e0 != op(e4,e0),
inference(superposition,[],[f171,f931]) ).
fof(f938,plain,
e0 != op(e1,e4),
inference(superposition,[],[f218,f931]) ).
fof(f942,plain,
e1 = op(op(e2,e4),e4),
inference(forward_demodulation,[],[f277,f430]) ).
fof(f943,plain,
e1 = op(e3,e4),
inference(forward_demodulation,[],[f942,f896]) ).
fof(f944,plain,
e1 != op(e3,e3),
inference(superposition,[],[f175,f943]) ).
fof(f945,plain,
e1 != op(e3,e2),
inference(superposition,[],[f176,f943]) ).
fof(f946,plain,
e1 != op(e3,e1),
inference(superposition,[],[f178,f943]) ).
fof(f947,plain,
e1 != op(e3,e0),
inference(superposition,[],[f181,f943]) ).
fof(f949,plain,
e1 != op(e1,e4),
inference(superposition,[],[f219,f943]) ).
fof(f954,definition,
( spl34_82
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl34_82])],[avatar_definition]) ).
fof(f956,plain,
( e4 = unit
| ~ spl34_82 ),
inference(avatar_component_clause,[],[f954]) ).
fof(f958,definition,
( spl34_83
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl34_83])],[avatar_definition]) ).
fof(f960,plain,
( e3 = unit
| ~ spl34_83 ),
inference(avatar_component_clause,[],[f958]) ).
fof(f962,definition,
( spl34_84
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl34_84])],[avatar_definition]) ).
fof(f964,plain,
( e2 = unit
| ~ spl34_84 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f966,definition,
( spl34_85
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl34_85])],[avatar_definition]) ).
fof(f968,plain,
( e1 = unit
| ~ spl34_85 ),
inference(avatar_component_clause,[],[f966]) ).
fof(f970,definition,
( spl34_86
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl34_86])],[avatar_definition]) ).
fof(f972,plain,
( e0 = unit
| ~ spl34_86 ),
inference(avatar_component_clause,[],[f970]) ).
fof(f973,plain,
( spl34_82
| spl34_83
| spl34_84
| spl34_85
| spl34_86 ),
inference(avatar_split_clause,[],[f104,f970,f966,f962,f958,f954]) ).
fof(f974,plain,
( e4 = op(e4,e4)
| ~ spl34_82 ),
inference(superposition,[],[f105,f956]) ).
fof(f997,plain,
( e0 = e4
| ~ spl34_82 ),
inference(forward_demodulation,[],[f974,f931]) ).
fof(f1004,plain,
( $false
| ~ spl34_82 ),
inference(forward_subsumption_resolution,[],[f997,f271]) ).
fof(f1005,plain,
~ spl34_82,
inference(avatar_contradiction_clause,[],[f1004]) ).
fof(f1007,plain,
( e4 = op(e3,e4)
| ~ spl34_83 ),
inference(superposition,[],[f106,f960]) ).
fof(f1021,plain,
( e1 = e4
| ~ spl34_83 ),
inference(forward_demodulation,[],[f1007,f943]) ).
fof(f1023,plain,
( $false
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f1021,f268]) ).
fof(f1024,plain,
~ spl34_83,
inference(avatar_contradiction_clause,[],[f1023]) ).
fof(f1028,plain,
( e4 = op(e2,e4)
| ~ spl34_84 ),
inference(superposition,[],[f106,f964]) ).
fof(f1041,plain,
( e3 = e4
| ~ spl34_84 ),
inference(forward_demodulation,[],[f1028,f896]) ).
fof(f1042,plain,
( $false
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f1041,f265]) ).
fof(f1043,plain,
~ spl34_84,
inference(avatar_contradiction_clause,[],[f1042]) ).
fof(f1052,plain,
( e0 = op(e0,e1)
| ~ spl34_85 ),
inference(superposition,[],[f113,f968]) ).
fof(f1053,plain,
( e0 = op(e1,e0)
| ~ spl34_85 ),
inference(superposition,[],[f114,f968]) ).
fof(f1160,plain,
( e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(forward_subsumption_resolution,[],[f81,f933]) ).
fof(f1164,definition,
( spl34_87
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_87])],[avatar_definition]) ).
fof(f1165,plain,
( e3 != op(e4,e2)
| spl34_87 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1166,plain,
( e3 = op(e4,e2)
| ~ spl34_87 ),
inference(avatar_component_clause,[],[f1164]) ).
fof(f1168,definition,
( spl34_88
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_88])],[avatar_definition]) ).
fof(f1169,plain,
( e1 != op(e4,e2)
| spl34_88 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1170,plain,
( e1 = op(e4,e2)
| ~ spl34_88 ),
inference(avatar_component_clause,[],[f1168]) ).
fof(f1180,plain,
( e1 = op(e4,e0)
| e2 = op(e4,e0)
| e3 = op(e4,e0)
| e4 = op(e4,e0) ),
inference(forward_subsumption_resolution,[],[f83,f935]) ).
fof(f1184,definition,
( spl34_89
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_89])],[avatar_definition]) ).
fof(f1185,plain,
( e3 != op(e4,e0)
| spl34_89 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1186,plain,
( e3 = op(e4,e0)
| ~ spl34_89 ),
inference(avatar_component_clause,[],[f1184]) ).
fof(f1188,definition,
( spl34_90
<=> e1 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_90])],[avatar_definition]) ).
fof(f1189,plain,
( e1 != op(e4,e0)
| spl34_90 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1190,plain,
( e1 = op(e4,e0)
| ~ spl34_90 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1192,plain,
( e3 != op(e4,e2)
| ~ spl34_89 ),
inference(superposition,[],[f173,f1186]) ).
fof(f1199,plain,
( e4 = op(e0,e3)
| ~ spl34_1
| ~ spl34_89 ),
inference(superposition,[],[f929,f1186]) ).
fof(f1203,plain,
( $false
| ~ spl34_87
| ~ spl34_89 ),
inference(forward_subsumption_resolution,[],[f1192,f1166]) ).
fof(f1204,plain,
( ~ spl34_87
| ~ spl34_89 ),
inference(avatar_contradiction_clause,[],[f1203]) ).
fof(f1376,plain,
( e0 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3) ),
inference(forward_subsumption_resolution,[],[f85,f944]) ).
fof(f1377,plain,
( e0 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3)
| ~ spl34_59 ),
inference(forward_subsumption_resolution,[],[f1376,f908]) ).
fof(f1379,definition,
( spl34_92
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_92])],[avatar_definition]) ).
fof(f1381,plain,
( e4 = op(e3,e3)
| ~ spl34_92 ),
inference(avatar_component_clause,[],[f1379]) ).
fof(f1383,definition,
( spl34_93
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_93])],[avatar_definition]) ).
fof(f1385,plain,
( e3 = op(e3,e3)
| ~ spl34_93 ),
inference(avatar_component_clause,[],[f1383]) ).
fof(f1387,definition,
( spl34_94
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_94])],[avatar_definition]) ).
fof(f1389,plain,
( e0 = op(e3,e3)
| ~ spl34_94 ),
inference(avatar_component_clause,[],[f1387]) ).
fof(f1390,plain,
( spl34_92
| spl34_93
| spl34_94
| ~ spl34_59 ),
inference(avatar_split_clause,[],[f1377,f738,f1387,f1383,f1379]) ).
fof(f1392,plain,
( e4 != op(e3,e1)
| ~ spl34_92 ),
inference(superposition,[],[f179,f1381]) ).
fof(f1395,plain,
( e4 != op(e1,e3)
| ~ spl34_92 ),
inference(superposition,[],[f229,f1381]) ).
fof(f1396,plain,
( e4 != op(e0,e3)
| ~ spl34_92 ),
inference(superposition,[],[f232,f1381]) ).
fof(f1399,plain,
( $false
| ~ spl34_1
| ~ spl34_89
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f1396,f1199]) ).
fof(f1400,plain,
( ~ spl34_1
| ~ spl34_89
| ~ spl34_92 ),
inference(avatar_contradiction_clause,[],[f1399]) ).
fof(f1425,plain,
( e0 != op(e1,e0)
| spl34_78
| ~ spl34_85 ),
inference(forward_demodulation,[],[f854,f1052]) ).
fof(f1430,plain,
( $false
| spl34_78
| ~ spl34_85 ),
inference(global_subsumption,[],[f1425,f1053]) ).
fof(f1431,plain,
( spl34_78
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f1430]) ).
fof(f1432,plain,
( e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1) ),
inference(forward_subsumption_resolution,[],[f82,f934]) ).
fof(f1433,plain,
( e1 = op(e4,e1)
| e3 = op(e4,e1)
| e4 = op(e4,e1)
| ~ spl34_59 ),
inference(forward_subsumption_resolution,[],[f1432,f906]) ).
fof(f1435,definition,
( spl34_95
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_95])],[avatar_definition]) ).
fof(f1436,plain,
( e4 != op(e4,e1)
| spl34_95 ),
inference(avatar_component_clause,[],[f1435]) ).
fof(f1437,plain,
( e4 = op(e4,e1)
| ~ spl34_95 ),
inference(avatar_component_clause,[],[f1435]) ).
fof(f1439,definition,
( spl34_96
<=> e3 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_96])],[avatar_definition]) ).
fof(f1441,plain,
( e3 = op(e4,e1)
| ~ spl34_96 ),
inference(avatar_component_clause,[],[f1439]) ).
fof(f1443,definition,
( spl34_97
<=> e1 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_97])],[avatar_definition]) ).
fof(f1445,plain,
( e1 = op(e4,e1)
| ~ spl34_97 ),
inference(avatar_component_clause,[],[f1443]) ).
fof(f1446,plain,
( spl34_95
| spl34_96
| spl34_97
| ~ spl34_59 ),
inference(avatar_split_clause,[],[f1433,f738,f1443,f1439,f1435]) ).
fof(f1448,plain,
( e4 != op(e4,e0)
| ~ spl34_95 ),
inference(superposition,[],[f174,f1437]) ).
fof(f1457,plain,
( e0 != op(e1,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP33
| spl34_1 ),
inference(forward_subsumption_resolution,[],[f422,f436]) ).
fof(f1459,definition,
( spl34_98
<=> e0 = op(e1,op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_98])],[avatar_definition]) ).
fof(f1461,plain,
( e0 != op(e1,op(e1,e0))
| spl34_98 ),
inference(avatar_component_clause,[],[f1459]) ).
fof(f1462,plain,
( spl34_2
| spl34_3
| ~ spl34_98
| spl34_1 ),
inference(avatar_split_clause,[],[f1457,f435,f1459,f443,f439]) ).
fof(f1463,plain,
( e4 = op(e4,e0)
| ~ spl34_86 ),
inference(superposition,[],[f105,f972]) ).
fof(f1464,plain,
( e4 = op(e0,e4)
| ~ spl34_86 ),
inference(superposition,[],[f106,f972]) ).
fof(f1465,plain,
( e3 = op(e3,e0)
| ~ spl34_86 ),
inference(superposition,[],[f107,f972]) ).
fof(f1466,plain,
( e3 = op(e0,e3)
| ~ spl34_86 ),
inference(superposition,[],[f108,f972]) ).
fof(f1467,plain,
( e2 = op(e2,e0)
| ~ spl34_86 ),
inference(superposition,[],[f109,f972]) ).
fof(f1468,plain,
( e2 = op(e0,e2)
| ~ spl34_86 ),
inference(superposition,[],[f110,f972]) ).
fof(f1469,plain,
( e1 = op(e1,e0)
| ~ spl34_86 ),
inference(superposition,[],[f111,f972]) ).
fof(f1470,plain,
( e1 = op(e0,e1)
| ~ spl34_86 ),
inference(superposition,[],[f112,f972]) ).
fof(f1479,plain,
( e3 = e4
| ~ spl34_86
| ~ spl34_89 ),
inference(forward_demodulation,[],[f1463,f1186]) ).
fof(f1480,plain,
( $false
| ~ spl34_86
| ~ spl34_89 ),
inference(forward_subsumption_resolution,[],[f1479,f265]) ).
fof(f1481,plain,
( ~ spl34_86
| ~ spl34_89 ),
inference(avatar_contradiction_clause,[],[f1480]) ).
fof(f1485,plain,
( e1 != op(e4,e2)
| ~ spl34_90 ),
inference(superposition,[],[f173,f1190]) ).
fof(f1494,plain,
( $false
| ~ spl34_88
| ~ spl34_90 ),
inference(forward_subsumption_resolution,[],[f1485,f1170]) ).
fof(f1495,plain,
( ~ spl34_88
| ~ spl34_90 ),
inference(avatar_contradiction_clause,[],[f1494]) ).
fof(f1500,plain,
( e2 != op(e4,e3)
| spl34_59 ),
inference(forward_demodulation,[],[f739,f896]) ).
fof(f1501,plain,
( e1 = op(e4,e3)
| e2 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3) ),
inference(global_subsumption,[],[f80,f932]) ).
fof(f1502,plain,
( e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2)
| spl34_88 ),
inference(forward_subsumption_resolution,[],[f1160,f1169]) ).
fof(f1503,plain,
( e2 = op(e4,e2)
| e4 = op(e4,e2)
| spl34_87
| spl34_88 ),
inference(forward_subsumption_resolution,[],[f1502,f1165]) ).
fof(f1514,plain,
( $false
| ~ spl34_86
| ~ spl34_95 ),
inference(forward_subsumption_resolution,[],[f1463,f1448]) ).
fof(f1515,plain,
( ~ spl34_86
| ~ spl34_95 ),
inference(avatar_contradiction_clause,[],[f1514]) ).
fof(f1516,plain,
( e1 = e4
| ~ spl34_86
| ~ spl34_90 ),
inference(forward_demodulation,[],[f1463,f1190]) ).
fof(f1517,plain,
( $false
| ~ spl34_86
| ~ spl34_90 ),
inference(forward_subsumption_resolution,[],[f1516,f268]) ).
fof(f1518,plain,
( ~ spl34_86
| ~ spl34_90 ),
inference(avatar_contradiction_clause,[],[f1517]) ).
fof(f1519,plain,
( e1 = op(e4,e0)
| e2 = op(e4,e0)
| e4 = op(e4,e0)
| spl34_89 ),
inference(forward_subsumption_resolution,[],[f1180,f1185]) ).
fof(f1521,definition,
( spl34_99
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_99])],[avatar_definition]) ).
fof(f1523,plain,
( e4 = op(e4,e2)
| ~ spl34_99 ),
inference(avatar_component_clause,[],[f1521]) ).
fof(f1525,definition,
( spl34_100
<=> e2 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_100])],[avatar_definition]) ).
fof(f1527,plain,
( e2 = op(e4,e2)
| ~ spl34_100 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1528,plain,
( spl34_99
| spl34_100
| spl34_87
| spl34_88 ),
inference(avatar_split_clause,[],[f1503,f1168,f1164,f1525,f1521]) ).
fof(f1530,plain,
( e4 != op(e2,e2)
| ~ spl34_99 ),
inference(superposition,[],[f236,f1523]) ).
fof(f1536,plain,
( $false
| ~ spl34_99 ),
inference(forward_subsumption_resolution,[],[f1530,f430]) ).
fof(f1537,plain,
~ spl34_99,
inference(avatar_contradiction_clause,[],[f1536]) ).
fof(f1541,plain,
( e2 != op(e0,e2)
| ~ spl34_100 ),
inference(superposition,[],[f241,f1527]) ).
fof(f1547,plain,
( e2 = op(e4,e0)
| e4 = op(e4,e0)
| spl34_89
| spl34_90 ),
inference(forward_subsumption_resolution,[],[f1519,f1189]) ).
fof(f1549,definition,
( spl34_101
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_101])],[avatar_definition]) ).
fof(f1551,plain,
( e4 = op(e4,e0)
| ~ spl34_101 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1553,definition,
( spl34_102
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_102])],[avatar_definition]) ).
fof(f1555,plain,
( e2 = op(e4,e0)
| ~ spl34_102 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1556,plain,
( spl34_101
| spl34_102
| spl34_89
| spl34_90 ),
inference(avatar_split_clause,[],[f1547,f1188,f1184,f1553,f1549]) ).
fof(f1565,plain,
( e1 = op(e4,e1)
| e2 = op(e4,e1)
| e3 = op(e4,e1)
| spl34_95 ),
inference(forward_subsumption_resolution,[],[f1432,f1436]) ).
fof(f1567,definition,
( spl34_103
<=> e2 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_103])],[avatar_definition]) ).
fof(f1569,plain,
( e2 = op(e4,e1)
| ~ spl34_103 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1570,plain,
( spl34_96
| spl34_103
| spl34_97
| spl34_95 ),
inference(avatar_split_clause,[],[f1565,f1435,f1443,f1567,f1439]) ).
fof(f1571,plain,
( e3 != op(e4,e2)
| ~ spl34_96 ),
inference(superposition,[],[f170,f1441]) ).
fof(f1573,plain,
( e3 != op(e3,e1)
| ~ spl34_96 ),
inference(superposition,[],[f245,f1441]) ).
fof(f1634,plain,
( e1 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl34_59 ),
inference(forward_subsumption_resolution,[],[f1501,f1500]) ).
fof(f1636,definition,
( spl34_104
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_104])],[avatar_definition]) ).
fof(f1638,plain,
( e4 = op(e4,e3)
| ~ spl34_104 ),
inference(avatar_component_clause,[],[f1636]) ).
fof(f1640,definition,
( spl34_105
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_105])],[avatar_definition]) ).
fof(f1642,plain,
( e3 = op(e4,e3)
| ~ spl34_105 ),
inference(avatar_component_clause,[],[f1640]) ).
fof(f1644,definition,
( spl34_106
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_106])],[avatar_definition]) ).
fof(f1646,plain,
( e1 = op(e4,e3)
| ~ spl34_106 ),
inference(avatar_component_clause,[],[f1644]) ).
fof(f1647,plain,
( spl34_104
| spl34_105
| spl34_106
| spl34_59 ),
inference(avatar_split_clause,[],[f1634,f738,f1644,f1640,f1636]) ).
fof(f1650,plain,
( e4 != op(e4,e0)
| ~ spl34_104 ),
inference(superposition,[],[f172,f1638]) ).
fof(f1659,plain,
( $false
| ~ spl34_101
| ~ spl34_104 ),
inference(forward_subsumption_resolution,[],[f1650,f1551]) ).
fof(f1660,plain,
( ~ spl34_101
| ~ spl34_104 ),
inference(avatar_contradiction_clause,[],[f1659]) ).
fof(f1661,plain,
( e1 != op(e4,e2)
| ~ spl34_106 ),
inference(superposition,[],[f167,f1646]) ).
fof(f1672,plain,
( e3 != op(e3,e2)
| ~ spl34_86 ),
inference(superposition,[],[f183,f1465]) ).
fof(f1677,plain,
( e3 != op(e0,e3)
| spl34_58
| ~ spl34_86 ),
inference(superposition,[],[f732,f1465]) ).
fof(f1681,plain,
( $false
| spl34_58
| ~ spl34_86 ),
inference(global_subsumption,[],[f1677,f1466]) ).
fof(f1682,plain,
( spl34_58
| ~ spl34_86 ),
inference(avatar_contradiction_clause,[],[f1681]) ).
fof(f1684,plain,
( e3 = op(e0,e3)
| ~ spl34_58
| ~ spl34_86 ),
inference(forward_demodulation,[],[f731,f1465]) ).
fof(f1685,plain,
( e3 != op(e0,e2)
| ~ spl34_58
| ~ spl34_86 ),
inference(superposition,[],[f207,f1684]) ).
fof(f1697,plain,
( $false
| ~ spl34_86
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f1468,f1541]) ).
fof(f1698,plain,
( ~ spl34_86
| ~ spl34_100 ),
inference(avatar_contradiction_clause,[],[f1697]) ).
fof(f1700,plain,
( ~ spl34_87
| ~ spl34_96 ),
inference(avatar_split_clause,[],[f1571,f1439,f1164]) ).
fof(f1703,plain,
( ~ spl34_88
| ~ spl34_106 ),
inference(avatar_split_clause,[],[f1661,f1644,f1168]) ).
fof(f1719,plain,
( e3 != op(e0,e3)
| ~ spl34_105 ),
inference(superposition,[],[f231,f1642]) ).
fof(f1724,plain,
( $false
| ~ spl34_58
| ~ spl34_86
| ~ spl34_105 ),
inference(forward_subsumption_resolution,[],[f1719,f1684]) ).
fof(f1725,plain,
( ~ spl34_58
| ~ spl34_86
| ~ spl34_105 ),
inference(avatar_contradiction_clause,[],[f1724]) ).
fof(f1729,plain,
( e2 = op(e4,e3)
| ~ spl34_59 ),
inference(forward_demodulation,[],[f740,f896]) ).
fof(f1736,plain,
( e2 != op(e2,e3)
| ~ spl34_59 ),
inference(superposition,[],[f226,f1729]) ).
fof(f1737,plain,
( e2 != op(e1,e3)
| ~ spl34_59 ),
inference(superposition,[],[f228,f1729]) ).
fof(f1748,plain,
( e2 != op(e2,e0)
| spl34_21
| ~ spl34_86 ),
inference(superposition,[],[f527,f1468]) ).
fof(f1760,plain,
( $false
| spl34_21
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f1748,f1467]) ).
fof(f1761,plain,
( spl34_21
| ~ spl34_86 ),
inference(avatar_contradiction_clause,[],[f1760]) ).
fof(f1850,definition,
( spl34_107
<=> op(e2,e3) = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_107])],[avatar_definition]) ).
fof(f1851,plain,
( op(e2,e3) = op(e3,e2)
| ~ spl34_107 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1852,plain,
( op(e2,e3) != op(e3,e2)
| spl34_107 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1874,plain,
( e1 = op(e0,e1)
| ~ spl34_4
| ~ spl34_86 ),
inference(superposition,[],[f449,f1469]) ).
fof(f1880,plain,
( e1 != op(e2,e1)
| ~ spl34_4
| ~ spl34_86 ),
inference(superposition,[],[f253,f1874]) ).
fof(f1881,plain,
( e1 != op(e1,e0)
| ~ spl34_4
| spl34_19
| ~ spl34_86 ),
inference(superposition,[],[f518,f1874]) ).
fof(f1885,plain,
( $false
| ~ spl34_4
| spl34_19
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f1881,f1469]) ).
fof(f1886,plain,
( ~ spl34_4
| spl34_19
| ~ spl34_86 ),
inference(avatar_contradiction_clause,[],[f1885]) ).
fof(f1897,plain,
( e0 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2) ),
inference(forward_subsumption_resolution,[],[f86,f945]) ).
fof(f1898,plain,
( e0 = op(e3,e2)
| e2 = op(e3,e2)
| e4 = op(e3,e2)
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f1897,f1672]) ).
fof(f1901,definition,
( spl34_108
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_108])],[avatar_definition]) ).
fof(f1902,plain,
( e2 != op(e3,e2)
| spl34_108 ),
inference(avatar_component_clause,[],[f1901]) ).
fof(f1903,plain,
( e2 = op(e3,e2)
| ~ spl34_108 ),
inference(avatar_component_clause,[],[f1901]) ).
fof(f1905,definition,
( spl34_109
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_109])],[avatar_definition]) ).
fof(f1906,plain,
( e0 != op(e3,e2)
| spl34_109 ),
inference(avatar_component_clause,[],[f1905]) ).
fof(f1907,plain,
( e0 = op(e3,e2)
| ~ spl34_109 ),
inference(avatar_component_clause,[],[f1905]) ).
fof(f1911,plain,
( e2 != op(e0,e2)
| ~ spl34_108 ),
inference(superposition,[],[f242,f1903]) ).
fof(f1916,plain,
( $false
| ~ spl34_86
| ~ spl34_108 ),
inference(forward_subsumption_resolution,[],[f1911,f1468]) ).
fof(f1917,plain,
( ~ spl34_86
| ~ spl34_108 ),
inference(avatar_contradiction_clause,[],[f1916]) ).
fof(f1925,plain,
( e0 != op(e2,e3)
| spl34_107
| ~ spl34_109 ),
inference(superposition,[],[f1852,f1907]) ).
fof(f1929,plain,
( e0 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1)
| e4 = op(e3,e1) ),
inference(forward_subsumption_resolution,[],[f87,f946]) ).
fof(f1930,plain,
( e0 = op(e3,e1)
| e2 = op(e3,e1)
| e4 = op(e3,e1)
| ~ spl34_96 ),
inference(forward_subsumption_resolution,[],[f1929,f1573]) ).
fof(f1931,plain,
( e0 = op(e3,e1)
| e2 = op(e3,e1)
| ~ spl34_92
| ~ spl34_96 ),
inference(forward_subsumption_resolution,[],[f1930,f1392]) ).
fof(f1933,definition,
( spl34_110
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl34_110])],[avatar_definition]) ).
fof(f1935,plain,
( e2 = op(e3,e1)
| ~ spl34_110 ),
inference(avatar_component_clause,[],[f1933]) ).
fof(f1937,definition,
( spl34_111
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl34_111])],[avatar_definition]) ).
fof(f1939,plain,
( e0 = op(e3,e1)
| ~ spl34_111 ),
inference(avatar_component_clause,[],[f1937]) ).
fof(f1940,plain,
( spl34_110
| spl34_111
| ~ spl34_92
| ~ spl34_96 ),
inference(avatar_split_clause,[],[f1931,f1439,f1379,f1937,f1933]) ).
fof(f1943,plain,
( e2 != op(e2,e1)
| ~ spl34_110 ),
inference(superposition,[],[f247,f1935]) ).
fof(f1951,plain,
( e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3)
| spl34_107
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f90,f1925]) ).
fof(f1952,plain,
( e1 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3)
| ~ spl34_59
| spl34_107
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f1951,f1736]) ).
fof(f1953,plain,
( e1 = op(e2,e3)
| e4 = op(e2,e3)
| ~ spl34_59
| spl34_107
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f1952,f897]) ).
fof(f1954,plain,
( e1 = op(e2,e3)
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f1953,f923]) ).
fof(f1958,plain,
( e3 != op(e1,e2)
| spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(superposition,[],[f608,f1954]) ).
fof(f1970,plain,
( e2 = op(e1,e3)
| ~ sP11
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(forward_demodulation,[],[f336,f1954]) ).
fof(f1975,plain,
( ~ sP11
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f1970,f1737]) ).
fof(f2026,plain,
( ~ spl34_38
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(avatar_split_clause,[],[f1975,f1905,f1850,f753,f738,f602]) ).
fof(f2031,plain,
( e1 = op(op(e1,e3),e3)
| ~ spl34_30 ),
inference(forward_subsumption_resolution,[],[f321,f567]) ).
fof(f2032,plain,
( e0 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1)
| e4 = op(e2,e1)
| ~ spl34_4
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f92,f1880]) ).
fof(f2033,plain,
( e0 = op(e2,e1)
| e3 = op(e2,e1)
| e4 = op(e2,e1)
| ~ spl34_4
| ~ spl34_86
| ~ spl34_110 ),
inference(forward_subsumption_resolution,[],[f2032,f1943]) ).
fof(f2034,plain,
( e0 = op(e2,e1)
| e4 = op(e2,e1)
| ~ spl34_4
| ~ spl34_86
| ~ spl34_110 ),
inference(forward_subsumption_resolution,[],[f2033,f899]) ).
fof(f2036,definition,
( spl34_112
<=> e4 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_112])],[avatar_definition]) ).
fof(f2037,plain,
( e4 != op(e2,e1)
| spl34_112 ),
inference(avatar_component_clause,[],[f2036]) ).
fof(f2038,plain,
( e4 = op(e2,e1)
| ~ spl34_112 ),
inference(avatar_component_clause,[],[f2036]) ).
fof(f2040,definition,
( spl34_113
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_113])],[avatar_definition]) ).
fof(f2041,plain,
( e0 != op(e2,e1)
| spl34_113 ),
inference(avatar_component_clause,[],[f2040]) ).
fof(f2042,plain,
( e0 = op(e2,e1)
| ~ spl34_113 ),
inference(avatar_component_clause,[],[f2040]) ).
fof(f2043,plain,
( spl34_112
| spl34_113
| ~ spl34_4
| ~ spl34_86
| ~ spl34_110 ),
inference(avatar_split_clause,[],[f2034,f1933,f970,f447,f2040,f2036]) ).
fof(f2044,plain,
( e4 != op(e2,e2)
| ~ spl34_112 ),
inference(superposition,[],[f190,f2038]) ).
fof(f2052,plain,
( $false
| ~ spl34_112 ),
inference(forward_subsumption_resolution,[],[f2044,f430]) ).
fof(f2053,plain,
~ spl34_112,
inference(avatar_contradiction_clause,[],[f2052]) ).
fof(f2056,plain,
( e2 = op(e1,e0)
| ~ spl34_76
| ~ spl34_113 ),
inference(superposition,[],[f847,f2042]) ).
fof(f2065,plain,
( e1 = e2
| ~ spl34_76
| ~ spl34_86
| ~ spl34_113 ),
inference(superposition,[],[f2056,f1469]) ).
fof(f2080,plain,
( $false
| ~ spl34_76
| ~ spl34_86
| ~ spl34_113 ),
inference(forward_subsumption_resolution,[],[f2065,f270]) ).
fof(f2081,plain,
( ~ spl34_76
| ~ spl34_86
| ~ spl34_113 ),
inference(avatar_contradiction_clause,[],[f2080]) ).
fof(f2083,plain,
( e0 = op(e2,e1)
| e2 = op(e2,e1)
| e4 = op(e2,e1)
| ~ spl34_4
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f2032,f899]) ).
fof(f2084,plain,
( e0 = op(e2,e1)
| e2 = op(e2,e1)
| ~ spl34_4
| ~ spl34_86
| spl34_112 ),
inference(forward_subsumption_resolution,[],[f2083,f2037]) ).
fof(f2085,plain,
( e0 != op(e3,e2)
| ~ spl34_111 ),
inference(superposition,[],[f180,f1939]) ).
fof(f2097,plain,
( $false
| ~ spl34_109
| ~ spl34_111 ),
inference(forward_subsumption_resolution,[],[f2085,f1907]) ).
fof(f2098,plain,
( ~ spl34_109
| ~ spl34_111 ),
inference(avatar_contradiction_clause,[],[f2097]) ).
fof(f2135,plain,
( e4 = op(e1,e3)
| ~ sP30
| ~ spl34_96 ),
inference(forward_demodulation,[],[f285,f1441]) ).
fof(f2138,plain,
( ~ sP30
| ~ spl34_92
| ~ spl34_96 ),
inference(forward_subsumption_resolution,[],[f2135,f1395]) ).
fof(f2141,plain,
( ~ spl34_8
| ~ spl34_92
| ~ spl34_96 ),
inference(avatar_split_clause,[],[f2138,f1439,f1379,f467]) ).
fof(f2143,plain,
( e3 = op(e1,e2)
| ~ sP31
| ~ spl34_110 ),
inference(forward_demodulation,[],[f283,f1935]) ).
fof(f2146,plain,
( ~ sP31
| spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109
| ~ spl34_110 ),
inference(forward_subsumption_resolution,[],[f2143,f1958]) ).
fof(f2149,plain,
( ~ spl34_6
| spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109
| ~ spl34_110 ),
inference(avatar_split_clause,[],[f2146,f1933,f1905,f1850,f753,f738,f606,f458]) ).
fof(f2150,plain,
( e3 = op(e1,e2)
| ~ spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(forward_demodulation,[],[f607,f1954]) ).
fof(f2162,plain,
( e1 = op(e1,e4)
| e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4) ),
inference(forward_subsumption_resolution,[],[f94,f938]) ).
fof(f2163,plain,
( e2 = op(e1,e4)
| e3 = op(e1,e4)
| e4 = op(e1,e4) ),
inference(forward_subsumption_resolution,[],[f2162,f949]) ).
fof(f2165,definition,
( spl34_114
<=> e4 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl34_114])],[avatar_definition]) ).
fof(f2167,plain,
( e4 = op(e1,e4)
| ~ spl34_114 ),
inference(avatar_component_clause,[],[f2165]) ).
fof(f2169,definition,
( spl34_115
<=> e3 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl34_115])],[avatar_definition]) ).
fof(f2170,plain,
( e3 != op(e1,e4)
| spl34_115 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2171,plain,
( e3 = op(e1,e4)
| ~ spl34_115 ),
inference(avatar_component_clause,[],[f2169]) ).
fof(f2173,definition,
( spl34_116
<=> e2 = op(e1,e4) ),
introduced(definition,[new_symbols(definition,[spl34_116])],[avatar_definition]) ).
fof(f2175,plain,
( e2 = op(e1,e4)
| ~ spl34_116 ),
inference(avatar_component_clause,[],[f2173]) ).
fof(f2176,plain,
( spl34_114
| spl34_115
| spl34_116 ),
inference(avatar_split_clause,[],[f2163,f2173,f2169,f2165]) ).
fof(f2182,plain,
( e4 != op(e0,e4)
| ~ spl34_114 ),
inference(superposition,[],[f224,f2167]) ).
fof(f2187,plain,
( $false
| ~ spl34_86
| ~ spl34_114 ),
inference(forward_subsumption_resolution,[],[f2182,f1464]) ).
fof(f2188,plain,
( ~ spl34_86
| ~ spl34_114 ),
inference(avatar_contradiction_clause,[],[f2187]) ).
fof(f2210,plain,
( e3 != op(e2,e4)
| ~ spl34_115 ),
inference(superposition,[],[f220,f2171]) ).
fof(f2218,plain,
( $false
| ~ spl34_115 ),
inference(forward_subsumption_resolution,[],[f2210,f896]) ).
fof(f2219,plain,
~ spl34_115,
inference(avatar_contradiction_clause,[],[f2218]) ).
fof(f2236,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e3 = op(e1,e3)
| e4 = op(e1,e3)
| ~ spl34_59 ),
inference(forward_subsumption_resolution,[],[f95,f1737]) ).
fof(f2237,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e3 = op(e1,e3)
| ~ spl34_59
| ~ spl34_92 ),
inference(forward_subsumption_resolution,[],[f2236,f1395]) ).
fof(f2239,definition,
( spl34_117
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl34_117])],[avatar_definition]) ).
fof(f2240,plain,
( e3 != op(e1,e3)
| spl34_117 ),
inference(avatar_component_clause,[],[f2239]) ).
fof(f2241,plain,
( e3 = op(e1,e3)
| ~ spl34_117 ),
inference(avatar_component_clause,[],[f2239]) ).
fof(f2243,definition,
( spl34_118
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl34_118])],[avatar_definition]) ).
fof(f2245,plain,
( e1 = op(e1,e3)
| ~ spl34_118 ),
inference(avatar_component_clause,[],[f2243]) ).
fof(f2247,definition,
( spl34_119
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl34_119])],[avatar_definition]) ).
fof(f2249,plain,
( e0 = op(e1,e3)
| ~ spl34_119 ),
inference(avatar_component_clause,[],[f2247]) ).
fof(f2250,plain,
( spl34_117
| spl34_118
| spl34_119
| ~ spl34_59
| ~ spl34_92 ),
inference(avatar_split_clause,[],[f2237,f1379,f738,f2247,f2243,f2239]) ).
fof(f2255,plain,
( e3 != op(e0,e3)
| ~ spl34_117 ),
inference(superposition,[],[f234,f2241]) ).
fof(f2263,plain,
( $false
| ~ spl34_58
| ~ spl34_86
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f2255,f1684]) ).
fof(f2264,plain,
( ~ spl34_58
| ~ spl34_86
| ~ spl34_117 ),
inference(avatar_contradiction_clause,[],[f2263]) ).
fof(f2276,plain,
( e1 = op(e0,e3)
| ~ spl34_30
| ~ spl34_119 ),
inference(superposition,[],[f2031,f2249]) ).
fof(f2282,plain,
( e1 != op(e0,e1)
| ~ spl34_30
| ~ spl34_119 ),
inference(superposition,[],[f209,f2276]) ).
fof(f2292,plain,
( $false
| ~ spl34_4
| ~ spl34_30
| ~ spl34_86
| ~ spl34_119 ),
inference(forward_subsumption_resolution,[],[f2282,f1874]) ).
fof(f2293,plain,
( ~ spl34_4
| ~ spl34_30
| ~ spl34_86
| ~ spl34_119 ),
inference(avatar_contradiction_clause,[],[f2292]) ).
fof(f2298,plain,
( e1 != op(e1,e0)
| ~ spl34_118 ),
inference(superposition,[],[f202,f2245]) ).
fof(f2311,plain,
( $false
| ~ spl34_86
| ~ spl34_118 ),
inference(forward_subsumption_resolution,[],[f2298,f1469]) ).
fof(f2312,plain,
( ~ spl34_86
| ~ spl34_118 ),
inference(avatar_contradiction_clause,[],[f2311]) ).
fof(f2315,plain,
( e3 = op(e1,e4)
| ~ sP5 ),
inference(forward_demodulation,[],[f354,f943]) ).
fof(f2321,plain,
( ~ sP5
| spl34_115 ),
inference(forward_subsumption_resolution,[],[f2315,f2170]) ).
fof(f2338,plain,
( ~ spl34_48
| spl34_115 ),
inference(avatar_split_clause,[],[f2321,f2169,f647]) ).
fof(f2340,plain,
( e4 != op(e0,e4)
| ~ sP20
| ~ spl34_101 ),
inference(forward_demodulation,[],[f310,f1551]) ).
fof(f2344,plain,
( sP22
| sP21
| sP20
| sP19
| sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18 ),
inference(forward_subsumption_resolution,[],[f433,f514]) ).
fof(f2347,plain,
( ~ sP20
| ~ spl34_86
| ~ spl34_101 ),
inference(forward_subsumption_resolution,[],[f2340,f1464]) ).
fof(f2350,plain,
( sP21
| sP20
| sP19
| sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20 ),
inference(forward_subsumption_resolution,[],[f2344,f523]) ).
fof(f2353,plain,
( sP20
| sP19
| sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22 ),
inference(forward_subsumption_resolution,[],[f2350,f532]) ).
fof(f2411,plain,
( e1 != op(e0,e1)
| ~ sP19
| ~ spl34_86 ),
inference(forward_demodulation,[],[f313,f1469]) ).
fof(f2416,plain,
( ~ sP19
| ~ spl34_4
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f2411,f1874]) ).
fof(f2466,plain,
( ~ spl34_24
| ~ spl34_86
| ~ spl34_101 ),
inference(avatar_split_clause,[],[f2347,f1549,f970,f539]) ).
fof(f2467,plain,
( ~ spl34_26
| ~ spl34_4
| ~ spl34_86 ),
inference(avatar_split_clause,[],[f2416,f970,f447,f548]) ).
fof(f2470,plain,
( e2 = op(e3,e4)
| ~ sP10 ),
inference(forward_demodulation,[],[f339,f896]) ).
fof(f2475,plain,
( e1 = e2
| ~ sP10 ),
inference(forward_demodulation,[],[f2470,f943]) ).
fof(f2479,plain,
~ sP10,
inference(forward_subsumption_resolution,[],[f2475,f270]) ).
fof(f2504,plain,
~ spl34_40,
inference(avatar_split_clause,[],[f2479,f611]) ).
fof(f2507,plain,
( e2 = op(e0,e1)
| ~ sP13
| ~ spl34_113 ),
inference(forward_demodulation,[],[f330,f2042]) ).
fof(f2511,plain,
( e1 = e2
| ~ sP13
| ~ spl34_4
| ~ spl34_86
| ~ spl34_113 ),
inference(forward_demodulation,[],[f2507,f1874]) ).
fof(f2515,plain,
( ~ sP13
| ~ spl34_4
| ~ spl34_86
| ~ spl34_113 ),
inference(forward_subsumption_resolution,[],[f2511,f270]) ).
fof(f2545,plain,
( ~ spl34_36
| ~ spl34_4
| ~ spl34_86
| ~ spl34_113 ),
inference(avatar_split_clause,[],[f2515,f2040,f970,f447,f593]) ).
fof(f2548,plain,
( e1 = op(e3,e2)
| ~ sP17
| ~ spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(forward_demodulation,[],[f318,f2150]) ).
fof(f2554,plain,
( ~ sP17
| ~ spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f2548,f945]) ).
fof(f2599,plain,
( e1 = op(e2,e4)
| ~ sP15
| ~ spl34_116 ),
inference(forward_demodulation,[],[f324,f2175]) ).
fof(f2603,plain,
( e1 = e3
| ~ sP15
| ~ spl34_116 ),
inference(forward_demodulation,[],[f2599,f896]) ).
fof(f2607,plain,
( ~ sP15
| ~ spl34_116 ),
inference(forward_subsumption_resolution,[],[f2603,f269]) ).
fof(f2640,plain,
( ~ spl34_28
| ~ spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(avatar_split_clause,[],[f2554,f1905,f1850,f753,f738,f606,f557]) ).
fof(f2641,plain,
( ~ spl34_32
| ~ spl34_116 ),
inference(avatar_split_clause,[],[f2607,f2173,f575]) ).
fof(f2644,plain,
( e3 = op(e2,e1)
| ~ sP8
| ~ spl34_110 ),
inference(forward_demodulation,[],[f345,f1935]) ).
fof(f2650,plain,
( ~ sP8
| ~ spl34_110 ),
inference(forward_subsumption_resolution,[],[f2644,f899]) ).
fof(f2674,plain,
( e4 != op(e0,e4)
| ~ sP4
| ~ spl34_101 ),
inference(forward_demodulation,[],[f358,f1551]) ).
fof(f2681,plain,
( ~ sP4
| ~ spl34_86
| ~ spl34_101 ),
inference(forward_subsumption_resolution,[],[f2674,f1464]) ).
fof(f2698,plain,
( e4 = op(e3,e1)
| ~ sP3
| ~ spl34_96 ),
inference(forward_demodulation,[],[f360,f1441]) ).
fof(f2704,plain,
( ~ sP3
| ~ spl34_92
| ~ spl34_96 ),
inference(forward_subsumption_resolution,[],[f2698,f1392]) ).
fof(f2717,plain,
( e3 = op(e0,e2)
| ~ sP7
| ~ spl34_109 ),
inference(forward_demodulation,[],[f348,f1907]) ).
fof(f2722,plain,
( ~ sP7
| ~ spl34_58
| ~ spl34_86
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f2717,f1685]) ).
fof(f2735,plain,
( ~ spl34_44
| ~ spl34_110 ),
inference(avatar_split_clause,[],[f2650,f1933,f629]) ).
fof(f2736,plain,
( ~ spl34_50
| ~ spl34_86
| ~ spl34_101 ),
inference(avatar_split_clause,[],[f2681,f1549,f970,f656]) ).
fof(f2737,plain,
( ~ spl34_52
| ~ spl34_92
| ~ spl34_96 ),
inference(avatar_split_clause,[],[f2704,f1439,f1379,f665]) ).
fof(f2738,plain,
( ~ spl34_46
| ~ spl34_58
| ~ spl34_86
| ~ spl34_109 ),
inference(avatar_split_clause,[],[f2722,f1905,f970,f730,f638]) ).
fof(f2739,plain,
( e2 != op(e1,e4)
| spl34_55
| ~ spl34_88 ),
inference(forward_demodulation,[],[f680,f1170]) ).
fof(f2745,plain,
( $false
| spl34_55
| ~ spl34_88
| ~ spl34_116 ),
inference(forward_subsumption_resolution,[],[f2739,f2175]) ).
fof(f2746,plain,
( spl34_55
| ~ spl34_88
| ~ spl34_116 ),
inference(avatar_contradiction_clause,[],[f2745]) ).
fof(f2799,plain,
( e3 != op(e0,e3)
| ~ sP9
| ~ spl34_86 ),
inference(forward_demodulation,[],[f343,f1465]) ).
fof(f2805,plain,
( ~ sP9
| ~ spl34_58
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f2799,f1684]) ).
fof(f2827,plain,
( ~ spl34_42
| ~ spl34_58
| ~ spl34_86 ),
inference(avatar_split_clause,[],[f2805,f970,f730,f620]) ).
fof(f2829,plain,
( e2 != op(e0,e2)
| ~ sP14
| ~ spl34_86 ),
inference(forward_demodulation,[],[f328,f1467]) ).
fof(f2835,plain,
( ~ sP14
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f2829,f1468]) ).
fof(f2884,plain,
( ~ spl34_34
| ~ spl34_86 ),
inference(avatar_split_clause,[],[f2835,f970,f584]) ).
fof(f2885,plain,
( sP19
| sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24 ),
inference(forward_subsumption_resolution,[],[f2353,f541]) ).
fof(f2888,plain,
( sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26 ),
inference(forward_subsumption_resolution,[],[f2885,f550]) ).
fof(f2958,plain,
( e1 != op(e0,e1)
| ~ spl34_97 ),
inference(superposition,[],[f251,f1445]) ).
fof(f2965,plain,
( $false
| ~ spl34_4
| ~ spl34_86
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f2958,f1874]) ).
fof(f2966,plain,
( ~ spl34_4
| ~ spl34_86
| ~ spl34_97 ),
inference(avatar_contradiction_clause,[],[f2965]) ).
fof(f2970,plain,
( e2 != op(e2,e1)
| ~ spl34_103 ),
inference(superposition,[],[f246,f1569]) ).
fof(f2987,definition,
( spl34_120
<=> op(e1,e3) = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl34_120])],[avatar_definition]) ).
fof(f2988,plain,
( op(e1,e3) = op(e3,e1)
| ~ spl34_120 ),
inference(avatar_component_clause,[],[f2987]) ).
fof(f2989,plain,
( op(e1,e3) != op(e3,e1)
| spl34_120 ),
inference(avatar_component_clause,[],[f2987]) ).
fof(f2995,plain,
( e1 != op(e2,e3)
| ~ spl34_106 ),
inference(superposition,[],[f226,f1646]) ).
fof(f3024,plain,
( e0 = op(e2,e3)
| ~ spl34_107
| ~ spl34_109 ),
inference(forward_demodulation,[],[f1851,f1907]) ).
fof(f3025,plain,
( e0 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3)
| e4 = op(e2,e3)
| ~ spl34_106 ),
inference(forward_subsumption_resolution,[],[f90,f2995]) ).
fof(f3026,plain,
( e0 = op(e2,e3)
| e2 = op(e2,e3)
| e4 = op(e2,e3)
| ~ spl34_106 ),
inference(forward_subsumption_resolution,[],[f3025,f897]) ).
fof(f3027,plain,
( e0 = op(e2,e3)
| e2 = op(e2,e3)
| spl34_62
| ~ spl34_106 ),
inference(forward_subsumption_resolution,[],[f3026,f923]) ).
fof(f3029,plain,
( e0 != op(e2,e1)
| ~ spl34_107
| ~ spl34_109 ),
inference(superposition,[],[f189,f3024]) ).
fof(f3037,plain,
( $false
| ~ spl34_107
| ~ spl34_109
| ~ spl34_113 ),
inference(forward_subsumption_resolution,[],[f3029,f2042]) ).
fof(f3038,plain,
( ~ spl34_107
| ~ spl34_109
| ~ spl34_113 ),
inference(avatar_contradiction_clause,[],[f3037]) ).
fof(f3064,plain,
( e0 = op(e3,e2)
| e4 = op(e3,e2)
| ~ spl34_86
| spl34_108 ),
inference(forward_subsumption_resolution,[],[f1898,f1902]) ).
fof(f3087,plain,
( e2 = op(e2,e1)
| ~ spl34_4
| ~ spl34_86
| spl34_112
| spl34_113 ),
inference(forward_subsumption_resolution,[],[f2084,f2041]) ).
fof(f3088,plain,
( $false
| ~ spl34_4
| ~ spl34_86
| ~ spl34_103
| spl34_112
| spl34_113 ),
inference(forward_subsumption_resolution,[],[f3087,f2970]) ).
fof(f3089,plain,
( ~ spl34_4
| ~ spl34_86
| ~ spl34_103
| spl34_112
| spl34_113 ),
inference(avatar_contradiction_clause,[],[f3088]) ).
fof(f3106,definition,
( spl34_121
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl34_121])],[avatar_definition]) ).
fof(f3108,plain,
( e2 = op(e2,e3)
| ~ spl34_121 ),
inference(avatar_component_clause,[],[f3106]) ).
fof(f3110,definition,
( spl34_122
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl34_122])],[avatar_definition]) ).
fof(f3112,plain,
( e0 = op(e2,e3)
| ~ spl34_122 ),
inference(avatar_component_clause,[],[f3110]) ).
fof(f3113,plain,
( spl34_121
| spl34_122
| spl34_62
| ~ spl34_106 ),
inference(avatar_split_clause,[],[f3027,f1644,f753,f3110,f3106]) ).
fof(f3116,plain,
( e2 != op(e2,e0)
| ~ spl34_121 ),
inference(superposition,[],[f192,f3108]) ).
fof(f3125,plain,
( $false
| ~ spl34_86
| ~ spl34_121 ),
inference(forward_subsumption_resolution,[],[f3116,f1467]) ).
fof(f3126,plain,
( ~ spl34_86
| ~ spl34_121 ),
inference(avatar_contradiction_clause,[],[f3125]) ).
fof(f3129,plain,
( e0 != op(e2,e1)
| ~ spl34_122 ),
inference(superposition,[],[f189,f3112]) ).
fof(f3138,plain,
( $false
| ~ spl34_113
| ~ spl34_122 ),
inference(forward_subsumption_resolution,[],[f3129,f2042]) ).
fof(f3139,plain,
( ~ spl34_113
| ~ spl34_122 ),
inference(avatar_contradiction_clause,[],[f3138]) ).
fof(f3197,plain,
( e3 != op(e4,e0)
| ~ spl34_96 ),
inference(superposition,[],[f174,f1441]) ).
fof(f3210,plain,
( e2 != op(e2,e0)
| ~ spl34_102 ),
inference(superposition,[],[f256,f1555]) ).
fof(f3219,plain,
( $false
| ~ spl34_86
| ~ spl34_102 ),
inference(forward_subsumption_resolution,[],[f3210,f1467]) ).
fof(f3220,plain,
( ~ spl34_86
| ~ spl34_102 ),
inference(avatar_contradiction_clause,[],[f3219]) ).
fof(f3222,plain,
( e2 = op(e4,e3)
| ~ spl34_59 ),
inference(forward_demodulation,[],[f740,f896]) ).
fof(f3226,plain,
( e3 != op(e3,e0)
| ~ spl34_93 ),
inference(superposition,[],[f182,f1385]) ).
fof(f3235,plain,
( $false
| ~ spl34_86
| ~ spl34_93 ),
inference(forward_subsumption_resolution,[],[f3226,f1465]) ).
fof(f3236,plain,
( ~ spl34_86
| ~ spl34_93 ),
inference(avatar_contradiction_clause,[],[f3235]) ).
fof(f3309,plain,
( e3 != op(e2,e4)
| spl34_57
| ~ spl34_59 ),
inference(superposition,[],[f689,f3222]) ).
fof(f3314,plain,
( $false
| spl34_57
| ~ spl34_59 ),
inference(forward_subsumption_resolution,[],[f3309,f896]) ).
fof(f3315,plain,
( spl34_57
| ~ spl34_59 ),
inference(avatar_contradiction_clause,[],[f3314]) ).
fof(f3320,plain,
( e1 != op(e0,op(e0,e1))
| e1 = op(e1,op(e1,e1))
| sP31
| sP30
| spl34_76 ),
inference(forward_subsumption_resolution,[],[f402,f846]) ).
fof(f3321,plain,
( e1 != op(e0,op(e0,e1))
| e1 != op(e1,op(e1,e1))
| sP31
| sP30
| spl34_76 ),
inference(forward_subsumption_resolution,[],[f404,f846]) ).
fof(f3324,plain,
( sP17
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30 ),
inference(forward_subsumption_resolution,[],[f2888,f568]) ).
fof(f3330,plain,
( e1 != op(e0,e1)
| e1 = op(e1,op(e1,e1))
| sP31
| sP30
| ~ spl34_4
| spl34_76
| ~ spl34_86 ),
inference(forward_demodulation,[],[f3320,f1874]) ).
fof(f3331,plain,
( e1 != op(e0,e1)
| e1 != op(e1,op(e1,e1))
| sP31
| sP30
| ~ spl34_4
| spl34_76
| ~ spl34_86 ),
inference(forward_demodulation,[],[f3321,f1874]) ).
fof(f3334,plain,
( sP17
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32 ),
inference(forward_subsumption_resolution,[],[f3324,f577]) ).
fof(f3338,plain,
( e1 = op(e1,op(e1,e1))
| sP31
| sP30
| ~ spl34_4
| spl34_76
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f3330,f1874]) ).
fof(f3339,plain,
( e1 != op(e1,op(e1,e1))
| sP31
| sP30
| ~ spl34_4
| spl34_76
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f3331,f1874]) ).
fof(f3345,plain,
( sP31
| sP30
| ~ spl34_4
| spl34_76
| ~ spl34_86 ),
inference(global_subsumption,[],[f3339,f3338]) ).
fof(f3399,plain,
( sP30
| ~ spl34_4
| spl34_6
| spl34_76
| ~ spl34_86 ),
inference(forward_subsumption_resolution,[],[f3345,f460]) ).
fof(f3400,plain,
( spl34_8
| ~ spl34_4
| spl34_6
| spl34_76
| ~ spl34_86 ),
inference(avatar_split_clause,[],[f3399,f970,f845,f458,f447,f467]) ).
fof(f3404,plain,
( e0 != op(e3,e2)
| ~ spl34_94 ),
inference(superposition,[],[f177,f1389]) ).
fof(f3416,plain,
( $false
| ~ spl34_94
| ~ spl34_109 ),
inference(forward_subsumption_resolution,[],[f3404,f1907]) ).
fof(f3417,plain,
( ~ spl34_94
| ~ spl34_109 ),
inference(avatar_contradiction_clause,[],[f3416]) ).
fof(f3442,plain,
( e4 = op(e3,e2)
| ~ spl34_86
| spl34_108
| spl34_109 ),
inference(forward_subsumption_resolution,[],[f3064,f1906]) ).
fof(f3446,plain,
( e4 != op(e2,e2)
| ~ spl34_86
| spl34_108
| spl34_109 ),
inference(superposition,[],[f237,f3442]) ).
fof(f3457,plain,
( $false
| ~ spl34_86
| spl34_108
| spl34_109 ),
inference(forward_subsumption_resolution,[],[f3446,f430]) ).
fof(f3458,plain,
( ~ spl34_86
| spl34_108
| spl34_109 ),
inference(avatar_contradiction_clause,[],[f3457]) ).
fof(f3460,plain,
( e1 != op(e0,e1)
| spl34_4
| ~ spl34_86 ),
inference(forward_demodulation,[],[f448,f1469]) ).
fof(f3471,plain,
( $false
| spl34_4
| ~ spl34_86 ),
inference(global_subsumption,[],[f3460,f1470]) ).
fof(f3472,plain,
( spl34_4
| ~ spl34_86 ),
inference(avatar_contradiction_clause,[],[f3471]) ).
fof(f3496,plain,
( e0 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0)
| e4 = op(e3,e0) ),
inference(forward_subsumption_resolution,[],[f88,f947]) ).
fof(f3497,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e4 = op(e2,e0) ),
inference(forward_subsumption_resolution,[],[f93,f900]) ).
fof(f3520,plain,
( $false
| ~ spl34_89
| ~ spl34_96 ),
inference(forward_subsumption_resolution,[],[f3197,f1186]) ).
fof(f3521,plain,
( ~ spl34_89
| ~ spl34_96 ),
inference(avatar_contradiction_clause,[],[f3520]) ).
fof(f3584,plain,
( e3 = op(e3,e1)
| ~ spl34_85 ),
inference(superposition,[],[f107,f968]) ).
fof(f3585,plain,
( e3 = op(e1,e3)
| ~ spl34_85 ),
inference(superposition,[],[f108,f968]) ).
fof(f3586,plain,
( e2 = op(e2,e1)
| ~ spl34_85 ),
inference(superposition,[],[f109,f968]) ).
fof(f3587,plain,
( e2 = op(e1,e2)
| ~ spl34_85 ),
inference(superposition,[],[f110,f968]) ).
fof(f3590,plain,
( e0 = op(e0,e1)
| ~ spl34_85 ),
inference(superposition,[],[f113,f968]) ).
fof(f3598,plain,
( $false
| ~ spl34_85
| spl34_117 ),
inference(forward_subsumption_resolution,[],[f3585,f2240]) ).
fof(f3599,plain,
( ~ spl34_85
| spl34_117 ),
inference(avatar_contradiction_clause,[],[f3598]) ).
fof(f3692,definition,
( spl34_125
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_125])],[avatar_definition]) ).
fof(f3693,plain,
( e2 != op(e3,e0)
| spl34_125 ),
inference(avatar_component_clause,[],[f3692]) ).
fof(f3694,plain,
( e2 = op(e3,e0)
| ~ spl34_125 ),
inference(avatar_component_clause,[],[f3692]) ).
fof(f3696,definition,
( spl34_126
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_126])],[avatar_definition]) ).
fof(f3697,plain,
( e0 != op(e3,e0)
| spl34_126 ),
inference(avatar_component_clause,[],[f3696]) ).
fof(f3698,plain,
( e0 = op(e3,e0)
| ~ spl34_126 ),
inference(avatar_component_clause,[],[f3696]) ).
fof(f3719,plain,
( e2 != op(e2,e0)
| ~ spl34_85 ),
inference(superposition,[],[f194,f3586]) ).
fof(f3721,plain,
( e2 != op(e1,e2)
| spl34_76
| ~ spl34_85 ),
inference(superposition,[],[f846,f3586]) ).
fof(f3729,plain,
( $false
| spl34_76
| ~ spl34_85 ),
inference(global_subsumption,[],[f3721,f3587]) ).
fof(f3730,plain,
( spl34_76
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f3729]) ).
fof(f3735,plain,
( e2 = op(e1,e2)
| ~ spl34_76
| ~ spl34_85 ),
inference(forward_demodulation,[],[f847,f3586]) ).
fof(f3756,plain,
( sP17
| sP14
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36 ),
inference(forward_subsumption_resolution,[],[f3334,f595]) ).
fof(f3760,plain,
( sP17
| sP14
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38 ),
inference(forward_subsumption_resolution,[],[f3756,f604]) ).
fof(f3764,plain,
( sP17
| sP14
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40 ),
inference(forward_subsumption_resolution,[],[f3760,f613]) ).
fof(f3767,plain,
( sP17
| sP14
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42 ),
inference(forward_subsumption_resolution,[],[f3764,f622]) ).
fof(f3770,plain,
( sP17
| sP14
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44 ),
inference(forward_subsumption_resolution,[],[f3767,f631]) ).
fof(f3773,plain,
( sP17
| sP14
| sP5
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46 ),
inference(forward_subsumption_resolution,[],[f3770,f640]) ).
fof(f3776,plain,
( sP17
| sP14
| sP4
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48 ),
inference(forward_subsumption_resolution,[],[f3773,f649]) ).
fof(f3779,plain,
( sP17
| sP14
| sP3
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48
| spl34_50 ),
inference(forward_subsumption_resolution,[],[f3776,f658]) ).
fof(f3782,plain,
( sP17
| sP14
| sP2
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48
| spl34_50
| spl34_52 ),
inference(forward_subsumption_resolution,[],[f3779,f667]) ).
fof(f3785,plain,
( sP17
| sP14
| sP1
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48
| spl34_50
| spl34_52
| spl34_54 ),
inference(forward_subsumption_resolution,[],[f3782,f676]) ).
fof(f3788,plain,
( sP17
| sP14
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48
| spl34_50
| spl34_52
| spl34_54
| spl34_56 ),
inference(forward_subsumption_resolution,[],[f3785,f685]) ).
fof(f3798,plain,
( spl34_34
| spl34_28
| spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_30
| spl34_32
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48
| spl34_50
| spl34_52
| spl34_54
| spl34_56 ),
inference(avatar_split_clause,[],[f3788,f683,f674,f665,f656,f647,f638,f629,f620,f611,f602,f593,f575,f566,f548,f539,f530,f521,f512,f557,f584]) ).
fof(f3819,definition,
( spl34_127
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_127])],[avatar_definition]) ).
fof(f3820,plain,
( e4 != op(e2,e0)
| spl34_127 ),
inference(avatar_component_clause,[],[f3819]) ).
fof(f3821,plain,
( e4 = op(e2,e0)
| ~ spl34_127 ),
inference(avatar_component_clause,[],[f3819]) ).
fof(f3823,definition,
( spl34_128
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_128])],[avatar_definition]) ).
fof(f3824,plain,
( e0 != op(e2,e0)
| spl34_128 ),
inference(avatar_component_clause,[],[f3823]) ).
fof(f3827,plain,
( e4 != op(e2,e2)
| ~ spl34_127 ),
inference(superposition,[],[f193,f3821]) ).
fof(f3835,plain,
( $false
| ~ spl34_127 ),
inference(forward_subsumption_resolution,[],[f3827,f430]) ).
fof(f3836,plain,
~ spl34_127,
inference(avatar_contradiction_clause,[],[f3835]) ).
fof(f3851,plain,
( e0 != op(e3,e2)
| ~ spl34_126 ),
inference(superposition,[],[f183,f3698]) ).
fof(f3860,plain,
( $false
| ~ spl34_109
| ~ spl34_126 ),
inference(forward_subsumption_resolution,[],[f3851,f1907]) ).
fof(f3861,plain,
( ~ spl34_109
| ~ spl34_126 ),
inference(avatar_contradiction_clause,[],[f3860]) ).
fof(f3872,plain,
( e0 != op(e3,e2)
| spl34_5
| ~ spl34_125 ),
inference(superposition,[],[f454,f3694]) ).
fof(f3877,plain,
( $false
| spl34_5
| ~ spl34_109
| ~ spl34_125 ),
inference(forward_subsumption_resolution,[],[f3872,f1907]) ).
fof(f3878,plain,
( spl34_5
| ~ spl34_109
| ~ spl34_125 ),
inference(avatar_contradiction_clause,[],[f3877]) ).
fof(f3881,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e4 = op(e2,e0)
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f3497,f3719]) ).
fof(f3882,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| ~ spl34_85
| spl34_127 ),
inference(forward_subsumption_resolution,[],[f3881,f3820]) ).
fof(f3906,plain,
( e3 != op(e1,e3)
| ~ spl34_93 ),
inference(superposition,[],[f229,f1385]) ).
fof(f3912,plain,
( $false
| ~ spl34_93
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f3906,f2241]) ).
fof(f3913,plain,
( ~ spl34_93
| ~ spl34_117 ),
inference(avatar_contradiction_clause,[],[f3912]) ).
fof(f3930,plain,
( e1 = op(e2,e0)
| ~ spl34_85
| spl34_127
| spl34_128 ),
inference(forward_subsumption_resolution,[],[f3882,f3824]) ).
fof(f3932,plain,
( e2 = op(e0,e1)
| ~ spl34_3
| ~ spl34_85
| spl34_127
| spl34_128 ),
inference(superposition,[],[f445,f3930]) ).
fof(f3943,plain,
( e2 != op(e2,e1)
| ~ spl34_3
| ~ spl34_85
| spl34_127
| spl34_128 ),
inference(superposition,[],[f253,f3932]) ).
fof(f3950,plain,
( $false
| ~ spl34_3
| ~ spl34_85
| spl34_127
| spl34_128 ),
inference(forward_subsumption_resolution,[],[f3943,f3586]) ).
fof(f3951,plain,
( ~ spl34_3
| ~ spl34_85
| spl34_127
| spl34_128 ),
inference(avatar_contradiction_clause,[],[f3950]) ).
fof(f4008,plain,
( e1 != op(e4,e2)
| ~ spl34_97 ),
inference(superposition,[],[f170,f1445]) ).
fof(f4019,plain,
( $false
| ~ spl34_88
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f4008,f1170]) ).
fof(f4020,plain,
( ~ spl34_88
| ~ spl34_97 ),
inference(avatar_contradiction_clause,[],[f4019]) ).
fof(f4022,plain,
( e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2)
| spl34_109 ),
inference(forward_subsumption_resolution,[],[f1897,f1906]) ).
fof(f4029,plain,
( e4 != op(e0,e1)
| ~ spl34_95 ),
inference(superposition,[],[f251,f1437]) ).
fof(f4036,plain,
( e2 != op(e1,e2)
| ~ spl34_108 ),
inference(superposition,[],[f239,f1903]) ).
fof(f4043,plain,
( $false
| ~ spl34_76
| ~ spl34_85
| ~ spl34_108 ),
inference(forward_subsumption_resolution,[],[f4036,f3735]) ).
fof(f4044,plain,
( ~ spl34_76
| ~ spl34_85
| ~ spl34_108 ),
inference(avatar_contradiction_clause,[],[f4043]) ).
fof(f4052,plain,
( e3 = op(e3,e1)
| ~ spl34_117
| ~ spl34_120 ),
inference(forward_demodulation,[],[f2988,f2241]) ).
fof(f4070,plain,
( e3 != op(e3,e2)
| ~ spl34_117
| ~ spl34_120 ),
inference(superposition,[],[f180,f4052]) ).
fof(f4096,plain,
( e3 = op(e3,e2)
| e4 = op(e3,e2)
| spl34_108
| spl34_109 ),
inference(forward_subsumption_resolution,[],[f4022,f1902]) ).
fof(f4097,plain,
( e4 = op(e3,e2)
| spl34_108
| spl34_109
| ~ spl34_117
| ~ spl34_120 ),
inference(forward_subsumption_resolution,[],[f4096,f4070]) ).
fof(f4098,plain,
( e4 != op(e2,e2)
| spl34_108
| spl34_109
| ~ spl34_117
| ~ spl34_120 ),
inference(superposition,[],[f237,f4097]) ).
fof(f4109,plain,
( $false
| spl34_108
| spl34_109
| ~ spl34_117
| ~ spl34_120 ),
inference(forward_subsumption_resolution,[],[f4098,f430]) ).
fof(f4110,plain,
( spl34_108
| spl34_109
| ~ spl34_117
| ~ spl34_120 ),
inference(avatar_contradiction_clause,[],[f4109]) ).
fof(f4112,plain,
( e3 != op(e3,e1)
| ~ spl34_117
| spl34_120 ),
inference(forward_demodulation,[],[f2989,f2241]) ).
fof(f4151,plain,
( $false
| ~ spl34_85
| ~ spl34_117
| spl34_120 ),
inference(forward_subsumption_resolution,[],[f3584,f4112]) ).
fof(f4152,plain,
( ~ spl34_85
| ~ spl34_117
| spl34_120 ),
inference(avatar_contradiction_clause,[],[f4151]) ).
fof(f4153,plain,
( e3 = op(e3,e1)
| ~ spl34_117
| ~ spl34_120 ),
inference(forward_demodulation,[],[f2988,f2241]) ).
fof(f4157,plain,
( e2 = op(e3,e0)
| e3 = op(e3,e0)
| e4 = op(e3,e0)
| spl34_126 ),
inference(forward_subsumption_resolution,[],[f3496,f3697]) ).
fof(f4189,plain,
( e3 != op(e3,e0)
| ~ spl34_117
| ~ spl34_120 ),
inference(superposition,[],[f184,f4153]) ).
fof(f4234,plain,
( e2 = op(e3,e0)
| e4 = op(e3,e0)
| ~ spl34_117
| ~ spl34_120
| spl34_126 ),
inference(forward_subsumption_resolution,[],[f4157,f4189]) ).
fof(f4236,plain,
( e4 = op(e0,e1)
| ~ sP32
| ~ spl34_90 ),
inference(forward_demodulation,[],[f281,f1190]) ).
fof(f4241,plain,
( ~ sP32
| ~ spl34_90
| ~ spl34_95 ),
inference(forward_subsumption_resolution,[],[f4236,f4029]) ).
fof(f4244,plain,
( ~ spl34_1
| ~ spl34_90
| ~ spl34_95 ),
inference(avatar_split_clause,[],[f4241,f1435,f1188,f435]) ).
fof(f4248,plain,
( e1 != op(e4,e0)
| ~ spl34_97 ),
inference(superposition,[],[f174,f1445]) ).
fof(f4258,plain,
( $false
| ~ spl34_90
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f4248,f1190]) ).
fof(f4259,plain,
( ~ spl34_90
| ~ spl34_97 ),
inference(avatar_contradiction_clause,[],[f4258]) ).
fof(f4270,plain,
( e2 != op(e2,e1)
| ~ spl34_103 ),
inference(superposition,[],[f246,f1569]) ).
fof(f4277,plain,
( $false
| ~ spl34_85
| ~ spl34_103 ),
inference(forward_subsumption_resolution,[],[f4270,f3586]) ).
fof(f4278,plain,
( ~ spl34_85
| ~ spl34_103 ),
inference(avatar_contradiction_clause,[],[f4277]) ).
fof(f4281,plain,
( e0 != op(e4,op(e4,e0))
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f282,f437]) ).
fof(f4282,plain,
( e4 = op(e0,op(e4,e0))
| ~ spl34_1 ),
inference(forward_subsumption_resolution,[],[f281,f437]) ).
fof(f4329,plain,
( e0 != op(e4,e4)
| ~ spl34_1
| ~ spl34_101 ),
inference(superposition,[],[f4281,f1551]) ).
fof(f4330,plain,
( $false
| ~ spl34_1
| ~ spl34_101 ),
inference(forward_subsumption_resolution,[],[f4329,f931]) ).
fof(f4331,plain,
( ~ spl34_1
| ~ spl34_101 ),
inference(avatar_contradiction_clause,[],[f4330]) ).
fof(f4349,plain,
( e3 != op(e1,e3)
| ~ spl34_105 ),
inference(superposition,[],[f228,f1642]) ).
fof(f4355,plain,
( $false
| ~ spl34_105
| ~ spl34_117 ),
inference(forward_subsumption_resolution,[],[f4349,f2241]) ).
fof(f4356,plain,
( ~ spl34_105
| ~ spl34_117 ),
inference(avatar_contradiction_clause,[],[f4355]) ).
fof(f4392,plain,
( e4 = op(e0,e2)
| ~ spl34_1
| ~ spl34_102 ),
inference(forward_demodulation,[],[f4282,f1555]) ).
fof(f4393,plain,
( e4 != op(e2,e2)
| ~ spl34_1
| ~ spl34_102 ),
inference(superposition,[],[f243,f4392]) ).
fof(f4400,plain,
( $false
| ~ spl34_1
| ~ spl34_102 ),
inference(forward_subsumption_resolution,[],[f4393,f430]) ).
fof(f4401,plain,
( ~ spl34_1
| ~ spl34_102 ),
inference(avatar_contradiction_clause,[],[f4400]) ).
fof(f4433,plain,
( e2 != op(e1,e2)
| ~ spl34_100 ),
inference(superposition,[],[f238,f1527]) ).
fof(f4439,plain,
( $false
| ~ spl34_76
| ~ spl34_85
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f4433,f3735]) ).
fof(f4440,plain,
( ~ spl34_76
| ~ spl34_85
| ~ spl34_100 ),
inference(avatar_contradiction_clause,[],[f4439]) ).
fof(f4479,plain,
( e4 != op(e4,e1)
| ~ spl34_104 ),
inference(superposition,[],[f169,f1638]) ).
fof(f4491,plain,
( $false
| ~ spl34_95
| ~ spl34_104 ),
inference(forward_subsumption_resolution,[],[f4479,f1437]) ).
fof(f4492,plain,
( ~ spl34_95
| ~ spl34_104 ),
inference(avatar_contradiction_clause,[],[f4491]) ).
fof(f4552,plain,
( e4 = op(e3,e0)
| ~ spl34_117
| ~ spl34_120
| spl34_125
| spl34_126 ),
inference(forward_subsumption_resolution,[],[f4234,f3693]) ).
fof(f4585,plain,
( e0 = op(e1,e0)
| ~ spl34_78
| ~ spl34_85 ),
inference(superposition,[],[f855,f3590]) ).
fof(f4593,plain,
( e0 != op(e2,e0)
| ~ spl34_78
| ~ spl34_85 ),
inference(superposition,[],[f260,f4585]) ).
fof(f4597,plain,
( e0 != op(e1,e0)
| ~ spl34_78
| ~ spl34_85
| spl34_98 ),
inference(superposition,[],[f1461,f4585]) ).
fof(f4602,plain,
( $false
| ~ spl34_78
| ~ spl34_85
| spl34_98 ),
inference(forward_subsumption_resolution,[],[f4597,f4585]) ).
fof(f4603,plain,
( ~ spl34_78
| ~ spl34_85
| spl34_98 ),
inference(avatar_contradiction_clause,[],[f4602]) ).
fof(f4702,plain,
( e3 = op(e0,e4)
| ~ spl34_81
| ~ spl34_117
| ~ spl34_120
| spl34_125
| spl34_126 ),
inference(forward_demodulation,[],[f927,f4552]) ).
fof(f4710,plain,
( e3 != op(e2,e4)
| ~ spl34_81
| ~ spl34_117
| ~ spl34_120
| spl34_125
| spl34_126 ),
inference(superposition,[],[f223,f4702]) ).
fof(f4721,plain,
( $false
| ~ spl34_81
| ~ spl34_117
| ~ spl34_120
| spl34_125
| spl34_126 ),
inference(forward_subsumption_resolution,[],[f4710,f896]) ).
fof(f4722,plain,
( ~ spl34_81
| ~ spl34_117
| ~ spl34_120
| spl34_125
| spl34_126 ),
inference(avatar_contradiction_clause,[],[f4721]) ).
fof(f4774,plain,
( ~ spl34_128
| ~ spl34_78
| ~ spl34_85 ),
inference(avatar_split_clause,[],[f4593,f966,f853,f3823]) ).
cnf(s424,plain,
( spl34_1
| spl34_2
| spl34_3
| spl34_4 ),
inference(sat_conversion,[],[f450]) ).
cnf(s472,plain,
( ~ spl34_2
| ~ spl34_5 ),
inference(sat_conversion,[],[f455]) ).
cnf(s502,plain,
( ~ spl34_18
| ~ spl34_19 ),
inference(sat_conversion,[],[f519]) ).
cnf(s506,plain,
( ~ spl34_20
| ~ spl34_21 ),
inference(sat_conversion,[],[f528]) ).
cnf(s574,plain,
( ~ spl34_54
| ~ spl34_55 ),
inference(sat_conversion,[],[f681]) ).
cnf(s578,plain,
( ~ spl34_56
| ~ spl34_57 ),
inference(sat_conversion,[],[f690]) ).
cnf(s588,plain,
( ~ spl34_22
| ~ spl34_58 ),
inference(sat_conversion,[],[f733]) ).
cnf(s739,plain,
~ spl34_62,
inference(sat_conversion,[],[f922]) ).
cnf(s743,plain,
( ~ spl34_2
| spl34_81 ),
inference(sat_conversion,[],[f928]) ).
cnf(s779,plain,
( spl34_82
| spl34_83
| spl34_84
| spl34_85
| spl34_86 ),
inference(sat_conversion,[],[f973]) ).
cnf(s791,plain,
~ spl34_82,
inference(sat_conversion,[],[f1005]) ).
cnf(s804,plain,
~ spl34_83,
inference(sat_conversion,[],[f1024]) ).
cnf(s819,plain,
~ spl34_84,
inference(sat_conversion,[],[f1043]) ).
cnf(s920,plain,
( ~ spl34_87
| ~ spl34_89 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s980,plain,
( ~ spl34_59
| spl34_92
| spl34_93
| spl34_94 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s983,plain,
( ~ spl34_1
| ~ spl34_89
| ~ spl34_92 ),
inference(sat_conversion,[],[f1400]) ).
cnf(s1013,plain,
( spl34_78
| ~ spl34_85 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s1051,plain,
( ~ spl34_59
| spl34_95
| spl34_96
| spl34_97 ),
inference(sat_conversion,[],[f1446]) ).
cnf(s1062,plain,
( spl34_1
| spl34_2
| spl34_3
| ~ spl34_98 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s1075,plain,
( ~ spl34_86
| ~ spl34_89 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s1091,plain,
( ~ spl34_88
| ~ spl34_90 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s1116,plain,
( ~ spl34_86
| ~ spl34_95 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s1120,plain,
( ~ spl34_86
| ~ spl34_90 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s1127,plain,
( spl34_87
| spl34_88
| spl34_99
| spl34_100 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s1132,plain,
~ spl34_99,
inference(sat_conversion,[],[f1537]) ).
cnf(s1145,plain,
( spl34_89
| spl34_90
| spl34_101
| spl34_102 ),
inference(sat_conversion,[],[f1556]) ).
cnf(s1156,plain,
( spl34_95
| spl34_96
| spl34_97
| spl34_103 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s1182,plain,
( spl34_59
| spl34_104
| spl34_105
| spl34_106 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s1186,plain,
( ~ spl34_101
| ~ spl34_104 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s1201,plain,
( spl34_58
| ~ spl34_86 ),
inference(sat_conversion,[],[f1682]) ).
cnf(s1213,plain,
( ~ spl34_86
| ~ spl34_100 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s1221,plain,
( ~ spl34_87
| ~ spl34_96 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s1228,plain,
( ~ spl34_88
| ~ spl34_106 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s1238,plain,
( ~ spl34_58
| ~ spl34_86
| ~ spl34_105 ),
inference(sat_conversion,[],[f1725]) ).
cnf(s1255,plain,
( spl34_21
| ~ spl34_86 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s1299,plain,
( ~ spl34_4
| spl34_19
| ~ spl34_86 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s1311,plain,
( ~ spl34_86
| ~ spl34_108 ),
inference(sat_conversion,[],[f1917]) ).
cnf(s1323,plain,
( ~ spl34_92
| ~ spl34_96
| spl34_110
| spl34_111 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s1343,plain,
( ~ spl34_38
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s1361,plain,
( ~ spl34_4
| ~ spl34_86
| ~ spl34_110
| spl34_112
| spl34_113 ),
inference(sat_conversion,[],[f2043]) ).
cnf(s1365,plain,
~ spl34_112,
inference(sat_conversion,[],[f2053]) ).
cnf(s1376,plain,
( ~ spl34_76
| ~ spl34_86
| ~ spl34_113 ),
inference(sat_conversion,[],[f2081]) ).
cnf(s1388,plain,
( ~ spl34_109
| ~ spl34_111 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s1409,plain,
( ~ spl34_8
| ~ spl34_92
| ~ spl34_96 ),
inference(sat_conversion,[],[f2141]) ).
cnf(s1416,plain,
( ~ spl34_6
| spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109
| ~ spl34_110 ),
inference(sat_conversion,[],[f2149]) ).
cnf(s1430,plain,
( spl34_114
| spl34_115
| spl34_116 ),
inference(sat_conversion,[],[f2176]) ).
cnf(s1433,plain,
( ~ spl34_86
| ~ spl34_114 ),
inference(sat_conversion,[],[f2188]) ).
cnf(s1444,plain,
~ spl34_115,
inference(sat_conversion,[],[f2219]) ).
cnf(s1455,plain,
( ~ spl34_59
| ~ spl34_92
| spl34_117
| spl34_118
| spl34_119 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s1459,plain,
( ~ spl34_58
| ~ spl34_86
| ~ spl34_117 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s1469,plain,
( ~ spl34_4
| ~ spl34_30
| ~ spl34_86
| ~ spl34_119 ),
inference(sat_conversion,[],[f2293]) ).
cnf(s1476,plain,
( ~ spl34_86
| ~ spl34_118 ),
inference(sat_conversion,[],[f2312]) ).
cnf(s1490,plain,
( ~ spl34_48
| spl34_115 ),
inference(sat_conversion,[],[f2338]) ).
cnf(s1505,plain,
( ~ spl34_24
| ~ spl34_86
| ~ spl34_101 ),
inference(sat_conversion,[],[f2466]) ).
cnf(s1507,plain,
( ~ spl34_4
| ~ spl34_26
| ~ spl34_86 ),
inference(sat_conversion,[],[f2467]) ).
cnf(s1518,plain,
~ spl34_40,
inference(sat_conversion,[],[f2504]) ).
cnf(s1529,plain,
( ~ spl34_4
| ~ spl34_36
| ~ spl34_86
| ~ spl34_113 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s1550,plain,
( ~ spl34_28
| ~ spl34_39
| ~ spl34_59
| spl34_62
| spl34_107
| ~ spl34_109 ),
inference(sat_conversion,[],[f2640]) ).
cnf(s1552,plain,
( ~ spl34_32
| ~ spl34_116 ),
inference(sat_conversion,[],[f2641]) ).
cnf(s1593,plain,
( ~ spl34_44
| ~ spl34_110 ),
inference(sat_conversion,[],[f2735]) ).
cnf(s1595,plain,
( ~ spl34_50
| ~ spl34_86
| ~ spl34_101 ),
inference(sat_conversion,[],[f2736]) ).
cnf(s1597,plain,
( ~ spl34_52
| ~ spl34_92
| ~ spl34_96 ),
inference(sat_conversion,[],[f2737]) ).
cnf(s1599,plain,
( ~ spl34_46
| ~ spl34_58
| ~ spl34_86
| ~ spl34_109 ),
inference(sat_conversion,[],[f2738]) ).
cnf(s1602,plain,
( spl34_55
| ~ spl34_88
| ~ spl34_116 ),
inference(sat_conversion,[],[f2746]) ).
cnf(s1700,plain,
( ~ spl34_42
| ~ spl34_58
| ~ spl34_86 ),
inference(sat_conversion,[],[f2827]) ).
cnf(s1710,plain,
( ~ spl34_34
| ~ spl34_86 ),
inference(sat_conversion,[],[f2884]) ).
cnf(s1737,plain,
( ~ spl34_4
| ~ spl34_86
| ~ spl34_97 ),
inference(sat_conversion,[],[f2966]) ).
cnf(s1772,plain,
( ~ spl34_107
| ~ spl34_109
| ~ spl34_113 ),
inference(sat_conversion,[],[f3038]) ).
cnf(s1820,plain,
( ~ spl34_4
| ~ spl34_86
| ~ spl34_103
| spl34_112
| spl34_113 ),
inference(sat_conversion,[],[f3089]) ).
cnf(s1825,plain,
( spl34_62
| ~ spl34_106
| spl34_121
| spl34_122 ),
inference(sat_conversion,[],[f3113]) ).
cnf(s1829,plain,
( ~ spl34_86
| ~ spl34_121 ),
inference(sat_conversion,[],[f3126]) ).
cnf(s1835,plain,
( ~ spl34_113
| ~ spl34_122 ),
inference(sat_conversion,[],[f3139]) ).
cnf(s1900,plain,
( ~ spl34_86
| ~ spl34_102 ),
inference(sat_conversion,[],[f3220]) ).
cnf(s1911,plain,
( ~ spl34_86
| ~ spl34_93 ),
inference(sat_conversion,[],[f3236]) ).
cnf(s1929,plain,
( spl34_57
| ~ spl34_59 ),
inference(sat_conversion,[],[f3315]) ).
cnf(s1984,plain,
( ~ spl34_4
| spl34_6
| spl34_8
| spl34_76
| ~ spl34_86 ),
inference(sat_conversion,[],[f3400]) ).
cnf(s1995,plain,
( ~ spl34_94
| ~ spl34_109 ),
inference(sat_conversion,[],[f3417]) ).
cnf(s2021,plain,
( ~ spl34_86
| spl34_108
| spl34_109 ),
inference(sat_conversion,[],[f3458]) ).
cnf(s2038,plain,
( spl34_4
| ~ spl34_86 ),
inference(sat_conversion,[],[f3472]) ).
cnf(s2134,plain,
( ~ spl34_89
| ~ spl34_96 ),
inference(sat_conversion,[],[f3521]) ).
cnf(s2188,plain,
( ~ spl34_85
| spl34_117 ),
inference(sat_conversion,[],[f3599]) ).
cnf(s2254,plain,
( spl34_76
| ~ spl34_85 ),
inference(sat_conversion,[],[f3730]) ).
cnf(s2280,plain,
( spl34_18
| spl34_20
| spl34_22
| spl34_24
| spl34_26
| spl34_28
| spl34_30
| spl34_32
| spl34_34
| spl34_36
| spl34_38
| spl34_40
| spl34_42
| spl34_44
| spl34_46
| spl34_48
| spl34_50
| spl34_52
| spl34_54
| spl34_56 ),
inference(sat_conversion,[],[f3798]) ).
cnf(s2309,plain,
~ spl34_127,
inference(sat_conversion,[],[f3836]) ).
cnf(s2329,plain,
( ~ spl34_109
| ~ spl34_126 ),
inference(sat_conversion,[],[f3861]) ).
cnf(s2345,plain,
( spl34_5
| ~ spl34_109
| ~ spl34_125 ),
inference(sat_conversion,[],[f3878]) ).
cnf(s2381,plain,
( ~ spl34_93
| ~ spl34_117 ),
inference(sat_conversion,[],[f3913]) ).
cnf(s2405,plain,
( ~ spl34_3
| ~ spl34_85
| spl34_127
| spl34_128 ),
inference(sat_conversion,[],[f3951]) ).
cnf(s2457,plain,
( ~ spl34_88
| ~ spl34_97 ),
inference(sat_conversion,[],[f4020]) ).
cnf(s2471,plain,
( ~ spl34_76
| ~ spl34_85
| ~ spl34_108 ),
inference(sat_conversion,[],[f4044]) ).
cnf(s2523,plain,
( spl34_108
| spl34_109
| ~ spl34_117
| ~ spl34_120 ),
inference(sat_conversion,[],[f4110]) ).
cnf(s2548,plain,
( ~ spl34_85
| ~ spl34_117
| spl34_120 ),
inference(sat_conversion,[],[f4152]) ).
cnf(s2615,plain,
( ~ spl34_1
| ~ spl34_90
| ~ spl34_95 ),
inference(sat_conversion,[],[f4244]) ).
cnf(s2627,plain,
( ~ spl34_90
| ~ spl34_97 ),
inference(sat_conversion,[],[f4259]) ).
cnf(s2644,plain,
( ~ spl34_85
| ~ spl34_103 ),
inference(sat_conversion,[],[f4278]) ).
cnf(s2680,plain,
( ~ spl34_1
| ~ spl34_101 ),
inference(sat_conversion,[],[f4331]) ).
cnf(s2695,plain,
( ~ spl34_105
| ~ spl34_117 ),
inference(sat_conversion,[],[f4356]) ).
cnf(s2713,plain,
( ~ spl34_1
| ~ spl34_102 ),
inference(sat_conversion,[],[f4401]) ).
cnf(s2743,plain,
( ~ spl34_76
| ~ spl34_85
| ~ spl34_100 ),
inference(sat_conversion,[],[f4440]) ).
cnf(s2782,plain,
( ~ spl34_95
| ~ spl34_104 ),
inference(sat_conversion,[],[f4492]) ).
cnf(s2848,plain,
( ~ spl34_78
| ~ spl34_85
| spl34_98 ),
inference(sat_conversion,[],[f4603]) ).
cnf(s2889,plain,
( ~ spl34_81
| ~ spl34_117
| ~ spl34_120
| spl34_125
| spl34_126 ),
inference(sat_conversion,[],[f4722]) ).
cnf(s2950,plain,
( ~ spl34_78
| ~ spl34_85
| ~ spl34_128 ),
inference(sat_conversion,[],[f4774]) ).
cnf(s2952,plain,
~ spl34_48,
inference(rat,[],[s1490,s1444]) ).
cnf(s2953,plain,
( spl34_114
| spl34_116 ),
inference(rat,[],[s1430,s1444]) ).
cnf(s2954,plain,
( ~ spl34_4
| ~ spl34_86
| ~ spl34_110
| spl34_113 ),
inference(rat,[],[s1361,s1365]) ).
cnf(s2956,plain,
( spl34_87
| spl34_88
| spl34_100 ),
inference(rat,[],[s1127,s1132]) ).
cnf(s2958,plain,
( spl34_85
| spl34_86 ),
inference(rat,[],[s779,s819,s804,s791]) ).
cnf(s2962,plain,
( ~ spl34_85
| spl34_98 ),
inference(rat,[],[s2848,s1013]) ).
cnf(s2963,plain,
( ~ spl34_96
| spl34_110
| spl34_94
| ~ spl34_86 ),
inference(rat,[],[s1182,s1228,s980,s2956,s1323,s1221,s1911,s1213,s1238,s1201,s1388,s2021,s1311,s1186,s1145,s1075,s1120,s1900]) ).
cnf(s2964,plain,
( spl34_113
| spl34_94
| ~ spl34_86
| ~ spl34_4 ),
inference(rat,[],[s1156,s2963,s2954,s1820,s1116,s1737,s1365]) ).
cnf(s2965,plain,
( spl34_94
| ~ spl34_86
| ~ spl34_4 ),
inference(rat,[],[s2280,s1550,s574,s1416,s1602,s1469,s1593,s1984,s2956,s1455,s1597,s2963,s1409,s1221,s578,s980,s1051,s1343,s1929,s1182,s1825,s1772,s1529,s1376,s1835,s2964,s1911,s1829,s1710,s1476,s1213,s1116,s1507,s506,s1255,s1700,s1599,s2021,s1311,s1459,s1238,s588,s1201,s1552,s2953,s1433,s1186,s1595,s1505,s1145,s1075,s1120,s1900,s1737,s502,s1299,s1518,s2952,s739]) ).
cnf(s2966,plain,
( spl34_3
| spl34_2
| spl34_1 ),
inference(rat,[],[s1995,s2965,s2021,s1311,s2958,s2962,s424,s1062]) ).
cnf(s2967,plain,
( ~ spl34_85
| ~ spl34_3 ),
inference(rat,[],[s2950,s1013,s2405,s2309]) ).
cnf(s2968,plain,
( spl34_108
| ~ spl34_86 ),
inference(rat,[],[s2965,s2038,s1995,s2021]) ).
cnf(s2969,plain,
~ spl34_86,
inference(rat,[],[s2968,s1311]) ).
cnf(s2970,plain,
spl34_85,
inference(rat,[],[s2958,s2969]) ).
cnf(s2971,plain,
~ spl34_103,
inference(rat,[],[s2644,s2970]) ).
cnf(s2972,plain,
~ spl34_3,
inference(rat,[],[s2967,s2970]) ).
cnf(s2975,plain,
spl34_76,
inference(rat,[],[s2254,s2970]) ).
cnf(s2977,plain,
spl34_117,
inference(rat,[],[s2188,s2970]) ).
cnf(s2983,plain,
~ spl34_100,
inference(rat,[],[s2743,s2970,s2975]) ).
cnf(s2984,plain,
~ spl34_108,
inference(rat,[],[s2471,s2970,s2975]) ).
cnf(s2988,plain,
~ spl34_105,
inference(rat,[],[s2695,s2977]) ).
cnf(s2989,plain,
spl34_120,
inference(rat,[],[s2548,s2970,s2977]) ).
cnf(s2990,plain,
~ spl34_93,
inference(rat,[],[s2381,s2977]) ).
cnf(s2992,plain,
spl34_109,
inference(rat,[],[s2523,s2989,s2984,s2977]) ).
cnf(s2998,plain,
~ spl34_126,
inference(rat,[],[s2329,s2992]) ).
cnf(s2999,plain,
~ spl34_94,
inference(rat,[],[s1995,s2992]) ).
cnf(s3003,plain,
~ spl34_2,
inference(rat,[],[s2889,s2345,s472,s743,s2977,s2989,s2998,s2992]) ).
cnf(s3004,plain,
spl34_1,
inference(rat,[],[s2966,s2972,s3003]) ).
cnf(s3005,plain,
~ spl34_102,
inference(rat,[],[s2713,s3004]) ).
cnf(s3006,plain,
~ spl34_101,
inference(rat,[],[s2680,s3004]) ).
cnf(s3007,plain,
~ spl34_97,
inference(rat,[],[s920,s2956,s1145,s2457,s2627,s2983,s3006,s3005]) ).
cnf(s3008,plain,
~ spl34_96,
inference(rat,[],[s1091,s2956,s1145,s1221,s2134,s2983,s3006,s3005]) ).
cnf(s3010,plain,
spl34_95,
inference(rat,[],[s1156,s2971,s3007,s3008]) ).
cnf(s3013,plain,
~ spl34_104,
inference(rat,[],[s2782,s3010]) ).
cnf(s3015,plain,
~ spl34_90,
inference(rat,[],[s2615,s3004,s3010]) ).
cnf(s3016,plain,
spl34_89,
inference(rat,[],[s1145,s3005,s3006,s3015]) ).
cnf(s3017,plain,
~ spl34_92,
inference(rat,[],[s983,s3004,s3016]) ).
cnf(s3018,plain,
~ spl34_87,
inference(rat,[],[s920,s3016]) ).
cnf(s3022,plain,
~ spl34_59,
inference(rat,[],[s980,s2999,s2990,s3017]) ).
cnf(s3023,plain,
spl34_88,
inference(rat,[],[s2956,s2983,s3018]) ).
cnf(s3027,plain,
spl34_106,
inference(rat,[],[s1182,s3013,s2988,s3022]) ).
cnf(s3029,plain,
$false,
inference(rat,[],[s1228,s3027,s3023]) ).
fof(f4775,plain,
$false,
inference(avatar_sat_refutation,[],[s3029]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG057+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.09/0.19 % Computer : n005.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 19:22:32 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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.87/0.44 % (1065795)Will run a generic schedule for satisfiability detection.
% 0.87/0.44 % (1065804)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4050658361:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.87/0.44 % (1065801)% WARNING: option uhcvi not known.
% 0.87/0.44 % (1065800)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=323422413_2999 on theBenchmark for (2999ds/0Mi)
% 0.87/0.44 % (1065801)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1534692589:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.87/0.44 % (1065802)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3283688567:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.87/0.44 % (1065803)dis+10_1_sil=32000:sp=arity:random_seed=3315472407:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.87/0.44 % (1065805)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2434343955:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.87/0.44 % (1065806)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2624046994:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.87/0.44 % (1065804)Instruction limit reached!
% 0.87/0.44 % (1065804)------------------------------
% 0.87/0.44 % (1065804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (1065804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (1065804)CaDiCaL version: 2.1.3
% 0.87/0.44 % (1065804)Termination reason: Instruction limit
% 0.87/0.44 % (1065804)Termination phase: Saturation
% 0.87/0.44 % (1065804)Time elapsed: 0.034 s
% 0.87/0.44 % (1065804)Peak memory usage: 13 MB
% 0.87/0.44 % (1065804)Instructions burned: 119 (million)
% 0.87/0.44 % Detected minimum model sizes of [5]
% 0.87/0.44 % Detected maximum model sizes of [max]
% 0.87/0.44 % TRYING [5]
% 0.87/0.44 % (1065814)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1006779026:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.87/0.44 % Detected minimum model sizes of [5]
% 0.87/0.44 % Detected maximum model sizes of [max]
% 0.87/0.44 % TRYING [5]
% 0.87/0.44 % TRYING [6]
% 0.87/0.44 % (1065803)Instruction limit reached!
% 0.87/0.44 % (1065803)------------------------------
% 0.87/0.44 % (1065803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (1065803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (1065803)CaDiCaL version: 2.1.3
% 0.87/0.44 % (1065803)Termination reason: Instruction limit
% 0.87/0.44 % (1065803)Termination phase: Saturation
% 0.87/0.44 % (1065803)Time elapsed: 0.058 s
% 0.87/0.44 % (1065803)Peak memory usage: 12 MB
% 0.87/0.44 % (1065803)Instructions burned: 111 (million)
% 0.87/0.44 % (1065805)Instruction limit reached!
% 0.87/0.44 % (1065805)------------------------------
% 0.87/0.44 % (1065805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (1065805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (1065805)CaDiCaL version: 2.1.3
% 0.87/0.44 % (1065805)Termination reason: Instruction limit
% 0.87/0.44 % (1065805)Termination phase: Saturation
% 0.87/0.44 % (1065805)Time elapsed: 0.064 s
% 0.87/0.44 % (1065805)Peak memory usage: 13 MB
% 0.87/0.44 % (1065805)Instructions burned: 131 (million)
% 0.87/0.44 % TRYING [6]
% 0.87/0.44 % (1065816)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2119430921:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.87/0.44 % (1065817)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3350194569:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.87/0.44 % TRYING [7]
% 0.87/0.44 % (1065806)Instruction limit reached!
% 0.87/0.44 % (1065806)------------------------------
% 0.87/0.44 % (1065806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (1065806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (1065806)CaDiCaL version: 2.1.3
% 0.87/0.44 % (1065806)Termination reason: Instruction limit
% 0.87/0.44 % (1065806)Termination phase: Saturation
% 0.87/0.44 % (1065806)Time elapsed: 0.090 s
% 0.87/0.44 % (1065806)Peak memory usage: 14 MB
% 0.87/0.44 % (1065806)Instructions burned: 159 (million)
% 0.87/0.44 % TRYING [7]
% 0.87/0.44 % (1065820)ott-21_1_sil=16000:fs=off:random_seed=3871860872:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.87/0.44 % TRYING [8]
% 0.87/0.44 % (1065802) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1065795-1065802"...
% 0.87/0.44 % (1065816)Instruction limit reached!
% 0.87/0.44 % (1065816)------------------------------
% 0.87/0.44 % (1065816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.44 % (1065816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.44 % (1065816)CaDiCaL version: 2.1.3
% 0.87/0.44 % (1065816)Termination reason: Instruction limit
% 0.87/0.44 % (1065816)Termination phase: Saturation
% 0.87/0.44 % (1065816)Time elapsed: 0.064 s
% 0.87/0.44 % (1065816)Peak memory usage: 13 MB
% 0.87/0.44 % (1065816)Instructions burned: 132 (million)
% 0.87/0.44 % (1065802)...printing done.
% 0.87/0.44 % (1065802)Refutation found. Thanks to Tanya!
% 0.87/0.44 % SZS status Theorem for theBenchmark
% 0.87/0.44 % SZS output start Proof for theBenchmark
% See solution above
% 0.87/0.45 % (1065802)------------------------------
% 0.87/0.45 % (1065802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.87/0.45 % (1065802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.87/0.45 % (1065802)CaDiCaL version: 2.1.3
% 0.87/0.45 % (1065802)Termination reason: Refutation
% 0.87/0.45 % (1065802)Time elapsed: 0.152 s
% 0.87/0.45 % (1065802)Peak memory usage: 15 MB
% 0.87/0.45 % (1065802)Instructions burned: 290 (million)
% 0.87/0.45 % (1065795)Success in time 0.199 s
% 0.87/0.45 % Vampire exiting
%------------------------------------------------------------------------------