%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG146+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:25:22 AM UTC 2026
% Result : Unsatisfiable 0.21s 0.30s
% Output : Refutation 0.21s
% 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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op(e0,e0) = e0
| op(e1,e1) = e1
| op(e2,e2) = e2
| op(e3,e3) = e3 )
& ( op(e0,e0) != e0
| op(e0,e0) = e0 )
& ( op(e0,e0) != e1
| op(e0,e1) = e0 )
& ( op(e0,e0) != e2
| op(e0,e2) = e0 )
& ( op(e0,e0) != e3
| op(e0,e3) = e0 )
& ( op(e1,e1) != e0
| op(e1,e0) = e1 )
& ( op(e1,e1) != e1
| op(e1,e1) = e1 )
& ( op(e1,e1) != e2
| op(e1,e2) = e1 )
& ( op(e1,e1) != e3
| op(e1,e3) = e1 )
& ( op(e2,e2) != e0
| op(e2,e0) = e2 )
& ( op(e2,e2) != e1
| op(e2,e1) = e2 )
& ( op(e2,e2) != e2
| op(e2,e2) = e2 )
& ( op(e2,e2) != e3
| op(e2,e3) = e2 )
& ( op(e3,e3) != e0
| op(e3,e0) = e3 )
& ( op(e3,e3) != e1
| op(e3,e1) = e3 )
& ( op(e3,e3) != e2
| op(e3,e2) = e3 )
& ( op(e3,e3) != e3
| op(e3,e3) = e3 )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0 )
| ( op(e0,e1) = e0
& op(e1,e0) = e0
& op(e1,e1) != e1 )
| ( op(e0,e2) = e0
& op(e2,e0) = e0
& op(e2,e2) != e2 )
| ( op(e0,e3) = e0
& op(e3,e0) = e0
& op(e3,e3) != e3 )
| ( op(e1,e0) = e1
& op(e0,e1) = e1
& op(e0,e0) != e0 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e1) != e1 )
| ( op(e1,e2) = e1
& op(e2,e1) = e1
& op(e2,e2) != e2 )
| ( op(e1,e3) = e1
& op(e3,e1) = e1
& op(e3,e3) != e3 )
| ( op(e2,e0) = e2
& op(e0,e2) = e2
& op(e0,e0) != e0 )
| ( op(e2,e1) = e2
& op(e1,e2) = e2
& op(e1,e1) != e1 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e2) != e2 )
| ( op(e2,e3) = e2
& op(e3,e2) = e2
& op(e3,e3) != e3 )
| ( op(e3,e0) = e3
& op(e0,e3) = e3
& op(e0,e0) != e0 )
| ( op(e3,e1) = e3
& op(e1,e3) = e3
& op(e1,e1) != e1 )
| ( op(e3,e2) = e3
& op(e2,e3) = e3
& op(e2,e2) != e2 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
fof(f7,axiom,
~ ( e0 = op(e2,e2)
& e1 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
fof(f9,axiom,
~ ( e0 = op(e1,e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax9) ).
fof(f11,axiom,
~ ( e0 = op(e1,e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e2 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
fof(f13,axiom,
~ ( e1 = op(e2,e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
fof(f15,axiom,
~ ( e1 = op(e0,e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e3 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
~ ( e1 = op(e2,e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e0 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax16) ).
fof(f19,axiom,
~ ( e2 = op(e1,e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax19) ).
fof(f21,axiom,
~ ( e2 = op(e0,e0)
& e1 = op(op(e0,e0),op(e0,e0))
& e3 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax21) ).
fof(f22,axiom,
~ ( e2 = op(e1,e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(e0,e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e1 = op(op(op(e0,e0),op(e0,e0)),e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
~ ( e3 = op(e2,e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e1 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax24) ).
fof(f26,axiom,
~ ( e3 = op(e2,e2)
& e1 = op(op(e2,e2),op(e2,e2))
& e0 = op(op(op(e2,e2),op(e2,e2)),e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax26) ).
fof(f28,axiom,
~ ( e3 = op(e1,e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(op(e1,e1),op(e1,e1)),e1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax28) ).
fof(f31,plain,
( e0 != op(e2,e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f33,plain,
( e0 != op(e1,e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f35,plain,
( e0 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f37,plain,
( e1 != op(e2,e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f39,plain,
( op(e0,e0) != e1
| e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f40,plain,
( e1 != op(e2,e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f43,plain,
( e2 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f45,plain,
( op(e0,e0) != e2
| e1 != op(op(e0,e0),op(e0,e0))
| e3 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f21]) ).
fof(f46,plain,
( e2 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f22]) ).
fof(f47,plain,
( op(e0,e0) != e2
| e3 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(op(e0,e0),op(e0,e0)),e0) ),
inference(ennf_transformation,[],[f23]) ).
fof(f48,plain,
( e3 != op(e2,e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e1 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f24]) ).
fof(f50,plain,
( e3 != op(e2,e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(op(e2,e2),op(e2,e2)),e2) ),
inference(ennf_transformation,[],[f26]) ).
fof(f52,plain,
( e3 != op(e1,e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(op(e1,e1),op(e1,e1)),e1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f54,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f58,plain,
( e3 = op(e1,e0)
| e2 = op(e1,e0)
| e1 = op(e1,e0)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f59,plain,
( e3 = op(e1,e1)
| e2 = op(e1,e1)
| e1 = op(e1,e1)
| e0 = op(e1,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f61,plain,
( e3 = op(e1,e3)
| e2 = op(e1,e3)
| e1 = op(e1,e3)
| e0 = op(e1,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f64,plain,
( e3 = op(e2,e2)
| e2 = op(e2,e2)
| e1 = op(e2,e2)
| e0 = op(e2,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f69,plain,
( e3 = op(e3,e3)
| e2 = op(e3,e3)
| e1 = op(e3,e3)
| e0 = op(e3,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f71,plain,
( e0 = op(e3,e0)
| e0 = op(e2,e0)
| e0 = op(e1,e0)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f72,plain,
( e1 = op(e0,e3)
| e1 = op(e0,e2)
| e1 = op(e0,e1)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f73,plain,
( e1 = op(e3,e0)
| e1 = op(e2,e0)
| e1 = op(e1,e0)
| op(e0,e0) = e1 ),
inference(cnf_transformation,[],[f2]) ).
fof(f74,plain,
( e2 = op(e0,e3)
| e2 = op(e0,e2)
| e2 = op(e0,e1)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f75,plain,
( e2 = op(e3,e0)
| e2 = op(e2,e0)
| e2 = op(e1,e0)
| op(e0,e0) = e2 ),
inference(cnf_transformation,[],[f2]) ).
fof(f76,plain,
( e3 = op(e0,e3)
| e3 = op(e0,e2)
| e3 = op(e0,e1)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f77,plain,
( e3 = op(e3,e0)
| e3 = op(e2,e0)
| e3 = op(e1,e0)
| op(e0,e0) = e3 ),
inference(cnf_transformation,[],[f2]) ).
fof(f78,plain,
( e0 = op(e1,e3)
| e0 = op(e1,e2)
| e0 = op(e1,e1)
| e0 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f79,plain,
( e0 = op(e3,e1)
| e0 = op(e2,e1)
| e0 = op(e1,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f81,plain,
( e1 = op(e3,e1)
| e1 = op(e2,e1)
| e1 = op(e1,e1)
| e1 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f82,plain,
( e2 = op(e1,e3)
| e2 = op(e1,e2)
| e2 = op(e1,e1)
| e2 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f83,plain,
( e2 = op(e3,e1)
| e2 = op(e2,e1)
| e2 = op(e1,e1)
| e2 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f84,plain,
( e3 = op(e1,e3)
| e3 = op(e1,e2)
| e3 = op(e1,e1)
| e3 = op(e1,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f85,plain,
( e3 = op(e3,e1)
| e3 = op(e2,e1)
| e3 = op(e1,e1)
| e3 = op(e0,e1) ),
inference(cnf_transformation,[],[f2]) ).
fof(f86,plain,
( e0 = op(e2,e3)
| e0 = op(e2,e2)
| e0 = op(e2,e1)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f87,plain,
( e0 = op(e3,e2)
| e0 = op(e2,e2)
| e0 = op(e1,e2)
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f88,plain,
( e1 = op(e2,e3)
| e1 = op(e2,e2)
| e1 = op(e2,e1)
| e1 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f89,plain,
( e1 = op(e3,e2)
| e1 = op(e2,e2)
| e1 = op(e1,e2)
| e1 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f90,plain,
( e2 = op(e2,e3)
| e2 = op(e2,e2)
| e2 = op(e2,e1)
| e2 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f91,plain,
( e2 = op(e3,e2)
| e2 = op(e2,e2)
| e2 = op(e1,e2)
| e2 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f92,plain,
( e3 = op(e2,e3)
| e3 = op(e2,e2)
| e3 = op(e2,e1)
| e3 = op(e2,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f93,plain,
( e3 = op(e3,e2)
| e3 = op(e2,e2)
| e3 = op(e1,e2)
| e3 = op(e0,e2) ),
inference(cnf_transformation,[],[f2]) ).
fof(f94,plain,
( e0 = op(e3,e3)
| e0 = op(e3,e2)
| e0 = op(e3,e1)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f95,plain,
( e0 = op(e3,e3)
| e0 = op(e2,e3)
| e0 = op(e1,e3)
| e0 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f96,plain,
( e1 = op(e3,e3)
| e1 = op(e3,e2)
| e1 = op(e3,e1)
| e1 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f97,plain,
( e1 = op(e3,e3)
| e1 = op(e2,e3)
| e1 = op(e1,e3)
| e1 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f98,plain,
( e2 = op(e3,e3)
| e2 = op(e3,e2)
| e2 = op(e3,e1)
| e2 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f99,plain,
( e2 = op(e3,e3)
| e2 = op(e2,e3)
| e2 = op(e1,e3)
| e2 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f100,plain,
( e3 = op(e3,e3)
| e3 = op(e3,e2)
| e3 = op(e3,e1)
| e3 = op(e3,e0) ),
inference(cnf_transformation,[],[f2]) ).
fof(f101,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e3)
| e3 = op(e1,e3)
| e3 = op(e0,e3) ),
inference(cnf_transformation,[],[f2]) ).
fof(f108,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f114,plain,
op(e1,e2) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f115,plain,
op(e1,e1) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f116,plain,
op(e1,e1) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f117,plain,
op(e1,e0) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f145,plain,
op(e1,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f146,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f149,plain,
op(e0,e0) != op(e1,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f150,plain,
e2 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f151,plain,
e1 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f152,plain,
e1 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f153,plain,
e0 != e3,
inference(cnf_transformation,[],[f4]) ).
fof(f154,plain,
e0 != e2,
inference(cnf_transformation,[],[f4]) ).
fof(f155,plain,
e0 != e1,
inference(cnf_transformation,[],[f4]) ).
fof(f156,plain,
( e0 != op(e0,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( e0 = op(e0,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( e1 != op(e1,e1)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( e0 = op(e1,e0)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
( e0 = op(e0,e1)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( e2 != op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( e0 = op(e2,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( e0 = op(e0,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
( e3 != op(e3,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( e0 = op(e3,e0)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( e0 = op(e0,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( e0 != op(e0,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( e1 = op(e0,e1)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( e1 = op(e1,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( e1 != op(e1,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( e1 = op(e1,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( e2 != op(e2,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( e1 = op(e2,e1)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( e1 = op(e1,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e3 != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( e1 = op(e3,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( e1 = op(e1,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( e0 != op(e0,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f181,plain,
( e2 = op(e0,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( e2 = op(e2,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( e1 != op(e1,e1)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( e2 = op(e1,e2)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f185,plain,
( e2 = op(e2,e1)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( e2 != op(e2,e2)
| ~ sP3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
( e2 = op(e2,e2)
| ~ sP3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f189,plain,
( e3 != op(e3,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f190,plain,
( e2 = op(e3,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f191,plain,
( e2 = op(e2,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( e0 != op(e0,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f193,plain,
( e3 = op(e0,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f194,plain,
( e3 = op(e3,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( e1 != op(e1,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f196,plain,
( e3 = op(e1,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
( e3 = op(e3,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
( e3 = op(e3,e3)
| e2 != op(e2,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
( e3 = op(e3,e3)
| e3 = op(e3,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
( e3 = op(e3,e3)
| e2 != op(e2,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
( e3 = op(e3,e3)
| e3 = op(e2,e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
( e3 = op(e3,e3)
| e3 = op(e3,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f204,plain,
( e3 != op(e3,e3)
| e2 != op(e2,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
( e3 != op(e3,e3)
| e3 = op(e2,e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
( e3 != op(e3,e3)
| e3 = op(e3,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
( e3 = op(e3,e3)
| e2 = op(e2,e2)
| e1 = op(e1,e1)
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( e0 = op(e0,e1)
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f209,plain,
( e0 = op(e0,e2)
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f210,plain,
( e0 = op(e0,e3)
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
( e1 = op(e1,e0)
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
( e1 = op(e1,e2)
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f213,plain,
( e1 = op(e1,e3)
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f214,plain,
( e2 = op(e2,e0)
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f215,plain,
( e2 = op(e2,e1)
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f216,plain,
( e2 = op(e2,e3)
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f5]) ).
fof(f217,plain,
( e3 = op(e3,e0)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f218,plain,
( e3 = op(e3,e1)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f219,plain,
( e3 = op(e3,e2)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f5]) ).
fof(f221,plain,
( e3 != op(op(op(e2,e2),op(e2,e2)),e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f223,plain,
( e3 != op(op(op(e1,e1),op(e1,e1)),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f225,plain,
( e2 != op(op(op(e1,e1),op(e1,e1)),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f227,plain,
( e3 != op(op(op(e2,e2),op(e2,e2)),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f37]) ).
fof(f229,plain,
( e3 != op(op(op(e0,e0),op(e0,e0)),e0)
| e2 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f39]) ).
fof(f230,plain,
( e0 != op(op(op(e2,e2),op(e2,e2)),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f233,plain,
( e3 != op(op(op(e1,e1),op(e1,e1)),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f235,plain,
( e3 != op(op(op(e0,e0),op(e0,e0)),e0)
| e1 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f45]) ).
fof(f236,plain,
( e0 != op(op(op(e1,e1),op(e1,e1)),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f237,plain,
( e1 != op(op(op(e0,e0),op(e0,e0)),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f47]) ).
fof(f238,plain,
( e1 != op(op(op(e2,e2),op(e2,e2)),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f48]) ).
fof(f240,plain,
( e0 != op(op(op(e2,e2),op(e2,e2)),e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f50]) ).
fof(f242,plain,
( e0 != op(op(op(e1,e1),op(e1,e1)),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f245,definition,
( spl14_1
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f246,plain,
( op(e0,e0) = e3
| ~ spl14_1 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f247,plain,
( op(e0,e0) != e3
| spl14_1 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f249,definition,
( spl14_2
<=> e2 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
fof(f250,plain,
( e2 = op(op(e0,e0),op(e0,e0))
| ~ spl14_2 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f251,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| spl14_2 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f253,definition,
( spl14_3
<=> e1 = op(op(op(e0,e0),op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition]) ).
fof(f254,plain,
( e1 = op(op(op(e0,e0),op(e0,e0)),e0)
| ~ spl14_3 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f255,plain,
( e1 != op(op(op(e0,e0),op(e0,e0)),e0)
| spl14_3 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f258,definition,
( spl14_4
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f259,plain,
( e3 = op(e1,e1)
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f260,plain,
( e3 != op(e1,e1)
| spl14_4 ),
inference(avatar_component_clause,[],[f258]) ).
fof(f262,definition,
( spl14_5
<=> e2 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f263,plain,
( e2 = op(op(e1,e1),op(e1,e1))
| ~ spl14_5 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f264,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| spl14_5 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f266,definition,
( spl14_6
<=> e0 = op(op(op(e1,e1),op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f268,plain,
( e0 != op(op(op(e1,e1),op(e1,e1)),e1)
| spl14_6 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f269,plain,
( ~ spl14_4
| ~ spl14_5
| ~ spl14_6 ),
inference(avatar_split_clause,[],[f242,f266,f262,f258]) ).
fof(f271,definition,
( spl14_7
<=> e1 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f272,plain,
( e1 = op(op(e0,e0),op(e0,e0))
| ~ spl14_7 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f273,plain,
( e1 != op(op(e0,e0),op(e0,e0))
| spl14_7 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f280,definition,
( spl14_9
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f281,plain,
( e3 = op(e2,e2)
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f280]) ).
fof(f284,definition,
( spl14_10
<=> e1 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
fof(f285,plain,
( e1 = op(op(e2,e2),op(e2,e2))
| ~ spl14_10 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f286,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| spl14_10 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f288,definition,
( spl14_11
<=> e0 = op(op(op(e2,e2),op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
fof(f289,plain,
( e0 = op(op(op(e2,e2),op(e2,e2)),e2)
| ~ spl14_11 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f290,plain,
( e0 != op(op(op(e2,e2),op(e2,e2)),e2)
| spl14_11 ),
inference(avatar_component_clause,[],[f288]) ).
fof(f291,plain,
( ~ spl14_9
| ~ spl14_10
| ~ spl14_11 ),
inference(avatar_split_clause,[],[f240,f288,f284,f280]) ).
fof(f293,definition,
( spl14_12
<=> e0 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f294,plain,
( e0 = op(op(e1,e1),op(e1,e1))
| ~ spl14_12 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| spl14_12 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f297,definition,
( spl14_13
<=> e2 = op(op(op(e1,e1),op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f299,plain,
( e2 != op(op(op(e1,e1),op(e1,e1)),e1)
| spl14_13 ),
inference(avatar_component_clause,[],[f297]) ).
fof(f302,definition,
( spl14_14
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
fof(f303,plain,
( e0 = op(op(e2,e2),op(e2,e2))
| ~ spl14_14 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f304,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl14_14 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl14_15
<=> e1 = op(op(op(e2,e2),op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
fof(f307,plain,
( e1 = op(op(op(e2,e2),op(e2,e2)),e2)
| ~ spl14_15 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f308,plain,
( e1 != op(op(op(e2,e2),op(e2,e2)),e2)
| spl14_15 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f309,plain,
( ~ spl14_9
| ~ spl14_14
| ~ spl14_15 ),
inference(avatar_split_clause,[],[f238,f306,f302,f280]) ).
fof(f311,definition,
( spl14_16
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition]) ).
fof(f312,plain,
( op(e0,e0) = e2
| ~ spl14_16 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f313,plain,
( op(e0,e0) != e2
| spl14_16 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl14_17
<=> e3 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl14_17])],[avatar_definition]) ).
fof(f317,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| spl14_17 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f318,plain,
( ~ spl14_16
| ~ spl14_17
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f237,f253,f315,f311]) ).
fof(f320,definition,
( spl14_18
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_18])],[avatar_definition]) ).
fof(f321,plain,
( e2 = op(e1,e1)
| ~ spl14_18 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( e2 != op(e1,e1)
| spl14_18 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl14_19
<=> e3 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl14_19])],[avatar_definition]) ).
fof(f325,plain,
( e3 = op(op(e1,e1),op(e1,e1))
| ~ spl14_19 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f326,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| spl14_19 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f327,plain,
( ~ spl14_18
| ~ spl14_19
| ~ spl14_6 ),
inference(avatar_split_clause,[],[f236,f266,f324,f320]) ).
fof(f329,definition,
( spl14_20
<=> e3 = op(op(op(e0,e0),op(e0,e0)),e0) ),
introduced(definition,[new_symbols(definition,[spl14_20])],[avatar_definition]) ).
fof(f331,plain,
( e3 != op(op(op(e0,e0),op(e0,e0)),e0)
| spl14_20 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f332,plain,
( ~ spl14_16
| ~ spl14_7
| ~ spl14_20 ),
inference(avatar_split_clause,[],[f235,f329,f271,f311]) ).
fof(f334,definition,
( spl14_21
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_21])],[avatar_definition]) ).
fof(f335,plain,
( e2 = op(e3,e3)
| ~ spl14_21 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f347,definition,
( spl14_24
<=> e3 = op(op(op(e1,e1),op(e1,e1)),e1) ),
introduced(definition,[new_symbols(definition,[spl14_24])],[avatar_definition]) ).
fof(f349,plain,
( e3 != op(op(op(e1,e1),op(e1,e1)),e1)
| spl14_24 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f350,plain,
( ~ spl14_18
| ~ spl14_12
| ~ spl14_24 ),
inference(avatar_split_clause,[],[f233,f347,f293,f320]) ).
fof(f361,definition,
( spl14_27
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl14_27])],[avatar_definition]) ).
fof(f362,plain,
( op(e0,e0) = e1
| ~ spl14_27 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f366,definition,
( spl14_28
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_28])],[avatar_definition]) ).
fof(f367,plain,
( e1 = op(e2,e2)
| ~ spl14_28 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f368,plain,
( e1 != op(e2,e2)
| spl14_28 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f370,definition,
( spl14_29
<=> e3 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl14_29])],[avatar_definition]) ).
fof(f371,plain,
( e3 = op(op(e2,e2),op(e2,e2))
| ~ spl14_29 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| spl14_29 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f373,plain,
( ~ spl14_28
| ~ spl14_29
| ~ spl14_11 ),
inference(avatar_split_clause,[],[f230,f288,f370,f366]) ).
fof(f374,plain,
( ~ spl14_27
| ~ spl14_2
| ~ spl14_20 ),
inference(avatar_split_clause,[],[f229,f329,f249,f361]) ).
fof(f376,definition,
( spl14_30
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_30])],[avatar_definition]) ).
fof(f377,plain,
( e1 = op(e3,e3)
| ~ spl14_30 ),
inference(avatar_component_clause,[],[f376]) ).
fof(f385,definition,
( spl14_32
<=> e3 = op(op(op(e2,e2),op(e2,e2)),e2) ),
introduced(definition,[new_symbols(definition,[spl14_32])],[avatar_definition]) ).
fof(f387,plain,
( e3 != op(op(op(e2,e2),op(e2,e2)),e2)
| spl14_32 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,plain,
( ~ spl14_28
| ~ spl14_14
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f227,f385,f302,f366]) ).
fof(f395,definition,
( spl14_34
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_34])],[avatar_definition]) ).
fof(f396,plain,
( e0 = op(e1,e1)
| ~ spl14_34 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f398,plain,
( ~ spl14_34
| ~ spl14_19
| ~ spl14_13 ),
inference(avatar_split_clause,[],[f225,f297,f324,f395]) ).
fof(f400,definition,
( spl14_35
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_35])],[avatar_definition]) ).
fof(f401,plain,
( e0 = op(e2,e2)
| ~ spl14_35 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f404,plain,
( ~ spl14_34
| ~ spl14_5
| ~ spl14_24 ),
inference(avatar_split_clause,[],[f223,f347,f262,f395]) ).
fof(f406,definition,
( spl14_36
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_36])],[avatar_definition]) ).
fof(f407,plain,
( e0 = op(e3,e3)
| ~ spl14_36 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f410,plain,
( ~ spl14_35
| ~ spl14_10
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f221,f385,f284,f400]) ).
fof(f413,definition,
( spl14_37
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl14_37])],[avatar_definition]) ).
fof(f417,definition,
( spl14_38
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl14_38])],[avatar_definition]) ).
fof(f418,plain,
( e0 = op(e0,e0)
| ~ spl14_38 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( ~ spl14_37
| ~ spl14_38 ),
inference(avatar_split_clause,[],[f156,f417,f413]) ).
fof(f422,plain,
( ~ spl14_37
| spl14_38 ),
inference(avatar_split_clause,[],[f158,f417,f413]) ).
fof(f424,definition,
( spl14_39
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl14_39])],[avatar_definition]) ).
fof(f428,definition,
( spl14_40
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_40])],[avatar_definition]) ).
fof(f429,plain,
( e1 = op(e1,e1)
| ~ spl14_40 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f431,plain,
( ~ spl14_39
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f159,f428,f424]) ).
fof(f433,definition,
( spl14_41
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_41])],[avatar_definition]) ).
fof(f435,plain,
( e0 = op(e1,e0)
| ~ spl14_41 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f436,plain,
( ~ spl14_39
| spl14_41 ),
inference(avatar_split_clause,[],[f160,f433,f424]) ).
fof(f438,definition,
( spl14_42
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_42])],[avatar_definition]) ).
fof(f440,plain,
( e0 = op(e0,e1)
| ~ spl14_42 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,plain,
( ~ spl14_39
| spl14_42 ),
inference(avatar_split_clause,[],[f161,f438,f424]) ).
fof(f443,definition,
( spl14_43
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl14_43])],[avatar_definition]) ).
fof(f447,definition,
( spl14_44
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_44])],[avatar_definition]) ).
fof(f448,plain,
( e2 = op(e2,e2)
| ~ spl14_44 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( ~ spl14_43
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f162,f447,f443]) ).
fof(f452,definition,
( spl14_45
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_45])],[avatar_definition]) ).
fof(f454,plain,
( e0 = op(e2,e0)
| ~ spl14_45 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f455,plain,
( ~ spl14_43
| spl14_45 ),
inference(avatar_split_clause,[],[f163,f452,f443]) ).
fof(f457,definition,
( spl14_46
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_46])],[avatar_definition]) ).
fof(f458,plain,
( e0 != op(e0,e2)
| spl14_46 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( e0 = op(e0,e2)
| ~ spl14_46 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f460,plain,
( ~ spl14_43
| spl14_46 ),
inference(avatar_split_clause,[],[f164,f457,f443]) ).
fof(f462,definition,
( spl14_47
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl14_47])],[avatar_definition]) ).
fof(f466,definition,
( spl14_48
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_48])],[avatar_definition]) ).
fof(f467,plain,
( e3 = op(e3,e3)
| ~ spl14_48 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f469,plain,
( ~ spl14_47
| ~ spl14_48 ),
inference(avatar_split_clause,[],[f165,f466,f462]) ).
fof(f471,definition,
( spl14_49
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_49])],[avatar_definition]) ).
fof(f473,plain,
( e0 = op(e3,e0)
| ~ spl14_49 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f474,plain,
( ~ spl14_47
| spl14_49 ),
inference(avatar_split_clause,[],[f166,f471,f462]) ).
fof(f476,definition,
( spl14_50
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_50])],[avatar_definition]) ).
fof(f478,plain,
( e0 = op(e0,e3)
| ~ spl14_50 ),
inference(avatar_component_clause,[],[f476]) ).
fof(f479,plain,
( ~ spl14_47
| spl14_50 ),
inference(avatar_split_clause,[],[f167,f476,f462]) ).
fof(f481,definition,
( spl14_51
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl14_51])],[avatar_definition]) ).
fof(f484,plain,
( ~ spl14_51
| ~ spl14_38 ),
inference(avatar_split_clause,[],[f168,f417,f481]) ).
fof(f486,definition,
( spl14_52
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_52])],[avatar_definition]) ).
fof(f488,plain,
( e1 = op(e0,e1)
| ~ spl14_52 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f489,plain,
( ~ spl14_51
| spl14_52 ),
inference(avatar_split_clause,[],[f169,f486,f481]) ).
fof(f491,definition,
( spl14_53
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_53])],[avatar_definition]) ).
fof(f493,plain,
( e1 = op(e1,e0)
| ~ spl14_53 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f494,plain,
( ~ spl14_51
| spl14_53 ),
inference(avatar_split_clause,[],[f170,f491,f481]) ).
fof(f496,definition,
( spl14_54
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl14_54])],[avatar_definition]) ).
fof(f499,plain,
( ~ spl14_54
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f171,f428,f496]) ).
fof(f501,plain,
( ~ spl14_54
| spl14_40 ),
inference(avatar_split_clause,[],[f173,f428,f496]) ).
fof(f503,definition,
( spl14_55
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl14_55])],[avatar_definition]) ).
fof(f506,plain,
( ~ spl14_55
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f174,f447,f503]) ).
fof(f508,definition,
( spl14_56
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_56])],[avatar_definition]) ).
fof(f510,plain,
( e1 = op(e2,e1)
| ~ spl14_56 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ~ spl14_55
| spl14_56 ),
inference(avatar_split_clause,[],[f175,f508,f503]) ).
fof(f513,definition,
( spl14_57
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_57])],[avatar_definition]) ).
fof(f515,plain,
( e1 = op(e1,e2)
| ~ spl14_57 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f516,plain,
( ~ spl14_55
| spl14_57 ),
inference(avatar_split_clause,[],[f176,f513,f503]) ).
fof(f518,definition,
( spl14_58
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl14_58])],[avatar_definition]) ).
fof(f521,plain,
( ~ spl14_58
| ~ spl14_48 ),
inference(avatar_split_clause,[],[f177,f466,f518]) ).
fof(f523,definition,
( spl14_59
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_59])],[avatar_definition]) ).
fof(f525,plain,
( e1 = op(e3,e1)
| ~ spl14_59 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f526,plain,
( ~ spl14_58
| spl14_59 ),
inference(avatar_split_clause,[],[f178,f523,f518]) ).
fof(f528,definition,
( spl14_60
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_60])],[avatar_definition]) ).
fof(f530,plain,
( e1 = op(e1,e3)
| ~ spl14_60 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f531,plain,
( ~ spl14_58
| spl14_60 ),
inference(avatar_split_clause,[],[f179,f528,f518]) ).
fof(f533,definition,
( spl14_61
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl14_61])],[avatar_definition]) ).
fof(f536,plain,
( ~ spl14_61
| ~ spl14_38 ),
inference(avatar_split_clause,[],[f180,f417,f533]) ).
fof(f538,definition,
( spl14_62
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_62])],[avatar_definition]) ).
fof(f540,plain,
( e2 = op(e0,e2)
| ~ spl14_62 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f541,plain,
( ~ spl14_61
| spl14_62 ),
inference(avatar_split_clause,[],[f181,f538,f533]) ).
fof(f543,definition,
( spl14_63
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_63])],[avatar_definition]) ).
fof(f545,plain,
( e2 = op(e2,e0)
| ~ spl14_63 ),
inference(avatar_component_clause,[],[f543]) ).
fof(f546,plain,
( ~ spl14_61
| spl14_63 ),
inference(avatar_split_clause,[],[f182,f543,f533]) ).
fof(f548,definition,
( spl14_64
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl14_64])],[avatar_definition]) ).
fof(f551,plain,
( ~ spl14_64
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f183,f428,f548]) ).
fof(f553,definition,
( spl14_65
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_65])],[avatar_definition]) ).
fof(f555,plain,
( e2 = op(e1,e2)
| ~ spl14_65 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f556,plain,
( ~ spl14_64
| spl14_65 ),
inference(avatar_split_clause,[],[f184,f553,f548]) ).
fof(f558,definition,
( spl14_66
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_66])],[avatar_definition]) ).
fof(f560,plain,
( e2 = op(e2,e1)
| ~ spl14_66 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f561,plain,
( ~ spl14_64
| spl14_66 ),
inference(avatar_split_clause,[],[f185,f558,f548]) ).
fof(f563,definition,
( spl14_67
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl14_67])],[avatar_definition]) ).
fof(f566,plain,
( ~ spl14_67
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f186,f447,f563]) ).
fof(f568,plain,
( ~ spl14_67
| spl14_44 ),
inference(avatar_split_clause,[],[f188,f447,f563]) ).
fof(f570,definition,
( spl14_68
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl14_68])],[avatar_definition]) ).
fof(f573,plain,
( ~ spl14_68
| ~ spl14_48 ),
inference(avatar_split_clause,[],[f189,f466,f570]) ).
fof(f575,definition,
( spl14_69
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_69])],[avatar_definition]) ).
fof(f577,plain,
( e2 = op(e3,e2)
| ~ spl14_69 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f578,plain,
( ~ spl14_68
| spl14_69 ),
inference(avatar_split_clause,[],[f190,f575,f570]) ).
fof(f580,definition,
( spl14_70
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_70])],[avatar_definition]) ).
fof(f582,plain,
( e2 = op(e2,e3)
| ~ spl14_70 ),
inference(avatar_component_clause,[],[f580]) ).
fof(f583,plain,
( ~ spl14_68
| spl14_70 ),
inference(avatar_split_clause,[],[f191,f580,f570]) ).
fof(f585,definition,
( spl14_71
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl14_71])],[avatar_definition]) ).
fof(f588,plain,
( ~ spl14_71
| ~ spl14_38 ),
inference(avatar_split_clause,[],[f192,f417,f585]) ).
fof(f590,definition,
( spl14_72
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_72])],[avatar_definition]) ).
fof(f592,plain,
( e3 = op(e0,e3)
| ~ spl14_72 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f593,plain,
( ~ spl14_71
| spl14_72 ),
inference(avatar_split_clause,[],[f193,f590,f585]) ).
fof(f595,definition,
( spl14_73
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_73])],[avatar_definition]) ).
fof(f597,plain,
( e3 = op(e3,e0)
| ~ spl14_73 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f598,plain,
( ~ spl14_71
| spl14_73 ),
inference(avatar_split_clause,[],[f194,f595,f585]) ).
fof(f600,definition,
( spl14_74
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl14_74])],[avatar_definition]) ).
fof(f603,plain,
( ~ spl14_74
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f195,f428,f600]) ).
fof(f605,definition,
( spl14_75
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_75])],[avatar_definition]) ).
fof(f607,plain,
( e3 = op(e1,e3)
| ~ spl14_75 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f608,plain,
( ~ spl14_74
| spl14_75 ),
inference(avatar_split_clause,[],[f196,f605,f600]) ).
fof(f610,definition,
( spl14_76
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_76])],[avatar_definition]) ).
fof(f612,plain,
( e3 = op(e3,e1)
| ~ spl14_76 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f613,plain,
( ~ spl14_74
| spl14_76 ),
inference(avatar_split_clause,[],[f197,f610,f600]) ).
fof(f614,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| ~ spl14_44
| spl14_48 ),
inference(avatar_split_clause,[],[f198,f466,f447,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f616,definition,
( spl14_77
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_77])],[avatar_definition]) ).
fof(f618,plain,
( e3 = op(e2,e3)
| ~ spl14_77 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f619,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_77
| spl14_48 ),
inference(avatar_split_clause,[],[f199,f466,f616,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f621,definition,
( spl14_78
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_78])],[avatar_definition]) ).
fof(f623,plain,
( e3 = op(e3,e2)
| ~ spl14_78 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f624,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_78
| spl14_48 ),
inference(avatar_split_clause,[],[f200,f466,f621,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f625,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| ~ spl14_44
| spl14_48 ),
inference(avatar_split_clause,[],[f201,f466,f447,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f626,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_77
| spl14_48 ),
inference(avatar_split_clause,[],[f202,f466,f616,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f627,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_78
| spl14_48 ),
inference(avatar_split_clause,[],[f203,f466,f621,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f628,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| ~ spl14_44
| ~ spl14_48 ),
inference(avatar_split_clause,[],[f204,f466,f447,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f629,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_77
| ~ spl14_48 ),
inference(avatar_split_clause,[],[f205,f466,f616,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f630,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_78
| ~ spl14_48 ),
inference(avatar_split_clause,[],[f206,f466,f621,f600,f585,f570,f563,f548,f533,f518,f503,f496,f481,f462,f443,f424,f413]) ).
fof(f631,plain,
( spl14_38
| spl14_40
| spl14_44
| spl14_48 ),
inference(avatar_split_clause,[],[f207,f466,f447,f428,f417]) ).
fof(f632,plain,
( ~ spl14_27
| spl14_42 ),
inference(avatar_split_clause,[],[f208,f438,f361]) ).
fof(f633,plain,
( ~ spl14_16
| spl14_46 ),
inference(avatar_split_clause,[],[f209,f457,f311]) ).
fof(f634,plain,
( ~ spl14_1
| spl14_50 ),
inference(avatar_split_clause,[],[f210,f476,f245]) ).
fof(f635,plain,
( ~ spl14_34
| spl14_53 ),
inference(avatar_split_clause,[],[f211,f491,f395]) ).
fof(f636,plain,
( ~ spl14_18
| spl14_57 ),
inference(avatar_split_clause,[],[f212,f513,f320]) ).
fof(f637,plain,
( ~ spl14_4
| spl14_60 ),
inference(avatar_split_clause,[],[f213,f528,f258]) ).
fof(f638,plain,
( ~ spl14_35
| spl14_63 ),
inference(avatar_split_clause,[],[f214,f543,f400]) ).
fof(f639,plain,
( ~ spl14_28
| spl14_66 ),
inference(avatar_split_clause,[],[f215,f558,f366]) ).
fof(f640,plain,
( ~ spl14_9
| spl14_70 ),
inference(avatar_split_clause,[],[f216,f580,f280]) ).
fof(f641,plain,
( ~ spl14_36
| spl14_73 ),
inference(avatar_split_clause,[],[f217,f595,f406]) ).
fof(f642,plain,
( ~ spl14_30
| spl14_76 ),
inference(avatar_split_clause,[],[f218,f610,f376]) ).
fof(f643,plain,
( ~ spl14_21
| spl14_78 ),
inference(avatar_split_clause,[],[f219,f621,f334]) ).
fof(f645,plain,
( spl14_38
| spl14_41
| spl14_45
| spl14_49 ),
inference(avatar_split_clause,[],[f71,f471,f452,f433,f417]) ).
fof(f647,definition,
( spl14_79
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_79])],[avatar_definition]) ).
fof(f649,plain,
( e1 = op(e0,e2)
| ~ spl14_79 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f651,definition,
( spl14_80
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_80])],[avatar_definition]) ).
fof(f653,plain,
( e1 = op(e0,e3)
| ~ spl14_80 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f654,plain,
( spl14_27
| spl14_52
| spl14_79
| spl14_80 ),
inference(avatar_split_clause,[],[f72,f651,f647,f486,f361]) ).
fof(f656,definition,
( spl14_81
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_81])],[avatar_definition]) ).
fof(f658,plain,
( e1 = op(e2,e0)
| ~ spl14_81 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f660,definition,
( spl14_82
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_82])],[avatar_definition]) ).
fof(f662,plain,
( e1 = op(e3,e0)
| ~ spl14_82 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,plain,
( spl14_27
| spl14_53
| spl14_81
| spl14_82 ),
inference(avatar_split_clause,[],[f73,f660,f656,f491,f361]) ).
fof(f665,definition,
( spl14_83
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_83])],[avatar_definition]) ).
fof(f667,plain,
( e2 = op(e0,e1)
| ~ spl14_83 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f669,definition,
( spl14_84
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_84])],[avatar_definition]) ).
fof(f671,plain,
( e2 = op(e0,e3)
| ~ spl14_84 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f672,plain,
( spl14_16
| spl14_83
| spl14_62
| spl14_84 ),
inference(avatar_split_clause,[],[f74,f669,f538,f665,f311]) ).
fof(f674,definition,
( spl14_85
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_85])],[avatar_definition]) ).
fof(f676,plain,
( e2 = op(e1,e0)
| ~ spl14_85 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f678,definition,
( spl14_86
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_86])],[avatar_definition]) ).
fof(f680,plain,
( e2 = op(e3,e0)
| ~ spl14_86 ),
inference(avatar_component_clause,[],[f678]) ).
fof(f681,plain,
( spl14_16
| spl14_85
| spl14_63
| spl14_86 ),
inference(avatar_split_clause,[],[f75,f678,f543,f674,f311]) ).
fof(f683,definition,
( spl14_87
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_87])],[avatar_definition]) ).
fof(f685,plain,
( e3 = op(e0,e1)
| ~ spl14_87 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,definition,
( spl14_88
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_88])],[avatar_definition]) ).
fof(f689,plain,
( e3 = op(e0,e2)
| ~ spl14_88 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( spl14_1
| spl14_87
| spl14_88
| spl14_72 ),
inference(avatar_split_clause,[],[f76,f590,f687,f683,f245]) ).
fof(f692,definition,
( spl14_89
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_89])],[avatar_definition]) ).
fof(f694,plain,
( e3 = op(e1,e0)
| ~ spl14_89 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f696,definition,
( spl14_90
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_90])],[avatar_definition]) ).
fof(f698,plain,
( e3 = op(e2,e0)
| ~ spl14_90 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f699,plain,
( spl14_1
| spl14_89
| spl14_90
| spl14_73 ),
inference(avatar_split_clause,[],[f77,f595,f696,f692,f245]) ).
fof(f701,definition,
( spl14_91
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_91])],[avatar_definition]) ).
fof(f703,plain,
( e0 = op(e1,e2)
| ~ spl14_91 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f705,definition,
( spl14_92
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_92])],[avatar_definition]) ).
fof(f707,plain,
( e0 = op(e1,e3)
| ~ spl14_92 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f708,plain,
( spl14_41
| spl14_34
| spl14_91
| spl14_92 ),
inference(avatar_split_clause,[],[f78,f705,f701,f395,f433]) ).
fof(f710,definition,
( spl14_93
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_93])],[avatar_definition]) ).
fof(f712,plain,
( e0 = op(e2,e1)
| ~ spl14_93 ),
inference(avatar_component_clause,[],[f710]) ).
fof(f714,definition,
( spl14_94
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_94])],[avatar_definition]) ).
fof(f716,plain,
( e0 = op(e3,e1)
| ~ spl14_94 ),
inference(avatar_component_clause,[],[f714]) ).
fof(f717,plain,
( spl14_42
| spl14_34
| spl14_93
| spl14_94 ),
inference(avatar_split_clause,[],[f79,f714,f710,f395,f438]) ).
fof(f719,plain,
( spl14_52
| spl14_40
| spl14_56
| spl14_59 ),
inference(avatar_split_clause,[],[f81,f523,f508,f428,f486]) ).
fof(f721,definition,
( spl14_95
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_95])],[avatar_definition]) ).
fof(f723,plain,
( e2 = op(e1,e3)
| ~ spl14_95 ),
inference(avatar_component_clause,[],[f721]) ).
fof(f724,plain,
( spl14_85
| spl14_18
| spl14_65
| spl14_95 ),
inference(avatar_split_clause,[],[f82,f721,f553,f320,f674]) ).
fof(f726,definition,
( spl14_96
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_96])],[avatar_definition]) ).
fof(f728,plain,
( e2 = op(e3,e1)
| ~ spl14_96 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f729,plain,
( spl14_83
| spl14_18
| spl14_66
| spl14_96 ),
inference(avatar_split_clause,[],[f83,f726,f558,f320,f665]) ).
fof(f731,definition,
( spl14_97
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_97])],[avatar_definition]) ).
fof(f733,plain,
( e3 = op(e1,e2)
| ~ spl14_97 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f734,plain,
( spl14_89
| spl14_4
| spl14_97
| spl14_75 ),
inference(avatar_split_clause,[],[f84,f605,f731,f258,f692]) ).
fof(f736,definition,
( spl14_98
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_98])],[avatar_definition]) ).
fof(f738,plain,
( e3 = op(e2,e1)
| ~ spl14_98 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f739,plain,
( spl14_87
| spl14_4
| spl14_98
| spl14_76 ),
inference(avatar_split_clause,[],[f85,f610,f736,f258,f683]) ).
fof(f741,definition,
( spl14_99
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_99])],[avatar_definition]) ).
fof(f743,plain,
( e0 = op(e2,e3)
| ~ spl14_99 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f744,plain,
( spl14_45
| spl14_93
| spl14_35
| spl14_99 ),
inference(avatar_split_clause,[],[f86,f741,f400,f710,f452]) ).
fof(f746,definition,
( spl14_100
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_100])],[avatar_definition]) ).
fof(f748,plain,
( e0 = op(e3,e2)
| ~ spl14_100 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f749,plain,
( spl14_46
| spl14_91
| spl14_35
| spl14_100 ),
inference(avatar_split_clause,[],[f87,f746,f400,f701,f457]) ).
fof(f751,definition,
( spl14_101
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_101])],[avatar_definition]) ).
fof(f753,plain,
( e1 = op(e2,e3)
| ~ spl14_101 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f754,plain,
( spl14_81
| spl14_56
| spl14_28
| spl14_101 ),
inference(avatar_split_clause,[],[f88,f751,f366,f508,f656]) ).
fof(f756,definition,
( spl14_102
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_102])],[avatar_definition]) ).
fof(f758,plain,
( e1 = op(e3,e2)
| ~ spl14_102 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f759,plain,
( spl14_79
| spl14_57
| spl14_28
| spl14_102 ),
inference(avatar_split_clause,[],[f89,f756,f366,f513,f647]) ).
fof(f760,plain,
( spl14_63
| spl14_66
| spl14_44
| spl14_70 ),
inference(avatar_split_clause,[],[f90,f580,f447,f558,f543]) ).
fof(f761,plain,
( spl14_62
| spl14_65
| spl14_44
| spl14_69 ),
inference(avatar_split_clause,[],[f91,f575,f447,f553,f538]) ).
fof(f762,plain,
( spl14_90
| spl14_98
| spl14_9
| spl14_77 ),
inference(avatar_split_clause,[],[f92,f616,f280,f736,f696]) ).
fof(f763,plain,
( spl14_88
| spl14_97
| spl14_9
| spl14_78 ),
inference(avatar_split_clause,[],[f93,f621,f280,f731,f687]) ).
fof(f764,plain,
( spl14_49
| spl14_94
| spl14_100
| spl14_36 ),
inference(avatar_split_clause,[],[f94,f406,f746,f714,f471]) ).
fof(f765,plain,
( spl14_50
| spl14_92
| spl14_99
| spl14_36 ),
inference(avatar_split_clause,[],[f95,f406,f741,f705,f476]) ).
fof(f766,plain,
( spl14_82
| spl14_59
| spl14_102
| spl14_30 ),
inference(avatar_split_clause,[],[f96,f376,f756,f523,f660]) ).
fof(f767,plain,
( spl14_80
| spl14_60
| spl14_101
| spl14_30 ),
inference(avatar_split_clause,[],[f97,f376,f751,f528,f651]) ).
fof(f768,plain,
( spl14_86
| spl14_96
| spl14_69
| spl14_21 ),
inference(avatar_split_clause,[],[f98,f334,f575,f726,f678]) ).
fof(f769,plain,
( spl14_84
| spl14_95
| spl14_70
| spl14_21 ),
inference(avatar_split_clause,[],[f99,f334,f580,f721,f669]) ).
fof(f770,plain,
( spl14_73
| spl14_76
| spl14_78
| spl14_48 ),
inference(avatar_split_clause,[],[f100,f466,f621,f610,f595]) ).
fof(f771,plain,
( spl14_72
| spl14_75
| spl14_77
| spl14_48 ),
inference(avatar_split_clause,[],[f101,f466,f616,f605,f590]) ).
fof(f772,plain,
( spl14_38
| spl14_27
| spl14_16
| spl14_1 ),
inference(avatar_split_clause,[],[f54,f245,f311,f361,f417]) ).
fof(f776,plain,
( spl14_41
| spl14_53
| spl14_85
| spl14_89 ),
inference(avatar_split_clause,[],[f58,f692,f674,f491,f433]) ).
fof(f777,plain,
( spl14_34
| spl14_40
| spl14_18
| spl14_4 ),
inference(avatar_split_clause,[],[f59,f258,f320,f428,f395]) ).
fof(f779,plain,
( spl14_92
| spl14_60
| spl14_95
| spl14_75 ),
inference(avatar_split_clause,[],[f61,f605,f721,f528,f705]) ).
fof(f782,plain,
( spl14_35
| spl14_28
| spl14_44
| spl14_9 ),
inference(avatar_split_clause,[],[f64,f280,f447,f366,f400]) ).
fof(f787,plain,
( spl14_36
| spl14_30
| spl14_21
| spl14_48 ),
inference(avatar_split_clause,[],[f69,f466,f334,f376,f406]) ).
fof(f791,plain,
( e1 != op(op(e3,e3),e2)
| ~ spl14_9
| spl14_15 ),
inference(forward_demodulation,[],[f308,f281]) ).
fof(f792,plain,
( e3 != op(e2,e2)
| ~ spl14_16
| spl14_17 ),
inference(forward_demodulation,[],[f317,f312]) ).
fof(f793,plain,
( e2 = e3
| ~ spl14_4
| ~ spl14_18 ),
inference(forward_demodulation,[],[f321,f259]) ).
fof(f794,plain,
( e3 != op(op(e2,e2),e0)
| ~ spl14_16
| spl14_20 ),
inference(forward_demodulation,[],[f331,f312]) ).
fof(f795,plain,
( e1 = e2
| ~ spl14_16
| ~ spl14_27 ),
inference(forward_demodulation,[],[f362,f312]) ).
fof(f799,plain,
( e0 = e2
| ~ spl14_16
| ~ spl14_38 ),
inference(forward_demodulation,[],[f418,f312]) ).
fof(f807,plain,
( e1 != op(e0,e2)
| ~ spl14_9
| spl14_15
| ~ spl14_36 ),
inference(forward_demodulation,[],[f791,f407]) ).
fof(f808,plain,
( $false
| ~ spl14_9
| ~ spl14_16
| spl14_17 ),
inference(forward_subsumption_resolution,[],[f792,f281]) ).
fof(f809,plain,
( ~ spl14_9
| ~ spl14_16
| spl14_17 ),
inference(avatar_contradiction_clause,[],[f808]) ).
fof(f810,plain,
( $false
| ~ spl14_4
| ~ spl14_18 ),
inference(forward_subsumption_resolution,[],[f793,f150]) ).
fof(f811,plain,
( ~ spl14_4
| ~ spl14_18 ),
inference(avatar_contradiction_clause,[],[f810]) ).
fof(f813,plain,
( $false
| ~ spl14_16
| ~ spl14_27 ),
inference(forward_subsumption_resolution,[],[f795,f152]) ).
fof(f814,plain,
( ~ spl14_16
| ~ spl14_27 ),
inference(avatar_contradiction_clause,[],[f813]) ).
fof(f815,plain,
( $false
| ~ spl14_16
| ~ spl14_38 ),
inference(forward_subsumption_resolution,[],[f799,f154]) ).
fof(f816,plain,
( ~ spl14_16
| ~ spl14_38 ),
inference(avatar_contradiction_clause,[],[f815]) ).
fof(f824,plain,
( e1 != op(op(e2,e2),e0)
| spl14_3
| ~ spl14_16 ),
inference(forward_demodulation,[],[f255,f312]) ).
fof(f825,plain,
( e2 != op(e3,e3)
| ~ spl14_4
| spl14_5 ),
inference(forward_demodulation,[],[f264,f259]) ).
fof(f827,plain,
( e1 != op(e2,e2)
| spl14_7
| ~ spl14_16 ),
inference(forward_demodulation,[],[f273,f312]) ).
fof(f828,plain,
( e1 != op(e3,e3)
| ~ spl14_9
| spl14_10 ),
inference(forward_demodulation,[],[f286,f281]) ).
fof(f837,plain,
( e1 = e3
| ~ spl14_4
| ~ spl14_40 ),
inference(forward_demodulation,[],[f429,f259]) ).
fof(f838,plain,
( e0 = e1
| ~ spl14_42
| ~ spl14_52 ),
inference(forward_demodulation,[],[f488,f440]) ).
fof(f839,plain,
( e0 = e1
| ~ spl14_41
| ~ spl14_53 ),
inference(forward_demodulation,[],[f493,f435]) ).
fof(f840,plain,
( e1 != op(e3,e0)
| spl14_3
| ~ spl14_9
| ~ spl14_16 ),
inference(forward_demodulation,[],[f824,f281]) ).
fof(f846,plain,
( $false
| ~ spl14_4
| ~ spl14_40 ),
inference(forward_subsumption_resolution,[],[f837,f151]) ).
fof(f847,plain,
( ~ spl14_4
| ~ spl14_40 ),
inference(avatar_contradiction_clause,[],[f846]) ).
fof(f848,plain,
( $false
| ~ spl14_42
| ~ spl14_52 ),
inference(forward_subsumption_resolution,[],[f838,f155]) ).
fof(f849,plain,
( ~ spl14_42
| ~ spl14_52 ),
inference(avatar_contradiction_clause,[],[f848]) ).
fof(f850,plain,
( $false
| ~ spl14_41
| ~ spl14_53 ),
inference(forward_subsumption_resolution,[],[f839,f155]) ).
fof(f851,plain,
( ~ spl14_41
| ~ spl14_53 ),
inference(avatar_contradiction_clause,[],[f850]) ).
fof(f854,plain,
( e0 = e3
| ~ spl14_4
| ~ spl14_34 ),
inference(forward_demodulation,[],[f396,f259]) ).
fof(f859,plain,
( $false
| ~ spl14_4
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f854,f153]) ).
fof(f860,plain,
( ~ spl14_4
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f859]) ).
fof(f863,plain,
( e0 = e2
| ~ spl14_66
| ~ spl14_93 ),
inference(forward_demodulation,[],[f712,f560]) ).
fof(f864,plain,
( e0 = e2
| ~ spl14_69
| ~ spl14_100 ),
inference(forward_demodulation,[],[f748,f577]) ).
fof(f870,plain,
( $false
| ~ spl14_66
| ~ spl14_93 ),
inference(forward_subsumption_resolution,[],[f863,f154]) ).
fof(f871,plain,
( ~ spl14_66
| ~ spl14_93 ),
inference(avatar_contradiction_clause,[],[f870]) ).
fof(f872,plain,
( $false
| ~ spl14_69
| ~ spl14_100 ),
inference(forward_subsumption_resolution,[],[f864,f154]) ).
fof(f873,plain,
( ~ spl14_69
| ~ spl14_100 ),
inference(avatar_contradiction_clause,[],[f872]) ).
fof(f897,plain,
( e1 = e2
| ~ spl14_57
| ~ spl14_65 ),
inference(superposition,[],[f555,f515]) ).
fof(f901,plain,
( $false
| ~ spl14_57
| ~ spl14_65 ),
inference(forward_subsumption_resolution,[],[f897,f152]) ).
fof(f902,plain,
( ~ spl14_57
| ~ spl14_65 ),
inference(avatar_contradiction_clause,[],[f901]) ).
fof(f904,plain,
( e1 = e2
| ~ spl14_69
| ~ spl14_102 ),
inference(forward_demodulation,[],[f758,f577]) ).
fof(f905,plain,
( $false
| ~ spl14_69
| ~ spl14_102 ),
inference(forward_subsumption_resolution,[],[f904,f152]) ).
fof(f906,plain,
( ~ spl14_69
| ~ spl14_102 ),
inference(avatar_contradiction_clause,[],[f905]) ).
fof(f909,plain,
( e1 = e2
| ~ spl14_56
| ~ spl14_66 ),
inference(superposition,[],[f560,f510]) ).
fof(f910,plain,
( e1 = e2
| ~ spl14_56
| ~ spl14_66 ),
inference(superposition,[],[f510,f560]) ).
fof(f911,plain,
( $false
| ~ spl14_56
| ~ spl14_66 ),
inference(forward_subsumption_resolution,[],[f910,f152]) ).
fof(f912,plain,
( ~ spl14_56
| ~ spl14_66 ),
inference(avatar_contradiction_clause,[],[f911]) ).
fof(f913,plain,
( $false
| ~ spl14_56
| ~ spl14_66 ),
inference(forward_subsumption_resolution,[],[f909,f152]) ).
fof(f914,plain,
( ~ spl14_56
| ~ spl14_66 ),
inference(avatar_contradiction_clause,[],[f913]) ).
fof(f916,plain,
( e0 = e1
| ~ spl14_60
| ~ spl14_92 ),
inference(superposition,[],[f707,f530]) ).
fof(f920,plain,
( $false
| ~ spl14_60
| ~ spl14_92 ),
inference(forward_subsumption_resolution,[],[f916,f155]) ).
fof(f921,plain,
( ~ spl14_60
| ~ spl14_92 ),
inference(avatar_contradiction_clause,[],[f920]) ).
fof(f922,plain,
( e1 = e3
| ~ spl14_30
| ~ spl14_48 ),
inference(forward_demodulation,[],[f377,f467]) ).
fof(f925,plain,
( op(e0,e0) != e2
| spl14_5
| ~ spl14_34 ),
inference(forward_demodulation,[],[f264,f396]) ).
fof(f927,plain,
( e2 != op(op(e0,e0),e1)
| spl14_13
| ~ spl14_34 ),
inference(forward_demodulation,[],[f299,f396]) ).
fof(f931,plain,
( $false
| ~ spl14_30
| ~ spl14_48 ),
inference(forward_subsumption_resolution,[],[f922,f151]) ).
fof(f932,plain,
( ~ spl14_30
| ~ spl14_48 ),
inference(avatar_contradiction_clause,[],[f931]) ).
fof(f933,plain,
( $false
| spl14_5
| ~ spl14_16
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f925,f312]) ).
fof(f934,plain,
( spl14_5
| ~ spl14_16
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f933]) ).
fof(f942,plain,
( e1 = e2
| ~ spl14_70
| ~ spl14_101 ),
inference(forward_demodulation,[],[f753,f582]) ).
fof(f943,plain,
( e1 != op(op(e1,e1),e0)
| spl14_3
| ~ spl14_27 ),
inference(forward_demodulation,[],[f255,f362]) ).
fof(f951,plain,
( $false
| ~ spl14_70
| ~ spl14_101 ),
inference(forward_subsumption_resolution,[],[f942,f152]) ).
fof(f952,plain,
( ~ spl14_70
| ~ spl14_101 ),
inference(avatar_contradiction_clause,[],[f951]) ).
fof(f953,plain,
( op(e0,e0) != e1
| spl14_3
| ~ spl14_27
| ~ spl14_34 ),
inference(forward_demodulation,[],[f943,f396]) ).
fof(f959,plain,
( $false
| spl14_3
| ~ spl14_27
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f953,f362]) ).
fof(f960,plain,
( spl14_3
| ~ spl14_27
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f959]) ).
fof(f965,plain,
( e3 != op(op(e1,e1),e0)
| spl14_20
| ~ spl14_27 ),
inference(forward_demodulation,[],[f331,f362]) ).
fof(f969,plain,
( op(e0,e0) != e1
| spl14_10
| ~ spl14_35 ),
inference(forward_demodulation,[],[f286,f401]) ).
fof(f981,plain,
( e3 != op(op(e0,e0),e2)
| spl14_32
| ~ spl14_35 ),
inference(forward_demodulation,[],[f387,f401]) ).
fof(f983,plain,
( e0 = e1
| ~ spl14_46
| ~ spl14_79 ),
inference(forward_demodulation,[],[f649,f459]) ).
fof(f987,plain,
( e3 != op(e1,e2)
| ~ spl14_27
| spl14_32
| ~ spl14_35 ),
inference(forward_demodulation,[],[f981,f362]) ).
fof(f988,plain,
( $false
| ~ spl14_46
| ~ spl14_79 ),
inference(forward_subsumption_resolution,[],[f983,f155]) ).
fof(f989,plain,
( ~ spl14_46
| ~ spl14_79 ),
inference(avatar_contradiction_clause,[],[f988]) ).
fof(f990,plain,
( $false
| ~ spl14_27
| spl14_32
| ~ spl14_35
| ~ spl14_97 ),
inference(forward_subsumption_resolution,[],[f987,f733]) ).
fof(f991,plain,
( ~ spl14_27
| spl14_32
| ~ spl14_35
| ~ spl14_97 ),
inference(avatar_contradiction_clause,[],[f990]) ).
fof(f1004,plain,
( e0 = e2
| ~ spl14_46
| ~ spl14_62 ),
inference(superposition,[],[f540,f459]) ).
fof(f1005,plain,
( e0 = e2
| ~ spl14_46
| ~ spl14_62 ),
inference(superposition,[],[f459,f540]) ).
fof(f1006,plain,
( $false
| ~ spl14_46
| ~ spl14_62 ),
inference(forward_subsumption_resolution,[],[f1005,f154]) ).
fof(f1007,plain,
( ~ spl14_46
| ~ spl14_62 ),
inference(avatar_contradiction_clause,[],[f1006]) ).
fof(f1008,plain,
( $false
| ~ spl14_46
| ~ spl14_62 ),
inference(forward_subsumption_resolution,[],[f1004,f154]) ).
fof(f1009,plain,
( ~ spl14_46
| ~ spl14_62 ),
inference(avatar_contradiction_clause,[],[f1008]) ).
fof(f1011,plain,
( e0 = e2
| ~ spl14_45
| ~ spl14_63 ),
inference(superposition,[],[f545,f454]) ).
fof(f1015,plain,
( $false
| ~ spl14_45
| ~ spl14_63 ),
inference(forward_subsumption_resolution,[],[f1011,f154]) ).
fof(f1016,plain,
( ~ spl14_45
| ~ spl14_63 ),
inference(avatar_contradiction_clause,[],[f1015]) ).
fof(f1021,plain,
( e0 != op(e3,e3)
| ~ spl14_9
| spl14_14 ),
inference(forward_demodulation,[],[f304,f281]) ).
fof(f1023,plain,
( e1 = e2
| ~ spl14_60
| ~ spl14_95 ),
inference(forward_demodulation,[],[f530,f723]) ).
fof(f1025,plain,
( e2 = e3
| ~ spl14_85
| ~ spl14_89 ),
inference(forward_demodulation,[],[f676,f694]) ).
fof(f1027,plain,
( e0 = e2
| ~ spl14_70
| ~ spl14_99 ),
inference(forward_demodulation,[],[f743,f582]) ).
fof(f1032,plain,
( e1 = op(e3,e3)
| ~ spl14_9
| ~ spl14_10 ),
inference(forward_demodulation,[],[f285,f281]) ).
fof(f1039,plain,
( $false
| ~ spl14_60
| ~ spl14_95 ),
inference(forward_subsumption_resolution,[],[f1023,f152]) ).
fof(f1040,plain,
( ~ spl14_60
| ~ spl14_95 ),
inference(avatar_contradiction_clause,[],[f1039]) ).
fof(f1041,plain,
( $false
| ~ spl14_85
| ~ spl14_89 ),
inference(forward_subsumption_resolution,[],[f1025,f150]) ).
fof(f1042,plain,
( ~ spl14_85
| ~ spl14_89 ),
inference(avatar_contradiction_clause,[],[f1041]) ).
fof(f1043,plain,
( $false
| ~ spl14_70
| ~ spl14_99 ),
inference(forward_subsumption_resolution,[],[f1027,f154]) ).
fof(f1044,plain,
( ~ spl14_70
| ~ spl14_99 ),
inference(avatar_contradiction_clause,[],[f1043]) ).
fof(f1046,plain,
( e1 = e3
| ~ spl14_9
| ~ spl14_10
| ~ spl14_48 ),
inference(forward_demodulation,[],[f1032,f467]) ).
fof(f1052,plain,
( $false
| ~ spl14_9
| ~ spl14_10
| ~ spl14_48 ),
inference(forward_subsumption_resolution,[],[f1046,f151]) ).
fof(f1053,plain,
( ~ spl14_9
| ~ spl14_10
| ~ spl14_48 ),
inference(avatar_contradiction_clause,[],[f1052]) ).
fof(f1060,plain,
( e2 = e3
| ~ spl14_21
| ~ spl14_48 ),
inference(forward_demodulation,[],[f335,f467]) ).
fof(f1064,plain,
( e2 = e3
| ~ spl14_66
| ~ spl14_98 ),
inference(forward_demodulation,[],[f560,f738]) ).
fof(f1066,plain,
( e2 = e3
| ~ spl14_73
| ~ spl14_86 ),
inference(forward_demodulation,[],[f680,f597]) ).
fof(f1070,plain,
( e0 != op(e1,e1)
| spl14_14
| ~ spl14_28 ),
inference(forward_demodulation,[],[f304,f367]) ).
fof(f1073,plain,
( e0 != op(op(e1,e1),e2)
| spl14_11
| ~ spl14_28 ),
inference(forward_demodulation,[],[f290,f367]) ).
fof(f1074,plain,
( e1 = op(e1,e1)
| ~ spl14_10
| ~ spl14_28 ),
inference(forward_demodulation,[],[f285,f367]) ).
fof(f1076,plain,
( e1 = op(op(e1,e1),e2)
| ~ spl14_15
| ~ spl14_28 ),
inference(forward_demodulation,[],[f307,f367]) ).
fof(f1078,plain,
( $false
| ~ spl14_21
| ~ spl14_48 ),
inference(forward_subsumption_resolution,[],[f1060,f150]) ).
fof(f1079,plain,
( ~ spl14_21
| ~ spl14_48 ),
inference(avatar_contradiction_clause,[],[f1078]) ).
fof(f1082,plain,
( $false
| ~ spl14_66
| ~ spl14_98 ),
inference(forward_subsumption_resolution,[],[f1064,f150]) ).
fof(f1083,plain,
( ~ spl14_66
| ~ spl14_98 ),
inference(avatar_contradiction_clause,[],[f1082]) ).
fof(f1084,plain,
( $false
| ~ spl14_73
| ~ spl14_86 ),
inference(forward_subsumption_resolution,[],[f1066,f150]) ).
fof(f1085,plain,
( ~ spl14_73
| ~ spl14_86 ),
inference(avatar_contradiction_clause,[],[f1084]) ).
fof(f1088,plain,
( e0 != op(e0,e2)
| spl14_11
| ~ spl14_28
| ~ spl14_34 ),
inference(forward_demodulation,[],[f1073,f396]) ).
fof(f1091,plain,
( e1 = op(e0,e2)
| ~ spl14_15
| ~ spl14_28
| ~ spl14_34 ),
inference(forward_demodulation,[],[f1076,f396]) ).
fof(f1093,plain,
( $false
| spl14_11
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(forward_subsumption_resolution,[],[f1088,f459]) ).
fof(f1094,plain,
( spl14_11
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(avatar_contradiction_clause,[],[f1093]) ).
fof(f1098,plain,
( e0 = e1
| ~ spl14_15
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(forward_demodulation,[],[f1091,f459]) ).
fof(f1099,plain,
( $false
| ~ spl14_15
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(forward_subsumption_resolution,[],[f1098,f155]) ).
fof(f1100,plain,
( ~ spl14_15
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(avatar_contradiction_clause,[],[f1099]) ).
fof(f1122,plain,
( e1 = e3
| ~ spl14_72
| ~ spl14_80 ),
inference(forward_demodulation,[],[f653,f592]) ).
fof(f1123,plain,
( e0 = e1
| ~ spl14_45
| ~ spl14_81 ),
inference(forward_demodulation,[],[f658,f454]) ).
fof(f1138,plain,
( $false
| ~ spl14_72
| ~ spl14_80 ),
inference(forward_subsumption_resolution,[],[f1122,f151]) ).
fof(f1139,plain,
( ~ spl14_72
| ~ spl14_80 ),
inference(avatar_contradiction_clause,[],[f1138]) ).
fof(f1140,plain,
( $false
| ~ spl14_45
| ~ spl14_81 ),
inference(forward_subsumption_resolution,[],[f1123,f155]) ).
fof(f1141,plain,
( ~ spl14_45
| ~ spl14_81 ),
inference(avatar_contradiction_clause,[],[f1140]) ).
fof(f1148,plain,
( e1 = e3
| ~ spl14_56
| ~ spl14_98 ),
inference(forward_demodulation,[],[f510,f738]) ).
fof(f1150,plain,
( $false
| ~ spl14_56
| ~ spl14_98 ),
inference(forward_subsumption_resolution,[],[f1148,f151]) ).
fof(f1151,plain,
( ~ spl14_56
| ~ spl14_98 ),
inference(avatar_contradiction_clause,[],[f1150]) ).
fof(f1159,plain,
( e2 != op(e2,e2)
| spl14_5
| ~ spl14_18 ),
inference(forward_demodulation,[],[f264,f321]) ).
fof(f1163,plain,
( e0 != op(e2,e2)
| spl14_12
| ~ spl14_18 ),
inference(forward_demodulation,[],[f295,f321]) ).
fof(f1166,plain,
( e3 != op(e2,e0)
| ~ spl14_18
| spl14_20
| ~ spl14_27 ),
inference(forward_demodulation,[],[f965,f321]) ).
fof(f1168,plain,
( e1 != op(e1,e1)
| spl14_10
| ~ spl14_28 ),
inference(forward_demodulation,[],[f286,f367]) ).
fof(f1169,plain,
( e1 != op(op(e1,e1),e2)
| spl14_15
| ~ spl14_28 ),
inference(forward_demodulation,[],[f308,f367]) ).
fof(f1170,plain,
( e3 = op(e1,e1)
| ~ spl14_28
| ~ spl14_29 ),
inference(forward_demodulation,[],[f371,f367]) ).
fof(f1175,plain,
( e3 != op(op(e1,e1),e2)
| ~ spl14_28
| spl14_32 ),
inference(forward_demodulation,[],[f387,f367]) ).
fof(f1185,plain,
( e1 != op(e2,e2)
| spl14_15
| ~ spl14_18
| ~ spl14_28 ),
inference(forward_demodulation,[],[f1169,f321]) ).
fof(f1186,plain,
( $false
| spl14_4
| ~ spl14_28
| ~ spl14_29 ),
inference(forward_subsumption_resolution,[],[f1170,f260]) ).
fof(f1187,plain,
( spl14_4
| ~ spl14_28
| ~ spl14_29 ),
inference(avatar_contradiction_clause,[],[f1186]) ).
fof(f1196,plain,
( $false
| spl14_15
| ~ spl14_18
| ~ spl14_28 ),
inference(forward_subsumption_resolution,[],[f1185,f367]) ).
fof(f1197,plain,
( spl14_15
| ~ spl14_18
| ~ spl14_28 ),
inference(avatar_contradiction_clause,[],[f1196]) ).
fof(f1201,plain,
( e0 = op(op(e1,e1),e2)
| ~ spl14_11
| ~ spl14_28 ),
inference(forward_demodulation,[],[f289,f367]) ).
fof(f1202,plain,
( e0 = op(e1,e1)
| ~ spl14_14
| ~ spl14_28 ),
inference(forward_demodulation,[],[f303,f367]) ).
fof(f1203,plain,
( e3 != op(e1,e1)
| ~ spl14_28
| spl14_29 ),
inference(forward_demodulation,[],[f372,f367]) ).
fof(f1218,plain,
( op(e0,e0) != e3
| spl14_19
| ~ spl14_34 ),
inference(forward_demodulation,[],[f326,f396]) ).
fof(f1221,plain,
( e3 != op(e0,e2)
| ~ spl14_28
| spl14_32
| ~ spl14_34 ),
inference(forward_demodulation,[],[f1175,f396]) ).
fof(f1222,plain,
( e0 = op(e0,e2)
| ~ spl14_11
| ~ spl14_28
| ~ spl14_34 ),
inference(forward_demodulation,[],[f1201,f396]) ).
fof(f1229,plain,
( $false
| ~ spl14_28
| spl14_32
| ~ spl14_34
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f1221,f689]) ).
fof(f1230,plain,
( ~ spl14_28
| spl14_32
| ~ spl14_34
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f1229]) ).
fof(f1240,plain,
( e1 = e3
| ~ spl14_59
| ~ spl14_76 ),
inference(superposition,[],[f612,f525]) ).
fof(f1244,plain,
( $false
| ~ spl14_59
| ~ spl14_76 ),
inference(forward_subsumption_resolution,[],[f1240,f151]) ).
fof(f1245,plain,
( ~ spl14_59
| ~ spl14_76 ),
inference(avatar_contradiction_clause,[],[f1244]) ).
fof(f1254,plain,
( e0 = e2
| ~ spl14_50
| ~ spl14_84 ),
inference(forward_demodulation,[],[f478,f671]) ).
fof(f1256,plain,
( e0 = e2
| ~ spl14_65
| ~ spl14_91 ),
inference(forward_demodulation,[],[f703,f555]) ).
fof(f1279,plain,
( $false
| ~ spl14_4
| ~ spl14_28
| spl14_29 ),
inference(forward_subsumption_resolution,[],[f1203,f259]) ).
fof(f1280,plain,
( ~ spl14_4
| ~ spl14_28
| spl14_29 ),
inference(avatar_contradiction_clause,[],[f1279]) ).
fof(f1283,plain,
( $false
| ~ spl14_50
| ~ spl14_84 ),
inference(forward_subsumption_resolution,[],[f1254,f154]) ).
fof(f1284,plain,
( ~ spl14_50
| ~ spl14_84 ),
inference(avatar_contradiction_clause,[],[f1283]) ).
fof(f1285,plain,
( $false
| ~ spl14_65
| ~ spl14_91 ),
inference(forward_subsumption_resolution,[],[f1256,f154]) ).
fof(f1286,plain,
( ~ spl14_65
| ~ spl14_91 ),
inference(avatar_contradiction_clause,[],[f1285]) ).
fof(f1337,plain,
( e2 = e3
| ~ spl14_69
| ~ spl14_78 ),
inference(superposition,[],[f623,f577]) ).
fof(f1338,plain,
( e2 = e3
| ~ spl14_69
| ~ spl14_78 ),
inference(superposition,[],[f577,f623]) ).
fof(f1339,plain,
( $false
| ~ spl14_69
| ~ spl14_78 ),
inference(forward_subsumption_resolution,[],[f1338,f150]) ).
fof(f1340,plain,
( ~ spl14_69
| ~ spl14_78 ),
inference(avatar_contradiction_clause,[],[f1339]) ).
fof(f1341,plain,
( $false
| ~ spl14_69
| ~ spl14_78 ),
inference(forward_subsumption_resolution,[],[f1337,f150]) ).
fof(f1342,plain,
( ~ spl14_69
| ~ spl14_78 ),
inference(avatar_contradiction_clause,[],[f1341]) ).
fof(f1343,plain,
( e0 = e2
| ~ spl14_41
| ~ spl14_85 ),
inference(forward_demodulation,[],[f435,f676]) ).
fof(f1355,plain,
( $false
| ~ spl14_41
| ~ spl14_85 ),
inference(forward_subsumption_resolution,[],[f1343,f154]) ).
fof(f1356,plain,
( ~ spl14_41
| ~ spl14_85 ),
inference(avatar_contradiction_clause,[],[f1355]) ).
fof(f1360,plain,
( e0 = e2
| ~ spl14_42
| ~ spl14_83 ),
inference(superposition,[],[f667,f440]) ).
fof(f1361,plain,
( e0 = e2
| ~ spl14_42
| ~ spl14_83 ),
inference(superposition,[],[f440,f667]) ).
fof(f1362,plain,
( $false
| ~ spl14_42
| ~ spl14_83 ),
inference(forward_subsumption_resolution,[],[f1361,f154]) ).
fof(f1363,plain,
( ~ spl14_42
| ~ spl14_83 ),
inference(avatar_contradiction_clause,[],[f1362]) ).
fof(f1364,plain,
( $false
| ~ spl14_42
| ~ spl14_83 ),
inference(forward_subsumption_resolution,[],[f1360,f154]) ).
fof(f1365,plain,
( ~ spl14_42
| ~ spl14_83 ),
inference(avatar_contradiction_clause,[],[f1364]) ).
fof(f1367,plain,
( e2 = e3
| ~ spl14_72
| ~ spl14_84 ),
inference(superposition,[],[f671,f592]) ).
fof(f1371,plain,
( $false
| ~ spl14_72
| ~ spl14_84 ),
inference(forward_subsumption_resolution,[],[f1367,f150]) ).
fof(f1372,plain,
( ~ spl14_72
| ~ spl14_84 ),
inference(avatar_contradiction_clause,[],[f1371]) ).
fof(f1376,plain,
( e0 = e3
| ~ spl14_46
| ~ spl14_88 ),
inference(superposition,[],[f689,f459]) ).
fof(f1380,plain,
( $false
| ~ spl14_46
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f1376,f153]) ).
fof(f1381,plain,
( ~ spl14_46
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f1380]) ).
fof(f1383,plain,
( e0 = e3
| ~ spl14_42
| ~ spl14_87 ),
inference(superposition,[],[f685,f440]) ).
fof(f1387,plain,
( $false
| ~ spl14_42
| ~ spl14_87 ),
inference(forward_subsumption_resolution,[],[f1383,f153]) ).
fof(f1388,plain,
( ~ spl14_42
| ~ spl14_87 ),
inference(avatar_contradiction_clause,[],[f1387]) ).
fof(f1389,plain,
( e3 != op(e1,e0)
| ~ spl14_16
| spl14_20
| ~ spl14_28 ),
inference(forward_demodulation,[],[f794,f367]) ).
fof(f1398,plain,
( e1 = e2
| ~ spl14_80
| ~ spl14_84 ),
inference(forward_demodulation,[],[f653,f671]) ).
fof(f1412,plain,
( e1 != op(op(e2,e2),e0)
| spl14_3
| ~ spl14_16 ),
inference(forward_demodulation,[],[f255,f312]) ).
fof(f1417,plain,
( $false
| ~ spl14_80
| ~ spl14_84 ),
inference(forward_subsumption_resolution,[],[f1398,f152]) ).
fof(f1418,plain,
( ~ spl14_80
| ~ spl14_84 ),
inference(avatar_contradiction_clause,[],[f1417]) ).
fof(f1422,plain,
( e1 != op(e1,e0)
| spl14_3
| ~ spl14_16
| ~ spl14_28 ),
inference(forward_demodulation,[],[f1412,f367]) ).
fof(f1426,plain,
( $false
| spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_53 ),
inference(forward_subsumption_resolution,[],[f1422,f493]) ).
fof(f1427,plain,
( spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_53 ),
inference(avatar_contradiction_clause,[],[f1426]) ).
fof(f1430,plain,
( spl14_34
| ~ spl14_14
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f1202,f366,f302,f395]) ).
fof(f1441,plain,
( e2 != op(e3,e1)
| ~ spl14_1
| spl14_13
| ~ spl14_34 ),
inference(forward_demodulation,[],[f927,f246]) ).
fof(f1448,plain,
( e2 = e3
| ~ spl14_83
| ~ spl14_87 ),
inference(forward_demodulation,[],[f667,f685]) ).
fof(f1451,plain,
( e0 = e1
| ~ spl14_50
| ~ spl14_80 ),
inference(forward_demodulation,[],[f653,f478]) ).
fof(f1466,plain,
( op(e0,e0) = e3
| ~ spl14_19
| ~ spl14_34 ),
inference(forward_demodulation,[],[f325,f396]) ).
fof(f1470,plain,
( $false
| ~ spl14_83
| ~ spl14_87 ),
inference(forward_subsumption_resolution,[],[f1448,f150]) ).
fof(f1471,plain,
( ~ spl14_83
| ~ spl14_87 ),
inference(avatar_contradiction_clause,[],[f1470]) ).
fof(f1472,plain,
( $false
| ~ spl14_50
| ~ spl14_80 ),
inference(forward_subsumption_resolution,[],[f1451,f155]) ).
fof(f1473,plain,
( ~ spl14_50
| ~ spl14_80 ),
inference(avatar_contradiction_clause,[],[f1472]) ).
fof(f1485,plain,
( e1 = e2
| ~ spl14_82
| ~ spl14_86 ),
inference(forward_demodulation,[],[f662,f680]) ).
fof(f1492,plain,
( $false
| ~ spl14_82
| ~ spl14_86 ),
inference(forward_subsumption_resolution,[],[f1485,f152]) ).
fof(f1493,plain,
( ~ spl14_82
| ~ spl14_86 ),
inference(avatar_contradiction_clause,[],[f1492]) ).
fof(f1494,plain,
( e2 = e3
| ~ spl14_65
| ~ spl14_97 ),
inference(forward_demodulation,[],[f555,f733]) ).
fof(f1499,plain,
( $false
| ~ spl14_65
| ~ spl14_97 ),
inference(forward_subsumption_resolution,[],[f1494,f150]) ).
fof(f1500,plain,
( ~ spl14_65
| ~ spl14_97 ),
inference(avatar_contradiction_clause,[],[f1499]) ).
fof(f1508,plain,
( e1 = e2
| ~ spl14_52
| ~ spl14_83 ),
inference(superposition,[],[f667,f488]) ).
fof(f1509,plain,
( e1 = e2
| ~ spl14_52
| ~ spl14_83 ),
inference(superposition,[],[f488,f667]) ).
fof(f1510,plain,
( $false
| ~ spl14_52
| ~ spl14_83 ),
inference(forward_subsumption_resolution,[],[f1509,f152]) ).
fof(f1511,plain,
( ~ spl14_52
| ~ spl14_83 ),
inference(avatar_contradiction_clause,[],[f1510]) ).
fof(f1512,plain,
( $false
| ~ spl14_52
| ~ spl14_83 ),
inference(forward_subsumption_resolution,[],[f1508,f152]) ).
fof(f1513,plain,
( ~ spl14_52
| ~ spl14_83 ),
inference(avatar_contradiction_clause,[],[f1512]) ).
fof(f1515,plain,
( op(e0,e0) = e2
| ~ spl14_5
| ~ spl14_34 ),
inference(forward_demodulation,[],[f263,f396]) ).
fof(f1518,plain,
( e2 = e3
| ~ spl14_1
| ~ spl14_16 ),
inference(forward_demodulation,[],[f312,f246]) ).
fof(f1526,plain,
( e3 != op(op(e0,e0),e1)
| spl14_24
| ~ spl14_34 ),
inference(forward_demodulation,[],[f349,f396]) ).
fof(f1532,plain,
( $false
| ~ spl14_1
| ~ spl14_16 ),
inference(forward_subsumption_resolution,[],[f1518,f150]) ).
fof(f1533,plain,
( ~ spl14_1
| ~ spl14_16 ),
inference(avatar_contradiction_clause,[],[f1532]) ).
fof(f1566,plain,
( e0 = e1
| ~ spl14_34
| ~ spl14_40 ),
inference(forward_demodulation,[],[f429,f396]) ).
fof(f1567,plain,
( e0 = e3
| ~ spl14_78
| ~ spl14_100 ),
inference(forward_demodulation,[],[f748,f623]) ).
fof(f1572,plain,
( $false
| ~ spl14_11
| ~ spl14_28
| ~ spl14_34
| spl14_46 ),
inference(forward_subsumption_resolution,[],[f1222,f458]) ).
fof(f1573,plain,
( ~ spl14_11
| ~ spl14_28
| ~ spl14_34
| spl14_46 ),
inference(avatar_contradiction_clause,[],[f1572]) ).
fof(f1585,plain,
( $false
| ~ spl14_34
| ~ spl14_40 ),
inference(forward_subsumption_resolution,[],[f1566,f155]) ).
fof(f1586,plain,
( ~ spl14_34
| ~ spl14_40 ),
inference(avatar_contradiction_clause,[],[f1585]) ).
fof(f1587,plain,
( $false
| ~ spl14_78
| ~ spl14_100 ),
inference(forward_subsumption_resolution,[],[f1567,f153]) ).
fof(f1588,plain,
( ~ spl14_78
| ~ spl14_100 ),
inference(avatar_contradiction_clause,[],[f1587]) ).
fof(f1591,plain,
( ~ spl14_34
| spl14_14
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f1070,f366,f302,f395]) ).
fof(f1593,plain,
( e1 = e3
| ~ spl14_73
| ~ spl14_82 ),
inference(forward_demodulation,[],[f662,f597]) ).
fof(f1602,plain,
( ~ spl14_40
| spl14_10
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f1168,f366,f284,f428]) ).
fof(f1606,plain,
( $false
| ~ spl14_73
| ~ spl14_82 ),
inference(forward_subsumption_resolution,[],[f1593,f151]) ).
fof(f1607,plain,
( ~ spl14_73
| ~ spl14_82 ),
inference(avatar_contradiction_clause,[],[f1606]) ).
fof(f1636,plain,
( e1 = e2
| ~ spl14_53
| ~ spl14_85 ),
inference(superposition,[],[f676,f493]) ).
fof(f1637,plain,
( e1 = e2
| ~ spl14_53
| ~ spl14_85 ),
inference(superposition,[],[f493,f676]) ).
fof(f1639,plain,
( $false
| ~ spl14_53
| ~ spl14_85 ),
inference(forward_subsumption_resolution,[],[f1637,f152]) ).
fof(f1640,plain,
( ~ spl14_53
| ~ spl14_85 ),
inference(avatar_contradiction_clause,[],[f1639]) ).
fof(f1641,plain,
( $false
| ~ spl14_53
| ~ spl14_85 ),
inference(forward_subsumption_resolution,[],[f1636,f152]) ).
fof(f1642,plain,
( ~ spl14_53
| ~ spl14_85 ),
inference(avatar_contradiction_clause,[],[f1641]) ).
fof(f1644,plain,
( e0 = e3
| ~ spl14_45
| ~ spl14_90 ),
inference(superposition,[],[f698,f454]) ).
fof(f1645,plain,
( e0 = e3
| ~ spl14_45
| ~ spl14_90 ),
inference(superposition,[],[f454,f698]) ).
fof(f1646,plain,
( $false
| ~ spl14_45
| ~ spl14_90 ),
inference(forward_subsumption_resolution,[],[f1645,f153]) ).
fof(f1647,plain,
( ~ spl14_45
| ~ spl14_90 ),
inference(avatar_contradiction_clause,[],[f1646]) ).
fof(f1648,plain,
( $false
| ~ spl14_45
| ~ spl14_90 ),
inference(forward_subsumption_resolution,[],[f1644,f153]) ).
fof(f1649,plain,
( ~ spl14_45
| ~ spl14_90 ),
inference(avatar_contradiction_clause,[],[f1648]) ).
fof(f1651,plain,
( e1 = e3
| ~ spl14_53
| ~ spl14_89 ),
inference(superposition,[],[f694,f493]) ).
fof(f1656,plain,
( $false
| ~ spl14_53
| ~ spl14_89 ),
inference(forward_subsumption_resolution,[],[f1651,f151]) ).
fof(f1657,plain,
( ~ spl14_53
| ~ spl14_89 ),
inference(avatar_contradiction_clause,[],[f1656]) ).
fof(f1673,plain,
( ~ spl14_82
| spl14_3
| ~ spl14_9
| ~ spl14_16 ),
inference(avatar_split_clause,[],[f840,f311,f280,f253,f660]) ).
fof(f1674,plain,
( e2 = e3
| ~ spl14_5
| ~ spl14_19 ),
inference(forward_demodulation,[],[f263,f325]) ).
fof(f1676,plain,
( ~ spl14_28
| spl14_7
| ~ spl14_16 ),
inference(avatar_split_clause,[],[f827,f311,f271,f366]) ).
fof(f1709,plain,
( $false
| spl14_1
| ~ spl14_19
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f1466,f247]) ).
fof(f1710,plain,
( spl14_1
| ~ spl14_19
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f1709]) ).
fof(f1712,plain,
( e0 = e3
| ~ spl14_36
| ~ spl14_48 ),
inference(forward_demodulation,[],[f407,f467]) ).
fof(f1714,plain,
( e1 = e3
| ~ spl14_60
| ~ spl14_75 ),
inference(forward_demodulation,[],[f530,f607]) ).
fof(f1716,plain,
( e2 = e3
| ~ spl14_70
| ~ spl14_77 ),
inference(forward_demodulation,[],[f582,f618]) ).
fof(f1721,plain,
( e2 = e3
| ~ spl14_76
| ~ spl14_96 ),
inference(forward_demodulation,[],[f728,f612]) ).
fof(f1737,plain,
( $false
| ~ spl14_5
| ~ spl14_19 ),
inference(forward_subsumption_resolution,[],[f1674,f150]) ).
fof(f1738,plain,
( ~ spl14_5
| ~ spl14_19 ),
inference(avatar_contradiction_clause,[],[f1737]) ).
fof(f1754,plain,
( $false
| ~ spl14_36
| ~ spl14_48 ),
inference(forward_subsumption_resolution,[],[f1712,f153]) ).
fof(f1755,plain,
( ~ spl14_36
| ~ spl14_48 ),
inference(avatar_contradiction_clause,[],[f1754]) ).
fof(f1756,plain,
( $false
| ~ spl14_60
| ~ spl14_75 ),
inference(forward_subsumption_resolution,[],[f1714,f151]) ).
fof(f1757,plain,
( ~ spl14_60
| ~ spl14_75 ),
inference(avatar_contradiction_clause,[],[f1756]) ).
fof(f1758,plain,
( $false
| ~ spl14_70
| ~ spl14_77 ),
inference(forward_subsumption_resolution,[],[f1716,f150]) ).
fof(f1759,plain,
( ~ spl14_70
| ~ spl14_77 ),
inference(avatar_contradiction_clause,[],[f1758]) ).
fof(f1760,plain,
( $false
| ~ spl14_76
| ~ spl14_96 ),
inference(forward_subsumption_resolution,[],[f1721,f150]) ).
fof(f1761,plain,
( ~ spl14_76
| ~ spl14_96 ),
inference(avatar_contradiction_clause,[],[f1760]) ).
fof(f1796,plain,
( e0 = e3
| ~ spl14_50
| ~ spl14_72 ),
inference(forward_demodulation,[],[f478,f592]) ).
fof(f1815,plain,
( $false
| ~ spl14_50
| ~ spl14_72 ),
inference(forward_subsumption_resolution,[],[f1796,f153]) ).
fof(f1816,plain,
( ~ spl14_50
| ~ spl14_72 ),
inference(avatar_contradiction_clause,[],[f1815]) ).
fof(f1818,plain,
( e1 = op(op(e2,e2),e0)
| ~ spl14_3
| ~ spl14_16 ),
inference(forward_demodulation,[],[f254,f312]) ).
fof(f1819,plain,
( e0 != op(e3,e1)
| spl14_6
| ~ spl14_19 ),
inference(forward_demodulation,[],[f268,f325]) ).
fof(f1820,plain,
( e1 = op(e2,e2)
| ~ spl14_7
| ~ spl14_16 ),
inference(forward_demodulation,[],[f272,f312]) ).
fof(f1822,plain,
( ~ spl14_44
| spl14_5
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f1159,f320,f262,f447]) ).
fof(f1823,plain,
( ~ spl14_35
| spl14_12
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f1163,f320,f293,f400]) ).
fof(f1834,plain,
( e0 = e1
| ~ spl14_49
| ~ spl14_82 ),
inference(forward_demodulation,[],[f662,f473]) ).
fof(f1850,plain,
( e0 != op(e0,e0)
| spl14_14
| ~ spl14_35 ),
inference(forward_demodulation,[],[f304,f401]) ).
fof(f1851,plain,
( e0 != op(op(e0,e0),e2)
| spl14_11
| ~ spl14_35 ),
inference(forward_demodulation,[],[f290,f401]) ).
fof(f1855,plain,
( op(e0,e0) = e1
| ~ spl14_3
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_demodulation,[],[f1818,f401]) ).
fof(f1858,plain,
( e0 = e1
| ~ spl14_7
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_demodulation,[],[f1820,f401]) ).
fof(f1862,plain,
( $false
| ~ spl14_49
| ~ spl14_82 ),
inference(forward_subsumption_resolution,[],[f1834,f155]) ).
fof(f1863,plain,
( ~ spl14_49
| ~ spl14_82 ),
inference(avatar_contradiction_clause,[],[f1862]) ).
fof(f1869,plain,
( e0 != op(e2,e2)
| spl14_11
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_demodulation,[],[f1851,f312]) ).
fof(f1871,plain,
( e1 = e2
| ~ spl14_3
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_demodulation,[],[f1855,f312]) ).
fof(f1872,plain,
( $false
| ~ spl14_7
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f1858,f155]) ).
fof(f1873,plain,
( ~ spl14_7
| ~ spl14_16
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f1872]) ).
fof(f1876,plain,
( $false
| spl14_11
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f1869,f401]) ).
fof(f1877,plain,
( spl14_11
| ~ spl14_16
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f1876]) ).
fof(f1879,plain,
( $false
| ~ spl14_3
| ~ spl14_16
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f1871,f152]) ).
fof(f1880,plain,
( ~ spl14_3
| ~ spl14_16
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f1879]) ).
fof(f1883,plain,
( e3 != op(e2,e2)
| ~ spl14_18
| spl14_19 ),
inference(forward_demodulation,[],[f326,f321]) ).
fof(f1894,plain,
( ~ spl14_89
| ~ spl14_16
| spl14_20
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f1389,f366,f329,f311,f692]) ).
fof(f1906,plain,
( e0 != op(op(e1,e1),e2)
| spl14_11
| ~ spl14_28 ),
inference(forward_demodulation,[],[f290,f367]) ).
fof(f1908,plain,
( e1 = op(e1,e0)
| ~ spl14_3
| ~ spl14_16
| ~ spl14_28 ),
inference(forward_demodulation,[],[f1818,f367]) ).
fof(f1921,plain,
( e0 = e1
| ~ spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_41 ),
inference(forward_demodulation,[],[f1908,f435]) ).
fof(f1927,plain,
( $false
| ~ spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_41 ),
inference(forward_subsumption_resolution,[],[f1921,f155]) ).
fof(f1928,plain,
( ~ spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_41 ),
inference(avatar_contradiction_clause,[],[f1927]) ).
fof(f1936,plain,
( e3 != op(op(e2,e2),e1)
| ~ spl14_18
| spl14_24 ),
inference(forward_demodulation,[],[f349,f321]) ).
fof(f1946,plain,
( e1 = e2
| ~ spl14_63
| ~ spl14_81 ),
inference(superposition,[],[f658,f545]) ).
fof(f1947,plain,
( e1 = e2
| ~ spl14_63
| ~ spl14_81 ),
inference(superposition,[],[f545,f658]) ).
fof(f1949,plain,
( $false
| ~ spl14_63
| ~ spl14_81 ),
inference(forward_subsumption_resolution,[],[f1947,f152]) ).
fof(f1950,plain,
( ~ spl14_63
| ~ spl14_81 ),
inference(avatar_contradiction_clause,[],[f1949]) ).
fof(f1951,plain,
( $false
| ~ spl14_63
| ~ spl14_81 ),
inference(forward_subsumption_resolution,[],[f1946,f152]) ).
fof(f1952,plain,
( ~ spl14_63
| ~ spl14_81 ),
inference(avatar_contradiction_clause,[],[f1951]) ).
fof(f1956,plain,
( e2 = e3
| ~ spl14_63
| ~ spl14_90 ),
inference(superposition,[],[f698,f545]) ).
fof(f1961,plain,
( $false
| ~ spl14_63
| ~ spl14_90 ),
inference(forward_subsumption_resolution,[],[f1956,f150]) ).
fof(f1962,plain,
( ~ spl14_63
| ~ spl14_90 ),
inference(avatar_contradiction_clause,[],[f1961]) ).
fof(f1965,plain,
( e0 = e3
| ~ spl14_75
| ~ spl14_92 ),
inference(superposition,[],[f707,f607]) ).
fof(f1966,plain,
( e0 = e3
| ~ spl14_75
| ~ spl14_92 ),
inference(superposition,[],[f607,f707]) ).
fof(f1968,plain,
( $false
| ~ spl14_75
| ~ spl14_92 ),
inference(forward_subsumption_resolution,[],[f1966,f153]) ).
fof(f1969,plain,
( ~ spl14_75
| ~ spl14_92 ),
inference(avatar_contradiction_clause,[],[f1968]) ).
fof(f1970,plain,
( $false
| ~ spl14_75
| ~ spl14_92 ),
inference(forward_subsumption_resolution,[],[f1965,f153]) ).
fof(f1971,plain,
( ~ spl14_75
| ~ spl14_92 ),
inference(avatar_contradiction_clause,[],[f1970]) ).
fof(f1973,plain,
( e0 = e3
| ~ spl14_76
| ~ spl14_94 ),
inference(superposition,[],[f716,f612]) ).
fof(f1977,plain,
( $false
| ~ spl14_76
| ~ spl14_94 ),
inference(forward_subsumption_resolution,[],[f1973,f153]) ).
fof(f1978,plain,
( ~ spl14_76
| ~ spl14_94 ),
inference(avatar_contradiction_clause,[],[f1977]) ).
fof(f1980,plain,
( e0 = op(e2,e2)
| ~ spl14_12
| ~ spl14_18 ),
inference(forward_demodulation,[],[f294,f321]) ).
fof(f2008,plain,
( e3 != op(e0,e1)
| ~ spl14_18
| spl14_24
| ~ spl14_35 ),
inference(forward_demodulation,[],[f1936,f401]) ).
fof(f2019,plain,
( e0 = e1
| ~ spl14_99
| ~ spl14_101 ),
inference(forward_demodulation,[],[f753,f743]) ).
fof(f2024,plain,
( e2 != op(e1,e1)
| spl14_5
| ~ spl14_40 ),
inference(forward_demodulation,[],[f264,f429]) ).
fof(f2026,plain,
( e0 = op(e1,e1)
| ~ spl14_12
| ~ spl14_40 ),
inference(forward_demodulation,[],[f294,f429]) ).
fof(f2027,plain,
( $false
| ~ spl14_99
| ~ spl14_101 ),
inference(forward_subsumption_resolution,[],[f2019,f155]) ).
fof(f2028,plain,
( ~ spl14_99
| ~ spl14_101 ),
inference(avatar_contradiction_clause,[],[f2027]) ).
fof(f2030,plain,
( spl14_34
| ~ spl14_12
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f2026,f428,f293,f395]) ).
fof(f2033,plain,
( e0 = e2
| ~ spl14_92
| ~ spl14_95 ),
inference(forward_demodulation,[],[f707,f723]) ).
fof(f2035,plain,
( e1 = e3
| ~ spl14_77
| ~ spl14_101 ),
inference(forward_demodulation,[],[f753,f618]) ).
fof(f2037,plain,
( $false
| ~ spl14_92
| ~ spl14_95 ),
inference(forward_subsumption_resolution,[],[f2033,f154]) ).
fof(f2038,plain,
( ~ spl14_92
| ~ spl14_95 ),
inference(avatar_contradiction_clause,[],[f2037]) ).
fof(f2039,plain,
( $false
| ~ spl14_77
| ~ spl14_101 ),
inference(forward_subsumption_resolution,[],[f2035,f151]) ).
fof(f2040,plain,
( ~ spl14_77
| ~ spl14_101 ),
inference(avatar_contradiction_clause,[],[f2039]) ).
fof(f2043,plain,
( e0 = e3
| ~ spl14_77
| ~ spl14_99 ),
inference(forward_demodulation,[],[f743,f618]) ).
fof(f2046,plain,
( $false
| ~ spl14_77
| ~ spl14_99 ),
inference(forward_subsumption_resolution,[],[f2043,f153]) ).
fof(f2047,plain,
( ~ spl14_77
| ~ spl14_99 ),
inference(avatar_contradiction_clause,[],[f2046]) ).
fof(f2049,plain,
( ~ spl14_30
| ~ spl14_9
| spl14_10 ),
inference(avatar_split_clause,[],[f828,f284,f280,f376]) ).
fof(f2050,plain,
( ~ spl14_36
| ~ spl14_9
| spl14_14 ),
inference(avatar_split_clause,[],[f1021,f302,f280,f406]) ).
fof(f2059,plain,
( e0 = e1
| ~ spl14_59
| ~ spl14_94 ),
inference(forward_demodulation,[],[f525,f716]) ).
fof(f2084,plain,
( $false
| ~ spl14_59
| ~ spl14_94 ),
inference(forward_subsumption_resolution,[],[f2059,f155]) ).
fof(f2085,plain,
( ~ spl14_59
| ~ spl14_94 ),
inference(avatar_contradiction_clause,[],[f2084]) ).
fof(f2095,plain,
( e1 = e2
| ~ spl14_59
| ~ spl14_96 ),
inference(forward_demodulation,[],[f525,f728]) ).
fof(f2103,plain,
( $false
| ~ spl14_59
| ~ spl14_96 ),
inference(forward_subsumption_resolution,[],[f2095,f152]) ).
fof(f2104,plain,
( ~ spl14_59
| ~ spl14_96 ),
inference(avatar_contradiction_clause,[],[f2103]) ).
fof(f2112,plain,
( $false
| ~ spl14_9
| ~ spl14_18
| spl14_19 ),
inference(forward_subsumption_resolution,[],[f1883,f281]) ).
fof(f2113,plain,
( ~ spl14_9
| ~ spl14_18
| spl14_19 ),
inference(avatar_contradiction_clause,[],[f2112]) ).
fof(f2191,plain,
( e0 = e3
| ~ spl14_49
| ~ spl14_73 ),
inference(superposition,[],[f597,f473]) ).
fof(f2195,plain,
( $false
| ~ spl14_49
| ~ spl14_73 ),
inference(forward_subsumption_resolution,[],[f2191,f153]) ).
fof(f2196,plain,
( ~ spl14_49
| ~ spl14_73 ),
inference(avatar_contradiction_clause,[],[f2195]) ).
fof(f2207,plain,
( e1 = e3
| ~ spl14_52
| ~ spl14_87 ),
inference(superposition,[],[f685,f488]) ).
fof(f2208,plain,
( e1 = e3
| ~ spl14_52
| ~ spl14_87 ),
inference(superposition,[],[f488,f685]) ).
fof(f2209,plain,
( $false
| ~ spl14_52
| ~ spl14_87 ),
inference(forward_subsumption_resolution,[],[f2208,f151]) ).
fof(f2210,plain,
( ~ spl14_52
| ~ spl14_87 ),
inference(avatar_contradiction_clause,[],[f2209]) ).
fof(f2211,plain,
( $false
| ~ spl14_52
| ~ spl14_87 ),
inference(forward_subsumption_resolution,[],[f2207,f151]) ).
fof(f2212,plain,
( ~ spl14_52
| ~ spl14_87 ),
inference(avatar_contradiction_clause,[],[f2211]) ).
fof(f2223,plain,
( e0 = e1
| ~ spl14_57
| ~ spl14_91 ),
inference(superposition,[],[f703,f515]) ).
fof(f2227,plain,
( $false
| ~ spl14_57
| ~ spl14_91 ),
inference(forward_subsumption_resolution,[],[f2223,f155]) ).
fof(f2228,plain,
( ~ spl14_57
| ~ spl14_91 ),
inference(avatar_contradiction_clause,[],[f2227]) ).
fof(f2231,plain,
( e0 = e1
| ~ spl14_56
| ~ spl14_93 ),
inference(superposition,[],[f712,f510]) ).
fof(f2232,plain,
( e0 = e1
| ~ spl14_56
| ~ spl14_93 ),
inference(superposition,[],[f510,f712]) ).
fof(f2233,plain,
( $false
| ~ spl14_56
| ~ spl14_93 ),
inference(forward_subsumption_resolution,[],[f2232,f155]) ).
fof(f2234,plain,
( ~ spl14_56
| ~ spl14_93 ),
inference(avatar_contradiction_clause,[],[f2233]) ).
fof(f2235,plain,
( $false
| ~ spl14_56
| ~ spl14_93 ),
inference(forward_subsumption_resolution,[],[f2231,f155]) ).
fof(f2236,plain,
( ~ spl14_56
| ~ spl14_93 ),
inference(avatar_contradiction_clause,[],[f2235]) ).
fof(f2242,plain,
( e0 = e3
| ~ spl14_9
| ~ spl14_35 ),
inference(forward_demodulation,[],[f401,f281]) ).
fof(f2243,plain,
( ~ spl14_27
| spl14_10
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f969,f400,f284,f361]) ).
fof(f2245,plain,
( ~ spl14_79
| ~ spl14_9
| spl14_15
| ~ spl14_36 ),
inference(avatar_split_clause,[],[f807,f406,f306,f280,f647]) ).
fof(f2252,plain,
( e2 = e3
| ~ spl14_75
| ~ spl14_95 ),
inference(forward_demodulation,[],[f723,f607]) ).
fof(f2253,plain,
( e0 = e1
| ~ spl14_100
| ~ spl14_102 ),
inference(forward_demodulation,[],[f758,f748]) ).
fof(f2274,plain,
( e0 != op(e0,e0)
| spl14_12
| ~ spl14_34 ),
inference(forward_demodulation,[],[f295,f396]) ).
fof(f2281,plain,
( $false
| ~ spl14_9
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f2242,f153]) ).
fof(f2282,plain,
( ~ spl14_9
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f2281]) ).
fof(f2283,plain,
( $false
| ~ spl14_75
| ~ spl14_95 ),
inference(forward_subsumption_resolution,[],[f2252,f150]) ).
fof(f2284,plain,
( ~ spl14_75
| ~ spl14_95 ),
inference(avatar_contradiction_clause,[],[f2283]) ).
fof(f2285,plain,
( $false
| ~ spl14_100
| ~ spl14_102 ),
inference(forward_subsumption_resolution,[],[f2253,f155]) ).
fof(f2286,plain,
( ~ spl14_100
| ~ spl14_102 ),
inference(avatar_contradiction_clause,[],[f2285]) ).
fof(f2292,plain,
( $false
| spl14_12
| ~ spl14_34
| ~ spl14_38 ),
inference(forward_subsumption_resolution,[],[f2274,f418]) ).
fof(f2293,plain,
( spl14_12
| ~ spl14_34
| ~ spl14_38 ),
inference(avatar_contradiction_clause,[],[f2292]) ).
fof(f2304,plain,
( spl14_30
| ~ spl14_9
| ~ spl14_10 ),
inference(avatar_split_clause,[],[f1032,f284,f280,f376]) ).
fof(f2305,plain,
( e0 = op(e0,e0)
| ~ spl14_12
| ~ spl14_34 ),
inference(forward_demodulation,[],[f294,f396]) ).
fof(f2313,plain,
( e1 = e2
| ~ spl14_62
| ~ spl14_79 ),
inference(forward_demodulation,[],[f649,f540]) ).
fof(f2338,plain,
( $false
| ~ spl14_1
| spl14_19
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f1218,f246]) ).
fof(f2339,plain,
( ~ spl14_1
| spl14_19
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f2338]) ).
fof(f2345,plain,
( $false
| ~ spl14_62
| ~ spl14_79 ),
inference(forward_subsumption_resolution,[],[f2313,f152]) ).
fof(f2346,plain,
( ~ spl14_62
| ~ spl14_79 ),
inference(avatar_contradiction_clause,[],[f2345]) ).
fof(f2355,plain,
( ~ spl14_21
| ~ spl14_4
| spl14_5 ),
inference(avatar_split_clause,[],[f825,f262,f258,f334]) ).
fof(f2377,plain,
( e0 = e1
| ~ spl14_27
| ~ spl14_38 ),
inference(forward_demodulation,[],[f362,f418]) ).
fof(f2381,plain,
( e1 = e3
| ~ spl14_9
| ~ spl14_28 ),
inference(forward_demodulation,[],[f367,f281]) ).
fof(f2394,plain,
( e0 != op(e3,e2)
| ~ spl14_4
| spl14_11
| ~ spl14_28 ),
inference(forward_demodulation,[],[f1906,f259]) ).
fof(f2477,plain,
( $false
| ~ spl14_27
| ~ spl14_38 ),
inference(forward_subsumption_resolution,[],[f2377,f155]) ).
fof(f2478,plain,
( ~ spl14_27
| ~ spl14_38 ),
inference(avatar_contradiction_clause,[],[f2477]) ).
fof(f2481,plain,
( $false
| ~ spl14_9
| ~ spl14_28 ),
inference(forward_subsumption_resolution,[],[f2381,f151]) ).
fof(f2482,plain,
( ~ spl14_9
| ~ spl14_28 ),
inference(avatar_contradiction_clause,[],[f2481]) ).
fof(f2493,plain,
( $false
| ~ spl14_4
| spl14_11
| ~ spl14_28
| ~ spl14_100 ),
inference(forward_subsumption_resolution,[],[f2394,f748]) ).
fof(f2494,plain,
( ~ spl14_4
| spl14_11
| ~ spl14_28
| ~ spl14_100 ),
inference(avatar_contradiction_clause,[],[f2493]) ).
fof(f2520,plain,
( e2 = e3
| ~ spl14_9
| ~ spl14_44 ),
inference(forward_demodulation,[],[f448,f281]) ).
fof(f2549,plain,
( $false
| ~ spl14_9
| ~ spl14_44 ),
inference(forward_subsumption_resolution,[],[f2520,f150]) ).
fof(f2550,plain,
( ~ spl14_9
| ~ spl14_44 ),
inference(avatar_contradiction_clause,[],[f2549]) ).
fof(f2609,plain,
( e1 = e2
| ~ spl14_28
| ~ spl14_44 ),
inference(superposition,[],[f448,f367]) ).
fof(f2614,plain,
( $false
| ~ spl14_28
| ~ spl14_44 ),
inference(forward_subsumption_resolution,[],[f2609,f152]) ).
fof(f2615,plain,
( ~ spl14_28
| ~ spl14_44 ),
inference(avatar_contradiction_clause,[],[f2614]) ).
fof(f2627,plain,
( e0 = e3
| ~ spl14_1
| ~ spl14_38 ),
inference(forward_demodulation,[],[f418,f246]) ).
fof(f2650,plain,
( $false
| ~ spl14_1
| ~ spl14_38 ),
inference(forward_subsumption_resolution,[],[f2627,f153]) ).
fof(f2651,plain,
( ~ spl14_1
| ~ spl14_38 ),
inference(avatar_contradiction_clause,[],[f2650]) ).
fof(f2664,plain,
( spl14_40
| ~ spl14_10
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f1074,f366,f284,f428]) ).
fof(f2667,plain,
( e1 = e3
| ~ spl14_1
| ~ spl14_27 ),
inference(forward_demodulation,[],[f362,f246]) ).
fof(f2669,plain,
( e1 = e2
| ~ spl14_21
| ~ spl14_30 ),
inference(forward_demodulation,[],[f377,f335]) ).
fof(f2694,plain,
( e2 = op(e1,e1)
| ~ spl14_5
| ~ spl14_40 ),
inference(forward_demodulation,[],[f263,f429]) ).
fof(f2704,plain,
( $false
| ~ spl14_1
| ~ spl14_27 ),
inference(forward_subsumption_resolution,[],[f2667,f151]) ).
fof(f2705,plain,
( ~ spl14_1
| ~ spl14_27 ),
inference(avatar_contradiction_clause,[],[f2704]) ).
fof(f2706,plain,
( $false
| ~ spl14_21
| ~ spl14_30 ),
inference(forward_subsumption_resolution,[],[f2669,f152]) ).
fof(f2707,plain,
( ~ spl14_21
| ~ spl14_30 ),
inference(avatar_contradiction_clause,[],[f2706]) ).
fof(f2720,plain,
( $false
| ~ spl14_5
| spl14_18
| ~ spl14_40 ),
inference(forward_subsumption_resolution,[],[f2694,f322]) ).
fof(f2721,plain,
( ~ spl14_5
| spl14_18
| ~ spl14_40 ),
inference(avatar_contradiction_clause,[],[f2720]) ).
fof(f2732,plain,
( e0 = e2
| ~ spl14_21
| ~ spl14_36 ),
inference(forward_demodulation,[],[f407,f335]) ).
fof(f2733,plain,
( e1 = e3
| ~ spl14_78
| ~ spl14_102 ),
inference(forward_demodulation,[],[f758,f623]) ).
fof(f2739,plain,
( $false
| ~ spl14_21
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f2732,f154]) ).
fof(f2740,plain,
( ~ spl14_21
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f2739]) ).
fof(f2741,plain,
( $false
| ~ spl14_78
| ~ spl14_102 ),
inference(forward_subsumption_resolution,[],[f2733,f151]) ).
fof(f2742,plain,
( ~ spl14_78
| ~ spl14_102 ),
inference(avatar_contradiction_clause,[],[f2741]) ).
fof(f2760,plain,
( e0 = e1
| ~ spl14_30
| ~ spl14_36 ),
inference(superposition,[],[f407,f377]) ).
fof(f2765,plain,
( $false
| ~ spl14_30
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f2760,f155]) ).
fof(f2766,plain,
( ~ spl14_30
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f2765]) ).
fof(f2776,plain,
( e1 = op(e2,e2)
| ~ spl14_10
| ~ spl14_44 ),
inference(forward_demodulation,[],[f285,f448]) ).
fof(f2778,plain,
( e0 = op(op(e2,e2),e2)
| ~ spl14_11
| ~ spl14_44 ),
inference(forward_demodulation,[],[f289,f448]) ).
fof(f2781,plain,
( $false
| ~ spl14_10
| spl14_28
| ~ spl14_44 ),
inference(forward_subsumption_resolution,[],[f2776,f368]) ).
fof(f2782,plain,
( ~ spl14_10
| spl14_28
| ~ spl14_44 ),
inference(avatar_contradiction_clause,[],[f2781]) ).
fof(f2783,plain,
( e0 = op(e2,e2)
| ~ spl14_11
| ~ spl14_44 ),
inference(forward_demodulation,[],[f2778,f448]) ).
fof(f2786,plain,
( e0 = e2
| ~ spl14_11
| ~ spl14_44 ),
inference(forward_demodulation,[],[f2783,f448]) ).
fof(f2787,plain,
( $false
| ~ spl14_11
| ~ spl14_44 ),
inference(forward_subsumption_resolution,[],[f2786,f154]) ).
fof(f2788,plain,
( ~ spl14_11
| ~ spl14_44 ),
inference(avatar_contradiction_clause,[],[f2787]) ).
fof(f2803,plain,
( e2 = e3
| ~ spl14_62
| ~ spl14_88 ),
inference(superposition,[],[f689,f540]) ).
fof(f2804,plain,
( e2 = e3
| ~ spl14_62
| ~ spl14_88 ),
inference(superposition,[],[f540,f689]) ).
fof(f2806,plain,
( $false
| ~ spl14_62
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f2804,f150]) ).
fof(f2807,plain,
( ~ spl14_62
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f2806]) ).
fof(f2808,plain,
( $false
| ~ spl14_62
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f2803,f150]) ).
fof(f2809,plain,
( ~ spl14_62
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f2808]) ).
fof(f2816,plain,
( e0 = e3
| ~ spl14_91
| ~ spl14_97 ),
inference(superposition,[],[f733,f703]) ).
fof(f2817,plain,
( e0 = e3
| ~ spl14_91
| ~ spl14_97 ),
inference(superposition,[],[f703,f733]) ).
fof(f2820,plain,
( $false
| ~ spl14_91
| ~ spl14_97 ),
inference(forward_subsumption_resolution,[],[f2817,f153]) ).
fof(f2821,plain,
( ~ spl14_91
| ~ spl14_97 ),
inference(avatar_contradiction_clause,[],[f2820]) ).
fof(f2822,plain,
( $false
| ~ spl14_91
| ~ spl14_97 ),
inference(forward_subsumption_resolution,[],[f2816,f153]) ).
fof(f2823,plain,
( ~ spl14_91
| ~ spl14_97 ),
inference(avatar_contradiction_clause,[],[f2822]) ).
fof(f2824,plain,
( spl14_38
| ~ spl14_12
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f2305,f395,f293,f417]) ).
fof(f2825,plain,
( ~ spl14_38
| spl14_14
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f1850,f400,f302,f417]) ).
fof(f2828,plain,
( e1 = e3
| ~ spl14_57
| ~ spl14_97 ),
inference(forward_demodulation,[],[f515,f733]) ).
fof(f2841,plain,
( op(e0,e0) != e3
| spl14_29
| ~ spl14_35 ),
inference(forward_demodulation,[],[f372,f401]) ).
fof(f2852,plain,
( $false
| ~ spl14_57
| ~ spl14_97 ),
inference(forward_subsumption_resolution,[],[f2828,f151]) ).
fof(f2853,plain,
( ~ spl14_57
| ~ spl14_97 ),
inference(avatar_contradiction_clause,[],[f2852]) ).
fof(f2859,plain,
( ~ spl14_96
| ~ spl14_1
| spl14_13
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f1441,f395,f297,f245,f726]) ).
fof(f2871,plain,
( ~ spl14_94
| spl14_6
| ~ spl14_19 ),
inference(avatar_split_clause,[],[f1819,f324,f266,f714]) ).
fof(f2901,plain,
( $false
| ~ spl14_1
| spl14_29
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f2841,f246]) ).
fof(f2902,plain,
( ~ spl14_1
| spl14_29
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f2901]) ).
fof(f2912,plain,
( e0 = e2
| ~ spl14_35
| ~ spl14_44 ),
inference(superposition,[],[f448,f401]) ).
fof(f2918,plain,
( $false
| ~ spl14_35
| ~ spl14_44 ),
inference(forward_subsumption_resolution,[],[f2912,f154]) ).
fof(f2919,plain,
( ~ spl14_35
| ~ spl14_44 ),
inference(avatar_contradiction_clause,[],[f2918]) ).
fof(f2922,plain,
( e0 = e3
| ~ spl14_93
| ~ spl14_98 ),
inference(forward_demodulation,[],[f712,f738]) ).
fof(f2944,plain,
( $false
| ~ spl14_93
| ~ spl14_98 ),
inference(forward_subsumption_resolution,[],[f2922,f153]) ).
fof(f2945,plain,
( ~ spl14_93
| ~ spl14_98 ),
inference(avatar_contradiction_clause,[],[f2944]) ).
fof(f2975,plain,
( e1 = e3
| ~ spl14_79
| ~ spl14_88 ),
inference(superposition,[],[f689,f649]) ).
fof(f2976,plain,
( e1 = e3
| ~ spl14_79
| ~ spl14_88 ),
inference(superposition,[],[f649,f689]) ).
fof(f2979,plain,
( $false
| ~ spl14_79
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f2976,f151]) ).
fof(f2980,plain,
( ~ spl14_79
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f2979]) ).
fof(f2981,plain,
( $false
| ~ spl14_79
| ~ spl14_88 ),
inference(forward_subsumption_resolution,[],[f2975,f151]) ).
fof(f2982,plain,
( ~ spl14_79
| ~ spl14_88 ),
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f3014,plain,
( e0 != op(op(e3,e3),e2)
| ~ spl14_9
| spl14_11 ),
inference(forward_demodulation,[],[f290,f281]) ).
fof(f3027,plain,
( e0 != op(e1,e2)
| ~ spl14_9
| spl14_11
| ~ spl14_30 ),
inference(forward_demodulation,[],[f3014,f377]) ).
fof(f3031,plain,
( $false
| ~ spl14_9
| spl14_11
| ~ spl14_30
| ~ spl14_91 ),
inference(forward_subsumption_resolution,[],[f3027,f703]) ).
fof(f3032,plain,
( ~ spl14_9
| spl14_11
| ~ spl14_30
| ~ spl14_91 ),
inference(avatar_contradiction_clause,[],[f3031]) ).
fof(f3035,plain,
( spl14_16
| ~ spl14_5
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f1515,f395,f262,f311]) ).
fof(f3042,plain,
( e3 != op(e2,e1)
| ~ spl14_16
| spl14_24
| ~ spl14_34 ),
inference(forward_demodulation,[],[f1526,f312]) ).
fof(f3064,plain,
( e3 != op(e2,e1)
| ~ spl14_5
| spl14_24 ),
inference(forward_demodulation,[],[f349,f263]) ).
fof(f3065,plain,
( e0 != op(e2,e1)
| ~ spl14_5
| spl14_6 ),
inference(forward_demodulation,[],[f268,f263]) ).
fof(f3073,plain,
( $false
| ~ spl14_16
| spl14_24
| ~ spl14_34
| ~ spl14_98 ),
inference(forward_subsumption_resolution,[],[f3042,f738]) ).
fof(f3074,plain,
( ~ spl14_16
| spl14_24
| ~ spl14_34
| ~ spl14_98 ),
inference(avatar_contradiction_clause,[],[f3073]) ).
fof(f3153,plain,
( e2 != op(e2,e3)
| ~ spl14_44 ),
inference(superposition,[],[f108,f448]) ).
fof(f3161,plain,
( e1 != op(e1,e3)
| ~ spl14_57 ),
inference(superposition,[],[f114,f515]) ).
fof(f3162,plain,
( e2 != op(e1,e3)
| ~ spl14_18 ),
inference(superposition,[],[f115,f321]) ).
fof(f3165,plain,
( e0 != op(e1,e3)
| ~ spl14_41 ),
inference(superposition,[],[f117,f435]) ).
fof(f3168,plain,
( e2 != op(e1,e0)
| ~ spl14_18 ),
inference(superposition,[],[f119,f321]) ).
fof(f3183,plain,
( e3 != op(e2,e3)
| ~ spl14_75 ),
inference(superposition,[],[f128,f607]) ).
fof(f3194,plain,
( e1 != op(e0,e2)
| ~ spl14_57 ),
inference(superposition,[],[f137,f515]) ).
fof(f3197,plain,
( e2 != op(e3,e1)
| ~ spl14_18 ),
inference(superposition,[],[f139,f321]) ).
fof(f3203,plain,
( e2 != op(e0,e1)
| ~ spl14_18 ),
inference(superposition,[],[f143,f321]) ).
fof(f3206,plain,
( e0 != op(e3,e0)
| ~ spl14_41 ),
inference(superposition,[],[f145,f435]) ).
fof(f3208,plain,
( e0 != op(e2,e0)
| ~ spl14_41 ),
inference(superposition,[],[f146,f435]) ).
fof(f3213,plain,
( e0 != op(e0,e0)
| ~ spl14_41 ),
inference(superposition,[],[f149,f435]) ).
fof(f3215,plain,
( e2 != op(e1,e1)
| spl14_2
| ~ spl14_27 ),
inference(superposition,[],[f251,f362]) ).
fof(f3216,plain,
( $false
| spl14_2
| ~ spl14_18
| ~ spl14_27 ),
inference(forward_subsumption_resolution,[],[f3215,f321]) ).
fof(f3217,plain,
( spl14_2
| ~ spl14_18
| ~ spl14_27 ),
inference(avatar_contradiction_clause,[],[f3216]) ).
fof(f3221,plain,
( ~ spl14_90
| ~ spl14_18
| spl14_20
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1166,f361,f329,f320,f696]) ).
fof(f3235,plain,
( $false
| ~ spl14_41
| ~ spl14_45 ),
inference(forward_subsumption_resolution,[],[f3208,f454]) ).
fof(f3236,plain,
( ~ spl14_41
| ~ spl14_45 ),
inference(avatar_contradiction_clause,[],[f3235]) ).
fof(f3245,plain,
( ~ spl14_98
| ~ spl14_5
| spl14_24 ),
inference(avatar_split_clause,[],[f3064,f347,f262,f736]) ).
fof(f3248,plain,
( ~ spl14_77
| ~ spl14_75 ),
inference(avatar_split_clause,[],[f3183,f605,f616]) ).
fof(f3260,plain,
( $false
| ~ spl14_38
| ~ spl14_41 ),
inference(forward_subsumption_resolution,[],[f3213,f418]) ).
fof(f3261,plain,
( ~ spl14_38
| ~ spl14_41 ),
inference(avatar_contradiction_clause,[],[f3260]) ).
fof(f3262,plain,
( op(e0,e0) = e2
| ~ spl14_2
| ~ spl14_38 ),
inference(forward_demodulation,[],[f250,f418]) ).
fof(f3269,plain,
( $false
| ~ spl14_2
| spl14_16
| ~ spl14_38 ),
inference(forward_subsumption_resolution,[],[f3262,f313]) ).
fof(f3270,plain,
( ~ spl14_2
| spl14_16
| ~ spl14_38 ),
inference(avatar_contradiction_clause,[],[f3269]) ).
fof(f3281,plain,
( ~ spl14_18
| spl14_5
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f2024,f428,f262,f320]) ).
fof(f3310,plain,
( e0 = e2
| ~ spl14_49
| ~ spl14_86 ),
inference(forward_demodulation,[],[f473,f680]) ).
fof(f3340,plain,
( $false
| ~ spl14_49
| ~ spl14_86 ),
inference(forward_subsumption_resolution,[],[f3310,f154]) ).
fof(f3341,plain,
( ~ spl14_49
| ~ spl14_86 ),
inference(avatar_contradiction_clause,[],[f3340]) ).
fof(f3358,plain,
( $false
| ~ spl14_5
| spl14_6
| ~ spl14_93 ),
inference(forward_subsumption_resolution,[],[f3065,f712]) ).
fof(f3359,plain,
( ~ spl14_5
| spl14_6
| ~ spl14_93 ),
inference(avatar_contradiction_clause,[],[f3358]) ).
fof(f3367,plain,
( ~ spl14_70
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f3153,f447,f580]) ).
fof(f3415,plain,
( spl14_35
| ~ spl14_12
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f1980,f320,f293,f400]) ).
fof(f3418,plain,
( ~ spl14_87
| ~ spl14_18
| spl14_24
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f2008,f400,f347,f320,f683]) ).
fof(f3419,plain,
( ~ spl14_83
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f3203,f320,f665]) ).
fof(f3420,plain,
( ~ spl14_95
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f3162,f320,f721]) ).
fof(f3421,plain,
( ~ spl14_85
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f3168,f320,f674]) ).
fof(f3422,plain,
( ~ spl14_96
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f3197,f320,f726]) ).
fof(f3430,plain,
( ~ spl14_92
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f3165,f433,f705]) ).
fof(f3432,plain,
( ~ spl14_49
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f3206,f433,f471]) ).
fof(f3436,plain,
( ~ spl14_79
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f3194,f513,f647]) ).
fof(f3437,plain,
( ~ spl14_60
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f3161,f513,f528]) ).
fof(f3502,plain,
( e1 != op(e1,e2)
| ~ spl14_40 ),
inference(superposition,[],[f116,f429]) ).
fof(f3506,plain,
( e1 != op(e0,e1)
| ~ spl14_40 ),
inference(superposition,[],[f143,f429]) ).
fof(f3509,plain,
( $false
| ~ spl14_40
| ~ spl14_52 ),
inference(forward_subsumption_resolution,[],[f3506,f488]) ).
fof(f3510,plain,
( ~ spl14_40
| ~ spl14_52 ),
inference(avatar_contradiction_clause,[],[f3509]) ).
fof(f3512,plain,
( $false
| ~ spl14_40
| ~ spl14_57 ),
inference(forward_subsumption_resolution,[],[f3502,f515]) ).
fof(f3513,plain,
( ~ spl14_40
| ~ spl14_57 ),
inference(avatar_contradiction_clause,[],[f3512]) ).
cnf(s2,plain,
( ~ spl14_4
| ~ spl14_5
| ~ spl14_6 ),
inference(sat_conversion,[],[f269]) ).
cnf(s4,plain,
( ~ spl14_9
| ~ spl14_10
| ~ spl14_11 ),
inference(sat_conversion,[],[f291]) ).
cnf(s6,plain,
( ~ spl14_9
| ~ spl14_14
| ~ spl14_15 ),
inference(sat_conversion,[],[f309]) ).
cnf(s7,plain,
( ~ spl14_3
| ~ spl14_16
| ~ spl14_17 ),
inference(sat_conversion,[],[f318]) ).
cnf(s8,plain,
( ~ spl14_6
| ~ spl14_18
| ~ spl14_19 ),
inference(sat_conversion,[],[f327]) ).
cnf(s9,plain,
( ~ spl14_7
| ~ spl14_16
| ~ spl14_20 ),
inference(sat_conversion,[],[f332]) ).
cnf(s11,plain,
( ~ spl14_12
| ~ spl14_18
| ~ spl14_24 ),
inference(sat_conversion,[],[f350]) ).
cnf(s14,plain,
( ~ spl14_11
| ~ spl14_28
| ~ spl14_29 ),
inference(sat_conversion,[],[f373]) ).
cnf(s15,plain,
( ~ spl14_2
| ~ spl14_20
| ~ spl14_27 ),
inference(sat_conversion,[],[f374]) ).
cnf(s17,plain,
( ~ spl14_14
| ~ spl14_28
| ~ spl14_32 ),
inference(sat_conversion,[],[f388]) ).
cnf(s19,plain,
( ~ spl14_13
| ~ spl14_19
| ~ spl14_34 ),
inference(sat_conversion,[],[f398]) ).
cnf(s21,plain,
( ~ spl14_5
| ~ spl14_24
| ~ spl14_34 ),
inference(sat_conversion,[],[f404]) ).
cnf(s23,plain,
( ~ spl14_10
| ~ spl14_32
| ~ spl14_35 ),
inference(sat_conversion,[],[f410]) ).
cnf(s25,plain,
( ~ spl14_37
| ~ spl14_38 ),
inference(sat_conversion,[],[f420]) ).
cnf(s27,plain,
( ~ spl14_37
| spl14_38 ),
inference(sat_conversion,[],[f422]) ).
cnf(s28,plain,
( ~ spl14_39
| ~ spl14_40 ),
inference(sat_conversion,[],[f431]) ).
cnf(s29,plain,
( ~ spl14_39
| spl14_41 ),
inference(sat_conversion,[],[f436]) ).
cnf(s30,plain,
( ~ spl14_39
| spl14_42 ),
inference(sat_conversion,[],[f441]) ).
cnf(s31,plain,
( ~ spl14_43
| ~ spl14_44 ),
inference(sat_conversion,[],[f450]) ).
cnf(s32,plain,
( ~ spl14_43
| spl14_45 ),
inference(sat_conversion,[],[f455]) ).
cnf(s33,plain,
( ~ spl14_43
| spl14_46 ),
inference(sat_conversion,[],[f460]) ).
cnf(s34,plain,
( ~ spl14_47
| ~ spl14_48 ),
inference(sat_conversion,[],[f469]) ).
cnf(s35,plain,
( ~ spl14_47
| spl14_49 ),
inference(sat_conversion,[],[f474]) ).
cnf(s36,plain,
( ~ spl14_47
| spl14_50 ),
inference(sat_conversion,[],[f479]) ).
cnf(s37,plain,
( ~ spl14_38
| ~ spl14_51 ),
inference(sat_conversion,[],[f484]) ).
cnf(s38,plain,
( ~ spl14_51
| spl14_52 ),
inference(sat_conversion,[],[f489]) ).
cnf(s39,plain,
( ~ spl14_51
| spl14_53 ),
inference(sat_conversion,[],[f494]) ).
cnf(s40,plain,
( ~ spl14_40
| ~ spl14_54 ),
inference(sat_conversion,[],[f499]) ).
cnf(s42,plain,
( spl14_40
| ~ spl14_54 ),
inference(sat_conversion,[],[f501]) ).
cnf(s43,plain,
( ~ spl14_44
| ~ spl14_55 ),
inference(sat_conversion,[],[f506]) ).
cnf(s44,plain,
( ~ spl14_55
| spl14_56 ),
inference(sat_conversion,[],[f511]) ).
cnf(s45,plain,
( ~ spl14_55
| spl14_57 ),
inference(sat_conversion,[],[f516]) ).
cnf(s46,plain,
( ~ spl14_48
| ~ spl14_58 ),
inference(sat_conversion,[],[f521]) ).
cnf(s47,plain,
( ~ spl14_58
| spl14_59 ),
inference(sat_conversion,[],[f526]) ).
cnf(s48,plain,
( ~ spl14_58
| spl14_60 ),
inference(sat_conversion,[],[f531]) ).
cnf(s49,plain,
( ~ spl14_38
| ~ spl14_61 ),
inference(sat_conversion,[],[f536]) ).
cnf(s50,plain,
( ~ spl14_61
| spl14_62 ),
inference(sat_conversion,[],[f541]) ).
cnf(s51,plain,
( ~ spl14_61
| spl14_63 ),
inference(sat_conversion,[],[f546]) ).
cnf(s52,plain,
( ~ spl14_40
| ~ spl14_64 ),
inference(sat_conversion,[],[f551]) ).
cnf(s53,plain,
( ~ spl14_64
| spl14_65 ),
inference(sat_conversion,[],[f556]) ).
cnf(s54,plain,
( ~ spl14_64
| spl14_66 ),
inference(sat_conversion,[],[f561]) ).
cnf(s55,plain,
( ~ spl14_44
| ~ spl14_67 ),
inference(sat_conversion,[],[f566]) ).
cnf(s57,plain,
( spl14_44
| ~ spl14_67 ),
inference(sat_conversion,[],[f568]) ).
cnf(s58,plain,
( ~ spl14_48
| ~ spl14_68 ),
inference(sat_conversion,[],[f573]) ).
cnf(s59,plain,
( ~ spl14_68
| spl14_69 ),
inference(sat_conversion,[],[f578]) ).
cnf(s60,plain,
( ~ spl14_68
| spl14_70 ),
inference(sat_conversion,[],[f583]) ).
cnf(s61,plain,
( ~ spl14_38
| ~ spl14_71 ),
inference(sat_conversion,[],[f588]) ).
cnf(s62,plain,
( ~ spl14_71
| spl14_72 ),
inference(sat_conversion,[],[f593]) ).
cnf(s63,plain,
( ~ spl14_71
| spl14_73 ),
inference(sat_conversion,[],[f598]) ).
cnf(s64,plain,
( ~ spl14_40
| ~ spl14_74 ),
inference(sat_conversion,[],[f603]) ).
cnf(s65,plain,
( ~ spl14_74
| spl14_75 ),
inference(sat_conversion,[],[f608]) ).
cnf(s66,plain,
( ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f613]) ).
cnf(s67,plain,
( spl14_37
| spl14_39
| spl14_43
| ~ spl14_44
| spl14_47
| spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74 ),
inference(sat_conversion,[],[f614]) ).
cnf(s68,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_77 ),
inference(sat_conversion,[],[f619]) ).
cnf(s69,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_78 ),
inference(sat_conversion,[],[f624]) ).
cnf(s70,plain,
( spl14_37
| spl14_39
| spl14_43
| ~ spl14_44
| spl14_47
| spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74 ),
inference(sat_conversion,[],[f625]) ).
cnf(s71,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_77 ),
inference(sat_conversion,[],[f626]) ).
cnf(s72,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_78 ),
inference(sat_conversion,[],[f627]) ).
cnf(s73,plain,
( spl14_37
| spl14_39
| spl14_43
| ~ spl14_44
| spl14_47
| ~ spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74 ),
inference(sat_conversion,[],[f628]) ).
cnf(s74,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| ~ spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_77 ),
inference(sat_conversion,[],[f629]) ).
cnf(s75,plain,
( spl14_37
| spl14_39
| spl14_43
| spl14_47
| ~ spl14_48
| spl14_51
| spl14_54
| spl14_55
| spl14_58
| spl14_61
| spl14_64
| spl14_67
| spl14_68
| spl14_71
| spl14_74
| spl14_78 ),
inference(sat_conversion,[],[f630]) ).
cnf(s76,plain,
( spl14_38
| spl14_40
| spl14_44
| spl14_48 ),
inference(sat_conversion,[],[f631]) ).
cnf(s77,plain,
( ~ spl14_27
| spl14_42 ),
inference(sat_conversion,[],[f632]) ).
cnf(s78,plain,
( ~ spl14_16
| spl14_46 ),
inference(sat_conversion,[],[f633]) ).
cnf(s79,plain,
( ~ spl14_1
| spl14_50 ),
inference(sat_conversion,[],[f634]) ).
cnf(s80,plain,
( ~ spl14_34
| spl14_53 ),
inference(sat_conversion,[],[f635]) ).
cnf(s81,plain,
( ~ spl14_18
| spl14_57 ),
inference(sat_conversion,[],[f636]) ).
cnf(s82,plain,
( ~ spl14_4
| spl14_60 ),
inference(sat_conversion,[],[f637]) ).
cnf(s83,plain,
( ~ spl14_35
| spl14_63 ),
inference(sat_conversion,[],[f638]) ).
cnf(s84,plain,
( ~ spl14_28
| spl14_66 ),
inference(sat_conversion,[],[f639]) ).
cnf(s85,plain,
( ~ spl14_9
| spl14_70 ),
inference(sat_conversion,[],[f640]) ).
cnf(s86,plain,
( ~ spl14_36
| spl14_73 ),
inference(sat_conversion,[],[f641]) ).
cnf(s87,plain,
( ~ spl14_30
| spl14_76 ),
inference(sat_conversion,[],[f642]) ).
cnf(s88,plain,
( ~ spl14_21
| spl14_78 ),
inference(sat_conversion,[],[f643]) ).
cnf(s90,plain,
( spl14_38
| spl14_41
| spl14_45
| spl14_49 ),
inference(sat_conversion,[],[f645]) ).
cnf(s91,plain,
( spl14_27
| spl14_52
| spl14_79
| spl14_80 ),
inference(sat_conversion,[],[f654]) ).
cnf(s92,plain,
( spl14_27
| spl14_53
| spl14_81
| spl14_82 ),
inference(sat_conversion,[],[f663]) ).
cnf(s93,plain,
( spl14_16
| spl14_62
| spl14_83
| spl14_84 ),
inference(sat_conversion,[],[f672]) ).
cnf(s94,plain,
( spl14_16
| spl14_63
| spl14_85
| spl14_86 ),
inference(sat_conversion,[],[f681]) ).
cnf(s95,plain,
( spl14_1
| spl14_72
| spl14_87
| spl14_88 ),
inference(sat_conversion,[],[f690]) ).
cnf(s96,plain,
( spl14_1
| spl14_73
| spl14_89
| spl14_90 ),
inference(sat_conversion,[],[f699]) ).
cnf(s97,plain,
( spl14_34
| spl14_41
| spl14_91
| spl14_92 ),
inference(sat_conversion,[],[f708]) ).
cnf(s98,plain,
( spl14_34
| spl14_42
| spl14_93
| spl14_94 ),
inference(sat_conversion,[],[f717]) ).
cnf(s100,plain,
( spl14_40
| spl14_52
| spl14_56
| spl14_59 ),
inference(sat_conversion,[],[f719]) ).
cnf(s101,plain,
( spl14_18
| spl14_65
| spl14_85
| spl14_95 ),
inference(sat_conversion,[],[f724]) ).
cnf(s102,plain,
( spl14_18
| spl14_66
| spl14_83
| spl14_96 ),
inference(sat_conversion,[],[f729]) ).
cnf(s103,plain,
( spl14_4
| spl14_75
| spl14_89
| spl14_97 ),
inference(sat_conversion,[],[f734]) ).
cnf(s104,plain,
( spl14_4
| spl14_76
| spl14_87
| spl14_98 ),
inference(sat_conversion,[],[f739]) ).
cnf(s105,plain,
( spl14_35
| spl14_45
| spl14_93
| spl14_99 ),
inference(sat_conversion,[],[f744]) ).
cnf(s106,plain,
( spl14_35
| spl14_46
| spl14_91
| spl14_100 ),
inference(sat_conversion,[],[f749]) ).
cnf(s107,plain,
( spl14_28
| spl14_56
| spl14_81
| spl14_101 ),
inference(sat_conversion,[],[f754]) ).
cnf(s108,plain,
( spl14_28
| spl14_57
| spl14_79
| spl14_102 ),
inference(sat_conversion,[],[f759]) ).
cnf(s109,plain,
( spl14_44
| spl14_63
| spl14_66
| spl14_70 ),
inference(sat_conversion,[],[f760]) ).
cnf(s110,plain,
( spl14_44
| spl14_62
| spl14_65
| spl14_69 ),
inference(sat_conversion,[],[f761]) ).
cnf(s111,plain,
( spl14_9
| spl14_77
| spl14_90
| spl14_98 ),
inference(sat_conversion,[],[f762]) ).
cnf(s112,plain,
( spl14_9
| spl14_78
| spl14_88
| spl14_97 ),
inference(sat_conversion,[],[f763]) ).
cnf(s113,plain,
( spl14_36
| spl14_49
| spl14_94
| spl14_100 ),
inference(sat_conversion,[],[f764]) ).
cnf(s114,plain,
( spl14_36
| spl14_50
| spl14_92
| spl14_99 ),
inference(sat_conversion,[],[f765]) ).
cnf(s115,plain,
( spl14_30
| spl14_59
| spl14_82
| spl14_102 ),
inference(sat_conversion,[],[f766]) ).
cnf(s116,plain,
( spl14_30
| spl14_60
| spl14_80
| spl14_101 ),
inference(sat_conversion,[],[f767]) ).
cnf(s117,plain,
( spl14_21
| spl14_69
| spl14_86
| spl14_96 ),
inference(sat_conversion,[],[f768]) ).
cnf(s118,plain,
( spl14_21
| spl14_70
| spl14_84
| spl14_95 ),
inference(sat_conversion,[],[f769]) ).
cnf(s119,plain,
( spl14_48
| spl14_73
| spl14_76
| spl14_78 ),
inference(sat_conversion,[],[f770]) ).
cnf(s120,plain,
( spl14_48
| spl14_72
| spl14_75
| spl14_77 ),
inference(sat_conversion,[],[f771]) ).
cnf(s121,plain,
( spl14_1
| spl14_16
| spl14_27
| spl14_38 ),
inference(sat_conversion,[],[f772]) ).
cnf(s125,plain,
( spl14_41
| spl14_53
| spl14_85
| spl14_89 ),
inference(sat_conversion,[],[f776]) ).
cnf(s126,plain,
( spl14_4
| spl14_18
| spl14_34
| spl14_40 ),
inference(sat_conversion,[],[f777]) ).
cnf(s128,plain,
( spl14_60
| spl14_75
| spl14_92
| spl14_95 ),
inference(sat_conversion,[],[f779]) ).
cnf(s131,plain,
( spl14_9
| spl14_28
| spl14_35
| spl14_44 ),
inference(sat_conversion,[],[f782]) ).
cnf(s136,plain,
( spl14_21
| spl14_30
| spl14_36
| spl14_48 ),
inference(sat_conversion,[],[f787]) ).
cnf(s138,plain,
( ~ spl14_9
| ~ spl14_16
| spl14_17 ),
inference(sat_conversion,[],[f809]) ).
cnf(s139,plain,
( ~ spl14_4
| ~ spl14_18 ),
inference(sat_conversion,[],[f811]) ).
cnf(s140,plain,
( ~ spl14_16
| ~ spl14_27 ),
inference(sat_conversion,[],[f814]) ).
cnf(s141,plain,
( ~ spl14_16
| ~ spl14_38 ),
inference(sat_conversion,[],[f816]) ).
cnf(s145,plain,
( ~ spl14_4
| ~ spl14_40 ),
inference(sat_conversion,[],[f847]) ).
cnf(s146,plain,
( ~ spl14_42
| ~ spl14_52 ),
inference(sat_conversion,[],[f849]) ).
cnf(s147,plain,
( ~ spl14_41
| ~ spl14_53 ),
inference(sat_conversion,[],[f851]) ).
cnf(s149,plain,
( ~ spl14_4
| ~ spl14_34 ),
inference(sat_conversion,[],[f860]) ).
cnf(s150,plain,
( ~ spl14_66
| ~ spl14_93 ),
inference(sat_conversion,[],[f871]) ).
cnf(s151,plain,
( ~ spl14_69
| ~ spl14_100 ),
inference(sat_conversion,[],[f873]) ).
cnf(s156,plain,
( ~ spl14_57
| ~ spl14_65 ),
inference(sat_conversion,[],[f902]) ).
cnf(s157,plain,
( ~ spl14_69
| ~ spl14_102 ),
inference(sat_conversion,[],[f906]) ).
cnf(s158,plain,
( ~ spl14_56
| ~ spl14_66 ),
inference(sat_conversion,[],[f912]) ).
cnf(s159,plain,
( ~ spl14_56
| ~ spl14_66 ),
inference(sat_conversion,[],[f914]) ).
cnf(s161,plain,
( ~ spl14_60
| ~ spl14_92 ),
inference(sat_conversion,[],[f921]) ).
cnf(s162,plain,
( ~ spl14_30
| ~ spl14_48 ),
inference(sat_conversion,[],[f932]) ).
cnf(s163,plain,
( spl14_5
| ~ spl14_16
| ~ spl14_34 ),
inference(sat_conversion,[],[f934]) ).
cnf(s165,plain,
( ~ spl14_70
| ~ spl14_101 ),
inference(sat_conversion,[],[f952]) ).
cnf(s167,plain,
( spl14_3
| ~ spl14_27
| ~ spl14_34 ),
inference(sat_conversion,[],[f960]) ).
cnf(s171,plain,
( ~ spl14_46
| ~ spl14_79 ),
inference(sat_conversion,[],[f989]) ).
cnf(s172,plain,
( ~ spl14_27
| spl14_32
| ~ spl14_35
| ~ spl14_97 ),
inference(sat_conversion,[],[f991]) ).
cnf(s173,plain,
( ~ spl14_46
| ~ spl14_62 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s174,plain,
( ~ spl14_46
| ~ spl14_62 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s176,plain,
( ~ spl14_45
| ~ spl14_63 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s177,plain,
( ~ spl14_60
| ~ spl14_95 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s178,plain,
( ~ spl14_85
| ~ spl14_89 ),
inference(sat_conversion,[],[f1042]) ).
cnf(s179,plain,
( ~ spl14_70
| ~ spl14_99 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s181,plain,
( ~ spl14_9
| ~ spl14_10
| ~ spl14_48 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s184,plain,
( ~ spl14_21
| ~ spl14_48 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s185,plain,
( ~ spl14_66
| ~ spl14_98 ),
inference(sat_conversion,[],[f1083]) ).
cnf(s186,plain,
( ~ spl14_73
| ~ spl14_86 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s188,plain,
( spl14_11
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(sat_conversion,[],[f1094]) ).
cnf(s190,plain,
( ~ spl14_15
| ~ spl14_28
| ~ spl14_34
| ~ spl14_46 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s191,plain,
( ~ spl14_72
| ~ spl14_80 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s192,plain,
( ~ spl14_45
| ~ spl14_81 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s193,plain,
( ~ spl14_56
| ~ spl14_98 ),
inference(sat_conversion,[],[f1151]) ).
cnf(s195,plain,
( spl14_4
| ~ spl14_28
| ~ spl14_29 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s198,plain,
( spl14_15
| ~ spl14_18
| ~ spl14_28 ),
inference(sat_conversion,[],[f1197]) ).
cnf(s202,plain,
( ~ spl14_28
| spl14_32
| ~ spl14_34
| ~ spl14_88 ),
inference(sat_conversion,[],[f1230]) ).
cnf(s204,plain,
( ~ spl14_59
| ~ spl14_76 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s208,plain,
( ~ spl14_4
| ~ spl14_28
| spl14_29 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s210,plain,
( ~ spl14_50
| ~ spl14_84 ),
inference(sat_conversion,[],[f1284]) ).
cnf(s211,plain,
( ~ spl14_65
| ~ spl14_91 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s219,plain,
( ~ spl14_69
| ~ spl14_78 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s220,plain,
( ~ spl14_69
| ~ spl14_78 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s221,plain,
( ~ spl14_41
| ~ spl14_85 ),
inference(sat_conversion,[],[f1356]) ).
cnf(s222,plain,
( ~ spl14_42
| ~ spl14_83 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s223,plain,
( ~ spl14_42
| ~ spl14_83 ),
inference(sat_conversion,[],[f1365]) ).
cnf(s225,plain,
( ~ spl14_72
| ~ spl14_84 ),
inference(sat_conversion,[],[f1372]) ).
cnf(s227,plain,
( ~ spl14_46
| ~ spl14_88 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s229,plain,
( ~ spl14_42
| ~ spl14_87 ),
inference(sat_conversion,[],[f1388]) ).
cnf(s234,plain,
( ~ spl14_80
| ~ spl14_84 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s237,plain,
( spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_53 ),
inference(sat_conversion,[],[f1427]) ).
cnf(s238,plain,
( ~ spl14_14
| ~ spl14_28
| spl14_34 ),
inference(sat_conversion,[],[f1430]) ).
cnf(s239,plain,
( ~ spl14_83
| ~ spl14_87 ),
inference(sat_conversion,[],[f1471]) ).
cnf(s240,plain,
( ~ spl14_50
| ~ spl14_80 ),
inference(sat_conversion,[],[f1473]) ).
cnf(s241,plain,
( ~ spl14_82
| ~ spl14_86 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s242,plain,
( ~ spl14_65
| ~ spl14_97 ),
inference(sat_conversion,[],[f1500]) ).
cnf(s243,plain,
( ~ spl14_52
| ~ spl14_83 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s244,plain,
( ~ spl14_52
| ~ spl14_83 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s246,plain,
( ~ spl14_1
| ~ spl14_16 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s253,plain,
( ~ spl14_11
| ~ spl14_28
| ~ spl14_34
| spl14_46 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s255,plain,
( ~ spl14_34
| ~ spl14_40 ),
inference(sat_conversion,[],[f1586]) ).
cnf(s256,plain,
( ~ spl14_78
| ~ spl14_100 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s257,plain,
( spl14_14
| ~ spl14_28
| ~ spl14_34 ),
inference(sat_conversion,[],[f1591]) ).
cnf(s261,plain,
( spl14_10
| ~ spl14_28
| ~ spl14_40 ),
inference(sat_conversion,[],[f1602]) ).
cnf(s262,plain,
( ~ spl14_73
| ~ spl14_82 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s263,plain,
( ~ spl14_53
| ~ spl14_85 ),
inference(sat_conversion,[],[f1640]) ).
cnf(s264,plain,
( ~ spl14_53
| ~ spl14_85 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s265,plain,
( ~ spl14_45
| ~ spl14_90 ),
inference(sat_conversion,[],[f1647]) ).
cnf(s266,plain,
( ~ spl14_45
| ~ spl14_90 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s268,plain,
( ~ spl14_53
| ~ spl14_89 ),
inference(sat_conversion,[],[f1657]) ).
cnf(s275,plain,
( spl14_3
| ~ spl14_9
| ~ spl14_16
| ~ spl14_82 ),
inference(sat_conversion,[],[f1673]) ).
cnf(s276,plain,
( spl14_7
| ~ spl14_16
| ~ spl14_28 ),
inference(sat_conversion,[],[f1676]) ).
cnf(s288,plain,
( spl14_1
| ~ spl14_19
| ~ spl14_34 ),
inference(sat_conversion,[],[f1710]) ).
cnf(s289,plain,
( ~ spl14_5
| ~ spl14_19 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s294,plain,
( ~ spl14_36
| ~ spl14_48 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s295,plain,
( ~ spl14_60
| ~ spl14_75 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s296,plain,
( ~ spl14_70
| ~ spl14_77 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s297,plain,
( ~ spl14_76
| ~ spl14_96 ),
inference(sat_conversion,[],[f1761]) ).
cnf(s300,plain,
( ~ spl14_50
| ~ spl14_72 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s301,plain,
( spl14_5
| ~ spl14_18
| ~ spl14_44 ),
inference(sat_conversion,[],[f1822]) ).
cnf(s302,plain,
( spl14_12
| ~ spl14_18
| ~ spl14_35 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s306,plain,
( ~ spl14_49
| ~ spl14_82 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s308,plain,
( ~ spl14_7
| ~ spl14_16
| ~ spl14_35 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s310,plain,
( spl14_11
| ~ spl14_16
| ~ spl14_35 ),
inference(sat_conversion,[],[f1877]) ).
cnf(s311,plain,
( ~ spl14_3
| ~ spl14_16
| ~ spl14_35 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s313,plain,
( ~ spl14_16
| spl14_20
| ~ spl14_28
| ~ spl14_89 ),
inference(sat_conversion,[],[f1894]) ).
cnf(s319,plain,
( ~ spl14_3
| ~ spl14_16
| ~ spl14_28
| ~ spl14_41 ),
inference(sat_conversion,[],[f1928]) ).
cnf(s321,plain,
( ~ spl14_63
| ~ spl14_81 ),
inference(sat_conversion,[],[f1950]) ).
cnf(s322,plain,
( ~ spl14_63
| ~ spl14_81 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s324,plain,
( ~ spl14_63
| ~ spl14_90 ),
inference(sat_conversion,[],[f1962]) ).
cnf(s325,plain,
( ~ spl14_75
| ~ spl14_92 ),
inference(sat_conversion,[],[f1969]) ).
cnf(s326,plain,
( ~ spl14_75
| ~ spl14_92 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s328,plain,
( ~ spl14_76
| ~ spl14_94 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s334,plain,
( ~ spl14_99
| ~ spl14_101 ),
inference(sat_conversion,[],[f2028]) ).
cnf(s335,plain,
( ~ spl14_12
| spl14_34
| ~ spl14_40 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s336,plain,
( ~ spl14_92
| ~ spl14_95 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s337,plain,
( ~ spl14_77
| ~ spl14_101 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s338,plain,
( ~ spl14_77
| ~ spl14_99 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s339,plain,
( ~ spl14_9
| spl14_10
| ~ spl14_30 ),
inference(sat_conversion,[],[f2049]) ).
cnf(s342,plain,
( ~ spl14_9
| spl14_14
| ~ spl14_36 ),
inference(sat_conversion,[],[f2050]) ).
cnf(s355,plain,
( ~ spl14_59
| ~ spl14_94 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s357,plain,
( ~ spl14_59
| ~ spl14_96 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s359,plain,
( ~ spl14_9
| ~ spl14_18
| spl14_19 ),
inference(sat_conversion,[],[f2113]) ).
cnf(s365,plain,
( ~ spl14_49
| ~ spl14_73 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s366,plain,
( ~ spl14_52
| ~ spl14_87 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s367,plain,
( ~ spl14_52
| ~ spl14_87 ),
inference(sat_conversion,[],[f2212]) ).
cnf(s369,plain,
( ~ spl14_57
| ~ spl14_91 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s370,plain,
( ~ spl14_56
| ~ spl14_93 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s371,plain,
( ~ spl14_56
| ~ spl14_93 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s377,plain,
( spl14_10
| ~ spl14_27
| ~ spl14_35 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s381,plain,
( ~ spl14_9
| spl14_15
| ~ spl14_36
| ~ spl14_79 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s383,plain,
( ~ spl14_9
| ~ spl14_35 ),
inference(sat_conversion,[],[f2282]) ).
cnf(s384,plain,
( ~ spl14_75
| ~ spl14_95 ),
inference(sat_conversion,[],[f2284]) ).
cnf(s385,plain,
( ~ spl14_100
| ~ spl14_102 ),
inference(sat_conversion,[],[f2286]) ).
cnf(s386,plain,
( spl14_12
| ~ spl14_34
| ~ spl14_38 ),
inference(sat_conversion,[],[f2293]) ).
cnf(s393,plain,
( ~ spl14_9
| ~ spl14_10
| spl14_30 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s399,plain,
( ~ spl14_1
| spl14_19
| ~ spl14_34 ),
inference(sat_conversion,[],[f2339]) ).
cnf(s402,plain,
( ~ spl14_62
| ~ spl14_79 ),
inference(sat_conversion,[],[f2346]) ).
cnf(s406,plain,
( ~ spl14_4
| spl14_5
| ~ spl14_21 ),
inference(sat_conversion,[],[f2355]) ).
cnf(s436,plain,
( ~ spl14_27
| ~ spl14_38 ),
inference(sat_conversion,[],[f2478]) ).
cnf(s437,plain,
( ~ spl14_9
| ~ spl14_28 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s441,plain,
( ~ spl14_4
| spl14_11
| ~ spl14_28
| ~ spl14_100 ),
inference(sat_conversion,[],[f2494]) ).
cnf(s448,plain,
( ~ spl14_9
| ~ spl14_44 ),
inference(sat_conversion,[],[f2550]) ).
cnf(s459,plain,
( ~ spl14_28
| ~ spl14_44 ),
inference(sat_conversion,[],[f2615]) ).
cnf(s466,plain,
( ~ spl14_1
| ~ spl14_38 ),
inference(sat_conversion,[],[f2651]) ).
cnf(s471,plain,
( ~ spl14_10
| ~ spl14_28
| spl14_40 ),
inference(sat_conversion,[],[f2664]) ).
cnf(s474,plain,
( ~ spl14_1
| ~ spl14_27 ),
inference(sat_conversion,[],[f2705]) ).
cnf(s475,plain,
( ~ spl14_21
| ~ spl14_30 ),
inference(sat_conversion,[],[f2707]) ).
cnf(s481,plain,
( ~ spl14_5
| spl14_18
| ~ spl14_40 ),
inference(sat_conversion,[],[f2721]) ).
cnf(s483,plain,
( ~ spl14_21
| ~ spl14_36 ),
inference(sat_conversion,[],[f2740]) ).
cnf(s484,plain,
( ~ spl14_78
| ~ spl14_102 ),
inference(sat_conversion,[],[f2742]) ).
cnf(s487,plain,
( ~ spl14_30
| ~ spl14_36 ),
inference(sat_conversion,[],[f2766]) ).
cnf(s488,plain,
( ~ spl14_10
| spl14_28
| ~ spl14_44 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s490,plain,
( ~ spl14_11
| ~ spl14_44 ),
inference(sat_conversion,[],[f2788]) ).
cnf(s491,plain,
( ~ spl14_62
| ~ spl14_88 ),
inference(sat_conversion,[],[f2807]) ).
cnf(s492,plain,
( ~ spl14_62
| ~ spl14_88 ),
inference(sat_conversion,[],[f2809]) ).
cnf(s493,plain,
( ~ spl14_91
| ~ spl14_97 ),
inference(sat_conversion,[],[f2821]) ).
cnf(s494,plain,
( ~ spl14_91
| ~ spl14_97 ),
inference(sat_conversion,[],[f2823]) ).
cnf(s495,plain,
( ~ spl14_12
| ~ spl14_34
| spl14_38 ),
inference(sat_conversion,[],[f2824]) ).
cnf(s496,plain,
( spl14_14
| ~ spl14_35
| ~ spl14_38 ),
inference(sat_conversion,[],[f2825]) ).
cnf(s498,plain,
( ~ spl14_57
| ~ spl14_97 ),
inference(sat_conversion,[],[f2853]) ).
cnf(s502,plain,
( ~ spl14_1
| spl14_13
| ~ spl14_34
| ~ spl14_96 ),
inference(sat_conversion,[],[f2859]) ).
cnf(s509,plain,
( spl14_6
| ~ spl14_19
| ~ spl14_94 ),
inference(sat_conversion,[],[f2871]) ).
cnf(s511,plain,
( ~ spl14_1
| spl14_29
| ~ spl14_35 ),
inference(sat_conversion,[],[f2902]) ).
cnf(s513,plain,
( ~ spl14_35
| ~ spl14_44 ),
inference(sat_conversion,[],[f2919]) ).
cnf(s514,plain,
( ~ spl14_93
| ~ spl14_98 ),
inference(sat_conversion,[],[f2945]) ).
cnf(s516,plain,
( ~ spl14_79
| ~ spl14_88 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s517,plain,
( ~ spl14_79
| ~ spl14_88 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s519,plain,
( ~ spl14_9
| spl14_11
| ~ spl14_30
| ~ spl14_91 ),
inference(sat_conversion,[],[f3032]) ).
cnf(s520,plain,
( ~ spl14_5
| spl14_16
| ~ spl14_34 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s523,plain,
( ~ spl14_16
| spl14_24
| ~ spl14_34
| ~ spl14_98 ),
inference(sat_conversion,[],[f3074]) ).
cnf(s527,plain,
( spl14_2
| ~ spl14_18
| ~ spl14_27 ),
inference(sat_conversion,[],[f3217]) ).
cnf(s528,plain,
( ~ spl14_18
| spl14_20
| ~ spl14_27
| ~ spl14_90 ),
inference(sat_conversion,[],[f3221]) ).
cnf(s530,plain,
( ~ spl14_41
| ~ spl14_45 ),
inference(sat_conversion,[],[f3236]) ).
cnf(s532,plain,
( ~ spl14_5
| spl14_24
| ~ spl14_98 ),
inference(sat_conversion,[],[f3245]) ).
cnf(s533,plain,
( ~ spl14_75
| ~ spl14_77 ),
inference(sat_conversion,[],[f3248]) ).
cnf(s534,plain,
( ~ spl14_38
| ~ spl14_41 ),
inference(sat_conversion,[],[f3261]) ).
cnf(s535,plain,
( ~ spl14_2
| spl14_16
| ~ spl14_38 ),
inference(sat_conversion,[],[f3270]) ).
cnf(s536,plain,
( spl14_5
| ~ spl14_18
| ~ spl14_40 ),
inference(sat_conversion,[],[f3281]) ).
cnf(s551,plain,
( ~ spl14_49
| ~ spl14_86 ),
inference(sat_conversion,[],[f3341]) ).
cnf(s561,plain,
( ~ spl14_5
| spl14_6
| ~ spl14_93 ),
inference(sat_conversion,[],[f3359]) ).
cnf(s565,plain,
( ~ spl14_44
| ~ spl14_70 ),
inference(sat_conversion,[],[f3367]) ).
cnf(s571,plain,
( ~ spl14_12
| ~ spl14_18
| spl14_35 ),
inference(sat_conversion,[],[f3415]) ).
cnf(s575,plain,
( ~ spl14_18
| spl14_24
| ~ spl14_35
| ~ spl14_87 ),
inference(sat_conversion,[],[f3418]) ).
cnf(s576,plain,
( ~ spl14_18
| ~ spl14_83 ),
inference(sat_conversion,[],[f3419]) ).
cnf(s577,plain,
( ~ spl14_18
| ~ spl14_95 ),
inference(sat_conversion,[],[f3420]) ).
cnf(s578,plain,
( ~ spl14_18
| ~ spl14_85 ),
inference(sat_conversion,[],[f3421]) ).
cnf(s579,plain,
( ~ spl14_18
| ~ spl14_96 ),
inference(sat_conversion,[],[f3422]) ).
cnf(s581,plain,
( ~ spl14_41
| ~ spl14_92 ),
inference(sat_conversion,[],[f3430]) ).
cnf(s583,plain,
( ~ spl14_41
| ~ spl14_49 ),
inference(sat_conversion,[],[f3432]) ).
cnf(s587,plain,
( ~ spl14_57
| ~ spl14_79 ),
inference(sat_conversion,[],[f3436]) ).
cnf(s588,plain,
( ~ spl14_57
| ~ spl14_60 ),
inference(sat_conversion,[],[f3437]) ).
cnf(s593,plain,
( ~ spl14_40
| ~ spl14_52 ),
inference(sat_conversion,[],[f3510]) ).
cnf(s594,plain,
( ~ spl14_40
| ~ spl14_57 ),
inference(sat_conversion,[],[f3513]) ).
cnf(s595,plain,
( ~ spl14_48
| ~ spl14_44
| spl14_55
| spl14_54
| spl14_64
| spl14_74
| spl14_39
| spl14_37
| spl14_51
| spl14_61
| spl14_71 ),
inference(rat,[],[s73,s34,s46,s55,s31,s60,s565]) ).
cnf(s598,plain,
( ~ spl14_72
| spl14_30
| spl14_70
| spl14_36
| spl14_21 ),
inference(rat,[],[s334,s116,s114,s177,s336,s118,s191,s225,s300]) ).
cnf(s600,plain,
( ~ spl14_73
| spl14_96
| spl14_94
| spl14_36
| spl14_21 ),
inference(rat,[],[s151,s117,s113,s186,s365]) ).
cnf(s601,plain,
( ~ spl14_50
| ~ spl14_42
| spl14_16
| spl14_1 ),
inference(rat,[],[s491,s93,s95,s210,s300,s229,s223]) ).
cnf(s603,plain,
( ~ spl14_50
| spl14_52
| spl14_27
| spl14_16
| spl14_1 ),
inference(rat,[],[s239,s93,s95,s402,s517,s91,s210,s240,s300]) ).
cnf(s604,plain,
( spl14_27
| spl14_18
| spl14_16
| spl14_14
| spl14_12
| spl14_10
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s178,s101,s103,s211,s494,s97,s161,s177,s295,s48,s70,s36,s603,s60,s31,s55,s565,s595,s131,s45,s261,s40,s52,s64,s593,s594,s126,s29,s496,s386,s25,s37,s49,s61,s534,s121]) ).
cnf(s605,plain,
( ~ spl14_62
| spl14_28
| spl14_57
| spl14_35
| spl14_9 ),
inference(rat,[],[s493,s106,s112,s385,s484,s108,s174,s402,s492]) ).
cnf(s606,plain,
( spl14_18
| spl14_16
| spl14_14
| spl14_12
| spl14_10
| spl14_9
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s117,s88,s186,s119,s204,s357,s157,s484,s47,s108,s70,s517,s595,s95,s62,s225,s93,s50,s605,s60,s31,s55,s565,s131,s45,s36,s38,s261,s28,s40,s52,s64,s594,s601,s146,s223,s229,s126,s27,s77,s167,s377,s436,s604]) ).
cnf(s608,plain,
( spl14_18
| spl14_14
| spl14_12
| spl14_11
| spl14_10
| spl14_9
| spl14_7
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s48,s72,s595,s177,s62,s118,s36,s88,s191,s234,s240,s484,s38,s60,s91,s108,s50,s28,s40,s52,s64,s593,s594,s31,s43,s55,s565,s171,s174,s27,s126,s131,s78,s140,s141,s163,s276,s310,s606]) ).
cnf(s610,plain,
( ~ spl14_27
| spl14_16
| ~ spl14_44
| spl14_18
| spl14_9
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s186,s119,s117,s88,s204,s357,s157,s484,s47,s108,s70,s517,s595,s95,s62,s225,s93,s50,s605,s36,s38,s28,s40,s52,s64,s594,s601,s146,s223,s229,s126,s27,s77,s167,s436,s513,s459,s55,s43,s31,s60,s565]) ).
cnf(s611,plain,
( spl14_16
| ~ spl14_44
| spl14_18
| spl14_12
| spl14_9
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s178,s101,s103,s211,s494,s97,s161,s177,s295,s48,s70,s36,s595,s603,s40,s52,s64,s593,s126,s29,s386,s25,s37,s49,s61,s534,s121,s610,s55,s43,s31,s60,s565]) ).
cnf(s612,plain,
( ~ spl14_44
| spl14_18
| spl14_12
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s48,s177,s72,s595,s118,s62,s36,s88,s191,s234,s240,s484,s38,s91,s108,s50,s28,s40,s52,s64,s593,s594,s171,s174,s27,s126,s78,s140,s141,s163,s611,s60,s31,s43,s55,s459,s565]) ).
cnf(s613,plain,
( ~ spl14_27
| spl14_44
| ~ spl14_14
| spl14_10
| spl14_9
| spl14_3 ),
inference(rat,[],[s238,s131,s167,s377]) ).
cnf(s614,plain,
( spl14_68
| spl14_58
| spl14_21
| spl14_48
| spl14_43
| spl14_81
| spl14_47
| spl14_54
| spl14_64
| spl14_74
| spl14_57
| spl14_28
| spl14_34
| spl14_37
| spl14_51
| spl14_61
| spl14_71
| spl14_41
| spl14_27
| spl14_44
| spl14_4 ),
inference(rat,[],[s87,s297,s116,s117,s234,s241,s118,s92,s161,s336,s268,s97,s103,s211,s242,s110,s402,s108,s296,s337,s533,s220,s484,s68,s69,s57,s29,s45]) ).
cnf(s615,plain,
( ~ spl14_70
| spl14_81
| spl14_90
| spl14_28
| spl14_9 ),
inference(rat,[],[s193,s107,s111,s165,s296]) ).
cnf(s616,plain,
( ~ spl14_60
| spl14_34
| spl14_41
| spl14_18
| spl14_4 ),
inference(rat,[],[s178,s101,s103,s211,s494,s97,s161,s177,s295]) ).
cnf(s617,plain,
( spl14_48
| spl14_60
| spl14_68
| spl14_43
| spl14_81
| spl14_47
| spl14_54
| spl14_64
| spl14_74
| spl14_57
| spl14_28
| spl14_34
| spl14_16
| spl14_27
| spl14_44
| spl14_4
| spl14_1 ),
inference(rat,[],[s239,s95,s93,s402,s517,s191,s234,s108,s116,s337,s484,s475,s68,s69,s614,s57,s61,s49,s37,s25,s29,s534,s121,s45,s48]) ).
cnf(s618,plain,
( spl14_16
| spl14_27
| spl14_44
| ~ spl14_14
| spl14_18
| spl14_12
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s118,s234,s336,s116,s114,s337,s338,s74,s162,s184,s294,s617,s48,s616,s60,s615,s32,s176,s322,s324,s36,s83,s603,s45,s131,s40,s52,s64,s593,s594,s238,s126,s29,s386,s25,s37,s49,s61,s534,s121,s57]) ).
cnf(s619,plain,
( spl14_18
| spl14_12
| spl14_1
| spl14_11
| spl14_10
| spl14_9
| spl14_7
| spl14_5
| spl14_4
| spl14_3 ),
inference(rat,[],[s131,s276,s310,s618,s613,s612,s608]) ).
cnf(s620,plain,
( ~ spl14_78
| spl14_65
| spl14_91
| spl14_44
| spl14_35 ),
inference(rat,[],[s173,s110,s106,s220,s256]) ).
cnf(s621,plain,
( spl14_12
| spl14_11
| spl14_1
| spl14_3
| spl14_10
| spl14_9
| spl14_7
| spl14_5
| spl14_4 ),
inference(rat,[],[s151,s106,s110,s227,s492,s112,s620,s156,s369,s498,s81,s301,s302,s619]) ).
cnf(s622,plain,
( ~ spl14_27
| spl14_18
| ~ spl14_44
| spl14_9
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s610,s140]) ).
cnf(s623,plain,
( ~ spl14_60
| spl14_41
| spl14_18
| spl14_4 ),
inference(rat,[],[s242,s101,s103,s264,s268,s80,s616,s177,s295]) ).
cnf(s624,plain,
( ~ spl14_50
| spl14_16
| spl14_27
| spl14_1 ),
inference(rat,[],[s491,s93,s95,s244,s367,s603,s210,s300]) ).
cnf(s626,plain,
( ~ spl14_88
| ~ spl14_65
| ~ spl14_44 ),
inference(rat,[],[s385,s106,s108,s227,s517,s513,s459,s211,s156]) ).
cnf(s627,plain,
( ~ spl14_65
| ~ spl14_44
| spl14_9 ),
inference(rat,[],[s171,s106,s108,s256,s484,s112,s626,s156,s211,s242,s513,s459]) ).
cnf(s628,plain,
( ~ spl14_74
| spl14_65
| spl14_18
| spl14_4 ),
inference(rat,[],[s263,s80,s101,s126,s384,s64,s65]) ).
cnf(s629,plain,
~ spl14_54,
inference(rat,[],[s40,s42]) ).
cnf(s630,plain,
( ~ spl14_39
| spl14_18
| ~ spl14_12
| spl14_4 ),
inference(rat,[],[s495,s126,s534,s28,s29]) ).
cnf(s631,plain,
( ~ spl14_60
| spl14_65
| spl14_18
| spl14_4 ),
inference(rat,[],[s221,s101,s623,s177]) ).
cnf(s632,plain,
( spl14_34
| spl14_18
| ~ spl14_12
| spl14_4 ),
inference(rat,[],[s126,s335]) ).
cnf(s633,plain,
( ~ spl14_44
| ~ spl14_12
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s70,s595,s61,s36,s624,s25,s37,s49,s163,s495,s632,s48,s631,s630,s628,s53,s627,s622,s60,s301,s31,s43,s55,s565,s629]) ).
cnf(s634,plain,
( ~ spl14_98
| ~ spl14_76
| spl14_40
| spl14_18 ),
inference(rat,[],[s243,s102,s100,s185,s193,s297,s204]) ).
cnf(s635,plain,
( ~ spl14_74
| ~ spl14_34
| spl14_18
| spl14_44
| spl14_11
| spl14_9
| spl14_4 ),
inference(rat,[],[s112,s202,s256,s17,s106,s257,s188,s131,s83,s324,s111,s634,s211,s242,s533,s628,s65,s66,s255]) ).
cnf(s636,plain,
( spl14_55
| spl14_68
| spl14_43
| spl14_64
| spl14_48
| spl14_74
| spl14_58
| spl14_50
| spl14_85
| spl14_89
| spl14_37
| spl14_51
| spl14_61
| spl14_71
| spl14_39
| spl14_18
| spl14_67
| spl14_4 ),
inference(rat,[],[s357,s117,s115,s186,s262,s86,s483,s487,s114,s336,s101,s242,s103,s338,s533,s220,s484,s68,s72,s36,s629]) ).
cnf(s637,plain,
( ~ spl14_57
| spl14_85
| spl14_89
| spl14_18
| spl14_4 ),
inference(rat,[],[s384,s101,s103,s156,s498]) ).
cnf(s638,plain,
( ~ spl14_88
| spl14_102
| spl14_57
| ~ spl14_34 ),
inference(rat,[],[s202,s17,s257,s108,s517]) ).
cnf(s639,plain,
( ~ spl14_68
| spl14_48
| spl14_57
| spl14_60
| spl14_50
| ~ spl14_34
| spl14_18
| spl14_9 ),
inference(rat,[],[s116,s487,s191,s114,s120,s336,s384,s101,s242,s112,s638,s157,s220,s165,s179,s296,s59,s60,s264,s80]) ).
cnf(s640,plain,
( ~ spl14_43
| ~ spl14_34
| spl14_44
| spl14_11
| spl14_9 ),
inference(rat,[],[s83,s131,s176,s188,s32,s33]) ).
cnf(s641,plain,
( ~ spl14_64
| ~ spl14_34
| spl14_44
| spl14_11
| spl14_9
| spl14_4 ),
inference(rat,[],[s112,s256,s202,s106,s17,s257,s188,s131,s83,s324,s111,s533,s103,s211,s242,s185,s53,s54,s268,s80]) ).
cnf(s642,plain,
( spl14_48
| spl14_64
| spl14_43
| spl14_74
| spl14_60
| spl14_50
| spl14_37
| spl14_51
| spl14_61
| spl14_71
| ~ spl14_34
| spl14_39
| spl14_18
| spl14_67
| spl14_9
| spl14_4 ),
inference(rat,[],[s636,s639,s48,s45,s637,s264,s268,s80]) ).
cnf(s643,plain,
( spl14_18
| ~ spl14_12
| spl14_11
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s101,s336,s242,s114,s103,s338,s533,s74,s58,s294,s642,s641,s640,s45,s637,s635,s48,s36,s623,s624,s264,s268,s25,s37,s49,s61,s534,s163,s167,s80,s495,s632,s630,s57,s633,s629]) ).
cnf(s644,plain,
( ~ spl14_74
| spl14_41
| spl14_50
| spl14_81
| spl14_90
| spl14_91
| spl14_96
| spl14_9
| spl14_1 ),
inference(rat,[],[s157,s117,s115,s483,s487,s114,s186,s262,s334,s96,s107,s268,s84,s80,s185,s193,s97,s111,s326,s533,s204,s65,s66]) ).
cnf(s645,plain,
( spl14_68
| spl14_77
| spl14_37
| spl14_43
| spl14_61
| spl14_39
| spl14_58
| spl14_47
| spl14_51
| spl14_74
| spl14_67
| spl14_64
| spl14_71
| spl14_55 ),
inference(rat,[],[s74,s68,s629]) ).
cnf(s646,plain,
( spl14_77
| spl14_74
| spl14_39
| spl14_47
| spl14_37
| spl14_51
| spl14_61
| spl14_71
| spl14_43
| spl14_64
| spl14_58
| spl14_81
| spl14_90
| spl14_67
| spl14_9 ),
inference(rat,[],[s645,s60,s615,s84,s44,s185,s193,s111]) ).
cnf(s647,plain,
( spl14_11
| spl14_10
| spl14_9
| spl14_7
| spl14_5
| spl14_4
| spl14_3
| spl14_2
| spl14_1 ),
inference(rat,[],[s117,s88,s151,s256,s113,s328,s104,s193,s86,s107,s241,s262,s306,s238,s92,s80,s268,s103,s337,s533,s646,s644,s29,s36,s496,s25,s37,s49,s61,s534,s32,s53,s48,s624,s121,s176,s322,s324,s575,s156,s369,s498,s588,s310,s83,s527,s11,s81,s571,s579,s643,s57,s633,s621]) ).
cnf(s648,plain,
( ~ spl14_74
| spl14_18
| ~ spl14_11
| spl14_9
| spl14_5
| spl14_4 ),
inference(rat,[],[s256,s112,s113,s227,s86,s253,s186,s551,s131,s94,s83,s264,s324,s163,s80,s111,s242,s126,s533,s634,s328,s628,s64,s65,s66,s490]) ).
cnf(s649,plain,
( spl14_43
| spl14_64
| spl14_37
| spl14_51
| spl14_61
| spl14_71
| spl14_50
| ~ spl14_34
| spl14_74
| spl14_18
| spl14_67
| spl14_9
| spl14_4 ),
inference(rat,[],[s101,s336,s242,s114,s103,s338,s533,s645,s58,s294,s642,s29,s36,s45,s637,s268,s264,s48,s623,s147,s80]) ).
cnf(s650,plain,
( ~ spl14_45
| spl14_85
| spl14_89
| spl14_16
| spl14_1 ),
inference(rat,[],[s186,s94,s96,s176,s266]) ).
cnf(s651,plain,
( ~ spl14_34
| spl14_18
| ~ spl14_11
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s87,s115,s328,s355,s113,s256,s484,s112,s227,s86,s253,s186,s241,s551,s131,s94,s83,s324,s111,s533,s103,s242,s185,s53,s54,s649,s32,s650,s25,s37,s49,s61,s624,s121,s264,s268,s163,s167,s80,s57,s490,s648]) ).
cnf(s652,plain,
( spl14_16
| spl14_27
| spl14_12
| spl14_18
| spl14_44
| spl14_10
| spl14_9
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s618,s606]) ).
cnf(s653,plain,
( spl14_18
| ~ spl14_11
| spl14_10
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s242,s110,s112,s157,s484,s108,s171,s174,s227,s78,s652,s377,s131,s261,s594,s632,s126,s651,s490]) ).
cnf(s654,plain,
( ~ spl14_34
| spl14_27
| ~ spl14_18
| spl14_67
| spl14_9
| spl14_5
| spl14_4
| spl14_1 ),
inference(rat,[],[s644,s646,s322,s324,s83,s571,s533,s32,s36,s386,s25,s37,s49,s61,s29,s103,s650,s624,s121,s147,s268,s163,s80,s579,s578,s498,s369,s48,s588,s53,s156,s81]) ).
cnf(s655,plain,
( ~ spl14_74
| spl14_34
| spl14_65
| spl14_91
| spl14_27
| spl14_40
| spl14_44
| spl14_1 ),
inference(rat,[],[s151,s110,s113,s174,s294,s78,s76,s121,s534,s583,s97,s326,s328,s65,s66]) ).
cnf(s656,plain,
( ~ spl14_12
| spl14_47
| ~ spl14_38
| spl14_74
| spl14_34
| spl14_27
| ~ spl14_18
| spl14_67
| spl14_9
| spl14_4 ),
inference(rat,[],[s117,s88,s151,s256,s113,s328,s104,s193,s107,s337,s86,s646,s241,s262,s306,s32,s92,s238,s176,s322,s324,s575,s496,s83,s11,s571,s579,s48,s588,s53,s156,s61,s49,s37,s25,s29,s268,s103,s326,s97,s534,s369,s498,s81]) ).
cnf(s657,plain,
( spl14_35
| spl14_65
| spl14_91
| spl14_97
| spl14_44
| spl14_9 ),
inference(rat,[],[s151,s106,s110,s227,s492,s112,s620]) ).
cnf(s658,plain,
( spl14_16
| ~ spl14_12
| spl14_74
| spl14_34
| spl14_27
| ~ spl14_18
| spl14_67
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s36,s656,s624,s121]) ).
cnf(s659,plain,
( spl14_10
| spl14_9
| spl14_1
| spl14_7
| spl14_5
| spl14_4
| spl14_3
| spl14_2 ),
inference(rat,[],[s598,s95,s162,s184,s294,s227,s76,s615,s78,s141,s276,s658,s575,s11,s322,s324,s302,s83,s657,s655,s654,s156,s369,s498,s527,s81,s536,s653,s57,s490,s647]) ).
cnf(s660,plain,
( ~ spl14_44
| ~ spl14_10 ),
inference(rat,[],[s488,s459]) ).
cnf(s661,plain,
( ~ spl14_34
| spl14_18
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s386,s643,s121,s651,s163,s167]) ).
cnf(s662,plain,
( ~ spl14_99
| spl14_43
| spl14_58
| spl14_47
| spl14_37
| spl14_61
| spl14_71
| ~ spl14_40
| spl14_67 ),
inference(rat,[],[s60,s645,s179,s338,s64,s52,s28,s45,s594,s38,s593]) ).
cnf(s663,plain,
( ~ spl14_45
| ~ spl14_89
| spl14_16
| spl14_27 ),
inference(rat,[],[s241,s94,s92,s176,s192,s268,s178]) ).
cnf(s664,plain,
( spl14_45
| spl14_93
| spl14_58
| spl14_35
| spl14_47
| spl14_37
| spl14_61
| spl14_71
| ~ spl14_40
| spl14_67 ),
inference(rat,[],[s662,s105,s32]) ).
cnf(s665,plain,
( spl14_16
| spl14_27
| spl14_12
| ~ spl14_40
| spl14_18
| spl14_44
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s92,s264,s262,s650,s96,s663,s192,s266,s664,s150,s84,s48,s131,s623,s496,s36,s25,s49,s61,s534,s618,s624,s121,s57]) ).
cnf(s666,plain,
( ~ spl14_16
| spl14_57
| spl14_44
| spl14_9
| spl14_7 ),
inference(rat,[],[s242,s110,s112,s157,s484,s108,s171,s174,s227,s78,s276]) ).
cnf(s667,plain,
( spl14_61
| spl14_71
| ~ spl14_65
| spl14_59
| spl14_94
| spl14_93
| spl14_98
| spl14_35
| spl14_47
| spl14_37
| spl14_16
| ~ spl14_40
| spl14_34
| spl14_67
| spl14_9
| spl14_4 ),
inference(rat,[],[s33,s72,s227,s162,s112,s115,s256,s385,s113,s86,s186,s241,s551,s94,s178,s60,s103,s296,s326,s111,s97,s176,s266,s530,s664,s64,s52,s28,s45,s594,s38,s593,s47,s242,s211,s629]) ).
cnf(s668,plain,
( ~ spl14_63
| spl14_93
| spl14_98
| spl14_35
| spl14_9 ),
inference(rat,[],[s338,s105,s111,s176,s324]) ).
cnf(s669,plain,
( ~ spl14_65
| spl14_59
| spl14_94
| spl14_93
| spl14_98
| spl14_35
| spl14_47
| spl14_37
| spl14_16
| ~ spl14_40
| spl14_34
| spl14_67
| spl14_9
| spl14_4 ),
inference(rat,[],[s325,s103,s97,s178,s221,s94,s186,s63,s667,s211,s242,s51,s668]) ).
cnf(s670,plain,
( spl14_85
| spl14_99
| spl14_65
| spl14_63
| spl14_50
| spl14_16
| spl14_18 ),
inference(rat,[],[s86,s114,s186,s336,s94,s101]) ).
cnf(s671,plain,
( ~ spl14_45
| spl14_35
| spl14_16
| spl14_34
| spl14_18
| spl14_44
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s116,s234,s487,s118,s600,s336,s88,s97,s620,s494,s96,s103,s178,s670,s296,s337,s338,s533,s111,s266,s530,s297,s668,s631,s669,s204,s328,s104,s229,s150,s185,s84,s131,s36,s601,s77,s27,s436,s665,s632,s126,s57]) ).
cnf(s672,plain,
( spl14_35
| spl14_16
| spl14_34
| spl14_18
| spl14_44
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s221,s94,s90,s186,s365,s63,s664,s671,s51,s668,s47,s204,s104,s150,s185,s84,s131,s57,s27,s436,s229,s36,s601,s77,s665,s632,s126]) ).
cnf(s673,plain,
( ~ spl14_56
| spl14_83
| spl14_87
| spl14_18
| spl14_4 ),
inference(rat,[],[s297,s102,s104,s159,s193]) ).
cnf(s674,plain,
( spl14_28
| spl14_61
| spl14_71
| spl14_56
| spl14_43
| spl14_81
| spl14_90
| spl14_47
| spl14_83
| spl14_37
| spl14_51
| spl14_55
| spl14_39
| spl14_64
| spl14_74
| spl14_18
| spl14_67
| spl14_9 ),
inference(rat,[],[s102,s357,s185,s47,s111,s645,s337,s60,s107,s615]) ).
cnf(s675,plain,
( ~ spl14_78
| ~ spl14_49
| ~ spl14_76 ),
inference(rat,[],[s475,s117,s115,s220,s484,s297,s204,s551,s306]) ).
cnf(s676,plain,
( spl14_78
| spl14_58
| spl14_37
| spl14_71
| spl14_39
| spl14_51
| spl14_43
| spl14_55
| spl14_47
| spl14_64
| spl14_67
| spl14_68
| spl14_61
| spl14_74 ),
inference(rat,[],[s69,s75,s629]) ).
cnf(s677,plain,
( spl14_61
| spl14_71
| spl14_43
| spl14_81
| spl14_90
| spl14_47
| spl14_83
| spl14_87
| spl14_37
| spl14_51
| spl14_55
| spl14_39
| spl14_64
| spl14_74
| spl14_18
| spl14_67
| spl14_9
| spl14_4 ),
inference(rat,[],[s186,s117,s86,s483,s113,s675,s220,s256,s676,s60,s47,s296,s204,s297,s328,s111,s104,s185,s84,s674,s673]) ).
cnf(s678,plain,
( ~ spl14_62
| spl14_97
| spl14_87
| spl14_57
| spl14_9
| spl14_4 ),
inference(rat,[],[s186,s117,s86,s483,s113,s675,s297,s328,s104,s185,s84,s108,s220,s256,s484,s112,s402,s492]) ).
cnf(s679,plain,
( spl14_18
| ~ spl14_10
| spl14_9
| spl14_7
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s62,s225,s677,s93,s50,s678,s32,s172,s176,s322,s324,s23,s83,s672,s36,s601,s223,s229,s27,s77,s436,s665,s666,s38,s45,s28,s52,s64,s593,s594,s632,s126,s661,s57,s660]) ).
cnf(s680,plain,
( spl14_9
| spl14_7
| spl14_1
| spl14_2
| spl14_5
| spl14_4
| spl14_3 ),
inference(rat,[],[s598,s95,s162,s184,s294,s227,s76,s78,s141,s575,s615,s658,s11,s322,s324,s302,s83,s655,s131,s654,s156,s369,s471,s527,s81,s536,s679,s57,s660,s659]) ).
cnf(s681,plain,
( ~ spl14_42
| spl14_18
| ~ spl14_9
| spl14_4 ),
inference(rat,[],[s297,s102,s104,s150,s514,s105,s192,s107,s673,s223,s229,s437,s383,s179,s165,s85]) ).
cnf(s682,plain,
( ~ spl14_10
| spl14_55
| spl14_64
| spl14_74
| spl14_52
| spl14_34
| spl14_58
| spl14_37
| spl14_51
| spl14_61
| spl14_71
| spl14_50
| spl14_42
| ~ spl14_9 ),
inference(rat,[],[s59,s151,s71,s106,s32,s171,s192,s91,s107,s191,s371,s120,s98,s326,s328,s114,s519,s87,s487,s4,s181,s393,s437,s383,s57,s448,s296,s179,s165,s85,s77,s30,s36,s629]) ).
cnf(s683,plain,
( ~ spl14_63
| ~ spl14_9 ),
inference(rat,[],[s370,s105,s107,s176,s322,s437,s383,s179,s165,s85]) ).
cnf(s684,plain,
( ~ spl14_36
| ~ spl14_79
| ~ spl14_9 ),
inference(rat,[],[s6,s342,s381]) ).
cnf(s685,plain,
( ~ spl14_68
| spl14_30
| spl14_57
| ~ spl14_9 ),
inference(rat,[],[s684,s136,s108,s88,s157,s220,s58,s59,s437]) ).
cnf(s686,plain,
( spl14_34
| spl14_16
| spl14_18
| ~ spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s239,s93,s95,s174,s227,s33,s645,s685,s191,s234,s116,s339,s682,s45,s52,s64,s593,s594,s126,s57,s448,s296,s165,s85,s51,s683,s30,s61,s37,s25,s36,s624,s48,s623,s534,s121,s77,s681]) ).
cnf(s687,plain,
( spl14_16
| spl14_18
| ~ spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s325,s114,s103,s86,s242,s186,s670,s94,s264,s268,s80,s686,s624,s179,s85,s683,s77,s681]) ).
cnf(s689,plain,
( spl14_45
| spl14_83
| spl14_68
| spl14_71
| spl14_47
| spl14_51
| spl14_55
| spl14_64
| spl14_74
| spl14_37
| spl14_39
| spl14_18
| ~ spl14_9 ),
inference(rat,[],[s357,s102,s47,s150,s645,s105,s32,s383,s57,s448,s296,s179,s85,s51,s683]) ).
cnf(s690,plain,
( spl14_18
| ~ spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s103,s268,s326,s92,s97,s192,s530,s689,s211,s242,s239,s110,s59,s95,s62,s36,s157,s191,s240,s38,s45,s108,s91,s52,s64,s593,s594,s171,s174,s227,s27,s126,s275,s78,s141,s163,s687,s30,s77,s681,s448,s437]) ).
cnf(s691,plain,
( spl14_16
| spl14_74
| spl14_64
| spl14_58
| spl14_91
| spl14_97
| spl14_34
| spl14_94
| spl14_27
| spl14_85
| spl14_63
| spl14_99
| spl14_77
| spl14_67
| spl14_35
| spl14_4
| spl14_1 ),
inference(rat,[],[s44,s371,s645,s105,s32,s59,s663,s151,s103,s113,s326,s86,s97,s29,s186,s551,s36,s25,s37,s61,s534,s94,s624,s121,s51]) ).
cnf(s692,plain,
( ~ spl14_9
| spl14_6
| spl14_5
| spl14_4
| spl14_3
| spl14_2
| spl14_1 ),
inference(rat,[],[s32,s645,s192,s44,s92,s371,s268,s98,s38,s103,s29,s229,s367,s326,s583,s95,s114,s113,s191,s240,s63,s151,s116,s600,s110,s34,s58,s162,s294,s174,s227,s76,s27,s275,s78,s141,s691,s88,s620,s655,s53,s48,s156,s369,s498,s588,s288,s509,s527,s81,s359,s536,s578,s579,s690,s51,s683,s165,s179,s296,s57,s85,s383,s448]) ).
cnf(s693,plain,
( spl14_16
| spl14_44
| spl14_34
| spl14_18
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s62,s225,s677,s93,s50,s36,s678,s172,s32,s601,s223,s229,s23,s27,s176,s322,s324,s77,s377,s436,s83,s665,s672,s632,s64,s52,s28,s45,s594,s38,s593,s126,s57]) ).
cnf(s694,plain,
( spl14_18
| ~ spl14_7
| spl14_9
| spl14_5
| spl14_4
| spl14_3
| spl14_1 ),
inference(rat,[],[s262,s92,s96,s192,s266,s664,s47,s355,s98,s229,s95,s62,s36,s191,s240,s150,s91,s50,s237,s313,s84,s171,s174,s227,s27,s131,s9,s78,s140,s141,s308,s693,s57,s612,s593,s632,s126,s661]) ).
cnf(s695,plain,
( spl14_9
| spl14_5
| spl14_1
| spl14_2
| spl14_3
| spl14_4 ),
inference(rat,[],[s658,s308,s302,s657,s655,s654,s156,s369,s498,s57,s527,s81,s301,s536,s694,s680]) ).
cnf(s696,plain,
( spl14_5
| spl14_4
| spl14_1
| spl14_2
| spl14_3 ),
inference(rat,[],[s8,s359,s692,s690,s695]) ).
cnf(s697,plain,
( ~ spl14_76
| ~ spl14_102 ),
inference(rat,[],[s86,s113,s186,s551,s117,s297,s328,s385,s157,s88,s484]) ).
cnf(s698,plain,
( spl14_18
| spl14_9
| ~ spl14_5
| spl14_4
| spl14_3 ),
inference(rat,[],[s62,s649,s191,s240,s91,s38,s367,s104,s697,s31,s55,s110,s628,s53,s242,s112,s157,s484,s108,s50,s171,s174,s227,s27,s637,s523,s78,s141,s237,s264,s268,s21,s167,s520,s80,s126,s481]) ).
cnf(s699,plain,
( spl14_55
| ~ spl14_44
| spl14_37
| spl14_43
| spl14_61
| spl14_51
| spl14_39
| spl14_47
| spl14_64
| spl14_58
| spl14_71
| spl14_74
| spl14_68
| spl14_67 ),
inference(rat,[],[s595,s70,s629]) ).
cnf(s700,plain,
( spl14_67
| spl14_34
| spl14_16
| spl14_27
| ~ spl14_18
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s699,s60,s43,s565,s657,s302,s658,s48,s588,s53,s156,s61,s49,s37,s25,s36,s624,s29,s65,s32,s663,s103,s326,s97,s369,s534,s121,s498,s81]) ).
cnf(s701,plain,
~ spl14_67,
inference(rat,[],[s55,s57]) ).
cnf(s702,plain,
( spl14_16
| spl14_27
| ~ spl14_18
| spl14_9
| ~ spl14_5
| spl14_4
| spl14_1 ),
inference(rat,[],[s700,s520,s701]) ).
cnf(s703,plain,
( ~ spl14_42
| spl14_88
| spl14_79
| spl14_27
| spl14_1 ),
inference(rat,[],[s191,s91,s95,s146,s229]) ).
cnf(s704,plain,
( ~ spl14_53
| spl14_34
| ~ spl14_57
| spl14_4 ),
inference(rat,[],[s325,s97,s103,s147,s268,s498,s369]) ).
cnf(s705,plain,
( ~ spl14_50
| spl14_88
| spl14_79
| spl14_27
| spl14_1 ),
inference(rat,[],[s366,s91,s95,s240,s300]) ).
cnf(s706,plain,
( ~ spl14_36
| spl14_69
| spl14_96 ),
inference(rat,[],[s186,s117,s86,s483]) ).
cnf(s707,plain,
( ~ spl14_76
| spl14_36
| ~ spl14_78 ),
inference(rat,[],[s113,s675,s328,s256]) ).
cnf(s708,plain,
( ~ spl14_73
| spl14_30
| spl14_36
| spl14_100
| spl14_102 ),
inference(rat,[],[s355,s115,s113,s262,s365]) ).
cnf(s709,plain,
( spl14_9
| spl14_4
| spl14_3
| spl14_2
| spl14_1 ),
inference(rat,[],[s104,s523,s21,s367,s704,s38,s39,s699,s63,s708,s66,s87,s707,s706,s36,s705,s30,s703,s31,s43,s110,s59,s220,s256,s484,s50,s112,s174,s227,s27,s78,s141,s702,s53,s48,s156,s498,s587,s588,s527,s81,s579,s698,s696,s701]) ).
cnf(s710,plain,
( spl14_4
| spl14_3
| spl14_1
| spl14_2 ),
inference(rat,[],[s242,s103,s101,s326,s336,s114,s264,s268,s705,s294,s80,s171,s227,s76,s126,s78,s141,s77,s481,s687,s681,s179,s359,s85,s448,s709,s289,s696]) ).
cnf(s711,plain,
( ~ spl14_76
| ~ spl14_42
| ~ spl14_4 ),
inference(rat,[],[s158,s100,s102,s204,s297,s145,s139,s223,s146]) ).
cnf(s712,plain,
( ~ spl14_66
| spl14_49
| spl14_77
| spl14_36
| spl14_52
| spl14_44
| spl14_9
| ~ spl14_4 ),
inference(rat,[],[s14,s441,s208,s131,s113,s83,s355,s324,s100,s111,s159,s185,s145]) ).
cnf(s713,plain,
( spl14_66
| ~ spl14_99
| spl14_44
| spl14_9 ),
inference(rat,[],[s193,s107,s111,s322,s324,s109,s84,s338,s334,s179]) ).
cnf(s714,plain,
( ~ spl14_27
| spl14_71
| spl14_37
| spl14_21
| spl14_44
| spl14_16
| spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s53,s211,s645,s97,s29,s583,s712,s713,s33,s50,s227,s492,s95,s598,s179,s338,s114,s38,s34,s46,s58,s162,s294,s601,s146,s229,s76,s77,s436,s149,s145,s161,s45,s588,s65,s295,s82,s701]) ).
cnf(s715,plain,
( spl14_36
| spl14_58
| spl14_30
| spl14_43
| spl14_64
| spl14_39
| spl14_51
| spl14_61
| spl14_50
| spl14_71
| spl14_37
| spl14_21
| ~ spl14_60 ),
inference(rat,[],[s645,s58,s338,s136,s114,s161,s45,s588,s65,s295,s36,s701]) ).
cnf(s716,plain,
( spl14_58
| spl14_30
| spl14_43
| spl14_53
| spl14_64
| spl14_39
| spl14_51
| spl14_61
| spl14_50
| spl14_27
| spl14_71
| spl14_37
| spl14_21
| spl14_44
| spl14_9
| ~ spl14_60 ),
inference(rat,[],[s60,s71,s179,s338,s105,s150,s84,s131,s83,s192,s322,s92,s262,s86,s294,s715,s45,s588,s65,s295,s36,s629,s701]) ).
cnf(s717,plain,
( ~ spl14_42
| spl14_43
| spl14_53
| spl14_64
| spl14_97
| spl14_39
| spl14_51
| spl14_61
| spl14_50
| spl14_27
| spl14_71
| spl14_37
| spl14_21
| spl14_44
| spl14_16
| spl14_9
| ~ spl14_4 ),
inference(rat,[],[s234,s93,s91,s492,s517,s112,s220,s706,s136,s357,s46,s47,s716,s87,s711,s146,s223,s82]) ).
cnf(s718,plain,
( spl14_58
| spl14_43
| spl14_53
| spl14_64
| spl14_39
| spl14_51
| spl14_61
| spl14_50
| spl14_27
| spl14_71
| spl14_37
| spl14_21
| spl14_44
| spl14_9
| ~ spl14_60 ),
inference(rat,[],[s60,s676,s179,s707,s114,s87,s487,s716,s161,s45,s588,s65,s295,s36,s701]) ).
cnf(s719,plain,
( spl14_43
| spl14_53
| spl14_64
| spl14_97
| spl14_39
| spl14_51
| spl14_61
| spl14_50
| spl14_27
| spl14_71
| spl14_37
| spl14_21
| spl14_44
| spl14_16
| spl14_9
| ~ spl14_4 ),
inference(rat,[],[s321,s92,s83,s262,s131,s86,s84,s136,s150,s87,s98,s204,s355,s46,s47,s718,s717,s149,s82]) ).
cnf(s720,plain,
( spl14_71
| spl14_37
| spl14_21
| spl14_44
| spl14_16
| spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s219,s110,s112,s174,s227,s33,s719,s264,s101,s53,s211,s494,s97,s29,s37,s49,s534,s624,s121,s714,s149,s139,s177,s161,s82]) ).
cnf(s721,plain,
( ~ spl14_71
| spl14_21
| spl14_44
| ~ spl14_4 ),
inference(rat,[],[s114,s179,s294,s118,s76,s225,s300,s61,s62,s145,s177,s161,s82]) ).
cnf(s722,plain,
~ spl14_37,
inference(rat,[],[s25,s27]) ).
cnf(s723,plain,
( spl14_21
| spl14_16
| spl14_44
| spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s720,s721,s722]) ).
cnf(s724,plain,
( spl14_16
| spl14_44
| spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s47,s355,s71,s98,s33,s703,s174,s402,s492,s338,s110,s53,s114,s36,s211,s624,s97,s29,s561,s59,s37,s49,s61,s436,s534,s2,s220,s76,s406,s88,s184,s483,s723,s149,s145,s161,s45,s588,s65,s295,s82,s722,s629,s701]) ).
cnf(s725,plain,
( spl14_44
| spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s366,s91,s95,s234,s598,s118,s179,s114,s705,s162,s184,s294,s171,s227,s76,s78,s140,s141,s724,s145,s177,s161,s82]) ).
cnf(s726,plain,
( ~ spl14_69
| spl14_97
| spl14_28
| spl14_9
| spl14_57 ),
inference(rat,[],[s516,s108,s112,s157,s220]) ).
cnf(s727,plain,
( spl14_72
| spl14_50
| spl14_69
| spl14_39
| spl14_51
| spl14_61
| spl14_64
| ~ spl14_44
| ~ spl14_60 ),
inference(rat,[],[s706,s114,s357,s338,s47,s120,s699,s595,s62,s161,s45,s588,s65,s295,s31,s60,s565,s36,s722,s701,s629]) ).
cnf(s728,plain,
( spl14_50
| spl14_16
| spl14_69
| spl14_39
| spl14_51
| spl14_64
| spl14_62
| ~ spl14_44
| ~ spl14_4 ),
inference(rat,[],[s47,s355,s699,s98,s63,s561,s708,s2,s256,s484,s223,s406,s88,s475,s483,s93,s118,s225,s727,s36,s149,s177,s45,s588,s65,s295,s82,s31,s60,s565,s50,s722,s701]) ).
cnf(s729,plain,
( ~ spl14_50
| spl14_16
| spl14_1 ),
inference(rat,[],[s77,s601,s624]) ).
cnf(s730,plain,
( spl14_16
| spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s729,s728,s605,s513,s53,s39,s264,s29,s726,s494,s97,s221,s101,s627,s177,s139,s161,s149,s459,s725,s588,s82]) ).
cnf(s731,plain,
( spl14_9
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s484,s108,s112,s171,s227,s78,s730,s494,s97,s221,s101,s627,s459,s725,s149,s139,s588,s177,s161,s82]) ).
cnf(s732,plain,
( spl14_16
| ~ spl14_4
| spl14_1 ),
inference(rat,[],[s689,s192,s53,s92,s244,s211,s264,s91,s97,s29,s94,s191,s37,s436,s534,s186,s262,s120,s76,s721,s685,s684,s86,s294,s483,s487,s114,s36,s729,s149,s145,s139,s161,s45,s588,s65,s295,s82,s448,s683,s296,s179,s85,s731,s722]) ).
cnf(s733,plain,
( ~ spl14_4
| spl14_1 ),
inference(rat,[],[s114,s705,s294,s171,s227,s76,s78,s140,s141,s732,s179,s85,s448,s731,s161,s82,s145]) ).
cnf(s734,plain,
( ~ spl14_27
| spl14_16
| spl14_44
| spl14_9
| spl14_2
| spl14_1 ),
inference(rat,[],[s185,s104,s102,s204,s357,s100,s255,s673,s693,s146,s223,s229,s527,s77,s733]) ).
cnf(s735,plain,
( ~ spl14_92
| spl14_85
| spl14_89
| spl14_18
| spl14_4 ),
inference(rat,[],[s242,s103,s101,s326,s336]) ).
cnf(s736,plain,
( ~ spl14_74
| spl14_5
| ~ spl14_34
| spl14_18
| spl14_44
| spl14_9
| spl14_4 ),
inference(rat,[],[s648,s635]) ).
cnf(s737,plain,
( spl14_18
| spl14_36
| spl14_51
| spl14_61
| spl14_71
| spl14_16
| spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s115,s355,s87,s113,s707,s256,s484,s112,s242,s53,s649,s736,s202,s17,s257,s241,s551,s131,s94,s83,s324,s111,s185,s713,s338,s114,s735,s32,s650,s264,s268,s520,s80,s693,s733,s729,s722,s701]) ).
cnf(s738,plain,
( ~ spl14_18
| spl14_27
| spl14_1
| spl14_16
| spl14_9
| spl14_4 ),
inference(rat,[],[s654,s702,s700,s701]) ).
cnf(s739,plain,
( spl14_16
| spl14_44
| spl14_9
| spl14_2
| spl14_1 ),
inference(rat,[],[s533,s103,s111,s242,s185,s53,s54,s636,s324,s32,s639,s45,s94,s650,s637,s186,s736,s264,s268,s86,s294,s48,s520,s80,s737,s623,s693,s738,s29,s37,s49,s61,s534,s121,s734,s729,s733,s722,s701]) ).
cnf(s740,plain,
( spl14_34
| spl14_58
| spl14_18
| spl14_89
| spl14_47
| spl14_42
| spl14_79
| spl14_62
| spl14_27
| spl14_35
| spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s110,s242,s157,s103,s115,s533,s262,s111,s96,s266,s664,s62,s191,s87,s91,s328,s355,s593,s98,s126,s733,s50,s185,s150,s84,s131,s722,s701]) ).
cnf(s741,plain,
( spl14_18
| spl14_89
| spl14_41
| spl14_79
| spl14_62
| spl14_88
| spl14_27
| spl14_38
| spl14_35
| spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s53,s242,s649,s103,s65,s38,s384,s367,s118,s32,s95,s62,s234,s266,s598,s116,s111,s179,s334,s338,s114,s735,s162,s184,s294,s264,s76,s80,s255,s740,s48,s623,s733,s50,s703,s185,s84,s131,s36,s705,s722,s701]) ).
cnf(s742,plain,
( spl14_44
| spl14_9
| spl14_2
| spl14_1 ),
inference(rat,[],[s704,s190,s125,s198,s81,s578,s741,s313,s9,s319,s276,s171,s174,s227,s131,s78,s140,s141,s311,s739,s710,s733]) ).
cnf(s743,plain,
( ~ spl14_40
| spl14_18
| spl14_16
| ~ spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s222,s77,s93,s121,s225,s61,s62,s699,s50,s38,s605,s28,s593,s594,s513,s459,s43,s31,s60,s565,s53,s36,s729,s628,s48,s631,s627,s733,s722,s701]) ).
cnf(s744,plain,
( ~ spl14_27
| spl14_61
| spl14_45
| ~ spl14_34
| spl14_74
| spl14_18
| spl14_50
| spl14_64
| spl14_43
| spl14_9
| spl14_4 ),
inference(rat,[],[s649,s63,s38,s365,s146,s90,s77,s436,s147,s80,s722,s701]) ).
cnf(s745,plain,
( spl14_18
| spl14_16
| ~ spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s699,s37,s61,s121,s744,s50,s605,s29,s637,s650,s147,s264,s268,s80,s126,s743,s48,s631,s628,s733,s513,s459,s43,s31,s60,s565,s53,s627,s36,s729,s722,s701]) ).
cnf(s746,plain,
( spl14_16
| spl14_9
| spl14_2
| spl14_1 ),
inference(rat,[],[s738,s527,s745,s733,s742]) ).
cnf(s747,plain,
( spl14_52
| spl14_58
| spl14_74
| spl14_39
| spl14_47
| spl14_61
| spl14_79
| spl14_27
| spl14_64
| ~ spl14_44 ),
inference(rat,[],[s62,s191,s699,s91,s38,s43,s31,s60,s565,s722,s701]) ).
cnf(s748,plain,
( spl14_18
| spl14_39
| spl14_47
| ~ spl14_16
| spl14_65
| ~ spl14_44
| spl14_4 ),
inference(rat,[],[s108,s697,s637,s104,s264,s268,s523,s21,s163,s80,s126,s367,s593,s747,s48,s631,s628,s459,s53,s140,s171,s50,s174,s78]) ).
cnf(s749,plain,
( spl14_9
| spl14_2
| spl14_1 ),
inference(rat,[],[s21,s704,s532,s39,s104,s699,s367,s63,s747,s708,s66,s87,s707,s706,s220,s256,s484,s112,s48,s498,s588,s81,s301,s579,s748,s30,s36,s703,s705,s50,s171,s174,s227,s78,s140,s746,s53,s60,s627,s31,s43,s565,s742,s733,s722,s701]) ).
cnf(s750,plain,
( spl14_16
| spl14_2
| spl14_1 ),
inference(rat,[],[s691,s53,s48,s655,s156,s369,s498,s588,s594,s509,s8,s288,s527,s81,s359,s578,s687,s733,s448,s383,s683,s296,s179,s85,s749,s701]) ).
cnf(s751,plain,
( spl14_4
| spl14_2
| spl14_1 ),
inference(rat,[],[s7,s138,s750,s749,s710]) ).
cnf(s752,plain,
( spl14_18
| spl14_44
| spl14_16
| spl14_9
| spl14_1 ),
inference(rat,[],[s185,s104,s102,s204,s357,s100,s255,s673,s693,s229,s223,s146,s77,s121,s535,s751,s733]) ).
cnf(s753,plain,
( spl14_44
| spl14_16
| spl14_9
| spl14_1 ),
inference(rat,[],[s676,s644,s29,s44,s581,s193,s114,s111,s220,s334,s337,s110,s50,s116,s492,s234,s95,s62,s118,s598,s32,s615,s471,s176,s322,s377,s83,s58,s162,s184,s294,s657,s53,s48,s76,s156,s369,s498,s588,s594,s528,s81,s577,s579,s752,s36,s729,s15,s229,s38,s146,s77,s121,s535,s751,s733,s722,s701]) ).
cnf(s754,plain,
( ~ spl14_80
| spl14_16
| spl14_1 ),
inference(rat,[],[s491,s95,s93,s191,s234,s229,s223,s77,s121,s535,s751,s733]) ).
cnf(s755,plain,
( ~ spl14_41
| spl14_80
| spl14_60
| spl14_40
| spl14_90
| spl14_95
| spl14_35
| spl14_52
| spl14_9 ),
inference(rat,[],[s87,s116,s204,s334,s100,s105,s193,s514,s111,s533,s128,s530,s581]) ).
cnf(s756,plain,
( ~ spl14_62
| spl14_91
| spl14_97
| spl14_35
| spl14_9 ),
inference(rat,[],[s256,s106,s112,s174,s492]) ).
cnf(s757,plain,
( spl14_16
| spl14_9
| spl14_1 ),
inference(rat,[],[s699,s65,s62,s225,s93,s50,s756,s326,s97,s29,s755,s754,s48,s369,s498,s588,s594,s520,s528,s81,s301,s577,s53,s60,s745,s627,s31,s43,s513,s565,s753,s38,s146,s223,s15,s77,s36,s121,s729,s535,s751,s733,s722,s701]) ).
cnf(s758,plain,
( ~ spl14_40
| spl14_18
| spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s741,s313,s319,s131,s9,s308,s694,s666,s481,s594,s733,s141,s140,s227,s174,s171,s78,s757]) ).
cnf(s759,plain,
( spl14_18
| spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s311,s741,s698,s147,s268,s163,s80,s126,s758,s733,s141,s140,s227,s174,s171,s78,s757]) ).
cnf(s760,plain,
( spl14_44
| spl14_9
| spl14_1 ),
inference(rat,[],[s219,s110,s112,s156,s498,s81,s759,s227,s174,s78,s757]) ).
cnf(s761,plain,
( spl14_9
| spl14_1 ),
inference(rat,[],[s21,s704,s532,s39,s104,s699,s367,s63,s747,s708,s66,s87,s707,s706,s220,s256,s484,s112,s48,s498,s588,s81,s301,s579,s748,s53,s60,s627,s31,s43,s565,s760,s30,s36,s703,s705,s50,s171,s174,s227,s78,s140,s757,s733,s722,s701]) ).
cnf(s762,plain,
( spl14_16
| spl14_1 ),
inference(rat,[],[s162,s116,s76,s588,s594,s81,s754,s687,s535,s751,s733,s448,s165,s85,s761]) ).
cnf(s763,plain,
( spl14_18
| spl14_1 ),
inference(rat,[],[s735,s114,s264,s268,s294,s80,s76,s126,s481,s690,s733,s448,s179,s85,s141,s7,s138,s761,s705,s171,s227,s78,s140,s762]) ).
cnf(s764,plain,
spl14_1,
inference(rat,[],[s63,s676,s32,s600,s44,s192,s58,s184,s294,s371,s92,s39,s53,s620,s48,s76,s98,s704,s655,s156,s369,s588,s594,s509,s8,s288,s81,s359,s579,s763,s30,s36,s703,s705,s275,s171,s227,s7,s78,s138,s140,s141,s762,s51,s683,s383,s448,s761,s733,s722,s701]) ).
cnf(s765,plain,
~ spl14_27,
inference(rat,[],[s474,s764]) ).
cnf(s766,plain,
~ spl14_38,
inference(rat,[],[s466,s764]) ).
cnf(s767,plain,
~ spl14_16,
inference(rat,[],[s246,s764]) ).
cnf(s768,plain,
spl14_50,
inference(rat,[],[s79,s764]) ).
cnf(s769,plain,
~ spl14_72,
inference(rat,[],[s300,s768]) ).
cnf(s770,plain,
~ spl14_80,
inference(rat,[],[s240,s768]) ).
cnf(s771,plain,
~ spl14_84,
inference(rat,[],[s210,s768]) ).
cnf(s772,plain,
~ spl14_71,
inference(rat,[],[s62,s769]) ).
cnf(s773,plain,
( ~ spl14_30
| ~ spl14_78 ),
inference(rat,[],[s707,s87,s487]) ).
cnf(s774,plain,
( spl14_60
| spl14_30
| spl14_81
| spl14_90
| spl14_102
| spl14_42
| spl14_43
| spl14_61
| spl14_51
| spl14_39
| spl14_64
| spl14_74
| spl14_34
| spl14_9 ),
inference(rat,[],[s115,s355,s306,s98,s35,s514,s646,s111,s337,s116,s48,s722,s772,s701,s770]) ).
cnf(s775,plain,
( ~ spl14_65
| spl14_42
| spl14_87
| spl14_61
| spl14_46
| spl14_88
| spl14_51
| spl14_39
| spl14_64
| spl14_74
| spl14_34
| spl14_4
| spl14_9 ),
inference(rat,[],[s107,s193,s337,s104,s120,s707,s184,s483,s118,s177,s295,s774,s773,s615,s195,s322,s324,s511,s83,s106,s256,s484,s112,s211,s242,s33,s769,s771,s764]) ).
cnf(s776,plain,
( spl14_34
| spl14_4
| spl14_18
| spl14_44
| spl14_9 ),
inference(rat,[],[s583,s97,s35,s336,s676,s118,s60,s615,s195,s322,s324,s511,s83,s106,s494,s112,s88,s48,s151,s220,s631,s110,s775,s223,s239,s33,s93,s50,s171,s402,s517,s91,s38,s45,s28,s52,s64,s593,s594,s126,s722,s701,s772,s771,s764,s767,s765,s770]) ).
cnf(s777,plain,
( ~ spl14_66
| ~ spl14_101
| spl14_9 ),
inference(rat,[],[s105,s83,s266,s324,s111,s150,s185,s337,s334]) ).
cnf(s778,plain,
( spl14_4
| spl14_18
| spl14_9
| spl14_44 ),
inference(rat,[],[s50,s402,s645,s32,s91,s38,s176,s244,s109,s102,s777,s53,s242,s103,s384,s118,s165,s337,s45,s116,s502,s623,s29,s637,s34,s46,s58,s162,s184,s736,s19,s147,s264,s268,s76,s520,s399,s80,s255,s776,s767,s766,s764,s771,s770,s765,s772,s722,s701]) ).
cnf(s779,plain,
( ~ spl14_53
| spl14_92
| spl14_95
| spl14_34
| spl14_18 ),
inference(rat,[],[s211,s97,s101,s147,s264]) ).
cnf(s780,plain,
( ~ spl14_63
| ~ spl14_70
| spl14_9 ),
inference(rat,[],[s84,s185,s615,s111,s322,s324,s296]) ).
cnf(s782,plain,
( ~ spl14_70
| spl14_44
| spl14_9 ),
inference(rat,[],[s265,s105,s111,s150,s185,s84,s131,s83,s780,s179,s296]) ).
cnf(s783,plain,
( ~ spl14_4
| spl14_70
| spl14_44 ),
inference(rat,[],[s118,s184,s177,s76,s82,s145,s771,s766]) ).
cnf(s784,plain,
( spl14_44
| spl14_9 ),
inference(rat,[],[s76,s184,s594,s118,s81,s577,s778,s783,s782,s771,s766]) ).
cnf(s785,plain,
( spl14_95
| ~ spl14_40
| spl14_4
| spl14_18
| spl14_9 ),
inference(rat,[],[s105,s514,s192,s104,s334,s92,s707,s116,s264,s88,s475,s101,s118,s239,s93,s306,s86,s365,s35,s699,s50,s605,s594,s459,s513,s31,s60,s565,s53,s48,s631,s28,s628,s627,s38,s593,s43,s784,s765,s770,s771,s701,s772,s722,s767]) ).
cnf(s786,plain,
( spl14_34
| spl14_4
| spl14_18
| spl14_9 ),
inference(rat,[],[s773,s112,s116,s494,s337,s97,s120,s336,s384,s785,s583,s35,s699,s517,s595,s50,s91,s38,s605,s28,s593,s594,s126,s513,s459,s43,s31,s60,s565,s53,s628,s48,s631,s627,s784,s770,s769,s722,s772,s701,s629,s765]) ).
cnf(s787,plain,
( spl14_4
| spl14_18
| spl14_9 ),
inference(rat,[],[s117,s88,s151,s256,s551,s106,s35,s171,s699,s91,s38,s494,s244,s103,s93,s50,s384,s605,s502,s29,s101,s637,s19,s147,s264,s268,s399,s80,s786,s48,s628,s631,s513,s459,s43,s31,s60,s565,s53,s627,s784,s722,s772,s701,s765,s770,s767,s771,s764]) ).
cnf(s788,plain,
( spl14_18
| spl14_9 ),
inference(rat,[],[s35,s67,s306,s47,s92,s355,s192,s98,s105,s561,s338,s29,s2,s120,s223,s39,s221,s406,s184,s93,s50,s779,s101,s118,s65,s605,s161,s177,s295,s588,s82,s149,s787,s513,s459,s43,s31,s60,s565,s53,s627,s784,s722,s772,s629,s701,s765,s769,s767,s771]) ).
cnf(s789,plain,
spl14_9,
inference(rat,[],[s756,s369,s498,s93,s81,s576,s788,s513,s784,s767,s771]) ).
cnf(s790,plain,
~ spl14_44,
inference(rat,[],[s448,s789]) ).
cnf(s791,plain,
~ spl14_28,
inference(rat,[],[s437,s789]) ).
cnf(s792,plain,
~ spl14_35,
inference(rat,[],[s383,s789]) ).
cnf(s793,plain,
spl14_70,
inference(rat,[],[s85,s789]) ).
cnf(s794,plain,
~ spl14_63,
inference(rat,[],[s683,s789]) ).
cnf(s795,plain,
~ spl14_77,
inference(rat,[],[s296,s793]) ).
cnf(s796,plain,
~ spl14_99,
inference(rat,[],[s179,s793]) ).
cnf(s797,plain,
~ spl14_101,
inference(rat,[],[s165,s793]) ).
cnf(s798,plain,
~ spl14_61,
inference(rat,[],[s51,s794]) ).
cnf(s799,plain,
( spl14_60
| spl14_39 ),
inference(rat,[],[s71,s59,s35,s151,s583,s106,s33,s97,s171,s38,s45,s519,s108,s326,s52,s64,s255,s593,s594,s4,s697,s120,s76,s339,s87,s162,s116,s48,s722,s772,s795,s629,s701,s798,s792,s789,s791,s769,s790,s766,s770,s797]) ).
cnf(s800,plain,
( spl14_4
| spl14_18 ),
inference(rat,[],[s52,s126,s645,s39,s80,s32,s34,s46,s58,s147,s530,s120,s65,s45,s623,s295,s588,s799,s30,s681,s789,s769,s772,s722,s795,s701,s798]) ).
cnf(s801,plain,
~ spl14_42,
inference(rat,[],[s402,s91,s93,s146,s223,s765,s770,s767,s771]) ).
cnf(s802,plain,
~ spl14_39,
inference(rat,[],[s30,s801]) ).
cnf(s803,plain,
~ spl14_46,
inference(rat,[],[s243,s91,s93,s171,s174,s765,s770,s767,s771]) ).
cnf(s804,plain,
~ spl14_43,
inference(rat,[],[s33,s803]) ).
cnf(s805,plain,
~ spl14_66,
inference(rat,[],[s192,s105,s107,s150,s159,s796,s792,s791,s797]) ).
cnf(s806,plain,
spl14_60,
inference(rat,[],[s799,s802]) ).
cnf(s807,plain,
~ spl14_64,
inference(rat,[],[s54,s805]) ).
cnf(s808,plain,
~ spl14_57,
inference(rat,[],[s588,s806]) ).
cnf(s809,plain,
~ spl14_75,
inference(rat,[],[s295,s806]) ).
cnf(s810,plain,
~ spl14_95,
inference(rat,[],[s177,s806]) ).
cnf(s811,plain,
~ spl14_92,
inference(rat,[],[s161,s806]) ).
cnf(s812,plain,
~ spl14_18,
inference(rat,[],[s81,s808]) ).
cnf(s813,plain,
~ spl14_55,
inference(rat,[],[s45,s808]) ).
cnf(s814,plain,
~ spl14_74,
inference(rat,[],[s65,s809]) ).
cnf(s815,plain,
spl14_48,
inference(rat,[],[s120,s769,s795,s809]) ).
cnf(s816,plain,
spl14_4,
inference(rat,[],[s800,s812]) ).
cnf(s820,plain,
~ spl14_68,
inference(rat,[],[s58,s815]) ).
cnf(s821,plain,
~ spl14_58,
inference(rat,[],[s46,s815]) ).
cnf(s822,plain,
~ spl14_47,
inference(rat,[],[s34,s815]) ).
cnf(s829,plain,
~ spl14_34,
inference(rat,[],[s149,s816]) ).
cnf(s833,plain,
spl14_51,
inference(rat,[],[s645,s772,s814,s722,s807,s804,s802,s820,s813,s795,s701,s798,s822,s821]) ).
cnf(s834,plain,
~ spl14_53,
inference(rat,[],[s779,s812,s811,s810,s829]) ).
cnf(s836,plain,
$false,
inference(rat,[],[s39,s834,s833]) ).
fof(f3514,plain,
$false,
inference(avatar_sat_refutation,[],[s836]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG146+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 % Computer : n015.cluster.edu
% 0.10/0.19 % Model : x86_64 x86_64
% 0.10/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19 % Memory : 8046.5625MB
% 0.10/0.19 % OS : Linux 6.8.0-71-generic
% 0.10/0.19 % CPULimit : 300
% 0.10/0.19 % WCLimit : 300
% 0.10/0.19 % DateTime : Mon Sep 28 19:39:02 UTC 2026
% 0.10/0.19 % CPUTime :
% 0.10/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 Running first-order model finding
% 0.10/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.30 % (2937325)Will run a generic schedule for satisfiability detection.
% 0.21/0.30 % (2937334)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3499330857:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.30 % (2937331)% WARNING: option uhcvi not known.
% 0.21/0.30 % (2937330)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2021482460_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.30 % (2937332)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3661499502:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.30 % (2937331)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1741378033:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.30 % (2937333)dis+10_1_sil=32000:sp=arity:random_seed=968355443:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.30 % (2937336)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2025446250:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.30 % (2937335)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1432600747:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.30 % Detected minimum model sizes of [4]
% 0.21/0.30 % Detected maximum model sizes of [max]
% 0.21/0.30 % TRYING [4]
% 0.21/0.30 % (2937334) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2937325-2937334"...
% 0.21/0.30 % TRYING [5]
% 0.21/0.30 % (2937334)...printing done.
% 0.21/0.30 % (2937334)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Unsatisfiable for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.31 % (2937334)------------------------------
% 0.21/0.31 % (2937334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.31 % (2937334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.31 % (2937334)CaDiCaL version: 2.1.3
% 0.21/0.31 % (2937334)Termination reason: Refutation
% 0.21/0.31 % (2937334)Time elapsed: 0.039 s
% 0.21/0.31 % (2937334)Peak memory usage: 13 MB
% 0.21/0.31 % (2937334)Instructions burned: 135 (million)
% 0.21/0.31 % (2937325)Success in time 0.07 s
% 0.21/0.31 % Vampire exiting
%------------------------------------------------------------------------------