%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG044+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:20:36 AM UTC 2026
% Result : Theorem 0.18s 0.27s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 78
% Syntax : Number of formulae : 426 ( 131 unt; 74 def)
% Number of atoms : 1966 (1083 equ)
% Maximal formula atoms : 220 ( 4 avg)
% Number of connectives : 2459 ( 919 ~; 990 |; 476 &)
% ( 74 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 66 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 127 ( 125 usr; 126 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( op(e0,e0) = e0
& op(e0,e1) = e1
& op(e0,e2) = e2
& op(e0,e3) = e3
& op(e1,e0) = e1
& op(e1,e1) = e3
& op(e1,e2) = e0
& op(e1,e3) = e2
& op(e2,e0) = e2
& op(e2,e1) = e0
& op(e2,e2) = e3
& op(e2,e3) = e1
& op(e3,e0) = e3
& op(e3,e1) = e2
& op(e3,e2) = e1
& op(e3,e3) = e0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
unit = e0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,conjecture,
( ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 )
& op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 )
& ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f5,negated_conjecture,
~ ( ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 )
& op(unit,e0) = e0
& op(e0,unit) = e0
& op(unit,e1) = e1
& op(e1,unit) = e1
& op(unit,e2) = e2
& op(e2,unit) = e2
& op(unit,e3) = e3
& op(e3,unit) = e3
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 )
& ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
inference(negated_conjecture,[status(cth)],[f4]) ).
fof(f6,plain,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 )
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3) )
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit )
| ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3) )
| ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0) )
| ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3) )
| ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0) )
| ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3) )
| ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0) )
| ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3) )
| ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0) )
| ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3) )
| ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1) )
| ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3) )
| ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1) )
| ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3) )
| ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1) )
| ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3) )
| ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1) )
| ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3) )
| ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2) )
| ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3) )
| ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2) )
| ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3) )
| ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2) )
| ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3) )
| ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2) )
| ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3) )
| ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3) )
| ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3) )
| ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3) )
| ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3) )
| ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3) )
| ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3) )
| ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 )
| ( e0 != op(e0,e0)
& e1 != op(e0,e0)
& e2 != op(e0,e0)
& e3 != op(e0,e0) )
| ( e0 != op(e0,e1)
& e1 != op(e0,e1)
& e2 != op(e0,e1)
& e3 != op(e0,e1) )
| ( e0 != op(e0,e2)
& e1 != op(e0,e2)
& e2 != op(e0,e2)
& e3 != op(e0,e2) )
| ( e0 != op(e0,e3)
& e1 != op(e0,e3)
& e2 != op(e0,e3)
& e3 != op(e0,e3) )
| ( e0 != op(e1,e0)
& e1 != op(e1,e0)
& e2 != op(e1,e0)
& e3 != op(e1,e0) )
| ( e0 != op(e1,e1)
& e1 != op(e1,e1)
& e2 != op(e1,e1)
& e3 != op(e1,e1) )
| ( e0 != op(e1,e2)
& e1 != op(e1,e2)
& e2 != op(e1,e2)
& e3 != op(e1,e2) )
| ( e0 != op(e1,e3)
& e1 != op(e1,e3)
& e2 != op(e1,e3)
& e3 != op(e1,e3) )
| ( e0 != op(e2,e0)
& e1 != op(e2,e0)
& e2 != op(e2,e0)
& e3 != op(e2,e0) )
| ( e0 != op(e2,e1)
& e1 != op(e2,e1)
& e2 != op(e2,e1)
& e3 != op(e2,e1) )
| ( e0 != op(e2,e2)
& e1 != op(e2,e2)
& e2 != op(e2,e2)
& e3 != op(e2,e2) )
| ( e0 != op(e2,e3)
& e1 != op(e2,e3)
& e2 != op(e2,e3)
& e3 != op(e2,e3) )
| ( e0 != op(e3,e0)
& e1 != op(e3,e0)
& e2 != op(e3,e0)
& e3 != op(e3,e0) )
| ( e0 != op(e3,e1)
& e1 != op(e3,e1)
& e2 != op(e3,e1)
& e3 != op(e3,e1) )
| ( e0 != op(e3,e2)
& e1 != op(e3,e2)
& e2 != op(e3,e2)
& e3 != op(e3,e2) )
| ( e0 != op(e3,e3)
& e1 != op(e3,e3)
& e2 != op(e3,e3)
& e3 != op(e3,e3) )
| e0 != op(unit,e0)
| e0 != op(e0,unit)
| e1 != op(unit,e1)
| e1 != op(e1,unit)
| e2 != op(unit,e2)
| e2 != op(e2,unit)
| e3 != op(unit,e3)
| e3 != op(e3,unit)
| ( e0 != unit
& e1 != unit
& e2 != unit
& e3 != unit )
| ( e0 != op(e0,e0)
& e0 != op(e0,e1)
& e0 != op(e0,e2)
& e0 != op(e0,e3) )
| ( e0 != op(e0,e0)
& e0 != op(e1,e0)
& e0 != op(e2,e0)
& e0 != op(e3,e0) )
| ( e1 != op(e0,e0)
& e1 != op(e0,e1)
& e1 != op(e0,e2)
& e1 != op(e0,e3) )
| ( e1 != op(e0,e0)
& e1 != op(e1,e0)
& e1 != op(e2,e0)
& e1 != op(e3,e0) )
| ( e2 != op(e0,e0)
& e2 != op(e0,e1)
& e2 != op(e0,e2)
& e2 != op(e0,e3) )
| ( e2 != op(e0,e0)
& e2 != op(e1,e0)
& e2 != op(e2,e0)
& e2 != op(e3,e0) )
| ( e3 != op(e0,e0)
& e3 != op(e0,e1)
& e3 != op(e0,e2)
& e3 != op(e0,e3) )
| ( e3 != op(e0,e0)
& e3 != op(e1,e0)
& e3 != op(e2,e0)
& e3 != op(e3,e0) )
| ( e0 != op(e1,e0)
& e0 != op(e1,e1)
& e0 != op(e1,e2)
& e0 != op(e1,e3) )
| ( e0 != op(e0,e1)
& e0 != op(e1,e1)
& e0 != op(e2,e1)
& e0 != op(e3,e1) )
| ( e1 != op(e1,e0)
& e1 != op(e1,e1)
& e1 != op(e1,e2)
& e1 != op(e1,e3) )
| ( e1 != op(e0,e1)
& e1 != op(e1,e1)
& e1 != op(e2,e1)
& e1 != op(e3,e1) )
| ( e2 != op(e1,e0)
& e2 != op(e1,e1)
& e2 != op(e1,e2)
& e2 != op(e1,e3) )
| ( e2 != op(e0,e1)
& e2 != op(e1,e1)
& e2 != op(e2,e1)
& e2 != op(e3,e1) )
| ( e3 != op(e1,e0)
& e3 != op(e1,e1)
& e3 != op(e1,e2)
& e3 != op(e1,e3) )
| ( e3 != op(e0,e1)
& e3 != op(e1,e1)
& e3 != op(e2,e1)
& e3 != op(e3,e1) )
| ( e0 != op(e2,e0)
& e0 != op(e2,e1)
& e0 != op(e2,e2)
& e0 != op(e2,e3) )
| ( e0 != op(e0,e2)
& e0 != op(e1,e2)
& e0 != op(e2,e2)
& e0 != op(e3,e2) )
| ( e1 != op(e2,e0)
& e1 != op(e2,e1)
& e1 != op(e2,e2)
& e1 != op(e2,e3) )
| ( e1 != op(e0,e2)
& e1 != op(e1,e2)
& e1 != op(e2,e2)
& e1 != op(e3,e2) )
| ( e2 != op(e2,e0)
& e2 != op(e2,e1)
& e2 != op(e2,e2)
& e2 != op(e2,e3) )
| ( e2 != op(e0,e2)
& e2 != op(e1,e2)
& e2 != op(e2,e2)
& e2 != op(e3,e2) )
| ( e3 != op(e2,e0)
& e3 != op(e2,e1)
& e3 != op(e2,e2)
& e3 != op(e2,e3) )
| ( e3 != op(e0,e2)
& e3 != op(e1,e2)
& e3 != op(e2,e2)
& e3 != op(e3,e2) )
| ( e0 != op(e3,e0)
& e0 != op(e3,e1)
& e0 != op(e3,e2)
& e0 != op(e3,e3) )
| ( e0 != op(e0,e3)
& e0 != op(e1,e3)
& e0 != op(e2,e3)
& e0 != op(e3,e3) )
| ( e1 != op(e3,e0)
& e1 != op(e3,e1)
& e1 != op(e3,e2)
& e1 != op(e3,e3) )
| ( e1 != op(e0,e3)
& e1 != op(e1,e3)
& e1 != op(e2,e3)
& e1 != op(e3,e3) )
| ( e2 != op(e3,e0)
& e2 != op(e3,e1)
& e2 != op(e3,e2)
& e2 != op(e3,e3) )
| ( e2 != op(e0,e3)
& e2 != op(e1,e3)
& e2 != op(e2,e3)
& e2 != op(e3,e3) )
| ( e3 != op(e3,e0)
& e3 != op(e3,e1)
& e3 != op(e3,e2)
& e3 != op(e3,e3) )
| ( e3 != op(e0,e3)
& e3 != op(e1,e3)
& e3 != op(e2,e3)
& e3 != op(e3,e3) ) ),
inference(flattening,[],[f6]) ).
fof(f11,plain,
e0 != e3,
inference(cnf_transformation,[],[f1]) ).
fof(f12,plain,
e0 != e2,
inference(cnf_transformation,[],[f1]) ).
fof(f13,plain,
e0 != e1,
inference(cnf_transformation,[],[f1]) ).
fof(f14,plain,
e0 = op(e3,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f15,plain,
e1 = op(e3,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f16,plain,
e2 = op(e3,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f17,plain,
e3 = op(e3,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f18,plain,
e1 = op(e2,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f19,plain,
e3 = op(e2,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f20,plain,
e0 = op(e2,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
e2 = op(e2,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f22,plain,
e2 = op(e1,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f23,plain,
e0 = op(e1,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
e3 = op(e1,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f25,plain,
e1 = op(e1,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f26,plain,
e3 = op(e0,e3),
inference(cnf_transformation,[],[f2]) ).
fof(f27,plain,
e2 = op(e0,e2),
inference(cnf_transformation,[],[f2]) ).
fof(f28,plain,
e1 = op(e0,e1),
inference(cnf_transformation,[],[f2]) ).
fof(f29,plain,
e0 = op(e0,e0),
inference(cnf_transformation,[],[f2]) ).
fof(f30,plain,
e0 = unit,
inference(cnf_transformation,[],[f3]) ).
fof(f32,plain,
( e0 = op(e2,e2)
| ~ sP50 ),
inference(cnf_transformation,[],[f7]) ).
fof(f35,plain,
( e1 = op(e3,e3)
| ~ sP49 ),
inference(cnf_transformation,[],[f7]) ).
fof(f42,plain,
( e2 = op(e0,e0)
| ~ sP48 ),
inference(cnf_transformation,[],[f7]) ).
fof(f46,plain,
( e3 = op(e0,e0)
| ~ sP47 ),
inference(cnf_transformation,[],[f7]) ).
fof(f50,plain,
( e0 != op(e0,e0)
| ~ sP46 ),
inference(cnf_transformation,[],[f7]) ).
fof(f53,plain,
( e1 != op(e0,e1)
| ~ sP45 ),
inference(cnf_transformation,[],[f7]) ).
fof(f56,plain,
( e2 != op(e0,e2)
| ~ sP44 ),
inference(cnf_transformation,[],[f7]) ).
fof(f59,plain,
( e3 != op(e0,e3)
| ~ sP43 ),
inference(cnf_transformation,[],[f7]) ).
fof(f65,plain,
( e1 != op(e1,e0)
| ~ sP42 ),
inference(cnf_transformation,[],[f7]) ).
fof(f67,plain,
( e3 != op(e1,e1)
| ~ sP41 ),
inference(cnf_transformation,[],[f7]) ).
fof(f74,plain,
( e0 != op(e1,e2)
| ~ sP40 ),
inference(cnf_transformation,[],[f7]) ).
fof(f76,plain,
( e2 != op(e1,e3)
| ~ sP39 ),
inference(cnf_transformation,[],[f7]) ).
fof(f80,plain,
( e2 != op(e2,e0)
| ~ sP38 ),
inference(cnf_transformation,[],[f7]) ).
fof(f86,plain,
( e0 != op(e2,e1)
| ~ sP37 ),
inference(cnf_transformation,[],[f7]) ).
fof(f87,plain,
( e3 != op(e2,e2)
| ~ sP36 ),
inference(cnf_transformation,[],[f7]) ).
fof(f93,plain,
( e1 != op(e2,e3)
| ~ sP35 ),
inference(cnf_transformation,[],[f7]) ).
fof(f95,plain,
( e3 != op(e3,e0)
| ~ sP34 ),
inference(cnf_transformation,[],[f7]) ).
fof(f100,plain,
( e2 != op(e3,e1)
| ~ sP33 ),
inference(cnf_transformation,[],[f7]) ).
fof(f105,plain,
( e1 != op(e3,e2)
| ~ sP32 ),
inference(cnf_transformation,[],[f7]) ).
fof(f110,plain,
( e0 != op(e3,e3)
| ~ sP31 ),
inference(cnf_transformation,[],[f7]) ).
fof(f114,plain,
( e0 != unit
| ~ sP30 ),
inference(cnf_transformation,[],[f7]) ).
fof(f118,plain,
( e0 != op(e0,e0)
| ~ sP29 ),
inference(cnf_transformation,[],[f7]) ).
fof(f122,plain,
( e0 != op(e0,e0)
| ~ sP28 ),
inference(cnf_transformation,[],[f7]) ).
fof(f125,plain,
( e1 != op(e0,e1)
| ~ sP27 ),
inference(cnf_transformation,[],[f7]) ).
fof(f129,plain,
( e1 != op(e1,e0)
| ~ sP26 ),
inference(cnf_transformation,[],[f7]) ).
fof(f132,plain,
( e2 != op(e0,e2)
| ~ sP25 ),
inference(cnf_transformation,[],[f7]) ).
fof(f136,plain,
( e2 != op(e2,e0)
| ~ sP24 ),
inference(cnf_transformation,[],[f7]) ).
fof(f139,plain,
( e3 != op(e0,e3)
| ~ sP23 ),
inference(cnf_transformation,[],[f7]) ).
fof(f143,plain,
( e3 != op(e3,e0)
| ~ sP22 ),
inference(cnf_transformation,[],[f7]) ).
fof(f148,plain,
( e0 != op(e1,e2)
| ~ sP21 ),
inference(cnf_transformation,[],[f7]) ).
fof(f152,plain,
( e0 != op(e2,e1)
| ~ sP20 ),
inference(cnf_transformation,[],[f7]) ).
fof(f158,plain,
( e1 != op(e1,e0)
| ~ sP19 ),
inference(cnf_transformation,[],[f7]) ).
fof(f162,plain,
( e1 != op(e0,e1)
| ~ sP18 ),
inference(cnf_transformation,[],[f7]) ).
fof(f163,plain,
( e2 != op(e1,e3)
| ~ sP17 ),
inference(cnf_transformation,[],[f7]) ).
fof(f167,plain,
( e2 != op(e3,e1)
| ~ sP16 ),
inference(cnf_transformation,[],[f7]) ).
fof(f173,plain,
( e3 != op(e1,e1)
| ~ sP15 ),
inference(cnf_transformation,[],[f7]) ).
fof(f177,plain,
( e3 != op(e1,e1)
| ~ sP14 ),
inference(cnf_transformation,[],[f7]) ).
fof(f181,plain,
( e0 != op(e2,e1)
| ~ sP13 ),
inference(cnf_transformation,[],[f7]) ).
fof(f185,plain,
( e0 != op(e1,e2)
| ~ sP12 ),
inference(cnf_transformation,[],[f7]) ).
fof(f187,plain,
( e1 != op(e2,e3)
| ~ sP11 ),
inference(cnf_transformation,[],[f7]) ).
fof(f191,plain,
( e1 != op(e3,e2)
| ~ sP10 ),
inference(cnf_transformation,[],[f7]) ).
fof(f198,plain,
( e2 != op(e2,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f7]) ).
fof(f202,plain,
( e2 != op(e0,e2)
| ~ sP8 ),
inference(cnf_transformation,[],[f7]) ).
fof(f204,plain,
( e3 != op(e2,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f7]) ).
fof(f208,plain,
( e3 != op(e2,e2)
| ~ sP6 ),
inference(cnf_transformation,[],[f7]) ).
fof(f211,plain,
( e0 != op(e3,e3)
| ~ sP5 ),
inference(cnf_transformation,[],[f7]) ).
fof(f215,plain,
( e0 != op(e3,e3)
| ~ sP4 ),
inference(cnf_transformation,[],[f7]) ).
fof(f220,plain,
( e1 != op(e3,e2)
| ~ sP3 ),
inference(cnf_transformation,[],[f7]) ).
fof(f224,plain,
( e1 != op(e2,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f7]) ).
fof(f229,plain,
( e2 != op(e3,e1)
| ~ sP1 ),
inference(cnf_transformation,[],[f7]) ).
fof(f233,plain,
( e2 != op(e1,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f7]) ).
fof(f238,plain,
( e3 != op(e0,e3)
| e3 != op(e3,e0)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| e0 != op(e0,unit)
| e0 != op(unit,e0)
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| sP49
| sP50 ),
inference(cnf_transformation,[],[f7]) ).
fof(f251,plain,
e1 != unit,
inference(definition_unfolding,[],[f13,f30]) ).
fof(f252,plain,
e2 != unit,
inference(definition_unfolding,[],[f12,f30]) ).
fof(f253,plain,
e3 != unit,
inference(definition_unfolding,[],[f11,f30]) ).
fof(f254,plain,
unit = op(unit,unit),
inference(definition_unfolding,[],[f29,f30,f30,f30]) ).
fof(f255,plain,
e1 = op(unit,e1),
inference(definition_unfolding,[],[f28,f30]) ).
fof(f256,plain,
e2 = op(unit,e2),
inference(definition_unfolding,[],[f27,f30]) ).
fof(f257,plain,
e3 = op(unit,e3),
inference(definition_unfolding,[],[f26,f30]) ).
fof(f258,plain,
e1 = op(e1,unit),
inference(definition_unfolding,[],[f25,f30]) ).
fof(f259,plain,
op(e1,e2) = unit,
inference(definition_unfolding,[],[f23,f30]) ).
fof(f260,plain,
e2 = op(e2,unit),
inference(definition_unfolding,[],[f21,f30]) ).
fof(f261,plain,
op(e2,e1) = unit,
inference(definition_unfolding,[],[f20,f30]) ).
fof(f262,plain,
e3 = op(e3,unit),
inference(definition_unfolding,[],[f17,f30]) ).
fof(f263,plain,
op(e3,e3) = unit,
inference(definition_unfolding,[],[f14,f30]) ).
fof(f276,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| e3 != op(e3,unit)
| e3 != op(unit,e3)
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| unit != op(unit,unit)
| unit != op(unit,unit)
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| sP49
| sP50 ),
inference(definition_unfolding,[],[f238,f30,f30,f30,f30,f30,f30]) ).
fof(f287,plain,
( op(e3,e3) != unit
| ~ sP4 ),
inference(definition_unfolding,[],[f215,f30]) ).
fof(f291,plain,
( op(e3,e3) != unit
| ~ sP5 ),
inference(definition_unfolding,[],[f211,f30]) ).
fof(f294,plain,
( e2 != op(unit,e2)
| ~ sP8 ),
inference(definition_unfolding,[],[f202,f30]) ).
fof(f295,plain,
( e2 != op(e2,unit)
| ~ sP9 ),
inference(definition_unfolding,[],[f198,f30]) ).
fof(f299,plain,
( op(e1,e2) != unit
| ~ sP12 ),
inference(definition_unfolding,[],[f185,f30]) ).
fof(f303,plain,
( op(e2,e1) != unit
| ~ sP13 ),
inference(definition_unfolding,[],[f181,f30]) ).
fof(f310,plain,
( e1 != op(unit,e1)
| ~ sP18 ),
inference(definition_unfolding,[],[f162,f30]) ).
fof(f311,plain,
( e1 != op(e1,unit)
| ~ sP19 ),
inference(definition_unfolding,[],[f158,f30]) ).
fof(f314,plain,
( op(e2,e1) != unit
| ~ sP20 ),
inference(definition_unfolding,[],[f152,f30]) ).
fof(f318,plain,
( op(e1,e2) != unit
| ~ sP21 ),
inference(definition_unfolding,[],[f148,f30]) ).
fof(f323,plain,
( e3 != op(e3,unit)
| ~ sP22 ),
inference(definition_unfolding,[],[f143,f30]) ).
fof(f327,plain,
( e3 != op(unit,e3)
| ~ sP23 ),
inference(definition_unfolding,[],[f139,f30]) ).
fof(f330,plain,
( e2 != op(e2,unit)
| ~ sP24 ),
inference(definition_unfolding,[],[f136,f30]) ).
fof(f334,plain,
( e2 != op(unit,e2)
| ~ sP25 ),
inference(definition_unfolding,[],[f132,f30]) ).
fof(f337,plain,
( e1 != op(e1,unit)
| ~ sP26 ),
inference(definition_unfolding,[],[f129,f30]) ).
fof(f341,plain,
( e1 != op(unit,e1)
| ~ sP27 ),
inference(definition_unfolding,[],[f125,f30]) ).
fof(f344,plain,
( unit != op(unit,unit)
| ~ sP28 ),
inference(definition_unfolding,[],[f122,f30,f30,f30]) ).
fof(f348,plain,
( unit != op(unit,unit)
| ~ sP29 ),
inference(definition_unfolding,[],[f118,f30,f30,f30]) ).
fof(f352,plain,
( unit != unit
| ~ sP30 ),
inference(definition_unfolding,[],[f114,f30]) ).
fof(f353,plain,
( op(e3,e3) != unit
| ~ sP31 ),
inference(definition_unfolding,[],[f110,f30]) ).
fof(f359,plain,
( e3 != op(e3,unit)
| ~ sP34 ),
inference(definition_unfolding,[],[f95,f30]) ).
fof(f362,plain,
( op(e2,e1) != unit
| ~ sP37 ),
inference(definition_unfolding,[],[f86,f30]) ).
fof(f365,plain,
( e2 != op(e2,unit)
| ~ sP38 ),
inference(definition_unfolding,[],[f80,f30]) ).
fof(f368,plain,
( op(e1,e2) != unit
| ~ sP40 ),
inference(definition_unfolding,[],[f74,f30]) ).
fof(f371,plain,
( e1 != op(e1,unit)
| ~ sP42 ),
inference(definition_unfolding,[],[f65,f30]) ).
fof(f377,plain,
( e3 != op(unit,e3)
| ~ sP43 ),
inference(definition_unfolding,[],[f59,f30]) ).
fof(f380,plain,
( e2 != op(unit,e2)
| ~ sP44 ),
inference(definition_unfolding,[],[f56,f30]) ).
fof(f383,plain,
( e1 != op(unit,e1)
| ~ sP45 ),
inference(definition_unfolding,[],[f53,f30]) ).
fof(f386,plain,
( unit != op(unit,unit)
| ~ sP46 ),
inference(definition_unfolding,[],[f50,f30,f30,f30]) ).
fof(f390,plain,
( e3 = op(unit,unit)
| ~ sP47 ),
inference(definition_unfolding,[],[f46,f30,f30]) ).
fof(f391,plain,
( e2 = op(unit,unit)
| ~ sP48 ),
inference(definition_unfolding,[],[f42,f30,f30]) ).
fof(f395,plain,
( op(e2,e2) = unit
| ~ sP50 ),
inference(definition_unfolding,[],[f32,f30]) ).
fof(f397,plain,
~ sP30,
inference(trivial_inequality_removal,[],[f352]) ).
fof(f401,plain,
( e3 != op(unit,e3)
| e3 != op(e3,unit)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13
| sP14
| sP15
| sP16
| sP17
| sP18
| sP19
| sP20
| sP21
| sP22
| sP23
| sP24
| sP25
| sP26
| sP27
| sP28
| sP29
| sP30
| e2 != op(e2,unit)
| e2 != op(unit,e2)
| e1 != op(e1,unit)
| e1 != op(unit,e1)
| unit != op(unit,unit)
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39
| sP40
| sP41
| sP42
| sP43
| sP44
| sP45
| sP46
| sP47
| sP48
| sP49
| sP50 ),
inference(duplicate_literal_removal,[],[f276]) ).
fof(f415,definition,
( spl51_1
<=> sP50 ),
introduced(definition,[new_symbols(definition,[spl51_1])],[avatar_definition]) ).
fof(f419,definition,
( spl51_2
<=> op(e3,e3) = unit ),
introduced(definition,[new_symbols(definition,[spl51_2])],[avatar_definition]) ).
fof(f421,plain,
( op(e3,e3) = unit
| ~ spl51_2 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f424,definition,
( spl51_3
<=> op(e2,e2) = unit ),
introduced(definition,[new_symbols(definition,[spl51_3])],[avatar_definition]) ).
fof(f426,plain,
( op(e2,e2) = unit
| ~ spl51_3 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f427,plain,
( ~ spl51_1
| spl51_3 ),
inference(avatar_split_clause,[],[f395,f424,f415]) ).
fof(f434,definition,
( spl51_5
<=> sP49 ),
introduced(definition,[new_symbols(definition,[spl51_5])],[avatar_definition]) ).
fof(f438,definition,
( spl51_6
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl51_6])],[avatar_definition]) ).
fof(f440,plain,
( e1 = op(e3,e3)
| ~ spl51_6 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( ~ spl51_5
| spl51_6 ),
inference(avatar_split_clause,[],[f35,f438,f434]) ).
fof(f458,definition,
( spl51_10
<=> sP48 ),
introduced(definition,[new_symbols(definition,[spl51_10])],[avatar_definition]) ).
fof(f477,definition,
( spl51_14
<=> e2 = op(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl51_14])],[avatar_definition]) ).
fof(f479,plain,
( e2 = op(unit,unit)
| ~ spl51_14 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f480,plain,
( ~ spl51_10
| spl51_14 ),
inference(avatar_split_clause,[],[f391,f477,f458]) ).
fof(f482,definition,
( spl51_15
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl51_15])],[avatar_definition]) ).
fof(f491,definition,
( spl51_17
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl51_17])],[avatar_definition]) ).
fof(f493,plain,
( e3 = op(e2,e2)
| ~ spl51_17 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f496,definition,
( spl51_18
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl51_18])],[avatar_definition]) ).
fof(f501,definition,
( spl51_19
<=> e3 = op(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl51_19])],[avatar_definition]) ).
fof(f503,plain,
( e3 = op(unit,unit)
| ~ spl51_19 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f504,plain,
( ~ spl51_15
| spl51_19 ),
inference(avatar_split_clause,[],[f390,f501,f482]) ).
fof(f506,definition,
( spl51_20
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl51_20])],[avatar_definition]) ).
fof(f513,definition,
( spl51_21
<=> unit = op(unit,unit) ),
introduced(definition,[new_symbols(definition,[spl51_21])],[avatar_definition]) ).
fof(f514,plain,
( unit = op(unit,unit)
| ~ spl51_21 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f516,plain,
( ~ spl51_20
| ~ spl51_21 ),
inference(avatar_split_clause,[],[f386,f513,f506]) ).
fof(f518,definition,
( spl51_22
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl51_22])],[avatar_definition]) ).
fof(f532,definition,
( spl51_25
<=> e1 = op(unit,e1) ),
introduced(definition,[new_symbols(definition,[spl51_25])],[avatar_definition]) ).
fof(f535,plain,
( ~ spl51_22
| ~ spl51_25 ),
inference(avatar_split_clause,[],[f383,f532,f518]) ).
fof(f542,definition,
( spl51_27
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl51_27])],[avatar_definition]) ).
fof(f551,definition,
( spl51_29
<=> e2 = op(unit,e2) ),
introduced(definition,[new_symbols(definition,[spl51_29])],[avatar_definition]) ).
fof(f554,plain,
( ~ spl51_27
| ~ spl51_29 ),
inference(avatar_split_clause,[],[f380,f551,f542]) ).
fof(f566,definition,
( spl51_32
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl51_32])],[avatar_definition]) ).
fof(f570,definition,
( spl51_33
<=> e3 = op(unit,e3) ),
introduced(definition,[new_symbols(definition,[spl51_33])],[avatar_definition]) ).
fof(f573,plain,
( ~ spl51_32
| ~ spl51_33 ),
inference(avatar_split_clause,[],[f377,f570,f566]) ).
fof(f590,definition,
( spl51_37
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl51_37])],[avatar_definition]) ).
fof(f604,definition,
( spl51_40
<=> e1 = op(e1,unit) ),
introduced(definition,[new_symbols(definition,[spl51_40])],[avatar_definition]) ).
fof(f607,plain,
( ~ spl51_37
| ~ spl51_40 ),
inference(avatar_split_clause,[],[f371,f604,f590]) ).
fof(f614,definition,
( spl51_42
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl51_42])],[avatar_definition]) ).
fof(f617,plain,
( ~ spl51_42
| ~ spl51_18 ),
inference(avatar_split_clause,[],[f67,f496,f614]) ).
fof(f622,definition,
( spl51_43
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl51_43])],[avatar_definition]) ).
fof(f641,definition,
( spl51_47
<=> op(e1,e2) = unit ),
introduced(definition,[new_symbols(definition,[spl51_47])],[avatar_definition]) ).
fof(f644,plain,
( ~ spl51_43
| ~ spl51_47 ),
inference(avatar_split_clause,[],[f368,f641,f622]) ).
fof(f646,definition,
( spl51_48
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl51_48])],[avatar_definition]) ).
fof(f655,definition,
( spl51_50
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl51_50])],[avatar_definition]) ).
fof(f658,plain,
( ~ spl51_48
| ~ spl51_50 ),
inference(avatar_split_clause,[],[f76,f655,f646]) ).
fof(f670,definition,
( spl51_53
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl51_53])],[avatar_definition]) ).
fof(f679,definition,
( spl51_55
<=> e2 = op(e2,unit) ),
introduced(definition,[new_symbols(definition,[spl51_55])],[avatar_definition]) ).
fof(f682,plain,
( ~ spl51_53
| ~ spl51_55 ),
inference(avatar_split_clause,[],[f365,f679,f670]) ).
fof(f694,definition,
( spl51_58
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl51_58])],[avatar_definition]) ).
fof(f713,definition,
( spl51_62
<=> op(e2,e1) = unit ),
introduced(definition,[new_symbols(definition,[spl51_62])],[avatar_definition]) ).
fof(f716,plain,
( ~ spl51_58
| ~ spl51_62 ),
inference(avatar_split_clause,[],[f362,f713,f694]) ).
fof(f718,definition,
( spl51_63
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl51_63])],[avatar_definition]) ).
fof(f721,plain,
( ~ spl51_63
| ~ spl51_17 ),
inference(avatar_split_clause,[],[f87,f491,f718]) ).
fof(f726,definition,
( spl51_64
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl51_64])],[avatar_definition]) ).
fof(f740,definition,
( spl51_67
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl51_67])],[avatar_definition]) ).
fof(f743,plain,
( ~ spl51_64
| ~ spl51_67 ),
inference(avatar_split_clause,[],[f93,f740,f726]) ).
fof(f750,definition,
( spl51_69
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl51_69])],[avatar_definition]) ).
fof(f754,definition,
( spl51_70
<=> e3 = op(e3,unit) ),
introduced(definition,[new_symbols(definition,[spl51_70])],[avatar_definition]) ).
fof(f757,plain,
( ~ spl51_69
| ~ spl51_70 ),
inference(avatar_split_clause,[],[f359,f754,f750]) ).
fof(f774,definition,
( spl51_74
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl51_74])],[avatar_definition]) ).
fof(f783,definition,
( spl51_76
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl51_76])],[avatar_definition]) ).
fof(f786,plain,
( ~ spl51_74
| ~ spl51_76 ),
inference(avatar_split_clause,[],[f100,f783,f774]) ).
fof(f798,definition,
( spl51_79
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl51_79])],[avatar_definition]) ).
fof(f812,definition,
( spl51_82
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl51_82])],[avatar_definition]) ).
fof(f815,plain,
( ~ spl51_79
| ~ spl51_82 ),
inference(avatar_split_clause,[],[f105,f812,f798]) ).
fof(f822,definition,
( spl51_84
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl51_84])],[avatar_definition]) ).
fof(f828,plain,
( ~ spl51_84
| ~ spl51_2 ),
inference(avatar_split_clause,[],[f353,f419,f822]) ).
fof(f830,definition,
( spl51_85
<=> sP30 ),
introduced(definition,[new_symbols(definition,[spl51_85])],[avatar_definition]) ).
fof(f834,definition,
( spl51_86
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl51_86])],[avatar_definition]) ).
fof(f836,plain,
( e3 != unit
| spl51_86 ),
inference(avatar_component_clause,[],[f834]) ).
fof(f839,definition,
( spl51_87
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl51_87])],[avatar_definition]) ).
fof(f841,plain,
( e2 != unit
| spl51_87 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f844,definition,
( spl51_88
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl51_88])],[avatar_definition]) ).
fof(f846,plain,
( e1 != unit
| spl51_88 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f848,plain,
~ spl51_85,
inference(avatar_split_clause,[],[f397,f830]) ).
fof(f850,definition,
( spl51_89
<=> sP29 ),
introduced(definition,[new_symbols(definition,[spl51_89])],[avatar_definition]) ).
fof(f856,plain,
( ~ spl51_89
| ~ spl51_21 ),
inference(avatar_split_clause,[],[f348,f513,f850]) ).
fof(f858,definition,
( spl51_90
<=> sP28 ),
introduced(definition,[new_symbols(definition,[spl51_90])],[avatar_definition]) ).
fof(f864,plain,
( ~ spl51_90
| ~ spl51_21 ),
inference(avatar_split_clause,[],[f344,f513,f858]) ).
fof(f866,definition,
( spl51_91
<=> sP27 ),
introduced(definition,[new_symbols(definition,[spl51_91])],[avatar_definition]) ).
fof(f871,plain,
( ~ spl51_91
| ~ spl51_25 ),
inference(avatar_split_clause,[],[f341,f532,f866]) ).
fof(f874,definition,
( spl51_92
<=> sP26 ),
introduced(definition,[new_symbols(definition,[spl51_92])],[avatar_definition]) ).
fof(f879,plain,
( ~ spl51_92
| ~ spl51_40 ),
inference(avatar_split_clause,[],[f337,f604,f874]) ).
fof(f882,definition,
( spl51_93
<=> sP25 ),
introduced(definition,[new_symbols(definition,[spl51_93])],[avatar_definition]) ).
fof(f886,plain,
( ~ spl51_93
| ~ spl51_29 ),
inference(avatar_split_clause,[],[f334,f551,f882]) ).
fof(f890,definition,
( spl51_94
<=> sP24 ),
introduced(definition,[new_symbols(definition,[spl51_94])],[avatar_definition]) ).
fof(f894,plain,
( ~ spl51_94
| ~ spl51_55 ),
inference(avatar_split_clause,[],[f330,f679,f890]) ).
fof(f898,definition,
( spl51_95
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl51_95])],[avatar_definition]) ).
fof(f901,plain,
( ~ spl51_95
| ~ spl51_33 ),
inference(avatar_split_clause,[],[f327,f570,f898]) ).
fof(f906,definition,
( spl51_96
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl51_96])],[avatar_definition]) ).
fof(f909,plain,
( ~ spl51_96
| ~ spl51_70 ),
inference(avatar_split_clause,[],[f323,f754,f906]) ).
fof(f914,definition,
( spl51_97
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl51_97])],[avatar_definition]) ).
fof(f918,plain,
( ~ spl51_97
| ~ spl51_47 ),
inference(avatar_split_clause,[],[f318,f641,f914]) ).
fof(f922,definition,
( spl51_98
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl51_98])],[avatar_definition]) ).
fof(f926,plain,
( ~ spl51_98
| ~ spl51_62 ),
inference(avatar_split_clause,[],[f314,f713,f922]) ).
fof(f930,definition,
( spl51_99
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl51_99])],[avatar_definition]) ).
fof(f936,plain,
( ~ spl51_99
| ~ spl51_40 ),
inference(avatar_split_clause,[],[f311,f604,f930]) ).
fof(f938,definition,
( spl51_100
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl51_100])],[avatar_definition]) ).
fof(f944,plain,
( ~ spl51_100
| ~ spl51_25 ),
inference(avatar_split_clause,[],[f310,f532,f938]) ).
fof(f946,definition,
( spl51_101
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl51_101])],[avatar_definition]) ).
fof(f949,plain,
( ~ spl51_101
| ~ spl51_50 ),
inference(avatar_split_clause,[],[f163,f655,f946]) ).
fof(f954,definition,
( spl51_102
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl51_102])],[avatar_definition]) ).
fof(f957,plain,
( ~ spl51_102
| ~ spl51_76 ),
inference(avatar_split_clause,[],[f167,f783,f954]) ).
fof(f962,definition,
( spl51_103
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl51_103])],[avatar_definition]) ).
fof(f967,plain,
( ~ spl51_103
| ~ spl51_18 ),
inference(avatar_split_clause,[],[f173,f496,f962]) ).
fof(f970,definition,
( spl51_104
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl51_104])],[avatar_definition]) ).
fof(f975,plain,
( ~ spl51_104
| ~ spl51_18 ),
inference(avatar_split_clause,[],[f177,f496,f970]) ).
fof(f978,definition,
( spl51_105
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl51_105])],[avatar_definition]) ).
fof(f983,plain,
( ~ spl51_105
| ~ spl51_62 ),
inference(avatar_split_clause,[],[f303,f713,f978]) ).
fof(f986,definition,
( spl51_106
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl51_106])],[avatar_definition]) ).
fof(f991,plain,
( ~ spl51_106
| ~ spl51_47 ),
inference(avatar_split_clause,[],[f299,f641,f986]) ).
fof(f994,definition,
( spl51_107
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl51_107])],[avatar_definition]) ).
fof(f997,plain,
( ~ spl51_107
| ~ spl51_67 ),
inference(avatar_split_clause,[],[f187,f740,f994]) ).
fof(f1002,definition,
( spl51_108
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl51_108])],[avatar_definition]) ).
fof(f1005,plain,
( ~ spl51_108
| ~ spl51_82 ),
inference(avatar_split_clause,[],[f191,f812,f1002]) ).
fof(f1010,definition,
( spl51_109
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl51_109])],[avatar_definition]) ).
fof(f1016,plain,
( ~ spl51_109
| ~ spl51_55 ),
inference(avatar_split_clause,[],[f295,f679,f1010]) ).
fof(f1018,definition,
( spl51_110
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl51_110])],[avatar_definition]) ).
fof(f1024,plain,
( ~ spl51_110
| ~ spl51_29 ),
inference(avatar_split_clause,[],[f294,f551,f1018]) ).
fof(f1026,definition,
( spl51_111
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl51_111])],[avatar_definition]) ).
fof(f1030,plain,
( ~ spl51_111
| ~ spl51_17 ),
inference(avatar_split_clause,[],[f204,f491,f1026]) ).
fof(f1034,definition,
( spl51_112
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl51_112])],[avatar_definition]) ).
fof(f1038,plain,
( ~ spl51_112
| ~ spl51_17 ),
inference(avatar_split_clause,[],[f208,f491,f1034]) ).
fof(f1042,definition,
( spl51_113
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl51_113])],[avatar_definition]) ).
fof(f1045,plain,
( ~ spl51_113
| ~ spl51_2 ),
inference(avatar_split_clause,[],[f291,f419,f1042]) ).
fof(f1050,definition,
( spl51_114
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl51_114])],[avatar_definition]) ).
fof(f1053,plain,
( ~ spl51_114
| ~ spl51_2 ),
inference(avatar_split_clause,[],[f287,f419,f1050]) ).
fof(f1058,definition,
( spl51_115
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl51_115])],[avatar_definition]) ).
fof(f1062,plain,
( ~ spl51_115
| ~ spl51_82 ),
inference(avatar_split_clause,[],[f220,f812,f1058]) ).
fof(f1066,definition,
( spl51_116
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl51_116])],[avatar_definition]) ).
fof(f1070,plain,
( ~ spl51_116
| ~ spl51_67 ),
inference(avatar_split_clause,[],[f224,f740,f1066]) ).
fof(f1074,definition,
( spl51_117
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl51_117])],[avatar_definition]) ).
fof(f1079,plain,
( ~ spl51_117
| ~ spl51_76 ),
inference(avatar_split_clause,[],[f229,f783,f1074]) ).
fof(f1082,definition,
( spl51_118
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl51_118])],[avatar_definition]) ).
fof(f1087,plain,
( ~ spl51_118
| ~ spl51_50 ),
inference(avatar_split_clause,[],[f233,f655,f1082]) ).
fof(f1092,plain,
( spl51_1
| spl51_5
| spl51_10
| spl51_15
| spl51_20
| spl51_22
| spl51_27
| spl51_32
| spl51_37
| spl51_42
| spl51_43
| spl51_48
| spl51_53
| spl51_58
| spl51_63
| spl51_64
| spl51_69
| spl51_74
| spl51_79
| spl51_84
| ~ spl51_21
| ~ spl51_25
| ~ spl51_40
| ~ spl51_29
| ~ spl51_55
| spl51_85
| spl51_89
| spl51_90
| spl51_91
| spl51_92
| spl51_93
| spl51_94
| spl51_95
| spl51_96
| spl51_97
| spl51_98
| spl51_99
| spl51_100
| spl51_101
| spl51_102
| spl51_103
| spl51_104
| spl51_105
| spl51_106
| spl51_107
| spl51_108
| spl51_109
| spl51_110
| spl51_111
| spl51_112
| spl51_113
| spl51_114
| spl51_115
| spl51_116
| spl51_117
| spl51_118
| ~ spl51_70
| ~ spl51_33 ),
inference(avatar_split_clause,[],[f401,f570,f754,f1082,f1074,f1066,f1058,f1050,f1042,f1034,f1026,f1018,f1010,f1002,f994,f986,f978,f970,f962,f954,f946,f938,f930,f922,f914,f906,f898,f890,f882,f874,f866,f858,f850,f830,f679,f551,f604,f532,f513,f822,f798,f774,f750,f726,f718,f694,f670,f646,f622,f614,f590,f566,f542,f518,f506,f482,f458,f434,f415]) ).
fof(f1105,plain,
spl51_2,
inference(avatar_split_clause,[],[f263,f419]) ).
fof(f1106,plain,
spl51_82,
inference(avatar_split_clause,[],[f15,f812]) ).
fof(f1107,plain,
spl51_76,
inference(avatar_split_clause,[],[f16,f783]) ).
fof(f1108,plain,
spl51_70,
inference(avatar_split_clause,[],[f262,f754]) ).
fof(f1109,plain,
spl51_67,
inference(avatar_split_clause,[],[f18,f740]) ).
fof(f1110,plain,
spl51_17,
inference(avatar_split_clause,[],[f19,f491]) ).
fof(f1111,plain,
spl51_62,
inference(avatar_split_clause,[],[f261,f713]) ).
fof(f1112,plain,
spl51_55,
inference(avatar_split_clause,[],[f260,f679]) ).
fof(f1113,plain,
spl51_50,
inference(avatar_split_clause,[],[f22,f655]) ).
fof(f1114,plain,
spl51_47,
inference(avatar_split_clause,[],[f259,f641]) ).
fof(f1115,plain,
spl51_18,
inference(avatar_split_clause,[],[f24,f496]) ).
fof(f1116,plain,
spl51_40,
inference(avatar_split_clause,[],[f258,f604]) ).
fof(f1117,plain,
spl51_33,
inference(avatar_split_clause,[],[f257,f570]) ).
fof(f1118,plain,
spl51_29,
inference(avatar_split_clause,[],[f256,f551]) ).
fof(f1119,plain,
spl51_25,
inference(avatar_split_clause,[],[f255,f532]) ).
fof(f1120,plain,
spl51_21,
inference(avatar_split_clause,[],[f254,f513]) ).
fof(f1121,plain,
~ spl51_86,
inference(avatar_split_clause,[],[f253,f834]) ).
fof(f1122,plain,
~ spl51_87,
inference(avatar_split_clause,[],[f252,f839]) ).
fof(f1123,plain,
~ spl51_88,
inference(avatar_split_clause,[],[f251,f844]) ).
fof(f1124,plain,
( e1 = unit
| ~ spl51_2
| ~ spl51_6 ),
inference(forward_demodulation,[],[f440,f421]) ).
fof(f1125,plain,
( $false
| ~ spl51_2
| ~ spl51_6
| spl51_88 ),
inference(forward_subsumption_resolution,[],[f1124,f846]) ).
fof(f1126,plain,
( ~ spl51_2
| ~ spl51_6
| spl51_88 ),
inference(avatar_contradiction_clause,[],[f1125]) ).
fof(f1145,plain,
( e3 = unit
| ~ spl51_19
| ~ spl51_21 ),
inference(forward_demodulation,[],[f503,f514]) ).
fof(f1146,plain,
( e2 = unit
| ~ spl51_14
| ~ spl51_21 ),
inference(forward_demodulation,[],[f479,f514]) ).
fof(f1151,plain,
( $false
| ~ spl51_19
| ~ spl51_21
| spl51_86 ),
inference(forward_subsumption_resolution,[],[f1145,f836]) ).
fof(f1152,plain,
( ~ spl51_19
| ~ spl51_21
| spl51_86 ),
inference(avatar_contradiction_clause,[],[f1151]) ).
fof(f1153,plain,
( $false
| ~ spl51_14
| ~ spl51_21
| spl51_87 ),
inference(forward_subsumption_resolution,[],[f1146,f841]) ).
fof(f1154,plain,
( ~ spl51_14
| ~ spl51_21
| spl51_87 ),
inference(avatar_contradiction_clause,[],[f1153]) ).
fof(f1164,plain,
( e3 = unit
| ~ spl51_3
| ~ spl51_17 ),
inference(superposition,[],[f493,f426]) ).
fof(f1168,plain,
( $false
| ~ spl51_3
| ~ spl51_17
| spl51_86 ),
inference(forward_subsumption_resolution,[],[f1164,f836]) ).
fof(f1169,plain,
( ~ spl51_3
| ~ spl51_17
| spl51_86 ),
inference(avatar_contradiction_clause,[],[f1168]) ).
cnf(s2,plain,
( ~ spl51_1
| spl51_3 ),
inference(sat_conversion,[],[f427]) ).
cnf(s4,plain,
( ~ spl51_5
| spl51_6 ),
inference(sat_conversion,[],[f441]) ).
cnf(s11,plain,
( ~ spl51_10
| spl51_14 ),
inference(sat_conversion,[],[f480]) ).
cnf(s15,plain,
( ~ spl51_15
| spl51_19 ),
inference(sat_conversion,[],[f504]) ).
cnf(s19,plain,
( ~ spl51_20
| ~ spl51_21 ),
inference(sat_conversion,[],[f516]) ).
cnf(s22,plain,
( ~ spl51_22
| ~ spl51_25 ),
inference(sat_conversion,[],[f535]) ).
cnf(s25,plain,
( ~ spl51_27
| ~ spl51_29 ),
inference(sat_conversion,[],[f554]) ).
cnf(s28,plain,
( ~ spl51_32
| ~ spl51_33 ),
inference(sat_conversion,[],[f573]) ).
cnf(s34,plain,
( ~ spl51_37
| ~ spl51_40 ),
inference(sat_conversion,[],[f607]) ).
cnf(s36,plain,
( ~ spl51_18
| ~ spl51_42 ),
inference(sat_conversion,[],[f617]) ).
cnf(s43,plain,
( ~ spl51_43
| ~ spl51_47 ),
inference(sat_conversion,[],[f644]) ).
cnf(s45,plain,
( ~ spl51_48
| ~ spl51_50 ),
inference(sat_conversion,[],[f658]) ).
cnf(s49,plain,
( ~ spl51_53
| ~ spl51_55 ),
inference(sat_conversion,[],[f682]) ).
cnf(s55,plain,
( ~ spl51_58
| ~ spl51_62 ),
inference(sat_conversion,[],[f716]) ).
cnf(s56,plain,
( ~ spl51_17
| ~ spl51_63 ),
inference(sat_conversion,[],[f721]) ).
cnf(s62,plain,
( ~ spl51_64
| ~ spl51_67 ),
inference(sat_conversion,[],[f743]) ).
cnf(s64,plain,
( ~ spl51_69
| ~ spl51_70 ),
inference(sat_conversion,[],[f757]) ).
cnf(s69,plain,
( ~ spl51_74
| ~ spl51_76 ),
inference(sat_conversion,[],[f786]) ).
cnf(s74,plain,
( ~ spl51_79
| ~ spl51_82 ),
inference(sat_conversion,[],[f815]) ).
cnf(s79,plain,
( ~ spl51_2
| ~ spl51_84 ),
inference(sat_conversion,[],[f828]) ).
cnf(s83,plain,
~ spl51_85,
inference(sat_conversion,[],[f848]) ).
cnf(s87,plain,
( ~ spl51_21
| ~ spl51_89 ),
inference(sat_conversion,[],[f856]) ).
cnf(s91,plain,
( ~ spl51_21
| ~ spl51_90 ),
inference(sat_conversion,[],[f864]) ).
cnf(s94,plain,
( ~ spl51_25
| ~ spl51_91 ),
inference(sat_conversion,[],[f871]) ).
cnf(s98,plain,
( ~ spl51_40
| ~ spl51_92 ),
inference(sat_conversion,[],[f879]) ).
cnf(s101,plain,
( ~ spl51_29
| ~ spl51_93 ),
inference(sat_conversion,[],[f886]) ).
cnf(s105,plain,
( ~ spl51_55
| ~ spl51_94 ),
inference(sat_conversion,[],[f894]) ).
cnf(s108,plain,
( ~ spl51_33
| ~ spl51_95 ),
inference(sat_conversion,[],[f901]) ).
cnf(s112,plain,
( ~ spl51_70
| ~ spl51_96 ),
inference(sat_conversion,[],[f909]) ).
cnf(s117,plain,
( ~ spl51_47
| ~ spl51_97 ),
inference(sat_conversion,[],[f918]) ).
cnf(s121,plain,
( ~ spl51_62
| ~ spl51_98 ),
inference(sat_conversion,[],[f926]) ).
cnf(s127,plain,
( ~ spl51_40
| ~ spl51_99 ),
inference(sat_conversion,[],[f936]) ).
cnf(s131,plain,
( ~ spl51_25
| ~ spl51_100 ),
inference(sat_conversion,[],[f944]) ).
cnf(s132,plain,
( ~ spl51_50
| ~ spl51_101 ),
inference(sat_conversion,[],[f949]) ).
cnf(s136,plain,
( ~ spl51_76
| ~ spl51_102 ),
inference(sat_conversion,[],[f957]) ).
cnf(s142,plain,
( ~ spl51_18
| ~ spl51_103 ),
inference(sat_conversion,[],[f967]) ).
cnf(s146,plain,
( ~ spl51_18
| ~ spl51_104 ),
inference(sat_conversion,[],[f975]) ).
cnf(s150,plain,
( ~ spl51_62
| ~ spl51_105 ),
inference(sat_conversion,[],[f983]) ).
cnf(s154,plain,
( ~ spl51_47
| ~ spl51_106 ),
inference(sat_conversion,[],[f991]) ).
cnf(s156,plain,
( ~ spl51_67
| ~ spl51_107 ),
inference(sat_conversion,[],[f997]) ).
cnf(s160,plain,
( ~ spl51_82
| ~ spl51_108 ),
inference(sat_conversion,[],[f1005]) ).
cnf(s167,plain,
( ~ spl51_55
| ~ spl51_109 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s171,plain,
( ~ spl51_29
| ~ spl51_110 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s173,plain,
( ~ spl51_17
| ~ spl51_111 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s177,plain,
( ~ spl51_17
| ~ spl51_112 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s180,plain,
( ~ spl51_2
| ~ spl51_113 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s184,plain,
( ~ spl51_2
| ~ spl51_114 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s189,plain,
( ~ spl51_82
| ~ spl51_115 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s193,plain,
( ~ spl51_67
| ~ spl51_116 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s198,plain,
( ~ spl51_76
| ~ spl51_117 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s202,plain,
( ~ spl51_50
| ~ spl51_118 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s207,plain,
( spl51_1
| spl51_5
| spl51_10
| spl51_15
| spl51_20
| ~ spl51_21
| spl51_22
| ~ spl51_25
| spl51_27
| ~ spl51_29
| spl51_32
| ~ spl51_33
| spl51_37
| ~ spl51_40
| spl51_42
| spl51_43
| spl51_48
| spl51_53
| ~ spl51_55
| spl51_58
| spl51_63
| spl51_64
| spl51_69
| ~ spl51_70
| spl51_74
| spl51_79
| spl51_84
| spl51_85
| spl51_89
| spl51_90
| spl51_91
| spl51_92
| spl51_93
| spl51_94
| spl51_95
| spl51_96
| spl51_97
| spl51_98
| spl51_99
| spl51_100
| spl51_101
| spl51_102
| spl51_103
| spl51_104
| spl51_105
| spl51_106
| spl51_107
| spl51_108
| spl51_109
| spl51_110
| spl51_111
| spl51_112
| spl51_113
| spl51_114
| spl51_115
| spl51_116
| spl51_117
| spl51_118 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s220,plain,
spl51_2,
inference(sat_conversion,[],[f1105]) ).
cnf(s221,plain,
spl51_82,
inference(sat_conversion,[],[f1106]) ).
cnf(s222,plain,
spl51_76,
inference(sat_conversion,[],[f1107]) ).
cnf(s223,plain,
spl51_70,
inference(sat_conversion,[],[f1108]) ).
cnf(s224,plain,
spl51_67,
inference(sat_conversion,[],[f1109]) ).
cnf(s225,plain,
spl51_17,
inference(sat_conversion,[],[f1110]) ).
cnf(s226,plain,
spl51_62,
inference(sat_conversion,[],[f1111]) ).
cnf(s227,plain,
spl51_55,
inference(sat_conversion,[],[f1112]) ).
cnf(s228,plain,
spl51_50,
inference(sat_conversion,[],[f1113]) ).
cnf(s229,plain,
spl51_47,
inference(sat_conversion,[],[f1114]) ).
cnf(s230,plain,
spl51_18,
inference(sat_conversion,[],[f1115]) ).
cnf(s231,plain,
spl51_40,
inference(sat_conversion,[],[f1116]) ).
cnf(s232,plain,
spl51_33,
inference(sat_conversion,[],[f1117]) ).
cnf(s233,plain,
spl51_29,
inference(sat_conversion,[],[f1118]) ).
cnf(s234,plain,
spl51_25,
inference(sat_conversion,[],[f1119]) ).
cnf(s235,plain,
spl51_21,
inference(sat_conversion,[],[f1120]) ).
cnf(s236,plain,
~ spl51_86,
inference(sat_conversion,[],[f1121]) ).
cnf(s237,plain,
~ spl51_87,
inference(sat_conversion,[],[f1122]) ).
cnf(s238,plain,
~ spl51_88,
inference(sat_conversion,[],[f1123]) ).
cnf(s239,plain,
( ~ spl51_2
| ~ spl51_6
| spl51_88 ),
inference(sat_conversion,[],[f1126]) ).
cnf(s245,plain,
( ~ spl51_19
| ~ spl51_21
| spl51_86 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s246,plain,
( ~ spl51_14
| ~ spl51_21
| spl51_87 ),
inference(sat_conversion,[],[f1154]) ).
cnf(s250,plain,
( ~ spl51_3
| ~ spl51_17
| spl51_86 ),
inference(sat_conversion,[],[f1169]) ).
cnf(s251,plain,
~ spl51_14,
inference(rat,[],[s246,s237,s235]) ).
cnf(s252,plain,
~ spl51_19,
inference(rat,[],[s245,s236,s235]) ).
cnf(s254,plain,
~ spl51_3,
inference(rat,[],[s250,s236,s225]) ).
cnf(s258,plain,
~ spl51_6,
inference(rat,[],[s239,s238,s220]) ).
cnf(s265,plain,
( spl51_1
| spl51_5
| spl51_10
| spl51_15
| spl51_20
| spl51_22
| spl51_27
| spl51_32
| spl51_37
| spl51_42
| spl51_43
| spl51_48
| spl51_53
| spl51_58
| spl51_63
| spl51_64
| spl51_69
| spl51_74
| spl51_79
| spl51_84
| spl51_85
| spl51_89
| spl51_90
| spl51_91
| spl51_92
| spl51_93
| spl51_94
| spl51_95
| spl51_96
| spl51_97
| spl51_98
| spl51_99
| spl51_100
| spl51_101
| spl51_102
| spl51_103
| spl51_104
| spl51_105
| spl51_106
| spl51_107
| spl51_108
| spl51_109
| spl51_110
| spl51_111
| spl51_112
| spl51_113
| spl51_114
| spl51_115
| spl51_116
| spl51_117
| spl51_118 ),
inference(rat,[],[s207,s223,s227,s231,s232,s233,s234,s235]) ).
cnf(s268,plain,
~ spl51_118,
inference(rat,[],[s202,s228]) ).
cnf(s269,plain,
~ spl51_117,
inference(rat,[],[s198,s222]) ).
cnf(s270,plain,
~ spl51_116,
inference(rat,[],[s193,s224]) ).
cnf(s271,plain,
~ spl51_115,
inference(rat,[],[s189,s221]) ).
cnf(s272,plain,
~ spl51_114,
inference(rat,[],[s184,s220]) ).
cnf(s273,plain,
~ spl51_113,
inference(rat,[],[s180,s220]) ).
cnf(s274,plain,
~ spl51_112,
inference(rat,[],[s177,s225]) ).
cnf(s275,plain,
~ spl51_111,
inference(rat,[],[s173,s225]) ).
cnf(s276,plain,
~ spl51_110,
inference(rat,[],[s171,s233]) ).
cnf(s277,plain,
~ spl51_109,
inference(rat,[],[s167,s227]) ).
cnf(s278,plain,
~ spl51_108,
inference(rat,[],[s160,s221]) ).
cnf(s279,plain,
~ spl51_107,
inference(rat,[],[s156,s224]) ).
cnf(s280,plain,
~ spl51_106,
inference(rat,[],[s154,s229]) ).
cnf(s281,plain,
~ spl51_105,
inference(rat,[],[s150,s226]) ).
cnf(s282,plain,
~ spl51_104,
inference(rat,[],[s146,s230]) ).
cnf(s283,plain,
~ spl51_103,
inference(rat,[],[s142,s230]) ).
cnf(s284,plain,
~ spl51_102,
inference(rat,[],[s136,s222]) ).
cnf(s285,plain,
~ spl51_101,
inference(rat,[],[s132,s228]) ).
cnf(s286,plain,
~ spl51_100,
inference(rat,[],[s131,s234]) ).
cnf(s287,plain,
~ spl51_99,
inference(rat,[],[s127,s231]) ).
cnf(s288,plain,
~ spl51_98,
inference(rat,[],[s121,s226]) ).
cnf(s289,plain,
~ spl51_97,
inference(rat,[],[s117,s229]) ).
cnf(s290,plain,
~ spl51_96,
inference(rat,[],[s112,s223]) ).
cnf(s291,plain,
~ spl51_95,
inference(rat,[],[s108,s232]) ).
cnf(s292,plain,
~ spl51_94,
inference(rat,[],[s105,s227]) ).
cnf(s293,plain,
~ spl51_93,
inference(rat,[],[s101,s233]) ).
cnf(s294,plain,
~ spl51_92,
inference(rat,[],[s98,s231]) ).
cnf(s295,plain,
~ spl51_91,
inference(rat,[],[s94,s234]) ).
cnf(s296,plain,
~ spl51_90,
inference(rat,[],[s91,s235]) ).
cnf(s297,plain,
~ spl51_89,
inference(rat,[],[s87,s235]) ).
cnf(s298,plain,
~ spl51_84,
inference(rat,[],[s79,s220]) ).
cnf(s299,plain,
~ spl51_79,
inference(rat,[],[s74,s221]) ).
cnf(s300,plain,
~ spl51_74,
inference(rat,[],[s69,s222]) ).
cnf(s301,plain,
~ spl51_69,
inference(rat,[],[s64,s223]) ).
cnf(s302,plain,
~ spl51_64,
inference(rat,[],[s62,s224]) ).
cnf(s303,plain,
~ spl51_63,
inference(rat,[],[s56,s225]) ).
cnf(s304,plain,
~ spl51_58,
inference(rat,[],[s55,s226]) ).
cnf(s305,plain,
~ spl51_53,
inference(rat,[],[s49,s227]) ).
cnf(s306,plain,
~ spl51_48,
inference(rat,[],[s45,s228]) ).
cnf(s307,plain,
~ spl51_43,
inference(rat,[],[s43,s229]) ).
cnf(s308,plain,
~ spl51_42,
inference(rat,[],[s36,s230]) ).
cnf(s309,plain,
~ spl51_37,
inference(rat,[],[s34,s231]) ).
cnf(s310,plain,
~ spl51_32,
inference(rat,[],[s28,s232]) ).
cnf(s311,plain,
~ spl51_27,
inference(rat,[],[s25,s233]) ).
cnf(s312,plain,
~ spl51_22,
inference(rat,[],[s22,s234]) ).
cnf(s313,plain,
~ spl51_20,
inference(rat,[],[s19,s235]) ).
cnf(s314,plain,
~ spl51_15,
inference(rat,[],[s15,s252]) ).
cnf(s315,plain,
~ spl51_10,
inference(rat,[],[s11,s251]) ).
cnf(s316,plain,
~ spl51_5,
inference(rat,[],[s4,s258]) ).
cnf(s317,plain,
spl51_1,
inference(rat,[],[s265,s268,s269,s270,s271,s272,s273,s274,s275,s276,s277,s278,s279,s280,s281,s282,s283,s284,s285,s286,s287,s288,s289,s290,s291,s292,s293,s294,s295,s296,s297,s83,s298,s299,s300,s301,s302,s303,s304,s305,s306,s307,s308,s309,s310,s311,s312,s313,s314,s315,s316]) ).
cnf(s319,plain,
$false,
inference(rat,[],[s2,s254,s317]) ).
fof(f1170,plain,
$false,
inference(avatar_sat_refutation,[],[s319]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG044+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.06/0.18 % Computer : n014.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 19:20:01 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.06/0.21 Running first-order model finding
% 0.06/0.21 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.18/0.27 % (2089272)Will run a generic schedule for satisfiability detection.
% 0.18/0.27 % (2089281)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2413548037:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.27 % (2089278)% WARNING: option uhcvi not known.
% 0.18/0.27 % (2089279)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2643865557:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.27 % (2089277)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3273039176_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.27 % (2089278)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1771129608:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.27 % (2089280)dis+10_1_sil=32000:sp=arity:random_seed=154448305:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.27 % (2089282)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2480733504:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.27 % (2089283)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1979960561:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.27 % (2089281) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2089272-2089281"...
% 0.18/0.27 % (2089280) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2089272-2089280"...
% 0.18/0.27 % (2089282) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2089272-2089282"...
% 0.18/0.27 % (2089283) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2089272-2089283"...
% 0.18/0.27 % (2089281)...printing done.
% 0.18/0.27 % (2089278) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2089272-2089278"...
% 0.18/0.27 % (2089281)Refutation found. Thanks to Tanya!
% 0.18/0.27 % SZS status Theorem for theBenchmark
% 0.18/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.27 % (2089281)------------------------------
% 0.18/0.27 % (2089281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.27 % (2089281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.27 % (2089281)CaDiCaL version: 2.1.3
% 0.18/0.27 % (2089281)Termination reason: Refutation
% 0.18/0.27 % (2089281)Time elapsed: 0.018 s
% 0.18/0.27 % (2089281)Peak memory usage: 13 MB
% 0.18/0.27 % (2089281)Instructions burned: 73 (million)
% 0.18/0.27 % (2089272)Success in time 0.05 s
% 0.18/0.27 % Vampire exiting
%------------------------------------------------------------------------------