%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG056+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 : n013.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.88s 0.40s
% Output : Refutation 0.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 98
% Syntax : Number of formulae : 614 ( 116 unt; 92 def)
% Number of atoms : 2289 (1228 equ)
% Maximal formula atoms : 125 ( 3 avg)
% Number of connectives : 2655 ( 980 ~;1102 |; 515 &)
% ( 58 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 101 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 94 ( 92 usr; 93 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) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(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) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(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) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 ) ) ),
inference(flattening,[],[f8]) ).
fof(f10,definition,
( ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(e4,e4) != e4 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f13,definition,
( ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ~ sP4 ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ~ sP5 ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP6 ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f17,definition,
( ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ~ sP7 ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f18,definition,
( ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ~ sP8 ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f19,definition,
( ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ~ sP9 ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f20,definition,
( ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ~ sP10 ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f21,definition,
( ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ~ sP11 ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f22,definition,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP12 ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f23,definition,
( ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ~ sP13 ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f24,definition,
( ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ~ sP14 ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f25,definition,
( ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ~ sP15 ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f26,definition,
( ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ~ sP16 ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f27,definition,
( ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ~ sP17 ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f28,definition,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP18 ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f29,definition,
( ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ~ sP19 ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f30,definition,
( ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ~ sP20 ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f31,definition,
( ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ~ sP21 ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f32,definition,
( ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ~ sP22 ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f33,definition,
( ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ~ 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) = e0
& op(e0,e0) = e0
& 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(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(f55,plain,
( ( op(e0,e0) = e1
& op(e1,e1) = e0
& op(e0,e1) != e0 )
| ~ sP23 ),
inference(nnf_transformation,[],[f33]) ).
fof(f56,plain,
( ( op(e0,e0) = e2
& op(e2,e2) = e0
& op(e0,e2) != e0 )
| ~ sP22 ),
inference(nnf_transformation,[],[f32]) ).
fof(f57,plain,
( ( op(e0,e0) = e3
& op(e3,e3) = e0
& op(e0,e3) != e0 )
| ~ sP21 ),
inference(nnf_transformation,[],[f31]) ).
fof(f58,plain,
( ( op(e0,e0) = e4
& op(e4,e4) = e0
& op(e0,e4) != e0 )
| ~ sP20 ),
inference(nnf_transformation,[],[f30]) ).
fof(f59,plain,
( ( op(e1,e1) = e0
& op(e0,e0) = e1
& op(e1,e0) != e1 )
| ~ sP19 ),
inference(nnf_transformation,[],[f29]) ).
fof(f60,plain,
( ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ~ sP18 ),
inference(nnf_transformation,[],[f28]) ).
fof(f61,plain,
( ( op(e1,e1) = e2
& op(e2,e2) = e1
& op(e1,e2) != e1 )
| ~ sP17 ),
inference(nnf_transformation,[],[f27]) ).
fof(f62,plain,
( ( op(e1,e1) = e3
& op(e3,e3) = e1
& op(e1,e3) != e1 )
| ~ sP16 ),
inference(nnf_transformation,[],[f26]) ).
fof(f63,plain,
( ( op(e1,e1) = e4
& op(e4,e4) = e1
& op(e1,e4) != e1 )
| ~ sP15 ),
inference(nnf_transformation,[],[f25]) ).
fof(f64,plain,
( ( op(e2,e2) = e0
& op(e0,e0) = e2
& op(e2,e0) != e2 )
| ~ sP14 ),
inference(nnf_transformation,[],[f24]) ).
fof(f65,plain,
( ( op(e2,e2) = e1
& op(e1,e1) = e2
& op(e2,e1) != e2 )
| ~ sP13 ),
inference(nnf_transformation,[],[f23]) ).
fof(f66,plain,
( ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ~ sP12 ),
inference(nnf_transformation,[],[f22]) ).
fof(f67,plain,
( ( op(e2,e2) = e3
& op(e3,e3) = e2
& op(e2,e3) != e2 )
| ~ sP11 ),
inference(nnf_transformation,[],[f21]) ).
fof(f68,plain,
( ( op(e2,e2) = e4
& op(e4,e4) = e2
& op(e2,e4) != e2 )
| ~ sP10 ),
inference(nnf_transformation,[],[f20]) ).
fof(f69,plain,
( ( op(e3,e3) = e0
& op(e0,e0) = e3
& op(e3,e0) != e3 )
| ~ sP9 ),
inference(nnf_transformation,[],[f19]) ).
fof(f70,plain,
( ( op(e3,e3) = e1
& op(e1,e1) = e3
& op(e3,e1) != e3 )
| ~ sP8 ),
inference(nnf_transformation,[],[f18]) ).
fof(f71,plain,
( ( op(e3,e3) = e2
& op(e2,e2) = e3
& op(e3,e2) != e3 )
| ~ sP7 ),
inference(nnf_transformation,[],[f17]) ).
fof(f72,plain,
( ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 )
| ~ sP6 ),
inference(nnf_transformation,[],[f16]) ).
fof(f73,plain,
( ( op(e3,e3) = e4
& op(e4,e4) = e3
& op(e3,e4) != e3 )
| ~ sP5 ),
inference(nnf_transformation,[],[f15]) ).
fof(f74,plain,
( ( op(e4,e4) = e0
& op(e0,e0) = e4
& op(e4,e0) != e4 )
| ~ sP4 ),
inference(nnf_transformation,[],[f14]) ).
fof(f75,plain,
( ( op(e4,e4) = e1
& op(e1,e1) = e4
& op(e4,e1) != e4 )
| ~ sP3 ),
inference(nnf_transformation,[],[f13]) ).
fof(f76,plain,
( ( op(e4,e4) = e2
& op(e2,e2) = e4
& op(e4,e2) != e4 )
| ~ sP2 ),
inference(nnf_transformation,[],[f12]) ).
fof(f77,plain,
( ( op(e4,e4) = e3
& op(e3,e3) = e4
& op(e4,e3) != e4 )
| ~ sP1 ),
inference(nnf_transformation,[],[f11]) ).
fof(f78,plain,
( ( op(e4,e4) = e4
& op(e4,e4) = e4
& op(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(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(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(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(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(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(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(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(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(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(f191,plain,
op(e2,e0) != op(e2,e4),
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(f223,plain,
op(e0,e4) != op(e2,e4),
inference(cnf_transformation,[],[f4]) ).
fof(f225,plain,
op(e3,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(f232,plain,
op(e0,e3) != op(e3,e3),
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(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(f256,plain,
op(e2,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f259,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f260,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f261,plain,
op(e0,e0) != op(e4,e0),
inference(cnf_transformation,[],[f4]) ).
fof(f264,plain,
op(e0,e0) != op(e1,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(f271,plain,
e0 != e4,
inference(cnf_transformation,[],[f5]) ).
fof(f272,plain,
e0 != e3,
inference(cnf_transformation,[],[f5]) ).
fof(f273,plain,
e0 != e2,
inference(cnf_transformation,[],[f5]) ).
fof(f274,plain,
e0 != e1,
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(f301,plain,
( op(e0,e0) = e1
| ~ sP23 ),
inference(cnf_transformation,[],[f55]) ).
fof(f303,plain,
( e0 = op(e2,e2)
| ~ sP22 ),
inference(cnf_transformation,[],[f56]) ).
fof(f306,plain,
( e0 = op(e3,e3)
| ~ sP21 ),
inference(cnf_transformation,[],[f57]) ).
fof(f310,plain,
( op(e0,e0) = e4
| ~ sP20 ),
inference(cnf_transformation,[],[f58]) ).
fof(f311,plain,
( e1 != op(e1,e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f59]) ).
fof(f314,plain,
( e1 != op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f60]) ).
fof(f316,plain,
( e1 = op(e1,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f60]) ).
fof(f318,plain,
( e1 = op(e2,e2)
| ~ sP17 ),
inference(cnf_transformation,[],[f61]) ).
fof(f321,plain,
( e1 = op(e3,e3)
| ~ sP16 ),
inference(cnf_transformation,[],[f62]) ).
fof(f324,plain,
( e1 = op(e4,e4)
| ~ sP15 ),
inference(cnf_transformation,[],[f63]) ).
fof(f328,plain,
( e0 = op(e2,e2)
| ~ sP14 ),
inference(cnf_transformation,[],[f64]) ).
fof(f331,plain,
( e1 = op(e2,e2)
| ~ sP13 ),
inference(cnf_transformation,[],[f65]) ).
fof(f332,plain,
( e2 != op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f66]) ).
fof(f334,plain,
( e2 = op(e2,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f66]) ).
fof(f337,plain,
( e3 = op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f67]) ).
fof(f339,plain,
( e2 = op(e4,e4)
| ~ sP10 ),
inference(cnf_transformation,[],[f68]) ).
fof(f341,plain,
( e3 != op(e3,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f69]) ).
fof(f346,plain,
( e1 = op(e3,e3)
| ~ sP8 ),
inference(cnf_transformation,[],[f70]) ).
fof(f348,plain,
( e3 = op(e2,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f71]) ).
fof(f350,plain,
( e3 != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f72]) ).
fof(f352,plain,
( e3 = op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f72]) ).
fof(f354,plain,
( e3 = op(e4,e4)
| ~ sP5 ),
inference(cnf_transformation,[],[f73]) ).
fof(f356,plain,
( e4 != op(e4,e0)
| ~ sP4 ),
inference(cnf_transformation,[],[f74]) ).
fof(f361,plain,
( e1 = op(e4,e4)
| ~ sP3 ),
inference(cnf_transformation,[],[f75]) ).
fof(f364,plain,
( e2 = op(e4,e4)
| ~ sP2 ),
inference(cnf_transformation,[],[f76]) ).
fof(f367,plain,
( e3 = op(e4,e4)
| ~ sP1 ),
inference(cnf_transformation,[],[f77]) ).
fof(f368,plain,
( e4 != op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f370,plain,
( e4 = op(e4,e4)
| ~ sP0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f371,plain,
( e0 != op(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(f373,plain,
( e0 = op(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(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(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,
( 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,[],[f373,f371]) ).
fof(f418,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(f434,plain,
( sP23
| sP22
| sP21
| sP20
| sP19
| sP17
| sP16
| sP15
| sP14
| sP13
| sP11
| sP10
| sP9
| sP8
| sP7
| sP5
| sP4
| sP3
| sP2
| sP1 ),
inference(global_subsumption,[],[f415,f316,f314,f334,f332,f352,f350,f370,f368]) ).
fof(f436,definition,
( spl34_1
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl34_1])],[avatar_definition]) ).
fof(f438,plain,
( ~ sP23
| spl34_1 ),
inference(avatar_component_clause,[],[f436]) ).
fof(f440,definition,
( spl34_2
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl34_2])],[avatar_definition]) ).
fof(f441,plain,
( e0 = op(e0,e1)
| ~ spl34_2 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f454,definition,
( spl34_5
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl34_5])],[avatar_definition]) ).
fof(f456,plain,
( ~ sP21
| spl34_5 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f463,definition,
( spl34_7
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl34_7])],[avatar_definition]) ).
fof(f464,plain,
( sP20
| ~ spl34_7 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f472,definition,
( spl34_9
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl34_9])],[avatar_definition]) ).
fof(f474,plain,
( ~ sP19
| spl34_9 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f476,definition,
( spl34_10
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl34_10])],[avatar_definition]) ).
fof(f477,plain,
( e1 = op(e1,e0)
| ~ spl34_10 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f478,plain,
( e1 != op(e1,e0)
| spl34_10 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f479,plain,
( ~ spl34_9
| ~ spl34_10 ),
inference(avatar_split_clause,[],[f311,f476,f472]) ).
fof(f481,definition,
( spl34_11
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl34_11])],[avatar_definition]) ).
fof(f483,plain,
( ~ sP17
| spl34_11 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f499,definition,
( spl34_15
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl34_15])],[avatar_definition]) ).
fof(f501,plain,
( ~ sP15
| spl34_15 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f508,definition,
( spl34_17
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl34_17])],[avatar_definition]) ).
fof(f510,plain,
( ~ sP14
| spl34_17 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f512,definition,
( spl34_18
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_18])],[avatar_definition]) ).
fof(f513,plain,
( e2 = op(e2,e0)
| ~ spl34_18 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f514,plain,
( e2 != op(e2,e0)
| spl34_18 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f517,definition,
( spl34_19
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl34_19])],[avatar_definition]) ).
fof(f519,plain,
( ~ sP13
| spl34_19 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f521,definition,
( spl34_20
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl34_20])],[avatar_definition]) ).
fof(f522,plain,
( e2 = op(e2,e1)
| ~ spl34_20 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f523,plain,
( e2 != op(e2,e1)
| spl34_20 ),
inference(avatar_component_clause,[],[f521]) ).
fof(f535,definition,
( spl34_23
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl34_23])],[avatar_definition]) ).
fof(f537,plain,
( ~ sP10
| spl34_23 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f544,definition,
( spl34_25
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl34_25])],[avatar_definition]) ).
fof(f546,plain,
( ~ sP9
| spl34_25 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f548,definition,
( spl34_26
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_26])],[avatar_definition]) ).
fof(f549,plain,
( e3 = op(e3,e0)
| ~ spl34_26 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f550,plain,
( e3 != op(e3,e0)
| spl34_26 ),
inference(avatar_component_clause,[],[f548]) ).
fof(f551,plain,
( ~ spl34_25
| ~ spl34_26 ),
inference(avatar_split_clause,[],[f341,f548,f544]) ).
fof(f553,definition,
( spl34_27
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl34_27])],[avatar_definition]) ).
fof(f557,definition,
( spl34_28
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl34_28])],[avatar_definition]) ).
fof(f558,plain,
( e3 = op(e3,e1)
| ~ spl34_28 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f562,definition,
( spl34_29
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl34_29])],[avatar_definition]) ).
fof(f564,plain,
( ~ sP7
| spl34_29 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl34_30
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_30])],[avatar_definition]) ).
fof(f568,plain,
( e3 != op(e3,e2)
| spl34_30 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f571,definition,
( spl34_31
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl34_31])],[avatar_definition]) ).
fof(f573,plain,
( ~ sP5
| spl34_31 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f580,definition,
( spl34_33
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl34_33])],[avatar_definition]) ).
fof(f582,plain,
( ~ sP4
| spl34_33 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f584,definition,
( spl34_34
<=> e4 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_34])],[avatar_definition]) ).
fof(f585,plain,
( e4 = op(e4,e0)
| ~ spl34_34 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f586,plain,
( e4 != op(e4,e0)
| spl34_34 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,plain,
( ~ spl34_33
| ~ spl34_34 ),
inference(avatar_split_clause,[],[f356,f584,f580]) ).
fof(f589,definition,
( spl34_35
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl34_35])],[avatar_definition]) ).
fof(f591,plain,
( ~ sP3
| spl34_35 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f593,definition,
( spl34_36
<=> e4 = op(e4,e1) ),
introduced(definition,[new_symbols(definition,[spl34_36])],[avatar_definition]) ).
fof(f594,plain,
( e4 = op(e4,e1)
| ~ spl34_36 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f598,definition,
( spl34_37
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl34_37])],[avatar_definition]) ).
fof(f600,plain,
( ~ sP2
| spl34_37 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f602,definition,
( spl34_38
<=> e4 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_38])],[avatar_definition]) ).
fof(f604,plain,
( e4 != op(e4,e2)
| spl34_38 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f611,definition,
( spl34_40
<=> e4 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_40])],[avatar_definition]) ).
fof(f612,plain,
( e4 = op(e4,e3)
| ~ spl34_40 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f616,definition,
( spl34_41
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl34_41])],[avatar_definition]) ).
fof(f617,plain,
( ~ sP32
| spl34_41 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f618,plain,
( sP32
| ~ spl34_41 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f620,definition,
( spl34_42
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl34_42])],[avatar_definition]) ).
fof(f621,plain,
( ~ sP33
| spl34_42 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f624,definition,
( spl34_43
<=> e2 = op(e0,op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_43])],[avatar_definition]) ).
fof(f625,plain,
( e2 != op(e0,op(e2,e0))
| spl34_43 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f626,plain,
( e2 = op(e0,op(e2,e0))
| ~ spl34_43 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f633,definition,
( spl34_45
<=> e0 = op(e3,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_45])],[avatar_definition]) ).
fof(f635,plain,
( e0 != op(e3,op(e3,e0))
| spl34_45 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,plain,
( ~ spl34_42
| ~ spl34_45 ),
inference(avatar_split_clause,[],[f280,f633,f620]) ).
fof(f752,definition,
( spl34_58
<=> e2 = op(e4,op(e2,e4)) ),
introduced(definition,[new_symbols(definition,[spl34_58])],[avatar_definition]) ).
fof(f753,plain,
( e2 != op(e4,op(e2,e4))
| spl34_58 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f754,plain,
( e2 = op(e4,op(e2,e4))
| ~ spl34_58 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f859,definition,
( spl34_75
<=> e2 = op(e1,op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl34_75])],[avatar_definition]) ).
fof(f860,plain,
( e2 != op(e1,op(e2,e1))
| spl34_75 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f861,plain,
( e2 = op(e1,op(e2,e1))
| ~ spl34_75 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f867,definition,
( spl34_77
<=> e0 = op(e1,op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl34_77])],[avatar_definition]) ).
fof(f868,plain,
( e0 != op(e1,op(e0,e1))
| spl34_77 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f869,plain,
( e0 = op(e1,op(e0,e1))
| ~ spl34_77 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f928,plain,
e3 = op(e2,e4),
inference(forward_demodulation,[],[f276,f430]) ).
fof(f938,plain,
e3 != op(e2,e0),
inference(superposition,[],[f191,f928]) ).
fof(f940,plain,
( e2 = op(e4,e3)
| ~ spl34_58 ),
inference(superposition,[],[f754,f928]) ).
fof(f947,plain,
( e2 != op(e3,e3)
| ~ spl34_58 ),
inference(superposition,[],[f225,f940]) ).
fof(f965,definition,
( spl34_80
<=> e3 = op(e0,op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_80])],[avatar_definition]) ).
fof(f967,plain,
( e3 = op(e0,op(e3,e0))
| ~ spl34_80 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,plain,
( ~ spl34_42
| spl34_80 ),
inference(avatar_split_clause,[],[f279,f965,f620]) ).
fof(f970,plain,
e0 = op(e4,e4),
inference(forward_demodulation,[],[f278,f430]) ).
fof(f971,plain,
e1 = op(op(e2,e4),e4),
inference(forward_demodulation,[],[f277,f430]) ).
fof(f972,plain,
e1 = op(e3,e4),
inference(forward_demodulation,[],[f971,f928]) ).
fof(f973,plain,
e1 != op(e3,e3),
inference(superposition,[],[f175,f972]) ).
fof(f974,plain,
e1 != op(e3,e2),
inference(superposition,[],[f176,f972]) ).
fof(f976,plain,
e1 != op(e3,e0),
inference(superposition,[],[f181,f972]) ).
fof(f984,definition,
( spl34_81
<=> e4 = unit ),
introduced(definition,[new_symbols(definition,[spl34_81])],[avatar_definition]) ).
fof(f986,plain,
( e4 = unit
| ~ spl34_81 ),
inference(avatar_component_clause,[],[f984]) ).
fof(f988,definition,
( spl34_82
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl34_82])],[avatar_definition]) ).
fof(f990,plain,
( e3 = unit
| ~ spl34_82 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f992,definition,
( spl34_83
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl34_83])],[avatar_definition]) ).
fof(f994,plain,
( e2 = unit
| ~ spl34_83 ),
inference(avatar_component_clause,[],[f992]) ).
fof(f996,definition,
( spl34_84
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl34_84])],[avatar_definition]) ).
fof(f998,plain,
( e1 = unit
| ~ spl34_84 ),
inference(avatar_component_clause,[],[f996]) ).
fof(f1000,definition,
( spl34_85
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl34_85])],[avatar_definition]) ).
fof(f1002,plain,
( e0 = unit
| ~ spl34_85 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1003,plain,
( spl34_81
| spl34_82
| spl34_83
| spl34_84
| spl34_85 ),
inference(avatar_split_clause,[],[f104,f1000,f996,f992,f988,f984]) ).
fof(f1006,plain,
( e3 = op(e3,e4)
| ~ spl34_81 ),
inference(superposition,[],[f107,f986]) ).
fof(f1025,plain,
( e1 = e3
| ~ spl34_81 ),
inference(forward_demodulation,[],[f1006,f972]) ).
fof(f1030,plain,
( $false
| ~ spl34_81 ),
inference(forward_subsumption_resolution,[],[f1025,f269]) ).
fof(f1031,plain,
~ spl34_81,
inference(avatar_contradiction_clause,[],[f1030]) ).
fof(f1037,plain,
( e4 = op(e3,e4)
| ~ spl34_82 ),
inference(superposition,[],[f106,f990]) ).
fof(f1051,plain,
( e1 = e4
| ~ spl34_82 ),
inference(forward_demodulation,[],[f1037,f972]) ).
fof(f1053,plain,
( $false
| ~ spl34_82 ),
inference(forward_subsumption_resolution,[],[f1051,f268]) ).
fof(f1054,plain,
~ spl34_82,
inference(avatar_contradiction_clause,[],[f1053]) ).
fof(f1058,plain,
( e4 = op(e2,e4)
| ~ spl34_83 ),
inference(superposition,[],[f106,f994]) ).
fof(f1071,plain,
( e3 = e4
| ~ spl34_83 ),
inference(forward_demodulation,[],[f1058,f928]) ).
fof(f1072,plain,
( $false
| ~ spl34_83 ),
inference(forward_subsumption_resolution,[],[f1071,f265]) ).
fof(f1073,plain,
~ spl34_83,
inference(avatar_contradiction_clause,[],[f1072]) ).
fof(f1074,plain,
( e4 = op(e4,e1)
| ~ spl34_84 ),
inference(superposition,[],[f105,f998]) ).
fof(f1076,plain,
( e3 = op(e3,e1)
| ~ spl34_84 ),
inference(superposition,[],[f107,f998]) ).
fof(f1078,plain,
( e2 = op(e2,e1)
| ~ spl34_84 ),
inference(superposition,[],[f109,f998]) ).
fof(f1082,plain,
( e0 = op(e0,e1)
| ~ spl34_84 ),
inference(superposition,[],[f113,f998]) ).
fof(f1087,plain,
( $false
| spl34_20
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f1078,f523]) ).
fof(f1088,plain,
( spl34_20
| ~ spl34_84 ),
inference(avatar_contradiction_clause,[],[f1087]) ).
fof(f1091,plain,
( e2 = op(e1,e2)
| ~ spl34_20
| ~ spl34_75 ),
inference(superposition,[],[f861,f522]) ).
fof(f1092,plain,
( e2 != op(e2,e0)
| ~ spl34_20 ),
inference(superposition,[],[f194,f522]) ).
fof(f1124,plain,
( spl34_36
| ~ spl34_84 ),
inference(avatar_split_clause,[],[f1074,f996,f593]) ).
fof(f1125,plain,
( e4 != op(e4,e2)
| ~ spl34_36 ),
inference(superposition,[],[f170,f594]) ).
fof(f1126,plain,
( e4 != op(e4,e0)
| ~ spl34_36 ),
inference(superposition,[],[f174,f594]) ).
fof(f1134,plain,
( ~ spl34_38
| ~ spl34_36 ),
inference(avatar_split_clause,[],[f1125,f593,f602]) ).
fof(f1135,plain,
( ~ spl34_34
| ~ spl34_36 ),
inference(avatar_split_clause,[],[f1126,f593,f584]) ).
fof(f1152,plain,
( spl34_28
| ~ spl34_84 ),
inference(avatar_split_clause,[],[f1076,f996,f557]) ).
fof(f1153,plain,
( e3 != op(e3,e2)
| ~ spl34_28 ),
inference(superposition,[],[f180,f558]) ).
fof(f1154,plain,
( e3 != op(e3,e0)
| ~ spl34_28 ),
inference(superposition,[],[f184,f558]) ).
fof(f1172,plain,
( ~ spl34_30
| ~ spl34_28 ),
inference(avatar_split_clause,[],[f1153,f557,f566]) ).
fof(f1173,plain,
( ~ spl34_26
| ~ spl34_28 ),
inference(avatar_split_clause,[],[f1154,f557,f548]) ).
fof(f1184,plain,
( spl34_2
| ~ spl34_84 ),
inference(avatar_split_clause,[],[f1082,f996,f440]) ).
fof(f1185,plain,
( e4 = op(e4,e0)
| ~ spl34_85 ),
inference(superposition,[],[f105,f1002]) ).
fof(f1187,plain,
( e3 = op(e3,e0)
| ~ spl34_85 ),
inference(superposition,[],[f107,f1002]) ).
fof(f1189,plain,
( e2 = op(e2,e0)
| ~ spl34_85 ),
inference(superposition,[],[f109,f1002]) ).
fof(f1191,plain,
( e1 = op(e1,e0)
| ~ spl34_85 ),
inference(superposition,[],[f111,f1002]) ).
fof(f1199,plain,
( $false
| spl34_10
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f1191,f478]) ).
fof(f1200,plain,
( spl34_10
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f1199]) ).
fof(f1203,plain,
( $false
| spl34_18
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f1189,f514]) ).
fof(f1204,plain,
( spl34_18
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f1203]) ).
fof(f1205,plain,
( $false
| spl34_26
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f1187,f550]) ).
fof(f1206,plain,
( spl34_26
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f1205]) ).
fof(f1207,plain,
( $false
| spl34_34
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f1185,f586]) ).
fof(f1208,plain,
( spl34_34
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f1207]) ).
fof(f1214,plain,
( e2 = op(e1,e2)
| ~ spl34_84 ),
inference(superposition,[],[f110,f998]) ).
fof(f1275,definition,
( spl34_86
<=> e3 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_86])],[avatar_definition]) ).
fof(f1276,plain,
( e3 != op(e4,e2)
| spl34_86 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1277,plain,
( e3 = op(e4,e2)
| ~ spl34_86 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1279,definition,
( spl34_87
<=> e1 = op(e4,e2) ),
introduced(definition,[new_symbols(definition,[spl34_87])],[avatar_definition]) ).
fof(f1280,plain,
( e1 != op(e4,e2)
| spl34_87 ),
inference(avatar_component_clause,[],[f1279]) ).
fof(f1281,plain,
( e1 = op(e4,e2)
| ~ spl34_87 ),
inference(avatar_component_clause,[],[f1279]) ).
fof(f1296,definition,
( spl34_88
<=> e3 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_88])],[avatar_definition]) ).
fof(f1297,plain,
( e3 != op(e4,e0)
| spl34_88 ),
inference(avatar_component_clause,[],[f1296]) ).
fof(f1298,plain,
( e3 = op(e4,e0)
| ~ spl34_88 ),
inference(avatar_component_clause,[],[f1296]) ).
fof(f1300,definition,
( spl34_89
<=> e1 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_89])],[avatar_definition]) ).
fof(f1301,plain,
( e1 != op(e4,e0)
| spl34_89 ),
inference(avatar_component_clause,[],[f1300]) ).
fof(f1302,plain,
( e1 = op(e4,e0)
| ~ spl34_89 ),
inference(avatar_component_clause,[],[f1300]) ).
fof(f1304,plain,
( e3 != op(e4,e2)
| ~ spl34_88 ),
inference(superposition,[],[f173,f1298]) ).
fof(f1316,plain,
( $false
| ~ spl34_86
| ~ spl34_88 ),
inference(forward_subsumption_resolution,[],[f1304,f1277]) ).
fof(f1317,plain,
( ~ spl34_86
| ~ spl34_88 ),
inference(avatar_contradiction_clause,[],[f1316]) ).
fof(f1377,plain,
( e0 = op(e3,e3)
| e2 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3) ),
inference(forward_subsumption_resolution,[],[f85,f973]) ).
fof(f1378,plain,
( e0 = op(e3,e3)
| e3 = op(e3,e3)
| e4 = op(e3,e3)
| ~ spl34_58 ),
inference(forward_subsumption_resolution,[],[f1377,f947]) ).
fof(f1380,definition,
( spl34_90
<=> e4 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_90])],[avatar_definition]) ).
fof(f1382,plain,
( e4 = op(e3,e3)
| ~ spl34_90 ),
inference(avatar_component_clause,[],[f1380]) ).
fof(f1384,definition,
( spl34_91
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_91])],[avatar_definition]) ).
fof(f1386,plain,
( e3 = op(e3,e3)
| ~ spl34_91 ),
inference(avatar_component_clause,[],[f1384]) ).
fof(f1388,definition,
( spl34_92
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl34_92])],[avatar_definition]) ).
fof(f1389,plain,
( e0 != op(e3,e3)
| spl34_92 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1390,plain,
( e0 = op(e3,e3)
| ~ spl34_92 ),
inference(avatar_component_clause,[],[f1388]) ).
fof(f1391,plain,
( spl34_90
| spl34_91
| spl34_92
| ~ spl34_58 ),
inference(avatar_split_clause,[],[f1378,f752,f1388,f1384,f1380]) ).
fof(f1397,plain,
( e4 != op(e0,e3)
| ~ spl34_90 ),
inference(superposition,[],[f232,f1382]) ).
fof(f1400,plain,
( e0 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2)
| e4 = op(e3,e2) ),
inference(forward_subsumption_resolution,[],[f86,f974]) ).
fof(f1401,plain,
( e0 = op(e3,e2)
| e2 = op(e3,e2)
| e4 = op(e3,e2)
| spl34_30 ),
inference(forward_subsumption_resolution,[],[f1400,f568]) ).
fof(f1404,definition,
( spl34_93
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_93])],[avatar_definition]) ).
fof(f1405,plain,
( e2 != op(e3,e2)
| spl34_93 ),
inference(avatar_component_clause,[],[f1404]) ).
fof(f1406,plain,
( e2 = op(e3,e2)
| ~ spl34_93 ),
inference(avatar_component_clause,[],[f1404]) ).
fof(f1408,definition,
( spl34_94
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl34_94])],[avatar_definition]) ).
fof(f1409,plain,
( e0 != op(e3,e2)
| spl34_94 ),
inference(avatar_component_clause,[],[f1408]) ).
fof(f1410,plain,
( e0 = op(e3,e2)
| ~ spl34_94 ),
inference(avatar_component_clause,[],[f1408]) ).
fof(f1413,plain,
( e2 != op(e1,e2)
| ~ spl34_93 ),
inference(superposition,[],[f239,f1406]) ).
fof(f1418,plain,
( $false
| ~ spl34_20
| ~ spl34_75
| ~ spl34_93 ),
inference(forward_subsumption_resolution,[],[f1413,f1091]) ).
fof(f1419,plain,
( ~ spl34_20
| ~ spl34_75
| ~ spl34_93 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
fof(f1421,plain,
( e2 != op(e1,e2)
| ~ spl34_20
| spl34_75 ),
inference(forward_demodulation,[],[f860,f522]) ).
fof(f1428,plain,
( $false
| ~ spl34_20
| spl34_75
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f1214,f1421]) ).
fof(f1429,plain,
( ~ spl34_20
| spl34_75
| ~ spl34_84 ),
inference(avatar_contradiction_clause,[],[f1428]) ).
fof(f1441,plain,
( ~ spl34_18
| ~ spl34_20 ),
inference(avatar_split_clause,[],[f1092,f521,f512]) ).
fof(f1442,plain,
( e2 = op(e1,e2)
| ~ spl34_20
| ~ spl34_75 ),
inference(forward_demodulation,[],[f861,f522]) ).
fof(f1455,plain,
( e2 != op(e4,e3)
| spl34_58 ),
inference(forward_demodulation,[],[f753,f928]) ).
fof(f1490,plain,
( e3 = op(e1,e3)
| ~ spl34_84 ),
inference(superposition,[],[f108,f998]) ).
fof(f1504,plain,
( e0 = op(e1,e0)
| ~ spl34_2
| ~ spl34_77 ),
inference(superposition,[],[f869,f441]) ).
fof(f1567,definition,
( spl34_95
<=> e3 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_95])],[avatar_definition]) ).
fof(f1568,plain,
( e3 != op(e4,e3)
| spl34_95 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1569,plain,
( e3 = op(e4,e3)
| ~ spl34_95 ),
inference(avatar_component_clause,[],[f1567]) ).
fof(f1571,definition,
( spl34_96
<=> e1 = op(e4,e3) ),
introduced(definition,[new_symbols(definition,[spl34_96])],[avatar_definition]) ).
fof(f1572,plain,
( e1 != op(e4,e3)
| spl34_96 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1573,plain,
( e1 = op(e4,e3)
| ~ spl34_96 ),
inference(avatar_component_clause,[],[f1571]) ).
fof(f1580,plain,
( e3 != op(e1,e3)
| ~ spl34_95 ),
inference(superposition,[],[f228,f1569]) ).
fof(f1584,plain,
( $false
| ~ spl34_84
| ~ spl34_95 ),
inference(forward_subsumption_resolution,[],[f1580,f1490]) ).
fof(f1585,plain,
( ~ spl34_84
| ~ spl34_95 ),
inference(avatar_contradiction_clause,[],[f1584]) ).
fof(f1588,plain,
( e1 != op(e4,e2)
| ~ spl34_96 ),
inference(superposition,[],[f167,f1573]) ).
fof(f1600,plain,
( $false
| ~ spl34_87
| ~ spl34_96 ),
inference(forward_subsumption_resolution,[],[f1588,f1281]) ).
fof(f1601,plain,
( ~ spl34_87
| ~ spl34_96 ),
inference(avatar_contradiction_clause,[],[f1600]) ).
fof(f1604,plain,
( e0 = op(e4,e0)
| e2 = op(e4,e0)
| e3 = op(e4,e0)
| e4 = op(e4,e0)
| spl34_89 ),
inference(forward_subsumption_resolution,[],[f83,f1301]) ).
fof(f1605,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e3 = op(e4,e3)
| e4 = op(e4,e3)
| spl34_58 ),
inference(forward_subsumption_resolution,[],[f80,f1455]) ).
fof(f1608,plain,
( e0 = op(e4,e3)
| e1 = op(e4,e3)
| e4 = op(e4,e3)
| spl34_58
| spl34_95 ),
inference(forward_subsumption_resolution,[],[f1605,f1568]) ).
fof(f1635,definition,
( spl34_97
<=> e2 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_97])],[avatar_definition]) ).
fof(f1636,plain,
( e2 != op(e4,e0)
| spl34_97 ),
inference(avatar_component_clause,[],[f1635]) ).
fof(f1637,plain,
( e2 = op(e4,e0)
| ~ spl34_97 ),
inference(avatar_component_clause,[],[f1635]) ).
fof(f1639,definition,
( spl34_98
<=> e0 = op(e4,e0) ),
introduced(definition,[new_symbols(definition,[spl34_98])],[avatar_definition]) ).
fof(f1640,plain,
( e0 != op(e4,e0)
| spl34_98 ),
inference(avatar_component_clause,[],[f1639]) ).
fof(f1672,plain,
e0 != op(e4,e3),
inference(superposition,[],[f165,f970]) ).
fof(f1673,plain,
e0 != op(e4,e2),
inference(superposition,[],[f166,f970]) ).
fof(f1675,plain,
e0 != op(e4,e0),
inference(superposition,[],[f171,f970]) ).
fof(f1710,plain,
( e1 = op(e4,e2)
| e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2) ),
inference(forward_subsumption_resolution,[],[f81,f1673]) ).
fof(f1711,plain,
( e2 = op(e4,e2)
| e3 = op(e4,e2)
| e4 = op(e4,e2)
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1710,f1280]) ).
fof(f1728,plain,
( e0 = e3
| ~ sP1 ),
inference(forward_demodulation,[],[f367,f970]) ).
fof(f1731,plain,
( e0 = e4
| ~ sP22 ),
inference(forward_demodulation,[],[f303,f430]) ).
fof(f1733,plain,
~ sP1,
inference(forward_subsumption_resolution,[],[f1728,f272]) ).
fof(f1736,plain,
~ sP22,
inference(forward_subsumption_resolution,[],[f1731,f271]) ).
fof(f1808,plain,
~ sP22,
inference(global_subsumption,[],[f1736]) ).
fof(f1811,plain,
( e3 = e4
| ~ sP11 ),
inference(forward_demodulation,[],[f337,f430]) ).
fof(f1815,plain,
~ sP11,
inference(forward_subsumption_resolution,[],[f1811,f265]) ).
fof(f1836,plain,
~ sP16,
inference(forward_subsumption_resolution,[],[f321,f973]) ).
fof(f1888,plain,
( sP21
| sP20
| spl34_1
| spl34_9
| spl34_11
| spl34_15
| spl34_17
| spl34_19
| spl34_23
| spl34_25
| spl34_27
| spl34_29
| spl34_31
| spl34_33
| spl34_35
| spl34_37 ),
inference(global_subsumption,[],[f1836,f1815,f1808,f1733,f973,f600,f591,f582,f573,f564,f546,f537,f519,f510,f501,f483,f474,f438,f434,f346]) ).
fof(f1894,plain,
~ spl34_98,
inference(avatar_split_clause,[],[f1675,f1639]) ).
fof(f1895,plain,
( sP20
| spl34_1
| spl34_5
| spl34_9
| spl34_11
| spl34_15
| spl34_17
| spl34_19
| spl34_23
| spl34_25
| spl34_27
| spl34_29
| spl34_31
| spl34_33
| spl34_35
| spl34_37 ),
inference(forward_subsumption_resolution,[],[f1888,f456]) ).
fof(f1896,plain,
( spl34_7
| spl34_1
| spl34_5
| spl34_9
| spl34_11
| spl34_15
| spl34_17
| spl34_19
| spl34_23
| spl34_25
| spl34_27
| spl34_29
| spl34_31
| spl34_33
| spl34_35
| spl34_37 ),
inference(avatar_split_clause,[],[f1895,f598,f589,f580,f571,f562,f553,f544,f535,f517,f508,f499,f481,f472,f454,f436,f463]) ).
fof(f1915,plain,
( e0 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0)
| e4 = op(e3,e0) ),
inference(forward_subsumption_resolution,[],[f88,f976]) ).
fof(f1935,plain,
( e0 = op(e3,e0)
| e2 = op(e3,e0)
| e4 = op(e3,e0)
| spl34_26 ),
inference(forward_subsumption_resolution,[],[f1915,f550]) ).
fof(f1936,plain,
( e2 = op(e4,e0)
| e3 = op(e4,e0)
| e4 = op(e4,e0)
| spl34_89
| spl34_98 ),
inference(forward_subsumption_resolution,[],[f1604,f1640]) ).
fof(f1937,plain,
( e2 = op(e4,e2)
| e3 = op(e4,e2)
| spl34_38
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1711,f604]) ).
fof(f1951,plain,
( e2 = op(e4,e2)
| spl34_38
| spl34_86
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1937,f1276]) ).
fof(f1954,plain,
( e2 != op(e1,e2)
| spl34_38
| spl34_86
| spl34_87 ),
inference(superposition,[],[f238,f1951]) ).
fof(f1960,plain,
( $false
| ~ spl34_20
| spl34_38
| ~ spl34_75
| spl34_86
| spl34_87 ),
inference(forward_subsumption_resolution,[],[f1954,f1442]) ).
fof(f1961,plain,
( ~ spl34_20
| spl34_38
| ~ spl34_75
| spl34_86
| spl34_87 ),
inference(avatar_contradiction_clause,[],[f1960]) ).
fof(f1964,plain,
( e1 = op(e4,e3)
| e4 = op(e4,e3)
| spl34_58
| spl34_95 ),
inference(forward_subsumption_resolution,[],[f1608,f1672]) ).
fof(f1975,definition,
( spl34_99
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_99])],[avatar_definition]) ).
fof(f1976,plain,
( e2 != op(e3,e0)
| spl34_99 ),
inference(avatar_component_clause,[],[f1975]) ).
fof(f1977,plain,
( e2 = op(e3,e0)
| ~ spl34_99 ),
inference(avatar_component_clause,[],[f1975]) ).
fof(f1979,definition,
( spl34_100
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl34_100])],[avatar_definition]) ).
fof(f1980,plain,
( e0 != op(e3,e0)
| spl34_100 ),
inference(avatar_component_clause,[],[f1979]) ).
fof(f1981,plain,
( e0 = op(e3,e0)
| ~ spl34_100 ),
inference(avatar_component_clause,[],[f1979]) ).
fof(f1988,plain,
( e0 != op(e3,e2)
| spl34_45
| ~ spl34_99 ),
inference(superposition,[],[f635,f1977]) ).
fof(f1992,plain,
( $false
| spl34_45
| ~ spl34_94
| ~ spl34_99 ),
inference(forward_subsumption_resolution,[],[f1988,f1410]) ).
fof(f1993,plain,
( spl34_45
| ~ spl34_94
| ~ spl34_99 ),
inference(avatar_contradiction_clause,[],[f1992]) ).
fof(f1998,plain,
( e0 != op(e1,e0)
| ~ spl34_100 ),
inference(superposition,[],[f259,f1981]) ).
fof(f2008,plain,
( $false
| ~ spl34_2
| ~ spl34_77
| ~ spl34_100 ),
inference(forward_subsumption_resolution,[],[f1998,f1504]) ).
fof(f2009,plain,
( ~ spl34_2
| ~ spl34_77
| ~ spl34_100 ),
inference(avatar_contradiction_clause,[],[f2008]) ).
fof(f2068,plain,
( e4 = op(e4,e3)
| spl34_58
| spl34_95
| spl34_96 ),
inference(forward_subsumption_resolution,[],[f1964,f1572]) ).
fof(f2069,plain,
( spl34_40
| spl34_58
| spl34_95
| spl34_96 ),
inference(avatar_split_clause,[],[f2068,f1571,f1567,f752,f611]) ).
fof(f2071,plain,
( e4 != op(e4,e1)
| ~ spl34_40 ),
inference(superposition,[],[f169,f612]) ).
fof(f2083,plain,
( $false
| ~ spl34_36
| ~ spl34_40 ),
inference(forward_subsumption_resolution,[],[f2071,f594]) ).
fof(f2084,plain,
( ~ spl34_36
| ~ spl34_40 ),
inference(avatar_contradiction_clause,[],[f2083]) ).
fof(f2168,plain,
( e4 = op(e0,e3)
| ~ sP32
| ~ spl34_88 ),
inference(forward_demodulation,[],[f281,f1298]) ).
fof(f2169,plain,
( e0 != op(e1,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| sP32
| spl34_42 ),
inference(forward_subsumption_resolution,[],[f418,f621]) ).
fof(f2176,plain,
( e0 = e2
| ~ sP10 ),
inference(forward_demodulation,[],[f339,f970]) ).
fof(f2181,plain,
( ~ sP32
| ~ spl34_88
| ~ spl34_90 ),
inference(forward_subsumption_resolution,[],[f2168,f1397]) ).
fof(f2186,plain,
~ sP10,
inference(forward_subsumption_resolution,[],[f2176,f273]) ).
fof(f2232,plain,
( ~ spl34_41
| ~ spl34_88
| ~ spl34_90 ),
inference(avatar_split_clause,[],[f2181,f1380,f1296,f616]) ).
fof(f2235,plain,
~ spl34_23,
inference(avatar_split_clause,[],[f2186,f535]) ).
fof(f2332,plain,
( e0 = e3
| ~ sP5 ),
inference(forward_demodulation,[],[f354,f970]) ).
fof(f2337,plain,
~ sP5,
inference(forward_subsumption_resolution,[],[f2332,f272]) ).
fof(f2352,plain,
( e1 = e4
| ~ sP17 ),
inference(forward_demodulation,[],[f318,f430]) ).
fof(f2357,plain,
~ sP17,
inference(forward_subsumption_resolution,[],[f2352,f268]) ).
fof(f2397,plain,
~ spl34_31,
inference(avatar_split_clause,[],[f2337,f571]) ).
fof(f2398,plain,
~ spl34_11,
inference(avatar_split_clause,[],[f2357,f481]) ).
fof(f2400,plain,
( e0 = e4
| ~ sP14 ),
inference(forward_demodulation,[],[f328,f430]) ).
fof(f2404,plain,
~ sP14,
inference(forward_subsumption_resolution,[],[f2400,f271]) ).
fof(f2439,plain,
( e0 = e2
| ~ sP2 ),
inference(forward_demodulation,[],[f364,f970]) ).
fof(f2443,plain,
~ sP2,
inference(forward_subsumption_resolution,[],[f2439,f273]) ).
fof(f2450,plain,
~ spl34_17,
inference(avatar_split_clause,[],[f2404,f508]) ).
fof(f2451,plain,
~ spl34_37,
inference(avatar_split_clause,[],[f2443,f598]) ).
fof(f2497,plain,
( e0 != op(e3,e2)
| ~ spl34_92 ),
inference(superposition,[],[f177,f1390]) ).
fof(f2510,plain,
( $false
| ~ spl34_92
| ~ spl34_94 ),
inference(forward_subsumption_resolution,[],[f2497,f1410]) ).
fof(f2511,plain,
( ~ spl34_92
| ~ spl34_94 ),
inference(avatar_contradiction_clause,[],[f2510]) ).
fof(f2516,plain,
( e3 != op(e1,e3)
| ~ spl34_91 ),
inference(superposition,[],[f229,f1386]) ).
fof(f2522,plain,
( $false
| ~ spl34_84
| ~ spl34_91 ),
inference(forward_subsumption_resolution,[],[f2516,f1490]) ).
fof(f2523,plain,
( ~ spl34_84
| ~ spl34_91 ),
inference(avatar_contradiction_clause,[],[f2522]) ).
fof(f2527,plain,
( e2 = op(e3,e0)
| e4 = op(e3,e0)
| spl34_26
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f1935,f1980]) ).
fof(f2528,plain,
( e0 = op(e3,e2)
| e4 = op(e3,e2)
| spl34_30
| spl34_93 ),
inference(forward_subsumption_resolution,[],[f1401,f1405]) ).
fof(f2576,plain,
( e4 = op(e3,e0)
| spl34_26
| spl34_99
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f2527,f1976]) ).
fof(f2582,plain,
( e3 = op(e0,e4)
| spl34_26
| ~ spl34_80
| spl34_99
| spl34_100 ),
inference(superposition,[],[f967,f2576]) ).
fof(f2590,plain,
( e3 != op(e2,e4)
| spl34_26
| ~ spl34_80
| spl34_99
| spl34_100 ),
inference(superposition,[],[f223,f2582]) ).
fof(f2598,plain,
( $false
| spl34_26
| ~ spl34_80
| spl34_99
| spl34_100 ),
inference(forward_subsumption_resolution,[],[f2590,f928]) ).
fof(f2599,plain,
( spl34_26
| ~ spl34_80
| spl34_99
| spl34_100 ),
inference(avatar_contradiction_clause,[],[f2598]) ).
fof(f2636,plain,
( e4 = op(e3,e2)
| spl34_30
| spl34_93
| spl34_94 ),
inference(forward_subsumption_resolution,[],[f2528,f1409]) ).
fof(f2637,plain,
( e4 != op(e2,e2)
| spl34_30
| spl34_93
| spl34_94 ),
inference(superposition,[],[f237,f2636]) ).
fof(f2648,plain,
( $false
| spl34_30
| spl34_93
| spl34_94 ),
inference(forward_subsumption_resolution,[],[f2637,f430]) ).
fof(f2649,plain,
( spl34_30
| spl34_93
| spl34_94 ),
inference(avatar_contradiction_clause,[],[f2648]) ).
fof(f2651,plain,
( e3 = op(e4,e0)
| e4 = op(e4,e0)
| spl34_89
| spl34_97
| spl34_98 ),
inference(forward_subsumption_resolution,[],[f1936,f1636]) ).
fof(f2655,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e4 = op(e2,e0) ),
inference(forward_subsumption_resolution,[],[f93,f938]) ).
fof(f2747,plain,
( e4 = op(e4,e0)
| spl34_88
| spl34_89
| spl34_97
| spl34_98 ),
inference(forward_subsumption_resolution,[],[f2651,f1297]) ).
fof(f2748,plain,
( spl34_34
| spl34_88
| spl34_89
| spl34_97
| spl34_98 ),
inference(avatar_split_clause,[],[f2747,f1639,f1635,f1300,f1296,f584]) ).
fof(f2749,plain,
( e0 != op(e1,op(e1,e0))
| e2 = op(e0,op(e2,e0))
| spl34_41
| spl34_42 ),
inference(forward_subsumption_resolution,[],[f2169,f617]) ).
fof(f2751,definition,
( spl34_103
<=> e0 = op(e1,op(e1,e0)) ),
introduced(definition,[new_symbols(definition,[spl34_103])],[avatar_definition]) ).
fof(f2753,plain,
( e0 != op(e1,op(e1,e0))
| spl34_103 ),
inference(avatar_component_clause,[],[f2751]) ).
fof(f2754,plain,
( spl34_43
| ~ spl34_103
| spl34_41
| spl34_42 ),
inference(avatar_split_clause,[],[f2749,f620,f616,f2751,f624]) ).
fof(f2766,plain,
( e2 = op(e0,e2)
| ~ spl34_85 ),
inference(superposition,[],[f110,f1002]) ).
fof(f2872,plain,
( op(e0,e0) != e1
| ~ spl34_10 ),
inference(superposition,[],[f264,f477]) ).
fof(f2890,plain,
( e3 != op(e3,e2)
| ~ spl34_26 ),
inference(superposition,[],[f183,f549]) ).
fof(f2904,plain,
( op(e0,e0) != e4
| ~ spl34_34 ),
inference(superposition,[],[f261,f585]) ).
fof(f3207,plain,
( e2 != op(e0,e2)
| ~ spl34_18
| spl34_43 ),
inference(forward_demodulation,[],[f625,f513]) ).
fof(f3209,plain,
( ~ spl34_30
| ~ spl34_26 ),
inference(avatar_split_clause,[],[f2890,f548,f566]) ).
fof(f3237,plain,
( e2 != op(e0,e2)
| ~ spl34_93 ),
inference(superposition,[],[f242,f1406]) ).
fof(f3362,plain,
( $false
| ~ spl34_18
| spl34_43
| ~ spl34_85 ),
inference(forward_subsumption_resolution,[],[f2766,f3207]) ).
fof(f3363,plain,
( ~ spl34_18
| spl34_43
| ~ spl34_85 ),
inference(avatar_contradiction_clause,[],[f3362]) ).
fof(f3364,plain,
( e2 = op(e0,e2)
| ~ spl34_18
| ~ spl34_43 ),
inference(forward_demodulation,[],[f626,f513]) ).
fof(f3365,plain,
( $false
| ~ spl34_18
| ~ spl34_43
| ~ spl34_93 ),
inference(forward_subsumption_resolution,[],[f3364,f3237]) ).
fof(f3366,plain,
( ~ spl34_18
| ~ spl34_43
| ~ spl34_93 ),
inference(avatar_contradiction_clause,[],[f3365]) ).
fof(f3369,plain,
( e1 = e4
| ~ sP13 ),
inference(forward_demodulation,[],[f331,f430]) ).
fof(f3373,plain,
~ sP13,
inference(forward_subsumption_resolution,[],[f3369,f268]) ).
fof(f3411,plain,
~ spl34_19,
inference(avatar_split_clause,[],[f3373,f517]) ).
fof(f3412,plain,
( e0 = e1
| ~ sP15 ),
inference(forward_demodulation,[],[f324,f970]) ).
fof(f3417,plain,
~ sP15,
inference(forward_subsumption_resolution,[],[f3412,f274]) ).
fof(f3461,plain,
( e0 = e1
| ~ sP3 ),
inference(forward_demodulation,[],[f361,f970]) ).
fof(f3465,plain,
~ sP3,
inference(forward_subsumption_resolution,[],[f3461,f274]) ).
fof(f3476,plain,
( e3 = e4
| ~ sP7 ),
inference(forward_demodulation,[],[f348,f430]) ).
fof(f3481,plain,
~ sP7,
inference(forward_subsumption_resolution,[],[f3476,f265]) ).
fof(f3501,plain,
~ sP8,
inference(global_subsumption,[],[f973,f346]) ).
fof(f3526,plain,
( ~ sP23
| ~ spl34_10 ),
inference(forward_subsumption_resolution,[],[f301,f2872]) ).
fof(f3590,plain,
~ spl34_15,
inference(avatar_split_clause,[],[f3417,f499]) ).
fof(f3591,plain,
~ spl34_35,
inference(avatar_split_clause,[],[f3465,f589]) ).
fof(f3592,plain,
~ spl34_29,
inference(avatar_split_clause,[],[f3481,f562]) ).
fof(f3593,plain,
~ spl34_27,
inference(avatar_split_clause,[],[f3501,f553]) ).
fof(f3594,plain,
( ~ spl34_1
| ~ spl34_10 ),
inference(avatar_split_clause,[],[f3526,f476,f436]) ).
fof(f3731,plain,
( ~ sP20
| ~ spl34_34 ),
inference(forward_subsumption_resolution,[],[f310,f2904]) ).
fof(f3732,plain,
( $false
| ~ spl34_7
| ~ spl34_34 ),
inference(forward_subsumption_resolution,[],[f3731,f464]) ).
fof(f3733,plain,
( ~ spl34_7
| ~ spl34_34 ),
inference(avatar_contradiction_clause,[],[f3732]) ).
fof(f3745,plain,
( ~ sP21
| spl34_92 ),
inference(forward_subsumption_resolution,[],[f306,f1389]) ).
fof(f3800,plain,
( ~ spl34_5
| spl34_92 ),
inference(avatar_split_clause,[],[f3745,f1388,f454]) ).
fof(f3916,plain,
( e0 = op(e1,e0)
| ~ spl34_84 ),
inference(superposition,[],[f114,f998]) ).
fof(f3924,plain,
( e0 != op(e1,e0)
| ~ spl34_2
| spl34_77 ),
inference(superposition,[],[f868,f441]) ).
fof(f4104,plain,
( $false
| ~ spl34_2
| spl34_77
| ~ spl34_84 ),
inference(forward_subsumption_resolution,[],[f3916,f3924]) ).
fof(f4105,plain,
( ~ spl34_2
| spl34_77
| ~ spl34_84 ),
inference(avatar_contradiction_clause,[],[f4104]) ).
fof(f4106,plain,
( e0 = op(e1,e0)
| ~ spl34_2
| ~ spl34_77 ),
inference(forward_demodulation,[],[f869,f441]) ).
fof(f4108,plain,
( e0 != op(e2,e0)
| ~ spl34_2
| ~ spl34_77 ),
inference(superposition,[],[f260,f4106]) ).
fof(f4112,plain,
( e0 != op(e1,e0)
| ~ spl34_2
| ~ spl34_77
| spl34_103 ),
inference(superposition,[],[f2753,f4106]) ).
fof(f4116,plain,
( $false
| ~ spl34_2
| ~ spl34_77
| spl34_103 ),
inference(forward_subsumption_resolution,[],[f4112,f4106]) ).
fof(f4117,plain,
( ~ spl34_2
| ~ spl34_77
| spl34_103 ),
inference(avatar_contradiction_clause,[],[f4116]) ).
fof(f4123,plain,
( e4 = op(e0,e2)
| ~ sP32
| ~ spl34_97 ),
inference(forward_demodulation,[],[f281,f1637]) ).
fof(f4151,plain,
( e4 = op(e0,e2)
| ~ spl34_41
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f4123,f618]) ).
fof(f4152,plain,
( e4 != op(e2,e2)
| ~ spl34_41
| ~ spl34_97 ),
inference(superposition,[],[f243,f4151]) ).
fof(f4159,plain,
( $false
| ~ spl34_41
| ~ spl34_97 ),
inference(forward_subsumption_resolution,[],[f4152,f430]) ).
fof(f4160,plain,
( ~ spl34_41
| ~ spl34_97 ),
inference(avatar_contradiction_clause,[],[f4159]) ).
fof(f4167,plain,
( e1 != op(e2,e0)
| ~ spl34_89 ),
inference(superposition,[],[f256,f1302]) ).
fof(f4268,plain,
( e0 = op(e2,e0)
| e2 = op(e2,e0)
| e4 = op(e2,e0)
| ~ spl34_89 ),
inference(forward_subsumption_resolution,[],[f2655,f4167]) ).
fof(f4274,plain,
( e0 = op(e2,e0)
| e4 = op(e2,e0)
| spl34_18
| ~ spl34_89 ),
inference(forward_subsumption_resolution,[],[f4268,f514]) ).
fof(f4330,plain,
( e4 = op(e2,e0)
| ~ spl34_2
| spl34_18
| ~ spl34_77
| ~ spl34_89 ),
inference(forward_subsumption_resolution,[],[f4274,f4108]) ).
fof(f4331,plain,
( e4 != op(e2,e2)
| ~ spl34_2
| spl34_18
| ~ spl34_77
| ~ spl34_89 ),
inference(superposition,[],[f193,f4330]) ).
fof(f4339,plain,
( $false
| ~ spl34_2
| spl34_18
| ~ spl34_77
| ~ spl34_89 ),
inference(forward_subsumption_resolution,[],[f4331,f430]) ).
fof(f4340,plain,
( ~ spl34_2
| spl34_18
| ~ spl34_77
| ~ spl34_89 ),
inference(avatar_contradiction_clause,[],[f4339]) ).
fof(f4341,plain,
( e1 = op(e2,e0)
| e2 = op(e2,e0)
| e4 = op(e2,e0)
| ~ spl34_2
| ~ spl34_77 ),
inference(forward_subsumption_resolution,[],[f2655,f4108]) ).
fof(f4344,plain,
( e1 = op(e2,e0)
| e4 = op(e2,e0)
| ~ spl34_2
| spl34_18
| ~ spl34_77 ),
inference(forward_subsumption_resolution,[],[f4341,f514]) ).
fof(f4390,definition,
( spl34_110
<=> e4 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_110])],[avatar_definition]) ).
fof(f4392,plain,
( e4 = op(e2,e0)
| ~ spl34_110 ),
inference(avatar_component_clause,[],[f4390]) ).
fof(f4394,definition,
( spl34_111
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl34_111])],[avatar_definition]) ).
fof(f4396,plain,
( e1 = op(e2,e0)
| ~ spl34_111 ),
inference(avatar_component_clause,[],[f4394]) ).
fof(f4397,plain,
( spl34_110
| spl34_111
| ~ spl34_2
| spl34_18
| ~ spl34_77 ),
inference(avatar_split_clause,[],[f4344,f867,f512,f440,f4394,f4390]) ).
fof(f4398,plain,
( e4 != op(e2,e2)
| ~ spl34_110 ),
inference(superposition,[],[f193,f4392]) ).
fof(f4405,plain,
( $false
| ~ spl34_110 ),
inference(forward_subsumption_resolution,[],[f4398,f430]) ).
fof(f4406,plain,
~ spl34_110,
inference(avatar_contradiction_clause,[],[f4405]) ).
fof(f4409,plain,
( e2 = op(e0,e1)
| ~ spl34_43
| ~ spl34_111 ),
inference(superposition,[],[f626,f4396]) ).
fof(f4415,plain,
( e0 = e2
| ~ spl34_2
| ~ spl34_43
| ~ spl34_111 ),
inference(superposition,[],[f4409,f441]) ).
fof(f4424,plain,
( $false
| ~ spl34_2
| ~ spl34_43
| ~ spl34_111 ),
inference(forward_subsumption_resolution,[],[f4415,f273]) ).
fof(f4425,plain,
( ~ spl34_2
| ~ spl34_43
| ~ spl34_111 ),
inference(avatar_contradiction_clause,[],[f4424]) ).
cnf(s390,plain,
( ~ spl34_9
| ~ spl34_10 ),
inference(sat_conversion,[],[f479]) ).
cnf(s422,plain,
( ~ spl34_25
| ~ spl34_26 ),
inference(sat_conversion,[],[f551]) ).
cnf(s438,plain,
( ~ spl34_33
| ~ spl34_34 ),
inference(sat_conversion,[],[f587]) ).
cnf(s558,plain,
( ~ spl34_42
| ~ spl34_45 ),
inference(sat_conversion,[],[f636]) ).
cnf(s783,plain,
( ~ spl34_42
| spl34_80 ),
inference(sat_conversion,[],[f968]) ).
cnf(s806,plain,
( spl34_81
| spl34_82
| spl34_83
| spl34_84
| spl34_85 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s816,plain,
~ spl34_81,
inference(sat_conversion,[],[f1031]) ).
cnf(s831,plain,
~ spl34_82,
inference(sat_conversion,[],[f1054]) ).
cnf(s846,plain,
~ spl34_83,
inference(sat_conversion,[],[f1073]) ).
cnf(s856,plain,
( spl34_20
| ~ spl34_84 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s879,plain,
( spl34_36
| ~ spl34_84 ),
inference(sat_conversion,[],[f1124]) ).
cnf(s888,plain,
( ~ spl34_36
| ~ spl34_38 ),
inference(sat_conversion,[],[f1134]) ).
cnf(s892,plain,
( ~ spl34_34
| ~ spl34_36 ),
inference(sat_conversion,[],[f1135]) ).
cnf(s907,plain,
( spl34_28
| ~ spl34_84 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s920,plain,
( ~ spl34_28
| ~ spl34_30 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s924,plain,
( ~ spl34_26
| ~ spl34_28 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s940,plain,
( spl34_2
| ~ spl34_84 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s952,plain,
( spl34_10
| ~ spl34_85 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s954,plain,
( spl34_18
| ~ spl34_85 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s956,plain,
( spl34_26
| ~ spl34_85 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s958,plain,
( spl34_34
| ~ spl34_85 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s1002,plain,
( ~ spl34_86
| ~ spl34_88 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s1032,plain,
( ~ spl34_58
| spl34_90
| spl34_91
| spl34_92 ),
inference(sat_conversion,[],[f1391]) ).
cnf(s1046,plain,
( ~ spl34_20
| ~ spl34_75
| ~ spl34_93 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s1069,plain,
( ~ spl34_20
| spl34_75
| ~ spl34_84 ),
inference(sat_conversion,[],[f1429]) ).
cnf(s1103,plain,
( ~ spl34_18
| ~ spl34_20 ),
inference(sat_conversion,[],[f1441]) ).
cnf(s1177,plain,
( ~ spl34_84
| ~ spl34_95 ),
inference(sat_conversion,[],[f1585]) ).
cnf(s1184,plain,
( ~ spl34_87
| ~ spl34_96 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s1333,plain,
~ spl34_98,
inference(sat_conversion,[],[f1894]) ).
cnf(s1339,plain,
( spl34_1
| spl34_5
| spl34_7
| spl34_9
| spl34_11
| spl34_15
| spl34_17
| spl34_19
| spl34_23
| spl34_25
| spl34_27
| spl34_29
| spl34_31
| spl34_33
| spl34_35
| spl34_37 ),
inference(sat_conversion,[],[f1896]) ).
cnf(s1372,plain,
( ~ spl34_20
| spl34_38
| ~ spl34_75
| spl34_86
| spl34_87 ),
inference(sat_conversion,[],[f1961]) ).
cnf(s1387,plain,
( spl34_45
| ~ spl34_94
| ~ spl34_99 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s1394,plain,
( ~ spl34_2
| ~ spl34_77
| ~ spl34_100 ),
inference(sat_conversion,[],[f2009]) ).
cnf(s1422,plain,
( spl34_40
| spl34_58
| spl34_95
| spl34_96 ),
inference(sat_conversion,[],[f2069]) ).
cnf(s1425,plain,
( ~ spl34_36
| ~ spl34_40 ),
inference(sat_conversion,[],[f2084]) ).
cnf(s1487,plain,
( ~ spl34_41
| ~ spl34_88
| ~ spl34_90 ),
inference(sat_conversion,[],[f2232]) ).
cnf(s1498,plain,
~ spl34_23,
inference(sat_conversion,[],[f2235]) ).
cnf(s1547,plain,
~ spl34_31,
inference(sat_conversion,[],[f2397]) ).
cnf(s1549,plain,
~ spl34_11,
inference(sat_conversion,[],[f2398]) ).
cnf(s1574,plain,
~ spl34_17,
inference(sat_conversion,[],[f2450]) ).
cnf(s1578,plain,
~ spl34_37,
inference(sat_conversion,[],[f2451]) ).
cnf(s1619,plain,
( ~ spl34_92
| ~ spl34_94 ),
inference(sat_conversion,[],[f2511]) ).
cnf(s1624,plain,
( ~ spl34_84
| ~ spl34_91 ),
inference(sat_conversion,[],[f2523]) ).
cnf(s1676,plain,
( spl34_26
| ~ spl34_80
| spl34_99
| spl34_100 ),
inference(sat_conversion,[],[f2599]) ).
cnf(s1710,plain,
( spl34_30
| spl34_93
| spl34_94 ),
inference(sat_conversion,[],[f2649]) ).
cnf(s1804,plain,
( spl34_34
| spl34_88
| spl34_89
| spl34_97
| spl34_98 ),
inference(sat_conversion,[],[f2748]) ).
cnf(s1809,plain,
( spl34_41
| spl34_42
| spl34_43
| ~ spl34_103 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s2094,plain,
( ~ spl34_26
| ~ spl34_30 ),
inference(sat_conversion,[],[f3209]) ).
cnf(s2200,plain,
( ~ spl34_18
| spl34_43
| ~ spl34_85 ),
inference(sat_conversion,[],[f3363]) ).
cnf(s2205,plain,
( ~ spl34_18
| ~ spl34_43
| ~ spl34_93 ),
inference(sat_conversion,[],[f3366]) ).
cnf(s2233,plain,
~ spl34_19,
inference(sat_conversion,[],[f3411]) ).
cnf(s2300,plain,
~ spl34_15,
inference(sat_conversion,[],[f3590]) ).
cnf(s2302,plain,
~ spl34_35,
inference(sat_conversion,[],[f3591]) ).
cnf(s2305,plain,
~ spl34_29,
inference(sat_conversion,[],[f3592]) ).
cnf(s2307,plain,
~ spl34_27,
inference(sat_conversion,[],[f3593]) ).
cnf(s2315,plain,
( ~ spl34_1
| ~ spl34_10 ),
inference(sat_conversion,[],[f3594]) ).
cnf(s2366,plain,
( ~ spl34_7
| ~ spl34_34 ),
inference(sat_conversion,[],[f3733]) ).
cnf(s2420,plain,
( ~ spl34_5
| spl34_92 ),
inference(sat_conversion,[],[f3800]) ).
cnf(s2600,plain,
( ~ spl34_2
| spl34_77
| ~ spl34_84 ),
inference(sat_conversion,[],[f4105]) ).
cnf(s2604,plain,
( ~ spl34_2
| ~ spl34_77
| spl34_103 ),
inference(sat_conversion,[],[f4117]) ).
cnf(s2615,plain,
( ~ spl34_41
| ~ spl34_97 ),
inference(sat_conversion,[],[f4160]) ).
cnf(s2738,plain,
( ~ spl34_2
| spl34_18
| ~ spl34_77
| ~ spl34_89 ),
inference(sat_conversion,[],[f4340]) ).
cnf(s2775,plain,
( ~ spl34_2
| spl34_18
| ~ spl34_77
| spl34_110
| spl34_111 ),
inference(sat_conversion,[],[f4397]) ).
cnf(s2779,plain,
~ spl34_110,
inference(sat_conversion,[],[f4406]) ).
cnf(s2788,plain,
( ~ spl34_2
| ~ spl34_43
| ~ spl34_111 ),
inference(sat_conversion,[],[f4425]) ).
cnf(s2789,plain,
( ~ spl34_2
| spl34_18
| ~ spl34_77
| spl34_111 ),
inference(rat,[],[s2775,s2779]) ).
cnf(s2802,plain,
( spl34_1
| spl34_5
| spl34_7
| spl34_9
| spl34_25
| spl34_33 ),
inference(rat,[],[s1339,s1578,s2302,s1547,s2305,s2307,s1498,s2233,s1574,s2300,s1549]) ).
cnf(s2806,plain,
( spl34_84
| spl34_85 ),
inference(rat,[],[s806,s846,s831,s816]) ).
cnf(s2810,plain,
( ~ spl34_85
| spl34_1 ),
inference(rat,[],[s1619,s1710,s2420,s2205,s2802,s390,s2200,s422,s2094,s438,s2366,s952,s954,s956,s958]) ).
cnf(s2811,plain,
( ~ spl34_42
| ~ spl34_84 ),
inference(rat,[],[s1387,s1676,s558,s783,s924,s1394,s2600,s940,s1710,s1046,s1069,s856,s920,s907]) ).
cnf(s2812,plain,
~ spl34_84,
inference(rat,[],[s1184,s1422,s1372,s1032,s1002,s1487,s1804,s2615,s1809,s2811,s1619,s2788,s1710,s2738,s2789,s2604,s1046,s1103,s888,s892,s1425,s920,s2600,s1069,s856,s879,s907,s940,s1177,s1624,s1333]) ).
cnf(s2813,plain,
spl34_85,
inference(rat,[],[s2806,s2812]) ).
cnf(s2821,plain,
spl34_10,
inference(rat,[],[s952,s2813]) ).
cnf(s2822,plain,
spl34_1,
inference(rat,[],[s2810,s2813]) ).
cnf(s2836,plain,
$false,
inference(rat,[],[s2315,s2821,s2822]) ).
fof(f4426,plain,
$false,
inference(avatar_sat_refutation,[],[s2836]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG056+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.08/0.19 % Computer : n013.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 19:21:59 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/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.88/0.40 % (1472102)Will run a generic schedule for satisfiability detection.
% 0.88/0.40 % (1472107)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3767120496_2999 on theBenchmark for (2999ds/0Mi)
% 0.88/0.40 % (1472108)% WARNING: option uhcvi not known.
% 0.88/0.40 % (1472108)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=980283644:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.88/0.40 % (1472110)dis+10_1_sil=32000:sp=arity:random_seed=1662792698:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.88/0.40 % (1472109)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=577170704:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.88/0.40 % (1472111)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3413474425:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.88/0.40 % (1472112)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=64417622:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.88/0.40 % (1472113)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2831881399:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.88/0.40 % Detected minimum model sizes of [5]
% 0.88/0.40 % Detected maximum model sizes of [max]
% 0.88/0.40 % TRYING [5]
% 0.88/0.40 % TRYING [6]
% 0.88/0.40 % TRYING [7]
% 0.88/0.40 % (1472110)Instruction limit reached!
% 0.88/0.40 % (1472110)------------------------------
% 0.88/0.40 % (1472110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.40 % (1472110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.40 % (1472110)CaDiCaL version: 2.1.3
% 0.88/0.40 % (1472110)Termination reason: Instruction limit
% 0.88/0.40 % (1472110)Termination phase: Saturation
% 0.88/0.40 % (1472110)Time elapsed: 0.055 s
% 0.88/0.40 % (1472110)Peak memory usage: 12 MB
% 0.88/0.40 % (1472110)Instructions burned: 105 (million)
% 0.88/0.40 % (1472111)Instruction limit reached!
% 0.88/0.40 % (1472111)------------------------------
% 0.88/0.40 % (1472111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.40 % (1472111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.40 % (1472111)CaDiCaL version: 2.1.3
% 0.88/0.40 % (1472111)Termination reason: Instruction limit
% 0.88/0.40 % (1472111)Termination phase: Saturation
% 0.88/0.40 % (1472111)Time elapsed: 0.059 s
% 0.88/0.40 % (1472111)Peak memory usage: 13 MB
% 0.88/0.40 % (1472111)Instructions burned: 116 (million)
% 0.88/0.40 % TRYING [8]
% 0.88/0.40 % (1472112)Instruction limit reached!
% 0.88/0.40 % (1472112)------------------------------
% 0.88/0.40 % (1472112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.40 % (1472112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.40 % (1472112)CaDiCaL version: 2.1.3
% 0.88/0.40 % (1472112)Termination reason: Instruction limit
% 0.88/0.40 % (1472112)Termination phase: Saturation
% 0.88/0.40 % (1472112)Time elapsed: 0.065 s
% 0.88/0.40 % (1472112)Peak memory usage: 13 MB
% 0.88/0.40 % (1472112)Instructions burned: 132 (million)
% 0.88/0.40 % (1472121)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1802667308:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.88/0.40 % (1472122)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1031253652:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.88/0.40 % (1472123)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=3928595609:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.88/0.40 % (1472113)Instruction limit reached!
% 0.88/0.40 % (1472113)------------------------------
% 0.88/0.40 % (1472113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.40 % (1472113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.40 % (1472113)CaDiCaL version: 2.1.3
% 0.88/0.40 % (1472113)Termination reason: Instruction limit
% 0.88/0.40 % (1472113)Termination phase: Saturation
% 0.88/0.40 % (1472113)Time elapsed: 0.088 s
% 0.88/0.40 % (1472113)Peak memory usage: 14 MB
% 0.88/0.40 % (1472113)Instructions burned: 160 (million)
% 0.88/0.40 % TRYING [9]
% 0.88/0.40 % Detected minimum model sizes of [5]
% 0.88/0.40 % Detected maximum model sizes of [max]
% 0.88/0.40 % TRYING [5]
% 0.88/0.40 % (1472127)ott-21_1_sil=16000:fs=off:random_seed=3610734523:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.88/0.40 % (1472109) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1472102-1472109"...
% 0.88/0.40 % TRYING [6]
% 0.88/0.40 % (1472122) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1472102-1472122"...
% 0.88/0.40 % (1472109)...printing done.
% 0.88/0.40 % (1472109)Refutation found. Thanks to Tanya!
% 0.88/0.40 % SZS status Theorem for theBenchmark
% 0.88/0.40 % SZS output start Proof for theBenchmark
% See solution above
% 0.88/0.41 % (1472109)------------------------------
% 0.88/0.41 % (1472109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.88/0.41 % (1472109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.88/0.41 % (1472109)CaDiCaL version: 2.1.3
% 0.88/0.41 % (1472109)Termination reason: Refutation
% 0.88/0.41 % (1472109)Time elapsed: 0.129 s
% 0.88/0.41 % (1472109)Peak memory usage: 15 MB
% 0.88/0.41 % (1472109)Instructions burned: 242 (million)
% 0.88/0.41 % (1472102)Success in time 0.173 s
% 0.88/0.41 % Vampire exiting
%------------------------------------------------------------------------------