%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG024+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:07 AM UTC 2026
% Result : Unsatisfiable 0.42s 0.30s
% Output : Refutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 117
% Syntax : Number of formulae : 955 ( 81 unt; 96 def)
% Number of atoms : 2437 ( 823 equ)
% Maximal formula atoms : 64 ( 2 avg)
% Number of connectives : 2945 (1463 ~;1253 |; 133 &)
% ( 96 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 98 ( 96 usr; 97 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( 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 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f3,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
& ( unit = e0
| unit = e1
| unit = e2
| unit = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( op(e0,inv(e0)) = unit
& op(inv(e0),e0) = unit
& op(e1,inv(e1)) = unit
& op(inv(e1),e1) = unit
& op(e2,inv(e2)) = unit
& op(inv(e2),e2) = unit
& op(e3,inv(e3)) = unit
& op(inv(e3),e3) = unit
& ( inv(e0) = e0
| inv(e0) = e1
| inv(e0) = e2
| inv(e0) = e3 )
& ( inv(e1) = e0
| inv(e1) = e1
| inv(e1) = e2
| inv(e1) = e3 )
& ( inv(e2) = e0
| inv(e2) = e1
| inv(e2) = e2
| inv(e2) = e3 )
& ( inv(e3) = e0
| inv(e3) = e1
| inv(e3) = e2
| inv(e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
inv(unit) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
( inv(inv(e0)) = e0
& inv(inv(e1)) = e1
& inv(inv(e2)) = e2
& inv(inv(e3)) = e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f8,axiom,
( inv(e0) != inv(e1)
& inv(e0) != inv(e2)
& inv(e0) != inv(e3)
& inv(e1) != inv(e2)
& inv(e1) != inv(e3)
& inv(e2) != inv(e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f9,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( ( 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 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e0 = op(op(e2,op(e2,e2)),e2)
& e1 = op(e2,op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f16,axiom,
~ ( e0 = op(op(e1,op(e1,e1)),e1)
& e3 = op(e1,op(e1,e1))
& e2 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e0 = op(op(e2,op(e2,e2)),e2)
& e3 = op(e2,op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
~ ( e1 = op(op(e2,op(e2,e2)),e2)
& e0 = op(e2,op(e2,e2))
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f21,axiom,
~ ( e1 = op(op(e3,op(e3,e3)),e3)
& e2 = op(e3,op(e3,e3))
& e0 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
fof(f22,axiom,
~ ( e1 = op(op(e0,op(e0,e0)),e0)
& e3 = op(e0,op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f25,axiom,
~ ( e2 = op(op(e3,op(e3,e3)),e3)
& e0 = op(e3,op(e3,e3))
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e2 = op(op(e0,op(e0,e0)),e0)
& e1 = op(e0,op(e0,e0))
& e3 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f29,axiom,
~ ( e2 = op(op(e1,op(e1,e1)),e1)
& e3 = op(e1,op(e1,e1))
& e0 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f31,axiom,
~ ( e3 = op(op(e2,op(e2,e2)),e2)
& e0 = op(e2,op(e2,e2))
& e1 = op(e2,e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax31) ).
fof(f32,axiom,
~ ( e3 = op(op(e0,op(e0,e0)),e0)
& e1 = op(e0,op(e0,e0))
& e2 = op(e0,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax32) ).
fof(f35,axiom,
~ ( e3 = op(op(e1,op(e1,e1)),e1)
& e2 = op(e1,op(e1,e1))
& e0 = op(e1,e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax35) ).
fof(f37,plain,
( ( e0 != op(e0,e0)
| e0 != op(e1,e1)
| e0 != op(e2,e2)
| e0 != op(e3,e3) )
& ( op(e0,e0) != e1
| e1 != op(e1,e1)
| e1 != op(e2,e2)
| e1 != op(e3,e3) )
& ( op(e0,e0) != e2
| e2 != op(e1,e1)
| e2 != op(e2,e2)
| e2 != op(e3,e3) )
& ( op(e0,e0) != e3
| e3 != op(e1,e1)
| e3 != op(e2,e2)
| e3 != op(e3,e3) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f38,plain,
( e0 != op(op(e2,op(e2,e2)),e2)
| e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f12]) ).
fof(f42,plain,
( e0 != op(op(e1,op(e1,e1)),e1)
| e3 != op(e1,op(e1,e1))
| e2 != op(e1,e1) ),
inference(ennf_transformation,[],[f16]) ).
fof(f43,plain,
( e0 != op(op(e2,op(e2,e2)),e2)
| e3 != op(e2,op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f17]) ).
fof(f44,plain,
( e1 != op(op(e2,op(e2,e2)),e2)
| e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2) ),
inference(ennf_transformation,[],[f18]) ).
fof(f47,plain,
( e1 != op(op(e3,op(e3,e3)),e3)
| e2 != op(e3,op(e3,e3))
| e0 != op(e3,e3) ),
inference(ennf_transformation,[],[f21]) ).
fof(f48,plain,
( e1 != op(op(e0,op(e0,e0)),e0)
| e3 != op(e0,op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f22]) ).
fof(f51,plain,
( e2 != op(op(e3,op(e3,e3)),e3)
| e0 != op(e3,op(e3,e3))
| e1 != op(e3,e3) ),
inference(ennf_transformation,[],[f25]) ).
fof(f52,plain,
( e2 != op(op(e0,op(e0,e0)),e0)
| e1 != op(e0,op(e0,e0))
| op(e0,e0) != e3 ),
inference(ennf_transformation,[],[f26]) ).
fof(f55,plain,
( e2 != op(op(e1,op(e1,e1)),e1)
| e3 != op(e1,op(e1,e1))
| e0 != op(e1,e1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f57,plain,
( e3 != op(op(e2,op(e2,e2)),e2)
| e0 != op(e2,op(e2,e2))
| e1 != op(e2,e2) ),
inference(ennf_transformation,[],[f31]) ).
fof(f58,plain,
( e3 != op(op(e0,op(e0,e0)),e0)
| e1 != op(e0,op(e0,e0))
| op(e0,e0) != e2 ),
inference(ennf_transformation,[],[f32]) ).
fof(f61,plain,
( e3 != op(op(e1,op(e1,e1)),e1)
| e2 != op(e1,op(e1,e1))
| e0 != op(e1,e1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f62,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e3 = op(e0,e1)
| e2 = op(e0,e1)
| e1 = op(e0,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e3 = op(e0,e2)
| e2 = op(e0,e2)
| e1 = op(e0,e2)
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
( e3 = op(e0,e3)
| e2 = op(e0,e3)
| e1 = op(e0,e3)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e3 = op(e1,e1)
| e2 = op(e1,e1)
| e1 = op(e1,e1)
| e0 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e3 = op(e1,e2)
| e2 = op(e1,e2)
| e1 = op(e1,e2)
| e0 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e3 = op(e2,e0)
| e2 = op(e2,e0)
| e1 = op(e2,e0)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
( e3 = op(e2,e1)
| e2 = op(e2,e1)
| e1 = op(e2,e1)
| e0 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
( e3 = op(e2,e2)
| e2 = op(e2,e2)
| e1 = op(e2,e2)
| e0 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f73,plain,
( e3 = op(e2,e3)
| e2 = op(e2,e3)
| e1 = op(e2,e3)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f74,plain,
( e3 = op(e3,e0)
| e2 = op(e3,e0)
| e1 = op(e3,e0)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f75,plain,
( e3 = op(e3,e1)
| e2 = op(e3,e1)
| e1 = op(e3,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f76,plain,
( e3 = op(e3,e2)
| e2 = op(e3,e2)
| e1 = op(e3,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f77,plain,
( e3 = op(e3,e3)
| e2 = op(e3,e3)
| e1 = op(e3,e3)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f142,plain,
( e3 = unit
| e2 = unit
| e1 = unit
| e0 = unit ),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
e3 = op(e3,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
e3 = op(unit,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
e2 = op(e2,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
e2 = op(unit,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
e1 = op(e1,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
e1 = op(unit,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
e0 = op(e0,unit),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e0 = op(unit,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
( e3 = inv(e0)
| e2 = inv(e0)
| e1 = inv(e0)
| e0 = inv(e0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
( e3 = inv(e3)
| e2 = inv(e3)
| e1 = inv(e3)
| e0 = inv(e3) ),
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
unit = op(inv(e3),e3),
inference(cnf_transformation,[],[f4]) ).
fof(f157,plain,
unit = op(inv(e2),e2),
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
unit = op(inv(e0),e0),
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
unit = op(e0,inv(e0)),
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
unit = inv(unit),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
e3 = inv(inv(e3)),
inference(cnf_transformation,[],[f6]) ).
fof(f167,plain,
e0 = inv(inv(e0)),
inference(cnf_transformation,[],[f6]) ).
fof(f181,plain,
inv(e1) != inv(e3),
inference(cnf_transformation,[],[f8]) ).
fof(f185,plain,
inv(e0) != inv(e1),
inference(cnf_transformation,[],[f8]) ).
fof(f187,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f188,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f189,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f190,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f191,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f192,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f193,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f194,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f195,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f196,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f197,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f198,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f200,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f201,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f202,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f203,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f204,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f205,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f206,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f207,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f208,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f209,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f210,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f211,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f212,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f213,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f214,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f215,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f9]) ).
fof(f216,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f217,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f218,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f219,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f220,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f221,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f9]) ).
fof(f222,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f223,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f224,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f225,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f226,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f227,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f9]) ).
fof(f228,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f9]) ).
fof(f229,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f9]) ).
fof(f230,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f9]) ).
fof(f231,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f9]) ).
fof(f232,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f9]) ).
fof(f233,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f9]) ).
fof(f237,plain,
e0 != e3,
inference(cnf_transformation,[],[f10]) ).
fof(f239,plain,
e0 != e1,
inference(cnf_transformation,[],[f10]) ).
fof(f240,plain,
( e0 != op(e3,e3)
| e0 != op(e2,e2)
| e0 != op(e1,e1)
| e0 != op(e0,e0) ),
inference(cnf_transformation,[],[f37]) ).
fof(f241,plain,
( e1 != op(e3,e3)
| e1 != op(e2,e2)
| e1 != op(e1,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f37]) ).
fof(f242,plain,
( e2 != op(e3,e3)
| e2 != op(e2,e2)
| e2 != op(e1,e1)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f37]) ).
fof(f243,plain,
( e3 != op(e3,e3)
| e3 != op(e2,e2)
| e3 != op(e1,e1)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f37]) ).
fof(f244,plain,
( e3 != op(e2,e2)
| e1 != op(e2,op(e2,e2))
| e0 != op(op(e2,op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f38]) ).
fof(f248,plain,
( e2 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f249,plain,
( e1 != op(e2,e2)
| e3 != op(e2,op(e2,e2))
| e0 != op(op(e2,op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f43]) ).
fof(f250,plain,
( e3 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e1 != op(op(e2,op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f44]) ).
fof(f253,plain,
( e0 != op(e3,e3)
| e2 != op(e3,op(e3,e3))
| e1 != op(op(e3,op(e3,e3)),e3) ),
inference(cnf_transformation,[],[f47]) ).
fof(f254,plain,
( op(e0,e0) != e2
| e3 != op(e0,op(e0,e0))
| e1 != op(op(e0,op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f48]) ).
fof(f257,plain,
( e1 != op(e3,e3)
| e0 != op(e3,op(e3,e3))
| e2 != op(op(e3,op(e3,e3)),e3) ),
inference(cnf_transformation,[],[f51]) ).
fof(f258,plain,
( op(e0,e0) != e3
| e1 != op(e0,op(e0,e0))
| e2 != op(op(e0,op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f52]) ).
fof(f261,plain,
( e0 != op(e1,e1)
| e3 != op(e1,op(e1,e1))
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f55]) ).
fof(f263,plain,
( e1 != op(e2,e2)
| e0 != op(e2,op(e2,e2))
| e3 != op(op(e2,op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f57]) ).
fof(f264,plain,
( op(e0,e0) != e2
| e1 != op(e0,op(e0,e0))
| e3 != op(op(e0,op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f58]) ).
fof(f267,plain,
( e0 != op(e1,e1)
| e2 != op(e1,op(e1,e1))
| e3 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f269,definition,
( spl0_1
<=> e3 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f271,plain,
( e3 != op(op(e1,op(e1,e1)),e1)
| spl0_1 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f273,definition,
( spl0_2
<=> e2 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f275,plain,
( e2 != op(e1,op(e1,e1))
| spl0_2 ),
inference(avatar_component_clause,[],[f273]) ).
fof(f277,definition,
( spl0_3
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f278,plain,
( e0 = op(e1,e1)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f277]) ).
fof(f280,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f267,f277,f273,f269]) ).
fof(f282,definition,
( spl0_4
<=> e3 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f283,plain,
( e3 = op(op(e0,op(e0,e0)),e0)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f284,plain,
( e3 != op(op(e0,op(e0,e0)),e0)
| spl0_4 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f290,definition,
( spl0_6
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f291,plain,
( op(e0,e0) = e1
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f292,plain,
( op(e0,e0) != e1
| spl0_6 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f295,definition,
( spl0_7
<=> e3 = op(op(e2,op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f297,plain,
( e3 != op(op(e2,op(e2,e2)),e2)
| spl0_7 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl0_8
<=> e1 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f300,plain,
( e1 = op(e2,op(e2,e2))
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f301,plain,
( e1 != op(e2,op(e2,e2))
| spl0_8 ),
inference(avatar_component_clause,[],[f299]) ).
fof(f303,definition,
( spl0_9
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f304,plain,
( e0 = op(e2,e2)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f308,definition,
( spl0_10
<=> e1 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f309,plain,
( e1 = op(e0,op(e0,e0))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( e1 != op(e0,op(e0,e0))
| spl0_10 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f312,definition,
( spl0_11
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f313,plain,
( op(e0,e0) = e2
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f312]) ).
fof(f315,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f264,f312,f308,f282]) ).
fof(f317,definition,
( spl0_12
<=> e0 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f318,plain,
( e0 = op(e2,op(e2,e2))
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f319,plain,
( e0 != op(e2,op(e2,e2))
| spl0_12 ),
inference(avatar_component_clause,[],[f317]) ).
fof(f321,definition,
( spl0_13
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f322,plain,
( e1 = op(e2,e2)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f324,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f263,f321,f317,f295]) ).
fof(f330,definition,
( spl0_15
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f331,plain,
( e2 = op(e1,e1)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f335,definition,
( spl0_16
<=> e2 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f337,plain,
( e2 != op(op(e1,op(e1,e1)),e1)
| spl0_16 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl0_17
<=> e3 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f341,plain,
( e3 != op(e1,op(e1,e1))
| spl0_17 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
( ~ spl0_16
| ~ spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f261,f277,f339,f335]) ).
fof(f344,definition,
( spl0_18
<=> e2 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f346,plain,
( e2 != op(op(e0,op(e0,e0)),e0)
| spl0_18 ),
inference(avatar_component_clause,[],[f344]) ).
fof(f348,definition,
( spl0_19
<=> e3 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f350,plain,
( e3 != op(e0,op(e0,e0))
| spl0_19 ),
inference(avatar_component_clause,[],[f348]) ).
fof(f353,definition,
( spl0_20
<=> e2 = op(op(e3,op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f355,plain,
( e2 != op(op(e3,op(e3,e3)),e3)
| spl0_20 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f361,definition,
( spl0_22
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f362,plain,
( e0 = op(e3,e3)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f366,definition,
( spl0_23
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f367,plain,
( op(e0,e0) = e3
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f369,plain,
( ~ spl0_18
| ~ spl0_10
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f258,f366,f308,f344]) ).
fof(f371,definition,
( spl0_24
<=> e0 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f373,plain,
( e0 != op(e3,op(e3,e3))
| spl0_24 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f375,definition,
( spl0_25
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f376,plain,
( e1 = op(e3,e3)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,plain,
( ~ spl0_20
| ~ spl0_24
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f257,f375,f371,f353]) ).
fof(f380,definition,
( spl0_26
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f381,plain,
( e3 = op(e1,e1)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f385,definition,
( spl0_27
<=> e1 = op(op(e2,op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f387,plain,
( e1 != op(op(e2,op(e2,e2)),e2)
| spl0_27 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f389,definition,
( spl0_28
<=> e3 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f391,plain,
( e3 != op(e2,op(e2,e2))
| spl0_28 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f394,definition,
( spl0_29
<=> e1 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f396,plain,
( e1 != op(op(e0,op(e0,e0)),e0)
| spl0_29 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
( ~ spl0_29
| ~ spl0_19
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f254,f312,f348,f394]) ).
fof(f399,definition,
( spl0_30
<=> e1 = op(op(e3,op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f401,plain,
( e1 != op(op(e3,op(e3,e3)),e3)
| spl0_30 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f403,definition,
( spl0_31
<=> e2 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f405,plain,
( e2 != op(e3,op(e3,e3))
| spl0_31 ),
inference(avatar_component_clause,[],[f403]) ).
fof(f406,plain,
( ~ spl0_30
| ~ spl0_31
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f253,f361,f403,f399]) ).
fof(f409,definition,
( spl0_32
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f414,definition,
( spl0_33
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f415,plain,
( e3 = op(e2,e2)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f417,plain,
( ~ spl0_27
| ~ spl0_12
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f250,f414,f317,f385]) ).
fof(f419,definition,
( spl0_34
<=> e0 = op(op(e2,op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f421,plain,
( e0 != op(op(e2,op(e2,e2)),e2)
| spl0_34 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( ~ spl0_34
| ~ spl0_28
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f249,f321,f389,f419]) ).
fof(f424,definition,
( spl0_35
<=> e0 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f426,plain,
( e0 != op(op(e1,op(e1,e1)),e1)
| spl0_35 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f427,plain,
( ~ spl0_35
| ~ spl0_17
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f248,f330,f339,f424]) ).
fof(f435,plain,
( ~ spl0_34
| ~ spl0_8
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f244,f414,f299,f419]) ).
fof(f437,definition,
( spl0_37
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f438,plain,
( e0 = op(e0,e0)
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f440,plain,
( ~ spl0_37
| ~ spl0_3
| ~ spl0_9
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f240,f361,f303,f277,f437]) ).
fof(f442,definition,
( spl0_38
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f443,plain,
( e1 = op(e1,e1)
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f442]) ).
fof(f445,plain,
( ~ spl0_6
| ~ spl0_38
| ~ spl0_13
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f241,f375,f321,f442,f290]) ).
fof(f447,definition,
( spl0_39
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f450,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_39
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f242,f409,f447,f330,f312]) ).
fof(f452,definition,
( spl0_40
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f453,plain,
( e3 = op(e3,e3)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( ~ spl0_23
| ~ spl0_26
| ~ spl0_33
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f243,f452,f414,f380,f366]) ).
fof(f461,definition,
( spl0_42
<=> e1 = inv(e0) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f466,definition,
( spl0_43
<=> e0 = inv(e2) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f468,plain,
( e0 = inv(e2)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f470,definition,
( spl0_44
<=> e2 = inv(e0) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f471,plain,
( e2 = inv(e0)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f475,definition,
( spl0_45
<=> e0 = inv(e3) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f477,plain,
( e0 = inv(e3)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f479,definition,
( spl0_46
<=> e3 = inv(e0) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f480,plain,
( e3 = inv(e0)
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f494,definition,
( spl0_49
<=> e1 = inv(e3) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f505,definition,
( spl0_51
<=> e2 = inv(e3) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f507,plain,
( e2 = inv(e3)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f517,definition,
( spl0_53
<=> e0 = inv(e0) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f519,plain,
( e0 = inv(e0)
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f520,plain,
( spl0_53
| spl0_42
| spl0_44
| spl0_46 ),
inference(avatar_split_clause,[],[f151,f479,f470,f461,f517]) ).
fof(f522,definition,
( spl0_54
<=> e1 = inv(e1) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f524,plain,
( e1 = inv(e1)
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f532,definition,
( spl0_56
<=> e3 = inv(e3) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f534,plain,
( e3 = inv(e3)
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f535,plain,
( spl0_45
| spl0_49
| spl0_51
| spl0_56 ),
inference(avatar_split_clause,[],[f154,f532,f505,f494,f475]) ).
fof(f537,definition,
( spl0_57
<=> e0 = unit ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f539,plain,
( e0 = unit
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f541,definition,
( spl0_58
<=> e1 = unit ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f543,plain,
( e1 = unit
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f545,definition,
( spl0_59
<=> e2 = unit ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f547,plain,
( e2 = unit
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f549,definition,
( spl0_60
<=> e3 = unit ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f551,plain,
( e3 = unit
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f552,plain,
( spl0_57
| spl0_58
| spl0_59
| spl0_60 ),
inference(avatar_split_clause,[],[f142,f549,f545,f541,f537]) ).
fof(f553,plain,
( spl0_37
| spl0_6
| spl0_11
| spl0_23 ),
inference(avatar_split_clause,[],[f62,f366,f312,f290,f437]) ).
fof(f555,definition,
( spl0_61
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f557,plain,
( e0 = op(e0,e1)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f559,definition,
( spl0_62
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f561,plain,
( e1 = op(e0,e1)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl0_63
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f565,plain,
( e2 = op(e0,e1)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl0_64
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f569,plain,
( e3 = op(e0,e1)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f570,plain,
( spl0_61
| spl0_62
| spl0_63
| spl0_64 ),
inference(avatar_split_clause,[],[f63,f567,f563,f559,f555]) ).
fof(f572,definition,
( spl0_65
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f576,definition,
( spl0_66
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f578,plain,
( e1 = op(e0,e2)
| ~ spl0_66 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f580,definition,
( spl0_67
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f582,plain,
( e2 = op(e0,e2)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f584,definition,
( spl0_68
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f586,plain,
( e3 = op(e0,e2)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,plain,
( spl0_65
| spl0_66
| spl0_67
| spl0_68 ),
inference(avatar_split_clause,[],[f64,f584,f580,f576,f572]) ).
fof(f589,definition,
( spl0_69
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f591,plain,
( e0 = op(e0,e3)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f593,definition,
( spl0_70
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f595,plain,
( e1 = op(e0,e3)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f597,definition,
( spl0_71
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f599,plain,
( e2 = op(e0,e3)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f601,definition,
( spl0_72
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f604,plain,
( spl0_69
| spl0_70
| spl0_71
| spl0_72 ),
inference(avatar_split_clause,[],[f65,f601,f597,f593,f589]) ).
fof(f606,definition,
( spl0_73
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f608,plain,
( e0 = op(e1,e0)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f610,definition,
( spl0_74
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f614,definition,
( spl0_75
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f616,plain,
( e2 = op(e1,e0)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f618,definition,
( spl0_76
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f620,plain,
( e3 = op(e1,e0)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f621,plain,
( spl0_73
| spl0_74
| spl0_75
| spl0_76 ),
inference(avatar_split_clause,[],[f66,f618,f614,f610,f606]) ).
fof(f622,plain,
( spl0_3
| spl0_38
| spl0_15
| spl0_26 ),
inference(avatar_split_clause,[],[f67,f380,f330,f442,f277]) ).
fof(f624,definition,
( spl0_77
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f626,plain,
( e0 = op(e1,e2)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f628,definition,
( spl0_78
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f630,plain,
( e1 = op(e1,e2)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f632,definition,
( spl0_79
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f634,plain,
( e2 = op(e1,e2)
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f636,definition,
( spl0_80
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f638,plain,
( e3 = op(e1,e2)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f639,plain,
( spl0_77
| spl0_78
| spl0_79
| spl0_80 ),
inference(avatar_split_clause,[],[f68,f636,f632,f628,f624]) ).
fof(f645,definition,
( spl0_82
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f647,plain,
( e1 = op(e1,e3)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f653,definition,
( spl0_84
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f655,plain,
( e3 = op(e1,e3)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f658,definition,
( spl0_85
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f662,definition,
( spl0_86
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f664,plain,
( e1 = op(e2,e0)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f666,definition,
( spl0_87
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f670,definition,
( spl0_88
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f672,plain,
( e3 = op(e2,e0)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f673,plain,
( spl0_85
| spl0_86
| spl0_87
| spl0_88 ),
inference(avatar_split_clause,[],[f70,f670,f666,f662,f658]) ).
fof(f675,definition,
( spl0_89
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f677,plain,
( e0 = op(e2,e1)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f679,definition,
( spl0_90
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f681,plain,
( e1 = op(e2,e1)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f683,definition,
( spl0_91
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f685,plain,
( e2 = op(e2,e1)
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,definition,
( spl0_92
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f689,plain,
( e3 = op(e2,e1)
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( spl0_89
| spl0_90
| spl0_91
| spl0_92 ),
inference(avatar_split_clause,[],[f71,f687,f683,f679,f675]) ).
fof(f691,plain,
( spl0_9
| spl0_13
| spl0_39
| spl0_33 ),
inference(avatar_split_clause,[],[f72,f414,f447,f321,f303]) ).
fof(f693,definition,
( spl0_93
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f695,plain,
( e0 = op(e2,e3)
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f697,definition,
( spl0_94
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f699,plain,
( e1 = op(e2,e3)
| ~ spl0_94 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f701,definition,
( spl0_95
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f703,plain,
( e2 = op(e2,e3)
| ~ spl0_95 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f705,definition,
( spl0_96
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f707,plain,
( e3 = op(e2,e3)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f708,plain,
( spl0_93
| spl0_94
| spl0_95
| spl0_96 ),
inference(avatar_split_clause,[],[f73,f705,f701,f697,f693]) ).
fof(f710,definition,
( spl0_97
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f712,plain,
( e0 = op(e3,e0)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f710]) ).
fof(f714,definition,
( spl0_98
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f718,definition,
( spl0_99
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f720,plain,
( e2 = op(e3,e0)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f722,definition,
( spl0_100
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f724,plain,
( e3 = op(e3,e0)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f725,plain,
( spl0_97
| spl0_98
| spl0_99
| spl0_100 ),
inference(avatar_split_clause,[],[f74,f722,f718,f714,f710]) ).
fof(f727,definition,
( spl0_101
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f729,plain,
( e0 = op(e3,e1)
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f731,definition,
( spl0_102
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f733,plain,
( e1 = op(e3,e1)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f735,definition,
( spl0_103
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f737,plain,
( e2 = op(e3,e1)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f739,definition,
( spl0_104
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f741,plain,
( e3 = op(e3,e1)
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f739]) ).
fof(f742,plain,
( spl0_101
| spl0_102
| spl0_103
| spl0_104 ),
inference(avatar_split_clause,[],[f75,f739,f735,f731,f727]) ).
fof(f744,definition,
( spl0_105
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f746,plain,
( e0 = op(e3,e2)
| ~ spl0_105 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f748,definition,
( spl0_106
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f750,plain,
( e1 = op(e3,e2)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f752,definition,
( spl0_107
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f754,plain,
( e2 = op(e3,e2)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f756,definition,
( spl0_108
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f759,plain,
( spl0_105
| spl0_106
| spl0_107
| spl0_108 ),
inference(avatar_split_clause,[],[f76,f756,f752,f748,f744]) ).
fof(f760,plain,
( spl0_22
| spl0_25
| spl0_32
| spl0_40 ),
inference(avatar_split_clause,[],[f77,f452,f409,f375,f361]) ).
fof(f799,plain,
( e3 = op(e3,e3)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f143,f551]) ).
fof(f800,plain,
( spl0_40
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f799,f549,f452]) ).
fof(f802,plain,
( e2 = op(e2,e3)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f145,f551]) ).
fof(f803,plain,
( spl0_95
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f802,f549,f701]) ).
fof(f807,plain,
( e1 = inv(e1)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f163,f543]) ).
fof(f808,plain,
( e3 = op(e3,e1)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f143,f543]) ).
fof(f809,plain,
( spl0_104
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f808,f541,f739]) ).
fof(f817,plain,
( e2 = op(e3,e2)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f146,f551]) ).
fof(f818,plain,
( spl0_107
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f817,f549,f752]) ).
fof(f819,plain,
( e1 = op(e1,e3)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f147,f551]) ).
fof(f820,plain,
( spl0_82
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f819,f549,f645]) ).
fof(f826,plain,
( e3 = op(e1,e3)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f144,f543]) ).
fof(f827,plain,
( spl0_84
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f826,f541,f653]) ).
fof(f828,plain,
( e2 = op(e2,e1)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f145,f543]) ).
fof(f829,plain,
( spl0_91
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f828,f541,f683]) ).
fof(f830,plain,
( e2 = op(e1,e2)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f146,f543]) ).
fof(f831,plain,
( spl0_79
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f830,f541,f632]) ).
fof(f832,plain,
( e1 = op(e1,e1)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f147,f543]) ).
fof(f833,plain,
( spl0_38
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f832,f541,f442]) ).
fof(f843,plain,
( e1 = op(e3,e1)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f148,f551]) ).
fof(f844,plain,
( spl0_102
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f843,f549,f731]) ).
fof(f845,plain,
( e0 = op(e0,e3)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f149,f551]) ).
fof(f846,plain,
( spl0_69
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f845,f549,f589]) ).
fof(f847,plain,
( e0 = op(e3,e0)
| ~ spl0_60 ),
inference(forward_demodulation,[],[f150,f551]) ).
fof(f848,plain,
( spl0_97
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f847,f549,f710]) ).
fof(f852,plain,
( e0 = inv(e2)
| ~ spl0_44 ),
inference(forward_demodulation,[],[f167,f471]) ).
fof(f860,plain,
( e1 != inv(e0)
| ~ spl0_54 ),
inference(forward_demodulation,[],[f185,f524]) ).
fof(f880,plain,
( e0 = e1
| ~ spl0_3
| ~ spl0_58 ),
inference(forward_demodulation,[],[f832,f278]) ).
fof(f885,plain,
( $false
| ~ spl0_3
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f880,f239]) ).
fof(f886,plain,
( ~ spl0_3
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f885]) ).
fof(f899,plain,
( e0 = op(e0,e1)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f149,f543]) ).
fof(f900,plain,
( e0 = op(e1,e0)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f150,f543]) ).
fof(f926,plain,
( op(e3,e3) = unit
| ~ spl0_56 ),
inference(forward_demodulation,[],[f155,f534]) ).
fof(f927,plain,
( e1 = op(e3,e3)
| ~ spl0_56
| ~ spl0_58 ),
inference(forward_demodulation,[],[f926,f543]) ).
fof(f931,plain,
( spl0_25
| ~ spl0_56
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f927,f541,f532,f375]) ).
fof(f942,plain,
( e2 != op(op(e3,e1),e3)
| spl0_20
| ~ spl0_25 ),
inference(forward_demodulation,[],[f355,f376]) ).
fof(f946,plain,
( op(e0,e2) = unit
| ~ spl0_43 ),
inference(forward_demodulation,[],[f157,f468]) ).
fof(f947,plain,
( e1 = op(e0,e2)
| ~ spl0_43
| ~ spl0_58 ),
inference(forward_demodulation,[],[f946,f543]) ).
fof(f951,plain,
( spl0_66
| ~ spl0_43
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f947,f541,f466,f576]) ).
fof(f976,plain,
( e1 != op(e3,e0)
| ~ spl0_25 ),
inference(forward_demodulation,[],[f189,f376]) ).
fof(f981,plain,
( ~ spl0_98
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f976,f375,f714]) ).
fof(f985,plain,
( e3 != op(e3,e0)
| ~ spl0_104 ),
inference(forward_demodulation,[],[f191,f741]) ).
fof(f990,plain,
( e0 != op(e2,e3)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f192,f304]) ).
fof(f991,plain,
( ~ spl0_93
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f990,f303,f693]) ).
fof(f997,plain,
( e0 != op(e2,e1)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f194,f304]) ).
fof(f1001,plain,
( e2 != op(e2,e3)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f193,f685]) ).
fof(f1002,plain,
( e1 != op(e2,e3)
| ~ spl0_86 ),
inference(forward_demodulation,[],[f195,f664]) ).
fof(f1003,plain,
( ~ spl0_95
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f1001,f683,f701]) ).
fof(f1004,plain,
( ~ spl0_94
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f1002,f662,f697]) ).
fof(f1008,plain,
( e0 != op(e2,e0)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f196,f304]) ).
fof(f1009,plain,
( e2 != op(e2,e0)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f197,f685]) ).
fof(f1023,plain,
( e0 != op(e0,e2)
| ~ spl0_69 ),
inference(forward_demodulation,[],[f204,f591]) ).
fof(f1024,plain,
( e0 != op(e0,e1)
| ~ spl0_69 ),
inference(forward_demodulation,[],[f205,f591]) ).
fof(f1027,plain,
( spl0_61
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f899,f541,f555]) ).
fof(f1028,plain,
( ~ spl0_61
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1024,f589,f555]) ).
fof(f1043,plain,
( op(e0,e0) != e1
| ~ spl0_66 ),
inference(forward_demodulation,[],[f208,f578]) ).
fof(f1047,plain,
( ~ spl0_6
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f1043,f576,f290]) ).
fof(f1051,plain,
( e0 != op(e0,e0)
| ~ spl0_61 ),
inference(forward_demodulation,[],[f209,f557]) ).
fof(f1052,plain,
( e1 != op(e2,e3)
| ~ spl0_25 ),
inference(forward_demodulation,[],[f210,f376]) ).
fof(f1057,plain,
( e3 != op(e2,e3)
| ~ spl0_84 ),
inference(forward_demodulation,[],[f212,f655]) ).
fof(f1058,plain,
( e2 != op(e2,e2)
| ~ spl0_91 ),
inference(forward_demodulation,[],[f194,f685]) ).
fof(f1059,plain,
( e1 != op(e2,e2)
| ~ spl0_86 ),
inference(forward_demodulation,[],[f196,f664]) ).
fof(f1060,plain,
( ~ spl0_96
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f1057,f653,f705]) ).
fof(f1061,plain,
( ~ spl0_39
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f1058,f683,f447]) ).
fof(f1062,plain,
( ~ spl0_13
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f1059,f662,f321]) ).
fof(f1072,plain,
( e3 != op(e0,e3)
| ~ spl0_84 ),
inference(forward_demodulation,[],[f215,f655]) ).
fof(f1077,plain,
( ~ spl0_72
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f1072,f653,f601]) ).
fof(f1079,plain,
( ~ spl0_37
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f1051,f555,f437]) ).
fof(f1087,plain,
( e0 != op(e2,e2)
| ~ spl0_105 ),
inference(forward_demodulation,[],[f216,f746]) ).
fof(f1089,plain,
( e3 != op(e1,e2)
| ~ spl0_33 ),
inference(forward_demodulation,[],[f218,f415]) ).
fof(f1092,plain,
( e3 != op(e0,e2)
| ~ spl0_33 ),
inference(forward_demodulation,[],[f220,f415]) ).
fof(f1094,plain,
( e2 != op(e0,e2)
| ~ spl0_79 ),
inference(forward_demodulation,[],[f221,f634]) ).
fof(f1106,plain,
( e1 != op(e0,e1)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f227,f443]) ).
fof(f1110,plain,
( e2 != op(e1,e0)
| ~ spl0_99 ),
inference(forward_demodulation,[],[f229,f720]) ).
fof(f1115,plain,
( op(e0,e0) != e1
| ~ spl0_86 ),
inference(forward_demodulation,[],[f232,f664]) ).
fof(f1117,plain,
( e1 != op(e2,e3)
| spl0_8
| ~ spl0_33 ),
inference(forward_demodulation,[],[f301,f415]) ).
fof(f1125,plain,
( e3 != op(op(e0,e3),e0)
| spl0_4
| ~ spl0_23 ),
inference(forward_demodulation,[],[f284,f367]) ).
fof(f1131,plain,
( e2 != op(op(e0,e3),e0)
| spl0_18
| ~ spl0_23 ),
inference(forward_demodulation,[],[f346,f367]) ).
fof(f1134,plain,
( e1 != op(op(e2,e3),e2)
| spl0_27
| ~ spl0_33 ),
inference(forward_demodulation,[],[f387,f415]) ).
fof(f1135,plain,
( e1 != op(e0,e2)
| spl0_27
| ~ spl0_33
| ~ spl0_93 ),
inference(forward_demodulation,[],[f1134,f695]) ).
fof(f1138,plain,
( e0 != op(e2,e3)
| spl0_12
| ~ spl0_33 ),
inference(forward_demodulation,[],[f319,f415]) ).
fof(f1143,plain,
( e0 = op(e2,e3)
| ~ spl0_12
| ~ spl0_33 ),
inference(forward_demodulation,[],[f318,f415]) ).
fof(f1146,plain,
( ~ spl0_66
| spl0_27
| ~ spl0_33
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f1135,f693,f414,f385,f576]) ).
fof(f1148,plain,
( e0 != op(e0,e2)
| ~ spl0_61 ),
inference(forward_demodulation,[],[f206,f557]) ).
fof(f1149,plain,
( e3 != op(e0,e2)
| ~ spl0_23 ),
inference(forward_demodulation,[],[f208,f367]) ).
fof(f1150,plain,
( ~ spl0_68
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1092,f414,f584]) ).
fof(f1151,plain,
( ~ spl0_67
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f1094,f632,f580]) ).
fof(f1153,plain,
( e1 = op(inv(e0),e0)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f161,f543]) ).
fof(f1154,plain,
( e1 = op(e0,inv(e0))
| ~ spl0_58 ),
inference(forward_demodulation,[],[f162,f543]) ).
fof(f1161,plain,
( ~ spl0_68
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f1149,f366,f584]) ).
fof(f1164,plain,
( ~ spl0_65
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f1148,f555,f572]) ).
fof(f1166,plain,
( ~ spl0_94
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f1052,f375,f697]) ).
fof(f1167,plain,
( ~ spl0_94
| spl0_8
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1117,f414,f299,f697]) ).
fof(f1170,plain,
( spl0_93
| ~ spl0_12
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1143,f414,f317,f693]) ).
fof(f1171,plain,
( ~ spl0_87
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f1009,f683,f666]) ).
fof(f1172,plain,
( e3 != op(e2,e0)
| ~ spl0_33 ),
inference(forward_demodulation,[],[f196,f415]) ).
fof(f1174,plain,
( e0 != op(e2,e0)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f230,f608]) ).
fof(f1179,plain,
( ~ spl0_88
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1172,f414,f670]) ).
fof(f1181,plain,
( e1 = op(e2,e3)
| ~ spl0_8
| ~ spl0_33 ),
inference(forward_demodulation,[],[f300,f415]) ).
fof(f1183,plain,
( ~ spl0_93
| spl0_12
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1138,f414,f317,f693]) ).
fof(f1185,plain,
( e0 != op(op(e2,e3),e2)
| ~ spl0_33
| spl0_34 ),
inference(forward_demodulation,[],[f421,f415]) ).
fof(f1186,plain,
( ~ spl0_85
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1174,f606,f658]) ).
fof(f1187,plain,
( e1 != inv(e3)
| ~ spl0_54 ),
inference(forward_demodulation,[],[f181,f524]) ).
fof(f1188,plain,
( e1 = op(inv(e3),e3)
| ~ spl0_58 ),
inference(forward_demodulation,[],[f155,f543]) ).
fof(f1193,plain,
( e3 != op(e3,e3)
| ~ spl0_84 ),
inference(forward_demodulation,[],[f211,f655]) ).
fof(f1194,plain,
( e2 != op(e3,e3)
| ~ spl0_71 ),
inference(forward_demodulation,[],[f213,f599]) ).
fof(f1195,plain,
( spl0_94
| ~ spl0_8
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1181,f414,f299,f697]) ).
fof(f1197,plain,
( ~ spl0_40
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f1193,f653,f452]) ).
fof(f1198,plain,
( spl0_73
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f900,f541,f606]) ).
fof(f1202,plain,
( ~ spl0_75
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f1110,f718,f614]) ).
fof(f1203,plain,
( e3 != op(e1,e0)
| ~ spl0_23 ),
inference(forward_demodulation,[],[f233,f367]) ).
fof(f1205,plain,
( ~ spl0_76
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f1203,f366,f618]) ).
fof(f1206,plain,
( ~ spl0_85
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1008,f303,f658]) ).
fof(f1209,plain,
( ~ spl0_32
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1194,f597,f409]) ).
fof(f1210,plain,
( ~ spl0_9
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f1087,f744,f303]) ).
fof(f1211,plain,
( e3 != op(e3,e2)
| ~ spl0_104 ),
inference(forward_demodulation,[],[f188,f741]) ).
fof(f1213,plain,
( e2 != op(e3,e2)
| ~ spl0_79 ),
inference(forward_demodulation,[],[f217,f634]) ).
fof(f1214,plain,
( ~ spl0_108
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f1211,f739,f756]) ).
fof(f1216,plain,
( ~ spl0_107
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f1213,f632,f752]) ).
fof(f1234,plain,
( e3 = inv(e0)
| ~ spl0_45 ),
inference(forward_demodulation,[],[f164,f477]) ).
fof(f1264,plain,
( e1 = op(e3,e0)
| ~ spl0_46
| ~ spl0_58 ),
inference(forward_demodulation,[],[f1153,f480]) ).
fof(f1267,plain,
( spl0_98
| ~ spl0_46
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f1264,f541,f479,f714]) ).
fof(f1281,plain,
( e1 != op(e3,e0)
| ~ spl0_106 ),
inference(forward_demodulation,[],[f190,f750]) ).
fof(f1288,plain,
( ~ spl0_100
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f985,f739,f722]) ).
fof(f1290,plain,
( e0 != op(e3,e0)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f229,f608]) ).
fof(f1291,plain,
( e1 != op(e3,e0)
| ~ spl0_6 ),
inference(forward_demodulation,[],[f231,f291]) ).
fof(f1292,plain,
( ~ spl0_98
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f1281,f748,f714]) ).
fof(f1297,plain,
( ~ spl0_98
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f1291,f290,f714]) ).
fof(f1302,plain,
( ~ spl0_97
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1290,f606,f710]) ).
fof(f1303,plain,
( ~ spl0_49
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f1187,f522,f494]) ).
fof(f1309,plain,
( spl0_54
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f807,f541,f522]) ).
fof(f1341,plain,
( op(e0,e0) = e1
| ~ spl0_53
| ~ spl0_58 ),
inference(forward_demodulation,[],[f1154,f519]) ).
fof(f1344,plain,
( e1 = op(e2,e3)
| ~ spl0_51
| ~ spl0_58 ),
inference(forward_demodulation,[],[f1188,f507]) ).
fof(f1349,plain,
( e1 != op(e2,e2)
| ~ spl0_94 ),
inference(forward_demodulation,[],[f192,f699]) ).
fof(f1355,plain,
( e1 != op(e2,e2)
| ~ spl0_106 ),
inference(forward_demodulation,[],[f216,f750]) ).
fof(f1357,plain,
( e0 != op(e0,e2)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f220,f304]) ).
fof(f1358,plain,
( e3 != op(e1,e0)
| ~ spl0_88 ),
inference(forward_demodulation,[],[f230,f672]) ).
fof(f1370,plain,
( e2 != op(e3,e0)
| ~ spl0_22
| spl0_31 ),
inference(forward_demodulation,[],[f405,f362]) ).
fof(f1373,plain,
( e1 != op(op(e3,e0),e3)
| ~ spl0_22
| spl0_30 ),
inference(forward_demodulation,[],[f401,f362]) ).
fof(f1375,plain,
( e1 != op(e2,e3)
| ~ spl0_22
| spl0_30
| ~ spl0_99 ),
inference(forward_demodulation,[],[f1373,f720]) ).
fof(f1379,plain,
( spl0_94
| ~ spl0_51
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f1344,f541,f505,f697]) ).
fof(f1381,plain,
( ~ spl0_94
| ~ spl0_22
| spl0_30
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f1375,f718,f399,f361,f697]) ).
fof(f1383,plain,
( ~ spl0_13
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f1355,f748,f321]) ).
fof(f1387,plain,
( spl0_46
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f1234,f475,f479]) ).
fof(f1453,plain,
( e0 != op(e2,e1)
| spl0_12
| ~ spl0_13 ),
inference(forward_demodulation,[],[f319,f322]) ).
fof(f1466,plain,
( e3 != op(op(e0,e2),e0)
| spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f284,f313]) ).
fof(f1469,plain,
( e3 != op(op(e2,e1),e2)
| spl0_7
| ~ spl0_13 ),
inference(forward_demodulation,[],[f297,f322]) ).
fof(f1484,plain,
( e1 != op(op(e0,e2),e0)
| ~ spl0_11
| spl0_29 ),
inference(forward_demodulation,[],[f396,f313]) ).
fof(f1485,plain,
( e1 != op(e3,e0)
| ~ spl0_11
| spl0_29
| ~ spl0_68 ),
inference(forward_demodulation,[],[f1484,f586]) ).
fof(f1488,plain,
( e3 != op(e0,e2)
| ~ spl0_11
| spl0_19 ),
inference(forward_demodulation,[],[f350,f313]) ).
fof(f1502,plain,
( ~ spl0_98
| ~ spl0_11
| spl0_29
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f1485,f584,f394,f312,f714]) ).
fof(f1505,plain,
( $false
| spl0_6
| ~ spl0_53
| ~ spl0_58 ),
inference(forward_subsumption_resolution,[],[f1341,f292]) ).
fof(f1506,plain,
( spl0_6
| ~ spl0_53
| ~ spl0_58 ),
inference(avatar_contradiction_clause,[],[f1505]) ).
fof(f1513,plain,
( e2 != op(e3,e0)
| ~ spl0_11 ),
inference(forward_demodulation,[],[f231,f313]) ).
fof(f1521,plain,
( ~ spl0_99
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1513,f312,f718]) ).
fof(f1523,plain,
( e3 = op(op(e0,e2),e0)
| ~ spl0_4
| ~ spl0_11 ),
inference(forward_demodulation,[],[f283,f313]) ).
fof(f1524,plain,
( ~ spl0_89
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f997,f303,f675]) ).
fof(f1525,plain,
( e1 != op(e0,e2)
| spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f310,f313]) ).
fof(f1527,plain,
( ~ spl0_99
| ~ spl0_22
| spl0_31 ),
inference(avatar_split_clause,[],[f1370,f403,f361,f718]) ).
fof(f1530,plain,
( e1 != op(e2,e3)
| ~ spl0_70 ),
inference(forward_demodulation,[],[f214,f595]) ).
fof(f1531,plain,
( e1 != op(e2,e1)
| ~ spl0_38 ),
inference(forward_demodulation,[],[f224,f443]) ).
fof(f1545,plain,
( e3 = op(e3,e0)
| ~ spl0_4
| ~ spl0_11
| ~ spl0_68 ),
inference(forward_demodulation,[],[f1523,f586]) ).
fof(f1546,plain,
( ~ spl0_94
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1530,f593,f697]) ).
fof(f1553,plain,
( spl0_100
| ~ spl0_4
| ~ spl0_11
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f1545,f584,f312,f282,f722]) ).
fof(f1560,plain,
( e0 != op(e1,e1)
| ~ spl0_73 ),
inference(forward_demodulation,[],[f203,f608]) ).
fof(f1561,plain,
( e0 != op(e1,e1)
| ~ spl0_61 ),
inference(forward_demodulation,[],[f227,f557]) ).
fof(f1562,plain,
( ~ spl0_3
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f1560,f606,f277]) ).
fof(f1563,plain,
( ~ spl0_3
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f1561,f555,f277]) ).
fof(f1570,plain,
( ~ spl0_90
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1531,f442,f679]) ).
fof(f1589,plain,
( e3 = op(e3,e2)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f143,f547]) ).
fof(f1590,plain,
( spl0_108
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f1589,f545,f756]) ).
fof(f1595,plain,
( e3 = op(e3,e0)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f143,f539]) ).
fof(f1596,plain,
( spl0_100
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f1595,f537,f722]) ).
fof(f1597,plain,
( e3 = op(e0,e3)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f144,f539]) ).
fof(f1602,plain,
( spl0_72
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f1597,f537,f601]) ).
fof(f1605,plain,
( ~ spl0_62
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f1106,f442,f559]) ).
fof(f1609,plain,
( e3 != op(e1,e2)
| ~ spl0_68 ),
inference(forward_demodulation,[],[f221,f586]) ).
fof(f1610,plain,
( e2 != op(e1,e0)
| ~ spl0_11 ),
inference(forward_demodulation,[],[f233,f313]) ).
fof(f1613,plain,
( ~ spl0_80
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f1609,f584,f636]) ).
fof(f1614,plain,
( ~ spl0_75
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1610,f312,f614]) ).
fof(f1681,plain,
( e0 = e3
| ~ spl0_97
| ~ spl0_100 ),
inference(forward_demodulation,[],[f724,f712]) ).
fof(f1682,plain,
( $false
| ~ spl0_97
| ~ spl0_100 ),
inference(forward_subsumption_resolution,[],[f1681,f237]) ).
fof(f1683,plain,
( ~ spl0_97
| ~ spl0_100 ),
inference(avatar_contradiction_clause,[],[f1682]) ).
fof(f1737,plain,
( spl0_43
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f852,f470,f466]) ).
fof(f1739,plain,
( ~ spl0_42
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f860,f522,f461]) ).
fof(f1768,plain,
( $false
| ~ spl0_76
| ~ spl0_88 ),
inference(forward_subsumption_resolution,[],[f1358,f620]) ).
fof(f1769,plain,
( ~ spl0_76
| ~ spl0_88 ),
inference(avatar_contradiction_clause,[],[f1768]) ).
fof(f1838,plain,
( ~ spl0_89
| spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1453,f321,f317,f675]) ).
fof(f1855,plain,
( e2 != op(e2,e0)
| ~ spl0_95 ),
inference(forward_demodulation,[],[f195,f703]) ).
fof(f1857,plain,
( e3 != op(e2,e0)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f197,f689]) ).
fof(f1858,plain,
( $false
| ~ spl0_88
| ~ spl0_92 ),
inference(forward_subsumption_resolution,[],[f1857,f672]) ).
fof(f1859,plain,
( ~ spl0_88
| ~ spl0_92 ),
inference(avatar_contradiction_clause,[],[f1858]) ).
fof(f1860,plain,
( e3 != op(e2,e1)
| ~ spl0_88 ),
inference(forward_demodulation,[],[f197,f672]) ).
fof(f1861,plain,
( ~ spl0_92
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f1860,f670,f687]) ).
fof(f1865,plain,
( e1 != op(e1,e2)
| ~ spl0_82 ),
inference(forward_demodulation,[],[f198,f647]) ).
fof(f1868,plain,
( ~ spl0_78
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1865,f645,f628]) ).
fof(f1873,plain,
( e0 != op(e1,e1)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f200,f626]) ).
fof(f1874,plain,
( e1 != op(e1,e0)
| ~ spl0_82 ),
inference(forward_demodulation,[],[f201,f647]) ).
fof(f1878,plain,
( ~ spl0_74
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1874,f645,f610]) ).
fof(f1882,plain,
( op(e0,e0) != e1
| ~ spl0_62 ),
inference(forward_demodulation,[],[f209,f561]) ).
fof(f1883,plain,
( ~ spl0_6
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f1882,f559,f290]) ).
fof(f1894,plain,
( e3 != op(e1,e0)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f203,f381]) ).
fof(f1899,plain,
( e3 != op(e2,e3)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f210,f453]) ).
fof(f1905,plain,
( e3 != op(e0,e3)
| ~ spl0_40 ),
inference(forward_demodulation,[],[f213,f453]) ).
fof(f1911,plain,
( e2 != op(e2,e2)
| ~ spl0_107 ),
inference(forward_demodulation,[],[f216,f754]) ).
fof(f1921,plain,
( ~ spl0_39
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f1911,f752,f447]) ).
fof(f1922,plain,
( e0 != op(e2,e2)
| ~ spl0_77 ),
inference(forward_demodulation,[],[f218,f626]) ).
fof(f1923,plain,
( ~ spl0_9
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f1922,f624,f303]) ).
fof(f1932,plain,
( e1 != op(e2,e1)
| ~ spl0_102 ),
inference(forward_demodulation,[],[f222,f733]) ).
fof(f1934,plain,
( e1 != op(e1,e1)
| ~ spl0_102 ),
inference(forward_demodulation,[],[f223,f733]) ).
fof(f1935,plain,
( e0 != op(e1,e1)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f224,f677]) ).
fof(f1936,plain,
( e1 != op(e0,e1)
| ~ spl0_102 ),
inference(forward_demodulation,[],[f225,f733]) ).
fof(f1938,plain,
( e3 != op(e0,e1)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f227,f381]) ).
fof(f1940,plain,
( e0 != op(e2,e0)
| ~ spl0_97 ),
inference(forward_demodulation,[],[f228,f712]) ).
fof(f1949,plain,
( e0 = op(e2,e1)
| ~ spl0_12
| ~ spl0_13 ),
inference(forward_demodulation,[],[f318,f322]) ).
fof(f1961,plain,
( e3 != op(e2,e1)
| ~ spl0_13
| spl0_28 ),
inference(forward_demodulation,[],[f391,f322]) ).
fof(f1964,plain,
( e3 != op(e0,e2)
| spl0_7
| ~ spl0_13
| ~ spl0_89 ),
inference(forward_demodulation,[],[f1469,f677]) ).
fof(f1969,plain,
( e2 != op(e0,e2)
| ~ spl0_107 ),
inference(forward_demodulation,[],[f219,f754]) ).
fof(f1975,plain,
( ~ spl0_68
| spl0_7
| ~ spl0_13
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1964,f675,f321,f295,f584]) ).
fof(f1976,plain,
( ~ spl0_65
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1023,f589,f572]) ).
fof(f1994,plain,
( ~ spl0_87
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f1855,f701,f666]) ).
fof(f1995,plain,
( ~ spl0_67
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f1969,f752,f580]) ).
fof(f2017,plain,
( e3 != op(e1,e2)
| ~ spl0_26 ),
inference(forward_demodulation,[],[f200,f381]) ).
fof(f2020,plain,
( e1 != op(e0,e3)
| ~ spl0_6 ),
inference(forward_demodulation,[],[f207,f291]) ).
fof(f2021,plain,
( e2 != op(e0,e3)
| ~ spl0_63 ),
inference(forward_demodulation,[],[f205,f565]) ).
fof(f2028,plain,
( ~ spl0_80
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f2017,f380,f636]) ).
fof(f2030,plain,
( ~ spl0_70
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f2020,f290,f593]) ).
fof(f2031,plain,
( ~ spl0_71
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f2021,f563,f597]) ).
fof(f2037,plain,
( e0 != op(e2,e3)
| ~ spl0_89 ),
inference(forward_demodulation,[],[f193,f677]) ).
fof(f2040,plain,
( e2 != op(e1,e1)
| ~ spl0_63 ),
inference(forward_demodulation,[],[f227,f565]) ).
fof(f2041,plain,
( ~ spl0_3
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1935,f675,f277]) ).
fof(f2042,plain,
( ~ spl0_15
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f2040,f563,f330]) ).
fof(f2050,plain,
( ~ spl0_38
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1934,f731,f442]) ).
fof(f2070,plain,
( e2 = op(e2,e0)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f145,f539]) ).
fof(f2071,plain,
( spl0_87
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2070,f537,f666]) ).
fof(f2072,plain,
( e2 = op(e0,e2)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f146,f539]) ).
fof(f2073,plain,
( spl0_67
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2072,f537,f580]) ).
fof(f2077,plain,
( spl0_89
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1949,f321,f317,f675]) ).
fof(f2078,plain,
( ~ spl0_92
| ~ spl0_13
| spl0_28 ),
inference(avatar_split_clause,[],[f1961,f389,f321,f687]) ).
fof(f2084,plain,
( e1 = op(e1,e0)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f147,f539]) ).
fof(f2087,plain,
( spl0_74
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2084,f537,f610]) ).
fof(f2088,plain,
( e1 = op(e0,e1)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f148,f539]) ).
fof(f2089,plain,
( spl0_62
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2088,f537,f559]) ).
fof(f2090,plain,
( e0 = op(e0,e0)
| ~ spl0_57 ),
inference(forward_demodulation,[],[f149,f539]) ).
fof(f2091,plain,
( spl0_37
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f2090,f537,f437]) ).
fof(f2198,plain,
( e0 != op(e3,e1)
| ~ spl0_22 ),
inference(forward_demodulation,[],[f187,f362]) ).
fof(f2216,plain,
( e3 != op(e3,e2)
| ~ spl0_100 ),
inference(forward_demodulation,[],[f190,f724]) ).
fof(f2226,plain,
( e2 != op(e3,e3)
| ~ spl0_103 ),
inference(forward_demodulation,[],[f187,f737]) ).
fof(f2240,plain,
( ~ spl0_108
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f2216,f722,f756]) ).
fof(f2249,plain,
( ~ spl0_80
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1089,f414,f636]) ).
fof(f2258,plain,
( ~ spl0_93
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f2037,f675,f693]) ).
fof(f2260,plain,
( e2 != op(e2,e2)
| ~ spl0_67 ),
inference(forward_demodulation,[],[f220,f582]) ).
fof(f2262,plain,
( ~ spl0_39
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f2260,f580,f447]) ).
fof(f2271,plain,
( ~ spl0_32
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f2226,f735,f409]) ).
fof(f2272,plain,
( ~ spl0_13
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f1349,f697,f321]) ).
fof(f2275,plain,
( ~ spl0_90
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1932,f731,f679]) ).
fof(f2383,plain,
( e2 != op(e1,e1)
| ~ spl0_103 ),
inference(forward_demodulation,[],[f223,f737]) ).
fof(f2385,plain,
( e2 != op(e0,e1)
| ~ spl0_103 ),
inference(forward_demodulation,[],[f225,f737]) ).
fof(f2413,plain,
( e0 != op(e1,e2)
| ~ spl0_33
| spl0_34
| ~ spl0_94 ),
inference(forward_demodulation,[],[f1185,f699]) ).
fof(f2414,plain,
( $false
| ~ spl0_33
| spl0_34
| ~ spl0_77
| ~ spl0_94 ),
inference(forward_subsumption_resolution,[],[f2413,f626]) ).
fof(f2415,plain,
( ~ spl0_33
| spl0_34
| ~ spl0_77
| ~ spl0_94 ),
inference(avatar_contradiction_clause,[],[f2414]) ).
fof(f2421,plain,
( ~ spl0_72
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1905,f452,f601]) ).
fof(f2430,plain,
( ~ spl0_62
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1936,f731,f559]) ).
fof(f2433,plain,
( e0 != op(e3,e0)
| ~ spl0_37 ),
inference(forward_demodulation,[],[f231,f438]) ).
fof(f2434,plain,
( e0 != op(e2,e0)
| ~ spl0_37 ),
inference(forward_demodulation,[],[f232,f438]) ).
fof(f2456,plain,
( ~ spl0_97
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f2433,f437,f710]) ).
fof(f2462,plain,
( ~ spl0_65
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1357,f303,f572]) ).
fof(f2476,plain,
( ~ spl0_96
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f1899,f452,f705]) ).
fof(f2593,plain,
( e3 != op(e1,e0)
| ~ spl0_80 ),
inference(forward_demodulation,[],[f202,f638]) ).
fof(f2595,plain,
( e2 != op(e1,e0)
| ~ spl0_15 ),
inference(forward_demodulation,[],[f203,f331]) ).
fof(f2596,plain,
( $false
| ~ spl0_15
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f2595,f616]) ).
fof(f2597,plain,
( ~ spl0_15
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f2596]) ).
fof(f2608,plain,
( op(e0,e0) != e3
| ~ spl0_64 ),
inference(forward_demodulation,[],[f209,f569]) ).
fof(f2609,plain,
( $false
| ~ spl0_23
| ~ spl0_64 ),
inference(forward_subsumption_resolution,[],[f2608,f367]) ).
fof(f2610,plain,
( ~ spl0_23
| ~ spl0_64 ),
inference(avatar_contradiction_clause,[],[f2609]) ).
fof(f2614,plain,
( e3 != op(e0,e1)
| ~ spl0_23 ),
inference(forward_demodulation,[],[f209,f367]) ).
fof(f2615,plain,
( ~ spl0_64
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f2614,f366,f567]) ).
fof(f2641,plain,
( e3 != op(e1,e1)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f224,f689]) ).
fof(f2654,plain,
( e1 != op(e0,e3)
| spl0_10
| ~ spl0_23 ),
inference(forward_demodulation,[],[f310,f367]) ).
fof(f2663,plain,
( op(e0,e0) != e3
| spl0_4
| ~ spl0_23
| ~ spl0_69 ),
inference(forward_demodulation,[],[f1125,f591]) ).
fof(f2664,plain,
( $false
| spl0_4
| ~ spl0_23
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f2663,f367]) ).
fof(f2665,plain,
( spl0_4
| ~ spl0_23
| ~ spl0_69 ),
inference(avatar_contradiction_clause,[],[f2664]) ).
fof(f2669,plain,
( e3 != op(op(e1,e0),e1)
| spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f271,f278]) ).
fof(f2670,plain,
( e3 != op(e2,e1)
| spl0_1
| ~ spl0_3
| ~ spl0_75 ),
inference(forward_demodulation,[],[f2669,f616]) ).
fof(f2674,plain,
( e2 != op(e1,e0)
| spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f275,f278]) ).
fof(f2676,plain,
( $false
| spl0_2
| ~ spl0_3
| ~ spl0_75 ),
inference(forward_subsumption_resolution,[],[f2674,f616]) ).
fof(f2677,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_75 ),
inference(avatar_contradiction_clause,[],[f2676]) ).
fof(f2689,plain,
( ~ spl0_76
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f2593,f636,f618]) ).
fof(f2696,plain,
( ~ spl0_101
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f2198,f361,f727]) ).
fof(f2705,plain,
( ~ spl0_76
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1894,f380,f618]) ).
fof(f2706,plain,
( ~ spl0_64
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1938,f380,f567]) ).
fof(f2720,plain,
( ~ spl0_3
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f1873,f624,f277]) ).
fof(f2734,plain,
( e3 != op(e2,e2)
| ~ spl0_92 ),
inference(forward_demodulation,[],[f194,f689]) ).
fof(f2736,plain,
( e1 != op(e2,e2)
| ~ spl0_66 ),
inference(forward_demodulation,[],[f220,f578]) ).
fof(f2737,plain,
( ~ spl0_26
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f2641,f687,f380]) ).
fof(f2745,plain,
( ~ spl0_33
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f2734,f687,f414]) ).
fof(f2760,plain,
( ~ spl0_15
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f2383,f735,f330]) ).
fof(f2761,plain,
( ~ spl0_63
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f2385,f735,f563]) ).
fof(f2762,plain,
( ~ spl0_6
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f1115,f662,f290]) ).
fof(f2764,plain,
( ~ spl0_70
| spl0_10
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f2654,f366,f308,f593]) ).
fof(f2785,plain,
( e3 = op(e2,e3)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f144,f547]) ).
fof(f2786,plain,
( spl0_96
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2785,f545,f705]) ).
fof(f2787,plain,
( ~ spl0_92
| spl0_1
| ~ spl0_3
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f2670,f614,f277,f269,f687]) ).
fof(f2790,plain,
( ~ spl0_85
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f1940,f710,f658]) ).
fof(f2791,plain,
( e2 = op(e2,e2)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f145,f547]) ).
fof(f2792,plain,
( spl0_39
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2791,f545,f447]) ).
fof(f2794,plain,
( e1 = op(e1,e2)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f147,f547]) ).
fof(f2795,plain,
( spl0_78
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2794,f545,f628]) ).
fof(f2796,plain,
( e1 = op(e2,e1)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f148,f547]) ).
fof(f2797,plain,
( spl0_90
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2796,f545,f679]) ).
fof(f2798,plain,
( e0 = op(e0,e2)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f149,f547]) ).
fof(f2799,plain,
( spl0_65
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2798,f545,f572]) ).
fof(f2800,plain,
( e0 = op(e2,e0)
| ~ spl0_59 ),
inference(forward_demodulation,[],[f150,f547]) ).
fof(f2801,plain,
( spl0_85
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f2800,f545,f658]) ).
fof(f2939,plain,
( e1 != op(e1,e0)
| ~ spl0_78 ),
inference(forward_demodulation,[],[f202,f630]) ).
fof(f2956,plain,
( e3 != op(e0,e3)
| ~ spl0_96 ),
inference(forward_demodulation,[],[f214,f707]) ).
fof(f2970,plain,
( e0 != op(e1,e1)
| ~ spl0_101 ),
inference(forward_demodulation,[],[f223,f729]) ).
fof(f2973,plain,
( e1 != op(e0,e1)
| ~ spl0_90 ),
inference(forward_demodulation,[],[f226,f681]) ).
fof(f3006,plain,
( e2 != op(e1,e0)
| spl0_18
| ~ spl0_23
| ~ spl0_70 ),
inference(forward_demodulation,[],[f1131,f595]) ).
fof(f3012,plain,
( ~ spl0_75
| spl0_18
| ~ spl0_23
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f3006,f593,f366,f344,f614]) ).
fof(f3014,plain,
( ~ spl0_74
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f2939,f628,f610]) ).
fof(f3026,plain,
( ~ spl0_72
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f2956,f705,f601]) ).
fof(f3031,plain,
( ~ spl0_62
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f2973,f679,f559]) ).
fof(f3045,plain,
( ~ spl0_85
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f2434,f437,f658]) ).
fof(f3248,plain,
( e0 != op(op(e1,e2),e1)
| ~ spl0_15
| spl0_35 ),
inference(forward_demodulation,[],[f426,f331]) ).
fof(f3249,plain,
( e0 != op(e3,e1)
| ~ spl0_15
| spl0_35
| ~ spl0_80 ),
inference(forward_demodulation,[],[f3248,f638]) ).
fof(f3250,plain,
( $false
| ~ spl0_15
| spl0_35
| ~ spl0_80
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3249,f729]) ).
fof(f3251,plain,
( ~ spl0_15
| spl0_35
| ~ spl0_80
| ~ spl0_101 ),
inference(avatar_contradiction_clause,[],[f3250]) ).
fof(f3252,plain,
( e3 != op(e1,e2)
| ~ spl0_15
| spl0_17 ),
inference(forward_demodulation,[],[f341,f331]) ).
fof(f3254,plain,
( $false
| ~ spl0_15
| spl0_17
| ~ spl0_80 ),
inference(forward_subsumption_resolution,[],[f3252,f638]) ).
fof(f3255,plain,
( ~ spl0_15
| spl0_17
| ~ spl0_80 ),
inference(avatar_contradiction_clause,[],[f3254]) ).
fof(f3263,plain,
( ~ spl0_3
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f2970,f727,f277]) ).
fof(f3376,plain,
( e0 != op(e3,e1)
| spl0_24
| ~ spl0_25 ),
inference(forward_demodulation,[],[f373,f376]) ).
fof(f3386,plain,
( e2 != op(op(e1,e0),e1)
| ~ spl0_3
| spl0_16 ),
inference(forward_demodulation,[],[f337,f278]) ).
fof(f3397,plain,
( e0 != op(op(e2,e1),e2)
| ~ spl0_13
| spl0_34 ),
inference(forward_demodulation,[],[f421,f322]) ).
fof(f3398,plain,
( e0 != op(e3,e2)
| ~ spl0_13
| spl0_34
| ~ spl0_92 ),
inference(forward_demodulation,[],[f3397,f689]) ).
fof(f3399,plain,
( $false
| ~ spl0_13
| spl0_34
| ~ spl0_92
| ~ spl0_105 ),
inference(forward_subsumption_resolution,[],[f3398,f746]) ).
fof(f3400,plain,
( ~ spl0_13
| spl0_34
| ~ spl0_92
| ~ spl0_105 ),
inference(avatar_contradiction_clause,[],[f3399]) ).
fof(f3401,plain,
( ~ spl0_68
| ~ spl0_11
| spl0_19 ),
inference(avatar_split_clause,[],[f1488,f348,f312,f584]) ).
fof(f3406,plain,
( ~ spl0_13
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f2736,f576,f321]) ).
fof(f3584,plain,
( e1 = op(e0,e2)
| ~ spl0_10
| ~ spl0_11 ),
inference(forward_demodulation,[],[f309,f313]) ).
fof(f3604,plain,
( e3 != op(e1,e0)
| spl0_4
| ~ spl0_11
| ~ spl0_66 ),
inference(forward_demodulation,[],[f1466,f578]) ).
fof(f3605,plain,
( $false
| spl0_4
| ~ spl0_11
| ~ spl0_66
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f3604,f620]) ).
fof(f3606,plain,
( spl0_4
| ~ spl0_11
| ~ spl0_66
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f3605]) ).
fof(f3609,plain,
( e2 != op(e3,e1)
| ~ spl0_3
| spl0_16
| ~ spl0_76 ),
inference(forward_demodulation,[],[f3386,f620]) ).
fof(f3633,plain,
( spl0_66
| ~ spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f3584,f312,f308,f576]) ).
fof(f3638,plain,
( ~ spl0_103
| ~ spl0_3
| spl0_16
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f3609,f618,f335,f277,f735]) ).
fof(f3642,plain,
( ~ spl0_66
| spl0_10
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1525,f312,f308,f576]) ).
fof(f3784,plain,
( e3 != op(e1,e0)
| ~ spl0_3
| spl0_17 ),
inference(forward_demodulation,[],[f341,f278]) ).
fof(f3785,plain,
( $false
| ~ spl0_3
| spl0_17
| ~ spl0_76 ),
inference(forward_subsumption_resolution,[],[f3784,f620]) ).
fof(f3786,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_76 ),
inference(avatar_contradiction_clause,[],[f3785]) ).
fof(f3791,plain,
( ~ spl0_101
| spl0_24
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f3376,f375,f371,f727]) ).
fof(f3881,plain,
( e2 != op(e0,e3)
| spl0_20
| ~ spl0_25
| ~ spl0_101 ),
inference(forward_demodulation,[],[f942,f729]) ).
fof(f3882,plain,
( $false
| spl0_20
| ~ spl0_25
| ~ spl0_71
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f3881,f599]) ).
fof(f3883,plain,
( spl0_20
| ~ spl0_25
| ~ spl0_71
| ~ spl0_101 ),
inference(avatar_contradiction_clause,[],[f3882]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f280]) ).
cnf(s4,plain,
( ~ spl0_4
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f315]) ).
cnf(s5,plain,
( ~ spl0_7
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f324]) ).
cnf(s7,plain,
( ~ spl0_3
| ~ spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f342]) ).
cnf(s10,plain,
( ~ spl0_10
| ~ spl0_18
| ~ spl0_23 ),
inference(sat_conversion,[],[f369]) ).
cnf(s11,plain,
( ~ spl0_20
| ~ spl0_24
| ~ spl0_25 ),
inference(sat_conversion,[],[f378]) ).
cnf(s14,plain,
( ~ spl0_11
| ~ spl0_19
| ~ spl0_29 ),
inference(sat_conversion,[],[f397]) ).
cnf(s15,plain,
( ~ spl0_22
| ~ spl0_30
| ~ spl0_31 ),
inference(sat_conversion,[],[f406]) ).
cnf(s18,plain,
( ~ spl0_12
| ~ spl0_27
| ~ spl0_33 ),
inference(sat_conversion,[],[f417]) ).
cnf(s19,plain,
( ~ spl0_13
| ~ spl0_28
| ~ spl0_34 ),
inference(sat_conversion,[],[f422]) ).
cnf(s20,plain,
( ~ spl0_15
| ~ spl0_17
| ~ spl0_35 ),
inference(sat_conversion,[],[f427]) ).
cnf(s24,plain,
( ~ spl0_8
| ~ spl0_33
| ~ spl0_34 ),
inference(sat_conversion,[],[f435]) ).
cnf(s25,plain,
( ~ spl0_3
| ~ spl0_9
| ~ spl0_22
| ~ spl0_37 ),
inference(sat_conversion,[],[f440]) ).
cnf(s26,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_25
| ~ spl0_38 ),
inference(sat_conversion,[],[f445]) ).
cnf(s27,plain,
( ~ spl0_11
| ~ spl0_15
| ~ spl0_32
| ~ spl0_39 ),
inference(sat_conversion,[],[f450]) ).
cnf(s28,plain,
( ~ spl0_23
| ~ spl0_26
| ~ spl0_33
| ~ spl0_40 ),
inference(sat_conversion,[],[f455]) ).
cnf(s41,plain,
( spl0_42
| spl0_44
| spl0_46
| spl0_53 ),
inference(sat_conversion,[],[f520]) ).
cnf(s44,plain,
( spl0_45
| spl0_49
| spl0_51
| spl0_56 ),
inference(sat_conversion,[],[f535]) ).
cnf(s45,plain,
( spl0_57
| spl0_58
| spl0_59
| spl0_60 ),
inference(sat_conversion,[],[f552]) ).
cnf(s46,plain,
( spl0_6
| spl0_11
| spl0_23
| spl0_37 ),
inference(sat_conversion,[],[f553]) ).
cnf(s47,plain,
( spl0_61
| spl0_62
| spl0_63
| spl0_64 ),
inference(sat_conversion,[],[f570]) ).
cnf(s48,plain,
( spl0_65
| spl0_66
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f587]) ).
cnf(s49,plain,
( spl0_69
| spl0_70
| spl0_71
| spl0_72 ),
inference(sat_conversion,[],[f604]) ).
cnf(s50,plain,
( spl0_73
| spl0_74
| spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f621]) ).
cnf(s51,plain,
( spl0_3
| spl0_15
| spl0_26
| spl0_38 ),
inference(sat_conversion,[],[f622]) ).
cnf(s52,plain,
( spl0_77
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f639]) ).
cnf(s54,plain,
( spl0_85
| spl0_86
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f673]) ).
cnf(s55,plain,
( spl0_89
| spl0_90
| spl0_91
| spl0_92 ),
inference(sat_conversion,[],[f690]) ).
cnf(s56,plain,
( spl0_9
| spl0_13
| spl0_33
| spl0_39 ),
inference(sat_conversion,[],[f691]) ).
cnf(s57,plain,
( spl0_93
| spl0_94
| spl0_95
| spl0_96 ),
inference(sat_conversion,[],[f708]) ).
cnf(s58,plain,
( spl0_97
| spl0_98
| spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f725]) ).
cnf(s59,plain,
( spl0_101
| spl0_102
| spl0_103
| spl0_104 ),
inference(sat_conversion,[],[f742]) ).
cnf(s60,plain,
( spl0_105
| spl0_106
| spl0_107
| spl0_108 ),
inference(sat_conversion,[],[f759]) ).
cnf(s61,plain,
( spl0_22
| spl0_25
| spl0_32
| spl0_40 ),
inference(sat_conversion,[],[f760]) ).
cnf(s70,plain,
( spl0_40
| ~ spl0_60 ),
inference(sat_conversion,[],[f800]) ).
cnf(s72,plain,
( ~ spl0_60
| spl0_95 ),
inference(sat_conversion,[],[f803]) ).
cnf(s73,plain,
( ~ spl0_58
| spl0_104 ),
inference(sat_conversion,[],[f809]) ).
cnf(s80,plain,
( ~ spl0_60
| spl0_107 ),
inference(sat_conversion,[],[f818]) ).
cnf(s81,plain,
( ~ spl0_60
| spl0_82 ),
inference(sat_conversion,[],[f820]) ).
cnf(s84,plain,
( ~ spl0_58
| spl0_84 ),
inference(sat_conversion,[],[f827]) ).
cnf(s85,plain,
( ~ spl0_58
| spl0_91 ),
inference(sat_conversion,[],[f829]) ).
cnf(s86,plain,
( ~ spl0_58
| spl0_79 ),
inference(sat_conversion,[],[f831]) ).
cnf(s87,plain,
( spl0_38
| ~ spl0_58 ),
inference(sat_conversion,[],[f833]) ).
cnf(s101,plain,
( ~ spl0_60
| spl0_102 ),
inference(sat_conversion,[],[f844]) ).
cnf(s102,plain,
( ~ spl0_60
| spl0_69 ),
inference(sat_conversion,[],[f846]) ).
cnf(s103,plain,
( ~ spl0_60
| spl0_97 ),
inference(sat_conversion,[],[f848]) ).
cnf(s112,plain,
( ~ spl0_3
| ~ spl0_58 ),
inference(sat_conversion,[],[f886]) ).
cnf(s128,plain,
( spl0_25
| ~ spl0_56
| ~ spl0_58 ),
inference(sat_conversion,[],[f931]) ).
cnf(s132,plain,
( ~ spl0_43
| ~ spl0_58
| spl0_66 ),
inference(sat_conversion,[],[f951]) ).
cnf(s137,plain,
( ~ spl0_25
| ~ spl0_98 ),
inference(sat_conversion,[],[f981]) ).
cnf(s140,plain,
( ~ spl0_9
| ~ spl0_93 ),
inference(sat_conversion,[],[f991]) ).
cnf(s143,plain,
( ~ spl0_91
| ~ spl0_95 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s144,plain,
( ~ spl0_86
| ~ spl0_94 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s146,plain,
( ~ spl0_58
| spl0_61 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s147,plain,
( ~ spl0_61
| ~ spl0_69 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s152,plain,
( ~ spl0_6
| ~ spl0_66 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s155,plain,
( ~ spl0_84
| ~ spl0_96 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s156,plain,
( ~ spl0_39
| ~ spl0_91 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s157,plain,
( ~ spl0_13
| ~ spl0_86 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s159,plain,
( ~ spl0_72
| ~ spl0_84 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s161,plain,
( ~ spl0_37
| ~ spl0_61 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s165,plain,
( spl0_27
| ~ spl0_33
| ~ spl0_66
| ~ spl0_93 ),
inference(sat_conversion,[],[f1146]) ).
cnf(s166,plain,
( ~ spl0_33
| ~ spl0_68 ),
inference(sat_conversion,[],[f1150]) ).
cnf(s167,plain,
( ~ spl0_67
| ~ spl0_79 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s172,plain,
( ~ spl0_23
| ~ spl0_68 ),
inference(sat_conversion,[],[f1161]) ).
cnf(s176,plain,
( ~ spl0_61
| ~ spl0_65 ),
inference(sat_conversion,[],[f1164]) ).
cnf(s178,plain,
( ~ spl0_25
| ~ spl0_94 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s179,plain,
( spl0_8
| ~ spl0_33
| ~ spl0_94 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s180,plain,
( ~ spl0_12
| ~ spl0_33
| spl0_93 ),
inference(sat_conversion,[],[f1170]) ).
cnf(s181,plain,
( ~ spl0_87
| ~ spl0_91 ),
inference(sat_conversion,[],[f1171]) ).
cnf(s186,plain,
( ~ spl0_33
| ~ spl0_88 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s188,plain,
( spl0_12
| ~ spl0_33
| ~ spl0_93 ),
inference(sat_conversion,[],[f1183]) ).
cnf(s189,plain,
( ~ spl0_73
| ~ spl0_85 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s190,plain,
( ~ spl0_8
| ~ spl0_33
| spl0_94 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s193,plain,
( ~ spl0_40
| ~ spl0_84 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s194,plain,
( ~ spl0_58
| spl0_73 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s198,plain,
( ~ spl0_75
| ~ spl0_99 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s200,plain,
( ~ spl0_23
| ~ spl0_76 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s201,plain,
( ~ spl0_9
| ~ spl0_85 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s205,plain,
( ~ spl0_32
| ~ spl0_71 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s206,plain,
( ~ spl0_9
| ~ spl0_105 ),
inference(sat_conversion,[],[f1210]) ).
cnf(s207,plain,
( ~ spl0_104
| ~ spl0_108 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s209,plain,
( ~ spl0_79
| ~ spl0_107 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s213,plain,
( ~ spl0_46
| ~ spl0_58
| spl0_98 ),
inference(sat_conversion,[],[f1267]) ).
cnf(s218,plain,
( ~ spl0_100
| ~ spl0_104 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s219,plain,
( ~ spl0_98
| ~ spl0_106 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s222,plain,
( ~ spl0_6
| ~ spl0_98 ),
inference(sat_conversion,[],[f1297]) ).
cnf(s225,plain,
( ~ spl0_73
| ~ spl0_97 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s226,plain,
( ~ spl0_49
| ~ spl0_54 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s228,plain,
( spl0_54
| ~ spl0_58 ),
inference(sat_conversion,[],[f1309]) ).
cnf(s238,plain,
( ~ spl0_51
| ~ spl0_58
| spl0_94 ),
inference(sat_conversion,[],[f1379]) ).
cnf(s239,plain,
( ~ spl0_22
| spl0_30
| ~ spl0_94
| ~ spl0_99 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s241,plain,
( ~ spl0_13
| ~ spl0_106 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s246,plain,
( ~ spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f1387]) ).
cnf(s266,plain,
( ~ spl0_11
| spl0_29
| ~ spl0_68
| ~ spl0_98 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s268,plain,
( spl0_6
| ~ spl0_53
| ~ spl0_58 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s280,plain,
( ~ spl0_11
| ~ spl0_99 ),
inference(sat_conversion,[],[f1521]) ).
cnf(s284,plain,
( ~ spl0_9
| ~ spl0_89 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s289,plain,
( ~ spl0_22
| spl0_31
| ~ spl0_99 ),
inference(sat_conversion,[],[f1527]) ).
cnf(s293,plain,
( ~ spl0_70
| ~ spl0_94 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s299,plain,
( ~ spl0_4
| ~ spl0_11
| ~ spl0_68
| spl0_100 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s309,plain,
( ~ spl0_3
| ~ spl0_73 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s310,plain,
( ~ spl0_3
| ~ spl0_61 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s316,plain,
( ~ spl0_38
| ~ spl0_90 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s319,plain,
( ~ spl0_59
| spl0_108 ),
inference(sat_conversion,[],[f1590]) ).
cnf(s320,plain,
( ~ spl0_57
| spl0_100 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s324,plain,
( ~ spl0_57
| spl0_72 ),
inference(sat_conversion,[],[f1602]) ).
cnf(s325,plain,
( ~ spl0_38
| ~ spl0_62 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s353,plain,
( ~ spl0_68
| ~ spl0_80 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s354,plain,
( ~ spl0_11
| ~ spl0_75 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s364,plain,
( ~ spl0_97
| ~ spl0_100 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s381,plain,
( spl0_43
| ~ spl0_44 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s383,plain,
( ~ spl0_42
| ~ spl0_54 ),
inference(sat_conversion,[],[f1739]) ).
cnf(s399,plain,
( ~ spl0_76
| ~ spl0_88 ),
inference(sat_conversion,[],[f1769]) ).
cnf(s405,plain,
( spl0_12
| ~ spl0_13
| ~ spl0_89 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s407,plain,
( ~ spl0_88
| ~ spl0_92 ),
inference(sat_conversion,[],[f1859]) ).
cnf(s408,plain,
( ~ spl0_88
| ~ spl0_92 ),
inference(sat_conversion,[],[f1861]) ).
cnf(s410,plain,
( ~ spl0_78
| ~ spl0_82 ),
inference(sat_conversion,[],[f1868]) ).
cnf(s412,plain,
( ~ spl0_74
| ~ spl0_82 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s415,plain,
( ~ spl0_6
| ~ spl0_62 ),
inference(sat_conversion,[],[f1883]) ).
cnf(s419,plain,
( ~ spl0_39
| ~ spl0_107 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s420,plain,
( ~ spl0_9
| ~ spl0_77 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s428,plain,
( spl0_7
| ~ spl0_13
| ~ spl0_68
| ~ spl0_89 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s429,plain,
( ~ spl0_65
| ~ spl0_69 ),
inference(sat_conversion,[],[f1976]) ).
cnf(s444,plain,
( ~ spl0_87
| ~ spl0_95 ),
inference(sat_conversion,[],[f1994]) ).
cnf(s445,plain,
( ~ spl0_67
| ~ spl0_107 ),
inference(sat_conversion,[],[f1995]) ).
cnf(s467,plain,
( ~ spl0_26
| ~ spl0_80 ),
inference(sat_conversion,[],[f2028]) ).
cnf(s470,plain,
( ~ spl0_6
| ~ spl0_70 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s471,plain,
( ~ spl0_63
| ~ spl0_71 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s478,plain,
( ~ spl0_3
| ~ spl0_89 ),
inference(sat_conversion,[],[f2041]) ).
cnf(s479,plain,
( ~ spl0_15
| ~ spl0_63 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s488,plain,
( ~ spl0_38
| ~ spl0_102 ),
inference(sat_conversion,[],[f2050]) ).
cnf(s495,plain,
( ~ spl0_57
| spl0_87 ),
inference(sat_conversion,[],[f2071]) ).
cnf(s496,plain,
( ~ spl0_57
| spl0_67 ),
inference(sat_conversion,[],[f2073]) ).
cnf(s506,plain,
( ~ spl0_12
| ~ spl0_13
| spl0_89 ),
inference(sat_conversion,[],[f2077]) ).
cnf(s507,plain,
( ~ spl0_13
| spl0_28
| ~ spl0_92 ),
inference(sat_conversion,[],[f2078]) ).
cnf(s530,plain,
( ~ spl0_57
| spl0_74 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s531,plain,
( ~ spl0_57
| spl0_62 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s532,plain,
( spl0_37
| ~ spl0_57 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s562,plain,
( ~ spl0_100
| ~ spl0_108 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s572,plain,
( ~ spl0_33
| ~ spl0_80 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s586,plain,
( ~ spl0_89
| ~ spl0_93 ),
inference(sat_conversion,[],[f2258]) ).
cnf(s590,plain,
( ~ spl0_39
| ~ spl0_67 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s599,plain,
( ~ spl0_32
| ~ spl0_103 ),
inference(sat_conversion,[],[f2271]) ).
cnf(s605,plain,
( ~ spl0_13
| ~ spl0_94 ),
inference(sat_conversion,[],[f2272]) ).
cnf(s608,plain,
( ~ spl0_90
| ~ spl0_102 ),
inference(sat_conversion,[],[f2275]) ).
cnf(s627,plain,
( ~ spl0_33
| spl0_34
| ~ spl0_77
| ~ spl0_94 ),
inference(sat_conversion,[],[f2415]) ).
cnf(s636,plain,
( ~ spl0_40
| ~ spl0_72 ),
inference(sat_conversion,[],[f2421]) ).
cnf(s657,plain,
( ~ spl0_62
| ~ spl0_102 ),
inference(sat_conversion,[],[f2430]) ).
cnf(s663,plain,
( ~ spl0_37
| ~ spl0_97 ),
inference(sat_conversion,[],[f2456]) ).
cnf(s671,plain,
( ~ spl0_9
| ~ spl0_65 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s734,plain,
( ~ spl0_40
| ~ spl0_96 ),
inference(sat_conversion,[],[f2476]) ).
cnf(s748,plain,
( ~ spl0_15
| ~ spl0_75 ),
inference(sat_conversion,[],[f2597]) ).
cnf(s751,plain,
( ~ spl0_23
| ~ spl0_64 ),
inference(sat_conversion,[],[f2610]) ).
cnf(s752,plain,
( ~ spl0_23
| ~ spl0_64 ),
inference(sat_conversion,[],[f2615]) ).
cnf(s753,plain,
( spl0_4
| ~ spl0_23
| ~ spl0_69 ),
inference(sat_conversion,[],[f2665]) ).
cnf(s755,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_75 ),
inference(sat_conversion,[],[f2677]) ).
cnf(s760,plain,
( ~ spl0_76
| ~ spl0_80 ),
inference(sat_conversion,[],[f2689]) ).
cnf(s771,plain,
( ~ spl0_22
| ~ spl0_101 ),
inference(sat_conversion,[],[f2696]) ).
cnf(s779,plain,
( ~ spl0_26
| ~ spl0_76 ),
inference(sat_conversion,[],[f2705]) ).
cnf(s781,plain,
( ~ spl0_26
| ~ spl0_64 ),
inference(sat_conversion,[],[f2706]) ).
cnf(s797,plain,
( ~ spl0_3
| ~ spl0_77 ),
inference(sat_conversion,[],[f2720]) ).
cnf(s805,plain,
( ~ spl0_26
| ~ spl0_92 ),
inference(sat_conversion,[],[f2737]) ).
cnf(s812,plain,
( ~ spl0_33
| ~ spl0_92 ),
inference(sat_conversion,[],[f2745]) ).
cnf(s849,plain,
( ~ spl0_15
| ~ spl0_103 ),
inference(sat_conversion,[],[f2760]) ).
cnf(s850,plain,
( ~ spl0_63
| ~ spl0_103 ),
inference(sat_conversion,[],[f2761]) ).
cnf(s853,plain,
( ~ spl0_6
| ~ spl0_86 ),
inference(sat_conversion,[],[f2762]) ).
cnf(s858,plain,
( spl0_10
| ~ spl0_23
| ~ spl0_70 ),
inference(sat_conversion,[],[f2764]) ).
cnf(s881,plain,
( ~ spl0_59
| spl0_96 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s882,plain,
( spl0_1
| ~ spl0_3
| ~ spl0_75
| ~ spl0_92 ),
inference(sat_conversion,[],[f2787]) ).
cnf(s888,plain,
( ~ spl0_85
| ~ spl0_97 ),
inference(sat_conversion,[],[f2790]) ).
cnf(s917,plain,
( spl0_39
| ~ spl0_59 ),
inference(sat_conversion,[],[f2792]) ).
cnf(s919,plain,
( ~ spl0_59
| spl0_78 ),
inference(sat_conversion,[],[f2795]) ).
cnf(s920,plain,
( ~ spl0_59
| spl0_90 ),
inference(sat_conversion,[],[f2797]) ).
cnf(s924,plain,
( ~ spl0_59
| spl0_65 ),
inference(sat_conversion,[],[f2799]) ).
cnf(s925,plain,
( ~ spl0_59
| spl0_85 ),
inference(sat_conversion,[],[f2801]) ).
cnf(s949,plain,
( spl0_18
| ~ spl0_23
| ~ spl0_70
| ~ spl0_75 ),
inference(sat_conversion,[],[f3012]) ).
cnf(s951,plain,
( ~ spl0_74
| ~ spl0_78 ),
inference(sat_conversion,[],[f3014]) ).
cnf(s962,plain,
( ~ spl0_72
| ~ spl0_96 ),
inference(sat_conversion,[],[f3026]) ).
cnf(s968,plain,
( ~ spl0_62
| ~ spl0_90 ),
inference(sat_conversion,[],[f3031]) ).
cnf(s1003,plain,
( ~ spl0_37
| ~ spl0_85 ),
inference(sat_conversion,[],[f3045]) ).
cnf(s1074,plain,
( ~ spl0_15
| spl0_35
| ~ spl0_80
| ~ spl0_101 ),
inference(sat_conversion,[],[f3251]) ).
cnf(s1075,plain,
( ~ spl0_15
| spl0_17
| ~ spl0_80 ),
inference(sat_conversion,[],[f3255]) ).
cnf(s1079,plain,
( ~ spl0_3
| ~ spl0_101 ),
inference(sat_conversion,[],[f3263]) ).
cnf(s1135,plain,
( ~ spl0_13
| spl0_34
| ~ spl0_92
| ~ spl0_105 ),
inference(sat_conversion,[],[f3400]) ).
cnf(s1138,plain,
( ~ spl0_11
| spl0_19
| ~ spl0_68 ),
inference(sat_conversion,[],[f3401]) ).
cnf(s1237,plain,
( ~ spl0_13
| ~ spl0_66 ),
inference(sat_conversion,[],[f3406]) ).
cnf(s1288,plain,
( spl0_4
| ~ spl0_11
| ~ spl0_66
| ~ spl0_76 ),
inference(sat_conversion,[],[f3606]) ).
cnf(s1353,plain,
( ~ spl0_10
| ~ spl0_11
| spl0_66 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s1357,plain,
( ~ spl0_3
| spl0_16
| ~ spl0_76
| ~ spl0_103 ),
inference(sat_conversion,[],[f3638]) ).
cnf(s1377,plain,
( spl0_10
| ~ spl0_11
| ~ spl0_66 ),
inference(sat_conversion,[],[f3642]) ).
cnf(s1387,plain,
( ~ spl0_3
| spl0_17
| ~ spl0_76 ),
inference(sat_conversion,[],[f3786]) ).
cnf(s1394,plain,
( spl0_24
| ~ spl0_25
| ~ spl0_101 ),
inference(sat_conversion,[],[f3791]) ).
cnf(s1423,plain,
( spl0_20
| ~ spl0_25
| ~ spl0_71
| ~ spl0_101 ),
inference(sat_conversion,[],[f3883]) ).
cnf(s1424,plain,
( ~ spl0_57
| spl0_13
| spl0_12
| spl0_9
| spl0_8 ),
inference(rat,[],[s57,s179,s188,s56,s962,s444,s590,s324,s495,s496]) ).
cnf(s1425,plain,
( ~ spl0_60
| spl0_11
| spl0_6
| spl0_4 ),
inference(rat,[],[s46,s753,s663,s102,s103]) ).
cnf(s1428,plain,
( ~ spl0_92
| ~ spl0_105
| ~ spl0_13 ),
inference(rat,[],[s19,s507,s1135]) ).
cnf(s1429,plain,
( spl0_12
| ~ spl0_57
| spl0_9
| spl0_8 ),
inference(rat,[],[s1428,s55,s60,s405,s241,s1424,s968,s531,s445,s496,s181,s495,s562,s320]) ).
cnf(s1430,plain,
( ~ spl0_33
| ~ spl0_12
| spl0_91
| spl0_90 ),
inference(rat,[],[s586,s55,s180,s812]) ).
cnf(s1431,plain,
( ~ spl0_57
| spl0_9
| spl0_8 ),
inference(rat,[],[s586,s57,s506,s605,s56,s1430,s1429,s962,s181,s444,s590,s968,s324,s495,s496,s531]) ).
cnf(s1436,plain,
( ~ spl0_60
| spl0_86
| spl0_6
| spl0_4 ),
inference(rat,[],[s399,s50,s54,s354,s444,s412,s225,s888,s1425,s72,s81,s103]) ).
cnf(s1439,plain,
( ~ spl0_60
| ~ spl0_10
| spl0_6
| spl0_4 ),
inference(rat,[],[s50,s1288,s354,s1353,s412,s225,s1425,s81,s103]) ).
cnf(s1440,plain,
( ~ spl0_33
| ~ spl0_58
| spl0_8 ),
inference(rat,[],[s18,s165,s188,s48,s57,s166,s179,s176,s146,s167,s86,s143,s85,s155,s84]) ).
cnf(s1443,plain,
( ~ spl0_57
| ~ spl0_9
| spl0_3 ),
inference(rat,[],[s1074,s20,s59,s1075,s849,s51,s805,s52,s55,s218,s181,s167,s951,s325,s657,s968,s320,s495,s496,s530,s531,s420,s284]) ).
cnf(s1445,plain,
( ~ spl0_33
| ~ spl0_57
| ~ spl0_8 ),
inference(rat,[],[s627,s52,s24,s190,s572,s951,s530,s167,s496]) ).
cnf(s1446,plain,
( ~ spl0_57
| spl0_9
| ~ spl0_8 ),
inference(rat,[],[s55,s1428,s586,s60,s57,s241,s605,s56,s1445,s562,s962,s181,s444,s445,s590,s968,s320,s324,s495,s496,s531]) ).
cnf(s1447,plain,
( ~ spl0_33
| ~ spl0_58
| ~ spl0_8 ),
inference(rat,[],[s54,s144,s186,s190,s189,s194,s181,s85]) ).
cnf(s1451,plain,
( ~ spl0_60
| spl0_77
| spl0_65
| spl0_6
| spl0_4 ),
inference(rat,[],[s353,s48,s52,s1377,s209,s445,s410,s1439,s1425,s80,s81]) ).
cnf(s1453,plain,
( ~ spl0_60
| spl0_9
| ~ spl0_6 ),
inference(rat,[],[s5,s428,s405,s55,s56,s408,s166,s54,s48,s143,s444,s419,s445,s608,s429,s888,s72,s80,s101,s102,s103,s853,s152]) ).
cnf(s1454,plain,
( ~ spl0_58
| spl0_9
| spl0_8
| ~ spl0_6 ),
inference(rat,[],[s44,s128,s238,s26,s605,s246,s56,s156,s226,s213,s1440,s85,s87,s228,s222]) ).
cnf(s1455,plain,
( ~ spl0_25
| ~ spl0_101
| ~ spl0_71 ),
inference(rat,[],[s11,s1394,s1423]) ).
cnf(s1456,plain,
( ~ spl0_59
| ~ spl0_6
| spl0_3 ),
inference(rat,[],[s1455,s61,s771,s59,s849,s51,s781,s47,s205,s471,s49,s207,s734,s962,s316,s608,s176,s429,s319,s881,s920,s924,s470,s415]) ).
cnf(s1457,plain,
( spl0_9
| spl0_8
| spl0_59
| ~ spl0_6 ),
inference(rat,[],[s45,s1454,s1453,s531,s415]) ).
cnf(s1458,plain,
( ~ spl0_60
| ~ spl0_9
| spl0_86 ),
inference(rat,[],[s407,s54,s55,s143,s444,s608,s72,s101,s284,s201]) ).
cnf(s1459,plain,
( ~ spl0_9
| spl0_59
| spl0_57
| spl0_98
| spl0_70
| spl0_86 ),
inference(rat,[],[s15,s239,s289,s61,s178,s205,s58,s57,s49,s218,s155,s159,s193,s143,s147,s225,s73,s84,s85,s146,s194,s45,s1458,s140]) ).
cnf(s1460,plain,
( ~ spl0_6
| spl0_3 ),
inference(rat,[],[s44,s128,s238,s26,s605,s246,s56,s156,s226,s213,s1447,s85,s87,s228,s45,s1457,s1453,s1459,s1456,s531,s222,s415,s470,s853]) ).
cnf(s1461,plain,
( ~ spl0_57
| spl0_9 ),
inference(rat,[],[s1446,s1431]) ).
cnf(s1462,plain,
( ~ spl0_60
| spl0_9
| spl0_4
| spl0_6 ),
inference(rat,[],[s166,s56,s48,s157,s1377,s419,s445,s429,s1439,s1436,s1425,s80,s102]) ).
cnf(s1463,plain,
( ~ spl0_58
| spl0_8
| spl0_9
| spl0_6 ),
inference(rat,[],[s14,s266,s1138,s213,s46,s41,s172,s381,s48,s132,s1237,s56,s156,s167,s161,s176,s383,s1440,s268,s85,s86,s146,s228]) ).
cnf(s1464,plain,
( ~ spl0_23
| spl0_10
| ~ spl0_59 ),
inference(rat,[],[s471,s47,s49,s752,s858,s429,s176,s924,s968,s920,s962,s881]) ).
cnf(s1465,plain,
( ~ spl0_11
| ~ spl0_59
| spl0_3 ),
inference(rat,[],[s771,s61,s59,s27,s849,s51,s137,s779,s58,s50,s280,s354,s917,s888,s189,s925,s608,s316,s920,s951,s919,s734,s881,s562,s207,s319]) ).
cnf(s1466,plain,
( ~ spl0_59
| spl0_3 ),
inference(rat,[],[s49,s949,s471,s10,s50,s47,s1464,s200,s752,s46,s1465,s962,s951,s968,s176,s429,s189,s1003,s881,s919,s920,s924,s925,s1460]) ).
cnf(s1467,plain,
( spl0_9
| spl0_4
| spl0_3 ),
inference(rat,[],[s14,s266,s1138,s213,s46,s41,s172,s381,s48,s132,s1237,s56,s1447,s156,s167,s161,s176,s383,s1463,s268,s85,s86,s146,s228,s45,s1462,s1461,s1460,s1466]) ).
cnf(s1468,plain,
( spl0_4
| spl0_3 ),
inference(rat,[],[s1459,s219,s144,s293,s60,s57,s207,s155,s143,s209,s73,s84,s85,s86,s45,s1451,s1443,s140,s206,s420,s671,s1467,s1460,s1466]) ).
cnf(s1469,plain,
( ~ spl0_23
| ~ spl0_33
| ~ spl0_60
| spl0_3 ),
inference(rat,[],[s479,s51,s47,s28,s752,s70,s147,s102,s657,s488,s101]) ).
cnf(s1470,plain,
( ~ spl0_33
| ~ spl0_60
| spl0_3 ),
inference(rat,[],[s4,s1377,s46,s1469,s48,s166,s1460,s1468,s663,s103,s429,s102,s445,s80]) ).
cnf(s1471,plain,
( ~ spl0_60
| spl0_9
| spl0_3 ),
inference(rat,[],[s46,s299,s172,s48,s1237,s56,s1470,s419,s445,s429,s364,s663,s80,s102,s103,s1460,s1468]) ).
cnf(s1472,plain,
( spl0_9
| spl0_3 ),
inference(rat,[],[s46,s299,s172,s48,s1237,s56,s1447,s218,s156,s167,s161,s176,s1463,s73,s85,s86,s146,s45,s1471,s1461,s1460,s1466,s1468]) ).
cnf(s1473,plain,
( ~ spl0_60
| spl0_3 ),
inference(rat,[],[s748,s51,s50,s467,s760,s52,s209,s410,s412,s488,s225,s80,s81,s101,s103,s420,s1472]) ).
cnf(s1474,plain,
spl0_3,
inference(rat,[],[s1459,s219,s144,s293,s60,s57,s207,s155,s143,s209,s73,s84,s85,s86,s45,s1473,s1443,s140,s206,s1472,s1466]) ).
cnf(s1475,plain,
~ spl0_101,
inference(rat,[],[s1079,s1474]) ).
cnf(s1477,plain,
~ spl0_77,
inference(rat,[],[s797,s1474]) ).
cnf(s1478,plain,
~ spl0_89,
inference(rat,[],[s478,s1474]) ).
cnf(s1479,plain,
~ spl0_61,
inference(rat,[],[s310,s1474]) ).
cnf(s1480,plain,
~ spl0_73,
inference(rat,[],[s309,s1474]) ).
cnf(s1481,plain,
~ spl0_58,
inference(rat,[],[s112,s1474]) ).
cnf(s1483,plain,
( ~ spl0_60
| spl0_75 ),
inference(rat,[],[s760,s52,s50,s209,s410,s412,s80,s81,s1477,s1480]) ).
cnf(s1484,plain,
( ~ spl0_59
| spl0_75 ),
inference(rat,[],[s7,s1357,s1387,s59,s50,s207,s951,s608,s319,s919,s920,s1474,s1475,s1480]) ).
cnf(s1485,plain,
~ spl0_57,
inference(rat,[],[s61,s599,s178,s59,s57,s25,s140,s218,s636,s962,s444,s657,s1461,s320,s324,s495,s531,s532,s1475,s1474]) ).
cnf(s1486,plain,
( ~ spl0_60
| spl0_1 ),
inference(rat,[],[s55,s882,s143,s608,s1483,s72,s101,s1478,s1474]) ).
cnf(s1487,plain,
~ spl0_59,
inference(rat,[],[s751,s46,s47,s222,s850,s58,s59,s198,s354,s207,s562,s608,s968,s888,s1003,s1484,s319,s920,s925,s1479,s1475]) ).
cnf(s1488,plain,
spl0_60,
inference(rat,[],[s45,s1481,s1485,s1487]) ).
cnf(s1497,plain,
spl0_75,
inference(rat,[],[s1483,s1488]) ).
cnf(s1498,plain,
spl0_1,
inference(rat,[],[s1486,s1488]) ).
cnf(s1537,plain,
spl0_2,
inference(rat,[],[s755,s1474,s1497]) ).
cnf(s1538,plain,
$false,
inference(rat,[],[s1,s1474,s1498,s1537]) ).
fof(f3884,plain,
$false,
inference(avatar_sat_refutation,[],[s1538]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG024+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.17 % Computer : n020.cluster.edu
% 0.07/0.17 % Model : x86_64 x86_64
% 0.07/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.17 % Memory : 8046.5625MB
% 0.07/0.17 % OS : Linux 6.8.0-71-generic
% 0.07/0.17 % CPULimit : 300
% 0.07/0.17 % WCLimit : 300
% 0.07/0.17 % DateTime : Mon Sep 28 19:19:50 UTC 2026
% 0.07/0.17 % CPUTime :
% 0.07/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20 Running first-order model finding
% 0.07/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.30 % (447457)Will run a generic schedule for satisfiability detection.
% 0.42/0.30 % (447462)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4240643448_2999 on theBenchmark for (2999ds/0Mi)
% 0.42/0.30 % (447468)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4167532144:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.42/0.30 % (447465)dis+10_1_sil=32000:sp=arity:random_seed=2466313315:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.42/0.30 % (447463)% WARNING: option uhcvi not known.
% 0.42/0.30 % (447464)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2688048548:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.42/0.30 % (447466)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=469687454:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.42/0.30 % (447467)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=174413829:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.42/0.30 % (447463)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=785193271:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.42/0.30 % Detected minimum model sizes of [4]
% 0.42/0.30 % Detected maximum model sizes of [max]
% 0.42/0.30 % TRYING [4]
% 0.42/0.30 % TRYING [5]
% 0.42/0.30 % (447463) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-447457-447463"...
% 0.42/0.30 % (447465)Instruction limit reached!
% 0.42/0.30 % (447465)------------------------------
% 0.42/0.30 % (447465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.30 % (447465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.30 % (447465)CaDiCaL version: 2.1.3
% 0.42/0.30 % (447465)Termination reason: Instruction limit
% 0.42/0.30 % (447465)Termination phase: Saturation
% 0.42/0.30 % (447465)Time elapsed: 0.051 s
% 0.42/0.30 % (447465)Peak memory usage: 12 MB
% 0.42/0.30 % (447465)Instructions burned: 103 (million)
% 0.42/0.30 % (447463)...printing done.
% 0.42/0.30 % (447463)Refutation found. Thanks to Tanya!
% 0.42/0.30 % SZS status Unsatisfiable for theBenchmark
% 0.42/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.42/0.31 % (447463)------------------------------
% 0.42/0.31 % (447463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.42/0.31 % (447463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.42/0.31 % (447463)CaDiCaL version: 2.1.3
% 0.42/0.31 % (447463)Termination reason: Refutation
% 0.42/0.31 % (447463)Time elapsed: 0.052 s
% 0.42/0.31 % (447463)Peak memory usage: 13 MB
% 0.42/0.31 % (447463)Instructions burned: 177 (million)
% 0.42/0.31 % (447457)Success in time 0.092 s
% 0.42/0.31 % Vampire exiting
%------------------------------------------------------------------------------