%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG133+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : 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:24:04 AM UTC 2026
% Result : Unsatisfiable 0.20s 0.35s
% Output : Refutation 0.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
fof(f2,axiom,
( ( op(e0,e0) = e0
| op(e0,e1) = e0
| op(e0,e2) = e0
| op(e0,e3) = e0 )
& ( op(e0,e0) = e0
| op(e1,e0) = e0
| op(e2,e0) = e0
| op(e3,e0) = e0 )
& ( op(e0,e0) = e1
| op(e0,e1) = e1
| op(e0,e2) = e1
| op(e0,e3) = e1 )
& ( op(e0,e0) = e1
| op(e1,e0) = e1
| op(e2,e0) = e1
| op(e3,e0) = e1 )
& ( op(e0,e0) = e2
| op(e0,e1) = e2
| op(e0,e2) = e2
| op(e0,e3) = e2 )
& ( op(e0,e0) = e2
| op(e1,e0) = e2
| op(e2,e0) = e2
| op(e3,e0) = e2 )
& ( op(e0,e0) = e3
| op(e0,e1) = e3
| op(e0,e2) = e3
| op(e0,e3) = e3 )
& ( op(e0,e0) = e3
| op(e1,e0) = e3
| op(e2,e0) = e3
| op(e3,e0) = e3 )
& ( op(e1,e0) = e0
| op(e1,e1) = e0
| op(e1,e2) = e0
| op(e1,e3) = e0 )
& ( op(e0,e1) = e0
| op(e1,e1) = e0
| op(e2,e1) = e0
| op(e3,e1) = e0 )
& ( op(e1,e0) = e1
| op(e1,e1) = e1
| op(e1,e2) = e1
| op(e1,e3) = e1 )
& ( op(e0,e1) = e1
| op(e1,e1) = e1
| op(e2,e1) = e1
| op(e3,e1) = e1 )
& ( op(e1,e0) = e2
| op(e1,e1) = e2
| op(e1,e2) = e2
| op(e1,e3) = e2 )
& ( op(e0,e1) = e2
| op(e1,e1) = e2
| op(e2,e1) = e2
| op(e3,e1) = e2 )
& ( op(e1,e0) = e3
| op(e1,e1) = e3
| op(e1,e2) = e3
| op(e1,e3) = e3 )
& ( op(e0,e1) = e3
| op(e1,e1) = e3
| op(e2,e1) = e3
| op(e3,e1) = e3 )
& ( op(e2,e0) = e0
| op(e2,e1) = e0
| op(e2,e2) = e0
| op(e2,e3) = e0 )
& ( op(e0,e2) = e0
| op(e1,e2) = e0
| op(e2,e2) = e0
| op(e3,e2) = e0 )
& ( op(e2,e0) = e1
| op(e2,e1) = e1
| op(e2,e2) = e1
| op(e2,e3) = e1 )
& ( op(e0,e2) = e1
| op(e1,e2) = e1
| op(e2,e2) = e1
| op(e3,e2) = e1 )
& ( op(e2,e0) = e2
| op(e2,e1) = e2
| op(e2,e2) = e2
| op(e2,e3) = e2 )
& ( op(e0,e2) = e2
| op(e1,e2) = e2
| op(e2,e2) = e2
| op(e3,e2) = e2 )
& ( op(e2,e0) = e3
| op(e2,e1) = e3
| op(e2,e2) = e3
| op(e2,e3) = e3 )
& ( op(e0,e2) = e3
| op(e1,e2) = e3
| op(e2,e2) = e3
| op(e3,e2) = e3 )
& ( op(e3,e0) = e0
| op(e3,e1) = e0
| op(e3,e2) = e0
| op(e3,e3) = e0 )
& ( op(e0,e3) = e0
| op(e1,e3) = e0
| op(e2,e3) = e0
| op(e3,e3) = e0 )
& ( op(e3,e0) = e1
| op(e3,e1) = e1
| op(e3,e2) = e1
| op(e3,e3) = e1 )
& ( op(e0,e3) = e1
| op(e1,e3) = e1
| op(e2,e3) = e1
| op(e3,e3) = e1 )
& ( op(e3,e0) = e2
| op(e3,e1) = e2
| op(e3,e2) = e2
| op(e3,e3) = e2 )
& ( op(e0,e3) = e2
| op(e1,e3) = e2
| op(e2,e3) = e2
| op(e3,e3) = e2 )
& ( op(e3,e0) = e3
| op(e3,e1) = e3
| op(e3,e2) = e3
| op(e3,e3) = e3 )
& ( op(e0,e3) = e3
| op(e1,e3) = e3
| op(e2,e3) = e3
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
fof(f3,axiom,
( op(e0,e0) != op(e1,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e1,e0) != op(e3,e0)
& op(e2,e0) != op(e3,e0)
& op(e0,e1) != op(e1,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e1,e1) != op(e3,e1)
& op(e2,e1) != op(e3,e1)
& op(e0,e2) != op(e1,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e1,e2) != op(e3,e2)
& op(e2,e2) != op(e3,e2)
& op(e0,e3) != op(e1,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e1,e3) != op(e3,e3)
& op(e2,e3) != op(e3,e3)
& op(e0,e0) != op(e0,e1)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e1) != op(e0,e3)
& op(e0,e2) != op(e0,e3)
& op(e1,e0) != op(e1,e1)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e1) != op(e1,e3)
& op(e1,e2) != op(e1,e3)
& op(e2,e0) != op(e2,e1)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e1) != op(e2,e3)
& op(e2,e2) != op(e2,e3)
& op(e3,e0) != op(e3,e1)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e1) != op(e3,e3)
& op(e3,e2) != op(e3,e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f4,axiom,
( e0 != e1
& e0 != e2
& e0 != e3
& e1 != e2
& e1 != e3
& e2 != e3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f5,axiom,
( ( op(op(e0,e0),e0) = op(e0,e0)
| op(op(e1,e0),e1) = op(e1,e0)
| op(op(e2,e0),e2) = op(e2,e0)
| op(op(e3,e0),e3) = op(e3,e0) )
& ( op(op(e0,e1),e0) = op(e0,e1)
| op(op(e1,e1),e1) = op(e1,e1)
| op(op(e2,e1),e2) = op(e2,e1)
| op(op(e3,e1),e3) = op(e3,e1) )
& ( op(op(e0,e2),e0) = op(e0,e2)
| op(op(e1,e2),e1) = op(e1,e2)
| op(op(e2,e2),e2) = op(e2,e2)
| op(op(e3,e2),e3) = op(e3,e2) )
& ( op(op(e0,e3),e0) = op(e0,e3)
| op(op(e1,e3),e1) = op(e1,e3)
| op(op(e2,e3),e2) = op(e2,e3)
| op(op(e3,e3),e3) = op(e3,e3) )
& ( ( op(e0,e0) = e0
& op(e0,e0) = e0
& op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3 )
| ( op(e0,e0) = e1
& op(e0,e1) = e0
& op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3 )
| ( op(e0,e0) = e2
& op(e0,e2) = e0
& op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3 )
| ( op(e0,e0) = e3
& op(e0,e3) = e0
& op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3 )
| ( op(e1,e1) = e0
& op(e1,e0) = e1
& op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3 )
| ( op(e1,e1) = e1
& op(e1,e1) = e1
& op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3 )
| ( op(e1,e1) = e2
& op(e1,e2) = e1
& op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3 )
| ( op(e1,e1) = e3
& op(e1,e3) = e1
& op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3 )
| ( op(e2,e2) = e0
& op(e2,e0) = e2
& op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3 )
| ( op(e2,e2) = e1
& op(e2,e1) = e2
& op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3 )
| ( op(e2,e2) = e2
& op(e2,e2) = e2
& op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3 )
| ( op(e2,e2) = e3
& op(e2,e3) = e2
& op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3 )
| ( op(e3,e3) = e0
& op(e3,e0) = e3
& op(e0,e0) != e0
& op(e0,e1) != e1
& op(e0,e2) != e2
& op(e0,e3) != e3 )
| ( op(e3,e3) = e1
& op(e3,e1) = e3
& op(e1,e0) != e0
& op(e1,e1) != e1
& op(e1,e2) != e2
& op(e1,e3) != e3 )
| ( op(e3,e3) = e2
& op(e3,e2) = e3
& op(e2,e0) != e0
& op(e2,e1) != e1
& op(e2,e2) != e2
& op(e2,e3) != e3 )
| ( op(e3,e3) = e3
& op(e3,e3) = e3
& op(e3,e0) != e0
& op(e3,e1) != e1
& op(e3,e2) != e2
& op(e3,e3) != e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f6,axiom,
~ ( e0 = op(e3,e3)
& e1 = op(op(e3,e3),op(e3,e3))
& e2 = op(op(e3,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f7,axiom,
~ ( e0 = op(e2,e2)
& e1 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(e2,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).
fof(f8,axiom,
~ ( e0 = op(e3,e3)
& e2 = op(op(e3,e3),op(e3,e3))
& e1 = op(op(e3,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).
fof(f9,axiom,
~ ( e0 = op(e1,e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(e1,e1),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax9) ).
fof(f10,axiom,
~ ( e0 = op(e2,e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e1 = op(op(e2,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f11,axiom,
~ ( e0 = op(e1,e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e2 = op(op(e1,e1),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f12,axiom,
~ ( e1 = op(e3,e3)
& e0 = op(op(e3,e3),op(e3,e3))
& e2 = op(op(e3,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax12) ).
fof(f13,axiom,
~ ( e1 = op(e2,e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e3 = op(op(e2,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13) ).
fof(f14,axiom,
~ ( e1 = op(e3,e3)
& e2 = op(op(e3,e3),op(e3,e3))
& e0 = op(op(e3,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14) ).
fof(f15,axiom,
~ ( e1 = op(e0,e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e3 = op(op(e0,e0),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax15) ).
fof(f16,axiom,
~ ( e1 = op(e2,e2)
& e3 = op(op(e2,e2),op(e2,e2))
& e0 = op(op(e2,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16) ).
fof(f17,axiom,
~ ( e1 = op(e0,e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e2 = op(op(e0,e0),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17) ).
fof(f18,axiom,
~ ( e2 = op(e3,e3)
& e0 = op(op(e3,e3),op(e3,e3))
& e1 = op(op(e3,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax18) ).
fof(f19,axiom,
~ ( e2 = op(e1,e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e3 = op(op(e1,e1),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax19) ).
fof(f20,axiom,
~ ( e2 = op(e3,e3)
& e1 = op(op(e3,e3),op(e3,e3))
& e0 = op(op(e3,e3),e3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
fof(f21,axiom,
~ ( e2 = op(e0,e0)
& e1 = op(op(e0,e0),op(e0,e0))
& e3 = op(op(e0,e0),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax21) ).
fof(f22,axiom,
~ ( e2 = op(e1,e1)
& e3 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(e1,e1),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax22) ).
fof(f23,axiom,
~ ( e2 = op(e0,e0)
& e3 = op(op(e0,e0),op(e0,e0))
& e1 = op(op(e0,e0),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax23) ).
fof(f24,axiom,
~ ( e3 = op(e2,e2)
& e0 = op(op(e2,e2),op(e2,e2))
& e1 = op(op(e2,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax24) ).
fof(f25,axiom,
~ ( e3 = op(e1,e1)
& e0 = op(op(e1,e1),op(e1,e1))
& e2 = op(op(e1,e1),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax25) ).
fof(f26,axiom,
~ ( e3 = op(e2,e2)
& e1 = op(op(e2,e2),op(e2,e2))
& e0 = op(op(e2,e2),e2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax26) ).
fof(f27,axiom,
~ ( e3 = op(e0,e0)
& e1 = op(op(e0,e0),op(e0,e0))
& e2 = op(op(e0,e0),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax27) ).
fof(f28,axiom,
~ ( e3 = op(e1,e1)
& e2 = op(op(e1,e1),op(e1,e1))
& e0 = op(op(e1,e1),e1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax28) ).
fof(f29,axiom,
~ ( e3 = op(e0,e0)
& e2 = op(op(e0,e0),op(e0,e0))
& e1 = op(op(e0,e0),e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax29) ).
fof(f30,plain,
( e0 != op(e3,e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e2 != op(op(e3,e3),e3) ),
inference(ennf_transformation,[],[f6]) ).
fof(f31,plain,
( e0 != op(e2,e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(e2,e2),e2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f32,plain,
( e0 != op(e3,e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e1 != op(op(e3,e3),e3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f33,plain,
( e0 != op(e1,e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(e1,e1),e1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f34,plain,
( e0 != op(e2,e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(op(e2,e2),e2) ),
inference(ennf_transformation,[],[f10]) ).
fof(f35,plain,
( e0 != op(e1,e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(e1,e1),e1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f36,plain,
( e1 != op(e3,e3)
| e0 != op(op(e3,e3),op(e3,e3))
| e2 != op(op(e3,e3),e3) ),
inference(ennf_transformation,[],[f12]) ).
fof(f37,plain,
( e1 != op(e2,e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(op(e2,e2),e2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f38,plain,
( e1 != op(e3,e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(e3,e3),e3) ),
inference(ennf_transformation,[],[f14]) ).
fof(f39,plain,
( op(e0,e0) != e1
| e2 != op(op(e0,e0),op(e0,e0))
| e3 != op(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(e2,e2),e2) ),
inference(ennf_transformation,[],[f16]) ).
fof(f41,plain,
( op(e0,e0) != e1
| e3 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(e0,e0),e0) ),
inference(ennf_transformation,[],[f17]) ).
fof(f42,plain,
( e2 != op(e3,e3)
| e0 != op(op(e3,e3),op(e3,e3))
| e1 != op(op(e3,e3),e3) ),
inference(ennf_transformation,[],[f18]) ).
fof(f43,plain,
( e2 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(op(e1,e1),e1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f44,plain,
( e2 != op(e3,e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(op(e3,e3),e3) ),
inference(ennf_transformation,[],[f20]) ).
fof(f45,plain,
( op(e0,e0) != e2
| e1 != op(op(e0,e0),op(e0,e0))
| e3 != op(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(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(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(e2,e2),e2) ),
inference(ennf_transformation,[],[f24]) ).
fof(f49,plain,
( e3 != op(e1,e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(op(e1,e1),e1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f50,plain,
( e3 != op(e2,e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e0 != op(op(e2,e2),e2) ),
inference(ennf_transformation,[],[f26]) ).
fof(f51,plain,
( op(e0,e0) != e3
| e1 != op(op(e0,e0),op(e0,e0))
| e2 != op(op(e0,e0),e0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f52,plain,
( e3 != op(e1,e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(op(e1,e1),e1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f53,plain,
( op(e0,e0) != e3
| e2 != op(op(e0,e0),op(e0,e0))
| e1 != op(op(e0,e0),e0) ),
inference(ennf_transformation,[],[f29]) ).
fof(f54,plain,
( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| e0 = op(e0,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f55,plain,
( e3 = op(e0,e1)
| e2 = op(e0,e1)
| e1 = op(e0,e1)
| e0 = op(e0,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f56,plain,
( e3 = op(e0,e2)
| e2 = op(e0,e2)
| e1 = op(e0,e2)
| e0 = op(e0,e2) ),
inference(cnf_transformation,[],[f1]) ).
fof(f57,plain,
( e3 = op(e0,e3)
| e2 = op(e0,e3)
| e1 = op(e0,e3)
| e0 = op(e0,e3) ),
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(f60,plain,
( e3 = op(e1,e2)
| e2 = op(e1,e2)
| e1 = op(e1,e2)
| e0 = op(e1,e2) ),
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(f62,plain,
( e3 = op(e2,e0)
| e2 = op(e2,e0)
| e1 = op(e2,e0)
| e0 = op(e2,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f63,plain,
( e3 = op(e2,e1)
| e2 = op(e2,e1)
| e1 = op(e2,e1)
| e0 = op(e2,e1) ),
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(f65,plain,
( e3 = op(e2,e3)
| e2 = op(e2,e3)
| e1 = op(e2,e3)
| e0 = op(e2,e3) ),
inference(cnf_transformation,[],[f1]) ).
fof(f66,plain,
( e3 = op(e3,e0)
| e2 = op(e3,e0)
| e1 = op(e3,e0)
| e0 = op(e3,e0) ),
inference(cnf_transformation,[],[f1]) ).
fof(f67,plain,
( e3 = op(e3,e1)
| e2 = op(e3,e1)
| e1 = op(e3,e1)
| e0 = op(e3,e1) ),
inference(cnf_transformation,[],[f1]) ).
fof(f68,plain,
( e3 = op(e3,e2)
| e2 = op(e3,e2)
| e1 = op(e3,e2)
| e0 = op(e3,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(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(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(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(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(f102,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f103,plain,
op(e3,e1) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f104,plain,
op(e3,e1) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f105,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f106,plain,
op(e3,e0) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f107,plain,
op(e3,e0) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f108,plain,
op(e2,e2) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f109,plain,
op(e2,e1) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
op(e2,e1) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
op(e2,e0) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f113,plain,
op(e2,e0) != op(e2,e1),
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(f118,plain,
op(e1,e0) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f119,plain,
op(e1,e0) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f120,plain,
op(e0,e2) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
op(e0,e1) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f123,plain,
op(e0,e0) != op(e0,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f124,plain,
op(e0,e0) != op(e0,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f125,plain,
op(e0,e0) != op(e0,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f127,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f128,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f129,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f131,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[],[f3]) ).
fof(f132,plain,
op(e2,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f133,plain,
op(e1,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f134,plain,
op(e1,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f135,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f136,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f137,plain,
op(e0,e2) != op(e1,e2),
inference(cnf_transformation,[],[f3]) ).
fof(f138,plain,
op(e2,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f139,plain,
op(e1,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f140,plain,
op(e1,e1) != op(e2,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f141,plain,
op(e0,e1) != op(e3,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f143,plain,
op(e0,e1) != op(e1,e1),
inference(cnf_transformation,[],[f3]) ).
fof(f144,plain,
op(e2,e0) != op(e3,e0),
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(f147,plain,
op(e0,e0) != op(e3,e0),
inference(cnf_transformation,[],[f3]) ).
fof(f148,plain,
op(e0,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(f159,plain,
( e0 != op(e0,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f161,plain,
( e0 = op(e0,e0)
| ~ sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( e1 != op(e1,e1)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f165,plain,
( e0 != op(e1,e0)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( e0 = op(e0,e1)
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( op(e0,e0) = e1
| ~ sP12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( e2 != op(e2,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( e0 != op(e2,e0)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( e0 = op(e0,e2)
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f173,plain,
( op(e0,e0) = e2
| ~ sP11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( e3 != op(e3,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f177,plain,
( e0 != op(e3,e0)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( e0 = op(e0,e3)
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( op(e0,e0) = e3
| ~ sP10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( e1 != op(e0,e1)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( e0 != op(e0,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( e1 = op(e1,e0)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f185,plain,
( e0 = op(e1,e1)
| ~ sP9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
( e1 != op(e1,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f191,plain,
( e1 = op(e1,e1)
| ~ sP8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( e3 != op(e2,e3)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f193,plain,
( e2 != op(e2,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f194,plain,
( e1 != op(e2,e1)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( e0 != op(e2,e0)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f196,plain,
( e1 = op(e1,e2)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
( e2 = op(e1,e1)
| ~ sP7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
( e3 != op(e3,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( e2 != op(e3,e2)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
( e1 != op(e3,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f201,plain,
( e0 != op(e3,e0)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
( e1 = op(e1,e3)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
( e3 = op(e1,e1)
| ~ sP6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f205,plain,
( e2 != op(e0,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
( e0 != op(e0,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( e2 = op(e2,e0)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f209,plain,
( e0 = op(e2,e2)
| ~ sP5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
( e2 != op(e1,e2)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
( e1 != op(e1,e1)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f214,plain,
( e2 = op(e2,e1)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f215,plain,
( e1 = op(e2,e2)
| ~ sP4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f217,plain,
( e2 != op(e2,e2)
| ~ sP3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f221,plain,
( e2 = op(e2,e2)
| ~ sP3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f222,plain,
( e3 != op(e3,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f223,plain,
( e2 != op(e3,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
( e1 != op(e3,e1)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f225,plain,
( e0 != op(e3,e0)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f226,plain,
( e2 = op(e2,e3)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f227,plain,
( e3 = op(e2,e2)
| ~ sP2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f228,plain,
( e3 != op(e0,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f231,plain,
( e0 != op(e0,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f232,plain,
( e3 = op(e3,e0)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f233,plain,
( e0 = op(e3,e3)
| ~ sP1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f234,plain,
( e3 != op(e1,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f236,plain,
( e1 != op(e1,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f238,plain,
( e3 = op(e3,e1)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f239,plain,
( e1 = op(e3,e3)
| ~ sP0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f246,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(f247,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(f248,plain,
( e3 = op(e3,e3)
| e1 != op(e2,e1)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f249,plain,
( e3 = op(e3,e3)
| e0 != op(e2,e0)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f250,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(f251,plain,
( e3 = op(e3,e3)
| e2 = op(e3,e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f268,plain,
( e2 != op(e3,e2)
| e3 = op(e3,e2)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f271,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(f272,plain,
( e3 != op(e3,e3)
| e1 != op(e2,e1)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f274,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(f275,plain,
( e3 != op(e3,e3)
| e2 = op(e3,e3)
| sP0
| sP1
| sP2
| sP3
| sP4
| sP5
| sP6
| sP7
| sP8
| sP9
| sP10
| sP11
| sP12
| sP13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f280,plain,
( e2 != op(op(e3,e3),e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f30]) ).
fof(f281,plain,
( e3 != op(op(e2,e2),e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f282,plain,
( e1 != op(op(e3,e3),e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e0 != op(e3,e3) ),
inference(cnf_transformation,[],[f32]) ).
fof(f283,plain,
( e3 != op(op(e1,e1),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f284,plain,
( e1 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e0 != op(e2,e2) ),
inference(cnf_transformation,[],[f34]) ).
fof(f285,plain,
( e2 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e0 != op(e1,e1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f286,plain,
( e2 != op(op(e3,e3),e3)
| e0 != op(op(e3,e3),op(e3,e3))
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f36]) ).
fof(f287,plain,
( e3 != op(op(e2,e2),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f37]) ).
fof(f288,plain,
( e0 != op(op(e3,e3),e3)
| e2 != op(op(e3,e3),op(e3,e3))
| e1 != op(e3,e3) ),
inference(cnf_transformation,[],[f38]) ).
fof(f289,plain,
( e3 != op(op(e0,e0),e0)
| e2 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f39]) ).
fof(f290,plain,
( e0 != op(op(e2,e2),e2)
| e3 != op(op(e2,e2),op(e2,e2))
| e1 != op(e2,e2) ),
inference(cnf_transformation,[],[f40]) ).
fof(f291,plain,
( e2 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e1 ),
inference(cnf_transformation,[],[f41]) ).
fof(f292,plain,
( e1 != op(op(e3,e3),e3)
| e0 != op(op(e3,e3),op(e3,e3))
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f42]) ).
fof(f293,plain,
( e3 != op(op(e1,e1),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f294,plain,
( e0 != op(op(e3,e3),e3)
| e1 != op(op(e3,e3),op(e3,e3))
| e2 != op(e3,e3) ),
inference(cnf_transformation,[],[f44]) ).
fof(f295,plain,
( e3 != op(op(e0,e0),e0)
| e1 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f45]) ).
fof(f296,plain,
( e0 != op(op(e1,e1),e1)
| e3 != op(op(e1,e1),op(e1,e1))
| e2 != op(e1,e1) ),
inference(cnf_transformation,[],[f46]) ).
fof(f297,plain,
( e1 != op(op(e0,e0),e0)
| e3 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e2 ),
inference(cnf_transformation,[],[f47]) ).
fof(f298,plain,
( e1 != op(op(e2,e2),e2)
| e0 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f48]) ).
fof(f299,plain,
( e2 != op(op(e1,e1),e1)
| e0 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f49]) ).
fof(f300,plain,
( e0 != op(op(e2,e2),e2)
| e1 != op(op(e2,e2),op(e2,e2))
| e3 != op(e2,e2) ),
inference(cnf_transformation,[],[f50]) ).
fof(f301,plain,
( e2 != op(op(e0,e0),e0)
| e1 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f51]) ).
fof(f302,plain,
( e0 != op(op(e1,e1),e1)
| e2 != op(op(e1,e1),op(e1,e1))
| e3 != op(e1,e1) ),
inference(cnf_transformation,[],[f52]) ).
fof(f303,plain,
( e1 != op(op(e0,e0),e0)
| e2 != op(op(e0,e0),op(e0,e0))
| op(e0,e0) != e3 ),
inference(cnf_transformation,[],[f53]) ).
fof(f304,plain,
( e3 != op(e3,e3)
| e2 = op(e3,e3)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f275]) ).
fof(f305,plain,
( e3 != op(e3,e3)
| e3 = op(e3,e2)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f274]) ).
fof(f307,plain,
( e3 != op(e3,e3)
| e1 != op(e2,e1)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f272]) ).
fof(f308,plain,
( e3 != op(e3,e3)
| e2 != op(e2,e2)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f271]) ).
fof(f311,plain,
( e2 != op(e3,e2)
| e3 = op(e3,e2)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f268]) ).
fof(f328,plain,
( e3 = op(e3,e3)
| e2 = op(e3,e3)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f251]) ).
fof(f329,plain,
( e3 = op(e3,e3)
| e3 = op(e3,e2)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f250]) ).
fof(f330,plain,
( e3 = op(e3,e3)
| e0 != op(e2,e0)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f249]) ).
fof(f331,plain,
( e3 = op(e3,e3)
| e1 != op(e2,e1)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f332,plain,
( e3 = op(e3,e3)
| e2 != op(e2,e2)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f247]) ).
fof(f333,plain,
( e3 = op(e3,e3)
| e3 != op(e2,e3)
| sP0
| ~ sP1
| ~ sP2
| ~ sP3
| sP4
| ~ sP5
| ~ sP6
| sP7
| ~ sP8
| ~ sP9
| sP10
| sP11
| sP12
| ~ sP13 ),
inference(consistent_polarity_flipping,[],[f246]) ).
fof(f340,plain,
( e0 = op(e3,e3)
| sP1 ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f341,plain,
( e3 = op(e3,e0)
| sP1 ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f342,plain,
( e0 != op(e0,e0)
| sP1 ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f345,plain,
( e3 != op(e0,e3)
| sP1 ),
inference(consistent_polarity_flipping,[],[f228]) ).
fof(f346,plain,
( e3 = op(e2,e2)
| sP2 ),
inference(consistent_polarity_flipping,[],[f227]) ).
fof(f347,plain,
( e2 = op(e2,e3)
| sP2 ),
inference(consistent_polarity_flipping,[],[f226]) ).
fof(f348,plain,
( e0 != op(e3,e0)
| sP2 ),
inference(consistent_polarity_flipping,[],[f225]) ).
fof(f349,plain,
( e1 != op(e3,e1)
| sP2 ),
inference(consistent_polarity_flipping,[],[f224]) ).
fof(f350,plain,
( e2 != op(e3,e2)
| sP2 ),
inference(consistent_polarity_flipping,[],[f223]) ).
fof(f351,plain,
( e3 != op(e3,e3)
| sP2 ),
inference(consistent_polarity_flipping,[],[f222]) ).
fof(f352,plain,
( e2 = op(e2,e2)
| sP3 ),
inference(consistent_polarity_flipping,[],[f221]) ).
fof(f356,plain,
( e2 != op(e2,e2)
| sP3 ),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f358,plain,
( e0 = op(e2,e2)
| sP5 ),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f359,plain,
( e2 = op(e2,e0)
| sP5 ),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f360,plain,
( e0 != op(e0,e0)
| sP5 ),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f362,plain,
( e2 != op(e0,e2)
| sP5 ),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f364,plain,
( e3 = op(e1,e1)
| sP6 ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f365,plain,
( e1 = op(e1,e3)
| sP6 ),
inference(consistent_polarity_flipping,[],[f202]) ).
fof(f366,plain,
( e0 != op(e3,e0)
| sP6 ),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f367,plain,
( e1 != op(e3,e1)
| sP6 ),
inference(consistent_polarity_flipping,[],[f200]) ).
fof(f368,plain,
( e2 != op(e3,e2)
| sP6 ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f369,plain,
( e3 != op(e3,e3)
| sP6 ),
inference(consistent_polarity_flipping,[],[f198]) ).
fof(f370,plain,
( e1 = op(e1,e1)
| sP8 ),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f373,plain,
( e1 != op(e1,e1)
| sP8 ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f376,plain,
( e0 = op(e1,e1)
| sP9 ),
inference(consistent_polarity_flipping,[],[f185]) ).
fof(f377,plain,
( e1 = op(e1,e0)
| sP9 ),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f378,plain,
( e0 != op(e0,e0)
| sP9 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f379,plain,
( e1 != op(e0,e1)
| sP9 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f382,plain,
( e0 = op(e0,e0)
| sP13 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f384,plain,
( e0 != op(e0,e0)
| sP13 ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f389,definition,
( spl14_1
<=> op(e0,e0) = e3 ),
introduced(definition,[new_symbols(definition,[spl14_1])],[avatar_definition]) ).
fof(f390,plain,
( op(e0,e0) = e3
| ~ spl14_1 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f393,definition,
( spl14_2
<=> e2 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl14_2])],[avatar_definition]) ).
fof(f395,plain,
( e2 != op(op(e0,e0),op(e0,e0))
| spl14_2 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f397,definition,
( spl14_3
<=> e1 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl14_3])],[avatar_definition]) ).
fof(f399,plain,
( e1 != op(op(e0,e0),e0)
| spl14_3 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f400,plain,
( ~ spl14_1
| ~ spl14_2
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f303,f397,f393,f389]) ).
fof(f402,definition,
( spl14_4
<=> e3 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_4])],[avatar_definition]) ).
fof(f403,plain,
( e3 = op(e1,e1)
| ~ spl14_4 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f406,definition,
( spl14_5
<=> e2 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl14_5])],[avatar_definition]) ).
fof(f408,plain,
( e2 != op(op(e1,e1),op(e1,e1))
| spl14_5 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f410,definition,
( spl14_6
<=> e0 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition]) ).
fof(f412,plain,
( e0 != op(op(e1,e1),e1)
| spl14_6 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f413,plain,
( ~ spl14_4
| ~ spl14_5
| ~ spl14_6 ),
inference(avatar_split_clause,[],[f302,f410,f406,f402]) ).
fof(f415,definition,
( spl14_7
<=> e1 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition]) ).
fof(f417,plain,
( e1 != op(op(e0,e0),op(e0,e0))
| spl14_7 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f419,definition,
( spl14_8
<=> e2 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl14_8])],[avatar_definition]) ).
fof(f421,plain,
( e2 != op(op(e0,e0),e0)
| spl14_8 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f422,plain,
( ~ spl14_1
| ~ spl14_7
| ~ spl14_8 ),
inference(avatar_split_clause,[],[f301,f419,f415,f389]) ).
fof(f424,definition,
( spl14_9
<=> e3 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_9])],[avatar_definition]) ).
fof(f425,plain,
( e3 = op(e2,e2)
| ~ spl14_9 ),
inference(avatar_component_clause,[],[f424]) ).
fof(f428,definition,
( spl14_10
<=> e1 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl14_10])],[avatar_definition]) ).
fof(f430,plain,
( e1 != op(op(e2,e2),op(e2,e2))
| spl14_10 ),
inference(avatar_component_clause,[],[f428]) ).
fof(f432,definition,
( spl14_11
<=> e0 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition]) ).
fof(f434,plain,
( e0 != op(op(e2,e2),e2)
| spl14_11 ),
inference(avatar_component_clause,[],[f432]) ).
fof(f435,plain,
( ~ spl14_9
| ~ spl14_10
| ~ spl14_11 ),
inference(avatar_split_clause,[],[f300,f432,f428,f424]) ).
fof(f437,definition,
( spl14_12
<=> e0 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl14_12])],[avatar_definition]) ).
fof(f439,plain,
( e0 != op(op(e1,e1),op(e1,e1))
| spl14_12 ),
inference(avatar_component_clause,[],[f437]) ).
fof(f441,definition,
( spl14_13
<=> e2 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl14_13])],[avatar_definition]) ).
fof(f443,plain,
( e2 != op(op(e1,e1),e1)
| spl14_13 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f444,plain,
( ~ spl14_4
| ~ spl14_12
| ~ spl14_13 ),
inference(avatar_split_clause,[],[f299,f441,f437,f402]) ).
fof(f446,definition,
( spl14_14
<=> e0 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl14_14])],[avatar_definition]) ).
fof(f448,plain,
( e0 != op(op(e2,e2),op(e2,e2))
| spl14_14 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f450,definition,
( spl14_15
<=> e1 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl14_15])],[avatar_definition]) ).
fof(f452,plain,
( e1 != op(op(e2,e2),e2)
| spl14_15 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,plain,
( ~ spl14_9
| ~ spl14_14
| ~ spl14_15 ),
inference(avatar_split_clause,[],[f298,f450,f446,f424]) ).
fof(f455,definition,
( spl14_16
<=> op(e0,e0) = e2 ),
introduced(definition,[new_symbols(definition,[spl14_16])],[avatar_definition]) ).
fof(f456,plain,
( op(e0,e0) = e2
| ~ spl14_16 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f459,definition,
( spl14_17
<=> e3 = op(op(e0,e0),op(e0,e0)) ),
introduced(definition,[new_symbols(definition,[spl14_17])],[avatar_definition]) ).
fof(f461,plain,
( e3 != op(op(e0,e0),op(e0,e0))
| spl14_17 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f462,plain,
( ~ spl14_16
| ~ spl14_17
| ~ spl14_3 ),
inference(avatar_split_clause,[],[f297,f397,f459,f455]) ).
fof(f464,definition,
( spl14_18
<=> e2 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_18])],[avatar_definition]) ).
fof(f465,plain,
( e2 = op(e1,e1)
| ~ spl14_18 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f468,definition,
( spl14_19
<=> e3 = op(op(e1,e1),op(e1,e1)) ),
introduced(definition,[new_symbols(definition,[spl14_19])],[avatar_definition]) ).
fof(f470,plain,
( e3 != op(op(e1,e1),op(e1,e1))
| spl14_19 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f471,plain,
( ~ spl14_18
| ~ spl14_19
| ~ spl14_6 ),
inference(avatar_split_clause,[],[f296,f410,f468,f464]) ).
fof(f473,definition,
( spl14_20
<=> e3 = op(op(e0,e0),e0) ),
introduced(definition,[new_symbols(definition,[spl14_20])],[avatar_definition]) ).
fof(f475,plain,
( e3 != op(op(e0,e0),e0)
| spl14_20 ),
inference(avatar_component_clause,[],[f473]) ).
fof(f476,plain,
( ~ spl14_16
| ~ spl14_7
| ~ spl14_20 ),
inference(avatar_split_clause,[],[f295,f473,f415,f455]) ).
fof(f478,definition,
( spl14_21
<=> e2 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_21])],[avatar_definition]) ).
fof(f479,plain,
( e2 = op(e3,e3)
| ~ spl14_21 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f482,definition,
( spl14_22
<=> e1 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl14_22])],[avatar_definition]) ).
fof(f484,plain,
( e1 != op(op(e3,e3),op(e3,e3))
| spl14_22 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f486,definition,
( spl14_23
<=> e0 = op(op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl14_23])],[avatar_definition]) ).
fof(f488,plain,
( e0 != op(op(e3,e3),e3)
| spl14_23 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f489,plain,
( ~ spl14_21
| ~ spl14_22
| ~ spl14_23 ),
inference(avatar_split_clause,[],[f294,f486,f482,f478]) ).
fof(f491,definition,
( spl14_24
<=> e3 = op(op(e1,e1),e1) ),
introduced(definition,[new_symbols(definition,[spl14_24])],[avatar_definition]) ).
fof(f493,plain,
( e3 != op(op(e1,e1),e1)
| spl14_24 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f494,plain,
( ~ spl14_18
| ~ spl14_12
| ~ spl14_24 ),
inference(avatar_split_clause,[],[f293,f491,f437,f464]) ).
fof(f496,definition,
( spl14_25
<=> e0 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl14_25])],[avatar_definition]) ).
fof(f498,plain,
( e0 != op(op(e3,e3),op(e3,e3))
| spl14_25 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f500,definition,
( spl14_26
<=> e1 = op(op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl14_26])],[avatar_definition]) ).
fof(f502,plain,
( e1 != op(op(e3,e3),e3)
| spl14_26 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f503,plain,
( ~ spl14_21
| ~ spl14_25
| ~ spl14_26 ),
inference(avatar_split_clause,[],[f292,f500,f496,f478]) ).
fof(f505,definition,
( spl14_27
<=> op(e0,e0) = e1 ),
introduced(definition,[new_symbols(definition,[spl14_27])],[avatar_definition]) ).
fof(f506,plain,
( op(e0,e0) = e1
| ~ spl14_27 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f508,plain,
( ~ spl14_27
| ~ spl14_17
| ~ spl14_8 ),
inference(avatar_split_clause,[],[f291,f419,f459,f505]) ).
fof(f510,definition,
( spl14_28
<=> e1 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_28])],[avatar_definition]) ).
fof(f511,plain,
( e1 = op(e2,e2)
| ~ spl14_28 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f514,definition,
( spl14_29
<=> e3 = op(op(e2,e2),op(e2,e2)) ),
introduced(definition,[new_symbols(definition,[spl14_29])],[avatar_definition]) ).
fof(f516,plain,
( e3 != op(op(e2,e2),op(e2,e2))
| spl14_29 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f517,plain,
( ~ spl14_28
| ~ spl14_29
| ~ spl14_11 ),
inference(avatar_split_clause,[],[f290,f432,f514,f510]) ).
fof(f518,plain,
( ~ spl14_27
| ~ spl14_2
| ~ spl14_20 ),
inference(avatar_split_clause,[],[f289,f473,f393,f505]) ).
fof(f520,definition,
( spl14_30
<=> e1 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_30])],[avatar_definition]) ).
fof(f521,plain,
( e1 = op(e3,e3)
| ~ spl14_30 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f524,definition,
( spl14_31
<=> e2 = op(op(e3,e3),op(e3,e3)) ),
introduced(definition,[new_symbols(definition,[spl14_31])],[avatar_definition]) ).
fof(f526,plain,
( e2 != op(op(e3,e3),op(e3,e3))
| spl14_31 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f527,plain,
( ~ spl14_30
| ~ spl14_31
| ~ spl14_23 ),
inference(avatar_split_clause,[],[f288,f486,f524,f520]) ).
fof(f529,definition,
( spl14_32
<=> e3 = op(op(e2,e2),e2) ),
introduced(definition,[new_symbols(definition,[spl14_32])],[avatar_definition]) ).
fof(f531,plain,
( e3 != op(op(e2,e2),e2)
| spl14_32 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f532,plain,
( ~ spl14_28
| ~ spl14_14
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f287,f529,f446,f510]) ).
fof(f534,definition,
( spl14_33
<=> e2 = op(op(e3,e3),e3) ),
introduced(definition,[new_symbols(definition,[spl14_33])],[avatar_definition]) ).
fof(f536,plain,
( e2 != op(op(e3,e3),e3)
| spl14_33 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f537,plain,
( ~ spl14_30
| ~ spl14_25
| ~ spl14_33 ),
inference(avatar_split_clause,[],[f286,f534,f496,f520]) ).
fof(f539,definition,
( spl14_34
<=> e0 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_34])],[avatar_definition]) ).
fof(f540,plain,
( e0 = op(e1,e1)
| ~ spl14_34 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f542,plain,
( ~ spl14_34
| ~ spl14_19
| ~ spl14_13 ),
inference(avatar_split_clause,[],[f285,f441,f468,f539]) ).
fof(f544,definition,
( spl14_35
<=> e0 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_35])],[avatar_definition]) ).
fof(f545,plain,
( e0 = op(e2,e2)
| ~ spl14_35 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( ~ spl14_35
| ~ spl14_29
| ~ spl14_15 ),
inference(avatar_split_clause,[],[f284,f450,f514,f544]) ).
fof(f548,plain,
( ~ spl14_34
| ~ spl14_5
| ~ spl14_24 ),
inference(avatar_split_clause,[],[f283,f491,f406,f539]) ).
fof(f550,definition,
( spl14_36
<=> e0 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_36])],[avatar_definition]) ).
fof(f551,plain,
( e0 = op(e3,e3)
| ~ spl14_36 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f553,plain,
( ~ spl14_36
| ~ spl14_31
| ~ spl14_26 ),
inference(avatar_split_clause,[],[f282,f500,f524,f550]) ).
fof(f554,plain,
( ~ spl14_35
| ~ spl14_10
| ~ spl14_32 ),
inference(avatar_split_clause,[],[f281,f529,f428,f544]) ).
fof(f555,plain,
( ~ spl14_36
| ~ spl14_22
| ~ spl14_33 ),
inference(avatar_split_clause,[],[f280,f534,f482,f550]) ).
fof(f557,definition,
( spl14_37
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl14_37])],[avatar_definition]) ).
fof(f561,definition,
( spl14_38
<=> e3 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_38])],[avatar_definition]) ).
fof(f562,plain,
( e3 = op(e0,e3)
| ~ spl14_38 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f566,definition,
( spl14_39
<=> e2 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_39])],[avatar_definition]) ).
fof(f567,plain,
( e2 = op(e0,e2)
| ~ spl14_39 ),
inference(avatar_component_clause,[],[f566]) ).
fof(f571,definition,
( spl14_40
<=> e1 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_40])],[avatar_definition]) ).
fof(f572,plain,
( e1 = op(e0,e1)
| ~ spl14_40 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f576,definition,
( spl14_41
<=> e0 = op(e0,e0) ),
introduced(definition,[new_symbols(definition,[spl14_41])],[avatar_definition]) ).
fof(f577,plain,
( e0 = op(e0,e0)
| ~ spl14_41 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f579,plain,
( spl14_37
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f384,f576,f557]) ).
fof(f581,plain,
( spl14_37
| spl14_41 ),
inference(avatar_split_clause,[],[f382,f576,f557]) ).
fof(f583,definition,
( spl14_42
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl14_42])],[avatar_definition]) ).
fof(f587,definition,
( spl14_43
<=> e3 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_43])],[avatar_definition]) ).
fof(f588,plain,
( e3 = op(e1,e3)
| ~ spl14_43 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f592,definition,
( spl14_44
<=> e2 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_44])],[avatar_definition]) ).
fof(f593,plain,
( e2 = op(e1,e2)
| ~ spl14_44 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f597,definition,
( spl14_45
<=> e1 = op(e1,e1) ),
introduced(definition,[new_symbols(definition,[spl14_45])],[avatar_definition]) ).
fof(f598,plain,
( e1 = op(e1,e1)
| ~ spl14_45 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f600,plain,
( ~ spl14_42
| ~ spl14_45 ),
inference(avatar_split_clause,[],[f164,f597,f583]) ).
fof(f602,definition,
( spl14_46
<=> e0 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_46])],[avatar_definition]) ).
fof(f603,plain,
( e0 = op(e1,e0)
| ~ spl14_46 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f605,plain,
( ~ spl14_42
| ~ spl14_46 ),
inference(avatar_split_clause,[],[f165,f602,f583]) ).
fof(f607,definition,
( spl14_47
<=> e0 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_47])],[avatar_definition]) ).
fof(f609,plain,
( e0 = op(e0,e1)
| ~ spl14_47 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( ~ spl14_42
| spl14_47 ),
inference(avatar_split_clause,[],[f166,f607,f583]) ).
fof(f611,plain,
( ~ spl14_42
| spl14_27 ),
inference(avatar_split_clause,[],[f167,f505,f583]) ).
fof(f613,definition,
( spl14_48
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl14_48])],[avatar_definition]) ).
fof(f617,definition,
( spl14_49
<=> e3 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_49])],[avatar_definition]) ).
fof(f618,plain,
( e3 = op(e2,e3)
| ~ spl14_49 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f622,definition,
( spl14_50
<=> e2 = op(e2,e2) ),
introduced(definition,[new_symbols(definition,[spl14_50])],[avatar_definition]) ).
fof(f623,plain,
( e2 = op(e2,e2)
| ~ spl14_50 ),
inference(avatar_component_clause,[],[f622]) ).
fof(f625,plain,
( ~ spl14_48
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f169,f622,f613]) ).
fof(f627,definition,
( spl14_51
<=> e1 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_51])],[avatar_definition]) ).
fof(f628,plain,
( e1 = op(e2,e1)
| ~ spl14_51 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f632,definition,
( spl14_52
<=> e0 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_52])],[avatar_definition]) ).
fof(f633,plain,
( e0 = op(e2,e0)
| ~ spl14_52 ),
inference(avatar_component_clause,[],[f632]) ).
fof(f635,plain,
( ~ spl14_48
| ~ spl14_52 ),
inference(avatar_split_clause,[],[f171,f632,f613]) ).
fof(f637,definition,
( spl14_53
<=> e0 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_53])],[avatar_definition]) ).
fof(f639,plain,
( e0 = op(e0,e2)
| ~ spl14_53 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f640,plain,
( ~ spl14_48
| spl14_53 ),
inference(avatar_split_clause,[],[f172,f637,f613]) ).
fof(f641,plain,
( ~ spl14_48
| spl14_16 ),
inference(avatar_split_clause,[],[f173,f455,f613]) ).
fof(f643,definition,
( spl14_54
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl14_54])],[avatar_definition]) ).
fof(f647,definition,
( spl14_55
<=> e3 = op(e3,e3) ),
introduced(definition,[new_symbols(definition,[spl14_55])],[avatar_definition]) ).
fof(f648,plain,
( e3 = op(e3,e3)
| ~ spl14_55 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f650,plain,
( ~ spl14_54
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f174,f647,f643]) ).
fof(f652,definition,
( spl14_56
<=> e2 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_56])],[avatar_definition]) ).
fof(f653,plain,
( e2 = op(e3,e2)
| ~ spl14_56 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f657,definition,
( spl14_57
<=> e1 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_57])],[avatar_definition]) ).
fof(f658,plain,
( e1 = op(e3,e1)
| ~ spl14_57 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f662,definition,
( spl14_58
<=> e0 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_58])],[avatar_definition]) ).
fof(f663,plain,
( e0 = op(e3,e0)
| ~ spl14_58 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f665,plain,
( ~ spl14_54
| ~ spl14_58 ),
inference(avatar_split_clause,[],[f177,f662,f643]) ).
fof(f667,definition,
( spl14_59
<=> e0 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_59])],[avatar_definition]) ).
fof(f669,plain,
( e0 = op(e0,e3)
| ~ spl14_59 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f670,plain,
( ~ spl14_54
| spl14_59 ),
inference(avatar_split_clause,[],[f178,f667,f643]) ).
fof(f671,plain,
( ~ spl14_54
| spl14_1 ),
inference(avatar_split_clause,[],[f179,f389,f643]) ).
fof(f673,definition,
( spl14_60
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl14_60])],[avatar_definition]) ).
fof(f678,plain,
( spl14_60
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f379,f571,f673]) ).
fof(f679,plain,
( spl14_60
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f378,f576,f673]) ).
fof(f681,definition,
( spl14_61
<=> e1 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_61])],[avatar_definition]) ).
fof(f683,plain,
( e1 = op(e1,e0)
| ~ spl14_61 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f684,plain,
( spl14_60
| spl14_61 ),
inference(avatar_split_clause,[],[f377,f681,f673]) ).
fof(f685,plain,
( spl14_60
| spl14_34 ),
inference(avatar_split_clause,[],[f376,f539,f673]) ).
fof(f687,definition,
( spl14_62
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl14_62])],[avatar_definition]) ).
fof(f692,plain,
( spl14_62
| ~ spl14_45 ),
inference(avatar_split_clause,[],[f373,f597,f687]) ).
fof(f695,plain,
( spl14_62
| spl14_45 ),
inference(avatar_split_clause,[],[f370,f597,f687]) ).
fof(f697,definition,
( spl14_63
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl14_63])],[avatar_definition]) ).
fof(f700,plain,
( ~ spl14_63
| ~ spl14_49 ),
inference(avatar_split_clause,[],[f192,f617,f697]) ).
fof(f701,plain,
( ~ spl14_63
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f193,f622,f697]) ).
fof(f702,plain,
( ~ spl14_63
| ~ spl14_51 ),
inference(avatar_split_clause,[],[f194,f627,f697]) ).
fof(f703,plain,
( ~ spl14_63
| ~ spl14_52 ),
inference(avatar_split_clause,[],[f195,f632,f697]) ).
fof(f705,definition,
( spl14_64
<=> e1 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_64])],[avatar_definition]) ).
fof(f707,plain,
( e1 = op(e1,e2)
| ~ spl14_64 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f708,plain,
( ~ spl14_63
| spl14_64 ),
inference(avatar_split_clause,[],[f196,f705,f697]) ).
fof(f709,plain,
( ~ spl14_63
| spl14_18 ),
inference(avatar_split_clause,[],[f197,f464,f697]) ).
fof(f711,definition,
( spl14_65
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl14_65])],[avatar_definition]) ).
fof(f714,plain,
( spl14_65
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f369,f647,f711]) ).
fof(f715,plain,
( spl14_65
| ~ spl14_56 ),
inference(avatar_split_clause,[],[f368,f652,f711]) ).
fof(f716,plain,
( spl14_65
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f367,f657,f711]) ).
fof(f717,plain,
( spl14_65
| ~ spl14_58 ),
inference(avatar_split_clause,[],[f366,f662,f711]) ).
fof(f719,definition,
( spl14_66
<=> e1 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_66])],[avatar_definition]) ).
fof(f721,plain,
( e1 = op(e1,e3)
| ~ spl14_66 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f722,plain,
( spl14_65
| spl14_66 ),
inference(avatar_split_clause,[],[f365,f719,f711]) ).
fof(f723,plain,
( spl14_65
| spl14_4 ),
inference(avatar_split_clause,[],[f364,f402,f711]) ).
fof(f725,definition,
( spl14_67
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl14_67])],[avatar_definition]) ).
fof(f729,plain,
( spl14_67
| ~ spl14_39 ),
inference(avatar_split_clause,[],[f362,f566,f725]) ).
fof(f731,plain,
( spl14_67
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f360,f576,f725]) ).
fof(f733,definition,
( spl14_68
<=> e2 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_68])],[avatar_definition]) ).
fof(f735,plain,
( e2 = op(e2,e0)
| ~ spl14_68 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f736,plain,
( spl14_67
| spl14_68 ),
inference(avatar_split_clause,[],[f359,f733,f725]) ).
fof(f737,plain,
( spl14_67
| spl14_35 ),
inference(avatar_split_clause,[],[f358,f544,f725]) ).
fof(f739,definition,
( spl14_69
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl14_69])],[avatar_definition]) ).
fof(f743,plain,
( ~ spl14_69
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f211,f592,f739]) ).
fof(f744,plain,
( ~ spl14_69
| ~ spl14_45 ),
inference(avatar_split_clause,[],[f212,f597,f739]) ).
fof(f747,definition,
( spl14_70
<=> e2 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_70])],[avatar_definition]) ).
fof(f749,plain,
( e2 = op(e2,e1)
| ~ spl14_70 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f750,plain,
( ~ spl14_69
| spl14_70 ),
inference(avatar_split_clause,[],[f214,f747,f739]) ).
fof(f751,plain,
( ~ spl14_69
| spl14_28 ),
inference(avatar_split_clause,[],[f215,f510,f739]) ).
fof(f753,definition,
( spl14_71
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl14_71])],[avatar_definition]) ).
fof(f757,plain,
( spl14_71
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f356,f622,f753]) ).
fof(f761,plain,
( spl14_71
| spl14_50 ),
inference(avatar_split_clause,[],[f352,f622,f753]) ).
fof(f763,definition,
( spl14_72
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl14_72])],[avatar_definition]) ).
fof(f766,plain,
( spl14_72
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f351,f647,f763]) ).
fof(f767,plain,
( spl14_72
| ~ spl14_56 ),
inference(avatar_split_clause,[],[f350,f652,f763]) ).
fof(f768,plain,
( spl14_72
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f349,f657,f763]) ).
fof(f769,plain,
( spl14_72
| ~ spl14_58 ),
inference(avatar_split_clause,[],[f348,f662,f763]) ).
fof(f771,definition,
( spl14_73
<=> e2 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_73])],[avatar_definition]) ).
fof(f773,plain,
( e2 = op(e2,e3)
| ~ spl14_73 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f774,plain,
( spl14_72
| spl14_73 ),
inference(avatar_split_clause,[],[f347,f771,f763]) ).
fof(f775,plain,
( spl14_72
| spl14_9 ),
inference(avatar_split_clause,[],[f346,f424,f763]) ).
fof(f777,definition,
( spl14_74
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl14_74])],[avatar_definition]) ).
fof(f780,plain,
( spl14_74
| ~ spl14_38 ),
inference(avatar_split_clause,[],[f345,f561,f777]) ).
fof(f783,plain,
( spl14_74
| ~ spl14_41 ),
inference(avatar_split_clause,[],[f342,f576,f777]) ).
fof(f785,definition,
( spl14_75
<=> e3 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_75])],[avatar_definition]) ).
fof(f787,plain,
( e3 = op(e3,e0)
| ~ spl14_75 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f788,plain,
( spl14_74
| spl14_75 ),
inference(avatar_split_clause,[],[f341,f785,f777]) ).
fof(f789,plain,
( spl14_74
| spl14_36 ),
inference(avatar_split_clause,[],[f340,f550,f777]) ).
fof(f791,definition,
( spl14_76
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl14_76])],[avatar_definition]) ).
fof(f794,plain,
( ~ spl14_76
| ~ spl14_43 ),
inference(avatar_split_clause,[],[f234,f587,f791]) ).
fof(f796,plain,
( ~ spl14_76
| ~ spl14_45 ),
inference(avatar_split_clause,[],[f236,f597,f791]) ).
fof(f799,definition,
( spl14_77
<=> e3 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_77])],[avatar_definition]) ).
fof(f801,plain,
( e3 = op(e3,e1)
| ~ spl14_77 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f802,plain,
( ~ spl14_76
| spl14_77 ),
inference(avatar_split_clause,[],[f238,f799,f791]) ).
fof(f803,plain,
( ~ spl14_76
| spl14_30 ),
inference(avatar_split_clause,[],[f239,f520,f791]) ).
fof(f809,definition,
( spl14_78
<=> e3 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_78])],[avatar_definition]) ).
fof(f811,plain,
( e3 = op(e3,e2)
| ~ spl14_78 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f814,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| ~ spl14_49
| spl14_55 ),
inference(avatar_split_clause,[],[f333,f647,f617,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f815,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| ~ spl14_50
| spl14_55 ),
inference(avatar_split_clause,[],[f332,f647,f622,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f816,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| ~ spl14_51
| spl14_55 ),
inference(avatar_split_clause,[],[f331,f647,f627,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f817,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| ~ spl14_52
| spl14_55 ),
inference(avatar_split_clause,[],[f330,f647,f632,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f818,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_78
| spl14_55 ),
inference(avatar_split_clause,[],[f329,f647,f809,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f819,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_21
| spl14_55 ),
inference(avatar_split_clause,[],[f328,f647,f478,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f836,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_78
| ~ spl14_56 ),
inference(avatar_split_clause,[],[f311,f652,f809,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f839,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| ~ spl14_50
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f308,f647,f622,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f840,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| ~ spl14_51
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f307,f647,f627,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f842,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_78
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f305,f647,f809,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f843,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_21
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f304,f647,f478,f791,f777,f763,f753,f739,f725,f711,f697,f687,f673,f643,f613,f583,f557]) ).
fof(f915,definition,
( spl14_95
<=> e1 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_95])],[avatar_definition]) ).
fof(f917,plain,
( e1 = op(e0,e2)
| ~ spl14_95 ),
inference(avatar_component_clause,[],[f915]) ).
fof(f919,definition,
( spl14_96
<=> e1 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_96])],[avatar_definition]) ).
fof(f922,plain,
( spl14_27
| spl14_40
| spl14_95
| spl14_96 ),
inference(avatar_split_clause,[],[f72,f919,f915,f571,f505]) ).
fof(f924,definition,
( spl14_97
<=> e1 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_97])],[avatar_definition]) ).
fof(f926,plain,
( e1 = op(e2,e0)
| ~ spl14_97 ),
inference(avatar_component_clause,[],[f924]) ).
fof(f928,definition,
( spl14_98
<=> e1 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_98])],[avatar_definition]) ).
fof(f930,plain,
( e1 = op(e3,e0)
| ~ spl14_98 ),
inference(avatar_component_clause,[],[f928]) ).
fof(f931,plain,
( spl14_27
| spl14_61
| spl14_97
| spl14_98 ),
inference(avatar_split_clause,[],[f73,f928,f924,f681,f505]) ).
fof(f933,definition,
( spl14_99
<=> e2 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_99])],[avatar_definition]) ).
fof(f937,definition,
( spl14_100
<=> e2 = op(e0,e3) ),
introduced(definition,[new_symbols(definition,[spl14_100])],[avatar_definition]) ).
fof(f939,plain,
( e2 = op(e0,e3)
| ~ spl14_100 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f942,definition,
( spl14_101
<=> e2 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_101])],[avatar_definition]) ).
fof(f944,plain,
( e2 = op(e1,e0)
| ~ spl14_101 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f946,definition,
( spl14_102
<=> e2 = op(e3,e0) ),
introduced(definition,[new_symbols(definition,[spl14_102])],[avatar_definition]) ).
fof(f948,plain,
( e2 = op(e3,e0)
| ~ spl14_102 ),
inference(avatar_component_clause,[],[f946]) ).
fof(f949,plain,
( spl14_16
| spl14_101
| spl14_68
| spl14_102 ),
inference(avatar_split_clause,[],[f75,f946,f733,f942,f455]) ).
fof(f951,definition,
( spl14_103
<=> e3 = op(e0,e1) ),
introduced(definition,[new_symbols(definition,[spl14_103])],[avatar_definition]) ).
fof(f955,definition,
( spl14_104
<=> e3 = op(e0,e2) ),
introduced(definition,[new_symbols(definition,[spl14_104])],[avatar_definition]) ).
fof(f957,plain,
( e3 = op(e0,e2)
| ~ spl14_104 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f958,plain,
( spl14_1
| spl14_103
| spl14_104
| spl14_38 ),
inference(avatar_split_clause,[],[f76,f561,f955,f951,f389]) ).
fof(f960,definition,
( spl14_105
<=> e3 = op(e1,e0) ),
introduced(definition,[new_symbols(definition,[spl14_105])],[avatar_definition]) ).
fof(f962,plain,
( e3 = op(e1,e0)
| ~ spl14_105 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f964,definition,
( spl14_106
<=> e3 = op(e2,e0) ),
introduced(definition,[new_symbols(definition,[spl14_106])],[avatar_definition]) ).
fof(f966,plain,
( e3 = op(e2,e0)
| ~ spl14_106 ),
inference(avatar_component_clause,[],[f964]) ).
fof(f967,plain,
( spl14_1
| spl14_105
| spl14_106
| spl14_75 ),
inference(avatar_split_clause,[],[f77,f785,f964,f960,f389]) ).
fof(f969,definition,
( spl14_107
<=> e0 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_107])],[avatar_definition]) ).
fof(f971,plain,
( e0 = op(e1,e2)
| ~ spl14_107 ),
inference(avatar_component_clause,[],[f969]) ).
fof(f973,definition,
( spl14_108
<=> e0 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_108])],[avatar_definition]) ).
fof(f975,plain,
( e0 = op(e1,e3)
| ~ spl14_108 ),
inference(avatar_component_clause,[],[f973]) ).
fof(f976,plain,
( spl14_46
| spl14_34
| spl14_107
| spl14_108 ),
inference(avatar_split_clause,[],[f78,f973,f969,f539,f602]) ).
fof(f978,definition,
( spl14_109
<=> e0 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_109])],[avatar_definition]) ).
fof(f980,plain,
( e0 = op(e2,e1)
| ~ spl14_109 ),
inference(avatar_component_clause,[],[f978]) ).
fof(f982,definition,
( spl14_110
<=> e0 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_110])],[avatar_definition]) ).
fof(f984,plain,
( e0 = op(e3,e1)
| ~ spl14_110 ),
inference(avatar_component_clause,[],[f982]) ).
fof(f985,plain,
( spl14_47
| spl14_34
| spl14_109
| spl14_110 ),
inference(avatar_split_clause,[],[f79,f982,f978,f539,f607]) ).
fof(f987,plain,
( spl14_40
| spl14_45
| spl14_51
| spl14_57 ),
inference(avatar_split_clause,[],[f81,f657,f627,f597,f571]) ).
fof(f989,definition,
( spl14_111
<=> e2 = op(e1,e3) ),
introduced(definition,[new_symbols(definition,[spl14_111])],[avatar_definition]) ).
fof(f991,plain,
( e2 = op(e1,e3)
| ~ spl14_111 ),
inference(avatar_component_clause,[],[f989]) ).
fof(f992,plain,
( spl14_101
| spl14_18
| spl14_44
| spl14_111 ),
inference(avatar_split_clause,[],[f82,f989,f592,f464,f942]) ).
fof(f994,definition,
( spl14_112
<=> e2 = op(e3,e1) ),
introduced(definition,[new_symbols(definition,[spl14_112])],[avatar_definition]) ).
fof(f996,plain,
( e2 = op(e3,e1)
| ~ spl14_112 ),
inference(avatar_component_clause,[],[f994]) ).
fof(f997,plain,
( spl14_99
| spl14_18
| spl14_70
| spl14_112 ),
inference(avatar_split_clause,[],[f83,f994,f747,f464,f933]) ).
fof(f999,definition,
( spl14_113
<=> e3 = op(e1,e2) ),
introduced(definition,[new_symbols(definition,[spl14_113])],[avatar_definition]) ).
fof(f1001,plain,
( e3 = op(e1,e2)
| ~ spl14_113 ),
inference(avatar_component_clause,[],[f999]) ).
fof(f1002,plain,
( spl14_105
| spl14_4
| spl14_113
| spl14_43 ),
inference(avatar_split_clause,[],[f84,f587,f999,f402,f960]) ).
fof(f1004,definition,
( spl14_114
<=> e3 = op(e2,e1) ),
introduced(definition,[new_symbols(definition,[spl14_114])],[avatar_definition]) ).
fof(f1006,plain,
( e3 = op(e2,e1)
| ~ spl14_114 ),
inference(avatar_component_clause,[],[f1004]) ).
fof(f1007,plain,
( spl14_103
| spl14_4
| spl14_114
| spl14_77 ),
inference(avatar_split_clause,[],[f85,f799,f1004,f402,f951]) ).
fof(f1009,definition,
( spl14_115
<=> e0 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_115])],[avatar_definition]) ).
fof(f1011,plain,
( e0 = op(e2,e3)
| ~ spl14_115 ),
inference(avatar_component_clause,[],[f1009]) ).
fof(f1012,plain,
( spl14_52
| spl14_109
| spl14_35
| spl14_115 ),
inference(avatar_split_clause,[],[f86,f1009,f544,f978,f632]) ).
fof(f1014,definition,
( spl14_116
<=> e0 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_116])],[avatar_definition]) ).
fof(f1016,plain,
( e0 = op(e3,e2)
| ~ spl14_116 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1019,definition,
( spl14_117
<=> e1 = op(e2,e3) ),
introduced(definition,[new_symbols(definition,[spl14_117])],[avatar_definition]) ).
fof(f1022,plain,
( spl14_97
| spl14_51
| spl14_28
| spl14_117 ),
inference(avatar_split_clause,[],[f88,f1019,f510,f627,f924]) ).
fof(f1024,definition,
( spl14_118
<=> e1 = op(e3,e2) ),
introduced(definition,[new_symbols(definition,[spl14_118])],[avatar_definition]) ).
fof(f1026,plain,
( e1 = op(e3,e2)
| ~ spl14_118 ),
inference(avatar_component_clause,[],[f1024]) ).
fof(f1027,plain,
( spl14_95
| spl14_64
| spl14_28
| spl14_118 ),
inference(avatar_split_clause,[],[f89,f1024,f510,f705,f915]) ).
fof(f1029,plain,
( spl14_39
| spl14_44
| spl14_50
| spl14_56 ),
inference(avatar_split_clause,[],[f91,f652,f622,f592,f566]) ).
fof(f1030,plain,
( spl14_106
| spl14_114
| spl14_9
| spl14_49 ),
inference(avatar_split_clause,[],[f92,f617,f424,f1004,f964]) ).
fof(f1031,plain,
( spl14_104
| spl14_113
| spl14_9
| spl14_78 ),
inference(avatar_split_clause,[],[f93,f809,f424,f999,f955]) ).
fof(f1032,plain,
( spl14_58
| spl14_110
| spl14_116
| spl14_36 ),
inference(avatar_split_clause,[],[f94,f550,f1014,f982,f662]) ).
fof(f1033,plain,
( spl14_59
| spl14_108
| spl14_115
| spl14_36 ),
inference(avatar_split_clause,[],[f95,f550,f1009,f973,f667]) ).
fof(f1034,plain,
( spl14_98
| spl14_57
| spl14_118
| spl14_30 ),
inference(avatar_split_clause,[],[f96,f520,f1024,f657,f928]) ).
fof(f1035,plain,
( spl14_96
| spl14_66
| spl14_117
| spl14_30 ),
inference(avatar_split_clause,[],[f97,f520,f1019,f719,f919]) ).
fof(f1036,plain,
( spl14_102
| spl14_112
| spl14_56
| spl14_21 ),
inference(avatar_split_clause,[],[f98,f478,f652,f994,f946]) ).
fof(f1037,plain,
( spl14_100
| spl14_111
| spl14_73
| spl14_21 ),
inference(avatar_split_clause,[],[f99,f478,f771,f989,f937]) ).
fof(f1038,plain,
( spl14_75
| spl14_77
| spl14_78
| spl14_55 ),
inference(avatar_split_clause,[],[f100,f647,f809,f799,f785]) ).
fof(f1039,plain,
( spl14_38
| spl14_43
| spl14_49
| spl14_55 ),
inference(avatar_split_clause,[],[f101,f647,f617,f587,f561]) ).
fof(f1040,plain,
( spl14_41
| spl14_27
| spl14_16
| spl14_1 ),
inference(avatar_split_clause,[],[f54,f389,f455,f505,f576]) ).
fof(f1041,plain,
( spl14_47
| spl14_40
| spl14_99
| spl14_103 ),
inference(avatar_split_clause,[],[f55,f951,f933,f571,f607]) ).
fof(f1042,plain,
( spl14_53
| spl14_95
| spl14_39
| spl14_104 ),
inference(avatar_split_clause,[],[f56,f955,f566,f915,f637]) ).
fof(f1043,plain,
( spl14_59
| spl14_96
| spl14_100
| spl14_38 ),
inference(avatar_split_clause,[],[f57,f561,f937,f919,f667]) ).
fof(f1044,plain,
( spl14_46
| spl14_61
| spl14_101
| spl14_105 ),
inference(avatar_split_clause,[],[f58,f960,f942,f681,f602]) ).
fof(f1045,plain,
( spl14_34
| spl14_45
| spl14_18
| spl14_4 ),
inference(avatar_split_clause,[],[f59,f402,f464,f597,f539]) ).
fof(f1046,plain,
( spl14_107
| spl14_64
| spl14_44
| spl14_113 ),
inference(avatar_split_clause,[],[f60,f999,f592,f705,f969]) ).
fof(f1047,plain,
( spl14_108
| spl14_66
| spl14_111
| spl14_43 ),
inference(avatar_split_clause,[],[f61,f587,f989,f719,f973]) ).
fof(f1048,plain,
( spl14_52
| spl14_97
| spl14_68
| spl14_106 ),
inference(avatar_split_clause,[],[f62,f964,f733,f924,f632]) ).
fof(f1049,plain,
( spl14_109
| spl14_51
| spl14_70
| spl14_114 ),
inference(avatar_split_clause,[],[f63,f1004,f747,f627,f978]) ).
fof(f1050,plain,
( spl14_35
| spl14_28
| spl14_50
| spl14_9 ),
inference(avatar_split_clause,[],[f64,f424,f622,f510,f544]) ).
fof(f1051,plain,
( spl14_115
| spl14_117
| spl14_73
| spl14_49 ),
inference(avatar_split_clause,[],[f65,f617,f771,f1019,f1009]) ).
fof(f1052,plain,
( spl14_58
| spl14_98
| spl14_102
| spl14_75 ),
inference(avatar_split_clause,[],[f66,f785,f946,f928,f662]) ).
fof(f1053,plain,
( spl14_110
| spl14_57
| spl14_112
| spl14_77 ),
inference(avatar_split_clause,[],[f67,f799,f994,f657,f982]) ).
fof(f1054,plain,
( spl14_116
| spl14_118
| spl14_56
| spl14_78 ),
inference(avatar_split_clause,[],[f68,f809,f652,f1024,f1014]) ).
fof(f1055,plain,
( spl14_36
| spl14_30
| spl14_21
| spl14_55 ),
inference(avatar_split_clause,[],[f69,f647,f478,f520,f550]) ).
fof(f1057,plain,
( e2 = e3
| ~ spl14_4
| ~ spl14_18 ),
inference(forward_demodulation,[],[f465,f403]) ).
fof(f1058,plain,
( $false
| ~ spl14_4
| ~ spl14_18 ),
inference(forward_subsumption_resolution,[],[f1057,f150]) ).
fof(f1059,plain,
( ~ spl14_4
| ~ spl14_18 ),
inference(avatar_contradiction_clause,[],[f1058]) ).
fof(f1061,plain,
( e1 = e2
| ~ spl14_16
| ~ spl14_27 ),
inference(forward_demodulation,[],[f506,f456]) ).
fof(f1062,plain,
( $false
| ~ spl14_16
| ~ spl14_27 ),
inference(forward_subsumption_resolution,[],[f1061,f152]) ).
fof(f1063,plain,
( ~ spl14_16
| ~ spl14_27 ),
inference(avatar_contradiction_clause,[],[f1062]) ).
fof(f1066,plain,
( e0 = e3
| ~ spl14_4
| ~ spl14_34 ),
inference(forward_demodulation,[],[f540,f403]) ).
fof(f1067,plain,
( $false
| ~ spl14_4
| ~ spl14_34 ),
inference(forward_subsumption_resolution,[],[f1066,f153]) ).
fof(f1068,plain,
( ~ spl14_4
| ~ spl14_34 ),
inference(avatar_contradiction_clause,[],[f1067]) ).
fof(f1070,plain,
( e0 = e3
| ~ spl14_9
| ~ spl14_35 ),
inference(forward_demodulation,[],[f545,f425]) ).
fof(f1071,plain,
( $false
| ~ spl14_9
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f1070,f153]) ).
fof(f1072,plain,
( ~ spl14_9
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f1071]) ).
fof(f1087,plain,
( e2 = e3
| ~ spl14_21
| ~ spl14_55 ),
inference(superposition,[],[f648,f479]) ).
fof(f1091,plain,
( $false
| ~ spl14_21
| ~ spl14_55 ),
inference(forward_subsumption_resolution,[],[f1087,f150]) ).
fof(f1092,plain,
( ~ spl14_21
| ~ spl14_55 ),
inference(avatar_contradiction_clause,[],[f1091]) ).
fof(f1094,plain,
( e0 = e3
| ~ spl14_38
| ~ spl14_59 ),
inference(forward_demodulation,[],[f669,f562]) ).
fof(f1095,plain,
( $false
| ~ spl14_38
| ~ spl14_59 ),
inference(forward_subsumption_resolution,[],[f1094,f153]) ).
fof(f1096,plain,
( ~ spl14_38
| ~ spl14_59 ),
inference(avatar_contradiction_clause,[],[f1095]) ).
fof(f1108,plain,
( e0 = e3
| ~ spl14_58
| ~ spl14_75 ),
inference(superposition,[],[f787,f663]) ).
fof(f1112,plain,
( $false
| ~ spl14_58
| ~ spl14_75 ),
inference(forward_subsumption_resolution,[],[f1108,f153]) ).
fof(f1113,plain,
( ~ spl14_58
| ~ spl14_75 ),
inference(avatar_contradiction_clause,[],[f1112]) ).
fof(f1121,plain,
( e2 = e3
| ~ spl14_38
| ~ spl14_100 ),
inference(forward_demodulation,[],[f939,f562]) ).
fof(f1122,plain,
( $false
| ~ spl14_38
| ~ spl14_100 ),
inference(forward_subsumption_resolution,[],[f1121,f150]) ).
fof(f1123,plain,
( ~ spl14_38
| ~ spl14_100 ),
inference(avatar_contradiction_clause,[],[f1122]) ).
fof(f1159,plain,
( e2 = e3
| ~ spl14_75
| ~ spl14_102 ),
inference(superposition,[],[f787,f948]) ).
fof(f1163,plain,
( $false
| ~ spl14_75
| ~ spl14_102 ),
inference(forward_subsumption_resolution,[],[f1159,f150]) ).
fof(f1164,plain,
( ~ spl14_75
| ~ spl14_102 ),
inference(avatar_contradiction_clause,[],[f1163]) ).
fof(f1166,plain,
( e2 != op(e1,e0)
| spl14_8
| ~ spl14_27 ),
inference(forward_demodulation,[],[f421,f506]) ).
fof(f1169,plain,
( e2 != op(e1,e1)
| spl14_2
| ~ spl14_27 ),
inference(forward_demodulation,[],[f395,f506]) ).
fof(f1172,plain,
( e1 = e3
| ~ spl14_1
| ~ spl14_27 ),
inference(superposition,[],[f390,f506]) ).
fof(f1177,plain,
( $false
| ~ spl14_1
| ~ spl14_27 ),
inference(forward_subsumption_resolution,[],[f1172,f151]) ).
fof(f1178,plain,
( ~ spl14_1
| ~ spl14_27 ),
inference(avatar_contradiction_clause,[],[f1177]) ).
fof(f1189,plain,
( ~ spl14_101
| spl14_8
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1166,f505,f419,f942]) ).
fof(f1191,plain,
( e0 = e3
| ~ spl14_49
| ~ spl14_115 ),
inference(forward_demodulation,[],[f1011,f618]) ).
fof(f1192,plain,
( $false
| ~ spl14_49
| ~ spl14_115 ),
inference(forward_subsumption_resolution,[],[f1191,f153]) ).
fof(f1193,plain,
( ~ spl14_49
| ~ spl14_115 ),
inference(avatar_contradiction_clause,[],[f1192]) ).
fof(f1201,plain,
( e2 = e3
| ~ spl14_68
| ~ spl14_106 ),
inference(superposition,[],[f966,f735]) ).
fof(f1206,plain,
( $false
| ~ spl14_68
| ~ spl14_106 ),
inference(forward_subsumption_resolution,[],[f1201,f150]) ).
fof(f1207,plain,
( ~ spl14_68
| ~ spl14_106 ),
inference(avatar_contradiction_clause,[],[f1206]) ).
fof(f1209,plain,
( e0 = e1
| ~ spl14_27
| ~ spl14_41 ),
inference(superposition,[],[f577,f506]) ).
fof(f1215,plain,
( $false
| ~ spl14_27
| ~ spl14_41 ),
inference(forward_subsumption_resolution,[],[f1209,f155]) ).
fof(f1216,plain,
( ~ spl14_27
| ~ spl14_41 ),
inference(avatar_contradiction_clause,[],[f1215]) ).
fof(f1244,plain,
( e0 = e1
| ~ spl14_66
| ~ spl14_108 ),
inference(superposition,[],[f975,f721]) ).
fof(f1249,plain,
( $false
| ~ spl14_66
| ~ spl14_108 ),
inference(forward_subsumption_resolution,[],[f1244,f155]) ).
fof(f1250,plain,
( ~ spl14_66
| ~ spl14_108 ),
inference(avatar_contradiction_clause,[],[f1249]) ).
fof(f1268,plain,
( e1 = e2
| ~ spl14_98
| ~ spl14_102 ),
inference(forward_demodulation,[],[f930,f948]) ).
fof(f1269,plain,
( $false
| ~ spl14_98
| ~ spl14_102 ),
inference(forward_subsumption_resolution,[],[f1268,f152]) ).
fof(f1270,plain,
( ~ spl14_98
| ~ spl14_102 ),
inference(avatar_contradiction_clause,[],[f1269]) ).
fof(f1279,plain,
( e0 = e1
| ~ spl14_51
| ~ spl14_109 ),
inference(superposition,[],[f980,f628]) ).
fof(f1283,plain,
( $false
| ~ spl14_51
| ~ spl14_109 ),
inference(forward_subsumption_resolution,[],[f1279,f155]) ).
fof(f1284,plain,
( ~ spl14_51
| ~ spl14_109 ),
inference(avatar_contradiction_clause,[],[f1283]) ).
fof(f1287,plain,
( e1 = e2
| ~ spl14_51
| ~ spl14_70 ),
inference(superposition,[],[f749,f628]) ).
fof(f1291,plain,
( $false
| ~ spl14_51
| ~ spl14_70 ),
inference(forward_subsumption_resolution,[],[f1287,f152]) ).
fof(f1292,plain,
( ~ spl14_51
| ~ spl14_70 ),
inference(avatar_contradiction_clause,[],[f1291]) ).
fof(f1300,plain,
( e0 = e1
| ~ spl14_28
| ~ spl14_35 ),
inference(forward_demodulation,[],[f511,f545]) ).
fof(f1302,plain,
( e1 = e3
| ~ spl14_4
| ~ spl14_45 ),
inference(forward_demodulation,[],[f598,f403]) ).
fof(f1304,plain,
( $false
| ~ spl14_28
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f1300,f155]) ).
fof(f1305,plain,
( ~ spl14_28
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f1304]) ).
fof(f1306,plain,
( $false
| ~ spl14_4
| ~ spl14_45 ),
inference(forward_subsumption_resolution,[],[f1302,f151]) ).
fof(f1307,plain,
( ~ spl14_4
| ~ spl14_45 ),
inference(avatar_contradiction_clause,[],[f1306]) ).
fof(f1310,plain,
( e2 = e3
| ~ spl14_49
| ~ spl14_73 ),
inference(forward_demodulation,[],[f773,f618]) ).
fof(f1311,plain,
( $false
| ~ spl14_49
| ~ spl14_73 ),
inference(forward_subsumption_resolution,[],[f1310,f150]) ).
fof(f1312,plain,
( ~ spl14_49
| ~ spl14_73 ),
inference(avatar_contradiction_clause,[],[f1311]) ).
fof(f1376,plain,
( e1 = e3
| ~ spl14_75
| ~ spl14_98 ),
inference(superposition,[],[f787,f930]) ).
fof(f1378,plain,
( e1 = e3
| ~ spl14_75
| ~ spl14_98 ),
inference(superposition,[],[f930,f787]) ).
fof(f1380,plain,
( $false
| ~ spl14_75
| ~ spl14_98 ),
inference(forward_subsumption_resolution,[],[f1378,f151]) ).
fof(f1381,plain,
( ~ spl14_75
| ~ spl14_98 ),
inference(avatar_contradiction_clause,[],[f1380]) ).
fof(f1382,plain,
( $false
| ~ spl14_75
| ~ spl14_98 ),
inference(forward_subsumption_resolution,[],[f1376,f151]) ).
fof(f1383,plain,
( ~ spl14_75
| ~ spl14_98 ),
inference(avatar_contradiction_clause,[],[f1382]) ).
fof(f1388,plain,
( e0 = e3
| ~ spl14_77
| ~ spl14_110 ),
inference(forward_demodulation,[],[f984,f801]) ).
fof(f1389,plain,
( $false
| ~ spl14_77
| ~ spl14_110 ),
inference(forward_subsumption_resolution,[],[f1388,f153]) ).
fof(f1390,plain,
( ~ spl14_77
| ~ spl14_110 ),
inference(avatar_contradiction_clause,[],[f1389]) ).
fof(f1406,plain,
( e1 = e2
| ~ spl14_66
| ~ spl14_111 ),
inference(superposition,[],[f991,f721]) ).
fof(f1412,plain,
( $false
| ~ spl14_66
| ~ spl14_111 ),
inference(forward_subsumption_resolution,[],[f1406,f152]) ).
fof(f1413,plain,
( ~ spl14_66
| ~ spl14_111 ),
inference(avatar_contradiction_clause,[],[f1412]) ).
fof(f1414,plain,
( e0 = e2
| ~ spl14_21
| ~ spl14_36 ),
inference(superposition,[],[f479,f551]) ).
fof(f1415,plain,
( e0 = e2
| ~ spl14_21
| ~ spl14_36 ),
inference(superposition,[],[f551,f479]) ).
fof(f1418,plain,
( $false
| ~ spl14_21
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f1415,f154]) ).
fof(f1419,plain,
( ~ spl14_21
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f1418]) ).
fof(f1420,plain,
( $false
| ~ spl14_21
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f1414,f154]) ).
fof(f1421,plain,
( ~ spl14_21
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f1420]) ).
fof(f1443,plain,
( e0 = e2
| ~ spl14_110
| ~ spl14_112 ),
inference(superposition,[],[f996,f984]) ).
fof(f1449,plain,
( $false
| ~ spl14_110
| ~ spl14_112 ),
inference(forward_subsumption_resolution,[],[f1443,f154]) ).
fof(f1450,plain,
( ~ spl14_110
| ~ spl14_112 ),
inference(avatar_contradiction_clause,[],[f1449]) ).
fof(f1461,plain,
( e0 = e1
| ~ spl14_116
| ~ spl14_118 ),
inference(forward_demodulation,[],[f1026,f1016]) ).
fof(f1462,plain,
( $false
| ~ spl14_116
| ~ spl14_118 ),
inference(forward_subsumption_resolution,[],[f1461,f155]) ).
fof(f1463,plain,
( ~ spl14_116
| ~ spl14_118 ),
inference(avatar_contradiction_clause,[],[f1462]) ).
fof(f1464,plain,
( e1 = e2
| ~ spl14_21
| ~ spl14_30 ),
inference(forward_demodulation,[],[f521,f479]) ).
fof(f1467,plain,
( $false
| ~ spl14_21
| ~ spl14_30 ),
inference(forward_subsumption_resolution,[],[f1464,f152]) ).
fof(f1468,plain,
( ~ spl14_21
| ~ spl14_30 ),
inference(avatar_contradiction_clause,[],[f1467]) ).
fof(f1476,plain,
( e2 != op(e3,e1)
| ~ spl14_21 ),
inference(forward_demodulation,[],[f103,f479]) ).
fof(f1478,plain,
( e2 != op(e3,e0)
| ~ spl14_21 ),
inference(forward_demodulation,[],[f105,f479]) ).
fof(f1479,plain,
( e1 != op(e3,e0)
| ~ spl14_118 ),
inference(forward_demodulation,[],[f106,f1026]) ).
fof(f1482,plain,
( e3 != op(e2,e2)
| ~ spl14_49 ),
inference(forward_demodulation,[],[f108,f618]) ).
fof(f1493,plain,
( e1 != op(e1,e1)
| ~ spl14_66 ),
inference(forward_demodulation,[],[f115,f721]) ).
fof(f1495,plain,
( e2 != op(e1,e1)
| ~ spl14_44 ),
inference(forward_demodulation,[],[f116,f593]) ).
fof(f1497,plain,
( e1 != op(e1,e0)
| ~ spl14_66 ),
inference(forward_demodulation,[],[f117,f721]) ).
fof(f1500,plain,
( e3 != op(e1,e0)
| ~ spl14_4 ),
inference(forward_demodulation,[],[f119,f403]) ).
fof(f1503,plain,
( e0 != op(e0,e1)
| ~ spl14_59 ),
inference(forward_demodulation,[],[f121,f669]) ).
fof(f1505,plain,
( e0 != op(e0,e0)
| ~ spl14_59 ),
inference(forward_demodulation,[],[f123,f669]) ).
fof(f1506,plain,
( op(e0,e0) != e3
| ~ spl14_104 ),
inference(forward_demodulation,[],[f124,f957]) ).
fof(f1512,plain,
( e2 != op(e0,e3)
| ~ spl14_21 ),
inference(forward_demodulation,[],[f129,f479]) ).
fof(f1514,plain,
( e1 != op(e0,e3)
| ~ spl14_66 ),
inference(forward_demodulation,[],[f131,f721]) ).
fof(f1516,plain,
( e1 != op(e2,e2)
| ~ spl14_118 ),
inference(forward_demodulation,[],[f132,f1026]) ).
fof(f1519,plain,
( e0 != op(e1,e2)
| ~ spl14_35 ),
inference(forward_demodulation,[],[f134,f545]) ).
fof(f1522,plain,
( e0 != op(e0,e2)
| ~ spl14_35 ),
inference(forward_demodulation,[],[f136,f545]) ).
fof(f1524,plain,
( e2 != op(e0,e2)
| ~ spl14_44 ),
inference(forward_demodulation,[],[f137,f593]) ).
fof(f1525,plain,
( e0 != op(e2,e1)
| ~ spl14_110 ),
inference(forward_demodulation,[],[f138,f984]) ).
fof(f1526,plain,
( e0 != op(e1,e1)
| ~ spl14_110 ),
inference(forward_demodulation,[],[f139,f984]) ).
fof(f1528,plain,
( e1 != op(e1,e1)
| ~ spl14_51 ),
inference(forward_demodulation,[],[f140,f628]) ).
fof(f1532,plain,
( e3 != op(e0,e1)
| ~ spl14_4 ),
inference(forward_demodulation,[],[f143,f403]) ).
fof(f1536,plain,
( op(e0,e0) != e3
| ~ spl14_75 ),
inference(forward_demodulation,[],[f147,f787]) ).
fof(f1537,plain,
( op(e0,e0) != e2
| ~ spl14_68 ),
inference(forward_demodulation,[],[f148,f735]) ).
fof(f1538,plain,
( e0 != op(e0,e0)
| ~ spl14_46 ),
inference(forward_demodulation,[],[f149,f603]) ).
fof(f1542,plain,
( e3 != op(e1,e0)
| spl14_20
| ~ spl14_27 ),
inference(forward_demodulation,[],[f475,f506]) ).
fof(f1543,plain,
( e0 != op(e2,e3)
| ~ spl14_21
| spl14_23 ),
inference(forward_demodulation,[],[f488,f479]) ).
fof(f1545,plain,
( e1 != op(e2,e3)
| ~ spl14_21
| spl14_26 ),
inference(forward_demodulation,[],[f502,f479]) ).
fof(f1551,plain,
( e2 != op(e3,e3)
| ~ spl14_4
| spl14_5 ),
inference(forward_demodulation,[],[f408,f403]) ).
fof(f1555,plain,
( e0 != op(e3,e1)
| ~ spl14_4
| spl14_6 ),
inference(forward_demodulation,[],[f412,f403]) ).
fof(f1556,plain,
( $false
| ~ spl14_4
| spl14_6
| ~ spl14_110 ),
inference(forward_subsumption_resolution,[],[f1555,f984]) ).
fof(f1557,plain,
( ~ spl14_4
| spl14_6
| ~ spl14_110 ),
inference(avatar_contradiction_clause,[],[f1556]) ).
fof(f1559,plain,
( ~ spl14_21
| ~ spl14_4
| spl14_5 ),
inference(avatar_split_clause,[],[f1551,f406,f402,f478]) ).
fof(f1562,plain,
( e3 != op(e3,e1)
| ~ spl14_4 ),
inference(forward_demodulation,[],[f139,f403]) ).
fof(f1563,plain,
( e1 != op(e0,e1)
| ~ spl14_27 ),
inference(forward_demodulation,[],[f125,f506]) ).
fof(f1564,plain,
( ~ spl14_47
| ~ spl14_59 ),
inference(avatar_split_clause,[],[f1503,f667,f607]) ).
fof(f1566,plain,
( e3 != op(e3,e3)
| ~ spl14_75 ),
inference(forward_demodulation,[],[f105,f787]) ).
fof(f1568,plain,
( e1 != op(e3,e3)
| ~ spl14_66 ),
inference(forward_demodulation,[],[f127,f721]) ).
fof(f1569,plain,
( e0 != op(e3,e3)
| ~ spl14_59 ),
inference(forward_demodulation,[],[f129,f669]) ).
fof(f1571,plain,
( ~ spl14_30
| ~ spl14_66 ),
inference(avatar_split_clause,[],[f1568,f719,f520]) ).
fof(f1572,plain,
( ~ spl14_36
| ~ spl14_59 ),
inference(avatar_split_clause,[],[f1569,f667,f550]) ).
fof(f1573,plain,
( e3 != op(e0,e3)
| ~ spl14_104 ),
inference(forward_demodulation,[],[f120,f957]) ).
fof(f1574,plain,
( e1 != op(e0,e3)
| ~ spl14_27 ),
inference(forward_demodulation,[],[f123,f506]) ).
fof(f1575,plain,
( ~ spl14_96
| ~ spl14_66 ),
inference(avatar_split_clause,[],[f1514,f719,f919]) ).
fof(f1576,plain,
( ~ spl14_96
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1574,f505,f919]) ).
fof(f1589,plain,
( e0 != op(e3,e1)
| ~ spl14_36 ),
inference(forward_demodulation,[],[f103,f551]) ).
fof(f1594,plain,
( e1 != op(e0,e3)
| spl14_26
| ~ spl14_36 ),
inference(forward_demodulation,[],[f502,f551]) ).
fof(f1595,plain,
( e2 != op(e0,e3)
| spl14_33
| ~ spl14_36 ),
inference(forward_demodulation,[],[f536,f551]) ).
fof(f1598,plain,
( op(e0,e0) != e1
| spl14_22
| ~ spl14_36 ),
inference(forward_demodulation,[],[f484,f551]) ).
fof(f1604,plain,
( e3 != op(e3,e2)
| ~ spl14_75 ),
inference(forward_demodulation,[],[f106,f787]) ).
fof(f1605,plain,
( e0 != op(e3,e2)
| ~ spl14_35 ),
inference(forward_demodulation,[],[f132,f545]) ).
fof(f1608,plain,
( e1 != op(e0,e2)
| ~ spl14_27 ),
inference(forward_demodulation,[],[f124,f506]) ).
fof(f1609,plain,
( ~ spl14_53
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f1522,f544,f637]) ).
fof(f1611,plain,
( ~ spl14_103
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f1532,f402,f951]) ).
fof(f1613,plain,
( ~ spl14_55
| ~ spl14_75 ),
inference(avatar_split_clause,[],[f1566,f785,f647]) ).
fof(f1614,plain,
( e0 != op(e2,e3)
| ~ spl14_35 ),
inference(forward_demodulation,[],[f108,f545]) ).
fof(f1616,plain,
( e2 != op(e2,e3)
| ~ spl14_68 ),
inference(forward_demodulation,[],[f111,f735]) ).
fof(f1617,plain,
( e1 != op(e2,e3)
| ~ spl14_66 ),
inference(forward_demodulation,[],[f128,f721]) ).
fof(f1623,plain,
( ~ spl14_78
| ~ spl14_75 ),
inference(avatar_split_clause,[],[f1604,f785,f809]) ).
fof(f1624,plain,
( ~ spl14_116
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f1605,f544,f1014]) ).
fof(f1626,plain,
( ~ spl14_95
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1608,f505,f915]) ).
fof(f1627,plain,
( ~ spl14_115
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f1614,f544,f1009]) ).
fof(f1629,plain,
( ~ spl14_73
| ~ spl14_68 ),
inference(avatar_split_clause,[],[f1616,f733,f771]) ).
fof(f1630,plain,
( ~ spl14_117
| ~ spl14_66 ),
inference(avatar_split_clause,[],[f1617,f719,f1019]) ).
fof(f1635,plain,
( ~ spl14_105
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f1500,f402,f960]) ).
fof(f1636,plain,
( ~ spl14_105
| spl14_20
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1542,f505,f473,f960]) ).
fof(f1639,plain,
( e1 != op(e3,e0)
| ~ spl14_27 ),
inference(forward_demodulation,[],[f147,f506]) ).
fof(f1640,plain,
( e3 != op(e1,e3)
| ~ spl14_4 ),
inference(forward_demodulation,[],[f115,f403]) ).
fof(f1643,plain,
( e3 != op(e2,e1)
| ~ spl14_4 ),
inference(forward_demodulation,[],[f140,f403]) ).
fof(f1646,plain,
( e1 != op(e1,e0)
| ~ spl14_27 ),
inference(forward_demodulation,[],[f149,f506]) ).
fof(f1647,plain,
( e3 != op(e1,e2)
| ~ spl14_4 ),
inference(forward_demodulation,[],[f116,f403]) ).
fof(f1649,plain,
( ~ spl14_98
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1639,f505,f928]) ).
fof(f1651,plain,
( ~ spl14_114
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f1643,f402,f1004]) ).
fof(f1652,plain,
( ~ spl14_61
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1646,f505,f681]) ).
fof(f1655,plain,
( ~ spl14_18
| spl14_2
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1169,f505,f393,f464]) ).
fof(f1656,plain,
( e0 != op(e1,e1)
| ~ spl14_47 ),
inference(forward_demodulation,[],[f143,f609]) ).
fof(f1658,plain,
( ~ spl14_34
| ~ spl14_47 ),
inference(avatar_split_clause,[],[f1656,f607,f539]) ).
fof(f1660,plain,
( e0 != op(e0,e0)
| ~ spl14_47 ),
inference(forward_demodulation,[],[f125,f609]) ).
fof(f1661,plain,
( op(e0,e0) != e2
| ~ spl14_100 ),
inference(forward_demodulation,[],[f123,f939]) ).
fof(f1662,plain,
( ~ spl14_16
| ~ spl14_68 ),
inference(avatar_split_clause,[],[f1537,f733,f455]) ).
fof(f1665,plain,
( ~ spl14_16
| ~ spl14_100 ),
inference(avatar_split_clause,[],[f1661,f937,f455]) ).
fof(f1683,plain,
( e2 = e3
| ~ spl14_56
| ~ spl14_78 ),
inference(superposition,[],[f811,f653]) ).
fof(f1687,plain,
( $false
| ~ spl14_56
| ~ spl14_78 ),
inference(forward_subsumption_resolution,[],[f1683,f150]) ).
fof(f1688,plain,
( ~ spl14_56
| ~ spl14_78 ),
inference(avatar_contradiction_clause,[],[f1687]) ).
fof(f1695,plain,
( e1 = e2
| ~ spl14_68
| ~ spl14_97 ),
inference(forward_demodulation,[],[f926,f735]) ).
fof(f1697,plain,
( $false
| ~ spl14_68
| ~ spl14_97 ),
inference(forward_subsumption_resolution,[],[f1695,f152]) ).
fof(f1698,plain,
( ~ spl14_68
| ~ spl14_97 ),
inference(avatar_contradiction_clause,[],[f1697]) ).
fof(f1699,plain,
( e2 = e3
| ~ spl14_1
| ~ spl14_16 ),
inference(forward_demodulation,[],[f456,f390]) ).
fof(f1703,plain,
( e3 != op(e0,e3)
| ~ spl14_1 ),
inference(forward_demodulation,[],[f123,f390]) ).
fof(f1704,plain,
( e3 != op(e2,e0)
| ~ spl14_1 ),
inference(forward_demodulation,[],[f148,f390]) ).
fof(f1707,plain,
( e1 != op(e0,e1)
| ~ spl14_57 ),
inference(forward_demodulation,[],[f141,f658]) ).
fof(f1708,plain,
( e2 != op(e0,e1)
| ~ spl14_18 ),
inference(forward_demodulation,[],[f143,f465]) ).
fof(f1709,plain,
( e3 != op(e0,e1)
| ~ spl14_1 ),
inference(forward_demodulation,[],[f125,f390]) ).
fof(f1713,plain,
( $false
| ~ spl14_1
| ~ spl14_16 ),
inference(forward_subsumption_resolution,[],[f1699,f150]) ).
fof(f1714,plain,
( ~ spl14_1
| ~ spl14_16 ),
inference(avatar_contradiction_clause,[],[f1713]) ).
fof(f1718,plain,
( ~ spl14_103
| ~ spl14_1 ),
inference(avatar_split_clause,[],[f1709,f389,f951]) ).
fof(f1757,plain,
( e1 = e3
| ~ spl14_64
| ~ spl14_113 ),
inference(superposition,[],[f1001,f707]) ).
fof(f1763,plain,
( $false
| ~ spl14_64
| ~ spl14_113 ),
inference(forward_subsumption_resolution,[],[f1757,f151]) ).
fof(f1764,plain,
( ~ spl14_64
| ~ spl14_113 ),
inference(avatar_contradiction_clause,[],[f1763]) ).
fof(f1766,plain,
( e2 = e3
| ~ spl14_70
| ~ spl14_114 ),
inference(superposition,[],[f1006,f749]) ).
fof(f1772,plain,
( $false
| ~ spl14_70
| ~ spl14_114 ),
inference(forward_subsumption_resolution,[],[f1766,f150]) ).
fof(f1773,plain,
( ~ spl14_70
| ~ spl14_114 ),
inference(avatar_contradiction_clause,[],[f1772]) ).
fof(f1783,plain,
( e3 != op(e3,e2)
| ~ spl14_55 ),
inference(forward_demodulation,[],[f102,f648]) ).
fof(f1784,plain,
( e3 != op(e3,e1)
| ~ spl14_55 ),
inference(forward_demodulation,[],[f103,f648]) ).
fof(f1788,plain,
( e1 != op(e3,e0)
| ~ spl14_57 ),
inference(forward_demodulation,[],[f107,f658]) ).
fof(f1793,plain,
( e3 != op(e2,e1)
| ~ spl14_9 ),
inference(forward_demodulation,[],[f110,f425]) ).
fof(f1795,plain,
( e3 != op(e2,e0)
| ~ spl14_9 ),
inference(forward_demodulation,[],[f112,f425]) ).
fof(f1798,plain,
( e2 != op(e1,e1)
| ~ spl14_111 ),
inference(forward_demodulation,[],[f115,f991]) ).
fof(f1799,plain,
( e1 != op(e1,e1)
| ~ spl14_64 ),
inference(forward_demodulation,[],[f116,f707]) ).
fof(f1824,plain,
( e1 != op(e1,e1)
| ~ spl14_57 ),
inference(forward_demodulation,[],[f139,f658]) ).
fof(f1826,plain,
( e2 != op(e1,e1)
| ~ spl14_70 ),
inference(forward_demodulation,[],[f140,f749]) ).
fof(f1829,plain,
( e0 != op(e1,e0)
| ~ spl14_58 ),
inference(forward_demodulation,[],[f145,f663]) ).
fof(f1831,plain,
( e0 != op(e0,e0)
| ~ spl14_58 ),
inference(forward_demodulation,[],[f147,f663]) ).
fof(f1832,plain,
( op(e0,e0) != e1
| ~ spl14_97 ),
inference(forward_demodulation,[],[f148,f926]) ).
fof(f1834,plain,
( op(e0,e0) != e3
| ~ spl14_105 ),
inference(forward_demodulation,[],[f149,f962]) ).
fof(f1835,plain,
( e1 != op(e2,e0)
| spl14_3
| ~ spl14_16 ),
inference(forward_demodulation,[],[f399,f456]) ).
fof(f1843,plain,
( e3 != op(e2,e0)
| ~ spl14_16
| spl14_20 ),
inference(forward_demodulation,[],[f475,f456]) ).
fof(f1850,plain,
( op(e0,e0) != e2
| spl14_5
| ~ spl14_34 ),
inference(forward_demodulation,[],[f408,f540]) ).
fof(f1854,plain,
( e3 != op(e0,e1)
| spl14_24
| ~ spl14_34 ),
inference(forward_demodulation,[],[f493,f540]) ).
fof(f1857,plain,
( e2 != op(e0,e1)
| ~ spl14_16 ),
inference(forward_demodulation,[],[f125,f456]) ).
fof(f1858,plain,
( ~ spl14_103
| spl14_24
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f1854,f539,f491,f951]) ).
fof(f1859,plain,
( ~ spl14_77
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f1784,f647,f799]) ).
fof(f1860,plain,
( ~ spl14_40
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f1707,f657,f571]) ).
fof(f1863,plain,
( e1 != op(e1,e3)
| ~ spl14_64 ),
inference(forward_demodulation,[],[f114,f707]) ).
fof(f1868,plain,
( e1 != op(e2,e1)
| ~ spl14_97 ),
inference(forward_demodulation,[],[f113,f926]) ).
fof(f1869,plain,
( ~ spl14_45
| ~ spl14_64 ),
inference(avatar_split_clause,[],[f1799,f705,f597]) ).
fof(f1871,plain,
( ~ spl14_45
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f1824,f657,f597]) ).
fof(f1873,plain,
( e1 != op(e2,e3)
| ~ spl14_97 ),
inference(forward_demodulation,[],[f111,f926]) ).
fof(f1875,plain,
( ~ spl14_117
| ~ spl14_97 ),
inference(avatar_split_clause,[],[f1873,f924,f1019]) ).
fof(f1894,plain,
( e2 != op(e2,e1)
| ~ spl14_73 ),
inference(forward_demodulation,[],[f109,f773]) ).
fof(f1895,plain,
( e0 != op(e1,e1)
| ~ spl14_108 ),
inference(forward_demodulation,[],[f115,f975]) ).
fof(f1898,plain,
( e0 != op(e1,e1)
| ~ spl14_109 ),
inference(forward_demodulation,[],[f140,f980]) ).
fof(f1913,plain,
( e0 != op(e3,e1)
| ~ spl14_58 ),
inference(forward_demodulation,[],[f107,f663]) ).
fof(f1919,plain,
( ~ spl14_34
| ~ spl14_108 ),
inference(avatar_split_clause,[],[f1895,f973,f539]) ).
fof(f1920,plain,
( ~ spl14_34
| ~ spl14_109 ),
inference(avatar_split_clause,[],[f1898,f978,f539]) ).
fof(f1923,plain,
( ~ spl14_18
| ~ spl14_70 ),
inference(avatar_split_clause,[],[f1826,f747,f464]) ).
fof(f1925,plain,
( ~ spl14_18
| ~ spl14_111 ),
inference(avatar_split_clause,[],[f1798,f989,f464]) ).
fof(f1927,plain,
( e0 = e2
| ~ spl14_73
| ~ spl14_115 ),
inference(forward_demodulation,[],[f1011,f773]) ).
fof(f1930,plain,
( ~ spl14_70
| ~ spl14_73 ),
inference(avatar_split_clause,[],[f1894,f771,f747]) ).
fof(f1931,plain,
( $false
| ~ spl14_73
| ~ spl14_115 ),
inference(forward_subsumption_resolution,[],[f1927,f154]) ).
fof(f1932,plain,
( ~ spl14_73
| ~ spl14_115 ),
inference(avatar_contradiction_clause,[],[f1931]) ).
fof(f1966,plain,
( e1 != op(e0,e3)
| ~ spl14_30 ),
inference(forward_demodulation,[],[f129,f521]) ).
fof(f1976,plain,
( e0 != op(e1,e3)
| spl14_23
| ~ spl14_30 ),
inference(forward_demodulation,[],[f488,f521]) ).
fof(f1979,plain,
( e2 != op(e1,e3)
| ~ spl14_30
| spl14_33 ),
inference(forward_demodulation,[],[f536,f521]) ).
fof(f1982,plain,
( e0 != op(e1,e1)
| spl14_25
| ~ spl14_30 ),
inference(forward_demodulation,[],[f498,f521]) ).
fof(f1989,plain,
( e0 = e1
| ~ spl14_53
| ~ spl14_95 ),
inference(forward_demodulation,[],[f917,f639]) ).
fof(f1998,plain,
( ~ spl14_108
| spl14_23
| ~ spl14_30 ),
inference(avatar_split_clause,[],[f1976,f520,f486,f973]) ).
fof(f1999,plain,
( ~ spl14_99
| ~ spl14_16 ),
inference(avatar_split_clause,[],[f1857,f455,f933]) ).
fof(f2004,plain,
( ~ spl14_34
| spl14_25
| ~ spl14_30 ),
inference(avatar_split_clause,[],[f1982,f520,f496,f539]) ).
fof(f2005,plain,
( $false
| ~ spl14_53
| ~ spl14_95 ),
inference(forward_subsumption_resolution,[],[f1989,f155]) ).
fof(f2006,plain,
( ~ spl14_53
| ~ spl14_95 ),
inference(avatar_contradiction_clause,[],[f2005]) ).
fof(f2008,plain,
( e1 = e3
| ~ spl14_9
| ~ spl14_28 ),
inference(forward_demodulation,[],[f511,f425]) ).
fof(f2009,plain,
( e2 != op(e1,e1)
| ~ spl14_30
| spl14_31 ),
inference(forward_demodulation,[],[f526,f521]) ).
fof(f2011,plain,
( ~ spl14_111
| ~ spl14_30
| spl14_33 ),
inference(avatar_split_clause,[],[f1979,f534,f520,f989]) ).
fof(f2013,plain,
( e2 = e3
| ~ spl14_77
| ~ spl14_112 ),
inference(forward_demodulation,[],[f996,f801]) ).
fof(f2015,plain,
( e3 != op(e3,e2)
| ~ spl14_9 ),
inference(forward_demodulation,[],[f132,f425]) ).
fof(f2016,plain,
( e3 != op(e3,e2)
| ~ spl14_77 ),
inference(forward_demodulation,[],[f104,f801]) ).
fof(f2021,plain,
( $false
| ~ spl14_9
| ~ spl14_28 ),
inference(forward_subsumption_resolution,[],[f2008,f151]) ).
fof(f2022,plain,
( ~ spl14_9
| ~ spl14_28 ),
inference(avatar_contradiction_clause,[],[f2021]) ).
fof(f2023,plain,
( $false
| ~ spl14_77
| ~ spl14_112 ),
inference(forward_subsumption_resolution,[],[f2013,f150]) ).
fof(f2024,plain,
( ~ spl14_77
| ~ spl14_112 ),
inference(avatar_contradiction_clause,[],[f2023]) ).
fof(f2027,plain,
( e1 != op(e2,e2)
| ~ spl14_97 ),
inference(forward_demodulation,[],[f112,f926]) ).
fof(f2029,plain,
( ~ spl14_28
| ~ spl14_97 ),
inference(avatar_split_clause,[],[f2027,f924,f510]) ).
fof(f2030,plain,
( ~ spl14_38
| ~ spl14_1 ),
inference(avatar_split_clause,[],[f1703,f389,f561]) ).
fof(f2031,plain,
( ~ spl14_106
| ~ spl14_1 ),
inference(avatar_split_clause,[],[f1704,f389,f964]) ).
fof(f2035,plain,
( e1 != op(e3,e0)
| ~ spl14_30 ),
inference(forward_demodulation,[],[f105,f521]) ).
fof(f2036,plain,
( ~ spl14_39
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f1524,f592,f566]) ).
fof(f2037,plain,
( ~ spl14_96
| ~ spl14_30 ),
inference(avatar_split_clause,[],[f1966,f520,f919]) ).
fof(f2038,plain,
( ~ spl14_98
| ~ spl14_30 ),
inference(avatar_split_clause,[],[f2035,f520,f928]) ).
fof(f2039,plain,
( ~ spl14_78
| ~ spl14_9 ),
inference(avatar_split_clause,[],[f2015,f424,f809]) ).
fof(f2041,plain,
( ~ spl14_114
| ~ spl14_9 ),
inference(avatar_split_clause,[],[f1793,f424,f1004]) ).
fof(f2042,plain,
( ~ spl14_106
| ~ spl14_9 ),
inference(avatar_split_clause,[],[f1795,f424,f964]) ).
fof(f2044,plain,
( ~ spl14_78
| ~ spl14_77 ),
inference(avatar_split_clause,[],[f2016,f799,f809]) ).
fof(f2047,plain,
( ~ spl14_27
| ~ spl14_97 ),
inference(avatar_split_clause,[],[f1832,f924,f505]) ).
fof(f2104,plain,
( e2 != op(e2,e2)
| ~ spl14_73 ),
inference(forward_demodulation,[],[f108,f773]) ).
fof(f2109,plain,
( e0 != op(e2,e0)
| ~ spl14_109 ),
inference(forward_demodulation,[],[f113,f980]) ).
fof(f2143,plain,
( e2 != op(e1,e0)
| ~ spl14_102 ),
inference(forward_demodulation,[],[f145,f948]) ).
fof(f2145,plain,
( op(e0,e0) != e2
| ~ spl14_102 ),
inference(forward_demodulation,[],[f147,f948]) ).
fof(f2150,plain,
( e1 != op(e3,e0)
| ~ spl14_1
| spl14_3 ),
inference(forward_demodulation,[],[f399,f390]) ).
fof(f2151,plain,
( e2 != op(e3,e0)
| ~ spl14_1
| spl14_8 ),
inference(forward_demodulation,[],[f421,f390]) ).
fof(f2161,plain,
( e1 != op(e3,e3)
| ~ spl14_1
| spl14_7 ),
inference(forward_demodulation,[],[f417,f390]) ).
fof(f2162,plain,
( $false
| ~ spl14_1
| spl14_7
| ~ spl14_30 ),
inference(forward_subsumption_resolution,[],[f2161,f521]) ).
fof(f2163,plain,
( ~ spl14_1
| spl14_7
| ~ spl14_30 ),
inference(avatar_contradiction_clause,[],[f2162]) ).
fof(f2164,plain,
( ~ spl14_99
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f1708,f464,f933]) ).
fof(f2171,plain,
( ~ spl14_1
| ~ spl14_105 ),
inference(avatar_split_clause,[],[f1834,f960,f389]) ).
fof(f2174,plain,
( e0 = e3
| ~ spl14_43
| ~ spl14_108 ),
inference(forward_demodulation,[],[f975,f588]) ).
fof(f2177,plain,
( ~ spl14_52
| ~ spl14_109 ),
inference(avatar_split_clause,[],[f2109,f978,f632]) ).
fof(f2180,plain,
( ~ spl14_18
| ~ spl14_30
| spl14_31 ),
inference(avatar_split_clause,[],[f2009,f524,f520,f464]) ).
fof(f2181,plain,
( ~ spl14_18
| ~ spl14_44 ),
inference(avatar_split_clause,[],[f1495,f592,f464]) ).
fof(f2183,plain,
( ~ spl14_16
| ~ spl14_102 ),
inference(avatar_split_clause,[],[f2145,f946,f455]) ).
fof(f2187,plain,
( $false
| ~ spl14_43
| ~ spl14_108 ),
inference(forward_subsumption_resolution,[],[f2174,f153]) ).
fof(f2188,plain,
( ~ spl14_43
| ~ spl14_108 ),
inference(avatar_contradiction_clause,[],[f2187]) ).
fof(f2227,plain,
( e1 != op(e3,e3)
| ~ spl14_9
| spl14_10 ),
inference(forward_demodulation,[],[f430,f425]) ).
fof(f2231,plain,
( e0 != op(e3,e2)
| ~ spl14_9
| spl14_11 ),
inference(forward_demodulation,[],[f434,f425]) ).
fof(f2234,plain,
( ~ spl14_102
| ~ spl14_1
| spl14_8 ),
inference(avatar_split_clause,[],[f2151,f419,f389,f946]) ).
fof(f2236,plain,
( ~ spl14_43
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f1640,f402,f587]) ).
fof(f2237,plain,
( ~ spl14_77
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f1562,f402,f799]) ).
fof(f2239,plain,
( ~ spl14_96
| spl14_26
| ~ spl14_36 ),
inference(avatar_split_clause,[],[f1594,f550,f500,f919]) ).
fof(f2240,plain,
( ~ spl14_41
| ~ spl14_46 ),
inference(avatar_split_clause,[],[f1538,f602,f576]) ).
fof(f2241,plain,
( ~ spl14_41
| ~ spl14_47 ),
inference(avatar_split_clause,[],[f1660,f607,f576]) ).
fof(f2242,plain,
( e2 = e3
| ~ spl14_9
| ~ spl14_50 ),
inference(forward_demodulation,[],[f623,f425]) ).
fof(f2243,plain,
( ~ spl14_45
| ~ spl14_51 ),
inference(avatar_split_clause,[],[f1528,f627,f597]) ).
fof(f2246,plain,
( ~ spl14_45
| ~ spl14_66 ),
inference(avatar_split_clause,[],[f1493,f719,f597]) ).
fof(f2248,plain,
( ~ spl14_1
| ~ spl14_75 ),
inference(avatar_split_clause,[],[f1536,f785,f389]) ).
fof(f2257,plain,
( e1 != op(e3,e2)
| ~ spl14_95 ),
inference(forward_demodulation,[],[f135,f917]) ).
fof(f2258,plain,
( ~ spl14_116
| ~ spl14_9
| spl14_11 ),
inference(avatar_split_clause,[],[f2231,f432,f424,f1014]) ).
fof(f2260,plain,
( e1 != op(e3,e0)
| ~ spl14_97 ),
inference(forward_demodulation,[],[f144,f926]) ).
fof(f2263,plain,
( ~ spl14_51
| ~ spl14_97 ),
inference(avatar_split_clause,[],[f1868,f924,f627]) ).
fof(f2266,plain,
( $false
| ~ spl14_9
| ~ spl14_50 ),
inference(forward_subsumption_resolution,[],[f2242,f150]) ).
fof(f2267,plain,
( ~ spl14_9
| ~ spl14_50 ),
inference(avatar_contradiction_clause,[],[f2266]) ).
fof(f2268,plain,
( ~ spl14_118
| ~ spl14_95 ),
inference(avatar_split_clause,[],[f2257,f915,f1024]) ).
fof(f2270,plain,
( ~ spl14_30
| ~ spl14_9
| spl14_10 ),
inference(avatar_split_clause,[],[f2227,f428,f424,f520]) ).
fof(f2271,plain,
( ~ spl14_100
| spl14_33
| ~ spl14_36 ),
inference(avatar_split_clause,[],[f1595,f550,f534,f937]) ).
fof(f2322,plain,
( e2 != op(e3,e0)
| ~ spl14_112 ),
inference(forward_demodulation,[],[f107,f996]) ).
fof(f2328,plain,
( e0 != op(e1,e1)
| ~ spl14_107 ),
inference(forward_demodulation,[],[f116,f971]) ).
fof(f2330,plain,
( e0 != op(e1,e0)
| ~ spl14_107 ),
inference(forward_demodulation,[],[f118,f971]) ).
fof(f2336,plain,
( op(e0,e0) != e2
| ~ spl14_39 ),
inference(forward_demodulation,[],[f124,f567]) ).
fof(f2360,plain,
( op(e0,e0) != e2
| ~ spl14_101 ),
inference(forward_demodulation,[],[f149,f944]) ).
fof(f2370,plain,
( e0 != op(e3,e3)
| ~ spl14_4
| spl14_12 ),
inference(forward_demodulation,[],[f439,f403]) ).
fof(f2374,plain,
( e2 != op(e3,e1)
| ~ spl14_4
| spl14_13 ),
inference(forward_demodulation,[],[f443,f403]) ).
fof(f2375,plain,
( $false
| ~ spl14_4
| spl14_13
| ~ spl14_112 ),
inference(forward_subsumption_resolution,[],[f2374,f996]) ).
fof(f2376,plain,
( ~ spl14_4
| spl14_13
| ~ spl14_112 ),
inference(avatar_contradiction_clause,[],[f2375]) ).
fof(f2386,plain,
( ~ spl14_41
| ~ spl14_58 ),
inference(avatar_split_clause,[],[f1831,f662,f576]) ).
fof(f2394,plain,
( e1 != op(e1,e1)
| ~ spl14_40 ),
inference(forward_demodulation,[],[f143,f572]) ).
fof(f2395,plain,
( ~ spl14_45
| ~ spl14_40 ),
inference(avatar_split_clause,[],[f2394,f571,f597]) ).
fof(f2399,plain,
( ~ spl14_66
| ~ spl14_64 ),
inference(avatar_split_clause,[],[f1863,f705,f719]) ).
fof(f2447,plain,
( e2 != op(e1,e0)
| ~ spl14_18 ),
inference(forward_demodulation,[],[f119,f465]) ).
fof(f2472,plain,
( e3 != op(e2,e1)
| ~ spl14_18
| spl14_24 ),
inference(forward_demodulation,[],[f493,f465]) ).
fof(f2479,plain,
( e0 != op(e2,e2)
| spl14_12
| ~ spl14_18 ),
inference(forward_demodulation,[],[f439,f465]) ).
fof(f2481,plain,
( e0 != op(e3,e3)
| ~ spl14_9
| spl14_14 ),
inference(forward_demodulation,[],[f448,f425]) ).
fof(f2482,plain,
( $false
| ~ spl14_9
| spl14_14
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f2481,f551]) ).
fof(f2483,plain,
( ~ spl14_9
| spl14_14
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f2482]) ).
fof(f2485,plain,
( e1 != op(e3,e2)
| ~ spl14_9
| spl14_15 ),
inference(forward_demodulation,[],[f452,f425]) ).
fof(f2487,plain,
( e3 != op(e2,e2)
| ~ spl14_16
| spl14_17 ),
inference(forward_demodulation,[],[f461,f456]) ).
fof(f2488,plain,
( $false
| ~ spl14_9
| ~ spl14_16
| spl14_17 ),
inference(forward_subsumption_resolution,[],[f2487,f425]) ).
fof(f2489,plain,
( ~ spl14_9
| ~ spl14_16
| spl14_17 ),
inference(avatar_contradiction_clause,[],[f2488]) ).
fof(f2491,plain,
( ~ spl14_97
| spl14_3
| ~ spl14_16 ),
inference(avatar_split_clause,[],[f1835,f455,f397,f924]) ).
fof(f2500,plain,
( ~ spl14_106
| ~ spl14_16
| spl14_20 ),
inference(avatar_split_clause,[],[f1843,f473,f455,f964]) ).
fof(f2502,plain,
( e0 != op(e2,e0)
| ~ spl14_46 ),
inference(forward_demodulation,[],[f146,f603]) ).
fof(f2513,plain,
( e2 != op(e3,e1)
| ~ spl14_18 ),
inference(forward_demodulation,[],[f139,f465]) ).
fof(f2516,plain,
( e0 != op(e2,e2)
| ~ spl14_109 ),
inference(forward_demodulation,[],[f110,f980]) ).
fof(f2520,plain,
( ~ spl14_50
| ~ spl14_73 ),
inference(avatar_split_clause,[],[f2104,f771,f622]) ).
fof(f2523,plain,
( ~ spl14_35
| spl14_12
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f2479,f464,f437,f544]) ).
fof(f2524,plain,
( ~ spl14_35
| ~ spl14_109 ),
inference(avatar_split_clause,[],[f2516,f978,f544]) ).
fof(f2525,plain,
( e1 != op(e2,e2)
| spl14_7
| ~ spl14_16 ),
inference(forward_demodulation,[],[f417,f456]) ).
fof(f2528,plain,
( ~ spl14_28
| spl14_7
| ~ spl14_16 ),
inference(avatar_split_clause,[],[f2525,f455,f415,f510]) ).
fof(f2529,plain,
( ~ spl14_98
| ~ spl14_1
| spl14_3 ),
inference(avatar_split_clause,[],[f2150,f397,f389,f928]) ).
fof(f2531,plain,
( ~ spl14_113
| ~ spl14_4 ),
inference(avatar_split_clause,[],[f1647,f402,f999]) ).
fof(f2534,plain,
( ~ spl14_9
| ~ spl14_49 ),
inference(avatar_split_clause,[],[f1482,f617,f424]) ).
fof(f2538,plain,
( ~ spl14_98
| ~ spl14_97 ),
inference(avatar_split_clause,[],[f2260,f924,f928]) ).
fof(f2539,plain,
( ~ spl14_109
| ~ spl14_110 ),
inference(avatar_split_clause,[],[f1525,f982,f978]) ).
fof(f2540,plain,
( ~ spl14_98
| ~ spl14_118 ),
inference(avatar_split_clause,[],[f1479,f1024,f928]) ).
fof(f2542,plain,
( ~ spl14_28
| ~ spl14_118 ),
inference(avatar_split_clause,[],[f1516,f1024,f510]) ).
fof(f2544,plain,
( ~ spl14_110
| ~ spl14_36 ),
inference(avatar_split_clause,[],[f1589,f550,f982]) ).
fof(f2547,plain,
( ~ spl14_52
| ~ spl14_46 ),
inference(avatar_split_clause,[],[f2502,f602,f632]) ).
fof(f2550,plain,
( ~ spl14_112
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f2513,f464,f994]) ).
fof(f2551,plain,
( ~ spl14_101
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f2447,f464,f942]) ).
fof(f2552,plain,
( ~ spl14_114
| ~ spl14_18
| spl14_24 ),
inference(avatar_split_clause,[],[f2472,f491,f464,f1004]) ).
fof(f2554,plain,
( ~ spl14_40
| ~ spl14_27 ),
inference(avatar_split_clause,[],[f1563,f505,f571]) ).
fof(f2557,plain,
( ~ spl14_107
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f1519,f544,f969]) ).
fof(f2558,plain,
( ~ spl14_16
| ~ spl14_39 ),
inference(avatar_split_clause,[],[f2336,f566,f455]) ).
fof(f2563,plain,
( ~ spl14_16
| ~ spl14_101 ),
inference(avatar_split_clause,[],[f2360,f942,f455]) ).
fof(f2564,plain,
( ~ spl14_46
| ~ spl14_107 ),
inference(avatar_split_clause,[],[f2330,f969,f602]) ).
fof(f2566,plain,
( ~ spl14_102
| ~ spl14_112 ),
inference(avatar_split_clause,[],[f2322,f994,f946]) ).
fof(f2569,plain,
( ~ spl14_27
| spl14_22
| ~ spl14_36 ),
inference(avatar_split_clause,[],[f1598,f550,f482,f505]) ).
fof(f2571,plain,
( ~ spl14_16
| spl14_5
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f1850,f539,f406,f455]) ).
fof(f2574,plain,
( ~ spl14_98
| ~ spl14_57 ),
inference(avatar_split_clause,[],[f1788,f657,f928]) ).
fof(f2575,plain,
( ~ spl14_101
| ~ spl14_102 ),
inference(avatar_split_clause,[],[f2143,f946,f942]) ).
fof(f2626,plain,
( e1 != op(e2,e1)
| ~ spl14_28 ),
inference(forward_demodulation,[],[f110,f511]) ).
fof(f2651,plain,
( e3 != op(e1,e2)
| ~ spl14_78 ),
inference(forward_demodulation,[],[f133,f811]) ).
fof(f2652,plain,
( e1 != op(e1,e2)
| ~ spl14_28 ),
inference(forward_demodulation,[],[f134,f511]) ).
fof(f2654,plain,
( e3 != op(e0,e2)
| ~ spl14_78 ),
inference(forward_demodulation,[],[f135,f811]) ).
fof(f2670,plain,
( e0 != op(e0,e0)
| ~ spl14_52 ),
inference(forward_demodulation,[],[f148,f633]) ).
fof(f2679,plain,
( e0 != op(e1,e2)
| spl14_11
| ~ spl14_28 ),
inference(forward_demodulation,[],[f434,f511]) ).
fof(f2685,plain,
( e3 != op(e1,e2)
| ~ spl14_28
| spl14_32 ),
inference(forward_demodulation,[],[f531,f511]) ).
fof(f2700,plain,
( op(e0,e0) != e3
| spl14_19
| ~ spl14_34 ),
inference(forward_demodulation,[],[f470,f540]) ).
fof(f2703,plain,
( e2 != op(e0,e1)
| spl14_13
| ~ spl14_34 ),
inference(forward_demodulation,[],[f443,f540]) ).
fof(f2707,plain,
( ~ spl14_1
| ~ spl14_104 ),
inference(avatar_split_clause,[],[f1506,f955,f389]) ).
fof(f2708,plain,
( ~ spl14_34
| ~ spl14_107 ),
inference(avatar_split_clause,[],[f2328,f969,f539]) ).
fof(f2713,plain,
( e1 != op(e1,e2)
| ~ spl14_61 ),
inference(forward_demodulation,[],[f118,f683]) ).
fof(f2714,plain,
( ~ spl14_64
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f2652,f510,f705]) ).
fof(f2715,plain,
( ~ spl14_107
| spl14_11
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f2679,f510,f432,f969]) ).
fof(f2717,plain,
( e1 != op(e1,e1)
| ~ spl14_61 ),
inference(forward_demodulation,[],[f119,f683]) ).
fof(f2720,plain,
( ~ spl14_41
| ~ spl14_52 ),
inference(avatar_split_clause,[],[f2670,f632,f576]) ).
fof(f2721,plain,
( ~ spl14_64
| ~ spl14_61 ),
inference(avatar_split_clause,[],[f2713,f681,f705]) ).
fof(f2722,plain,
( ~ spl14_45
| ~ spl14_61 ),
inference(avatar_split_clause,[],[f2717,f681,f597]) ).
fof(f2724,plain,
( e0 != op(e1,e1)
| spl14_14
| ~ spl14_28 ),
inference(forward_demodulation,[],[f448,f511]) ).
fof(f2726,plain,
( ~ spl14_34
| spl14_14
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f2724,f510,f446,f539]) ).
fof(f2761,plain,
( e0 != op(e2,e1)
| spl14_6
| ~ spl14_18 ),
inference(forward_demodulation,[],[f412,f465]) ).
fof(f2773,plain,
( e3 != op(e2,e2)
| ~ spl14_18
| spl14_19 ),
inference(forward_demodulation,[],[f470,f465]) ).
fof(f2776,plain,
( e3 != op(e1,e1)
| ~ spl14_28
| spl14_29 ),
inference(forward_demodulation,[],[f516,f511]) ).
fof(f2777,plain,
( op(e0,e0) != e2
| spl14_31
| ~ spl14_36 ),
inference(forward_demodulation,[],[f526,f551]) ).
fof(f2778,plain,
( $false
| ~ spl14_16
| spl14_31
| ~ spl14_36 ),
inference(forward_subsumption_resolution,[],[f2777,f456]) ).
fof(f2779,plain,
( ~ spl14_16
| spl14_31
| ~ spl14_36 ),
inference(avatar_contradiction_clause,[],[f2778]) ).
fof(f2787,plain,
( ~ spl14_61
| ~ spl14_66 ),
inference(avatar_split_clause,[],[f1497,f719,f681]) ).
fof(f2876,plain,
( e1 != op(e0,e2)
| spl14_15
| ~ spl14_35 ),
inference(forward_demodulation,[],[f452,f545]) ).
fof(f2881,plain,
( e3 != op(e0,e2)
| spl14_32
| ~ spl14_35 ),
inference(forward_demodulation,[],[f531,f545]) ).
fof(f2882,plain,
( e2 != op(e3,e3)
| ~ spl14_1
| spl14_2 ),
inference(forward_demodulation,[],[f395,f390]) ).
fof(f2887,plain,
( op(e0,e0) != e1
| spl14_10
| ~ spl14_35 ),
inference(forward_demodulation,[],[f430,f545]) ).
fof(f2890,plain,
( op(e0,e0) != e3
| spl14_29
| ~ spl14_35 ),
inference(forward_demodulation,[],[f516,f545]) ).
fof(f2894,plain,
( ~ spl14_118
| ~ spl14_9
| spl14_15 ),
inference(avatar_split_clause,[],[f2485,f450,f424,f1024]) ).
fof(f2907,plain,
( ~ spl14_109
| spl14_6
| ~ spl14_18 ),
inference(avatar_split_clause,[],[f2761,f464,f410,f978]) ).
fof(f2911,plain,
( ~ spl14_9
| ~ spl14_18
| spl14_19 ),
inference(avatar_split_clause,[],[f2773,f468,f464,f424]) ).
fof(f2914,plain,
( ~ spl14_113
| ~ spl14_28
| spl14_32 ),
inference(avatar_split_clause,[],[f2685,f529,f510,f999]) ).
fof(f2915,plain,
( ~ spl14_51
| ~ spl14_28 ),
inference(avatar_split_clause,[],[f2626,f510,f627]) ).
fof(f2916,plain,
( ~ spl14_4
| ~ spl14_28
| spl14_29 ),
inference(avatar_split_clause,[],[f2776,f514,f510,f402]) ).
fof(f2918,plain,
( ~ spl14_78
| ~ spl14_55 ),
inference(avatar_split_clause,[],[f1783,f647,f809]) ).
fof(f2919,plain,
( ~ spl14_41
| ~ spl14_59 ),
inference(avatar_split_clause,[],[f1505,f667,f576]) ).
fof(f2922,plain,
( ~ spl14_113
| ~ spl14_78 ),
inference(avatar_split_clause,[],[f2651,f809,f999]) ).
fof(f2923,plain,
( ~ spl14_34
| ~ spl14_110 ),
inference(avatar_split_clause,[],[f1526,f982,f539]) ).
fof(f2926,plain,
( ~ spl14_36
| ~ spl14_4
| spl14_12 ),
inference(avatar_split_clause,[],[f2370,f437,f402,f550]) ).
fof(f2927,plain,
( ~ spl14_46
| ~ spl14_58 ),
inference(avatar_split_clause,[],[f1829,f662,f602]) ).
fof(f2928,plain,
( ~ spl14_110
| ~ spl14_58 ),
inference(avatar_split_clause,[],[f1913,f662,f982]) ).
fof(f2931,plain,
( ~ spl14_38
| ~ spl14_104 ),
inference(avatar_split_clause,[],[f1573,f955,f561]) ).
fof(f3016,plain,
( e2 != op(e1,e2)
| ~ spl14_50 ),
inference(forward_demodulation,[],[f134,f623]) ).
fof(f3030,plain,
( e3 != op(e1,e0)
| ~ spl14_106 ),
inference(forward_demodulation,[],[f146,f966]) ).
fof(f3048,plain,
( e3 != op(e1,e1)
| spl14_17
| ~ spl14_27 ),
inference(forward_demodulation,[],[f461,f506]) ).
fof(f3049,plain,
( $false
| ~ spl14_4
| spl14_17
| ~ spl14_27 ),
inference(forward_subsumption_resolution,[],[f3048,f403]) ).
fof(f3050,plain,
( ~ spl14_4
| spl14_17
| ~ spl14_27 ),
inference(avatar_contradiction_clause,[],[f3049]) ).
fof(f3054,plain,
( $false
| spl14_10
| ~ spl14_27
| ~ spl14_35 ),
inference(forward_subsumption_resolution,[],[f2887,f506]) ).
fof(f3055,plain,
( spl14_10
| ~ spl14_27
| ~ spl14_35 ),
inference(avatar_contradiction_clause,[],[f3054]) ).
fof(f3056,plain,
( $false
| spl14_32
| ~ spl14_35
| ~ spl14_104 ),
inference(forward_subsumption_resolution,[],[f2881,f957]) ).
fof(f3057,plain,
( spl14_32
| ~ spl14_35
| ~ spl14_104 ),
inference(avatar_contradiction_clause,[],[f3056]) ).
fof(f3068,plain,
( ~ spl14_100
| ~ spl14_21 ),
inference(avatar_split_clause,[],[f1512,f478,f937]) ).
fof(f3069,plain,
( ~ spl14_117
| ~ spl14_21
| spl14_26 ),
inference(avatar_split_clause,[],[f1545,f500,f478,f1019]) ).
fof(f3070,plain,
( ~ spl14_112
| ~ spl14_21 ),
inference(avatar_split_clause,[],[f1476,f478,f994]) ).
fof(f3071,plain,
( ~ spl14_104
| ~ spl14_78 ),
inference(avatar_split_clause,[],[f2654,f809,f955]) ).
fof(f3072,plain,
( ~ spl14_105
| ~ spl14_106 ),
inference(avatar_split_clause,[],[f3030,f964,f960]) ).
fof(f3186,plain,
( e1 != op(e2,e2)
| ~ spl14_21
| spl14_22 ),
inference(forward_demodulation,[],[f484,f479]) ).
fof(f3197,plain,
( $false
| ~ spl14_1
| spl14_2
| ~ spl14_21 ),
inference(forward_subsumption_resolution,[],[f2882,f479]) ).
fof(f3198,plain,
( ~ spl14_1
| spl14_2
| ~ spl14_21 ),
inference(avatar_contradiction_clause,[],[f3197]) ).
fof(f3200,plain,
( ~ spl14_28
| ~ spl14_21
| spl14_22 ),
inference(avatar_split_clause,[],[f3186,f482,f478,f510]) ).
fof(f3201,plain,
( e0 != op(e2,e2)
| ~ spl14_21
| spl14_25 ),
inference(forward_demodulation,[],[f498,f479]) ).
fof(f3214,plain,
( ~ spl14_1
| spl14_19
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f2700,f539,f468,f389]) ).
fof(f3215,plain,
( ~ spl14_99
| spl14_13
| ~ spl14_34 ),
inference(avatar_split_clause,[],[f2703,f539,f441,f933]) ).
fof(f3216,plain,
( ~ spl14_1
| spl14_29
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f2890,f544,f514,f389]) ).
fof(f3217,plain,
( ~ spl14_95
| spl14_15
| ~ spl14_35 ),
inference(avatar_split_clause,[],[f2876,f544,f450,f915]) ).
fof(f3219,plain,
( ~ spl14_35
| ~ spl14_21
| spl14_25 ),
inference(avatar_split_clause,[],[f3201,f496,f478,f544]) ).
fof(f3223,plain,
( ~ spl14_115
| ~ spl14_21
| spl14_23 ),
inference(avatar_split_clause,[],[f1543,f486,f478,f1009]) ).
fof(f3227,plain,
( ~ spl14_44
| ~ spl14_50 ),
inference(avatar_split_clause,[],[f3016,f622,f592]) ).
fof(f3230,plain,
( ~ spl14_102
| ~ spl14_21 ),
inference(avatar_split_clause,[],[f1478,f478,f946]) ).
cnf(s1,plain,
( ~ spl14_1
| ~ spl14_2
| ~ spl14_3 ),
inference(sat_conversion,[],[f400]) ).
cnf(s2,plain,
( ~ spl14_4
| ~ spl14_5
| ~ spl14_6 ),
inference(sat_conversion,[],[f413]) ).
cnf(s3,plain,
( ~ spl14_1
| ~ spl14_7
| ~ spl14_8 ),
inference(sat_conversion,[],[f422]) ).
cnf(s4,plain,
( ~ spl14_9
| ~ spl14_10
| ~ spl14_11 ),
inference(sat_conversion,[],[f435]) ).
cnf(s5,plain,
( ~ spl14_4
| ~ spl14_12
| ~ spl14_13 ),
inference(sat_conversion,[],[f444]) ).
cnf(s6,plain,
( ~ spl14_9
| ~ spl14_14
| ~ spl14_15 ),
inference(sat_conversion,[],[f453]) ).
cnf(s7,plain,
( ~ spl14_3
| ~ spl14_16
| ~ spl14_17 ),
inference(sat_conversion,[],[f462]) ).
cnf(s8,plain,
( ~ spl14_6
| ~ spl14_18
| ~ spl14_19 ),
inference(sat_conversion,[],[f471]) ).
cnf(s9,plain,
( ~ spl14_7
| ~ spl14_16
| ~ spl14_20 ),
inference(sat_conversion,[],[f476]) ).
cnf(s10,plain,
( ~ spl14_21
| ~ spl14_22
| ~ spl14_23 ),
inference(sat_conversion,[],[f489]) ).
cnf(s11,plain,
( ~ spl14_12
| ~ spl14_18
| ~ spl14_24 ),
inference(sat_conversion,[],[f494]) ).
cnf(s12,plain,
( ~ spl14_21
| ~ spl14_25
| ~ spl14_26 ),
inference(sat_conversion,[],[f503]) ).
cnf(s13,plain,
( ~ spl14_8
| ~ spl14_17
| ~ spl14_27 ),
inference(sat_conversion,[],[f508]) ).
cnf(s14,plain,
( ~ spl14_11
| ~ spl14_28
| ~ spl14_29 ),
inference(sat_conversion,[],[f517]) ).
cnf(s15,plain,
( ~ spl14_2
| ~ spl14_20
| ~ spl14_27 ),
inference(sat_conversion,[],[f518]) ).
cnf(s16,plain,
( ~ spl14_23
| ~ spl14_30
| ~ spl14_31 ),
inference(sat_conversion,[],[f527]) ).
cnf(s17,plain,
( ~ spl14_14
| ~ spl14_28
| ~ spl14_32 ),
inference(sat_conversion,[],[f532]) ).
cnf(s18,plain,
( ~ spl14_25
| ~ spl14_30
| ~ spl14_33 ),
inference(sat_conversion,[],[f537]) ).
cnf(s19,plain,
( ~ spl14_13
| ~ spl14_19
| ~ spl14_34 ),
inference(sat_conversion,[],[f542]) ).
cnf(s20,plain,
( ~ spl14_15
| ~ spl14_29
| ~ spl14_35 ),
inference(sat_conversion,[],[f547]) ).
cnf(s21,plain,
( ~ spl14_5
| ~ spl14_24
| ~ spl14_34 ),
inference(sat_conversion,[],[f548]) ).
cnf(s22,plain,
( ~ spl14_26
| ~ spl14_31
| ~ spl14_36 ),
inference(sat_conversion,[],[f553]) ).
cnf(s23,plain,
( ~ spl14_10
| ~ spl14_32
| ~ spl14_35 ),
inference(sat_conversion,[],[f554]) ).
cnf(s24,plain,
( ~ spl14_22
| ~ spl14_33
| ~ spl14_36 ),
inference(sat_conversion,[],[f555]) ).
cnf(s28,plain,
( spl14_37
| ~ spl14_41 ),
inference(sat_conversion,[],[f579]) ).
cnf(s30,plain,
( spl14_37
| spl14_41 ),
inference(sat_conversion,[],[f581]) ).
cnf(s33,plain,
( ~ spl14_42
| ~ spl14_45 ),
inference(sat_conversion,[],[f600]) ).
cnf(s34,plain,
( ~ spl14_42
| ~ spl14_46 ),
inference(sat_conversion,[],[f605]) ).
cnf(s35,plain,
( ~ spl14_42
| spl14_47 ),
inference(sat_conversion,[],[f610]) ).
cnf(s36,plain,
( spl14_27
| ~ spl14_42 ),
inference(sat_conversion,[],[f611]) ).
cnf(s38,plain,
( ~ spl14_48
| ~ spl14_50 ),
inference(sat_conversion,[],[f625]) ).
cnf(s40,plain,
( ~ spl14_48
| ~ spl14_52 ),
inference(sat_conversion,[],[f635]) ).
cnf(s41,plain,
( ~ spl14_48
| spl14_53 ),
inference(sat_conversion,[],[f640]) ).
cnf(s42,plain,
( spl14_16
| ~ spl14_48 ),
inference(sat_conversion,[],[f641]) ).
cnf(s43,plain,
( ~ spl14_54
| ~ spl14_55 ),
inference(sat_conversion,[],[f650]) ).
cnf(s46,plain,
( ~ spl14_54
| ~ spl14_58 ),
inference(sat_conversion,[],[f665]) ).
cnf(s47,plain,
( ~ spl14_54
| spl14_59 ),
inference(sat_conversion,[],[f670]) ).
cnf(s48,plain,
( spl14_1
| ~ spl14_54 ),
inference(sat_conversion,[],[f671]) ).
cnf(s51,plain,
( ~ spl14_40
| spl14_60 ),
inference(sat_conversion,[],[f678]) ).
cnf(s52,plain,
( ~ spl14_41
| spl14_60 ),
inference(sat_conversion,[],[f679]) ).
cnf(s53,plain,
( spl14_60
| spl14_61 ),
inference(sat_conversion,[],[f684]) ).
cnf(s54,plain,
( spl14_34
| spl14_60 ),
inference(sat_conversion,[],[f685]) ).
cnf(s57,plain,
( ~ spl14_45
| spl14_62 ),
inference(sat_conversion,[],[f692]) ).
cnf(s60,plain,
( spl14_45
| spl14_62 ),
inference(sat_conversion,[],[f695]) ).
cnf(s61,plain,
( ~ spl14_49
| ~ spl14_63 ),
inference(sat_conversion,[],[f700]) ).
cnf(s62,plain,
( ~ spl14_50
| ~ spl14_63 ),
inference(sat_conversion,[],[f701]) ).
cnf(s63,plain,
( ~ spl14_51
| ~ spl14_63 ),
inference(sat_conversion,[],[f702]) ).
cnf(s64,plain,
( ~ spl14_52
| ~ spl14_63 ),
inference(sat_conversion,[],[f703]) ).
cnf(s65,plain,
( ~ spl14_63
| spl14_64 ),
inference(sat_conversion,[],[f708]) ).
cnf(s66,plain,
( spl14_18
| ~ spl14_63 ),
inference(sat_conversion,[],[f709]) ).
cnf(s67,plain,
( ~ spl14_55
| spl14_65 ),
inference(sat_conversion,[],[f714]) ).
cnf(s68,plain,
( ~ spl14_56
| spl14_65 ),
inference(sat_conversion,[],[f715]) ).
cnf(s69,plain,
( ~ spl14_57
| spl14_65 ),
inference(sat_conversion,[],[f716]) ).
cnf(s70,plain,
( ~ spl14_58
| spl14_65 ),
inference(sat_conversion,[],[f717]) ).
cnf(s71,plain,
( spl14_65
| spl14_66 ),
inference(sat_conversion,[],[f722]) ).
cnf(s72,plain,
( spl14_4
| spl14_65 ),
inference(sat_conversion,[],[f723]) ).
cnf(s74,plain,
( ~ spl14_39
| spl14_67 ),
inference(sat_conversion,[],[f729]) ).
cnf(s76,plain,
( ~ spl14_41
| spl14_67 ),
inference(sat_conversion,[],[f731]) ).
cnf(s77,plain,
( spl14_67
| spl14_68 ),
inference(sat_conversion,[],[f736]) ).
cnf(s78,plain,
( spl14_35
| spl14_67 ),
inference(sat_conversion,[],[f737]) ).
cnf(s80,plain,
( ~ spl14_44
| ~ spl14_69 ),
inference(sat_conversion,[],[f743]) ).
cnf(s81,plain,
( ~ spl14_45
| ~ spl14_69 ),
inference(sat_conversion,[],[f744]) ).
cnf(s83,plain,
( ~ spl14_69
| spl14_70 ),
inference(sat_conversion,[],[f750]) ).
cnf(s84,plain,
( spl14_28
| ~ spl14_69 ),
inference(sat_conversion,[],[f751]) ).
cnf(s86,plain,
( ~ spl14_50
| spl14_71 ),
inference(sat_conversion,[],[f757]) ).
cnf(s90,plain,
( spl14_50
| spl14_71 ),
inference(sat_conversion,[],[f761]) ).
cnf(s91,plain,
( ~ spl14_55
| spl14_72 ),
inference(sat_conversion,[],[f766]) ).
cnf(s92,plain,
( ~ spl14_56
| spl14_72 ),
inference(sat_conversion,[],[f767]) ).
cnf(s93,plain,
( ~ spl14_57
| spl14_72 ),
inference(sat_conversion,[],[f768]) ).
cnf(s94,plain,
( ~ spl14_58
| spl14_72 ),
inference(sat_conversion,[],[f769]) ).
cnf(s95,plain,
( spl14_72
| spl14_73 ),
inference(sat_conversion,[],[f774]) ).
cnf(s96,plain,
( spl14_9
| spl14_72 ),
inference(sat_conversion,[],[f775]) ).
cnf(s97,plain,
( ~ spl14_38
| spl14_74 ),
inference(sat_conversion,[],[f780]) ).
cnf(s100,plain,
( ~ spl14_41
| spl14_74 ),
inference(sat_conversion,[],[f783]) ).
cnf(s101,plain,
( spl14_74
| spl14_75 ),
inference(sat_conversion,[],[f788]) ).
cnf(s102,plain,
( spl14_36
| spl14_74 ),
inference(sat_conversion,[],[f789]) ).
cnf(s103,plain,
( ~ spl14_43
| ~ spl14_76 ),
inference(sat_conversion,[],[f794]) ).
cnf(s105,plain,
( ~ spl14_45
| ~ spl14_76 ),
inference(sat_conversion,[],[f796]) ).
cnf(s107,plain,
( ~ spl14_76
| spl14_77 ),
inference(sat_conversion,[],[f802]) ).
cnf(s108,plain,
( spl14_30
| ~ spl14_76 ),
inference(sat_conversion,[],[f803]) ).
cnf(s115,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| ~ spl14_49
| spl14_54
| spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f814]) ).
cnf(s116,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| ~ spl14_50
| spl14_54
| spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f815]) ).
cnf(s117,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| ~ spl14_51
| spl14_54
| spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f816]) ).
cnf(s118,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| ~ spl14_52
| spl14_54
| spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f817]) ).
cnf(s119,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_78 ),
inference(sat_conversion,[],[f818]) ).
cnf(s120,plain,
( spl14_21
| ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f819]) ).
cnf(s137,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_56
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_78 ),
inference(sat_conversion,[],[f836]) ).
cnf(s140,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| ~ spl14_50
| spl14_54
| ~ spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f839]) ).
cnf(s141,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| ~ spl14_51
| spl14_54
| ~ spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f840]) ).
cnf(s143,plain,
( ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76
| spl14_78 ),
inference(sat_conversion,[],[f842]) ).
cnf(s144,plain,
( spl14_21
| ~ spl14_37
| spl14_42
| spl14_48
| spl14_54
| ~ spl14_55
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_71
| ~ spl14_72
| ~ spl14_74
| spl14_76 ),
inference(sat_conversion,[],[f843]) ).
cnf(s151,plain,
( spl14_27
| spl14_40
| spl14_95
| spl14_96 ),
inference(sat_conversion,[],[f922]) ).
cnf(s152,plain,
( spl14_27
| spl14_61
| spl14_97
| spl14_98 ),
inference(sat_conversion,[],[f931]) ).
cnf(s154,plain,
( spl14_16
| spl14_68
| spl14_101
| spl14_102 ),
inference(sat_conversion,[],[f949]) ).
cnf(s155,plain,
( spl14_1
| spl14_38
| spl14_103
| spl14_104 ),
inference(sat_conversion,[],[f958]) ).
cnf(s156,plain,
( spl14_1
| spl14_75
| spl14_105
| spl14_106 ),
inference(sat_conversion,[],[f967]) ).
cnf(s157,plain,
( spl14_34
| spl14_46
| spl14_107
| spl14_108 ),
inference(sat_conversion,[],[f976]) ).
cnf(s158,plain,
( spl14_34
| spl14_47
| spl14_109
| spl14_110 ),
inference(sat_conversion,[],[f985]) ).
cnf(s160,plain,
( spl14_40
| spl14_45
| spl14_51
| spl14_57 ),
inference(sat_conversion,[],[f987]) ).
cnf(s161,plain,
( spl14_18
| spl14_44
| spl14_101
| spl14_111 ),
inference(sat_conversion,[],[f992]) ).
cnf(s162,plain,
( spl14_18
| spl14_70
| spl14_99
| spl14_112 ),
inference(sat_conversion,[],[f997]) ).
cnf(s163,plain,
( spl14_4
| spl14_43
| spl14_105
| spl14_113 ),
inference(sat_conversion,[],[f1002]) ).
cnf(s164,plain,
( spl14_4
| spl14_77
| spl14_103
| spl14_114 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s165,plain,
( spl14_35
| spl14_52
| spl14_109
| spl14_115 ),
inference(sat_conversion,[],[f1012]) ).
cnf(s167,plain,
( spl14_28
| spl14_51
| spl14_97
| spl14_117 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s168,plain,
( spl14_28
| spl14_64
| spl14_95
| spl14_118 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s170,plain,
( spl14_39
| spl14_44
| spl14_50
| spl14_56 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s171,plain,
( spl14_9
| spl14_49
| spl14_106
| spl14_114 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s172,plain,
( spl14_9
| spl14_78
| spl14_104
| spl14_113 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s173,plain,
( spl14_36
| spl14_58
| spl14_110
| spl14_116 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s174,plain,
( spl14_36
| spl14_59
| spl14_108
| spl14_115 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s175,plain,
( spl14_30
| spl14_57
| spl14_98
| spl14_118 ),
inference(sat_conversion,[],[f1034]) ).
cnf(s176,plain,
( spl14_30
| spl14_66
| spl14_96
| spl14_117 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s177,plain,
( spl14_21
| spl14_56
| spl14_102
| spl14_112 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s178,plain,
( spl14_21
| spl14_73
| spl14_100
| spl14_111 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s179,plain,
( spl14_55
| spl14_75
| spl14_77
| spl14_78 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s180,plain,
( spl14_38
| spl14_43
| spl14_49
| spl14_55 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s181,plain,
( spl14_1
| spl14_16
| spl14_27
| spl14_41 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s182,plain,
( spl14_40
| spl14_47
| spl14_99
| spl14_103 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s183,plain,
( spl14_39
| spl14_53
| spl14_95
| spl14_104 ),
inference(sat_conversion,[],[f1042]) ).
cnf(s184,plain,
( spl14_38
| spl14_59
| spl14_96
| spl14_100 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s185,plain,
( spl14_46
| spl14_61
| spl14_101
| spl14_105 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s186,plain,
( spl14_4
| spl14_18
| spl14_34
| spl14_45 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s187,plain,
( spl14_44
| spl14_64
| spl14_107
| spl14_113 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s188,plain,
( spl14_43
| spl14_66
| spl14_108
| spl14_111 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s189,plain,
( spl14_52
| spl14_68
| spl14_97
| spl14_106 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s190,plain,
( spl14_51
| spl14_70
| spl14_109
| spl14_114 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s191,plain,
( spl14_9
| spl14_28
| spl14_35
| spl14_50 ),
inference(sat_conversion,[],[f1050]) ).
cnf(s192,plain,
( spl14_49
| spl14_73
| spl14_115
| spl14_117 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s193,plain,
( spl14_58
| spl14_75
| spl14_98
| spl14_102 ),
inference(sat_conversion,[],[f1052]) ).
cnf(s194,plain,
( spl14_57
| spl14_77
| spl14_110
| spl14_112 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s195,plain,
( spl14_56
| spl14_78
| spl14_116
| spl14_118 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s196,plain,
( spl14_21
| spl14_30
| spl14_36
| spl14_55 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s197,plain,
( ~ spl14_4
| ~ spl14_18 ),
inference(sat_conversion,[],[f1059]) ).
cnf(s198,plain,
( ~ spl14_16
| ~ spl14_27 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s199,plain,
( ~ spl14_4
| ~ spl14_34 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s200,plain,
( ~ spl14_9
| ~ spl14_35 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s205,plain,
( ~ spl14_21
| ~ spl14_55 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s206,plain,
( ~ spl14_38
| ~ spl14_59 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s210,plain,
( ~ spl14_58
| ~ spl14_75 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s213,plain,
( ~ spl14_38
| ~ spl14_100 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s223,plain,
( ~ spl14_75
| ~ spl14_102 ),
inference(sat_conversion,[],[f1164]) ).
cnf(s226,plain,
( ~ spl14_1
| ~ spl14_27 ),
inference(sat_conversion,[],[f1178]) ).
cnf(s229,plain,
( spl14_8
| ~ spl14_27
| ~ spl14_101 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s231,plain,
( ~ spl14_49
| ~ spl14_115 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s233,plain,
( ~ spl14_68
| ~ spl14_106 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s235,plain,
( ~ spl14_27
| ~ spl14_41 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s241,plain,
( ~ spl14_66
| ~ spl14_108 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s246,plain,
( ~ spl14_98
| ~ spl14_102 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s248,plain,
( ~ spl14_51
| ~ spl14_109 ),
inference(sat_conversion,[],[f1284]) ).
cnf(s250,plain,
( ~ spl14_51
| ~ spl14_70 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s253,plain,
( ~ spl14_28
| ~ spl14_35 ),
inference(sat_conversion,[],[f1305]) ).
cnf(s254,plain,
( ~ spl14_4
| ~ spl14_45 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s255,plain,
( ~ spl14_49
| ~ spl14_73 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s267,plain,
( ~ spl14_75
| ~ spl14_98 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s268,plain,
( ~ spl14_75
| ~ spl14_98 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s269,plain,
( ~ spl14_77
| ~ spl14_110 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s271,plain,
( ~ spl14_66
| ~ spl14_111 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s272,plain,
( ~ spl14_21
| ~ spl14_36 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s273,plain,
( ~ spl14_21
| ~ spl14_36 ),
inference(sat_conversion,[],[f1421]) ).
cnf(s279,plain,
( ~ spl14_110
| ~ spl14_112 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s282,plain,
( ~ spl14_116
| ~ spl14_118 ),
inference(sat_conversion,[],[f1463]) ).
cnf(s283,plain,
( ~ spl14_21
| ~ spl14_30 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s287,plain,
( ~ spl14_4
| spl14_6
| ~ spl14_110 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s288,plain,
( ~ spl14_4
| spl14_5
| ~ spl14_21 ),
inference(sat_conversion,[],[f1559]) ).
cnf(s289,plain,
( ~ spl14_47
| ~ spl14_59 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s292,plain,
( ~ spl14_30
| ~ spl14_66 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s293,plain,
( ~ spl14_36
| ~ spl14_59 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s294,plain,
( ~ spl14_66
| ~ spl14_96 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s295,plain,
( ~ spl14_27
| ~ spl14_96 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s298,plain,
( ~ spl14_35
| ~ spl14_53 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s299,plain,
( ~ spl14_4
| ~ spl14_103 ),
inference(sat_conversion,[],[f1611]) ).
cnf(s300,plain,
( ~ spl14_55
| ~ spl14_75 ),
inference(sat_conversion,[],[f1613]) ).
cnf(s302,plain,
( ~ spl14_75
| ~ spl14_78 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s303,plain,
( ~ spl14_35
| ~ spl14_116 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s305,plain,
( ~ spl14_27
| ~ spl14_95 ),
inference(sat_conversion,[],[f1626]) ).
cnf(s306,plain,
( ~ spl14_35
| ~ spl14_115 ),
inference(sat_conversion,[],[f1627]) ).
cnf(s308,plain,
( ~ spl14_68
| ~ spl14_73 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s309,plain,
( ~ spl14_66
| ~ spl14_117 ),
inference(sat_conversion,[],[f1630]) ).
cnf(s312,plain,
( ~ spl14_4
| ~ spl14_105 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s313,plain,
( spl14_20
| ~ spl14_27
| ~ spl14_105 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s319,plain,
( ~ spl14_27
| ~ spl14_98 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s321,plain,
( ~ spl14_4
| ~ spl14_114 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s322,plain,
( ~ spl14_27
| ~ spl14_61 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s325,plain,
( spl14_2
| ~ spl14_18
| ~ spl14_27 ),
inference(sat_conversion,[],[f1655]) ).
cnf(s329,plain,
( ~ spl14_34
| ~ spl14_47 ),
inference(sat_conversion,[],[f1658]) ).
cnf(s330,plain,
( ~ spl14_16
| ~ spl14_68 ),
inference(sat_conversion,[],[f1662]) ).
cnf(s332,plain,
( ~ spl14_16
| ~ spl14_100 ),
inference(sat_conversion,[],[f1665]) ).
cnf(s334,plain,
( ~ spl14_56
| ~ spl14_78 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s336,plain,
( ~ spl14_68
| ~ spl14_97 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s337,plain,
( ~ spl14_1
| ~ spl14_16 ),
inference(sat_conversion,[],[f1714]) ).
cnf(s340,plain,
( ~ spl14_1
| ~ spl14_103 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s344,plain,
( ~ spl14_64
| ~ spl14_113 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s346,plain,
( ~ spl14_70
| ~ spl14_114 ),
inference(sat_conversion,[],[f1773]) ).
cnf(s353,plain,
( spl14_24
| ~ spl14_34
| ~ spl14_103 ),
inference(sat_conversion,[],[f1858]) ).
cnf(s354,plain,
( ~ spl14_55
| ~ spl14_77 ),
inference(sat_conversion,[],[f1859]) ).
cnf(s355,plain,
( ~ spl14_40
| ~ spl14_57 ),
inference(sat_conversion,[],[f1860]) ).
cnf(s360,plain,
( ~ spl14_45
| ~ spl14_64 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s361,plain,
( ~ spl14_45
| ~ spl14_57 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s362,plain,
( ~ spl14_97
| ~ spl14_117 ),
inference(sat_conversion,[],[f1875]) ).
cnf(s368,plain,
( ~ spl14_34
| ~ spl14_108 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s369,plain,
( ~ spl14_34
| ~ spl14_109 ),
inference(sat_conversion,[],[f1920]) ).
cnf(s371,plain,
( ~ spl14_18
| ~ spl14_70 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s372,plain,
( ~ spl14_18
| ~ spl14_111 ),
inference(sat_conversion,[],[f1925]) ).
cnf(s376,plain,
( ~ spl14_70
| ~ spl14_73 ),
inference(sat_conversion,[],[f1930]) ).
cnf(s377,plain,
( ~ spl14_73
| ~ spl14_115 ),
inference(sat_conversion,[],[f1932]) ).
cnf(s389,plain,
( spl14_23
| ~ spl14_30
| ~ spl14_108 ),
inference(sat_conversion,[],[f1998]) ).
cnf(s390,plain,
( ~ spl14_16
| ~ spl14_99 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s392,plain,
( spl14_25
| ~ spl14_30
| ~ spl14_34 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s393,plain,
( ~ spl14_53
| ~ spl14_95 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s394,plain,
( ~ spl14_30
| spl14_33
| ~ spl14_111 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s399,plain,
( ~ spl14_9
| ~ spl14_28 ),
inference(sat_conversion,[],[f2022]) ).
cnf(s401,plain,
( ~ spl14_77
| ~ spl14_112 ),
inference(sat_conversion,[],[f2024]) ).
cnf(s405,plain,
( ~ spl14_28
| ~ spl14_97 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s407,plain,
( ~ spl14_1
| ~ spl14_38 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s408,plain,
( ~ spl14_1
| ~ spl14_106 ),
inference(sat_conversion,[],[f2031]) ).
cnf(s412,plain,
( ~ spl14_39
| ~ spl14_44 ),
inference(sat_conversion,[],[f2036]) ).
cnf(s413,plain,
( ~ spl14_30
| ~ spl14_96 ),
inference(sat_conversion,[],[f2037]) ).
cnf(s414,plain,
( ~ spl14_30
| ~ spl14_98 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s415,plain,
( ~ spl14_9
| ~ spl14_78 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s417,plain,
( ~ spl14_9
| ~ spl14_114 ),
inference(sat_conversion,[],[f2041]) ).
cnf(s418,plain,
( ~ spl14_9
| ~ spl14_106 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s420,plain,
( ~ spl14_77
| ~ spl14_78 ),
inference(sat_conversion,[],[f2044]) ).
cnf(s427,plain,
( ~ spl14_27
| ~ spl14_97 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s436,plain,
( ~ spl14_1
| spl14_7
| ~ spl14_30 ),
inference(sat_conversion,[],[f2163]) ).
cnf(s438,plain,
( ~ spl14_18
| ~ spl14_99 ),
inference(sat_conversion,[],[f2164]) ).
cnf(s442,plain,
( ~ spl14_1
| ~ spl14_105 ),
inference(sat_conversion,[],[f2171]) ).
cnf(s446,plain,
( ~ spl14_52
| ~ spl14_109 ),
inference(sat_conversion,[],[f2177]) ).
cnf(s450,plain,
( ~ spl14_18
| ~ spl14_30
| spl14_31 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s451,plain,
( ~ spl14_18
| ~ spl14_44 ),
inference(sat_conversion,[],[f2181]) ).
cnf(s455,plain,
( ~ spl14_16
| ~ spl14_102 ),
inference(sat_conversion,[],[f2183]) ).
cnf(s458,plain,
( ~ spl14_43
| ~ spl14_108 ),
inference(sat_conversion,[],[f2188]) ).
cnf(s474,plain,
( ~ spl14_1
| spl14_8
| ~ spl14_102 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s476,plain,
( ~ spl14_4
| ~ spl14_43 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s477,plain,
( ~ spl14_4
| ~ spl14_77 ),
inference(sat_conversion,[],[f2237]) ).
cnf(s481,plain,
( spl14_26
| ~ spl14_36
| ~ spl14_96 ),
inference(sat_conversion,[],[f2239]) ).
cnf(s485,plain,
( ~ spl14_41
| ~ spl14_46 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s488,plain,
( ~ spl14_41
| ~ spl14_47 ),
inference(sat_conversion,[],[f2241]) ).
cnf(s489,plain,
( ~ spl14_45
| ~ spl14_51 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s494,plain,
( ~ spl14_45
| ~ spl14_66 ),
inference(sat_conversion,[],[f2246]) ).
cnf(s497,plain,
( ~ spl14_1
| ~ spl14_75 ),
inference(sat_conversion,[],[f2248]) ).
cnf(s510,plain,
( ~ spl14_9
| spl14_11
| ~ spl14_116 ),
inference(sat_conversion,[],[f2258]) ).
cnf(s511,plain,
( ~ spl14_51
| ~ spl14_97 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s513,plain,
( ~ spl14_9
| ~ spl14_50 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s514,plain,
( ~ spl14_95
| ~ spl14_118 ),
inference(sat_conversion,[],[f2268]) ).
cnf(s517,plain,
( ~ spl14_9
| spl14_10
| ~ spl14_30 ),
inference(sat_conversion,[],[f2270]) ).
cnf(s518,plain,
( spl14_33
| ~ spl14_36
| ~ spl14_100 ),
inference(sat_conversion,[],[f2271]) ).
cnf(s529,plain,
( ~ spl14_4
| spl14_13
| ~ spl14_112 ),
inference(sat_conversion,[],[f2376]) ).
cnf(s535,plain,
( ~ spl14_41
| ~ spl14_58 ),
inference(sat_conversion,[],[f2386]) ).
cnf(s546,plain,
( ~ spl14_40
| ~ spl14_45 ),
inference(sat_conversion,[],[f2395]) ).
cnf(s556,plain,
( ~ spl14_64
| ~ spl14_66 ),
inference(sat_conversion,[],[f2399]) ).
cnf(s575,plain,
( ~ spl14_9
| spl14_14
| ~ spl14_36 ),
inference(sat_conversion,[],[f2483]) ).
cnf(s576,plain,
( ~ spl14_9
| ~ spl14_16
| spl14_17 ),
inference(sat_conversion,[],[f2489]) ).
cnf(s577,plain,
( spl14_3
| ~ spl14_16
| ~ spl14_97 ),
inference(sat_conversion,[],[f2491]) ).
cnf(s592,plain,
( ~ spl14_16
| spl14_20
| ~ spl14_106 ),
inference(sat_conversion,[],[f2500]) ).
cnf(s595,plain,
( ~ spl14_50
| ~ spl14_73 ),
inference(sat_conversion,[],[f2520]) ).
cnf(s599,plain,
( spl14_12
| ~ spl14_18
| ~ spl14_35 ),
inference(sat_conversion,[],[f2523]) ).
cnf(s603,plain,
( ~ spl14_35
| ~ spl14_109 ),
inference(sat_conversion,[],[f2524]) ).
cnf(s608,plain,
( spl14_7
| ~ spl14_16
| ~ spl14_28 ),
inference(sat_conversion,[],[f2528]) ).
cnf(s613,plain,
( ~ spl14_1
| spl14_3
| ~ spl14_98 ),
inference(sat_conversion,[],[f2529]) ).
cnf(s617,plain,
( ~ spl14_4
| ~ spl14_113 ),
inference(sat_conversion,[],[f2531]) ).
cnf(s625,plain,
( ~ spl14_9
| ~ spl14_49 ),
inference(sat_conversion,[],[f2534]) ).
cnf(s634,plain,
( ~ spl14_97
| ~ spl14_98 ),
inference(sat_conversion,[],[f2538]) ).
cnf(s638,plain,
( ~ spl14_109
| ~ spl14_110 ),
inference(sat_conversion,[],[f2539]) ).
cnf(s641,plain,
( ~ spl14_98
| ~ spl14_118 ),
inference(sat_conversion,[],[f2540]) ).
cnf(s642,plain,
( ~ spl14_28
| ~ spl14_118 ),
inference(sat_conversion,[],[f2542]) ).
cnf(s646,plain,
( ~ spl14_36
| ~ spl14_110 ),
inference(sat_conversion,[],[f2544]) ).
cnf(s650,plain,
( ~ spl14_46
| ~ spl14_52 ),
inference(sat_conversion,[],[f2547]) ).
cnf(s658,plain,
( ~ spl14_18
| ~ spl14_112 ),
inference(sat_conversion,[],[f2550]) ).
cnf(s659,plain,
( ~ spl14_18
| ~ spl14_101 ),
inference(sat_conversion,[],[f2551]) ).
cnf(s660,plain,
( ~ spl14_18
| spl14_24
| ~ spl14_114 ),
inference(sat_conversion,[],[f2552]) ).
cnf(s667,plain,
( ~ spl14_27
| ~ spl14_40 ),
inference(sat_conversion,[],[f2554]) ).
cnf(s674,plain,
( ~ spl14_35
| ~ spl14_107 ),
inference(sat_conversion,[],[f2557]) ).
cnf(s682,plain,
( ~ spl14_16
| ~ spl14_39 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s706,plain,
( ~ spl14_16
| ~ spl14_101 ),
inference(sat_conversion,[],[f2563]) ).
cnf(s707,plain,
( ~ spl14_46
| ~ spl14_107 ),
inference(sat_conversion,[],[f2564]) ).
cnf(s712,plain,
( ~ spl14_102
| ~ spl14_112 ),
inference(sat_conversion,[],[f2566]) ).
cnf(s722,plain,
( spl14_22
| ~ spl14_27
| ~ spl14_36 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s725,plain,
( spl14_5
| ~ spl14_16
| ~ spl14_34 ),
inference(sat_conversion,[],[f2571]) ).
cnf(s752,plain,
( ~ spl14_57
| ~ spl14_98 ),
inference(sat_conversion,[],[f2574]) ).
cnf(s769,plain,
( ~ spl14_101
| ~ spl14_102 ),
inference(sat_conversion,[],[f2575]) ).
cnf(s795,plain,
( ~ spl14_1
| ~ spl14_104 ),
inference(sat_conversion,[],[f2707]) ).
cnf(s797,plain,
( ~ spl14_34
| ~ spl14_107 ),
inference(sat_conversion,[],[f2708]) ).
cnf(s800,plain,
( ~ spl14_28
| ~ spl14_64 ),
inference(sat_conversion,[],[f2714]) ).
cnf(s801,plain,
( spl14_11
| ~ spl14_28
| ~ spl14_107 ),
inference(sat_conversion,[],[f2715]) ).
cnf(s807,plain,
( ~ spl14_41
| ~ spl14_52 ),
inference(sat_conversion,[],[f2720]) ).
cnf(s811,plain,
( ~ spl14_61
| ~ spl14_64 ),
inference(sat_conversion,[],[f2721]) ).
cnf(s812,plain,
( ~ spl14_45
| ~ spl14_61 ),
inference(sat_conversion,[],[f2722]) ).
cnf(s814,plain,
( spl14_14
| ~ spl14_28
| ~ spl14_34 ),
inference(sat_conversion,[],[f2726]) ).
cnf(s816,plain,
( ~ spl14_16
| spl14_31
| ~ spl14_36 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s842,plain,
( ~ spl14_61
| ~ spl14_66 ),
inference(sat_conversion,[],[f2787]) ).
cnf(s871,plain,
( ~ spl14_9
| spl14_15
| ~ spl14_118 ),
inference(sat_conversion,[],[f2894]) ).
cnf(s921,plain,
( spl14_6
| ~ spl14_18
| ~ spl14_109 ),
inference(sat_conversion,[],[f2907]) ).
cnf(s923,plain,
( ~ spl14_9
| ~ spl14_18
| spl14_19 ),
inference(sat_conversion,[],[f2911]) ).
cnf(s940,plain,
( ~ spl14_28
| spl14_32
| ~ spl14_113 ),
inference(sat_conversion,[],[f2914]) ).
cnf(s942,plain,
( ~ spl14_28
| ~ spl14_51 ),
inference(sat_conversion,[],[f2915]) ).
cnf(s944,plain,
( ~ spl14_4
| ~ spl14_28
| spl14_29 ),
inference(sat_conversion,[],[f2916]) ).
cnf(s955,plain,
( ~ spl14_55
| ~ spl14_78 ),
inference(sat_conversion,[],[f2918]) ).
cnf(s971,plain,
( ~ spl14_41
| ~ spl14_59 ),
inference(sat_conversion,[],[f2919]) ).
cnf(s984,plain,
( ~ spl14_78
| ~ spl14_113 ),
inference(sat_conversion,[],[f2922]) ).
cnf(s1003,plain,
( ~ spl14_34
| ~ spl14_110 ),
inference(sat_conversion,[],[f2923]) ).
cnf(s1011,plain,
( ~ spl14_4
| spl14_12
| ~ spl14_36 ),
inference(sat_conversion,[],[f2926]) ).
cnf(s1036,plain,
( ~ spl14_46
| ~ spl14_58 ),
inference(sat_conversion,[],[f2927]) ).
cnf(s1038,plain,
( ~ spl14_58
| ~ spl14_110 ),
inference(sat_conversion,[],[f2928]) ).
cnf(s1060,plain,
( ~ spl14_38
| ~ spl14_104 ),
inference(sat_conversion,[],[f2931]) ).
cnf(s1081,plain,
( ~ spl14_4
| spl14_17
| ~ spl14_27 ),
inference(sat_conversion,[],[f3050]) ).
cnf(s1090,plain,
( spl14_10
| ~ spl14_27
| ~ spl14_35 ),
inference(sat_conversion,[],[f3055]) ).
cnf(s1092,plain,
( spl14_32
| ~ spl14_35
| ~ spl14_104 ),
inference(sat_conversion,[],[f3057]) ).
cnf(s1114,plain,
( ~ spl14_21
| ~ spl14_100 ),
inference(sat_conversion,[],[f3068]) ).
cnf(s1115,plain,
( ~ spl14_21
| spl14_26
| ~ spl14_117 ),
inference(sat_conversion,[],[f3069]) ).
cnf(s1116,plain,
( ~ spl14_21
| ~ spl14_112 ),
inference(sat_conversion,[],[f3070]) ).
cnf(s1132,plain,
( ~ spl14_78
| ~ spl14_104 ),
inference(sat_conversion,[],[f3071]) ).
cnf(s1139,plain,
( ~ spl14_105
| ~ spl14_106 ),
inference(sat_conversion,[],[f3072]) ).
cnf(s1158,plain,
( ~ spl14_1
| spl14_2
| ~ spl14_21 ),
inference(sat_conversion,[],[f3198]) ).
cnf(s1164,plain,
( ~ spl14_21
| spl14_22
| ~ spl14_28 ),
inference(sat_conversion,[],[f3200]) ).
cnf(s1206,plain,
( ~ spl14_1
| spl14_19
| ~ spl14_34 ),
inference(sat_conversion,[],[f3214]) ).
cnf(s1207,plain,
( spl14_13
| ~ spl14_34
| ~ spl14_99 ),
inference(sat_conversion,[],[f3215]) ).
cnf(s1212,plain,
( ~ spl14_1
| spl14_29
| ~ spl14_35 ),
inference(sat_conversion,[],[f3216]) ).
cnf(s1215,plain,
( spl14_15
| ~ spl14_35
| ~ spl14_95 ),
inference(sat_conversion,[],[f3217]) ).
cnf(s1250,plain,
( ~ spl14_21
| spl14_25
| ~ spl14_35 ),
inference(sat_conversion,[],[f3219]) ).
cnf(s1272,plain,
( ~ spl14_21
| spl14_23
| ~ spl14_115 ),
inference(sat_conversion,[],[f3223]) ).
cnf(s1281,plain,
( ~ spl14_44
| ~ spl14_50 ),
inference(sat_conversion,[],[f3227]) ).
cnf(s1323,plain,
( ~ spl14_21
| ~ spl14_102 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s1326,plain,
spl14_71,
inference(rat,[],[s86,s90]) ).
cnf(s1327,plain,
( ~ spl14_62
| spl14_76
| spl14_42
| spl14_48
| spl14_21
| spl14_54
| ~ spl14_60
| ~ spl14_74
| spl14_63
| ~ spl14_65
| ~ spl14_37
| ~ spl14_67
| spl14_69
| ~ spl14_72 ),
inference(rat,[],[s120,s144,s1326]) ).
cnf(s1333,plain,
( ~ spl14_50
| spl14_76
| spl14_48
| spl14_42
| spl14_54
| ~ spl14_37
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_72
| ~ spl14_74 ),
inference(rat,[],[s116,s140,s1326]) ).
cnf(s1339,plain,
( spl14_18
| ~ spl14_67
| ~ spl14_37
| spl14_34
| spl14_27
| spl14_97
| spl14_28
| spl14_9
| spl14_4
| spl14_54 ),
inference(rat,[],[s12,s1250,s1115,s191,s1327,s1333,s41,s393,s101,s168,s268,s641,s167,s152,s57,s105,s360,s489,s812,s186,s66,s72,s96,s84,s36,s54]) ).
cnf(s1341,plain,
( ~ spl14_69
| spl14_113
| spl14_107 ),
inference(rat,[],[s187,s800,s80,s84]) ).
cnf(s1345,plain,
( ~ spl14_51
| spl14_76
| spl14_48
| spl14_42
| spl14_54
| ~ spl14_37
| ~ spl14_60
| ~ spl14_62
| spl14_63
| ~ spl14_65
| ~ spl14_67
| spl14_69
| ~ spl14_72
| ~ spl14_74 ),
inference(rat,[],[s117,s141,s1326]) ).
cnf(s1347,plain,
( spl14_76
| spl14_69
| ~ spl14_62
| spl14_63
| spl14_108
| spl14_110
| ~ spl14_37
| ~ spl14_60
| ~ spl14_67
| ~ spl14_74
| spl14_58
| spl14_59
| spl14_42
| spl14_48
| spl14_9
| ~ spl14_65
| spl14_54 ),
inference(rat,[],[s1164,s10,s191,s1272,s303,s174,s173,s273,s1327,s1333,s96]) ).
cnf(s1348,plain,
( ~ spl14_76
| ~ spl14_34 ),
inference(rat,[],[s394,s188,s18,s292,s392,s103,s108,s368]) ).
cnf(s1349,plain,
( ~ spl14_69
| ~ spl14_34 ),
inference(rat,[],[s940,s17,s814,s1341,s84,s797]) ).
cnf(s1350,plain,
spl14_62,
inference(rat,[],[s57,s60]) ).
cnf(s1351,plain,
( spl14_18
| spl14_34
| ~ spl14_37
| ~ spl14_60
| ~ spl14_67
| ~ spl14_74
| spl14_58
| spl14_52
| spl14_27
| spl14_48
| spl14_9
| spl14_4
| spl14_54 ),
inference(rat,[],[s1272,s10,s165,s1164,s253,s1339,s634,s638,s193,s194,s302,s420,s119,s205,s1116,s1323,s1327,s81,s105,s361,s186,s66,s72,s96,s36,s1326,s1350]) ).
cnf(s1352,plain,
( spl14_76
| spl14_63
| ~ spl14_18
| ~ spl14_37
| ~ spl14_60
| ~ spl14_67
| ~ spl14_74
| spl14_58
| spl14_52
| spl14_42
| spl14_16
| spl14_9
| ~ spl14_65
| spl14_54 ),
inference(rat,[],[s10,s1272,s1164,s165,s191,s638,s599,s194,s11,s752,s660,s193,s171,s302,s420,s233,s119,s115,s154,s205,s1323,s1327,s1333,s96,s42,s659,s658,s83,s371,s1326,s1350]) ).
cnf(s1353,plain,
( ~ spl14_76
| ~ spl14_18 ),
inference(rat,[],[s389,s188,s16,s292,s450,s103,s108,s372]) ).
cnf(s1354,plain,
( ~ spl14_18
| ~ spl14_37
| ~ spl14_60
| ~ spl14_67
| ~ spl14_74
| spl14_46
| spl14_58
| spl14_52
| spl14_42
| spl14_16
| spl14_9
| ~ spl14_65
| spl14_54 ),
inference(rat,[],[s660,s11,s171,s599,s1139,s191,s185,s800,s811,s61,s62,s65,s1352,s1353,s659]) ).
cnf(s1355,plain,
( spl14_27
| spl14_16
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s1347,s1349,s1348,s368,s1003,s1351,s66,s1354,s28,s52,s76,s100,s485,s535,s807,s971,s181,s36,s48,s72,s42,s1350]) ).
cnf(s1356,plain,
( ~ spl14_74
| ~ spl14_67
| spl14_42
| spl14_69
| spl14_76
| spl14_57
| spl14_66
| spl14_63
| ~ spl14_37
| ~ spl14_60
| spl14_96
| spl14_98
| spl14_48
| spl14_9
| ~ spl14_65
| spl14_54 ),
inference(rat,[],[s1250,s12,s191,s1115,s642,s176,s175,s283,s1327,s1333,s96,s1350]) ).
cnf(s1357,plain,
( spl14_74
| ~ spl14_27 ),
inference(rat,[],[s518,s24,s184,s722,s293,s97,s102,s295]) ).
cnf(s1358,plain,
( spl14_67
| ~ spl14_27 ),
inference(rat,[],[s1092,s23,s183,s1090,s298,s74,s78,s305]) ).
cnf(s1359,plain,
( spl14_18
| spl14_34
| ~ spl14_67
| ~ spl14_74
| ~ spl14_37
| ~ spl14_60
| spl14_96
| spl14_98
| spl14_48
| spl14_9
| spl14_4
| spl14_54 ),
inference(rat,[],[s1356,s33,s81,s105,s361,s494,s186,s66,s72]) ).
cnf(s1360,plain,
( ~ spl14_18
| ~ spl14_27
| spl14_16
| spl14_9
| ~ spl14_65
| spl14_54 ),
inference(rat,[],[s660,s11,s190,s599,s603,s191,s800,s62,s63,s65,s1352,s34,s650,s1036,s185,s313,s15,s1353,s325,s371,s659,s53,s322,s30,s235,s1357,s1358]) ).
cnf(s1361,plain,
( spl14_28
| ~ spl14_21
| spl14_50
| spl14_51
| spl14_97
| spl14_9 ),
inference(rat,[],[s12,s1115,s1250,s167,s191]) ).
cnf(s1362,plain,
( spl14_16
| spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s1272,s10,s165,s1164,s253,s1361,s118,s205,s1327,s1333,s1345,s35,s1349,s1348,s329,s369,s1359,s66,s1360,s1358,s1357,s30,s53,s235,s295,s319,s322,s427,s1355,s42,s48,s72,s96,s1350,s1326]) ).
cnf(s1364,plain,
( spl14_34
| spl14_76
| ~ spl14_74
| ~ spl14_60
| spl14_48
| ~ spl14_37
| spl14_18
| ~ spl14_67
| spl14_27
| spl14_9
| spl14_4
| spl14_54 ),
inference(rat,[],[s1038,s194,s1351,s420,s118,s119,s205,s1116,s1327,s81,s361,s186,s72,s96,s36,s66,s1350,s1326]) ).
cnf(s1365,plain,
( spl14_76
| ~ spl14_74
| ~ spl14_60
| spl14_48
| ~ spl14_37
| spl14_18
| ~ spl14_16
| spl14_9
| spl14_4
| spl14_54 ),
inference(rat,[],[s194,s420,s355,s119,s182,s205,s1116,s353,s1327,s21,s1349,s725,s329,s1003,s1364,s72,s96,s390,s77,s330,s36,s198,s66,s1326,s1350]) ).
cnf(s1366,plain,
( ~ spl14_76
| spl14_18
| spl14_4 ),
inference(rat,[],[s186,s1348,s105]) ).
cnf(s1367,plain,
( spl14_74
| ~ spl14_16 ),
inference(rat,[],[s481,s22,s184,s816,s293,s97,s102,s332]) ).
cnf(s1368,plain,
( spl14_60
| ~ spl14_16 ),
inference(rat,[],[s353,s21,s182,s725,s329,s51,s54,s390]) ).
cnf(s1369,plain,
( ~ spl14_48
| ~ spl14_16
| spl14_9 ),
inference(rat,[],[s592,s9,s189,s608,s405,s191,s298,s38,s40,s41,s330]) ).
cnf(s1370,plain,
spl14_37,
inference(rat,[],[s28,s30]) ).
cnf(s1371,plain,
( spl14_18
| ~ spl14_16
| spl14_9
| spl14_4
| spl14_54 ),
inference(rat,[],[s1365,s1366,s1367,s1368,s1369,s1370]) ).
cnf(s1372,plain,
( spl14_63
| spl14_69
| spl14_76
| spl14_44
| spl14_42
| ~ spl14_67
| spl14_48
| ~ spl14_60
| ~ spl14_74
| spl14_39
| ~ spl14_72
| ~ spl14_65
| spl14_54 ),
inference(rat,[],[s137,s334,s170,s1333,s1350,s1370,s1326]) ).
cnf(s1373,plain,
( spl14_9
| spl14_4
| spl14_1 ),
inference(rat,[],[s660,s11,s190,s599,s603,s191,s800,s62,s63,s65,s1372,s83,s1353,s371,s451,s1371,s36,s77,s1369,s1368,s1367,s198,s330,s682,s1362,s96,s48,s72]) ).
cnf(s1374,plain,
( ~ spl14_72
| spl14_42
| spl14_76
| spl14_48
| spl14_54
| ~ spl14_60
| ~ spl14_74
| spl14_78
| ~ spl14_65
| ~ spl14_67
| spl14_69
| spl14_63 ),
inference(rat,[],[s143,s119,s1350,s1326,s1370]) ).
cnf(s1375,plain,
( spl14_96
| ~ spl14_45
| spl14_117
| spl14_56
| spl14_27
| ~ spl14_9 ),
inference(rat,[],[s510,s4,s195,s517,s514,s176,s151,s415,s546,s494]) ).
cnf(s1376,plain,
( ~ spl14_118
| spl14_110
| spl14_58
| ~ spl14_9 ),
inference(rat,[],[s575,s173,s6,s871,s282]) ).
cnf(s1377,plain,
( spl14_27
| ~ spl14_74
| ~ spl14_60
| spl14_18
| spl14_16
| spl14_4
| spl14_1 ),
inference(rat,[],[s1375,s413,s186,s175,s369,s93,s1376,s362,s634,s638,s189,s165,s308,s377,s92,s95,s1374,s535,s807,s181,s36,s48,s72,s418,s415,s84,s399,s78,s200,s1373,s42,s66,s1366]) ).
cnf(s1378,plain,
( spl14_72
| ~ spl14_27
| spl14_18
| ~ spl14_9
| spl14_4 ),
inference(rat,[],[s4,s510,s517,s195,s175,s1376,s1003,s186,s489,s190,s446,s189,s308,s376,s92,s93,s94,s95,s418,s417,s415,s427,s319]) ).
cnf(s1379,plain,
( ~ spl14_42
| spl14_18
| spl14_4 ),
inference(rat,[],[s186,s329,s33,s35]) ).
cnf(s1380,plain,
( ~ spl14_74
| ~ spl14_60
| spl14_18
| spl14_16
| spl14_4
| spl14_1 ),
inference(rat,[],[s1378,s1374,s1377,s48,s72,s415,s84,s399,s78,s200,s1373,s42,s66,s1366,s1379]) ).
cnf(s1381,plain,
( spl14_74
| spl14_16
| spl14_1 ),
inference(rat,[],[s181,s1357,s100]) ).
cnf(s1382,plain,
( spl14_60
| spl14_16
| spl14_1 ),
inference(rat,[],[s181,s322,s52,s53]) ).
cnf(s1383,plain,
( spl14_27
| spl14_16
| spl14_4
| spl14_1 ),
inference(rat,[],[s308,s189,s95,s807,s1374,s181,s36,s48,s72,s418,s415,s84,s399,s78,s200,s42,s1353,s511,s63,s190,s921,s8,s923,s371,s1380,s1382,s1381,s417,s1373]) ).
cnf(s1384,plain,
( spl14_16
| spl14_4
| spl14_1 ),
inference(rat,[],[s95,s308,s1374,s189,s34,s650,s185,s313,s15,s325,s322,s1383,s63,s511,s190,s921,s1353,s8,s371,s659,s923,s1380,s1382,s1381,s42,s48,s72,s418,s417,s415,s84,s399,s78,s200,s1373]) ).
cnf(s1385,plain,
( spl14_18
| spl14_48
| spl14_63
| spl14_109
| ~ spl14_16
| ~ spl14_67
| spl14_69
| spl14_78
| spl14_114
| spl14_4
| spl14_54 ),
inference(rat,[],[s21,s353,s725,s164,s186,s401,s489,s162,s190,s376,s95,s1374,s1366,s72,s390,s1367,s1368,s36,s198]) ).
cnf(s1386,plain,
( spl14_4
| spl14_1 ),
inference(rat,[],[s92,s170,s1372,s1353,s451,s1385,s40,s64,s446,s189,s577,s36,s7,s1368,s1367,s198,s330,s576,s682,s1384,s78,s84,s200,s399,s415,s417,s418,s513,s1373,s72,s48]) ).
cnf(s1387,plain,
( spl14_72
| spl14_52
| spl14_58
| spl14_98
| ~ spl14_9 ),
inference(rat,[],[s4,s510,s517,s195,s175,s1376,s638,s165,s377,s92,s93,s95,s415,s200]) ).
cnf(s1388,plain,
( spl14_65
| spl14_58
| spl14_98
| spl14_55
| ~ spl14_9
| ~ spl14_4 ),
inference(rat,[],[s288,s2,s196,s287,s646,s1376,s175,s292,s69,s71]) ).
cnf(s1389,plain,
( spl14_27
| ~ spl14_9
| spl14_16
| spl14_1 ),
inference(rat,[],[s1387,s807,s1374,s181,s36,s48,s107,s477,s54,s199,s66,s197,s42,s1381,s415,s84,s399,s78,s200,s1388,s210,s268,s300,s156,s418,s312,s1386]) ).
cnf(s1390,plain,
( ~ spl14_9
| spl14_16
| spl14_1 ),
inference(rat,[],[s1374,s95,s34,s308,s185,s154,s229,s13,s1081,s322,s1389,s1388,s210,s223,s268,s300,s78,s84,s156,s200,s399,s415,s418,s48,s312,s107,s477,s54,s199,s66,s197,s1386,s42,s1381]) ).
cnf(s1391,plain,
( spl14_69
| ~ spl14_65
| spl14_27
| spl14_16
| spl14_1 ),
inference(rat,[],[s194,s287,s752,s2,s193,s288,s1116,s1323,s302,s1327,s1374,s48,s107,s477,s54,s199,s66,s197,s1386,s42,s1381,s96,s1390,s36,s535,s76,s181,s1350,s1370]) ).
cnf(s1392,plain,
( ~ spl14_69
| ~ spl14_4 ),
inference(rat,[],[s14,s801,s944,s1341,s84,s617]) ).
cnf(s1393,plain,
( spl14_38
| spl14_102
| spl14_108
| spl14_96
| spl14_55
| spl14_56
| spl14_59
| ~ spl14_4 ),
inference(rat,[],[s5,s529,s1011,s177,s174,s1114,s231,s184,s180,s476]) ).
cnf(s1394,plain,
( spl14_28
| spl14_97
| spl14_100
| spl14_35
| spl14_111
| spl14_117
| spl14_47
| spl14_9
| ~ spl14_4 ),
inference(rat,[],[s2,s287,s288,s158,s178,s248,s595,s167,s191,s199]) ).
cnf(s1395,plain,
( spl14_27
| spl14_16
| spl14_1 ),
inference(rat,[],[s14,s801,s944,s1394,s634,s193,s302,s172,s213,s1060,s1393,s674,s769,s157,s185,s241,s271,s294,s309,s842,s67,s68,s71,s485,s488,s535,s971,s1391,s181,s617,s312,s199,s1392,s1386,s1390]) ).
cnf(s1396,plain,
( spl14_65
| ~ spl14_27
| spl14_9
| ~ spl14_4 ),
inference(rat,[],[s1092,s23,s183,s1090,s298,s191,s412,s1281,s942,s187,s160,s556,s69,s71,s617,s254,s667,s305,s707,s185,s229,s13,s1081,s312,s322]) ).
cnf(s1397,plain,
( spl14_16
| spl14_1 ),
inference(rat,[],[s193,s1323,s302,s1327,s1374,s1396,s34,s1036,s185,s229,s13,s1081,s1358,s319,s322,s1395,s96,s1390,s1381,s42,s48,s312,s107,s477,s54,s199,s66,s197,s1392,s1386,s1350,s1370]) ).
cnf(s1398,plain,
( ~ spl14_78
| spl14_9
| spl14_65
| spl14_1 ),
inference(rat,[],[s5,s1011,s529,s174,s162,s306,s250,s191,s167,s608,s9,s592,s634,s206,s156,s193,s155,s302,s1132,s312,s299,s455,s390,s70,s309,s241,s1281,s161,s271,s71,s197,s1386,s706,s1397]) ).
cnf(s1399,plain,
( spl14_9
| spl14_65
| spl14_1 ),
inference(rat,[],[s2,s287,s288,s173,s178,s282,s293,s255,s175,s184,s180,s268,s1060,s179,s172,s1398,s617,s477,s476,s1386,s332,s1397,s70,s69,s67,s294,s292,s271,s71]) ).
cnf(s1400,plain,
( spl14_65
| spl14_1 ),
inference(rat,[],[s267,s156,s1388,s418,s1399,s67,s70,s312,s1386]) ).
cnf(s1401,plain,
( spl14_9
| spl14_1 ),
inference(rat,[],[s192,s362,s306,s1361,s191,s608,s9,s376,s592,s162,s156,s115,s1116,s302,s955,s1345,s1327,s1333,s1374,s1369,s96,s48,s312,s107,s477,s54,s199,s66,s197,s1392,s1386,s390,s1367,s77,s330,s36,s198,s1397,s1400,s1370,s1350,s1326]) ).
cnf(s1402,plain,
spl14_1,
inference(rat,[],[s4,s510,s517,s195,s175,s1376,s279,s162,s376,s92,s93,s95,s118,s40,s189,s577,s210,s268,s300,s7,s156,s576,s415,s418,s1401,s1400,s36,s77,s1367,s198,s330,s390,s1397,s1392,s66,s54,s107,s197,s199,s312,s477,s1386,s48,s1370,s1350,s1326]) ).
cnf(s1403,plain,
~ spl14_104,
inference(rat,[],[s795,s1402]) ).
cnf(s1404,plain,
~ spl14_75,
inference(rat,[],[s497,s1402]) ).
cnf(s1405,plain,
~ spl14_105,
inference(rat,[],[s442,s1402]) ).
cnf(s1406,plain,
~ spl14_106,
inference(rat,[],[s408,s1402]) ).
cnf(s1407,plain,
~ spl14_38,
inference(rat,[],[s407,s1402]) ).
cnf(s1408,plain,
~ spl14_103,
inference(rat,[],[s340,s1402]) ).
cnf(s1409,plain,
~ spl14_16,
inference(rat,[],[s337,s1402]) ).
cnf(s1410,plain,
~ spl14_27,
inference(rat,[],[s226,s1402]) ).
cnf(s1411,plain,
spl14_74,
inference(rat,[],[s101,s1404]) ).
cnf(s1412,plain,
~ spl14_48,
inference(rat,[],[s42,s1409]) ).
cnf(s1413,plain,
~ spl14_42,
inference(rat,[],[s36,s1410]) ).
cnf(s1414,plain,
( spl14_102
| spl14_65
| ~ spl14_4 ),
inference(rat,[],[s1158,s196,s1,s293,s613,s1393,s193,s70,s68,s67,s294,s292,s241,s71,s1402,s1407,s1404]) ).
cnf(s1415,plain,
( spl14_65
| ~ spl14_4 ),
inference(rat,[],[s646,s194,s196,s712,s1323,s1414,s292,s67,s69,s71,s477]) ).
cnf(s1416,plain,
spl14_67,
inference(rat,[],[s1215,s20,s183,s1212,s298,s74,s78,s1403,s1402]) ).
cnf(s1417,plain,
( ~ spl14_98
| spl14_36
| spl14_55 ),
inference(rat,[],[s1158,s1,s196,s613,s414,s1402]) ).
cnf(s1418,plain,
( spl14_55
| ~ spl14_49
| ~ spl14_60
| spl14_63
| ~ spl14_65
| spl14_76
| spl14_69
| ~ spl14_72 ),
inference(rat,[],[s436,s3,s196,s474,s1323,s193,s1417,s293,s46,s47,s115,s1411,s1326,s1350,s1370,s1416,s1413,s1412,s1404,s1402]) ).
cnf(s1419,plain,
( spl14_9
| ~ spl14_4 ),
inference(rat,[],[s1418,s955,s171,s172,s96,s617,s321,s1392,s107,s477,s54,s199,s66,s197,s1415,s1406,s1403]) ).
cnf(s1420,plain,
~ spl14_4,
inference(rat,[],[s1327,s43,s91,s205,s180,s625,s1419,s1415,s66,s54,s107,s1392,s197,s199,s476,s477,s1413,s1416,s1350,s1412,s1370,s1411,s1407]) ).
cnf(s1421,plain,
spl14_65,
inference(rat,[],[s72,s1420]) ).
cnf(s1422,plain,
( spl14_18
| spl14_112
| spl14_70
| spl14_54
| spl14_76
| ~ spl14_60
| spl14_9 ),
inference(rat,[],[s19,s1207,s1206,s162,s1364,s1402,s1411,s1370,s1412,s1416,s1410,s1420]) ).
cnf(s1423,plain,
( spl14_63
| ~ spl14_78
| spl14_54
| spl14_76
| spl14_69
| ~ spl14_60
| spl14_9 ),
inference(rat,[],[s10,s1272,s1164,s174,s1361,s289,s336,s182,s154,s438,s659,s1422,s355,s194,s1038,s193,s1417,s273,s1116,s1323,s1333,s1345,s1327,s96,s955,s458,s163,s984,s346,s164,s420,s1408,s1409,s1404,s1412,s1370,s1350,s1413,s1411,s1416,s1421,s1420,s1405]) ).
cnf(s1424,plain,
( ~ spl14_78
| spl14_54
| spl14_76
| spl14_69
| ~ spl14_60
| spl14_9 ),
inference(rat,[],[s599,s191,s11,s800,s660,s62,s65,s66,s1423,s164,s420,s1420,s1408]) ).
cnf(s1425,plain,
( spl14_54
| spl14_76
| spl14_69
| ~ spl14_60
| spl14_9 ),
inference(rat,[],[s65,s344,s1374,s172,s1424,s96,s1411,s1412,s1413,s1416,s1421,s1403]) ).
cnf(s1426,plain,
~ spl14_54,
inference(rat,[],[s436,s3,s196,s474,s1323,s193,s1417,s293,s43,s46,s47,s1402,s1404]) ).
cnf(s1427,plain,
~ spl14_76,
inference(rat,[],[s1366,s1353,s1420]) ).
cnf(s1428,plain,
~ spl14_69,
inference(rat,[],[s186,s371,s1349,s81,s83,s1420]) ).
cnf(s1429,plain,
spl14_60,
inference(rat,[],[s1207,s19,s182,s1206,s329,s51,s54,s1408,s1402]) ).
cnf(s1430,plain,
spl14_9,
inference(rat,[],[s1425,s1428,s1427,s1426,s1429]) ).
cnf(s1433,plain,
~ spl14_114,
inference(rat,[],[s417,s1430]) ).
cnf(s1435,plain,
~ spl14_78,
inference(rat,[],[s415,s1430]) ).
cnf(s1438,plain,
spl14_77,
inference(rat,[],[s164,s1408,s1420,s1433]) ).
cnf(s1440,plain,
~ spl14_112,
inference(rat,[],[s401,s1438]) ).
cnf(s1441,plain,
~ spl14_55,
inference(rat,[],[s354,s1438]) ).
cnf(s1442,plain,
~ spl14_110,
inference(rat,[],[s269,s1438]) ).
cnf(s1444,plain,
spl14_72,
inference(rat,[],[s272,s177,s1417,s246,s175,s517,s4,s510,s195,s1376,s92,s93,s94,s1440,s1441,s1430,s1435,s1442]) ).
cnf(s1445,plain,
spl14_63,
inference(rat,[],[s1374,s1421,s1428,s1416,s1413,s1412,s1429,s1411,s1435,s1427,s1426,s1444]) ).
cnf(s1446,plain,
spl14_18,
inference(rat,[],[s66,s1445]) ).
cnf(s1449,plain,
~ spl14_51,
inference(rat,[],[s63,s1445]) ).
cnf(s1450,plain,
spl14_19,
inference(rat,[],[s923,s1430,s1446]) ).
cnf(s1455,plain,
~ spl14_70,
inference(rat,[],[s371,s1446]) ).
cnf(s1457,plain,
~ spl14_6,
inference(rat,[],[s8,s1450,s1446]) ).
cnf(s1467,plain,
spl14_109,
inference(rat,[],[s190,s1433,s1455,s1449]) ).
cnf(s1469,plain,
$false,
inference(rat,[],[s921,s1446,s1457,s1467]) ).
fof(f3231,plain,
$false,
inference(avatar_sat_refutation,[],[s1469]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG133+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n015.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 19:35:32 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.35 % (2935937)Will run a generic schedule for satisfiability detection.
% 0.20/0.35 % (2935958)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2760575079:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.20/0.35 % (2935955)% WARNING: option uhcvi not known.
% 0.20/0.35 % (2935954)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3217823144_2999 on theBenchmark for (2999ds/0Mi)
% 0.20/0.35 % (2935956)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2776900260:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.20/0.35 % (2935955)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2377616235:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.20/0.35 % (2935957)dis+10_1_sil=32000:sp=arity:random_seed=3570217648:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.20/0.35 % (2935959)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2923276142:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.20/0.35 % (2935960)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1114436135:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.20/0.35 % Detected minimum model sizes of [4]
% 0.20/0.35 % Detected maximum model sizes of [max]
% 0.20/0.35 % TRYING [4]
% 0.20/0.35 % (2935958)Instruction limit reached!
% 0.20/0.35 % (2935958)------------------------------
% 0.20/0.35 % (2935958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2935958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2935958)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2935958)Termination reason: Instruction limit
% 0.20/0.35 % (2935958)Termination phase: Saturation
% 0.20/0.35 % (2935958)Time elapsed: 0.033 s
% 0.20/0.35 % (2935958)Peak memory usage: 13 MB
% 0.20/0.35 % (2935958)Instructions burned: 119 (million)
% 0.20/0.35 % TRYING [5]
% 0.20/0.35 % (2935976)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3643074256:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.20/0.35 % Detected minimum model sizes of [4]
% 0.20/0.35 % Detected maximum model sizes of [max]
% 0.20/0.35 % TRYING [4]
% 0.20/0.35 % TRYING [5]
% 0.20/0.35 % TRYING [6]
% 0.20/0.35 % TRYING [6]
% 0.20/0.35 % (2935957)Instruction limit reached!
% 0.20/0.35 % (2935957)------------------------------
% 0.20/0.35 % (2935957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2935957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2935957)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2935957)Termination reason: Instruction limit
% 0.20/0.35 % (2935957)Termination phase: Saturation
% 0.20/0.35 % (2935957)Time elapsed: 0.062 s
% 0.20/0.35 % (2935957)Peak memory usage: 12 MB
% 0.20/0.35 % (2935957)Instructions burned: 104 (million)
% 0.20/0.35 % (2935959)Instruction limit reached!
% 0.20/0.35 % (2935959)------------------------------
% 0.20/0.35 % (2935959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.35 % (2935959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.35 % (2935959)CaDiCaL version: 2.1.3
% 0.20/0.35 % (2935959)Termination reason: Instruction limit
% 0.20/0.35 % (2935959)Termination phase: Saturation
% 0.20/0.35 % (2935959)Time elapsed: 0.067 s
% 0.20/0.35 % (2935959)Peak memory usage: 13 MB
% 0.20/0.35 % (2935959)Instructions burned: 133 (million)
% 0.20/0.35 % (2935955) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2935937-2935955"...
% 0.20/0.35 % (2935960) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2935937-2935960"...
% 0.20/0.35 % (2935988)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1857125840:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 0.20/0.35 % TRYING [7]
% 0.20/0.35 % (2935991)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1395048886:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.20/0.35 % (2935955)...printing done.
% 0.20/0.35 % (2935955)Refutation found. Thanks to Tanya!
% 0.20/0.35 % SZS status Unsatisfiable for theBenchmark
% 0.20/0.35 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/0.37 % (2935955)------------------------------
% 0.20/0.37 % (2935955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.37 % (2935955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.37 % (2935955)CaDiCaL version: 2.1.3
% 0.20/0.37 % (2935955)Termination reason: Refutation
% 0.20/0.37 % (2935955)Time elapsed: 0.088 s
% 0.20/0.37 % (2935955)Peak memory usage: 13 MB
% 0.20/0.37 % (2935955)Instructions burned: 165 (million)
% 0.20/0.37 % (2935937)Success in time 0.136 s
% 0.20/0.37 % Vampire exiting
%------------------------------------------------------------------------------