%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG141+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:13:42 AM UTC 2026
% Result : Unsatisfiable 5.60s 1.60s
% Output : Refutation 7.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,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',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op(op(e0,e0),op(e0,e0)) = e0
& op(op(e0,e1),op(e0,e1)) = e1
& op(op(e0,e2),op(e0,e2)) = e2
& op(op(e0,e3),op(e0,e3)) = e3 )
| ( op(op(e1,e0),op(e1,e0)) = e0
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e1,e2),op(e1,e2)) = e2
& op(op(e1,e3),op(e1,e3)) = e3 )
| ( op(op(e2,e0),op(e2,e0)) = e0
& op(op(e2,e1),op(e2,e1)) = e1
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e2,e3),op(e2,e3)) = e3 )
| ( op(op(e3,e0),op(e3,e0)) = e0
& op(op(e3,e1),op(e3,e1)) = e1
& op(op(e3,e2),op(e3,e2)) = e2
& op(op(e3,e3),op(e3,e3)) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f10,axiom,
~ ( e0 = op(e2,op(e2,e2))
& e3 = op(e2,e2)
& e1 = op(op(e2,op(e2,e2)),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(e1,op(e1,e1))
& e3 = op(e1,e1)
& e2 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e1 = op(e3,op(e3,e3))
& e0 = op(e3,e3)
& e2 = op(op(e3,op(e3,e3)),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f14,axiom,
~ ( e1 = op(e3,op(e3,e3))
& e2 = op(e3,e3)
& e0 = op(op(e3,op(e3,e3)),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f16,axiom,
~ ( e1 = op(e2,op(e2,e2))
& e3 = op(e2,e2)
& e0 = op(op(e2,op(e2,e2)),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e1 = op(e0,op(e0,e0))
& e3 = op(e0,e0)
& e2 = op(op(e0,op(e0,e0)),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f19,axiom,
~ ( e2 = op(e1,op(e1,e1))
& e0 = op(e1,e1)
& e3 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f22,axiom,
~ ( e2 = op(e1,op(e1,e1))
& e3 = op(e1,e1)
& e0 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(e0,op(e0,e0))
& e3 = op(e0,e0)
& e1 = op(op(e0,op(e0,e0)),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f25,axiom,
~ ( e3 = op(e1,op(e1,e1))
& e0 = op(e1,e1)
& e2 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f28,axiom,
~ ( e3 = op(e1,op(e1,e1))
& e2 = op(e1,e1)
& e0 = op(op(e1,op(e1,e1)),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f34,plain,
( e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e1 != op(op(e2,op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,plain,
( e1 != op(e3,op(e3,e3))
| e0 != op(e3,e3)
| e2 != op(op(e3,op(e3,e3)),e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f38,plain,
( e1 != op(e3,op(e3,e3))
| e2 != op(e3,e3)
| e0 != op(op(e3,op(e3,e3)),e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f40,plain,
( e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f41,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e2 != op(op(e0,op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f43,plain,
( e2 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e3 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f46,plain,
( e2 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( e2 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e1 != op(op(e0,op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f49,plain,
( e3 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f52,plain,
( e3 != op(e1,op(e1,e1))
| e2 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f54,definition,
( ( op(op(e3,e0),op(e3,e0)) = e0
& op(op(e3,e1),op(e3,e1)) = e1
& op(op(e3,e2),op(e3,e2)) = e2
& op(op(e3,e3),op(e3,e3)) = e3 )
| ~ sP0 ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f55,definition,
( ( op(op(e2,e0),op(e2,e0)) = e0
& op(op(e2,e1),op(e2,e1)) = e1
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e2,e3),op(e2,e3)) = e3 )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f56,definition,
( ( op(op(e1,e0),op(e1,e0)) = e0
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e1,e2),op(e1,e2)) = e2
& op(op(e1,e3),op(e1,e3)) = e3 )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f57,plain,
( ( op(op(e0,e0),op(e0,e0)) = e0
& op(op(e0,e1),op(e0,e1)) = e1
& op(op(e0,e2),op(e0,e2)) = e2
& op(op(e0,e3),op(e0,e3)) = e3 )
| sP2
| sP1
| sP0 ),
inference(definition_folding,[],[f5,f56,f55,f54]) ).
fof(f58,plain,
( ( op(op(e1,e0),op(e1,e0)) = e0
& op(op(e1,e1),op(e1,e1)) = e1
& op(op(e1,e2),op(e1,e2)) = e2
& op(op(e1,e3),op(e1,e3)) = e3 )
| ~ sP2 ),
inference(nnf_transformation,[],[f56]) ).
fof(f59,plain,
( ( op(op(e2,e0),op(e2,e0)) = e0
& op(op(e2,e1),op(e2,e1)) = e1
& op(op(e2,e2),op(e2,e2)) = e2
& op(op(e2,e3),op(e2,e3)) = e3 )
| ~ sP1 ),
inference(nnf_transformation,[],[f55]) ).
fof(f60,plain,
( ( op(op(e3,e0),op(e3,e0)) = e0
& op(op(e3,e1),op(e3,e1)) = e1
& op(op(e3,e2),op(e3,e2)) = e2
& op(op(e3,e3),op(e3,e3)) = e3 )
| ~ sP0 ),
inference(nnf_transformation,[],[f54]) ).
fof(f62,plain,
( e0 = op(e3,e2)
| e1 = op(e3,e2)
| e2 = op(e3,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e0 = op(e3,e1)
| e1 = op(e3,e1)
| e2 = op(e3,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e0 = op(e3,e0)
| e1 = op(e3,e0)
| e2 = op(e3,e0)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f65,plain,
( e0 = op(e2,e3)
| e1 = op(e2,e3)
| e2 = op(e2,e3)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e0 = op(e2,e2)
| e1 = op(e2,e2)
| e2 = op(e2,e2)
| e3 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e0 = op(e2,e1)
| e1 = op(e2,e1)
| e2 = op(e2,e1)
| e3 = op(e2,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e0 = op(e2,e0)
| e1 = op(e2,e0)
| e2 = op(e2,e0)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
( e0 = op(e1,e3)
| e1 = op(e1,e3)
| e2 = op(e1,e3)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f70,plain,
( e0 = op(e1,e2)
| e1 = op(e1,e2)
| e2 = op(e1,e2)
| e3 = op(e1,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
( e0 = op(e1,e1)
| e1 = op(e1,e1)
| e2 = op(e1,e1)
| e3 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f72,plain,
( e0 = op(e1,e0)
| e1 = op(e1,e0)
| e2 = op(e1,e0)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f73,plain,
( e0 = op(e0,e3)
| e1 = op(e0,e3)
| e2 = op(e0,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f74,plain,
( e0 = op(e0,e2)
| e1 = op(e0,e2)
| e2 = op(e0,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f75,plain,
( e0 = op(e0,e1)
| e1 = op(e0,e1)
| e2 = op(e0,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f76,plain,
( e0 = op(e0,e0)
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f1]) ).
fof(f77,plain,
( e3 = op(e0,e3)
| e3 = op(e1,e3)
| e3 = op(e2,e3)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
( e3 = op(e3,e0)
| e3 = op(e3,e1)
| e3 = op(e3,e2)
| e3 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
( e2 = op(e0,e3)
| e2 = op(e1,e3)
| e2 = op(e2,e3)
| e2 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e1 = op(e3,e0)
| e1 = op(e3,e1)
| e1 = op(e3,e2)
| e1 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
( e0 = op(e3,e0)
| e0 = op(e3,e1)
| e0 = op(e3,e2)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e3 = op(e0,e2)
| e3 = op(e1,e2)
| e3 = op(e2,e2)
| e3 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e3 = op(e2,e0)
| e3 = op(e2,e1)
| e3 = op(e2,e2)
| e3 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e0 = op(e0,e2)
| e0 = op(e1,e2)
| e0 = op(e2,e2)
| e0 = op(e3,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e0 = op(e2,e0)
| e0 = op(e2,e1)
| e0 = op(e2,e2)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e3 = op(e0,e1)
| e3 = op(e1,e1)
| e3 = op(e2,e1)
| e3 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e3 = op(e1,e0)
| e3 = op(e1,e1)
| e3 = op(e1,e2)
| e3 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
( e2 = op(e0,e1)
| e2 = op(e1,e1)
| e2 = op(e2,e1)
| e2 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
( e2 = op(e1,e0)
| e2 = op(e1,e1)
| e2 = op(e1,e2)
| e2 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
( e1 = op(e1,e0)
| e1 = op(e1,e1)
| e1 = op(e1,e2)
| e1 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e0 = op(e0,e1)
| e0 = op(e1,e1)
| e0 = op(e2,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e0 = op(e1,e0)
| e0 = op(e1,e1)
| e0 = op(e1,e2)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f102,plain,
( op(e0,e0) = e3
| e3 = op(e0,e1)
| e3 = op(e0,e2)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f103,plain,
( op(e0,e0) = e2
| e2 = op(e1,e0)
| e2 = op(e2,e0)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f104,plain,
( op(e0,e0) = e2
| e2 = op(e0,e1)
| e2 = op(e0,e2)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f106,plain,
( op(e0,e0) = e1
| e1 = op(e0,e1)
| e1 = op(e0,e2)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f107,plain,
( e0 = op(e0,e0)
| e0 = op(e1,e0)
| e0 = op(e2,e0)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
( e0 = op(e0,e0)
| e0 = op(e0,e1)
| e0 = op(e0,e2)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f113,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f118,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f120,plain,
op(e2,e0) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f122,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f124,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f126,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f129,plain,
op(e0,e1) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f130,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f131,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f132,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f133,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e0,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f142,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f147,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e0,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f151,plain,
op(e2,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f152,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f153,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f154,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f155,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f156,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f157,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f158,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f159,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f160,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f161,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f162,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f163,plain,
( e3 = op(op(e1,e3),op(e1,e3))
| ~ sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f164,plain,
( e2 = op(op(e1,e2),op(e1,e2))
| ~ sP2 ),
inference(cnf_transformation,[],[f58]) ).
fof(f167,plain,
( e3 = op(op(e2,e3),op(e2,e3))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f168,plain,
( e2 = op(op(e2,e2),op(e2,e2))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f169,plain,
( e1 = op(op(e2,e1),op(e2,e1))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f170,plain,
( e0 = op(op(e2,e0),op(e2,e0))
| ~ sP1 ),
inference(cnf_transformation,[],[f59]) ).
fof(f171,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f172,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f173,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f174,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| ~ sP0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f175,plain,
( e3 = op(op(e0,e3),op(e0,e3))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f176,plain,
( e2 = op(op(e0,e2),op(e0,e2))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f177,plain,
( e1 = op(op(e0,e1),op(e0,e1))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f178,plain,
( e0 = op(op(e0,e0),op(e0,e0))
| sP2
| sP1
| sP0 ),
inference(cnf_transformation,[],[f57]) ).
fof(f183,plain,
( e0 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e1 != op(op(e2,op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f184,plain,
( e0 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f185,plain,
( e1 != op(e3,op(e3,e3))
| e0 != op(e3,e3)
| e2 != op(op(e3,op(e3,e3)),e3) ),
inference(cnf_transformation,[],[f36]) ).
fof(f187,plain,
( e1 != op(e3,op(e3,e3))
| e2 != op(e3,e3)
| e0 != op(op(e3,op(e3,e3)),e3) ),
inference(cnf_transformation,[],[f38]) ).
fof(f189,plain,
( e1 != op(e2,op(e2,e2))
| e3 != op(e2,e2)
| e0 != op(op(e2,op(e2,e2)),e2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f190,plain,
( e1 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e2 != op(op(e0,op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f41]) ).
fof(f192,plain,
( e2 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e3 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f195,plain,
( e2 != op(e1,op(e1,e1))
| e3 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f196,plain,
( e2 != op(e0,op(e0,e0))
| op(e0,e0) != e3
| e1 != op(op(e0,op(e0,e0)),e0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f198,plain,
( e3 != op(e1,op(e1,e1))
| e0 != op(e1,e1)
| e2 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f201,plain,
( e3 != op(e1,op(e1,e1))
| e2 != op(e1,e1)
| e0 != op(op(e1,op(e1,e1)),e1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f204,definition,
( spl3_1
<=> e1 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl3_1])],[avatar_definition]) ).
fof(f206,plain,
( e1 != op(op(e0,op(e0,e0)),e0)
| spl3_1 ),
inference(avatar_component_clause,[],[f204]) ).
fof(f208,definition,
( spl3_2
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f209,plain,
( op(e0,e0) = e2
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( op(e0,e0) != e2
| spl3_2 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f212,definition,
( spl3_3
<=> e3 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f213,plain,
( e3 = op(e0,op(e0,e0))
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f214,plain,
( e3 != op(e0,op(e0,e0))
| spl3_3 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f217,definition,
( spl3_4
<=> e0 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f218,plain,
( e0 = op(op(e1,op(e1,e1)),e1)
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f219,plain,
( e0 != op(op(e1,op(e1,e1)),e1)
| spl3_4 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f221,definition,
( spl3_5
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f222,plain,
( e2 = op(e1,e1)
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f223,plain,
( e2 != op(e1,e1)
| spl3_5 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f225,definition,
( spl3_6
<=> e3 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_6])],[avatar_definition]) ).
fof(f226,plain,
( e3 = op(e1,op(e1,e1))
| ~ spl3_6 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( e3 != op(e1,op(e1,e1))
| spl3_6 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,plain,
( ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(avatar_split_clause,[],[f201,f225,f221,f217]) ).
fof(f230,definition,
( spl3_7
<=> e2 = op(op(e0,op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl3_7])],[avatar_definition]) ).
fof(f232,plain,
( e2 != op(op(e0,op(e0,e0)),e0)
| spl3_7 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f234,definition,
( spl3_8
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl3_8])],[avatar_definition]) ).
fof(f235,plain,
( op(e0,e0) = e1
| ~ spl3_8 ),
inference(avatar_component_clause,[],[f234]) ).
fof(f239,definition,
( spl3_9
<=> e0 = op(op(e2,op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl3_9])],[avatar_definition]) ).
fof(f241,plain,
( e0 != op(op(e2,op(e2,e2)),e2)
| spl3_9 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f243,definition,
( spl3_10
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_10])],[avatar_definition]) ).
fof(f244,plain,
( e1 = op(e2,e2)
| ~ spl3_10 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f252,definition,
( spl3_12
<=> e2 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl3_12])],[avatar_definition]) ).
fof(f253,plain,
( e2 = op(op(e1,op(e1,e1)),e1)
| ~ spl3_12 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( e2 != op(op(e1,op(e1,e1)),e1)
| spl3_12 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f256,definition,
( spl3_13
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_13])],[avatar_definition]) ).
fof(f257,plain,
( e0 = op(e1,e1)
| ~ spl3_13 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f258,plain,
( e0 != op(e1,e1)
| spl3_13 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f259,plain,
( ~ spl3_12
| ~ spl3_13
| ~ spl3_6 ),
inference(avatar_split_clause,[],[f198,f225,f256,f252]) ).
fof(f261,definition,
( spl3_14
<=> e1 = op(op(e2,op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl3_14])],[avatar_definition]) ).
fof(f263,plain,
( e1 != op(op(e2,op(e2,e2)),e2)
| spl3_14 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f265,definition,
( spl3_15
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f266,plain,
( e0 = op(e2,e2)
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f270,definition,
( spl3_16
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl3_16])],[avatar_definition]) ).
fof(f271,plain,
( op(e0,e0) = e3
| ~ spl3_16 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f274,definition,
( spl3_17
<=> e2 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_17])],[avatar_definition]) ).
fof(f275,plain,
( e2 = op(e0,op(e0,e0))
| ~ spl3_17 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f276,plain,
( e2 != op(e0,op(e0,e0))
| spl3_17 ),
inference(avatar_component_clause,[],[f274]) ).
fof(f277,plain,
( ~ spl3_1
| ~ spl3_16
| ~ spl3_17 ),
inference(avatar_split_clause,[],[f196,f274,f270,f204]) ).
fof(f279,definition,
( spl3_18
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_18])],[avatar_definition]) ).
fof(f280,plain,
( e3 = op(e1,e1)
| ~ spl3_18 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f281,plain,
( e3 != op(e1,e1)
| spl3_18 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f283,definition,
( spl3_19
<=> e2 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_19])],[avatar_definition]) ).
fof(f284,plain,
( e2 = op(e1,op(e1,e1))
| ~ spl3_19 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f285,plain,
( e2 != op(e1,op(e1,e1))
| spl3_19 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( ~ spl3_4
| ~ spl3_18
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f195,f283,f279,f217]) ).
fof(f293,definition,
( spl3_21
<=> e0 = op(op(e3,op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl3_21])],[avatar_definition]) ).
fof(f295,plain,
( e0 != op(op(e3,op(e3,e3)),e3)
| spl3_21 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl3_22
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_22])],[avatar_definition]) ).
fof(f298,plain,
( e1 = op(e3,e3)
| ~ spl3_22 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f299,plain,
( e1 != op(e3,e3)
| spl3_22 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f306,definition,
( spl3_24
<=> e3 = op(op(e1,op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl3_24])],[avatar_definition]) ).
fof(f308,plain,
( e3 != op(op(e1,op(e1,e1)),e1)
| spl3_24 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
( ~ spl3_24
| ~ spl3_13
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f192,f283,f256,f306]) ).
fof(f315,definition,
( spl3_26
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_26])],[avatar_definition]) ).
fof(f316,plain,
( e0 = op(e3,e3)
| ~ spl3_26 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f317,plain,
( e0 != op(e3,e3)
| spl3_26 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f320,definition,
( spl3_27
<=> e1 = op(e0,op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_27])],[avatar_definition]) ).
fof(f321,plain,
( e1 = op(e0,op(e0,e0))
| ~ spl3_27 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( e1 != op(e0,op(e0,e0))
| spl3_27 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f323,plain,
( ~ spl3_7
| ~ spl3_16
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f190,f320,f270,f230]) ).
fof(f325,definition,
( spl3_28
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_28])],[avatar_definition]) ).
fof(f326,plain,
( e3 = op(e2,e2)
| ~ spl3_28 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f327,plain,
( e3 != op(e2,e2)
| spl3_28 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f329,definition,
( spl3_29
<=> e1 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_29])],[avatar_definition]) ).
fof(f330,plain,
( e1 = op(e2,op(e2,e2))
| ~ spl3_29 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f331,plain,
( e1 != op(e2,op(e2,e2))
| spl3_29 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( ~ spl3_9
| ~ spl3_28
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f189,f329,f325,f239]) ).
fof(f335,definition,
( spl3_30
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_30])],[avatar_definition]) ).
fof(f336,plain,
( e2 = op(e3,e3)
| ~ spl3_30 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( e2 != op(e3,e3)
| spl3_30 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f339,definition,
( spl3_31
<=> e1 = op(e3,op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_31])],[avatar_definition]) ).
fof(f340,plain,
( e1 = op(e3,op(e3,e3))
| ~ spl3_31 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f341,plain,
( e1 != op(e3,op(e3,e3))
| spl3_31 ),
inference(avatar_component_clause,[],[f339]) ).
fof(f342,plain,
( ~ spl3_21
| ~ spl3_30
| ~ spl3_31 ),
inference(avatar_split_clause,[],[f187,f339,f335,f293]) ).
fof(f349,definition,
( spl3_33
<=> e2 = op(op(e3,op(e3,e3)),e3) ),
introduced(definition,[new_symbols(definition,[spl3_33])],[avatar_definition]) ).
fof(f351,plain,
( e2 != op(op(e3,op(e3,e3)),e3)
| spl3_33 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f352,plain,
( ~ spl3_33
| ~ spl3_26
| ~ spl3_31 ),
inference(avatar_split_clause,[],[f185,f339,f315,f349]) ).
fof(f354,definition,
( spl3_34
<=> e0 = op(e1,op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_34])],[avatar_definition]) ).
fof(f355,plain,
( e0 = op(e1,op(e1,e1))
| ~ spl3_34 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( e0 != op(e1,op(e1,e1))
| spl3_34 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f357,plain,
( ~ spl3_12
| ~ spl3_18
| ~ spl3_34 ),
inference(avatar_split_clause,[],[f184,f354,f279,f252]) ).
fof(f359,definition,
( spl3_35
<=> e0 = op(e2,op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_35])],[avatar_definition]) ).
fof(f360,plain,
( e0 = op(e2,op(e2,e2))
| ~ spl3_35 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f361,plain,
( e0 != op(e2,op(e2,e2))
| spl3_35 ),
inference(avatar_component_clause,[],[f359]) ).
fof(f362,plain,
( ~ spl3_14
| ~ spl3_28
| ~ spl3_35 ),
inference(avatar_split_clause,[],[f183,f359,f325,f261]) ).
fof(f372,definition,
( spl3_37
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl3_37])],[avatar_definition]) ).
fof(f376,definition,
( spl3_38
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl3_38])],[avatar_definition]) ).
fof(f380,definition,
( spl3_39
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl3_39])],[avatar_definition]) ).
fof(f384,definition,
( spl3_40
<=> e3 = op(op(e0,e3),op(e0,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_40])],[avatar_definition]) ).
fof(f386,plain,
( e3 = op(op(e0,e3),op(e0,e3))
| ~ spl3_40 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f387,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_40 ),
inference(avatar_split_clause,[],[f175,f384,f380,f376,f372]) ).
fof(f389,definition,
( spl3_41
<=> e2 = op(op(e0,e2),op(e0,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_41])],[avatar_definition]) ).
fof(f391,plain,
( e2 = op(op(e0,e2),op(e0,e2))
| ~ spl3_41 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_41 ),
inference(avatar_split_clause,[],[f176,f389,f380,f376,f372]) ).
fof(f394,definition,
( spl3_42
<=> e1 = op(op(e0,e1),op(e0,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_42])],[avatar_definition]) ).
fof(f396,plain,
( e1 = op(op(e0,e1),op(e0,e1))
| ~ spl3_42 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_42 ),
inference(avatar_split_clause,[],[f177,f394,f380,f376,f372]) ).
fof(f399,definition,
( spl3_43
<=> e0 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_43])],[avatar_definition]) ).
fof(f400,plain,
( e0 != op(op(e0,e0),op(e0,e0))
| spl3_43 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f401,plain,
( e0 = op(op(e0,e0),op(e0,e0))
| ~ spl3_43 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_43 ),
inference(avatar_split_clause,[],[f178,f399,f380,f376,f372]) ).
fof(f404,definition,
( spl3_44
<=> e3 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_44])],[avatar_definition]) ).
fof(f405,plain,
( e3 != op(op(e3,e3),op(e3,e3))
| spl3_44 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f406,plain,
( e3 = op(op(e3,e3),op(e3,e3))
| ~ spl3_44 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,plain,
( ~ spl3_37
| spl3_44 ),
inference(avatar_split_clause,[],[f171,f404,f372]) ).
fof(f409,definition,
( spl3_45
<=> e2 = op(op(e3,e2),op(e3,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_45])],[avatar_definition]) ).
fof(f411,plain,
( e2 = op(op(e3,e2),op(e3,e2))
| ~ spl3_45 ),
inference(avatar_component_clause,[],[f409]) ).
fof(f412,plain,
( ~ spl3_37
| spl3_45 ),
inference(avatar_split_clause,[],[f172,f409,f372]) ).
fof(f414,definition,
( spl3_46
<=> e1 = op(op(e3,e1),op(e3,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_46])],[avatar_definition]) ).
fof(f416,plain,
( e1 = op(op(e3,e1),op(e3,e1))
| ~ spl3_46 ),
inference(avatar_component_clause,[],[f414]) ).
fof(f417,plain,
( ~ spl3_37
| spl3_46 ),
inference(avatar_split_clause,[],[f173,f414,f372]) ).
fof(f419,definition,
( spl3_47
<=> e0 = op(op(e3,e0),op(e3,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_47])],[avatar_definition]) ).
fof(f421,plain,
( e0 = op(op(e3,e0),op(e3,e0))
| ~ spl3_47 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( ~ spl3_37
| spl3_47 ),
inference(avatar_split_clause,[],[f174,f419,f372]) ).
fof(f424,definition,
( spl3_48
<=> e3 = op(op(e2,e3),op(e2,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_48])],[avatar_definition]) ).
fof(f426,plain,
( e3 = op(op(e2,e3),op(e2,e3))
| ~ spl3_48 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f427,plain,
( ~ spl3_38
| spl3_48 ),
inference(avatar_split_clause,[],[f167,f424,f376]) ).
fof(f429,definition,
( spl3_49
<=> e2 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_49])],[avatar_definition]) ).
fof(f430,plain,
( e2 != op(op(e2,e2),op(e2,e2))
| spl3_49 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f431,plain,
( e2 = op(op(e2,e2),op(e2,e2))
| ~ spl3_49 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f432,plain,
( ~ spl3_38
| spl3_49 ),
inference(avatar_split_clause,[],[f168,f429,f376]) ).
fof(f434,definition,
( spl3_50
<=> e1 = op(op(e2,e1),op(e2,e1)) ),
introduced(definition,[new_symbols(definition,[spl3_50])],[avatar_definition]) ).
fof(f436,plain,
( e1 = op(op(e2,e1),op(e2,e1))
| ~ spl3_50 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f437,plain,
( ~ spl3_38
| spl3_50 ),
inference(avatar_split_clause,[],[f169,f434,f376]) ).
fof(f439,definition,
( spl3_51
<=> e0 = op(op(e2,e0),op(e2,e0)) ),
introduced(definition,[new_symbols(definition,[spl3_51])],[avatar_definition]) ).
fof(f441,plain,
( e0 = op(op(e2,e0),op(e2,e0))
| ~ spl3_51 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f442,plain,
( ~ spl3_38
| spl3_51 ),
inference(avatar_split_clause,[],[f170,f439,f376]) ).
fof(f444,definition,
( spl3_52
<=> e3 = op(op(e1,e3),op(e1,e3)) ),
introduced(definition,[new_symbols(definition,[spl3_52])],[avatar_definition]) ).
fof(f446,plain,
( e3 = op(op(e1,e3),op(e1,e3))
| ~ spl3_52 ),
inference(avatar_component_clause,[],[f444]) ).
fof(f447,plain,
( ~ spl3_39
| spl3_52 ),
inference(avatar_split_clause,[],[f163,f444,f380]) ).
fof(f449,definition,
( spl3_53
<=> e2 = op(op(e1,e2),op(e1,e2)) ),
introduced(definition,[new_symbols(definition,[spl3_53])],[avatar_definition]) ).
fof(f451,plain,
( e2 = op(op(e1,e2),op(e1,e2))
| ~ spl3_53 ),
inference(avatar_component_clause,[],[f449]) ).
fof(f452,plain,
( ~ spl3_39
| spl3_53 ),
inference(avatar_split_clause,[],[f164,f449,f380]) ).
fof(f464,definition,
( spl3_56
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl3_56])],[avatar_definition]) ).
fof(f465,plain,
( e3 != op(e3,e3)
| spl3_56 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f466,plain,
( e3 = op(e3,e3)
| ~ spl3_56 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f468,definition,
( spl3_57
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_57])],[avatar_definition]) ).
fof(f470,plain,
( e3 = op(e2,e3)
| ~ spl3_57 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f472,definition,
( spl3_58
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_58])],[avatar_definition]) ).
fof(f473,plain,
( e3 != op(e1,e3)
| spl3_58 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f474,plain,
( e3 = op(e1,e3)
| ~ spl3_58 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f476,definition,
( spl3_59
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_59])],[avatar_definition]) ).
fof(f478,plain,
( e3 = op(e0,e3)
| ~ spl3_59 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f479,plain,
( spl3_56
| spl3_57
| spl3_58
| spl3_59 ),
inference(avatar_split_clause,[],[f77,f476,f472,f468,f464]) ).
fof(f481,definition,
( spl3_60
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_60])],[avatar_definition]) ).
fof(f483,plain,
( e3 = op(e3,e2)
| ~ spl3_60 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f485,definition,
( spl3_61
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_61])],[avatar_definition]) ).
fof(f487,plain,
( e3 = op(e3,e1)
| ~ spl3_61 ),
inference(avatar_component_clause,[],[f485]) ).
fof(f489,definition,
( spl3_62
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_62])],[avatar_definition]) ).
fof(f491,plain,
( e3 = op(e3,e0)
| ~ spl3_62 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f492,plain,
( spl3_56
| spl3_60
| spl3_61
| spl3_62 ),
inference(avatar_split_clause,[],[f78,f489,f485,f481,f464]) ).
fof(f494,definition,
( spl3_63
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_63])],[avatar_definition]) ).
fof(f496,plain,
( e2 = op(e2,e3)
| ~ spl3_63 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f498,definition,
( spl3_64
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_64])],[avatar_definition]) ).
fof(f500,plain,
( e2 = op(e1,e3)
| ~ spl3_64 ),
inference(avatar_component_clause,[],[f498]) ).
fof(f502,definition,
( spl3_65
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_65])],[avatar_definition]) ).
fof(f504,plain,
( e2 = op(e0,e3)
| ~ spl3_65 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f505,plain,
( spl3_30
| spl3_63
| spl3_64
| spl3_65 ),
inference(avatar_split_clause,[],[f79,f502,f498,f494,f335]) ).
fof(f507,definition,
( spl3_66
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_66])],[avatar_definition]) ).
fof(f509,plain,
( e2 = op(e3,e2)
| ~ spl3_66 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f511,definition,
( spl3_67
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_67])],[avatar_definition]) ).
fof(f513,plain,
( e2 = op(e3,e1)
| ~ spl3_67 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f515,definition,
( spl3_68
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_68])],[avatar_definition]) ).
fof(f517,plain,
( e2 = op(e3,e0)
| ~ spl3_68 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f520,definition,
( spl3_69
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_69])],[avatar_definition]) ).
fof(f522,plain,
( e1 = op(e2,e3)
| ~ spl3_69 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f524,definition,
( spl3_70
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_70])],[avatar_definition]) ).
fof(f526,plain,
( e1 = op(e1,e3)
| ~ spl3_70 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f528,definition,
( spl3_71
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition]) ).
fof(f530,plain,
( e1 = op(e0,e3)
| ~ spl3_71 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f533,definition,
( spl3_72
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_72])],[avatar_definition]) ).
fof(f535,plain,
( e1 = op(e3,e2)
| ~ spl3_72 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f537,definition,
( spl3_73
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_73])],[avatar_definition]) ).
fof(f539,plain,
( e1 = op(e3,e1)
| ~ spl3_73 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f541,definition,
( spl3_74
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_74])],[avatar_definition]) ).
fof(f543,plain,
( e1 = op(e3,e0)
| ~ spl3_74 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f544,plain,
( spl3_22
| spl3_72
| spl3_73
| spl3_74 ),
inference(avatar_split_clause,[],[f82,f541,f537,f533,f297]) ).
fof(f546,definition,
( spl3_75
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl3_75])],[avatar_definition]) ).
fof(f548,plain,
( e0 = op(e2,e3)
| ~ spl3_75 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f550,definition,
( spl3_76
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl3_76])],[avatar_definition]) ).
fof(f552,plain,
( e0 = op(e1,e3)
| ~ spl3_76 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f554,definition,
( spl3_77
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl3_77])],[avatar_definition]) ).
fof(f556,plain,
( e0 = op(e0,e3)
| ~ spl3_77 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f559,definition,
( spl3_78
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl3_78])],[avatar_definition]) ).
fof(f561,plain,
( e0 = op(e3,e2)
| ~ spl3_78 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f563,definition,
( spl3_79
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl3_79])],[avatar_definition]) ).
fof(f565,plain,
( e0 = op(e3,e1)
| ~ spl3_79 ),
inference(avatar_component_clause,[],[f563]) ).
fof(f567,definition,
( spl3_80
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl3_80])],[avatar_definition]) ).
fof(f569,plain,
( e0 = op(e3,e0)
| ~ spl3_80 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f570,plain,
( spl3_26
| spl3_78
| spl3_79
| spl3_80 ),
inference(avatar_split_clause,[],[f84,f567,f563,f559,f315]) ).
fof(f572,definition,
( spl3_81
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_81])],[avatar_definition]) ).
fof(f574,plain,
( e3 = op(e1,e2)
| ~ spl3_81 ),
inference(avatar_component_clause,[],[f572]) ).
fof(f576,definition,
( spl3_82
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_82])],[avatar_definition]) ).
fof(f578,plain,
( e3 = op(e0,e2)
| ~ spl3_82 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f579,plain,
( spl3_60
| spl3_28
| spl3_81
| spl3_82 ),
inference(avatar_split_clause,[],[f85,f576,f572,f325,f481]) ).
fof(f581,definition,
( spl3_83
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_83])],[avatar_definition]) ).
fof(f583,plain,
( e3 = op(e2,e1)
| ~ spl3_83 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f585,definition,
( spl3_84
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_84])],[avatar_definition]) ).
fof(f587,plain,
( e3 = op(e2,e0)
| ~ spl3_84 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,plain,
( spl3_57
| spl3_28
| spl3_83
| spl3_84 ),
inference(avatar_split_clause,[],[f86,f585,f581,f325,f468]) ).
fof(f590,definition,
( spl3_85
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl3_85])],[avatar_definition]) ).
fof(f591,plain,
( e2 != op(e2,e2)
| spl3_85 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f592,plain,
( e2 = op(e2,e2)
| ~ spl3_85 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f594,definition,
( spl3_86
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_86])],[avatar_definition]) ).
fof(f595,plain,
( e2 != op(e1,e2)
| spl3_86 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f596,plain,
( e2 = op(e1,e2)
| ~ spl3_86 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f598,definition,
( spl3_87
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_87])],[avatar_definition]) ).
fof(f600,plain,
( e2 = op(e0,e2)
| ~ spl3_87 ),
inference(avatar_component_clause,[],[f598]) ).
fof(f603,definition,
( spl3_88
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_88])],[avatar_definition]) ).
fof(f605,plain,
( e2 = op(e2,e1)
| ~ spl3_88 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f607,definition,
( spl3_89
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_89])],[avatar_definition]) ).
fof(f609,plain,
( e2 = op(e2,e0)
| ~ spl3_89 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f612,definition,
( spl3_90
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_90])],[avatar_definition]) ).
fof(f614,plain,
( e1 = op(e1,e2)
| ~ spl3_90 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f616,definition,
( spl3_91
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_91])],[avatar_definition]) ).
fof(f618,plain,
( e1 = op(e0,e2)
| ~ spl3_91 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f621,definition,
( spl3_92
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_92])],[avatar_definition]) ).
fof(f623,plain,
( e1 = op(e2,e1)
| ~ spl3_92 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl3_93
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_93])],[avatar_definition]) ).
fof(f627,plain,
( e1 = op(e2,e0)
| ~ spl3_93 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f630,definition,
( spl3_94
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl3_94])],[avatar_definition]) ).
fof(f632,plain,
( e0 = op(e1,e2)
| ~ spl3_94 ),
inference(avatar_component_clause,[],[f630]) ).
fof(f634,definition,
( spl3_95
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl3_95])],[avatar_definition]) ).
fof(f636,plain,
( e0 = op(e0,e2)
| ~ spl3_95 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f637,plain,
( spl3_78
| spl3_15
| spl3_94
| spl3_95 ),
inference(avatar_split_clause,[],[f91,f634,f630,f265,f559]) ).
fof(f639,definition,
( spl3_96
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl3_96])],[avatar_definition]) ).
fof(f641,plain,
( e0 = op(e2,e1)
| ~ spl3_96 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f643,definition,
( spl3_97
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl3_97])],[avatar_definition]) ).
fof(f645,plain,
( e0 = op(e2,e0)
| ~ spl3_97 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,plain,
( spl3_75
| spl3_15
| spl3_96
| spl3_97 ),
inference(avatar_split_clause,[],[f92,f643,f639,f265,f546]) ).
fof(f648,definition,
( spl3_98
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_98])],[avatar_definition]) ).
fof(f649,plain,
( e3 != op(e0,e1)
| spl3_98 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f650,plain,
( e3 = op(e0,e1)
| ~ spl3_98 ),
inference(avatar_component_clause,[],[f648]) ).
fof(f651,plain,
( spl3_61
| spl3_83
| spl3_18
| spl3_98 ),
inference(avatar_split_clause,[],[f93,f648,f279,f581,f485]) ).
fof(f653,definition,
( spl3_99
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_99])],[avatar_definition]) ).
fof(f655,plain,
( e3 = op(e1,e0)
| ~ spl3_99 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f656,plain,
( spl3_58
| spl3_81
| spl3_18
| spl3_99 ),
inference(avatar_split_clause,[],[f94,f653,f279,f572,f472]) ).
fof(f658,definition,
( spl3_100
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_100])],[avatar_definition]) ).
fof(f660,plain,
( e2 = op(e0,e1)
| ~ spl3_100 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f661,plain,
( spl3_67
| spl3_88
| spl3_5
| spl3_100 ),
inference(avatar_split_clause,[],[f95,f658,f221,f603,f511]) ).
fof(f663,definition,
( spl3_101
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_101])],[avatar_definition]) ).
fof(f665,plain,
( e2 = op(e1,e0)
| ~ spl3_101 ),
inference(avatar_component_clause,[],[f663]) ).
fof(f666,plain,
( spl3_64
| spl3_86
| spl3_5
| spl3_101 ),
inference(avatar_split_clause,[],[f96,f663,f221,f594,f498]) ).
fof(f668,definition,
( spl3_102
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl3_102])],[avatar_definition]) ).
fof(f669,plain,
( e1 != op(e1,e1)
| spl3_102 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f670,plain,
( e1 = op(e1,e1)
| ~ spl3_102 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f672,definition,
( spl3_103
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_103])],[avatar_definition]) ).
fof(f674,plain,
( e1 = op(e0,e1)
| ~ spl3_103 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f677,definition,
( spl3_104
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_104])],[avatar_definition]) ).
fof(f679,plain,
( e1 = op(e1,e0)
| ~ spl3_104 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f680,plain,
( spl3_70
| spl3_90
| spl3_102
| spl3_104 ),
inference(avatar_split_clause,[],[f98,f677,f668,f612,f524]) ).
fof(f682,definition,
( spl3_105
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl3_105])],[avatar_definition]) ).
fof(f684,plain,
( e0 = op(e0,e1)
| ~ spl3_105 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f685,plain,
( spl3_79
| spl3_96
| spl3_13
| spl3_105 ),
inference(avatar_split_clause,[],[f99,f682,f256,f639,f563]) ).
fof(f687,definition,
( spl3_106
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl3_106])],[avatar_definition]) ).
fof(f689,plain,
( e0 = op(e1,e0)
| ~ spl3_106 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( spl3_76
| spl3_94
| spl3_13
| spl3_106 ),
inference(avatar_split_clause,[],[f100,f687,f256,f630,f550]) ).
fof(f692,plain,
( spl3_59
| spl3_82
| spl3_98
| spl3_16 ),
inference(avatar_split_clause,[],[f102,f270,f648,f576,f476]) ).
fof(f693,plain,
( spl3_68
| spl3_89
| spl3_101
| spl3_2 ),
inference(avatar_split_clause,[],[f103,f208,f663,f607,f515]) ).
fof(f694,plain,
( spl3_65
| spl3_87
| spl3_100
| spl3_2 ),
inference(avatar_split_clause,[],[f104,f208,f658,f598,f502]) ).
fof(f696,plain,
( spl3_71
| spl3_91
| spl3_103
| spl3_8 ),
inference(avatar_split_clause,[],[f106,f234,f672,f616,f528]) ).
fof(f698,definition,
( spl3_107
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl3_107])],[avatar_definition]) ).
fof(f699,plain,
( e0 != op(e0,e0)
| spl3_107 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f700,plain,
( e0 = op(e0,e0)
| ~ spl3_107 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f701,plain,
( spl3_80
| spl3_97
| spl3_106
| spl3_107 ),
inference(avatar_split_clause,[],[f107,f698,f687,f643,f567]) ).
fof(f702,plain,
( spl3_77
| spl3_95
| spl3_105
| spl3_107 ),
inference(avatar_split_clause,[],[f108,f698,f682,f634,f554]) ).
fof(f704,plain,
( spl3_60
| spl3_66
| spl3_72
| spl3_78 ),
inference(avatar_split_clause,[],[f62,f559,f533,f507,f481]) ).
fof(f705,plain,
( spl3_61
| spl3_67
| spl3_73
| spl3_79 ),
inference(avatar_split_clause,[],[f63,f563,f537,f511,f485]) ).
fof(f706,plain,
( spl3_62
| spl3_68
| spl3_74
| spl3_80 ),
inference(avatar_split_clause,[],[f64,f567,f541,f515,f489]) ).
fof(f707,plain,
( spl3_57
| spl3_63
| spl3_69
| spl3_75 ),
inference(avatar_split_clause,[],[f65,f546,f520,f494,f468]) ).
fof(f708,plain,
( spl3_28
| spl3_85
| spl3_10
| spl3_15 ),
inference(avatar_split_clause,[],[f66,f265,f243,f590,f325]) ).
fof(f709,plain,
( spl3_83
| spl3_88
| spl3_92
| spl3_96 ),
inference(avatar_split_clause,[],[f67,f639,f621,f603,f581]) ).
fof(f710,plain,
( spl3_84
| spl3_89
| spl3_93
| spl3_97 ),
inference(avatar_split_clause,[],[f68,f643,f625,f607,f585]) ).
fof(f711,plain,
( spl3_58
| spl3_64
| spl3_70
| spl3_76 ),
inference(avatar_split_clause,[],[f69,f550,f524,f498,f472]) ).
fof(f712,plain,
( spl3_81
| spl3_86
| spl3_90
| spl3_94 ),
inference(avatar_split_clause,[],[f70,f630,f612,f594,f572]) ).
fof(f713,plain,
( spl3_18
| spl3_5
| spl3_102
| spl3_13 ),
inference(avatar_split_clause,[],[f71,f256,f668,f221,f279]) ).
fof(f714,plain,
( spl3_99
| spl3_101
| spl3_104
| spl3_106 ),
inference(avatar_split_clause,[],[f72,f687,f677,f663,f653]) ).
fof(f715,plain,
( spl3_59
| spl3_65
| spl3_71
| spl3_77 ),
inference(avatar_split_clause,[],[f73,f554,f528,f502,f476]) ).
fof(f716,plain,
( spl3_82
| spl3_87
| spl3_91
| spl3_95 ),
inference(avatar_split_clause,[],[f74,f634,f616,f598,f576]) ).
fof(f717,plain,
( spl3_98
| spl3_100
| spl3_103
| spl3_105 ),
inference(avatar_split_clause,[],[f75,f682,f672,f658,f648]) ).
fof(f718,plain,
( spl3_16
| spl3_2
| spl3_8
| spl3_107 ),
inference(avatar_split_clause,[],[f76,f698,f234,f208,f270]) ).
fof(f719,plain,
( e1 = e2
| ~ spl3_2
| ~ spl3_8 ),
inference(superposition,[],[f235,f209]) ).
fof(f723,plain,
( $false
| ~ spl3_2
| ~ spl3_8 ),
inference(forward_subsumption_resolution,[],[f719,f159]) ).
fof(f724,plain,
( ~ spl3_2
| ~ spl3_8 ),
inference(avatar_contradiction_clause,[],[f723]) ).
fof(f726,plain,
( e0 = e2
| ~ spl3_5
| ~ spl3_13 ),
inference(superposition,[],[f257,f222]) ).
fof(f730,plain,
( $false
| ~ spl3_5
| ~ spl3_13 ),
inference(forward_subsumption_resolution,[],[f726,f161]) ).
fof(f731,plain,
( ~ spl3_5
| ~ spl3_13 ),
inference(avatar_contradiction_clause,[],[f730]) ).
fof(f733,plain,
( e0 = e1
| ~ spl3_10
| ~ spl3_15 ),
inference(superposition,[],[f266,f244]) ).
fof(f737,plain,
( $false
| ~ spl3_10
| ~ spl3_15 ),
inference(forward_subsumption_resolution,[],[f733,f162]) ).
fof(f738,plain,
( ~ spl3_10
| ~ spl3_15 ),
inference(avatar_contradiction_clause,[],[f737]) ).
fof(f751,plain,
( e1 = e2
| ~ spl3_64
| ~ spl3_70 ),
inference(superposition,[],[f526,f500]) ).
fof(f755,plain,
( $false
| ~ spl3_64
| ~ spl3_70 ),
inference(forward_subsumption_resolution,[],[f751,f159]) ).
fof(f756,plain,
( ~ spl3_64
| ~ spl3_70 ),
inference(avatar_contradiction_clause,[],[f755]) ).
fof(f800,plain,
( e2 = e3
| ~ spl3_30
| ~ spl3_56 ),
inference(superposition,[],[f336,f466]) ).
fof(f804,plain,
( $false
| ~ spl3_30
| ~ spl3_56 ),
inference(forward_subsumption_resolution,[],[f800,f157]) ).
fof(f805,plain,
( ~ spl3_30
| ~ spl3_56 ),
inference(avatar_contradiction_clause,[],[f804]) ).
fof(f832,plain,
( e0 = e3
| ~ spl3_26
| ~ spl3_56 ),
inference(superposition,[],[f316,f466]) ).
fof(f837,plain,
( $false
| ~ spl3_26
| ~ spl3_56 ),
inference(forward_subsumption_resolution,[],[f832,f160]) ).
fof(f838,plain,
( ~ spl3_26
| ~ spl3_56 ),
inference(avatar_contradiction_clause,[],[f837]) ).
fof(f843,plain,
( e0 = e2
| ~ spl3_15
| ~ spl3_85 ),
inference(superposition,[],[f592,f266]) ).
fof(f849,plain,
( $false
| ~ spl3_15
| ~ spl3_85 ),
inference(forward_subsumption_resolution,[],[f843,f161]) ).
fof(f850,plain,
( ~ spl3_15
| ~ spl3_85 ),
inference(avatar_contradiction_clause,[],[f849]) ).
fof(f852,plain,
( e2 = e3
| ~ spl3_81
| ~ spl3_86 ),
inference(superposition,[],[f596,f574]) ).
fof(f856,plain,
( $false
| ~ spl3_81
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f852,f157]) ).
fof(f857,plain,
( ~ spl3_81
| ~ spl3_86 ),
inference(avatar_contradiction_clause,[],[f856]) ).
fof(f897,plain,
( e1 = e3
| ~ spl3_60
| ~ spl3_72 ),
inference(superposition,[],[f483,f535]) ).
fof(f899,plain,
( e1 = e3
| ~ spl3_60
| ~ spl3_72 ),
inference(superposition,[],[f535,f483]) ).
fof(f901,plain,
( $false
| ~ spl3_60
| ~ spl3_72 ),
inference(forward_subsumption_resolution,[],[f899,f158]) ).
fof(f902,plain,
( ~ spl3_60
| ~ spl3_72 ),
inference(avatar_contradiction_clause,[],[f901]) ).
fof(f903,plain,
( $false
| ~ spl3_60
| ~ spl3_72 ),
inference(forward_subsumption_resolution,[],[f897,f158]) ).
fof(f904,plain,
( ~ spl3_60
| ~ spl3_72 ),
inference(avatar_contradiction_clause,[],[f903]) ).
fof(f928,plain,
( e2 = e3
| ~ spl3_61
| ~ spl3_67 ),
inference(superposition,[],[f513,f487]) ).
fof(f933,plain,
( $false
| ~ spl3_61
| ~ spl3_67 ),
inference(forward_subsumption_resolution,[],[f928,f157]) ).
fof(f934,plain,
( ~ spl3_61
| ~ spl3_67 ),
inference(avatar_contradiction_clause,[],[f933]) ).
fof(f935,plain,
( e2 = e3
| ~ spl3_5
| ~ spl3_18 ),
inference(superposition,[],[f280,f222]) ).
fof(f940,plain,
( $false
| ~ spl3_5
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f935,f157]) ).
fof(f941,plain,
( ~ spl3_5
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f940]) ).
fof(f947,plain,
( e1 = e3
| ~ spl3_99
| ~ spl3_104 ),
inference(superposition,[],[f679,f655]) ).
fof(f951,plain,
( $false
| ~ spl3_99
| ~ spl3_104 ),
inference(forward_subsumption_resolution,[],[f947,f158]) ).
fof(f952,plain,
( ~ spl3_99
| ~ spl3_104 ),
inference(avatar_contradiction_clause,[],[f951]) ).
fof(f961,plain,
( e0 = e3
| ~ spl3_13
| ~ spl3_18 ),
inference(superposition,[],[f257,f280]) ).
fof(f966,plain,
( $false
| ~ spl3_13
| ~ spl3_18 ),
inference(forward_subsumption_resolution,[],[f961,f160]) ).
fof(f967,plain,
( ~ spl3_13
| ~ spl3_18 ),
inference(avatar_contradiction_clause,[],[f966]) ).
fof(f972,plain,
( e0 = e3
| ~ spl3_82
| ~ spl3_95 ),
inference(superposition,[],[f578,f636]) ).
fof(f973,plain,
( $false
| ~ spl3_82
| ~ spl3_95 ),
inference(forward_subsumption_resolution,[],[f972,f160]) ).
fof(f974,plain,
( ~ spl3_82
| ~ spl3_95 ),
inference(avatar_contradiction_clause,[],[f973]) ).
fof(f994,plain,
( e1 = e3
| ~ spl3_82
| ~ spl3_91 ),
inference(superposition,[],[f618,f578]) ).
fof(f999,plain,
( $false
| ~ spl3_82
| ~ spl3_91 ),
inference(forward_subsumption_resolution,[],[f994,f158]) ).
fof(f1000,plain,
( ~ spl3_82
| ~ spl3_91 ),
inference(avatar_contradiction_clause,[],[f999]) ).
fof(f1001,plain,
( e0 = e3
| ~ spl3_15
| ~ spl3_28 ),
inference(superposition,[],[f326,f266]) ).
fof(f1007,plain,
( $false
| ~ spl3_15
| ~ spl3_28 ),
inference(forward_subsumption_resolution,[],[f1001,f160]) ).
fof(f1008,plain,
( ~ spl3_15
| ~ spl3_28 ),
inference(avatar_contradiction_clause,[],[f1007]) ).
fof(f1032,plain,
( e0 = e1
| ~ spl3_13
| ~ spl3_102 ),
inference(superposition,[],[f670,f257]) ).
fof(f1038,plain,
( $false
| ~ spl3_13
| ~ spl3_102 ),
inference(forward_subsumption_resolution,[],[f1032,f162]) ).
fof(f1039,plain,
( ~ spl3_13
| ~ spl3_102 ),
inference(avatar_contradiction_clause,[],[f1038]) ).
fof(f1051,plain,
( e0 = e3
| ~ spl3_99
| ~ spl3_106 ),
inference(superposition,[],[f689,f655]) ).
fof(f1054,plain,
( e0 = e3
| ~ spl3_99
| ~ spl3_106 ),
inference(superposition,[],[f655,f689]) ).
fof(f1055,plain,
( $false
| ~ spl3_99
| ~ spl3_106 ),
inference(forward_subsumption_resolution,[],[f1054,f160]) ).
fof(f1056,plain,
( ~ spl3_99
| ~ spl3_106 ),
inference(avatar_contradiction_clause,[],[f1055]) ).
fof(f1057,plain,
( $false
| ~ spl3_99
| ~ spl3_106 ),
inference(forward_subsumption_resolution,[],[f1051,f160]) ).
fof(f1058,plain,
( ~ spl3_99
| ~ spl3_106 ),
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1060,plain,
( e0 = e1
| ~ spl3_8
| ~ spl3_107 ),
inference(superposition,[],[f700,f235]) ).
fof(f1066,plain,
( $false
| ~ spl3_8
| ~ spl3_107 ),
inference(forward_subsumption_resolution,[],[f1060,f162]) ).
fof(f1067,plain,
( ~ spl3_8
| ~ spl3_107 ),
inference(avatar_contradiction_clause,[],[f1066]) ).
fof(f1076,plain,
( e2 != op(e3,e0)
| ~ spl3_67 ),
inference(superposition,[],[f114,f513]) ).
fof(f1079,plain,
( e0 != op(e2,e1)
| ~ spl3_15 ),
inference(superposition,[],[f117,f266]) ).
fof(f1080,plain,
( ~ spl3_96
| ~ spl3_15 ),
inference(avatar_split_clause,[],[f1079,f265,f639]) ).
fof(f1083,plain,
( e0 != op(e2,e0)
| ~ spl3_15 ),
inference(superposition,[],[f119,f266]) ).
fof(f1084,plain,
( ~ spl3_97
| ~ spl3_15 ),
inference(avatar_split_clause,[],[f1083,f265,f643]) ).
fof(f1091,plain,
( e2 != op(e1,e1)
| ~ spl3_86 ),
inference(superposition,[],[f123,f596]) ).
fof(f1092,plain,
( e0 != op(e1,e0)
| ~ spl3_76 ),
inference(superposition,[],[f124,f552]) ).
fof(f1093,plain,
( e2 != op(e1,e0)
| ~ spl3_86 ),
inference(superposition,[],[f125,f596]) ).
fof(f1098,plain,
( e2 != op(e0,e1)
| ~ spl3_65 ),
inference(superposition,[],[f128,f504]) ).
fof(f1099,plain,
( ~ spl3_100
| ~ spl3_65 ),
inference(avatar_split_clause,[],[f1098,f502,f658]) ).
fof(f1101,plain,
( e3 != op(e0,e1)
| ~ spl3_82 ),
inference(superposition,[],[f129,f578]) ).
fof(f1102,plain,
( op(e0,e0) != e2
| ~ spl3_65 ),
inference(superposition,[],[f130,f504]) ).
fof(f1103,plain,
( op(e0,e0) != e3
| ~ spl3_82 ),
inference(superposition,[],[f131,f578]) ).
fof(f1104,plain,
( e0 != op(e0,e0)
| ~ spl3_105 ),
inference(superposition,[],[f132,f684]) ).
fof(f1105,plain,
( e3 != op(e2,e3)
| ~ spl3_56 ),
inference(superposition,[],[f133,f466]) ).
fof(f1106,plain,
( ~ spl3_57
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f1105,f464,f468]) ).
fof(f1108,plain,
( e3 != op(e1,e3)
| ~ spl3_56 ),
inference(superposition,[],[f134,f466]) ).
fof(f1109,plain,
( ~ spl3_58
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f1108,f464,f472]) ).
fof(f1111,plain,
( e1 != op(e1,e3)
| ~ spl3_69 ),
inference(superposition,[],[f135,f522]) ).
fof(f1112,plain,
( e3 != op(e0,e3)
| ~ spl3_56 ),
inference(superposition,[],[f136,f466]) ).
fof(f1113,plain,
( ~ spl3_59
| ~ spl3_56 ),
inference(avatar_split_clause,[],[f1112,f464,f476]) ).
fof(f1116,plain,
( e0 != op(e0,e3)
| ~ spl3_76 ),
inference(superposition,[],[f138,f552]) ).
fof(f1117,plain,
( e1 != op(e2,e2)
| ~ spl3_72 ),
inference(superposition,[],[f139,f535]) ).
fof(f1118,plain,
( e1 != op(e1,e2)
| ~ spl3_72 ),
inference(superposition,[],[f140,f535]) ).
fof(f1119,plain,
( ~ spl3_90
| ~ spl3_72 ),
inference(avatar_split_clause,[],[f1118,f533,f612]) ).
fof(f1121,plain,
( e0 != op(e1,e2)
| ~ spl3_15 ),
inference(superposition,[],[f141,f266]) ).
fof(f1122,plain,
( e1 != op(e0,e2)
| ~ spl3_72 ),
inference(superposition,[],[f142,f535]) ).
fof(f1123,plain,
( e0 != op(e0,e2)
| ~ spl3_15 ),
inference(superposition,[],[f143,f266]) ).
fof(f1126,plain,
( e2 != op(e1,e1)
| ~ spl3_67 ),
inference(superposition,[],[f146,f513]) ).
fof(f1127,plain,
( e3 != op(e1,e1)
| ~ spl3_83 ),
inference(superposition,[],[f147,f583]) ).
fof(f1128,plain,
( e2 != op(e0,e1)
| ~ spl3_67 ),
inference(superposition,[],[f148,f513]) ).
fof(f1130,plain,
( e1 != op(e0,e1)
| ~ spl3_102 ),
inference(superposition,[],[f150,f670]) ).
fof(f1132,plain,
( e0 != op(e1,e0)
| ~ spl3_80 ),
inference(superposition,[],[f152,f569]) ).
fof(f1133,plain,
( e2 != op(e1,e0)
| ~ spl3_89 ),
inference(superposition,[],[f153,f609]) ).
fof(f1134,plain,
( e0 != op(e0,e0)
| ~ spl3_80 ),
inference(superposition,[],[f154,f569]) ).
fof(f1136,plain,
( op(e0,e0) != e3
| ~ spl3_99 ),
inference(superposition,[],[f156,f655]) ).
fof(f1137,plain,
( e3 != op(e0,e1)
| spl3_3
| ~ spl3_8 ),
inference(superposition,[],[f214,f235]) ).
fof(f1139,plain,
( e2 != op(e1,e1)
| spl3_19
| ~ spl3_102 ),
inference(superposition,[],[f285,f670]) ).
fof(f1143,plain,
( e0 != op(op(e1,e1),e1)
| spl3_4
| ~ spl3_102 ),
inference(superposition,[],[f219,f670]) ).
fof(f1144,plain,
( e2 != op(op(e1,e1),e1)
| spl3_12
| ~ spl3_102 ),
inference(superposition,[],[f254,f670]) ).
fof(f1148,plain,
( e0 != op(e1,e1)
| spl3_4
| ~ spl3_102 ),
inference(superposition,[],[f1143,f670]) ).
fof(f1151,plain,
( e3 = op(e2,e2)
| ~ spl3_40
| ~ spl3_65 ),
inference(superposition,[],[f386,f504]) ).
fof(f1155,plain,
( e2 != op(e1,e1)
| spl3_12
| ~ spl3_102 ),
inference(superposition,[],[f1144,f670]) ).
fof(f1156,plain,
( e2 = op(e3,e3)
| ~ spl3_41
| ~ spl3_82 ),
inference(superposition,[],[f391,f578]) ).
fof(f1157,plain,
( $false
| spl3_30
| ~ spl3_41
| ~ spl3_82 ),
inference(forward_subsumption_resolution,[],[f1156,f337]) ).
fof(f1158,plain,
( spl3_30
| ~ spl3_41
| ~ spl3_82 ),
inference(avatar_contradiction_clause,[],[f1157]) ).
fof(f1160,plain,
( op(e0,e0) = e1
| ~ spl3_42
| ~ spl3_105 ),
inference(superposition,[],[f396,f684]) ).
fof(f1161,plain,
( e0 = op(e1,e1)
| ~ spl3_8
| ~ spl3_43 ),
inference(superposition,[],[f401,f235]) ).
fof(f1164,plain,
( e0 != op(e1,e1)
| ~ spl3_8
| spl3_43 ),
inference(superposition,[],[f400,f235]) ).
fof(f1166,plain,
( e3 = op(e1,e1)
| ~ spl3_48
| ~ spl3_69 ),
inference(superposition,[],[f426,f522]) ).
fof(f1170,plain,
( e2 = op(e1,e1)
| ~ spl3_45
| ~ spl3_72 ),
inference(superposition,[],[f411,f535]) ).
fof(f1173,plain,
( ~ spl3_5
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f1091,f594,f221]) ).
fof(f1174,plain,
( ~ spl3_5
| ~ spl3_67 ),
inference(avatar_split_clause,[],[f1126,f511,f221]) ).
fof(f1175,plain,
( ~ spl3_5
| spl3_19
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1139,f668,f283,f221]) ).
fof(f1176,plain,
( ~ spl3_5
| spl3_12
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1155,f668,f252,f221]) ).
fof(f1177,plain,
( spl3_5
| ~ spl3_45
| ~ spl3_72 ),
inference(avatar_split_clause,[],[f1170,f533,f409,f221]) ).
fof(f1180,plain,
( e1 = op(e2,e2)
| ~ spl3_46
| ~ spl3_67 ),
inference(superposition,[],[f416,f513]) ).
fof(f1185,plain,
( e0 = op(e0,e0)
| ~ spl3_47
| ~ spl3_80 ),
inference(superposition,[],[f421,f569]) ).
fof(f1186,plain,
( $false
| ~ spl3_47
| ~ spl3_80
| spl3_107 ),
inference(forward_subsumption_resolution,[],[f1185,f699]) ).
fof(f1187,plain,
( ~ spl3_47
| ~ spl3_80
| spl3_107 ),
inference(avatar_contradiction_clause,[],[f1186]) ).
fof(f1190,plain,
( op(e0,e0) = e2
| ~ spl3_15
| ~ spl3_49 ),
inference(superposition,[],[f431,f266]) ).
fof(f1191,plain,
( $false
| spl3_2
| ~ spl3_15
| ~ spl3_49 ),
inference(forward_subsumption_resolution,[],[f1190,f210]) ).
fof(f1192,plain,
( spl3_2
| ~ spl3_15
| ~ spl3_49 ),
inference(avatar_contradiction_clause,[],[f1191]) ).
fof(f1197,plain,
( e1 = op(e3,e3)
| ~ spl3_50
| ~ spl3_83 ),
inference(superposition,[],[f436,f583]) ).
fof(f1200,plain,
( spl3_22
| ~ spl3_50
| ~ spl3_83 ),
inference(avatar_split_clause,[],[f1197,f581,f434,f297]) ).
fof(f1201,plain,
( e1 = e3
| ~ spl3_22
| ~ spl3_56 ),
inference(superposition,[],[f298,f466]) ).
fof(f1202,plain,
( e1 != op(e3,e2)
| ~ spl3_22 ),
inference(superposition,[],[f109,f298]) ).
fof(f1203,plain,
( e1 != op(e3,e1)
| ~ spl3_22 ),
inference(superposition,[],[f110,f298]) ).
fof(f1204,plain,
( e1 != op(e3,e0)
| ~ spl3_22 ),
inference(superposition,[],[f112,f298]) ).
fof(f1205,plain,
( e1 != op(e2,e3)
| ~ spl3_22 ),
inference(superposition,[],[f133,f298]) ).
fof(f1207,plain,
( e1 != op(e0,e3)
| ~ spl3_22 ),
inference(superposition,[],[f136,f298]) ).
fof(f1212,plain,
( e3 = op(e1,e1)
| ~ spl3_22
| ~ spl3_44 ),
inference(superposition,[],[f406,f298]) ).
fof(f1225,plain,
( $false
| ~ spl3_22
| ~ spl3_56 ),
inference(forward_subsumption_resolution,[],[f1201,f158]) ).
fof(f1226,plain,
( ~ spl3_22
| ~ spl3_56 ),
inference(avatar_contradiction_clause,[],[f1225]) ).
fof(f1233,plain,
( e0 = op(e2,e2)
| ~ spl3_51
| ~ spl3_89 ),
inference(superposition,[],[f441,f609]) ).
fof(f1234,plain,
( op(e0,e0) = e3
| ~ spl3_52
| ~ spl3_76 ),
inference(superposition,[],[f446,f552]) ).
fof(f1237,plain,
( ~ spl3_16
| ~ spl3_82 ),
inference(avatar_split_clause,[],[f1103,f576,f270]) ).
fof(f1238,plain,
( ~ spl3_16
| ~ spl3_99 ),
inference(avatar_split_clause,[],[f1136,f653,f270]) ).
fof(f1240,plain,
( spl3_16
| ~ spl3_52
| ~ spl3_76 ),
inference(avatar_split_clause,[],[f1234,f550,f444,f270]) ).
fof(f1241,plain,
( ~ spl3_72
| ~ spl3_22 ),
inference(avatar_split_clause,[],[f1202,f297,f533]) ).
fof(f1242,plain,
( ~ spl3_69
| ~ spl3_22 ),
inference(avatar_split_clause,[],[f1205,f297,f520]) ).
fof(f1244,plain,
( spl3_15
| ~ spl3_51
| ~ spl3_89 ),
inference(avatar_split_clause,[],[f1233,f607,f439,f265]) ).
fof(f1246,plain,
( spl3_10
| ~ spl3_46
| ~ spl3_67 ),
inference(avatar_split_clause,[],[f1180,f511,f414,f243]) ).
fof(f1248,plain,
( ~ spl3_2
| ~ spl3_65 ),
inference(avatar_split_clause,[],[f1102,f502,f208]) ).
fof(f1250,plain,
( e1 != op(e2,e0)
| ~ spl3_10 ),
inference(superposition,[],[f119,f244]) ).
fof(f1251,plain,
( e1 != op(e1,e2)
| ~ spl3_10 ),
inference(superposition,[],[f141,f244]) ).
fof(f1252,plain,
( e1 != op(e0,e2)
| ~ spl3_10 ),
inference(superposition,[],[f143,f244]) ).
fof(f1259,plain,
( ~ spl3_93
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f1250,f243,f625]) ).
fof(f1260,plain,
( e0 != op(e1,e0)
| ~ spl3_13 ),
inference(superposition,[],[f126,f257]) ).
fof(f1261,plain,
( e0 != op(e0,e1)
| ~ spl3_13 ),
inference(superposition,[],[f150,f257]) ).
fof(f1264,plain,
( e2 != op(op(e1,e0),e1)
| spl3_12
| ~ spl3_13 ),
inference(superposition,[],[f254,f257]) ).
fof(f1266,plain,
( e2 != op(e1,e0)
| ~ spl3_13
| spl3_19 ),
inference(superposition,[],[f285,f257]) ).
fof(f1268,plain,
( ~ spl3_105
| ~ spl3_13 ),
inference(avatar_split_clause,[],[f1261,f256,f682]) ).
fof(f1270,plain,
( e0 != op(e3,e2)
| ~ spl3_26 ),
inference(superposition,[],[f109,f316]) ).
fof(f1271,plain,
( e0 != op(e3,e1)
| ~ spl3_26 ),
inference(superposition,[],[f110,f316]) ).
fof(f1272,plain,
( e0 != op(e3,e0)
| ~ spl3_26 ),
inference(superposition,[],[f112,f316]) ).
fof(f1274,plain,
( e0 != op(e1,e3)
| ~ spl3_26 ),
inference(superposition,[],[f134,f316]) ).
fof(f1281,plain,
( ~ spl3_76
| ~ spl3_26 ),
inference(avatar_split_clause,[],[f1274,f315,f550]) ).
fof(f1283,plain,
( ~ spl3_80
| ~ spl3_26 ),
inference(avatar_split_clause,[],[f1272,f315,f567]) ).
fof(f1284,plain,
( ~ spl3_79
| ~ spl3_26 ),
inference(avatar_split_clause,[],[f1271,f315,f563]) ).
fof(f1286,plain,
( e3 != op(e2,e2)
| ~ spl3_57 ),
inference(superposition,[],[f115,f470]) ).
fof(f1287,plain,
( e3 != op(e2,e1)
| ~ spl3_57 ),
inference(superposition,[],[f116,f470]) ).
fof(f1288,plain,
( e3 != op(e2,e0)
| ~ spl3_57 ),
inference(superposition,[],[f118,f470]) ).
fof(f1290,plain,
( e3 != op(e0,e3)
| ~ spl3_57 ),
inference(superposition,[],[f137,f470]) ).
fof(f1292,plain,
( ~ spl3_59
| ~ spl3_57 ),
inference(avatar_split_clause,[],[f1290,f468,f476]) ).
fof(f1293,plain,
( ~ spl3_84
| ~ spl3_57 ),
inference(avatar_split_clause,[],[f1288,f468,f585]) ).
fof(f1294,plain,
( ~ spl3_83
| ~ spl3_57 ),
inference(avatar_split_clause,[],[f1287,f468,f581]) ).
fof(f1298,plain,
( ~ spl3_70
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f1111,f520,f524]) ).
fof(f1299,plain,
( ~ spl3_74
| ~ spl3_22 ),
inference(avatar_split_clause,[],[f1204,f297,f541]) ).
fof(f1300,plain,
( ~ spl3_68
| ~ spl3_67 ),
inference(avatar_split_clause,[],[f1076,f511,f515]) ).
fof(f1302,plain,
( ~ spl3_107
| ~ spl3_80 ),
inference(avatar_split_clause,[],[f1134,f567,f698]) ).
fof(f1305,plain,
( ~ spl3_101
| ~ spl3_86 ),
inference(avatar_split_clause,[],[f1093,f594,f663]) ).
fof(f1306,plain,
( ~ spl3_101
| ~ spl3_13
| spl3_19 ),
inference(avatar_split_clause,[],[f1266,f283,f256,f663]) ).
fof(f1307,plain,
( ~ spl3_101
| ~ spl3_89 ),
inference(avatar_split_clause,[],[f1133,f607,f663]) ).
fof(f1309,plain,
( e3 != op(e0,e3)
| spl3_3
| ~ spl3_16 ),
inference(superposition,[],[f214,f271]) ).
fof(f1314,plain,
( ~ spl3_59
| spl3_3
| ~ spl3_16 ),
inference(avatar_split_clause,[],[f1309,f270,f212,f476]) ).
fof(f1320,plain,
( e1 != op(e0,e3)
| ~ spl3_22 ),
inference(superposition,[],[f136,f298]) ).
fof(f1328,plain,
( e3 != op(e1,e1)
| ~ spl3_58 ),
inference(superposition,[],[f122,f474]) ).
fof(f1329,plain,
( e3 != op(e1,e0)
| ~ spl3_58 ),
inference(superposition,[],[f124,f474]) ).
fof(f1330,plain,
( e3 != op(e0,e3)
| ~ spl3_58 ),
inference(superposition,[],[f138,f474]) ).
fof(f1332,plain,
( ~ spl3_59
| ~ spl3_58 ),
inference(avatar_split_clause,[],[f1330,f472,f476]) ).
fof(f1333,plain,
( ~ spl3_99
| ~ spl3_58 ),
inference(avatar_split_clause,[],[f1329,f472,f653]) ).
fof(f1354,plain,
( e3 != op(e3,e1)
| ~ spl3_60 ),
inference(superposition,[],[f111,f483]) ).
fof(f1356,plain,
( e3 != op(e2,e2)
| ~ spl3_60 ),
inference(superposition,[],[f139,f483]) ).
fof(f1357,plain,
( e3 != op(e1,e2)
| ~ spl3_60 ),
inference(superposition,[],[f140,f483]) ).
fof(f1363,plain,
( ~ spl3_81
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f1357,f481,f572]) ).
fof(f1364,plain,
( ~ spl3_61
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f1354,f481,f485]) ).
fof(f1365,plain,
( e3 != op(e3,e0)
| ~ spl3_61 ),
inference(superposition,[],[f114,f487]) ).
fof(f1366,plain,
( e3 != op(e2,e1)
| ~ spl3_61 ),
inference(superposition,[],[f145,f487]) ).
fof(f1367,plain,
( e3 != op(e1,e1)
| ~ spl3_61 ),
inference(superposition,[],[f146,f487]) ).
fof(f1368,plain,
( e3 != op(e0,e1)
| ~ spl3_61 ),
inference(superposition,[],[f148,f487]) ).
fof(f1370,plain,
( ~ spl3_83
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1366,f485,f581]) ).
fof(f1371,plain,
( e2 != op(e3,e1)
| ~ spl3_66 ),
inference(superposition,[],[f111,f509]) ).
fof(f1373,plain,
( e2 != op(e2,e2)
| ~ spl3_66 ),
inference(superposition,[],[f139,f509]) ).
fof(f1374,plain,
( e2 != op(e1,e2)
| ~ spl3_66 ),
inference(superposition,[],[f140,f509]) ).
fof(f1380,plain,
( ~ spl3_86
| ~ spl3_66 ),
inference(avatar_split_clause,[],[f1374,f507,f594]) ).
fof(f1381,plain,
( ~ spl3_85
| ~ spl3_66 ),
inference(avatar_split_clause,[],[f1373,f507,f590]) ).
fof(f1383,plain,
( ~ spl3_67
| ~ spl3_66 ),
inference(avatar_split_clause,[],[f1371,f507,f511]) ).
fof(f1389,plain,
( e1 != op(e0,e3)
| ~ spl3_70 ),
inference(superposition,[],[f138,f526]) ).
fof(f1395,plain,
( e1 != op(e2,e0)
| ~ spl3_74 ),
inference(superposition,[],[f151,f543]) ).
fof(f1396,plain,
( e1 != op(e1,e0)
| ~ spl3_74 ),
inference(superposition,[],[f152,f543]) ).
fof(f1397,plain,
( op(e0,e0) != e1
| ~ spl3_74 ),
inference(superposition,[],[f154,f543]) ).
fof(f1403,plain,
( ~ spl3_104
| ~ spl3_74 ),
inference(avatar_split_clause,[],[f1396,f541,f677]) ).
fof(f1404,plain,
( ~ spl3_93
| ~ spl3_74 ),
inference(avatar_split_clause,[],[f1395,f541,f625]) ).
fof(f1409,plain,
( e3 != op(e1,e1)
| ~ spl3_81 ),
inference(superposition,[],[f123,f574]) ).
fof(f1410,plain,
( e3 != op(e1,e0)
| ~ spl3_81 ),
inference(superposition,[],[f125,f574]) ).
fof(f1415,plain,
( ~ spl3_99
| ~ spl3_81 ),
inference(avatar_split_clause,[],[f1410,f572,f653]) ).
fof(f1419,plain,
( e2 != op(e1,e1)
| ~ spl3_88 ),
inference(superposition,[],[f147,f605]) ).
fof(f1420,plain,
( e2 != op(e0,e1)
| ~ spl3_88 ),
inference(superposition,[],[f149,f605]) ).
fof(f1425,plain,
( e0 != op(e0,e1)
| ~ spl3_95 ),
inference(superposition,[],[f129,f636]) ).
fof(f1426,plain,
( e0 != op(e0,e0)
| ~ spl3_95 ),
inference(superposition,[],[f131,f636]) ).
fof(f1431,plain,
( ~ spl3_107
| ~ spl3_95 ),
inference(avatar_split_clause,[],[f1426,f634,f698]) ).
fof(f1432,plain,
( ~ spl3_105
| ~ spl3_95 ),
inference(avatar_split_clause,[],[f1425,f634,f682]) ).
fof(f1433,plain,
( e0 != op(e1,e0)
| ~ spl3_97 ),
inference(superposition,[],[f153,f645]) ).
fof(f1434,plain,
( e0 != op(e0,e0)
| ~ spl3_97 ),
inference(superposition,[],[f155,f645]) ).
fof(f1438,plain,
( ~ spl3_107
| ~ spl3_97 ),
inference(avatar_split_clause,[],[f1434,f643,f698]) ).
fof(f1440,plain,
( op(e0,e0) != e2
| ~ spl3_101 ),
inference(superposition,[],[f156,f665]) ).
fof(f1443,plain,
( op(e0,e0) != e1
| ~ spl3_103 ),
inference(superposition,[],[f132,f674]) ).
fof(f1444,plain,
( e1 = op(e1,e1)
| ~ spl3_42
| ~ spl3_103 ),
inference(superposition,[],[f396,f674]) ).
fof(f1452,plain,
( e3 = op(e0,e3)
| ~ spl3_3
| ~ spl3_16 ),
inference(superposition,[],[f213,f271]) ).
fof(f1466,plain,
( e0 != op(e2,e1)
| spl3_4
| ~ spl3_19 ),
inference(superposition,[],[f219,f284]) ).
fof(f1470,plain,
( e3 != op(e1,e0)
| spl3_6
| ~ spl3_13 ),
inference(superposition,[],[f227,f257]) ).
fof(f1473,plain,
( e1 != op(e0,e3)
| ~ spl3_16
| spl3_27 ),
inference(superposition,[],[f322,f271]) ).
fof(f1477,plain,
( e2 = op(e2,e1)
| ~ spl3_12
| ~ spl3_19 ),
inference(superposition,[],[f253,f284]) ).
fof(f1480,plain,
( e3 != op(e2,e1)
| ~ spl3_19
| spl3_24 ),
inference(superposition,[],[f308,f284]) ).
fof(f1484,plain,
( e0 = op(e3,e3)
| ~ spl3_16
| ~ spl3_43 ),
inference(superposition,[],[f401,f271]) ).
fof(f1485,plain,
( op(e0,e0) != e3
| ~ spl3_26
| spl3_44 ),
inference(superposition,[],[f405,f316]) ).
fof(f1488,plain,
( op(e0,e0) = e3
| ~ spl3_26
| ~ spl3_44 ),
inference(superposition,[],[f406,f316]) ).
fof(f1489,plain,
( e1 = op(e3,e3)
| ~ spl3_46
| ~ spl3_61 ),
inference(superposition,[],[f416,f487]) ).
fof(f1490,plain,
( $false
| spl3_22
| ~ spl3_46
| ~ spl3_61 ),
inference(forward_subsumption_resolution,[],[f1489,f299]) ).
fof(f1491,plain,
( spl3_22
| ~ spl3_46
| ~ spl3_61 ),
inference(avatar_contradiction_clause,[],[f1490]) ).
fof(f1494,plain,
( e0 = op(e1,e1)
| ~ spl3_47
| ~ spl3_74 ),
inference(superposition,[],[f421,f543]) ).
fof(f1496,plain,
( e2 = op(e1,e1)
| ~ spl3_10
| ~ spl3_49 ),
inference(superposition,[],[f431,f244]) ).
fof(f1501,plain,
( e1 = op(e2,e2)
| ~ spl3_50
| ~ spl3_88 ),
inference(superposition,[],[f436,f605]) ).
fof(f1503,plain,
( e3 = op(e1,e1)
| ~ spl3_52
| ~ spl3_70 ),
inference(superposition,[],[f446,f526]) ).
fof(f1506,plain,
( ~ spl3_98
| spl3_3
| ~ spl3_8 ),
inference(avatar_split_clause,[],[f1137,f234,f212,f648]) ).
fof(f1508,plain,
( ~ spl3_99
| spl3_6
| ~ spl3_13 ),
inference(avatar_split_clause,[],[f1470,f256,f225,f653]) ).
fof(f1511,plain,
( spl3_88
| ~ spl3_12
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f1477,f283,f252,f603]) ).
fof(f1512,plain,
( spl3_16
| ~ spl3_26
| ~ spl3_44 ),
inference(avatar_split_clause,[],[f1488,f404,f315,f270]) ).
fof(f1513,plain,
( ~ spl3_8
| ~ spl3_74 ),
inference(avatar_split_clause,[],[f1397,f541,f234]) ).
fof(f1514,plain,
( ~ spl3_13
| ~ spl3_8
| spl3_43 ),
inference(avatar_split_clause,[],[f1164,f399,f234,f256]) ).
fof(f1515,plain,
( ~ spl3_16
| ~ spl3_26
| spl3_44 ),
inference(avatar_split_clause,[],[f1485,f404,f315,f270]) ).
fof(f1516,plain,
( spl3_5
| ~ spl3_10
| ~ spl3_49 ),
inference(avatar_split_clause,[],[f1496,f429,f243,f221]) ).
fof(f1517,plain,
( ~ spl3_98
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1368,f485,f648]) ).
fof(f1518,plain,
( ~ spl3_98
| ~ spl3_82 ),
inference(avatar_split_clause,[],[f1101,f576,f648]) ).
fof(f1519,plain,
( ~ spl3_5
| ~ spl3_88 ),
inference(avatar_split_clause,[],[f1419,f603,f221]) ).
fof(f1520,plain,
( ~ spl3_78
| ~ spl3_26 ),
inference(avatar_split_clause,[],[f1270,f315,f559]) ).
fof(f1523,plain,
( spl3_18
| ~ spl3_52
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f1503,f524,f444,f279]) ).
fof(f1524,plain,
( ~ spl3_62
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1365,f485,f489]) ).
fof(f1525,plain,
( ~ spl3_18
| ~ spl3_61 ),
inference(avatar_split_clause,[],[f1367,f485,f279]) ).
fof(f1535,plain,
( e3 != op(e0,e1)
| ~ spl3_18 ),
inference(superposition,[],[f150,f280]) ).
fof(f1543,plain,
( e0 != op(e1,e3)
| ~ spl3_18
| spl3_34 ),
inference(superposition,[],[f356,f280]) ).
fof(f1547,plain,
( ~ spl3_98
| ~ spl3_18 ),
inference(avatar_split_clause,[],[f1535,f279,f648]) ).
fof(f1551,plain,
( op(e0,e0) != e3
| ~ spl3_62 ),
inference(superposition,[],[f154,f491]) ).
fof(f1566,plain,
( e1 != op(e3,e0)
| ~ spl3_73 ),
inference(superposition,[],[f114,f539]) ).
fof(f1567,plain,
( e1 != op(e2,e1)
| ~ spl3_73 ),
inference(superposition,[],[f145,f539]) ).
fof(f1568,plain,
( e1 != op(e1,e1)
| ~ spl3_73 ),
inference(superposition,[],[f146,f539]) ).
fof(f1569,plain,
( e1 != op(e0,e1)
| ~ spl3_73 ),
inference(superposition,[],[f148,f539]) ).
fof(f1573,plain,
( ~ spl3_103
| ~ spl3_73 ),
inference(avatar_split_clause,[],[f1569,f537,f672]) ).
fof(f1574,plain,
( ~ spl3_92
| ~ spl3_73 ),
inference(avatar_split_clause,[],[f1567,f537,f621]) ).
fof(f1575,plain,
( ~ spl3_74
| ~ spl3_73 ),
inference(avatar_split_clause,[],[f1566,f537,f541]) ).
fof(f1593,plain,
( e0 != op(e1,e1)
| ~ spl3_94 ),
inference(superposition,[],[f123,f632]) ).
fof(f1595,plain,
( e0 != op(e0,e2)
| ~ spl3_94 ),
inference(superposition,[],[f144,f632]) ).
fof(f1599,plain,
( ~ spl3_95
| ~ spl3_94 ),
inference(avatar_split_clause,[],[f1595,f630,f634]) ).
fof(f1612,plain,
( e2 != op(e1,e3)
| ~ spl3_18
| spl3_19 ),
inference(superposition,[],[f285,f280]) ).
fof(f1628,plain,
( e2 = op(e2,e2)
| ~ spl3_45
| ~ spl3_66 ),
inference(superposition,[],[f411,f509]) ).
fof(f1629,plain,
( $false
| ~ spl3_45
| ~ spl3_66
| spl3_85 ),
inference(forward_subsumption_resolution,[],[f1628,f591]) ).
fof(f1630,plain,
( ~ spl3_45
| ~ spl3_66
| spl3_85 ),
inference(avatar_contradiction_clause,[],[f1629]) ).
fof(f1633,plain,
( e3 = op(e3,e3)
| ~ spl3_48
| ~ spl3_57 ),
inference(superposition,[],[f426,f470]) ).
fof(f1634,plain,
( $false
| ~ spl3_48
| spl3_56
| ~ spl3_57 ),
inference(forward_subsumption_resolution,[],[f1633,f465]) ).
fof(f1635,plain,
( ~ spl3_48
| spl3_56
| ~ spl3_57 ),
inference(avatar_contradiction_clause,[],[f1634]) ).
fof(f1638,plain,
( e0 = op(e0,e0)
| ~ spl3_51
| ~ spl3_97 ),
inference(superposition,[],[f441,f645]) ).
fof(f1639,plain,
( $false
| ~ spl3_51
| ~ spl3_97
| spl3_107 ),
inference(forward_subsumption_resolution,[],[f1638,f699]) ).
fof(f1640,plain,
( ~ spl3_51
| ~ spl3_97
| spl3_107 ),
inference(avatar_contradiction_clause,[],[f1639]) ).
fof(f1643,plain,
( op(e0,e0) = e2
| ~ spl3_53
| ~ spl3_94 ),
inference(superposition,[],[f451,f632]) ).
fof(f1644,plain,
( $false
| spl3_2
| ~ spl3_53
| ~ spl3_94 ),
inference(forward_subsumption_resolution,[],[f1643,f210]) ).
fof(f1645,plain,
( spl3_2
| ~ spl3_53
| ~ spl3_94 ),
inference(avatar_contradiction_clause,[],[f1644]) ).
fof(f1648,plain,
( ~ spl3_94
| ~ spl3_15 ),
inference(avatar_split_clause,[],[f1121,f265,f630]) ).
fof(f1650,plain,
( spl3_10
| ~ spl3_50
| ~ spl3_88 ),
inference(avatar_split_clause,[],[f1501,f603,f434,f243]) ).
fof(f1651,plain,
( ~ spl3_10
| ~ spl3_72 ),
inference(avatar_split_clause,[],[f1117,f533,f243]) ).
fof(f1688,plain,
( e2 = op(e2,e2)
| ~ spl3_53
| ~ spl3_86 ),
inference(superposition,[],[f451,f596]) ).
fof(f1690,plain,
( $false
| ~ spl3_53
| spl3_85
| ~ spl3_86 ),
inference(forward_subsumption_resolution,[],[f1688,f591]) ).
fof(f1691,plain,
( ~ spl3_53
| spl3_85
| ~ spl3_86 ),
inference(avatar_contradiction_clause,[],[f1690]) ).
fof(f1698,plain,
( ~ spl3_107
| ~ spl3_105 ),
inference(avatar_split_clause,[],[f1104,f682,f698]) ).
fof(f1699,plain,
( ~ spl3_18
| ~ spl3_58 ),
inference(avatar_split_clause,[],[f1328,f472,f279]) ).
fof(f1700,plain,
( spl3_8
| ~ spl3_42
| ~ spl3_105 ),
inference(avatar_split_clause,[],[f1160,f682,f394,f234]) ).
fof(f1702,plain,
( e2 != op(e1,e0)
| ~ spl3_5 ),
inference(superposition,[],[f126,f222]) ).
fof(f1703,plain,
( e2 != op(e0,e1)
| ~ spl3_5 ),
inference(superposition,[],[f150,f222]) ).
fof(f1705,plain,
( e3 != op(e1,e2)
| ~ spl3_5
| spl3_6 ),
inference(superposition,[],[f227,f222]) ).
fof(f1714,plain,
( ~ spl3_100
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f1703,f221,f658]) ).
fof(f1715,plain,
( ~ spl3_101
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f1702,f221,f663]) ).
fof(f1717,plain,
( ~ spl3_106
| ~ spl3_13 ),
inference(avatar_split_clause,[],[f1260,f256,f687]) ).
fof(f1720,plain,
( ~ spl3_96
| spl3_4
| ~ spl3_19 ),
inference(avatar_split_clause,[],[f1466,f283,f217,f639]) ).
fof(f1721,plain,
( ~ spl3_13
| ~ spl3_94 ),
inference(avatar_split_clause,[],[f1593,f630,f256]) ).
fof(f1728,plain,
( e3 = op(e3,e3)
| ~ spl3_52
| ~ spl3_58 ),
inference(superposition,[],[f446,f474]) ).
fof(f1731,plain,
( $false
| ~ spl3_52
| spl3_56
| ~ spl3_58 ),
inference(forward_subsumption_resolution,[],[f1728,f465]) ).
fof(f1732,plain,
( ~ spl3_52
| spl3_56
| ~ spl3_58 ),
inference(avatar_contradiction_clause,[],[f1731]) ).
fof(f1740,plain,
( e2 != op(e2,e2)
| ~ spl3_63 ),
inference(superposition,[],[f115,f496]) ).
fof(f1743,plain,
( e2 != op(e1,e3)
| ~ spl3_63 ),
inference(superposition,[],[f135,f496]) ).
fof(f1744,plain,
( e2 != op(e0,e3)
| ~ spl3_63 ),
inference(superposition,[],[f137,f496]) ).
fof(f1747,plain,
( ~ spl3_65
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1744,f494,f502]) ).
fof(f1750,plain,
( ~ spl3_85
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1740,f494,f590]) ).
fof(f1751,plain,
( ~ spl3_100
| ~ spl3_67 ),
inference(avatar_split_clause,[],[f1128,f511,f658]) ).
fof(f1752,plain,
( e3 != op(e2,e1)
| ~ spl3_28 ),
inference(superposition,[],[f117,f326]) ).
fof(f1753,plain,
( e3 != op(e2,e0)
| ~ spl3_28 ),
inference(superposition,[],[f119,f326]) ).
fof(f1754,plain,
( e3 != op(e1,e2)
| ~ spl3_28 ),
inference(superposition,[],[f141,f326]) ).
fof(f1755,plain,
( e3 != op(e0,e2)
| ~ spl3_28 ),
inference(superposition,[],[f143,f326]) ).
fof(f1761,plain,
( e0 != op(e2,e3)
| ~ spl3_28
| spl3_35 ),
inference(superposition,[],[f361,f326]) ).
fof(f1762,plain,
( ~ spl3_82
| ~ spl3_28 ),
inference(avatar_split_clause,[],[f1755,f325,f576]) ).
fof(f1763,plain,
( ~ spl3_84
| ~ spl3_28 ),
inference(avatar_split_clause,[],[f1753,f325,f585]) ).
fof(f1782,plain,
( e1 != op(e0,e2)
| ~ spl3_71 ),
inference(superposition,[],[f127,f530]) ).
fof(f1783,plain,
( e1 != op(e0,e1)
| ~ spl3_71 ),
inference(superposition,[],[f128,f530]) ).
fof(f1790,plain,
( op(e0,e0) != e2
| ~ spl3_87 ),
inference(superposition,[],[f131,f600]) ).
fof(f1796,plain,
( op(e0,e0) != e1
| ~ spl3_93 ),
inference(superposition,[],[f155,f627]) ).
fof(f1806,plain,
( e0 != op(e2,e0)
| ~ spl3_96 ),
inference(superposition,[],[f120,f641]) ).
fof(f1807,plain,
( e0 != op(e1,e1)
| ~ spl3_96 ),
inference(superposition,[],[f147,f641]) ).
fof(f1808,plain,
( e0 != op(e0,e1)
| ~ spl3_96 ),
inference(superposition,[],[f149,f641]) ).
fof(f1811,plain,
( ~ spl3_105
| ~ spl3_96 ),
inference(avatar_split_clause,[],[f1808,f639,f682]) ).
fof(f1812,plain,
( ~ spl3_97
| ~ spl3_96 ),
inference(avatar_split_clause,[],[f1806,f639,f643]) ).
fof(f1814,plain,
( op(e0,e0) != e3
| ~ spl3_98 ),
inference(superposition,[],[f132,f650]) ).
fof(f1815,plain,
( e1 = op(e3,e3)
| ~ spl3_42
| ~ spl3_98 ),
inference(superposition,[],[f396,f650]) ).
fof(f1821,plain,
( ~ spl3_73
| ~ spl3_22 ),
inference(avatar_split_clause,[],[f1203,f297,f537]) ).
fof(f1822,plain,
( $false
| ~ spl3_22
| ~ spl3_71 ),
inference(forward_subsumption_resolution,[],[f1207,f530]) ).
fof(f1823,plain,
( ~ spl3_22
| ~ spl3_71 ),
inference(avatar_contradiction_clause,[],[f1822]) ).
fof(f1824,plain,
( $false
| ~ spl3_22
| ~ spl3_71 ),
inference(forward_subsumption_resolution,[],[f1320,f530]) ).
fof(f1825,plain,
( ~ spl3_22
| ~ spl3_71 ),
inference(avatar_contradiction_clause,[],[f1824]) ).
fof(f1827,plain,
( ~ spl3_28
| ~ spl3_60 ),
inference(avatar_split_clause,[],[f1356,f481,f325]) ).
fof(f1828,plain,
( ~ spl3_102
| ~ spl3_73 ),
inference(avatar_split_clause,[],[f1568,f537,f668]) ).
fof(f1830,plain,
( spl3_22
| ~ spl3_42
| ~ spl3_98 ),
inference(avatar_split_clause,[],[f1815,f648,f394,f297]) ).
fof(f1833,plain,
( ~ spl3_16
| ~ spl3_98 ),
inference(avatar_split_clause,[],[f1814,f648,f270]) ).
fof(f1859,plain,
( e2 != op(e1,e0)
| ~ spl3_68 ),
inference(superposition,[],[f152,f517]) ).
fof(f1860,plain,
( op(e0,e0) != e2
| ~ spl3_68 ),
inference(superposition,[],[f154,f517]) ).
fof(f1861,plain,
( e0 = op(e2,e2)
| ~ spl3_47
| ~ spl3_68 ),
inference(superposition,[],[f421,f517]) ).
fof(f1870,plain,
( ~ spl3_101
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f1859,f515,f663]) ).
fof(f1881,plain,
( op(e0,e0) != e3
| ~ spl3_84 ),
inference(superposition,[],[f155,f587]) ).
fof(f1890,plain,
( op(e0,e0) != e1
| ~ spl3_104 ),
inference(superposition,[],[f156,f679]) ).
fof(f1895,plain,
( op(e0,e0) != e3
| spl3_3
| ~ spl3_107 ),
inference(superposition,[],[f214,f700]) ).
fof(f1899,plain,
( e2 = op(e1,e2)
| ~ spl3_5
| ~ spl3_19 ),
inference(superposition,[],[f284,f222]) ).
fof(f1902,plain,
( $false
| ~ spl3_5
| ~ spl3_19
| spl3_86 ),
inference(forward_subsumption_resolution,[],[f1899,f595]) ).
fof(f1903,plain,
( ~ spl3_5
| ~ spl3_19
| spl3_86 ),
inference(avatar_contradiction_clause,[],[f1902]) ).
fof(f1908,plain,
( e0 != op(e1,e2)
| spl3_9
| ~ spl3_29 ),
inference(superposition,[],[f241,f330]) ).
fof(f1916,plain,
( e1 != op(e3,e0)
| ~ spl3_26
| spl3_31 ),
inference(superposition,[],[f341,f316]) ).
fof(f1933,plain,
( e1 != op(e2,e3)
| ~ spl3_28
| spl3_29 ),
inference(superposition,[],[f331,f326]) ).
fof(f1969,plain,
( e3 != op(e1,e1)
| spl3_6
| ~ spl3_102 ),
inference(superposition,[],[f227,f670]) ).
fof(f1977,plain,
( e0 = op(e2,e3)
| ~ spl3_28
| ~ spl3_35 ),
inference(superposition,[],[f360,f326]) ).
fof(f2003,plain,
( e3 = op(e1,e1)
| ~ spl3_40
| ~ spl3_71 ),
inference(superposition,[],[f386,f530]) ).
fof(f2004,plain,
( $false
| spl3_18
| ~ spl3_40
| ~ spl3_71 ),
inference(forward_subsumption_resolution,[],[f2003,f281]) ).
fof(f2005,plain,
( spl3_18
| ~ spl3_40
| ~ spl3_71 ),
inference(avatar_contradiction_clause,[],[f2004]) ).
fof(f2007,plain,
( e2 = op(e2,e2)
| ~ spl3_41
| ~ spl3_87 ),
inference(superposition,[],[f391,f600]) ).
fof(f2021,plain,
( e0 = op(e3,e3)
| ~ spl3_47
| ~ spl3_62 ),
inference(superposition,[],[f421,f491]) ).
fof(f2022,plain,
( e3 = op(e2,e2)
| ~ spl3_48
| ~ spl3_63 ),
inference(superposition,[],[f426,f496]) ).
fof(f2023,plain,
( e2 = op(e3,e3)
| ~ spl3_28
| ~ spl3_49 ),
inference(superposition,[],[f431,f326]) ).
fof(f2026,plain,
( $false
| spl3_13
| ~ spl3_47
| ~ spl3_74 ),
inference(forward_subsumption_resolution,[],[f1494,f258]) ).
fof(f2027,plain,
( spl3_13
| ~ spl3_47
| ~ spl3_74 ),
inference(avatar_contradiction_clause,[],[f2026]) ).
fof(f2030,plain,
( spl3_85
| ~ spl3_41
| ~ spl3_87 ),
inference(avatar_split_clause,[],[f2007,f598,f389,f590]) ).
fof(f2033,plain,
( ~ spl3_2
| ~ spl3_87 ),
inference(avatar_split_clause,[],[f1790,f598,f208]) ).
fof(f2034,plain,
( ~ spl3_2
| ~ spl3_101 ),
inference(avatar_split_clause,[],[f1440,f663,f208]) ).
fof(f2053,plain,
( e2 != op(e1,e2)
| ~ spl3_64 ),
inference(superposition,[],[f121,f500]) ).
fof(f2054,plain,
( e2 != op(e1,e1)
| ~ spl3_64 ),
inference(superposition,[],[f122,f500]) ).
fof(f2061,plain,
( ~ spl3_81
| ~ spl3_5
| spl3_6 ),
inference(avatar_split_clause,[],[f1705,f225,f221,f572]) ).
fof(f2062,plain,
( ~ spl3_5
| ~ spl3_64 ),
inference(avatar_split_clause,[],[f2054,f498,f221]) ).
fof(f2063,plain,
( ~ spl3_90
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f1251,f243,f612]) ).
fof(f2095,plain,
( ~ spl3_94
| spl3_9
| ~ spl3_29 ),
inference(avatar_split_clause,[],[f1908,f329,f239,f630]) ).
fof(f2130,plain,
( e0 != op(e2,e0)
| ~ spl3_75 ),
inference(superposition,[],[f118,f548]) ).
fof(f2132,plain,
( e0 != op(e0,e3)
| ~ spl3_75 ),
inference(superposition,[],[f137,f548]) ).
fof(f2138,plain,
( ~ spl3_77
| ~ spl3_75 ),
inference(avatar_split_clause,[],[f2132,f546,f554]) ).
fof(f2147,plain,
( e0 != op(e0,e0)
| ~ spl3_77 ),
inference(superposition,[],[f130,f556]) ).
fof(f2152,plain,
( ~ spl3_107
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f2147,f554,f698]) ).
fof(f2154,plain,
( e0 != op(e3,e0)
| ~ spl3_79 ),
inference(superposition,[],[f114,f565]) ).
fof(f2156,plain,
( e0 != op(e1,e1)
| ~ spl3_79 ),
inference(superposition,[],[f146,f565]) ).
fof(f2197,plain,
( e0 != op(e0,e0)
| ~ spl3_106 ),
inference(superposition,[],[f156,f689]) ).
fof(f2198,plain,
( ~ spl3_107
| ~ spl3_106 ),
inference(avatar_split_clause,[],[f2197,f687,f698]) ).
fof(f2200,plain,
( e3 = op(e0,e1)
| ~ spl3_3
| ~ spl3_8 ),
inference(superposition,[],[f213,f235]) ).
fof(f2209,plain,
( spl3_13
| ~ spl3_8
| ~ spl3_43 ),
inference(avatar_split_clause,[],[f1161,f399,f234,f256]) ).
fof(f2210,plain,
( ~ spl3_106
| ~ spl3_97 ),
inference(avatar_split_clause,[],[f1433,f643,f687]) ).
fof(f2219,plain,
( $false
| spl3_26
| ~ spl3_47
| ~ spl3_62 ),
inference(forward_subsumption_resolution,[],[f2021,f317]) ).
fof(f2220,plain,
( spl3_26
| ~ spl3_47
| ~ spl3_62 ),
inference(avatar_contradiction_clause,[],[f2219]) ).
fof(f2222,plain,
( ~ spl3_8
| ~ spl3_104 ),
inference(avatar_split_clause,[],[f1890,f677,f234]) ).
fof(f2226,plain,
( e1 != op(e0,e2)
| ~ spl3_2
| spl3_27 ),
inference(superposition,[],[f322,f209]) ).
fof(f2228,plain,
( ~ spl3_91
| ~ spl3_2
| spl3_27 ),
inference(avatar_split_clause,[],[f2226,f320,f208,f616]) ).
fof(f2241,plain,
( e2 != op(e3,e1)
| ~ spl3_30 ),
inference(superposition,[],[f110,f336]) ).
fof(f2242,plain,
( e2 != op(e3,e0)
| ~ spl3_30 ),
inference(superposition,[],[f112,f336]) ).
fof(f2244,plain,
( e2 != op(e1,e3)
| ~ spl3_30 ),
inference(superposition,[],[f134,f336]) ).
fof(f2245,plain,
( e2 != op(e0,e3)
| ~ spl3_30 ),
inference(superposition,[],[f136,f336]) ).
fof(f2251,plain,
( e1 != op(e3,e2)
| ~ spl3_30
| spl3_31 ),
inference(superposition,[],[f341,f336]) ).
fof(f2253,plain,
( ~ spl3_72
| ~ spl3_30
| spl3_31 ),
inference(avatar_split_clause,[],[f2251,f339,f335,f533]) ).
fof(f2254,plain,
( ~ spl3_64
| ~ spl3_30 ),
inference(avatar_split_clause,[],[f2244,f335,f498]) ).
fof(f2255,plain,
( ~ spl3_68
| ~ spl3_30 ),
inference(avatar_split_clause,[],[f2242,f335,f515]) ).
fof(f2261,plain,
( ~ spl3_91
| ~ spl3_10 ),
inference(avatar_split_clause,[],[f1252,f243,f616]) ).
fof(f2262,plain,
( ~ spl3_91
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f1782,f528,f616]) ).
fof(f2263,plain,
( ~ spl3_97
| ~ spl3_75 ),
inference(avatar_split_clause,[],[f2130,f546,f643]) ).
fof(f2264,plain,
( ~ spl3_2
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f1860,f515,f208]) ).
fof(f2323,plain,
( e0 != op(e3,e0)
| ~ spl3_78 ),
inference(superposition,[],[f113,f561]) ).
fof(f2324,plain,
( e0 != op(e2,e2)
| ~ spl3_78 ),
inference(superposition,[],[f139,f561]) ).
fof(f2360,plain,
( e1 != op(e1,e0)
| spl3_1
| ~ spl3_27 ),
inference(superposition,[],[f206,f321]) ).
fof(f2361,plain,
( $false
| spl3_1
| ~ spl3_27
| ~ spl3_104 ),
inference(forward_subsumption_resolution,[],[f2360,f679]) ).
fof(f2362,plain,
( spl3_1
| ~ spl3_27
| ~ spl3_104 ),
inference(avatar_contradiction_clause,[],[f2361]) ).
fof(f2379,plain,
( e0 = e2
| ~ spl3_4
| ~ spl3_12 ),
inference(superposition,[],[f253,f218]) ).
fof(f2384,plain,
( $false
| ~ spl3_4
| ~ spl3_12 ),
inference(forward_subsumption_resolution,[],[f2379,f161]) ).
fof(f2385,plain,
( ~ spl3_4
| ~ spl3_12 ),
inference(avatar_contradiction_clause,[],[f2384]) ).
fof(f2393,plain,
( op(e0,e0) = e2
| ~ spl3_45
| ~ spl3_78 ),
inference(superposition,[],[f411,f561]) ).
fof(f2397,plain,
( e1 = op(e1,e1)
| ~ spl3_46
| ~ spl3_73 ),
inference(superposition,[],[f416,f539]) ).
fof(f2398,plain,
( $false
| ~ spl3_46
| ~ spl3_73
| spl3_102 ),
inference(forward_subsumption_resolution,[],[f2397,f669]) ).
fof(f2399,plain,
( ~ spl3_46
| ~ spl3_73
| spl3_102 ),
inference(avatar_contradiction_clause,[],[f2398]) ).
fof(f2411,plain,
( e3 = op(e2,e2)
| ~ spl3_52
| ~ spl3_64 ),
inference(superposition,[],[f446,f500]) ).
fof(f2414,plain,
( ~ spl3_83
| ~ spl3_28 ),
inference(avatar_split_clause,[],[f1752,f325,f581]) ).
fof(f2415,plain,
( ~ spl3_81
| ~ spl3_28 ),
inference(avatar_split_clause,[],[f1754,f325,f572]) ).
fof(f2420,plain,
( spl3_28
| ~ spl3_52
| ~ spl3_64 ),
inference(avatar_split_clause,[],[f2411,f498,f444,f325]) ).
fof(f2447,plain,
( e2 = e3
| ~ spl3_28
| ~ spl3_85 ),
inference(superposition,[],[f592,f326]) ).
fof(f2448,plain,
( e2 != op(e2,e1)
| ~ spl3_85 ),
inference(superposition,[],[f117,f592]) ).
fof(f2449,plain,
( e2 != op(e2,e0)
| ~ spl3_85 ),
inference(superposition,[],[f119,f592]) ).
fof(f2451,plain,
( e2 != op(e0,e2)
| ~ spl3_85 ),
inference(superposition,[],[f143,f592]) ).
fof(f2460,plain,
( e2 != op(e2,e2)
| spl3_49
| ~ spl3_85 ),
inference(superposition,[],[f430,f592]) ).
fof(f2461,plain,
( $false
| spl3_49
| ~ spl3_85 ),
inference(forward_subsumption_resolution,[],[f2460,f592]) ).
fof(f2462,plain,
( spl3_49
| ~ spl3_85 ),
inference(avatar_contradiction_clause,[],[f2461]) ).
fof(f2469,plain,
( ~ spl3_89
| ~ spl3_85 ),
inference(avatar_split_clause,[],[f2449,f590,f607]) ).
fof(f2470,plain,
( ~ spl3_88
| ~ spl3_85 ),
inference(avatar_split_clause,[],[f2448,f590,f603]) ).
fof(f2471,plain,
( $false
| ~ spl3_28
| ~ spl3_85 ),
inference(forward_subsumption_resolution,[],[f2447,f157]) ).
fof(f2472,plain,
( ~ spl3_28
| ~ spl3_85 ),
inference(avatar_contradiction_clause,[],[f2471]) ).
fof(f2482,plain,
( e1 != op(e0,e2)
| ~ spl3_90 ),
inference(superposition,[],[f144,f614]) ).
fof(f2487,plain,
( e1 != op(e2,e0)
| ~ spl3_92 ),
inference(superposition,[],[f120,f623]) ).
fof(f2488,plain,
( e1 != op(e1,e1)
| ~ spl3_92 ),
inference(superposition,[],[f147,f623]) ).
fof(f2493,plain,
( e2 != op(e3,e1)
| spl3_12
| ~ spl3_13
| ~ spl3_99 ),
inference(superposition,[],[f1264,f655]) ).
fof(f2499,plain,
( ~ spl3_13
| spl3_4
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1148,f668,f217,f256]) ).
fof(f2504,plain,
( spl3_102
| ~ spl3_42
| ~ spl3_103 ),
inference(avatar_split_clause,[],[f1444,f672,f394,f668]) ).
fof(f2508,plain,
( ~ spl3_87
| ~ spl3_85 ),
inference(avatar_split_clause,[],[f2451,f590,f598]) ).
fof(f2510,plain,
( ~ spl3_13
| ~ spl3_96 ),
inference(avatar_split_clause,[],[f1807,f639,f256]) ).
fof(f2511,plain,
( ~ spl3_103
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1130,f668,f672]) ).
fof(f2515,plain,
( ~ spl3_71
| ~ spl3_70 ),
inference(avatar_split_clause,[],[f1389,f524,f528]) ).
fof(f2516,plain,
( ~ spl3_106
| ~ spl3_80 ),
inference(avatar_split_clause,[],[f1132,f567,f687]) ).
fof(f2517,plain,
( ~ spl3_102
| ~ spl3_92 ),
inference(avatar_split_clause,[],[f2488,f621,f668]) ).
fof(f2519,plain,
( ~ spl3_64
| ~ spl3_18
| spl3_19 ),
inference(avatar_split_clause,[],[f1612,f283,f279,f498]) ).
fof(f2627,plain,
( e3 = op(e1,e3)
| ~ spl3_6
| ~ spl3_18 ),
inference(superposition,[],[f226,f280]) ).
fof(f2631,plain,
( $false
| ~ spl3_6
| ~ spl3_18
| spl3_58 ),
inference(forward_subsumption_resolution,[],[f2627,f473]) ).
fof(f2632,plain,
( ~ spl3_6
| ~ spl3_18
| spl3_58 ),
inference(avatar_contradiction_clause,[],[f2631]) ).
fof(f2645,plain,
( op(e0,e0) = e3
| ~ spl3_48
| ~ spl3_75 ),
inference(superposition,[],[f426,f548]) ).
fof(f2652,plain,
( ~ spl3_91
| ~ spl3_72 ),
inference(avatar_split_clause,[],[f1122,f533,f616]) ).
fof(f2653,plain,
( ~ spl3_16
| ~ spl3_84 ),
inference(avatar_split_clause,[],[f1881,f585,f270]) ).
fof(f2654,plain,
( spl3_16
| ~ spl3_48
| ~ spl3_75 ),
inference(avatar_split_clause,[],[f2645,f546,f424,f270]) ).
fof(f2655,plain,
( spl3_59
| ~ spl3_3
| ~ spl3_16 ),
inference(avatar_split_clause,[],[f1452,f270,f212,f476]) ).
fof(f2656,plain,
( $false
| ~ spl3_3
| ~ spl3_8
| spl3_98 ),
inference(forward_subsumption_resolution,[],[f2200,f649]) ).
fof(f2657,plain,
( ~ spl3_3
| ~ spl3_8
| spl3_98 ),
inference(avatar_contradiction_clause,[],[f2656]) ).
fof(f2658,plain,
( ~ spl3_75
| ~ spl3_28
| spl3_35 ),
inference(avatar_split_clause,[],[f1761,f359,f325,f546]) ).
fof(f2659,plain,
( spl3_30
| ~ spl3_28
| ~ spl3_49 ),
inference(avatar_split_clause,[],[f2023,f429,f325,f335]) ).
fof(f2660,plain,
( $false
| ~ spl3_30
| ~ spl3_67 ),
inference(forward_subsumption_resolution,[],[f2241,f513]) ).
fof(f2661,plain,
( ~ spl3_30
| ~ spl3_67 ),
inference(avatar_contradiction_clause,[],[f2660]) ).
fof(f2663,plain,
( ~ spl3_65
| ~ spl3_30 ),
inference(avatar_split_clause,[],[f2245,f335,f502]) ).
fof(f2664,plain,
( ~ spl3_16
| ~ spl3_62 ),
inference(avatar_split_clause,[],[f1551,f489,f270]) ).
fof(f2665,plain,
( spl3_28
| ~ spl3_48
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f2022,f494,f424,f325]) ).
fof(f2676,plain,
( ~ spl3_77
| ~ spl3_76 ),
inference(avatar_split_clause,[],[f1116,f550,f554]) ).
fof(f2677,plain,
( ~ spl3_80
| ~ spl3_78 ),
inference(avatar_split_clause,[],[f2323,f559,f567]) ).
fof(f2680,plain,
( ~ spl3_91
| ~ spl3_90 ),
inference(avatar_split_clause,[],[f2482,f612,f616]) ).
fof(f2681,plain,
( ~ spl3_76
| ~ spl3_18
| spl3_34 ),
inference(avatar_split_clause,[],[f1543,f354,f279,f550]) ).
fof(f2682,plain,
( ~ spl3_8
| ~ spl3_103 ),
inference(avatar_split_clause,[],[f1443,f672,f234]) ).
fof(f2783,plain,
( e2 != op(e1,e3)
| ~ spl3_31
| spl3_33 ),
inference(superposition,[],[f351,f340]) ).
fof(f2804,plain,
( e2 != op(e0,e1)
| spl3_12
| ~ spl3_34 ),
inference(superposition,[],[f254,f355]) ).
fof(f2815,plain,
( op(e0,e0) = e1
| ~ spl3_50
| ~ spl3_96 ),
inference(superposition,[],[f436,f641]) ).
fof(f2818,plain,
( $false
| ~ spl3_16
| spl3_26
| ~ spl3_43 ),
inference(forward_subsumption_resolution,[],[f1484,f317]) ).
fof(f2819,plain,
( ~ spl3_16
| spl3_26
| ~ spl3_43 ),
inference(avatar_contradiction_clause,[],[f2818]) ).
fof(f2821,plain,
( ~ spl3_69
| ~ spl3_28
| spl3_29 ),
inference(avatar_split_clause,[],[f1933,f329,f325,f520]) ).
fof(f2822,plain,
( spl3_75
| ~ spl3_28
| ~ spl3_35 ),
inference(avatar_split_clause,[],[f1977,f359,f325,f546]) ).
fof(f2825,plain,
( ~ spl3_103
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f1783,f528,f672]) ).
fof(f2836,plain,
( e2 != op(e0,e3)
| ~ spl3_16
| spl3_17 ),
inference(superposition,[],[f276,f271]) ).
fof(f2837,plain,
( ~ spl3_65
| ~ spl3_16
| spl3_17 ),
inference(avatar_split_clause,[],[f2836,f274,f270,f502]) ).
fof(f2884,plain,
( e1 = op(e1,e1)
| ~ spl3_50
| ~ spl3_92 ),
inference(superposition,[],[f436,f623]) ).
fof(f2887,plain,
( $false
| ~ spl3_50
| ~ spl3_92
| spl3_102 ),
inference(forward_subsumption_resolution,[],[f2884,f669]) ).
fof(f2888,plain,
( ~ spl3_50
| ~ spl3_92
| spl3_102 ),
inference(avatar_contradiction_clause,[],[f2887]) ).
fof(f2905,plain,
( e1 = op(e0,e3)
| ~ spl3_16
| ~ spl3_27 ),
inference(superposition,[],[f321,f271]) ).
fof(f2907,plain,
( e2 != op(e1,e0)
| spl3_7
| ~ spl3_27 ),
inference(superposition,[],[f232,f321]) ).
fof(f2913,plain,
( e1 != op(e0,e2)
| spl3_14
| ~ spl3_35 ),
inference(superposition,[],[f263,f360]) ).
fof(f2933,plain,
( e2 = op(e1,e1)
| ~ spl3_53
| ~ spl3_90 ),
inference(superposition,[],[f451,f614]) ).
fof(f2934,plain,
( $false
| spl3_5
| ~ spl3_53
| ~ spl3_90 ),
inference(forward_subsumption_resolution,[],[f2933,f223]) ).
fof(f2935,plain,
( spl3_5
| ~ spl3_53
| ~ spl3_90 ),
inference(avatar_contradiction_clause,[],[f2934]) ).
fof(f2936,plain,
( ~ spl3_106
| ~ spl3_76 ),
inference(avatar_split_clause,[],[f1092,f550,f687]) ).
fof(f2937,plain,
( ~ spl3_18
| ~ spl3_81 ),
inference(avatar_split_clause,[],[f1409,f572,f279]) ).
fof(f2938,plain,
( ~ spl3_18
| ~ spl3_83 ),
inference(avatar_split_clause,[],[f1127,f581,f279]) ).
fof(f2939,plain,
( ~ spl3_18
| spl3_6
| ~ spl3_102 ),
inference(avatar_split_clause,[],[f1969,f668,f225,f279]) ).
fof(f2940,plain,
( ~ spl3_101
| spl3_7
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f2907,f320,f230,f663]) ).
fof(f2941,plain,
( spl3_71
| ~ spl3_16
| ~ spl3_27 ),
inference(avatar_split_clause,[],[f2905,f320,f270,f528]) ).
fof(f2942,plain,
( ~ spl3_71
| ~ spl3_16
| spl3_27 ),
inference(avatar_split_clause,[],[f1473,f320,f270,f528]) ).
fof(f2969,plain,
( e2 = op(e3,e3)
| ~ spl3_53
| ~ spl3_81 ),
inference(superposition,[],[f451,f574]) ).
fof(f2974,plain,
( ~ spl3_67
| ~ spl3_30 ),
inference(avatar_split_clause,[],[f2241,f335,f511]) ).
fof(f2975,plain,
( ~ spl3_100
| spl3_12
| ~ spl3_34 ),
inference(avatar_split_clause,[],[f2804,f354,f252,f658]) ).
fof(f2976,plain,
( spl3_18
| ~ spl3_48
| ~ spl3_69 ),
inference(avatar_split_clause,[],[f1166,f520,f424,f279]) ).
fof(f2977,plain,
( spl3_8
| ~ spl3_50
| ~ spl3_96 ),
inference(avatar_split_clause,[],[f2815,f639,f434,f234]) ).
fof(f2978,plain,
( ~ spl3_67
| spl3_12
| ~ spl3_13
| ~ spl3_99 ),
inference(avatar_split_clause,[],[f2493,f653,f256,f252,f511]) ).
fof(f2979,plain,
( ~ spl3_95
| ~ spl3_15 ),
inference(avatar_split_clause,[],[f1123,f265,f634]) ).
fof(f2981,plain,
( ~ spl3_74
| ~ spl3_26
| spl3_31 ),
inference(avatar_split_clause,[],[f1916,f339,f315,f541]) ).
fof(f2985,plain,
( ~ spl3_8
| ~ spl3_93 ),
inference(avatar_split_clause,[],[f1796,f625,f234]) ).
fof(f2986,plain,
( ~ spl3_16
| spl3_3
| ~ spl3_107 ),
inference(avatar_split_clause,[],[f1895,f698,f212,f270]) ).
fof(f2987,plain,
( spl3_15
| ~ spl3_47
| ~ spl3_68 ),
inference(avatar_split_clause,[],[f1861,f515,f419,f265]) ).
fof(f3084,plain,
( op(e0,e0) != e2
| ~ spl3_100 ),
inference(superposition,[],[f132,f660]) ).
fof(f3097,plain,
( e0 != op(e3,e1)
| spl3_4
| ~ spl3_6 ),
inference(superposition,[],[f219,f226]) ).
fof(f3102,plain,
( e1 != op(e2,e0)
| spl3_1
| ~ spl3_17 ),
inference(superposition,[],[f206,f275]) ).
fof(f3103,plain,
( $false
| spl3_1
| ~ spl3_17
| ~ spl3_93 ),
inference(forward_subsumption_resolution,[],[f3102,f627]) ).
fof(f3104,plain,
( spl3_1
| ~ spl3_17
| ~ spl3_93 ),
inference(avatar_contradiction_clause,[],[f3103]) ).
fof(f3134,plain,
( e3 = op(e3,e3)
| ~ spl3_40
| ~ spl3_59 ),
inference(superposition,[],[f386,f478]) ).
fof(f3135,plain,
( $false
| ~ spl3_40
| spl3_56
| ~ spl3_59 ),
inference(forward_subsumption_resolution,[],[f3134,f465]) ).
fof(f3136,plain,
( ~ spl3_40
| spl3_56
| ~ spl3_59 ),
inference(avatar_contradiction_clause,[],[f3135]) ).
fof(f3139,plain,
( $false
| spl3_14
| ~ spl3_35
| ~ spl3_91 ),
inference(forward_subsumption_resolution,[],[f2913,f618]) ).
fof(f3140,plain,
( spl3_14
| ~ spl3_35
| ~ spl3_91 ),
inference(avatar_contradiction_clause,[],[f3139]) ).
fof(f3142,plain,
( spl3_28
| ~ spl3_40
| ~ spl3_65 ),
inference(avatar_split_clause,[],[f1151,f502,f384,f325]) ).
fof(f3144,plain,
( ~ spl3_13
| ~ spl3_79 ),
inference(avatar_split_clause,[],[f2156,f563,f256]) ).
fof(f3145,plain,
( ~ spl3_100
| ~ spl3_88 ),
inference(avatar_split_clause,[],[f1420,f603,f658]) ).
fof(f3147,plain,
( ~ spl3_15
| ~ spl3_78 ),
inference(avatar_split_clause,[],[f2324,f559,f265]) ).
fof(f3149,plain,
( spl3_2
| ~ spl3_45
| ~ spl3_78 ),
inference(avatar_split_clause,[],[f2393,f559,f409,f208]) ).
fof(f3212,plain,
( op(e0,e0) = e3
| ~ spl3_40
| ~ spl3_77 ),
inference(superposition,[],[f386,f556]) ).
fof(f3223,plain,
( ~ spl3_86
| ~ spl3_64 ),
inference(avatar_split_clause,[],[f2053,f498,f594]) ).
fof(f3224,plain,
( $false
| ~ spl3_2
| ~ spl3_100 ),
inference(forward_subsumption_resolution,[],[f3084,f209]) ).
fof(f3225,plain,
( ~ spl3_2
| ~ spl3_100 ),
inference(avatar_contradiction_clause,[],[f3224]) ).
fof(f3226,plain,
( ~ spl3_64
| ~ spl3_63 ),
inference(avatar_split_clause,[],[f1743,f494,f498]) ).
fof(f3228,plain,
( ~ spl3_83
| ~ spl3_19
| spl3_24 ),
inference(avatar_split_clause,[],[f1480,f306,f283,f581]) ).
fof(f3230,plain,
( spl3_16
| ~ spl3_40
| ~ spl3_77 ),
inference(avatar_split_clause,[],[f3212,f554,f384,f270]) ).
fof(f3232,plain,
( spl3_18
| ~ spl3_22
| ~ spl3_44 ),
inference(avatar_split_clause,[],[f1212,f404,f297,f279]) ).
fof(f3233,plain,
( ~ spl3_28
| ~ spl3_57 ),
inference(avatar_split_clause,[],[f1286,f468,f325]) ).
fof(f3234,plain,
( ~ spl3_80
| ~ spl3_79 ),
inference(avatar_split_clause,[],[f2154,f563,f567]) ).
fof(f3351,plain,
( e2 = op(e3,e3)
| ~ spl3_45
| ~ spl3_60 ),
inference(superposition,[],[f411,f483]) ).
fof(f3352,plain,
( $false
| spl3_30
| ~ spl3_45
| ~ spl3_60 ),
inference(forward_subsumption_resolution,[],[f3351,f337]) ).
fof(f3353,plain,
( spl3_30
| ~ spl3_45
| ~ spl3_60 ),
inference(avatar_contradiction_clause,[],[f3352]) ).
fof(f3355,plain,
( ~ spl3_79
| spl3_4
| ~ spl3_6 ),
inference(avatar_split_clause,[],[f3097,f225,f217,f563]) ).
fof(f3356,plain,
( ~ spl3_64
| ~ spl3_31
| spl3_33 ),
inference(avatar_split_clause,[],[f2783,f349,f339,f498]) ).
fof(f3359,plain,
( spl3_30
| ~ spl3_53
| ~ spl3_81 ),
inference(avatar_split_clause,[],[f2969,f572,f449,f335]) ).
fof(f3360,plain,
( ~ spl3_93
| ~ spl3_92 ),
inference(avatar_split_clause,[],[f2487,f621,f625]) ).
fof(f3381,plain,
( e3 = op(e2,e2)
| ~ spl3_30
| ~ spl3_44 ),
inference(superposition,[],[f406,f336]) ).
fof(f3383,plain,
( $false
| spl3_28
| ~ spl3_30
| ~ spl3_44 ),
inference(forward_subsumption_resolution,[],[f3381,f327]) ).
fof(f3384,plain,
( spl3_28
| ~ spl3_30
| ~ spl3_44 ),
inference(avatar_contradiction_clause,[],[f3383]) ).
fof(f3463,plain,
( e0 != op(e1,e3)
| spl3_21
| ~ spl3_31 ),
inference(superposition,[],[f295,f340]) ).
fof(f3465,plain,
( $false
| spl3_21
| ~ spl3_31
| ~ spl3_76 ),
inference(forward_subsumption_resolution,[],[f3463,f552]) ).
fof(f3466,plain,
( spl3_21
| ~ spl3_31
| ~ spl3_76 ),
inference(avatar_contradiction_clause,[],[f3465]) ).
cnf(s2,plain,
( ~ spl3_4
| ~ spl3_5
| ~ spl3_6 ),
inference(sat_conversion,[],[f228]) ).
cnf(s5,plain,
( ~ spl3_6
| ~ spl3_12
| ~ spl3_13 ),
inference(sat_conversion,[],[f259]) ).
cnf(s7,plain,
( ~ spl3_1
| ~ spl3_16
| ~ spl3_17 ),
inference(sat_conversion,[],[f277]) ).
cnf(s8,plain,
( ~ spl3_4
| ~ spl3_18
| ~ spl3_19 ),
inference(sat_conversion,[],[f286]) ).
cnf(s11,plain,
( ~ spl3_13
| ~ spl3_19
| ~ spl3_24 ),
inference(sat_conversion,[],[f309]) ).
cnf(s13,plain,
( ~ spl3_7
| ~ spl3_16
| ~ spl3_27 ),
inference(sat_conversion,[],[f323]) ).
cnf(s14,plain,
( ~ spl3_9
| ~ spl3_28
| ~ spl3_29 ),
inference(sat_conversion,[],[f332]) ).
cnf(s16,plain,
( ~ spl3_21
| ~ spl3_30
| ~ spl3_31 ),
inference(sat_conversion,[],[f342]) ).
cnf(s18,plain,
( ~ spl3_26
| ~ spl3_31
| ~ spl3_33 ),
inference(sat_conversion,[],[f352]) ).
cnf(s19,plain,
( ~ spl3_12
| ~ spl3_18
| ~ spl3_34 ),
inference(sat_conversion,[],[f357]) ).
cnf(s20,plain,
( ~ spl3_14
| ~ spl3_28
| ~ spl3_35 ),
inference(sat_conversion,[],[f362]) ).
cnf(s25,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_40 ),
inference(sat_conversion,[],[f387]) ).
cnf(s26,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_41 ),
inference(sat_conversion,[],[f392]) ).
cnf(s27,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_42 ),
inference(sat_conversion,[],[f397]) ).
cnf(s28,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_43 ),
inference(sat_conversion,[],[f402]) ).
cnf(s29,plain,
( ~ spl3_37
| spl3_44 ),
inference(sat_conversion,[],[f407]) ).
cnf(s30,plain,
( ~ spl3_37
| spl3_45 ),
inference(sat_conversion,[],[f412]) ).
cnf(s31,plain,
( ~ spl3_37
| spl3_46 ),
inference(sat_conversion,[],[f417]) ).
cnf(s32,plain,
( ~ spl3_37
| spl3_47 ),
inference(sat_conversion,[],[f422]) ).
cnf(s33,plain,
( ~ spl3_38
| spl3_48 ),
inference(sat_conversion,[],[f427]) ).
cnf(s34,plain,
( ~ spl3_38
| spl3_49 ),
inference(sat_conversion,[],[f432]) ).
cnf(s35,plain,
( ~ spl3_38
| spl3_50 ),
inference(sat_conversion,[],[f437]) ).
cnf(s36,plain,
( ~ spl3_38
| spl3_51 ),
inference(sat_conversion,[],[f442]) ).
cnf(s37,plain,
( ~ spl3_39
| spl3_52 ),
inference(sat_conversion,[],[f447]) ).
cnf(s38,plain,
( ~ spl3_39
| spl3_53 ),
inference(sat_conversion,[],[f452]) ).
cnf(s41,plain,
( spl3_56
| spl3_57
| spl3_58
| spl3_59 ),
inference(sat_conversion,[],[f479]) ).
cnf(s42,plain,
( spl3_56
| spl3_60
| spl3_61
| spl3_62 ),
inference(sat_conversion,[],[f492]) ).
cnf(s43,plain,
( spl3_30
| spl3_63
| spl3_64
| spl3_65 ),
inference(sat_conversion,[],[f505]) ).
cnf(s46,plain,
( spl3_22
| spl3_72
| spl3_73
| spl3_74 ),
inference(sat_conversion,[],[f544]) ).
cnf(s48,plain,
( spl3_26
| spl3_78
| spl3_79
| spl3_80 ),
inference(sat_conversion,[],[f570]) ).
cnf(s49,plain,
( spl3_28
| spl3_60
| spl3_81
| spl3_82 ),
inference(sat_conversion,[],[f579]) ).
cnf(s50,plain,
( spl3_28
| spl3_57
| spl3_83
| spl3_84 ),
inference(sat_conversion,[],[f588]) ).
cnf(s55,plain,
( spl3_15
| spl3_78
| spl3_94
| spl3_95 ),
inference(sat_conversion,[],[f637]) ).
cnf(s56,plain,
( spl3_15
| spl3_75
| spl3_96
| spl3_97 ),
inference(sat_conversion,[],[f646]) ).
cnf(s57,plain,
( spl3_18
| spl3_61
| spl3_83
| spl3_98 ),
inference(sat_conversion,[],[f651]) ).
cnf(s58,plain,
( spl3_18
| spl3_58
| spl3_81
| spl3_99 ),
inference(sat_conversion,[],[f656]) ).
cnf(s59,plain,
( spl3_5
| spl3_67
| spl3_88
| spl3_100 ),
inference(sat_conversion,[],[f661]) ).
cnf(s60,plain,
( spl3_5
| spl3_64
| spl3_86
| spl3_101 ),
inference(sat_conversion,[],[f666]) ).
cnf(s62,plain,
( spl3_70
| spl3_90
| spl3_102
| spl3_104 ),
inference(sat_conversion,[],[f680]) ).
cnf(s63,plain,
( spl3_13
| spl3_79
| spl3_96
| spl3_105 ),
inference(sat_conversion,[],[f685]) ).
cnf(s64,plain,
( spl3_13
| spl3_76
| spl3_94
| spl3_106 ),
inference(sat_conversion,[],[f690]) ).
cnf(s66,plain,
( spl3_16
| spl3_59
| spl3_82
| spl3_98 ),
inference(sat_conversion,[],[f692]) ).
cnf(s67,plain,
( spl3_2
| spl3_68
| spl3_89
| spl3_101 ),
inference(sat_conversion,[],[f693]) ).
cnf(s68,plain,
( spl3_2
| spl3_65
| spl3_87
| spl3_100 ),
inference(sat_conversion,[],[f694]) ).
cnf(s70,plain,
( spl3_8
| spl3_71
| spl3_91
| spl3_103 ),
inference(sat_conversion,[],[f696]) ).
cnf(s71,plain,
( spl3_80
| spl3_97
| spl3_106
| spl3_107 ),
inference(sat_conversion,[],[f701]) ).
cnf(s72,plain,
( spl3_77
| spl3_95
| spl3_105
| spl3_107 ),
inference(sat_conversion,[],[f702]) ).
cnf(s74,plain,
( spl3_60
| spl3_66
| spl3_72
| spl3_78 ),
inference(sat_conversion,[],[f704]) ).
cnf(s75,plain,
( spl3_61
| spl3_67
| spl3_73
| spl3_79 ),
inference(sat_conversion,[],[f705]) ).
cnf(s76,plain,
( spl3_62
| spl3_68
| spl3_74
| spl3_80 ),
inference(sat_conversion,[],[f706]) ).
cnf(s77,plain,
( spl3_57
| spl3_63
| spl3_69
| spl3_75 ),
inference(sat_conversion,[],[f707]) ).
cnf(s78,plain,
( spl3_10
| spl3_15
| spl3_28
| spl3_85 ),
inference(sat_conversion,[],[f708]) ).
cnf(s79,plain,
( spl3_83
| spl3_88
| spl3_92
| spl3_96 ),
inference(sat_conversion,[],[f709]) ).
cnf(s80,plain,
( spl3_84
| spl3_89
| spl3_93
| spl3_97 ),
inference(sat_conversion,[],[f710]) ).
cnf(s81,plain,
( spl3_58
| spl3_64
| spl3_70
| spl3_76 ),
inference(sat_conversion,[],[f711]) ).
cnf(s82,plain,
( spl3_81
| spl3_86
| spl3_90
| spl3_94 ),
inference(sat_conversion,[],[f712]) ).
cnf(s83,plain,
( spl3_5
| spl3_13
| spl3_18
| spl3_102 ),
inference(sat_conversion,[],[f713]) ).
cnf(s84,plain,
( spl3_99
| spl3_101
| spl3_104
| spl3_106 ),
inference(sat_conversion,[],[f714]) ).
cnf(s85,plain,
( spl3_59
| spl3_65
| spl3_71
| spl3_77 ),
inference(sat_conversion,[],[f715]) ).
cnf(s86,plain,
( spl3_82
| spl3_87
| spl3_91
| spl3_95 ),
inference(sat_conversion,[],[f716]) ).
cnf(s87,plain,
( spl3_98
| spl3_100
| spl3_103
| spl3_105 ),
inference(sat_conversion,[],[f717]) ).
cnf(s88,plain,
( spl3_2
| spl3_8
| spl3_16
| spl3_107 ),
inference(sat_conversion,[],[f718]) ).
cnf(s90,plain,
( ~ spl3_2
| ~ spl3_8 ),
inference(sat_conversion,[],[f724]) ).
cnf(s92,plain,
( ~ spl3_5
| ~ spl3_13 ),
inference(sat_conversion,[],[f731]) ).
cnf(s94,plain,
( ~ spl3_10
| ~ spl3_15 ),
inference(sat_conversion,[],[f738]) ).
cnf(s98,plain,
( ~ spl3_64
| ~ spl3_70 ),
inference(sat_conversion,[],[f756]) ).
cnf(s110,plain,
( ~ spl3_30
| ~ spl3_56 ),
inference(sat_conversion,[],[f805]) ).
cnf(s118,plain,
( ~ spl3_26
| ~ spl3_56 ),
inference(sat_conversion,[],[f838]) ).
cnf(s120,plain,
( ~ spl3_15
| ~ spl3_85 ),
inference(sat_conversion,[],[f850]) ).
cnf(s122,plain,
( ~ spl3_81
| ~ spl3_86 ),
inference(sat_conversion,[],[f857]) ).
cnf(s133,plain,
( ~ spl3_60
| ~ spl3_72 ),
inference(sat_conversion,[],[f902]) ).
cnf(s134,plain,
( ~ spl3_60
| ~ spl3_72 ),
inference(sat_conversion,[],[f904]) ).
cnf(s140,plain,
( ~ spl3_61
| ~ spl3_67 ),
inference(sat_conversion,[],[f934]) ).
cnf(s142,plain,
( ~ spl3_5
| ~ spl3_18 ),
inference(sat_conversion,[],[f941]) ).
cnf(s144,plain,
( ~ spl3_99
| ~ spl3_104 ),
inference(sat_conversion,[],[f952]) ).
cnf(s148,plain,
( ~ spl3_13
| ~ spl3_18 ),
inference(sat_conversion,[],[f967]) ).
cnf(s149,plain,
( ~ spl3_82
| ~ spl3_95 ),
inference(sat_conversion,[],[f974]) ).
cnf(s156,plain,
( ~ spl3_82
| ~ spl3_91 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s158,plain,
( ~ spl3_15
| ~ spl3_28 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s164,plain,
( ~ spl3_13
| ~ spl3_102 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s167,plain,
( ~ spl3_99
| ~ spl3_106 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s168,plain,
( ~ spl3_99
| ~ spl3_106 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s170,plain,
( ~ spl3_8
| ~ spl3_107 ),
inference(sat_conversion,[],[f1067]) ).
cnf(s172,plain,
( ~ spl3_15
| ~ spl3_96 ),
inference(sat_conversion,[],[f1080]) ).
cnf(s173,plain,
( ~ spl3_15
| ~ spl3_97 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s176,plain,
( ~ spl3_65
| ~ spl3_100 ),
inference(sat_conversion,[],[f1099]) ).
cnf(s177,plain,
( ~ spl3_56
| ~ spl3_57 ),
inference(sat_conversion,[],[f1106]) ).
cnf(s178,plain,
( ~ spl3_56
| ~ spl3_58 ),
inference(sat_conversion,[],[f1109]) ).
cnf(s179,plain,
( ~ spl3_56
| ~ spl3_59 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s180,plain,
( ~ spl3_72
| ~ spl3_90 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s182,plain,
( spl3_30
| ~ spl3_41
| ~ spl3_82 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s186,plain,
( ~ spl3_5
| ~ spl3_86 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s187,plain,
( ~ spl3_5
| ~ spl3_67 ),
inference(sat_conversion,[],[f1174]) ).
cnf(s188,plain,
( ~ spl3_5
| spl3_19
| ~ spl3_102 ),
inference(sat_conversion,[],[f1175]) ).
cnf(s189,plain,
( ~ spl3_5
| spl3_12
| ~ spl3_102 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s190,plain,
( spl3_5
| ~ spl3_45
| ~ spl3_72 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s192,plain,
( ~ spl3_47
| ~ spl3_80
| spl3_107 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s193,plain,
( spl3_2
| ~ spl3_15
| ~ spl3_49 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s196,plain,
( spl3_22
| ~ spl3_50
| ~ spl3_83 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s202,plain,
( ~ spl3_22
| ~ spl3_56 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s204,plain,
( ~ spl3_16
| ~ spl3_82 ),
inference(sat_conversion,[],[f1237]) ).
cnf(s205,plain,
( ~ spl3_16
| ~ spl3_99 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s207,plain,
( spl3_16
| ~ spl3_52
| ~ spl3_76 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s208,plain,
( ~ spl3_22
| ~ spl3_72 ),
inference(sat_conversion,[],[f1241]) ).
cnf(s209,plain,
( ~ spl3_22
| ~ spl3_69 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s212,plain,
( spl3_15
| ~ spl3_51
| ~ spl3_89 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s214,plain,
( spl3_10
| ~ spl3_46
| ~ spl3_67 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s216,plain,
( ~ spl3_2
| ~ spl3_65 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s218,plain,
( ~ spl3_10
| ~ spl3_93 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s219,plain,
( ~ spl3_13
| ~ spl3_105 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s220,plain,
( ~ spl3_26
| ~ spl3_76 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s222,plain,
( ~ spl3_26
| ~ spl3_80 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s223,plain,
( ~ spl3_26
| ~ spl3_79 ),
inference(sat_conversion,[],[f1284]) ).
cnf(s224,plain,
( ~ spl3_57
| ~ spl3_59 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s225,plain,
( ~ spl3_57
| ~ spl3_84 ),
inference(sat_conversion,[],[f1293]) ).
cnf(s226,plain,
( ~ spl3_57
| ~ spl3_83 ),
inference(sat_conversion,[],[f1294]) ).
cnf(s229,plain,
( ~ spl3_69
| ~ spl3_70 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s231,plain,
( ~ spl3_22
| ~ spl3_74 ),
inference(sat_conversion,[],[f1299]) ).
cnf(s234,plain,
( ~ spl3_67
| ~ spl3_68 ),
inference(sat_conversion,[],[f1300]) ).
cnf(s236,plain,
( ~ spl3_80
| ~ spl3_107 ),
inference(sat_conversion,[],[f1302]) ).
cnf(s241,plain,
( ~ spl3_86
| ~ spl3_101 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s242,plain,
( ~ spl3_13
| spl3_19
| ~ spl3_101 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s243,plain,
( ~ spl3_89
| ~ spl3_101 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s245,plain,
( spl3_3
| ~ spl3_16
| ~ spl3_59 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s250,plain,
( ~ spl3_58
| ~ spl3_59 ),
inference(sat_conversion,[],[f1332]) ).
cnf(s251,plain,
( ~ spl3_58
| ~ spl3_99 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s269,plain,
( ~ spl3_60
| ~ spl3_81 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s270,plain,
( ~ spl3_60
| ~ spl3_61 ),
inference(sat_conversion,[],[f1364]) ).
cnf(s271,plain,
( ~ spl3_61
| ~ spl3_83 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s273,plain,
( ~ spl3_66
| ~ spl3_86 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s274,plain,
( ~ spl3_66
| ~ spl3_85 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s276,plain,
( ~ spl3_66
| ~ spl3_67 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s280,plain,
( ~ spl3_74
| ~ spl3_104 ),
inference(sat_conversion,[],[f1403]) ).
cnf(s281,plain,
( ~ spl3_74
| ~ spl3_93 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s283,plain,
( ~ spl3_81
| ~ spl3_99 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s285,plain,
( ~ spl3_95
| ~ spl3_107 ),
inference(sat_conversion,[],[f1431]) ).
cnf(s286,plain,
( ~ spl3_95
| ~ spl3_105 ),
inference(sat_conversion,[],[f1432]) ).
cnf(s287,plain,
( ~ spl3_97
| ~ spl3_107 ),
inference(sat_conversion,[],[f1438]) ).
cnf(s293,plain,
( spl3_22
| ~ spl3_46
| ~ spl3_61 ),
inference(sat_conversion,[],[f1491]) ).
cnf(s296,plain,
( spl3_3
| ~ spl3_8
| ~ spl3_98 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s304,plain,
( spl3_6
| ~ spl3_13
| ~ spl3_99 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s307,plain,
( ~ spl3_12
| ~ spl3_19
| spl3_88 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s308,plain,
( spl3_16
| ~ spl3_26
| ~ spl3_44 ),
inference(sat_conversion,[],[f1512]) ).
cnf(s309,plain,
( ~ spl3_8
| ~ spl3_74 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s310,plain,
( ~ spl3_8
| ~ spl3_13
| spl3_43 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s311,plain,
( ~ spl3_16
| ~ spl3_26
| spl3_44 ),
inference(sat_conversion,[],[f1515]) ).
cnf(s312,plain,
( spl3_5
| ~ spl3_10
| ~ spl3_49 ),
inference(sat_conversion,[],[f1516]) ).
cnf(s313,plain,
( ~ spl3_61
| ~ spl3_98 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s314,plain,
( ~ spl3_82
| ~ spl3_98 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s317,plain,
( ~ spl3_5
| ~ spl3_88 ),
inference(sat_conversion,[],[f1519]) ).
cnf(s319,plain,
( ~ spl3_26
| ~ spl3_78 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s323,plain,
( spl3_18
| ~ spl3_52
| ~ spl3_70 ),
inference(sat_conversion,[],[f1523]) ).
cnf(s328,plain,
( ~ spl3_61
| ~ spl3_62 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s329,plain,
( ~ spl3_18
| ~ spl3_61 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s333,plain,
( ~ spl3_18
| ~ spl3_98 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s341,plain,
( ~ spl3_73
| ~ spl3_103 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s342,plain,
( ~ spl3_73
| ~ spl3_92 ),
inference(sat_conversion,[],[f1574]) ).
cnf(s343,plain,
( ~ spl3_73
| ~ spl3_74 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s346,plain,
( ~ spl3_94
| ~ spl3_95 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s350,plain,
( ~ spl3_45
| ~ spl3_66
| spl3_85 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s351,plain,
( ~ spl3_48
| spl3_56
| ~ spl3_57 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s352,plain,
( ~ spl3_51
| ~ spl3_97
| spl3_107 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s353,plain,
( spl3_2
| ~ spl3_53
| ~ spl3_94 ),
inference(sat_conversion,[],[f1645]) ).
cnf(s357,plain,
( ~ spl3_15
| ~ spl3_94 ),
inference(sat_conversion,[],[f1648]) ).
cnf(s359,plain,
( spl3_10
| ~ spl3_50
| ~ spl3_88 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s361,plain,
( ~ spl3_10
| ~ spl3_72 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s377,plain,
( ~ spl3_53
| spl3_85
| ~ spl3_86 ),
inference(sat_conversion,[],[f1691]) ).
cnf(s388,plain,
( ~ spl3_105
| ~ spl3_107 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s390,plain,
( ~ spl3_18
| ~ spl3_58 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s391,plain,
( spl3_8
| ~ spl3_42
| ~ spl3_105 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s398,plain,
( ~ spl3_5
| ~ spl3_100 ),
inference(sat_conversion,[],[f1714]) ).
cnf(s399,plain,
( ~ spl3_5
| ~ spl3_101 ),
inference(sat_conversion,[],[f1715]) ).
cnf(s401,plain,
( ~ spl3_13
| ~ spl3_106 ),
inference(sat_conversion,[],[f1717]) ).
cnf(s406,plain,
( spl3_4
| ~ spl3_19
| ~ spl3_96 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s409,plain,
( ~ spl3_13
| ~ spl3_94 ),
inference(sat_conversion,[],[f1721]) ).
cnf(s413,plain,
( ~ spl3_52
| spl3_56
| ~ spl3_58 ),
inference(sat_conversion,[],[f1732]) ).
cnf(s415,plain,
( ~ spl3_63
| ~ spl3_65 ),
inference(sat_conversion,[],[f1747]) ).
cnf(s418,plain,
( ~ spl3_63
| ~ spl3_85 ),
inference(sat_conversion,[],[f1750]) ).
cnf(s420,plain,
( ~ spl3_67
| ~ spl3_100 ),
inference(sat_conversion,[],[f1751]) ).
cnf(s426,plain,
( ~ spl3_28
| ~ spl3_82 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s427,plain,
( ~ spl3_28
| ~ spl3_84 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s435,plain,
( ~ spl3_96
| ~ spl3_105 ),
inference(sat_conversion,[],[f1811]) ).
cnf(s436,plain,
( ~ spl3_96
| ~ spl3_97 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s445,plain,
( ~ spl3_22
| ~ spl3_73 ),
inference(sat_conversion,[],[f1821]) ).
cnf(s446,plain,
( ~ spl3_22
| ~ spl3_71 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s449,plain,
( ~ spl3_22
| ~ spl3_71 ),
inference(sat_conversion,[],[f1825]) ).
cnf(s451,plain,
( ~ spl3_28
| ~ spl3_60 ),
inference(sat_conversion,[],[f1827]) ).
cnf(s453,plain,
( ~ spl3_73
| ~ spl3_102 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s455,plain,
( spl3_22
| ~ spl3_42
| ~ spl3_98 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s458,plain,
( ~ spl3_16
| ~ spl3_98 ),
inference(sat_conversion,[],[f1833]) ).
cnf(s468,plain,
( ~ spl3_68
| ~ spl3_101 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s472,plain,
( ~ spl3_5
| ~ spl3_19
| spl3_86 ),
inference(sat_conversion,[],[f1903]) ).
cnf(s509,plain,
( spl3_18
| ~ spl3_40
| ~ spl3_71 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s516,plain,
( spl3_13
| ~ spl3_47
| ~ spl3_74 ),
inference(sat_conversion,[],[f2027]) ).
cnf(s521,plain,
( ~ spl3_41
| spl3_85
| ~ spl3_87 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s530,plain,
( ~ spl3_2
| ~ spl3_87 ),
inference(sat_conversion,[],[f2033]) ).
cnf(s532,plain,
( ~ spl3_2
| ~ spl3_101 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s541,plain,
( ~ spl3_5
| spl3_6
| ~ spl3_81 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s546,plain,
( ~ spl3_5
| ~ spl3_64 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s549,plain,
( ~ spl3_10
| ~ spl3_90 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s593,plain,
( spl3_9
| ~ spl3_29
| ~ spl3_94 ),
inference(sat_conversion,[],[f2095]) ).
cnf(s618,plain,
( ~ spl3_75
| ~ spl3_77 ),
inference(sat_conversion,[],[f2138]) ).
cnf(s622,plain,
( ~ spl3_77
| ~ spl3_107 ),
inference(sat_conversion,[],[f2152]) ).
cnf(s627,plain,
( ~ spl3_106
| ~ spl3_107 ),
inference(sat_conversion,[],[f2198]) ).
cnf(s632,plain,
( ~ spl3_8
| spl3_13
| ~ spl3_43 ),
inference(sat_conversion,[],[f2209]) ).
cnf(s635,plain,
( ~ spl3_97
| ~ spl3_106 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s645,plain,
( spl3_26
| ~ spl3_47
| ~ spl3_62 ),
inference(sat_conversion,[],[f2220]) ).
cnf(s662,plain,
( ~ spl3_8
| ~ spl3_104 ),
inference(sat_conversion,[],[f2222]) ).
cnf(s663,plain,
( ~ spl3_2
| spl3_27
| ~ spl3_91 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s667,plain,
( ~ spl3_30
| spl3_31
| ~ spl3_72 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s668,plain,
( ~ spl3_30
| ~ spl3_64 ),
inference(sat_conversion,[],[f2254]) ).
cnf(s669,plain,
( ~ spl3_30
| ~ spl3_68 ),
inference(sat_conversion,[],[f2255]) ).
cnf(s680,plain,
( ~ spl3_10
| ~ spl3_91 ),
inference(sat_conversion,[],[f2261]) ).
cnf(s686,plain,
( ~ spl3_71
| ~ spl3_91 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s687,plain,
( ~ spl3_75
| ~ spl3_97 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s690,plain,
( ~ spl3_2
| ~ spl3_68 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s703,plain,
( spl3_1
| ~ spl3_27
| ~ spl3_104 ),
inference(sat_conversion,[],[f2362]) ).
cnf(s707,plain,
( ~ spl3_4
| ~ spl3_12 ),
inference(sat_conversion,[],[f2385]) ).
cnf(s709,plain,
( ~ spl3_46
| ~ spl3_73
| spl3_102 ),
inference(sat_conversion,[],[f2399]) ).
cnf(s712,plain,
( ~ spl3_28
| ~ spl3_83 ),
inference(sat_conversion,[],[f2414]) ).
cnf(s714,plain,
( ~ spl3_28
| ~ spl3_81 ),
inference(sat_conversion,[],[f2415]) ).
cnf(s735,plain,
( spl3_28
| ~ spl3_52
| ~ spl3_64 ),
inference(sat_conversion,[],[f2420]) ).
cnf(s742,plain,
( spl3_49
| ~ spl3_85 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s746,plain,
( ~ spl3_85
| ~ spl3_89 ),
inference(sat_conversion,[],[f2469]) ).
cnf(s747,plain,
( ~ spl3_85
| ~ spl3_88 ),
inference(sat_conversion,[],[f2470]) ).
cnf(s748,plain,
( ~ spl3_28
| ~ spl3_85 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s753,plain,
( spl3_4
| ~ spl3_13
| ~ spl3_102 ),
inference(sat_conversion,[],[f2499]) ).
cnf(s762,plain,
( ~ spl3_42
| spl3_102
| ~ spl3_103 ),
inference(sat_conversion,[],[f2504]) ).
cnf(s776,plain,
( ~ spl3_85
| ~ spl3_87 ),
inference(sat_conversion,[],[f2508]) ).
cnf(s779,plain,
( ~ spl3_13
| ~ spl3_96 ),
inference(sat_conversion,[],[f2510]) ).
cnf(s782,plain,
( ~ spl3_102
| ~ spl3_103 ),
inference(sat_conversion,[],[f2511]) ).
cnf(s811,plain,
( ~ spl3_70
| ~ spl3_71 ),
inference(sat_conversion,[],[f2515]) ).
cnf(s822,plain,
( ~ spl3_80
| ~ spl3_106 ),
inference(sat_conversion,[],[f2516]) ).
cnf(s827,plain,
( ~ spl3_92
| ~ spl3_102 ),
inference(sat_conversion,[],[f2517]) ).
cnf(s842,plain,
( ~ spl3_18
| spl3_19
| ~ spl3_64 ),
inference(sat_conversion,[],[f2519]) ).
cnf(s869,plain,
( ~ spl3_6
| ~ spl3_18
| spl3_58 ),
inference(sat_conversion,[],[f2632]) ).
cnf(s875,plain,
( ~ spl3_72
| ~ spl3_91 ),
inference(sat_conversion,[],[f2652]) ).
cnf(s880,plain,
( ~ spl3_16
| ~ spl3_84 ),
inference(sat_conversion,[],[f2653]) ).
cnf(s884,plain,
( spl3_16
| ~ spl3_48
| ~ spl3_75 ),
inference(sat_conversion,[],[f2654]) ).
cnf(s885,plain,
( ~ spl3_3
| ~ spl3_16
| spl3_59 ),
inference(sat_conversion,[],[f2655]) ).
cnf(s886,plain,
( ~ spl3_3
| ~ spl3_8
| spl3_98 ),
inference(sat_conversion,[],[f2657]) ).
cnf(s890,plain,
( ~ spl3_28
| spl3_35
| ~ spl3_75 ),
inference(sat_conversion,[],[f2658]) ).
cnf(s894,plain,
( ~ spl3_28
| spl3_30
| ~ spl3_49 ),
inference(sat_conversion,[],[f2659]) ).
cnf(s899,plain,
( ~ spl3_30
| ~ spl3_67 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s901,plain,
( ~ spl3_30
| ~ spl3_65 ),
inference(sat_conversion,[],[f2663]) ).
cnf(s903,plain,
( ~ spl3_16
| ~ spl3_62 ),
inference(sat_conversion,[],[f2664]) ).
cnf(s910,plain,
( spl3_28
| ~ spl3_48
| ~ spl3_63 ),
inference(sat_conversion,[],[f2665]) ).
cnf(s950,plain,
( ~ spl3_76
| ~ spl3_77 ),
inference(sat_conversion,[],[f2676]) ).
cnf(s951,plain,
( ~ spl3_78
| ~ spl3_80 ),
inference(sat_conversion,[],[f2677]) ).
cnf(s965,plain,
( ~ spl3_90
| ~ spl3_91 ),
inference(sat_conversion,[],[f2680]) ).
cnf(s966,plain,
( ~ spl3_18
| spl3_34
| ~ spl3_76 ),
inference(sat_conversion,[],[f2681]) ).
cnf(s968,plain,
( ~ spl3_8
| ~ spl3_103 ),
inference(sat_conversion,[],[f2682]) ).
cnf(s989,plain,
( ~ spl3_16
| spl3_26
| ~ spl3_43 ),
inference(sat_conversion,[],[f2819]) ).
cnf(s995,plain,
( ~ spl3_28
| spl3_29
| ~ spl3_69 ),
inference(sat_conversion,[],[f2821]) ).
cnf(s996,plain,
( ~ spl3_28
| ~ spl3_35
| spl3_75 ),
inference(sat_conversion,[],[f2822]) ).
cnf(s1007,plain,
( ~ spl3_71
| ~ spl3_103 ),
inference(sat_conversion,[],[f2825]) ).
cnf(s1030,plain,
( ~ spl3_16
| spl3_17
| ~ spl3_65 ),
inference(sat_conversion,[],[f2837]) ).
cnf(s1040,plain,
( ~ spl3_50
| ~ spl3_92
| spl3_102 ),
inference(sat_conversion,[],[f2888]) ).
cnf(s1045,plain,
( spl3_5
| ~ spl3_53
| ~ spl3_90 ),
inference(sat_conversion,[],[f2935]) ).
cnf(s1059,plain,
( ~ spl3_76
| ~ spl3_106 ),
inference(sat_conversion,[],[f2936]) ).
cnf(s1061,plain,
( ~ spl3_18
| ~ spl3_81 ),
inference(sat_conversion,[],[f2937]) ).
cnf(s1063,plain,
( ~ spl3_18
| ~ spl3_83 ),
inference(sat_conversion,[],[f2938]) ).
cnf(s1072,plain,
( spl3_6
| ~ spl3_18
| ~ spl3_102 ),
inference(sat_conversion,[],[f2939]) ).
cnf(s1074,plain,
( spl3_7
| ~ spl3_27
| ~ spl3_101 ),
inference(sat_conversion,[],[f2940]) ).
cnf(s1075,plain,
( ~ spl3_16
| ~ spl3_27
| spl3_71 ),
inference(sat_conversion,[],[f2941]) ).
cnf(s1076,plain,
( ~ spl3_16
| spl3_27
| ~ spl3_71 ),
inference(sat_conversion,[],[f2942]) ).
cnf(s1082,plain,
( ~ spl3_30
| ~ spl3_67 ),
inference(sat_conversion,[],[f2974]) ).
cnf(s1084,plain,
( spl3_12
| ~ spl3_34
| ~ spl3_100 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s1085,plain,
( spl3_18
| ~ spl3_48
| ~ spl3_69 ),
inference(sat_conversion,[],[f2976]) ).
cnf(s1087,plain,
( spl3_8
| ~ spl3_50
| ~ spl3_96 ),
inference(sat_conversion,[],[f2977]) ).
cnf(s1126,plain,
( spl3_12
| ~ spl3_13
| ~ spl3_67
| ~ spl3_99 ),
inference(sat_conversion,[],[f2978]) ).
cnf(s1133,plain,
( ~ spl3_15
| ~ spl3_95 ),
inference(sat_conversion,[],[f2979]) ).
cnf(s1153,plain,
( ~ spl3_26
| spl3_31
| ~ spl3_74 ),
inference(sat_conversion,[],[f2981]) ).
cnf(s1178,plain,
( ~ spl3_8
| ~ spl3_93 ),
inference(sat_conversion,[],[f2985]) ).
cnf(s1182,plain,
( spl3_3
| ~ spl3_16
| ~ spl3_107 ),
inference(sat_conversion,[],[f2986]) ).
cnf(s1184,plain,
( spl3_15
| ~ spl3_47
| ~ spl3_68 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s1210,plain,
( spl3_1
| ~ spl3_17
| ~ spl3_93 ),
inference(sat_conversion,[],[f3104]) ).
cnf(s1212,plain,
( ~ spl3_40
| spl3_56
| ~ spl3_59 ),
inference(sat_conversion,[],[f3136]) ).
cnf(s1224,plain,
( spl3_14
| ~ spl3_35
| ~ spl3_91 ),
inference(sat_conversion,[],[f3140]) ).
cnf(s1233,plain,
( spl3_28
| ~ spl3_40
| ~ spl3_65 ),
inference(sat_conversion,[],[f3142]) ).
cnf(s1246,plain,
( ~ spl3_13
| ~ spl3_79 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s1247,plain,
( ~ spl3_88
| ~ spl3_100 ),
inference(sat_conversion,[],[f3145]) ).
cnf(s1282,plain,
( ~ spl3_15
| ~ spl3_78 ),
inference(sat_conversion,[],[f3147]) ).
cnf(s1296,plain,
( spl3_2
| ~ spl3_45
| ~ spl3_78 ),
inference(sat_conversion,[],[f3149]) ).
cnf(s1321,plain,
( ~ spl3_64
| ~ spl3_86 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s1340,plain,
( ~ spl3_2
| ~ spl3_100 ),
inference(sat_conversion,[],[f3225]) ).
cnf(s1341,plain,
( ~ spl3_63
| ~ spl3_64 ),
inference(sat_conversion,[],[f3226]) ).
cnf(s1368,plain,
( ~ spl3_19
| spl3_24
| ~ spl3_83 ),
inference(sat_conversion,[],[f3228]) ).
cnf(s1374,plain,
( spl3_16
| ~ spl3_40
| ~ spl3_77 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s1377,plain,
( spl3_18
| ~ spl3_22
| ~ spl3_44 ),
inference(sat_conversion,[],[f3232]) ).
cnf(s1379,plain,
( ~ spl3_28
| ~ spl3_57 ),
inference(sat_conversion,[],[f3233]) ).
cnf(s1404,plain,
( ~ spl3_79
| ~ spl3_80 ),
inference(sat_conversion,[],[f3234]) ).
cnf(s1441,plain,
( spl3_30
| ~ spl3_45
| ~ spl3_60 ),
inference(sat_conversion,[],[f3353]) ).
cnf(s1443,plain,
( spl3_4
| ~ spl3_6
| ~ spl3_79 ),
inference(sat_conversion,[],[f3355]) ).
cnf(s1449,plain,
( ~ spl3_31
| spl3_33
| ~ spl3_64 ),
inference(sat_conversion,[],[f3356]) ).
cnf(s1454,plain,
( spl3_30
| ~ spl3_53
| ~ spl3_81 ),
inference(sat_conversion,[],[f3359]) ).
cnf(s1477,plain,
( ~ spl3_92
| ~ spl3_93 ),
inference(sat_conversion,[],[f3360]) ).
cnf(s1483,plain,
( spl3_28
| ~ spl3_30
| ~ spl3_44 ),
inference(sat_conversion,[],[f3384]) ).
cnf(s1494,plain,
( spl3_21
| ~ spl3_31
| ~ spl3_76 ),
inference(sat_conversion,[],[f3466]) ).
cnf(s1495,plain,
( spl3_39
| spl3_38
| spl3_37
| spl3_59
| spl3_30
| spl3_22
| spl3_16 ),
inference(rat,[],[s66,s182,s455,s26,s27]) ).
cnf(s1496,plain,
( ~ spl3_39
| spl3_106
| spl3_16
| spl3_13
| spl3_2 ),
inference(rat,[],[s64,s207,s353,s37,s38]) ).
cnf(s1497,plain,
( spl3_38
| spl3_37
| spl3_39
| spl3_16
| spl3_30
| spl3_22 ),
inference(rat,[],[s1212,s179,s25,s1495]) ).
cnf(s1498,plain,
( ~ spl3_50
| spl3_22
| spl3_92
| spl3_10
| spl3_8 ),
inference(rat,[],[s79,s359,s1087,s196]) ).
cnf(s1499,plain,
( ~ spl3_37
| spl3_22
| spl3_73
| spl3_13
| spl3_5 ),
inference(rat,[],[s46,s190,s516,s30,s32]) ).
cnf(s1500,plain,
( spl3_22
| spl3_18
| spl3_39
| spl3_77
| spl3_16
| spl3_13
| spl3_10
| spl3_8
| spl3_5 ),
inference(rat,[],[s1212,s85,s110,s901,s509,s1497,s25,s1499,s35,s1498,s827,s453,s83]) ).
cnf(s1501,plain,
( ~ spl3_40
| spl3_35
| spl3_56
| spl3_69
| spl3_71
| spl3_77 ),
inference(rat,[],[s77,s890,s1379,s1233,s415,s85,s1212]) ).
cnf(s1502,plain,
( ~ spl3_38
| spl3_97
| spl3_16
| spl3_15
| spl3_8 ),
inference(rat,[],[s56,s884,s1087,s33,s35]) ).
cnf(s1503,plain,
( spl3_22
| spl3_37
| spl3_38
| spl3_39
| spl3_105
| spl3_77
| spl3_16
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_6
| spl3_5 ),
inference(rat,[],[s81,s966,s811,s1084,s85,s87,s1212,s762,s110,s668,s901,s390,s1072,s455,s1497,s1500,s27,s25]) ).
cnf(s1504,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_105
| spl3_77
| spl3_16
| spl3_14
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_6
| spl3_5 ),
inference(rat,[],[s762,s782,s70,s1224,s1501,s202,s209,s449,s1503,s25,s27]) ).
cnf(s1505,plain,
( spl3_16
| spl3_15
| spl3_14
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_6
| spl3_5
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s516,s1184,s29,s32,s1504,s1502,s1496,s236,s287,s388,s622,s627,s88]) ).
cnf(s1506,plain,
( ~ spl3_103
| ~ spl3_42 ),
inference(rat,[],[s762,s782]) ).
cnf(s1507,plain,
( ~ spl3_71
| spl3_19
| spl3_76
| ~ spl3_40 ),
inference(rat,[],[s81,s842,s390,s509,s811]) ).
cnf(s1508,plain,
( spl3_73
| spl3_22
| spl3_72
| spl3_67
| spl3_97
| ~ spl3_26
| spl3_84
| spl3_5 ),
inference(rat,[],[s60,s1449,s243,s273,s18,s80,s74,s1153,s281,s270,s46,s75,s319,s223]) ).
cnf(s1509,plain,
( ~ spl3_73
| spl3_65
| spl3_19
| spl3_56
| spl3_80
| spl3_59
| spl3_62
| spl3_15
| spl3_13
| spl3_10
| spl3_5 ),
inference(rat,[],[s78,s418,s1379,s43,s41,s669,s842,s390,s76,s83,s343,s453]) ).
cnf(s1510,plain,
( spl3_39
| spl3_38
| spl3_37
| spl3_59
| ~ spl3_16
| spl3_15
| spl3_13
| spl3_10
| spl3_8
| spl3_5
| spl3_4 ),
inference(rat,[],[s1377,s329,s1508,s75,s1509,s875,s70,s1507,s176,s420,s87,s1506,s406,s436,s63,s118,s220,s222,s223,s311,s391,s989,s25,s27,s28,s903,s880,s458]) ).
cnf(s1511,plain,
( ~ spl3_56
| spl3_18
| ~ spl3_53
| spl3_99 ),
inference(rat,[],[s1454,s58,s110,s178]) ).
cnf(s1512,plain,
( spl3_18
| ~ spl3_39
| spl3_59
| ~ spl3_16
| spl3_7
| spl3_5 ),
inference(rat,[],[s85,s1076,s950,s1074,s81,s901,s60,s735,s1454,s122,s1379,s58,s41,s413,s1511,s323,s205,s38,s37]) ).
cnf(s1513,plain,
( ~ spl3_39
| spl3_59
| ~ spl3_16
| spl3_7
| spl3_5
| spl3_2 ),
inference(rat,[],[s176,s59,s43,s234,s669,s67,s418,s746,s747,s377,s241,s1321,s82,s1061,s1512,s353,s1045,s38]) ).
cnf(s1514,plain,
( ~ spl3_38
| spl3_59
| spl3_107
| ~ spl3_16
| spl3_15
| spl3_10
| spl3_8
| spl3_1 ),
inference(rat,[],[s446,s85,s1030,s1498,s618,s1210,s1477,s56,s80,s1087,s352,s212,s35,s36,s880]) ).
cnf(s1515,plain,
( spl3_15
| spl3_14
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s76,s192,s516,s1184,s32,s1510,s1514,s1513,s245,s903,s1182,s1505]) ).
cnf(s1516,plain,
( ~ spl3_37
| ~ spl3_15
| spl3_5 ),
inference(rat,[],[s1441,s74,s1483,s350,s190,s29,s30,s1282,s158,s120]) ).
cnf(s1517,plain,
( spl3_16
| spl3_37
| spl3_38
| spl3_14
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_6
| spl3_5
| spl3_2 ),
inference(rat,[],[s1504,s1496,s388,s622,s627,s88]) ).
cnf(s1518,plain,
( spl3_14
| spl3_13
| spl3_1
| spl3_12
| spl3_10
| spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s63,s223,s391,s989,s27,s28,s1513,s245,s1517,s1516,s34,s172,s193,s1515]) ).
cnf(s1519,plain,
( spl3_38
| spl3_37
| spl3_39
| spl3_105
| spl3_77
| spl3_16
| ~ spl3_14
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_6
| spl3_5 ),
inference(rat,[],[s1233,s85,s20,s1212,s1501,s202,s209,s449,s25,s1503]) ).
cnf(s1520,plain,
( ~ spl3_38
| spl3_16
| spl3_8
| spl3_2 ),
inference(rat,[],[s193,s1502,s34,s287,s88]) ).
cnf(s1521,plain,
( spl3_16
| ~ spl3_14
| spl3_13
| spl3_12
| spl3_10
| spl3_8
| spl3_6
| spl3_5
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s516,s1184,s1516,s29,s32,s1519,s1520,s1496,s236,s388,s622,s627,s88]) ).
cnf(s1522,plain,
( spl3_38
| spl3_37
| spl3_59
| spl3_4
| ~ spl3_16
| spl3_39
| spl3_13
| spl3_10
| spl3_8
| spl3_5 ),
inference(rat,[],[s223,s63,s989,s391,s172,s28,s27,s1510]) ).
cnf(s1523,plain,
( ~ spl3_38
| spl3_59
| spl3_107
| ~ spl3_16
| spl3_10
| spl3_8
| spl3_2
| spl3_1 ),
inference(rat,[],[s193,s1514,s34]) ).
cnf(s1524,plain,
( spl3_13
| spl3_12
| spl3_1
| spl3_2
| spl3_10
| spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3 ),
inference(rat,[],[s76,s192,s516,s1184,s1516,s32,s1522,s1523,s1513,s245,s903,s1182,s1521,s1518]) ).
cnf(s1526,plain,
( ~ spl3_59
| ~ spl3_40 ),
inference(rat,[],[s1212,s179]) ).
cnf(s1527,plain,
( spl3_39
| spl3_37
| spl3_77
| spl3_38
| spl3_16
| spl3_18
| spl3_8 ),
inference(rat,[],[s20,s1224,s1501,s202,s209,s455,s1233,s66,s85,s1526,s156,s70,s509,s1506,s25,s27]) ).
cnf(s1528,plain,
( ~ spl3_39
| spl3_16
| spl3_18
| spl3_99 ),
inference(rat,[],[s668,s1454,s81,s58,s323,s413,s207,s1511,s37,s38]) ).
cnf(s1529,plain,
( spl3_16
| spl3_18
| spl3_99
| spl3_94
| spl3_8
| spl3_5
| spl3_2 ),
inference(rat,[],[s55,s1296,s1516,s30,s1527,s1528,s285,s622,s1520,s88]) ).
cnf(s1530,plain,
( spl3_28
| spl3_15
| spl3_72
| spl3_90
| spl3_65
| ~ spl3_44
| spl3_78
| spl3_94
| spl3_10 ),
inference(rat,[],[s82,s269,s1321,s74,s43,s274,s418,s1483,s78]) ).
cnf(s1531,plain,
( spl3_15
| spl3_72
| spl3_10
| spl3_90
| spl3_65
| ~ spl3_44
| spl3_78
| spl3_94 ),
inference(rat,[],[s273,s74,s82,s451,s714,s1530]) ).
cnf(s1532,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_107
| ~ spl3_16
| spl3_18
| spl3_105
| spl3_106
| spl3_94
| spl3_10
| spl3_8 ),
inference(rat,[],[s1531,s173,s71,s875,s965,s176,s222,s311,s319,s70,s87,s989,s509,s1506,s28,s25,s27,s458]) ).
cnf(s1533,plain,
( ~ spl3_13
| spl3_10
| spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s293,s75,s1377,s709,s214,s29,s31,s1532,s1523,s1513,s245,s1182,s1529,s148,s219,s304,s401,s409,s753,s1246]) ).
cnf(s1534,plain,
( spl3_37
| spl3_39
| spl3_105
| spl3_77
| spl3_38
| spl3_16
| ~ spl3_12
| spl3_8 ),
inference(rat,[],[s1507,s85,s307,s176,s1247,s87,s966,s1526,s1506,s19,s333,s25,s27,s1527]) ).
cnf(s1535,plain,
( spl3_16
| ~ spl3_12
| spl3_13
| spl3_8
| spl3_5
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s516,s1184,s1516,s29,s32,s1534,s1496,s236,s388,s622,s627,s1520,s88]) ).
cnf(s1536,plain,
( spl3_13
| spl3_10
| spl3_1
| spl3_2
| spl3_3
| spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_4 ),
inference(rat,[],[s76,s192,s516,s1184,s1516,s32,s1522,s1523,s1513,s245,s903,s1182,s1535,s1524]) ).
cnf(s1537,plain,
( spl3_10
| spl3_8
| spl3_1
| spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s1536,s1533]) ).
cnf(s1538,plain,
( spl3_37
| spl3_39
| spl3_95
| spl3_105
| spl3_77
| spl3_12
| spl3_16
| spl3_38
| spl3_85
| spl3_91
| spl3_8 ),
inference(rat,[],[s668,s81,s966,s182,s811,s1084,s86,s70,s87,s521,s1506,s333,s390,s26,s27,s1527]) ).
cnf(s1539,plain,
( spl3_16
| spl3_13
| spl3_38
| spl3_85
| spl3_15
| spl3_91
| spl3_8
| spl3_5
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s516,s1184,s29,s32,s1538,s1496,s236,s285,s388,s622,s627,s1535,s88]) ).
cnf(s1542,plain,
( spl3_37
| spl3_39
| spl3_18
| spl3_38
| spl3_91
| spl3_8 ),
inference(rat,[],[s70,s509,s1506,s25,s27]) ).
cnf(s1543,plain,
( ~ spl3_37
| spl3_85
| spl3_72
| spl3_2 ),
inference(rat,[],[s1483,s1441,s451,s74,s350,s1296,s29,s30]) ).
cnf(s1544,plain,
( ~ spl3_16
| spl3_37
| spl3_38
| spl3_90
| spl3_91
| spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s703,s62,s1076,s811,s70,s1506,s1072,s27,s1542,s1513,s245]) ).
cnf(s1545,plain,
( spl3_8
| spl3_7
| spl3_1
| spl3_2
| spl3_6
| spl3_5
| spl3_4
| spl3_3 ),
inference(rat,[],[s1529,s148,s304,s409,s1539,s1544,s1543,s34,s742,s94,s312,s361,s549,s680,s1537]) ).
cnf(s1546,plain,
( ~ spl3_39
| spl3_16
| spl3_13
| spl3_104
| spl3_6
| spl3_5
| spl3_2 ),
inference(rat,[],[s176,s59,s43,s234,s669,s67,s418,s746,s747,s377,s241,s98,s82,s62,s1061,s1072,s1528,s168,s353,s1045,s1496,s38]) ).
cnf(s1547,plain,
( ~ spl3_38
| spl3_16
| spl3_107
| spl3_98
| spl3_103
| spl3_93
| spl3_4
| spl3_2 ),
inference(rat,[],[s19,s1084,s966,s81,s842,s390,s1085,s229,s77,s910,s87,s225,s427,s406,s435,s80,s56,s212,s884,s193,s352,s33,s34,s36]) ).
cnf(s1548,plain,
( spl3_16
| spl3_43
| spl3_13
| spl3_107
| spl3_98
| spl3_74
| spl3_104
| spl3_103
| spl3_93
| spl3_6
| spl3_5
| spl3_4
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s192,s1184,s1516,s29,s32,s28,s1547,s1546]) ).
cnf(s1549,plain,
( ~ spl3_38
| spl3_84
| ~ spl3_8
| spl3_2 ),
inference(rat,[],[s212,s80,s193,s352,s34,s36,s1178,s170]) ).
cnf(s1550,plain,
( spl3_13
| ~ spl3_8
| spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s76,s192,s1184,s1516,s32,s28,s1549,s1513,s245,s880,s903,s1548,s632,s1178,s968,s662,s309,s296,s170]) ).
cnf(s1551,plain,
( spl3_7
| spl3_6
| spl3_1
| spl3_2
| spl3_3
| spl3_5
| spl3_4 ),
inference(rat,[],[s85,s509,s1526,s1374,s25,s1528,s32,s989,s192,s222,s35,s76,s1040,s328,s79,s57,s1368,s11,s176,s1247,s242,s468,s87,s84,s310,s148,s219,s304,s401,s753,s779,s1550,s170,s296,s309,s662,s968,s1545]) ).
cnf(s1552,plain,
( spl3_37
| spl3_39
| spl3_105
| spl3_77
| spl3_12
| spl3_38
| spl3_16
| spl3_8 ),
inference(rat,[],[s81,s811,s668,s966,s85,s182,s1084,s176,s66,s87,s333,s390,s1526,s1506,s1527,s25,s26,s27]) ).
cnf(s1553,plain,
( spl3_16
| spl3_13
| spl3_8
| spl3_5
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s516,s1184,s1516,s29,s32,s1552,s1496,s236,s388,s622,s627,s1535,s1520,s88]) ).
cnf(s1554,plain,
( spl3_39
| spl3_38
| spl3_37
| spl3_71
| spl3_59
| ~ spl3_16
| spl3_13
| spl3_8
| spl3_5
| spl3_4 ),
inference(rat,[],[s70,s1506,s680,s27,s1522]) ).
cnf(s1555,plain,
( spl3_18
| ~ spl3_39
| spl3_71
| spl3_99
| spl3_59 ),
inference(rat,[],[s950,s85,s81,s901,s735,s1454,s714,s58,s413,s323,s1511,s38,s37]) ).
cnf(s1556,plain,
( ~ spl3_39
| spl3_71
| spl3_99
| spl3_59
| spl3_5
| spl3_2 ),
inference(rat,[],[s176,s59,s43,s234,s669,s67,s418,s746,s747,s377,s241,s1321,s82,s1061,s1555,s353,s1045,s38]) ).
cnf(s1557,plain,
( ~ spl3_38
| spl3_59
| spl3_107
| ~ spl3_16
| spl3_8
| spl3_5
| spl3_2
| spl3_1 ),
inference(rat,[],[s312,s1523,s34]) ).
cnf(s1558,plain,
( spl3_13
| spl3_8
| ~ spl3_7
| spl3_5
| spl3_4
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s76,s192,s516,s1184,s1516,s32,s1554,s1557,s1556,s1076,s13,s205,s245,s903,s1182,s1553]) ).
cnf(s1559,plain,
( spl3_37
| spl3_8
| spl3_38
| spl3_107
| ~ spl3_16
| spl3_18
| spl3_39
| spl3_105
| spl3_94
| spl3_106 ),
inference(rat,[],[s680,s1542,s1532]) ).
cnf(s1560,plain,
( spl3_8
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s214,s312,s75,s742,s293,s1543,s1377,s190,s709,s29,s30,s31,s1559,s1556,s1557,s1076,s13,s245,s1182,s1529,s148,s219,s304,s401,s409,s753,s1246,s1558,s1551]) ).
cnf(s1561,plain,
( spl3_13
| ~ spl3_8
| ~ spl3_7
| spl3_6
| spl3_5
| spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s76,s192,s1184,s1516,s32,s28,s1556,s1549,s1076,s13,s205,s245,s880,s903,s1548,s632,s1178,s968,s662,s309,s296,s170]) ).
cnf(s1562,plain,
( spl3_6
| spl3_5
| spl3_1
| spl3_2
| spl3_3
| spl3_4 ),
inference(rat,[],[s85,s509,s1526,s1374,s25,s1528,s32,s989,s192,s222,s35,s76,s1040,s328,s79,s57,s1368,s11,s176,s1247,s242,s468,s87,s84,s310,s148,s219,s304,s401,s753,s779,s1561,s170,s296,s309,s662,s968,s1560,s1551]) ).
cnf(s1563,plain,
( ~ spl3_18
| ~ spl3_6 ),
inference(rat,[],[s390,s869]) ).
cnf(s1564,plain,
( spl3_37
| spl3_38
| spl3_39
| spl3_59
| ~ spl3_16
| spl3_13
| spl3_8
| spl3_18
| spl3_5
| spl3_4 ),
inference(rat,[],[s686,s1542,s1554]) ).
cnf(s1565,plain,
( spl3_13
| spl3_8
| spl3_5
| spl3_4
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s1377,s1499,s29,s1564,s1557,s1513,s453,s245,s1182,s83,s1558,s1553,s1563,s1562]) ).
cnf(s1566,plain,
( ~ spl3_39
| spl3_104
| spl3_102
| spl3_18
| spl3_5 ),
inference(rat,[],[s62,s323,s1045,s37,s38]) ).
cnf(s1567,plain,
( spl3_16
| spl3_94
| spl3_102
| spl3_8
| spl3_18
| spl3_5
| spl3_2 ),
inference(rat,[],[s55,s1296,s1516,s30,s1527,s1566,s144,s285,s622,s1529,s1520,s88]) ).
cnf(s1568,plain,
( ~ spl3_39
| spl3_59
| ~ spl3_16
| spl3_102
| spl3_18
| spl3_5
| spl3_1 ),
inference(rat,[],[s703,s1076,s1566,s1555,s205]) ).
cnf(s1569,plain,
( spl3_8
| spl3_5
| spl3_4
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s214,s312,s75,s742,s293,s1543,s1377,s190,s709,s29,s30,s31,s1559,s1568,s1557,s245,s1182,s1567,s219,s401,s409,s753,s1565,s1443,s1563,s1562]) ).
cnf(s1570,plain,
( ~ spl3_39
| spl3_16
| spl3_13
| spl3_18
| spl3_2 ),
inference(rat,[],[s167,s1528,s1496]) ).
cnf(s1571,plain,
( ~ spl3_37
| spl3_13
| spl3_18
| spl3_5 ),
inference(rat,[],[s1377,s1499,s29,s453,s83]) ).
cnf(s1572,plain,
( spl3_16
| spl3_37
| spl3_43
| spl3_13
| spl3_107
| spl3_98
| spl3_103
| spl3_93
| spl3_18
| spl3_4
| spl3_2 ),
inference(rat,[],[s28,s1570,s1547]) ).
cnf(s1573,plain,
( spl3_13
| ~ spl3_8
| spl3_18
| spl3_5
| spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s13,s1076,s1513,s1555,s28,s1549,s205,s245,s880,s1572,s1571,s632,s1178,s968,s296,s170]) ).
cnf(s1574,plain,
( ~ spl3_40
| spl3_16
| spl3_65
| spl3_18 ),
inference(rat,[],[s85,s509,s1526,s1374]) ).
cnf(s1575,plain,
( spl3_16
| spl3_65
| spl3_39
| spl3_107
| spl3_98
| spl3_103
| spl3_93
| spl3_18
| spl3_79
| spl3_4
| spl3_2 ),
inference(rat,[],[s48,s308,s1296,s192,s29,s30,s32,s25,s1574,s1547]) ).
cnf(s1576,plain,
( spl3_5
| spl3_4
| spl3_1
| spl3_2
| spl3_3 ),
inference(rat,[],[s76,s468,s222,s84,s989,s205,s903,s1575,s176,s87,s1566,s310,s219,s401,s753,s1573,s170,s296,s309,s662,s968,s1178,s1569,s1563,s1443,s1562]) ).
cnf(s1577,plain,
( spl3_8
| spl3_16
| ~ spl3_5
| spl3_4
| spl3_2 ),
inference(rat,[],[s82,s357,s541,s1184,s180,s1443,s76,s46,s48,s645,s1377,s308,s1296,s709,s516,s29,s30,s31,s32,s1527,s236,s622,s1520,s88,s188,s472,s186,s1570,s92,s142]) ).
cnf(s1578,plain,
( spl3_16
| ~ spl3_5
| spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s82,s357,s541,s1184,s180,s1443,s76,s46,s48,s645,s1377,s308,s1296,s709,s192,s29,s30,s31,s32,s1572,s632,s170,s296,s309,s968,s1178,s1577,s142,s92,s188,s472,s186]) ).
cnf(s1579,plain,
( ~ spl3_42
| spl3_8
| spl3_98
| spl3_100 ),
inference(rat,[],[s87,s1506,s391]) ).
cnf(s1580,plain,
( ~ spl3_38
| spl3_8
| spl3_59
| spl3_107
| ~ spl3_16
| spl3_2
| spl3_1 ),
inference(rat,[],[s212,s80,s218,s193,s352,s1523,s34,s36,s880]) ).
cnf(s1581,plain,
( ~ spl3_39
| spl3_59
| ~ spl3_16
| spl3_18
| spl3_101
| spl3_64
| spl3_1 ),
inference(rat,[],[s84,s1059,s703,s81,s413,s1076,s323,s1511,s1555,s37,s38,s205]) ).
cnf(s1582,plain,
( ~ spl3_37
| spl3_62
| spl3_107
| ~ spl3_5
| spl3_4 ),
inference(rat,[],[s541,s1443,s82,s357,s75,s180,s1184,s293,s46,s76,s1377,s709,s192,s516,s29,s31,s32,s187,s142,s92,s188,s472,s186]) ).
cnf(s1583,plain,
( spl3_8
| spl3_37
| spl3_39
| spl3_59
| spl3_107
| ~ spl3_16
| spl3_100
| spl3_2
| spl3_1 ),
inference(rat,[],[s27,s1580,s1579,s458]) ).
cnf(s1584,plain,
( spl3_4
| spl3_3
| spl3_1
| spl3_2 ),
inference(rat,[],[s28,s1549,s632,s1583,s1582,s1581,s245,s880,s903,s1182,s1578,s92,s142,s398,s399,s546,s1576]) ).
cnf(s1585,plain,
( spl3_8
| spl3_16
| spl3_2
| spl3_5 ),
inference(rat,[],[s1567,s148,s164,s409,s1553]) ).
cnf(s1586,plain,
( spl3_38
| spl3_39
| spl3_37
| spl3_98
| ~ spl3_8
| spl3_16 ),
inference(rat,[],[s149,s72,s66,s219,s1526,s1374,s632,s25,s28,s170]) ).
cnf(s1587,plain,
( ~ spl3_38
| spl3_98
| ~ spl3_8
| spl3_16
| ~ spl3_4
| spl3_2 ),
inference(rat,[],[s81,s842,s966,s8,s390,s1084,s1085,s229,s87,s77,s435,s910,s56,s225,s427,s884,s193,s352,s1549,s33,s34,s36,s707,s968,s170]) ).
cnf(s1588,plain,
( spl3_13
| ~ spl3_39
| spl3_16
| spl3_5
| spl3_2 ),
inference(rat,[],[s1563,s1546,s1570,s662,s1585]) ).
cnf(s1589,plain,
( ~ spl3_39
| spl3_16
| spl3_5
| spl3_2 ),
inference(rat,[],[s1566,s148,s164,s1588,s662,s1585]) ).
cnf(s1590,plain,
( spl3_16
| spl3_5
| ~ spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s645,s76,s308,s1184,s192,s1516,s29,s32,s1586,s1589,s1587,s170,s296,s309,s1585]) ).
cnf(s1591,plain,
( spl3_18
| spl3_13
| ~ spl3_44
| ~ spl3_26
| spl3_67
| spl3_39
| spl3_37
| spl3_38
| spl3_8
| spl3_84
| spl3_5 ),
inference(rat,[],[s1508,s875,s453,s1542,s1377,s83,s436,s63,s223,s391,s27]) ).
cnf(s1592,plain,
( spl3_13
| ~ spl3_44
| ~ spl3_26
| spl3_65
| spl3_67
| spl3_39
| spl3_37
| spl3_38
| spl3_8
| spl3_59
| spl3_84
| spl3_62
| spl3_5
| ~ spl3_4 ),
inference(rat,[],[s680,s70,s1509,s1507,s75,s8,s329,s1591,s172,s63,s25,s391,s1506,s27,s223,s222,s220,s118]) ).
cnf(s1593,plain,
( spl3_39
| spl3_37
| spl3_8
| spl3_59
| spl3_107
| ~ spl3_16
| spl3_5
| ~ spl3_4
| spl3_2
| spl3_1 ),
inference(rat,[],[s1559,s148,s401,s409,s1592,s311,s391,s989,s176,s420,s27,s28,s1583,s903,s880,s1580]) ).
cnf(s1594,plain,
( ~ spl3_39
| spl3_59
| ~ spl3_16
| spl3_5
| spl3_2 ),
inference(rat,[],[s1076,s13,s1556,s1513,s205]) ).
cnf(s1595,plain,
( ~ spl3_37
| spl3_5
| spl3_2 ),
inference(rat,[],[s1441,s74,s1483,s274,s748,s1543,s190,s1296,s29,s30]) ).
cnf(s1596,plain,
( spl3_5
| spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s468,s76,s84,s222,s401,s989,s632,s28,s1549,s309,s662,s1593,s1595,s1594,s205,s245,s880,s903,s1182,s1590,s1584]) ).
cnf(s1597,plain,
( spl3_8
| spl3_16
| spl3_81
| spl3_102
| spl3_13
| spl3_18
| spl3_86
| spl3_2 ),
inference(rat,[],[s357,s82,s1184,s180,s76,s46,s645,s1377,s308,s709,s516,s29,s31,s32,s1527,s236,s622,s1520,s88,s1570]) ).
cnf(s1598,plain,
( spl3_16
| spl3_81
| spl3_102
| spl3_13
| spl3_18
| spl3_86
| ~ spl3_4
| spl3_3
| spl3_2 ),
inference(rat,[],[s357,s82,s1184,s180,s76,s46,s645,s1377,s308,s709,s192,s29,s31,s32,s1586,s1587,s170,s296,s309,s1597,s1570]) ).
cnf(s1599,plain,
( ~ spl3_37
| spl3_56
| spl3_62
| spl3_102
| spl3_13
| spl3_18 ),
inference(rat,[],[s133,s42,s46,s293,s1377,s709,s516,s29,s31,s32]) ).
cnf(s1600,plain,
( spl3_3
| spl3_2
| spl3_1 ),
inference(rat,[],[s28,s1549,s632,s1583,s1599,s178,s58,s1581,s205,s245,s880,s903,s1182,s1598,s541,s189,s2,s92,s142,s186,s398,s399,s546,s1596,s707,s1584]) ).
cnf(s1601,plain,
( spl3_38
| ~ spl3_98
| spl3_39
| ~ spl3_8
| spl3_16
| spl3_37 ),
inference(rat,[],[s951,s71,s74,s687,s276,s996,s451,s75,s1233,s1501,s202,s208,s209,s445,s401,s1246,s1574,s509,s1374,s455,s632,s25,s27,s28,s170,s333,s313]) ).
cnf(s1602,plain,
( spl3_16
| spl3_5
| ~ spl3_3
| spl3_2 ),
inference(rat,[],[s77,s910,s225,s427,s1085,s884,s1549,s33,s1601,s333,s886,s1589,s1585,s1595]) ).
cnf(s1604,plain,
( ~ spl3_83
| spl3_56
| spl3_58
| spl3_99
| spl3_62 ),
inference(rat,[],[s269,s42,s58,s271,s1063]) ).
cnf(s1605,plain,
( ~ spl3_16
| ~ spl3_3 ),
inference(rat,[],[s329,s42,s58,s451,s714,s50,s1604,s179,s224,s250,s205,s880,s885,s903]) ).
cnf(s1606,plain,
( spl3_8
| ~ spl3_5
| spl3_16
| spl3_2 ),
inference(rat,[],[s541,s2,s1597,s1577,s142,s92,s188,s472,s186]) ).
cnf(s1607,plain,
( ~ spl3_38
| ~ spl3_8
| spl3_18
| spl3_16
| spl3_2 ),
inference(rat,[],[s910,s77,s225,s427,s1085,s884,s1549,s33]) ).
cnf(s1608,plain,
( spl3_16
| spl3_2
| ~ spl3_3 ),
inference(rat,[],[s49,s158,s541,s1184,s2,s134,s76,s1582,s46,s645,s1377,s308,s709,s192,s29,s31,s32,s28,s1607,s314,s632,s170,s309,s886,s1606,s188,s1570,s472,s92,s142,s186,s1602]) ).
cnf(s1609,plain,
( spl3_2
| spl3_1 ),
inference(rat,[],[s1608,s1605,s1600]) ).
cnf(s1610,plain,
( spl3_18
| spl3_39
| spl3_37
| spl3_5
| spl3_16
| ~ spl3_2 ),
inference(rat,[],[s351,s177,s77,s910,s894,s1082,s59,s359,s1085,s884,s312,s33,s34,s35,s25,s1574,s1340,s216]) ).
cnf(s1611,plain,
( spl3_39
| spl3_37
| spl3_5
| spl3_16
| ~ spl3_2 ),
inference(rat,[],[s359,s79,s312,s1040,s1087,s34,s35,s27,s1579,s1072,s333,s1563,s1063,s1610,s1340,s90]) ).
cnf(s1613,plain,
( ~ spl3_35
| ~ spl3_91
| ~ spl3_28 ),
inference(rat,[],[s1224,s20]) ).
cnf(s1614,plain,
( spl3_18
| spl3_90
| ~ spl3_39
| spl3_16
| spl3_87 ),
inference(rat,[],[s14,s593,s995,s77,s890,s1613,s86,s346,s426,s1379,s82,s735,s1321,s1341,s81,s251,s283,s323,s1528,s207,s37]) ).
cnf(s1615,plain,
( ~ spl3_28
| spl3_102
| spl3_81
| ~ spl3_53
| spl3_5
| spl3_1 ),
inference(rat,[],[s663,s703,s86,s62,s346,s98,s82,s60,s377,s426,s748,s532,s530,s1609,s1045]) ).
cnf(s1616,plain,
( ~ spl3_39
| spl3_5
| spl3_16
| spl3_1 ),
inference(rat,[],[s899,s43,s59,s418,s747,s377,s60,s735,s1615,s1072,s1563,s1061,s1614,s1045,s37,s38,s1340,s532,s530,s216,s1609]) ).
cnf(s1617,plain,
( spl3_18
| ~ spl3_37
| spl3_5
| spl3_101 ),
inference(rat,[],[s5,s1126,s304,s84,s280,s46,s75,s709,s293,s164,s401,s1246,s1377,s1571,s31,s29,s190,s30]) ).
cnf(s1618,plain,
( spl3_5
| spl3_16
| spl3_1 ),
inference(rat,[],[s192,s236,s76,s516,s148,s1617,s645,s308,s29,s32,s1611,s1616,s690,s532,s1609]) ).
cnf(s1619,plain,
( ~ spl3_39
| spl3_18
| spl3_64
| spl3_16 ),
inference(rat,[],[s81,s251,s323,s207,s1528,s37]) ).
cnf(s1620,plain,
( ~ spl3_38
| spl3_102
| spl3_18
| spl3_88
| spl3_16
| spl3_8 ),
inference(rat,[],[s77,s910,s226,s712,s79,s1085,s884,s1040,s1087,s33,s35]) ).
cnf(s1621,plain,
( spl3_16
| spl3_1 ),
inference(rat,[],[s1404,s75,s76,s293,s645,s1377,s308,s709,s516,s29,s31,s32,s25,s1620,s1619,s188,s1574,s472,s92,s142,s186,s187,s317,s546,s1618,s690,s216,s90,s1609]) ).
cnf(s1622,plain,
( spl3_18
| ~ spl3_39
| spl3_5
| ~ spl3_16 ),
inference(rat,[],[s1076,s13,s1555,s1512,s205,s245,s1605]) ).
cnf(s1623,plain,
( ~ spl3_39
| spl3_5
| spl3_1 ),
inference(rat,[],[s899,s43,s59,s418,s747,s377,s60,s735,s1615,s1072,s1563,s1061,s1622,s37,s38,s1340,s532,s216,s1609,s1621]) ).
cnf(s1624,plain,
( ~ spl3_91
| spl3_1 ),
inference(rat,[],[s1075,s663,s686,s1609,s1621]) ).
cnf(s1625,plain,
( spl3_18
| spl3_5
| spl3_1 ),
inference(rat,[],[s352,s56,s36,s779,s27,s83,s1617,s532,s1579,s90,s1182,s1133,s782,s618,s85,s1007,s87,s286,s86,s1624,s530,s204,s458,s1340,s245,s1605,s1621,s216,s1609,s1623]) ).
cnf(s1626,plain,
( spl3_5
| spl3_1 ),
inference(rat,[],[s27,s35,s1499,s1087,s231,s56,s76,s635,s822,s64,s148,s1625,s1623,s690,s903,s1579,s90,s1133,s346,s341,s950,s618,s85,s1007,s87,s286,s86,s1624,s530,s204,s458,s1340,s245,s1605,s1621,s216,s1609]) ).
cnf(s1627,plain,
spl3_1,
inference(rat,[],[s27,s35,s32,s1087,s516,s56,s76,s635,s822,s64,s1581,s92,s142,s546,s1626,s618,s950,s85,s1007,s87,s286,s346,s1133,s86,s1624,s245,s1579,s1605,s204,s458,s903,s1621,s90,s216,s530,s532,s690,s1340,s1609]) ).
cnf(s1628,plain,
( ~ spl3_64
| spl3_81
| spl3_87
| spl3_90
| ~ spl3_52 ),
inference(rat,[],[s14,s593,s995,s77,s890,s1613,s86,s346,s426,s1379,s82,s735,s1321,s1341]) ).
cnf(s1629,plain,
( ~ spl3_39
| spl3_5
| spl3_16 ),
inference(rat,[],[s899,s43,s59,s418,s747,s377,s60,s1628,s1061,s1614,s216,s530,s532,s1340,s1045,s1589,s37,s38]) ).
cnf(s1630,plain,
( ~ spl3_2
| spl3_18
| spl3_5
| spl3_16 ),
inference(rat,[],[s1617,s1611,s532,s1629]) ).
cnf(s1631,plain,
( spl3_18
| spl3_5
| spl3_16 ),
inference(rat,[],[s1607,s1586,s296,s1595,s1585,s1608,s1630,s1629]) ).
cnf(s1632,plain,
( ~ spl3_2
| spl3_5
| spl3_16 ),
inference(rat,[],[s192,s236,s76,s645,s308,s516,s29,s32,s1611,s690,s1629,s148,s1631]) ).
cnf(s1633,plain,
( spl3_5
| spl3_16 ),
inference(rat,[],[s1547,s1586,s170,s968,s1178,s1590,s1595,s1585,s1608,s1632,s333,s1631,s1629]) ).
cnf(s1634,plain,
( ~ spl3_2
| spl3_16 ),
inference(rat,[],[s1404,s75,s76,s293,s645,s1377,s308,s709,s516,s29,s31,s32,s25,s1620,s1574,s90,s216,s690,s317,s187,s92,s1619,s142,s546,s188,s472,s186,s1633]) ).
cnf(s1635,plain,
spl3_16,
inference(rat,[],[s541,s1598,s2,s1578,s1608,s1634,s188,s472,s92,s142,s186,s1633]) ).
cnf(s1636,plain,
~ spl3_62,
inference(rat,[],[s903,s1635]) ).
cnf(s1637,plain,
~ spl3_84,
inference(rat,[],[s880,s1635]) ).
cnf(s1638,plain,
~ spl3_98,
inference(rat,[],[s458,s1635]) ).
cnf(s1639,plain,
~ spl3_99,
inference(rat,[],[s205,s1635]) ).
cnf(s1641,plain,
~ spl3_17,
inference(rat,[],[s7,s1627,s1635]) ).
cnf(s1642,plain,
~ spl3_3,
inference(rat,[],[s1605,s1635]) ).
cnf(s1643,plain,
~ spl3_65,
inference(rat,[],[s1030,s1635,s1641]) ).
cnf(s1644,plain,
~ spl3_107,
inference(rat,[],[s1182,s1635,s1642]) ).
cnf(s1645,plain,
~ spl3_59,
inference(rat,[],[s245,s1635,s1642]) ).
cnf(s1646,plain,
( spl3_5
| ~ spl3_39 ),
inference(rat,[],[s899,s43,s59,s418,s747,s377,s60,s1628,s1061,s530,s532,s1340,s1045,s1622,s1594,s38,s37,s1643,s1635,s1645]) ).
cnf(s1647,plain,
~ spl3_39,
inference(rat,[],[s16,s1494,s667,s46,s342,s280,s79,s84,s1454,s435,s1059,s58,s1604,s87,s81,s413,s449,s1007,s323,s1511,s1555,s142,s317,s398,s399,s546,s1646,s37,s38,s1639,s1636,s1638,s1645]) ).
cnf(s1648,plain,
( ~ spl3_2
| spl3_18
| spl3_5 ),
inference(rat,[],[s85,s618,s449,s77,s196,s226,s910,s57,s894,s140,s1082,s59,s359,s1085,s312,s33,s34,s35,s27,s1579,s1617,s90,s532,s1340,s1645,s1643,s1638,s1647]) ).
cnf(s1649,plain,
( spl3_38
| spl3_8
| spl3_18
| spl3_5 ),
inference(rat,[],[s1559,s401,s409,s1591,s420,s311,s1579,s391,s989,s27,s28,s1595,s1648,s1647,s1635,s1644,s1637,s1638]) ).
cnf(s1650,plain,
( spl3_8
| spl3_18
| spl3_5 ),
inference(rat,[],[s1498,s449,s1477,s85,s80,s618,s212,s56,s312,s193,s1087,s352,s34,s35,s36,s1649,s1648,s1645,s1643,s1637,s1644]) ).
cnf(s1651,plain,
( spl3_18
| spl3_5 ),
inference(rat,[],[s468,s76,s84,s222,s401,s989,s632,s28,s1549,s309,s662,s1650,s1595,s1648,s1637,s1647,s1635,s1639,s1636]) ).
cnf(s1652,plain,
( ~ spl3_38
| spl3_8
| spl3_5 ),
inference(rat,[],[s359,s79,s312,s1040,s1087,s34,s35,s1063,s1072,s1563,s1651]) ).
cnf(s1653,plain,
( ~ spl3_2
| spl3_5 ),
inference(rat,[],[s76,s192,s516,s32,s27,s1652,s1579,s90,s690,s1340,s148,s1651,s1636,s1644,s1647,s1638]) ).
cnf(s1654,plain,
( spl3_8
| spl3_5 ),
inference(rat,[],[s1507,s406,s1554,s63,s1592,s220,s223,s311,s420,s989,s1579,s391,s28,s25,s27,s1652,s148,s1651,s1595,s1653,s1647,s1635,s1645,s1643,s1637,s1636,s1638]) ).
cnf(s1655,plain,
spl3_5,
inference(rat,[],[s28,s632,s1549,s1654,s1595,s1653,s148,s1651,s1647,s1637]) ).
cnf(s1658,plain,
~ spl3_100,
inference(rat,[],[s398,s1655]) ).
cnf(s1659,plain,
~ spl3_88,
inference(rat,[],[s317,s1655]) ).
cnf(s1661,plain,
~ spl3_86,
inference(rat,[],[s186,s1655]) ).
cnf(s1662,plain,
~ spl3_18,
inference(rat,[],[s142,s1655]) ).
cnf(s1663,plain,
~ spl3_13,
inference(rat,[],[s92,s1655]) ).
cnf(s1664,plain,
~ spl3_19,
inference(rat,[],[s472,s1655,s1661]) ).
cnf(s1665,plain,
~ spl3_102,
inference(rat,[],[s188,s1655,s1664]) ).
cnf(s1666,plain,
( ~ spl3_38
| spl3_8 ),
inference(rat,[],[s85,s618,s449,s77,s910,s196,s226,s712,s79,s1085,s1040,s1087,s33,s35,s1645,s1643,s1659,s1662,s1665]) ).
cnf(s1667,plain,
~ spl3_2,
inference(rat,[],[s76,s192,s516,s32,s27,s1666,s1579,s90,s690,s1636,s1644,s1663,s1647,s1638,s1658]) ).
cnf(s1668,plain,
spl3_87,
inference(rat,[],[s68,s1658,s1643,s1667]) ).
cnf(s1669,plain,
~ spl3_85,
inference(rat,[],[s776,s1668]) ).
cnf(s1670,plain,
~ spl3_41,
inference(rat,[],[s521,s1668,s1669]) ).
cnf(s1671,plain,
~ spl3_38,
inference(rat,[],[s1666,s1549,s1637,s1667]) ).
cnf(s1672,plain,
spl3_37,
inference(rat,[],[s26,s1670,s1647,s1671]) ).
cnf(s1677,plain,
spl3_56,
inference(rat,[],[s1599,s1662,s1663,s1636,s1665,s1672]) ).
cnf(s1678,plain,
spl3_4,
inference(rat,[],[s1582,s1644,s1636,s1655,s1672]) ).
cnf(s1687,plain,
~ spl3_58,
inference(rat,[],[s178,s1677]) ).
cnf(s1694,plain,
~ spl3_6,
inference(rat,[],[s2,s1655,s1678]) ).
cnf(s1701,plain,
spl3_81,
inference(rat,[],[s58,s1639,s1662,s1687]) ).
cnf(s1704,plain,
$false,
inference(rat,[],[s541,s1655,s1694,s1701]) ).
fof(f3467,plain,
$false,
inference(avatar_sat_refutation,[],[s1704]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG141+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n006.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 19:34:07 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.38/1.38 % (95441)Detected formulas, will run a generic FOF schedule.
% 4.38/1.38 % (95450)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1699489055:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.38/1.38 % (95450)Refutation not found, incomplete strategy
% 4.38/1.38 % (95450)------------------------------
% 4.38/1.38 % (95450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.38/1.38 % (95450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/1.38 % (95450)CaDiCaL version: 2.1.3
% 4.38/1.38 % (95450)Termination reason: Refutation not found, incomplete strategy
% 4.38/1.38 % (95450)Time elapsed: 0.0000 s
% 4.38/1.38 % (95450)Peak memory usage: 86 MB
% 4.38/1.38 % (95446)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1991594932:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.38/1.38 % (95449)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2371733989:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.38/1.38 % (95449)Refutation not found, incomplete strategy
% 4.38/1.38 % (95449)------------------------------
% 4.38/1.38 % (95449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.38/1.38 % (95449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/1.38 % (95449)CaDiCaL version: 2.1.3
% 4.38/1.38 % (95449)Termination reason: Refutation not found, incomplete strategy
% 4.38/1.38 % (95449)Time elapsed: 0.001 s
% 4.38/1.38 % (95449)Peak memory usage: 86 MB
% 4.38/1.38 % (95447)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1544291080:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.38/1.38 % (95448)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1810012804:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.38/1.38 % (95452)dis-21_1_sil=8000:lcm=predicate:random_seed=524150696:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.38/1.38 % (95451)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2322816699:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.38/1.38 % (95452)Refutation not found, incomplete strategy
% 4.38/1.38 % (95452)------------------------------
% 4.38/1.38 % (95452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.38/1.38 % (95452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/1.38 % (95452)CaDiCaL version: 2.1.3
% 4.38/1.38 % (95452)Termination reason: Refutation not found, incomplete strategy
% 4.38/1.38 % (95452)Time elapsed: 0.007 s
% 4.38/1.38 % (95452)Peak memory usage: 88 MB
% 4.38/1.38 % (95452)Instructions burned: 12 (million)
% 4.38/1.38 % (95451)Instruction limit reached!
% 4.38/1.38 % (95451)------------------------------
% 4.38/1.38 % (95451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.38/1.38 % (95451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/1.38 % (95451)CaDiCaL version: 2.1.3
% 4.38/1.38 % (95451)Termination reason: Instruction limit
% 4.38/1.38 % (95451)Termination phase: Saturation
% 4.38/1.38 % (95451)Time elapsed: 0.073 s
% 4.38/1.38 % (95451)Peak memory usage: 89 MB
% 4.38/1.38 % (95451)Instructions burned: 139 (million)
% 4.38/1.38 % (95450)------------------------------
% 4.38/1.38 % (95450)------------------------------
% 4.38/1.38 % (95460)lrs+10_1_sil=8000:sp=occurrence:random_seed=2427900058:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.38/1.38 % (95460)Refutation not found, incomplete strategy
% 4.38/1.38 % (95460)------------------------------
% 4.38/1.38 % (95460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.38/1.38 % (95460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.38/1.38 % (95460)CaDiCaL version: 2.1.3
% 4.38/1.38 % (95460)Termination reason: Refutation not found, incomplete strategy
% 4.38/1.38 % (95460)Time elapsed: 0.001 s
% 4.38/1.38 % (95460)Peak memory usage: 86 MB
% 4.38/1.38 % (95461)lrs+10_1_sil=32000:urr=on:br=off:random_seed=790748483:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.38/1.38 % (95461)Refutation not found, incomplete strategy
% 5.60/1.60 % (95461)------------------------------
% 5.60/1.60 % (95461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.60 % (95461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.60 % (95461)CaDiCaL version: 2.1.3
% 5.60/1.60 % (95461)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.60 % (95461)Time elapsed: 0.0000 s
% 5.60/1.60 % (95461)Peak memory usage: 87 MB
% 5.60/1.60 % (95461)Instructions burned: 2 (million)
% 5.60/1.60 % (95449)------------------------------
% 5.60/1.60 % (95449)------------------------------
% 5.60/1.60 % (95452)------------------------------
% 5.60/1.60 % (95452)------------------------------
% 5.60/1.60 % (95464)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3182769230:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 5.60/1.60 % (95464)Refutation not found, incomplete strategy
% 5.60/1.60 % (95464)------------------------------
% 5.60/1.60 % (95464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.60 % (95464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.60 % (95464)CaDiCaL version: 2.1.3
% 5.60/1.60 % (95464)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.60 % (95464)Time elapsed: 0.001 s
% 5.60/1.60 % (95464)Peak memory usage: 86 MB
% 5.60/1.60 % (95461)------------------------------
% 5.60/1.60 % (95461)------------------------------
% 5.60/1.60 [W928 19:34:08.207330912 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.207360109 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.207396079 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.207408915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.207434305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.207445389 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213306028 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213339661 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213374664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213388294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213414268 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213455878 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213474435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213530038 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213575361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213589265 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213616508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 [W928 19:34:08.213628641 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 5.60/1.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 5.60/1.60 % (95465)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=52568841:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 5.60/1.60 % (95460)------------------------------
% 5.60/1.60 % (95460)------------------------------
% 5.60/1.60 % (95467)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=247345878:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 5.60/1.60 % (95467)Refutation not found, incomplete strategy
% 5.60/1.60 % (95467)------------------------------
% 5.60/1.60 % (95467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.60 % (95467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.60 % (95467)CaDiCaL version: 2.1.3
% 5.60/1.60 % (95467)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.60 % (95467)Time elapsed: 0.0000 s
% 5.60/1.60 % (95467)Peak memory usage: 86 MB
% 5.60/1.60 % (95465)First to succeed.
% 5.60/1.60 % (95465)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-95441"
% 5.60/1.60 % (95448)Refutation not found, incomplete strategy
% 5.60/1.60 % (95448)------------------------------
% 5.60/1.60 % (95448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.60 % (95448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.60 % (95448)CaDiCaL version: 2.1.3
% 5.60/1.60 % (95448)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.60 % (95448)Time elapsed: 0.570 s
% 5.60/1.60 % (95448)Peak memory usage: 127 MB
% 5.60/1.60 % (95448)Instructions burned: 846 (million)
% 5.60/1.60 % (95470)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1163149257:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 5.60/1.60 % (95464)------------------------------
% 5.60/1.60 % (95464)------------------------------
% 5.60/1.60 % (95467)------------------------------
% 5.60/1.60 % (95467)------------------------------
% 5.60/1.60 % (95446)Also succeeded, but the first one will report.
% 5.60/1.60 % (95447)Also succeeded, but the first one will report.
% 5.60/1.60 % (95473)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=983016573:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 5.60/1.60 % (95473)Refutation not found, incomplete strategy
% 5.60/1.60 % (95473)------------------------------
% 5.60/1.60 % (95473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.60 % (95473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.60 % (95473)CaDiCaL version: 2.1.3
% 5.60/1.60 % (95473)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.60 % (95473)Time elapsed: 0.001 s
% 5.60/1.60 % (95473)Peak memory usage: 87 MB
% 5.60/1.60 % (95473)Instructions burned: 3 (million)
% 5.60/1.60 % (95472)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3659854089:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 5.60/1.60 % (95472)Refutation not found, incomplete strategy
% 5.60/1.60 % (95472)------------------------------
% 5.60/1.60 % (95472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.60 % (95472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.60 % (95472)CaDiCaL version: 2.1.3
% 5.60/1.60 % (95472)Termination reason: Refutation not found, incomplete strategy
% 5.60/1.60 % (95472)Time elapsed: 0.005 s
% 5.60/1.60 % (95472)Peak memory usage: 88 MB
% 5.60/1.60 % (95472)Instructions burned: 8 (million)
% 5.60/1.60 % (95465)Refutation found. Thanks to Tanya!
% 5.60/1.60 % SZS status Unsatisfiable for theBenchmark
% 5.60/1.60 % SZS output start Proof for theBenchmark
% See solution above
% 7.13/1.79 % (95465)------------------------------
% 7.13/1.79 % (95465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.13/1.79 % (95465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.13/1.79 % (95465)CaDiCaL version: 2.1.3
% 7.13/1.79 % (95465)Termination reason: Refutation
% 7.13/1.79 % (95465)Time elapsed: 0.109 s
% 7.13/1.79 % (95465)Peak memory usage: 90 MB
% 7.13/1.79 % (95465)Instructions burned: 182 (million)
% 7.13/1.79 % (95465)------------------------------
% 7.13/1.79 % (95465)------------------------------
% 7.13/1.79 % (95441)Success in time 0.929 s
% 7.13/1.79 % Vampire exiting
%------------------------------------------------------------------------------