%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN481-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 01:56:14 PM UTC 2026
% Result : Unsatisfiable 0.66s 1.00s
% Output : Refutation 2.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 268
% Syntax : Number of formulae : 1109 ( 25 unt; 143 def)
% Number of atoms : 3668 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 4680 (2121 ~;2416 |; 0 &)
% ( 143 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 177 ( 176 usr; 173 prp; 0-1 aty)
% Number of functors : 28 ( 28 usr; 28 con; 0-0 aty)
% Number of variables : 147 ( 0 sgn 147 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp20
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f2,negated_conjecture,
( ~ hskp30
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f5,negated_conjecture,
( ~ hskp27
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
fof(f12,negated_conjecture,
( ~ hskp20
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
fof(f33,negated_conjecture,
( hskp27
| hskp20
| hskp30 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f35,negated_conjecture,
( hskp12
| hskp5
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( hskp12
| hskp25
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp30
| hskp6
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp10
| hskp18
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f39,negated_conjecture,
( hskp0
| hskp5
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f42,negated_conjecture,
( hskp15
| hskp19
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f44,negated_conjecture,
( hskp25
| hskp17
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f47,negated_conjecture,
( ~ hskp30
| c0_1(a1712) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp30
| c2_1(a1712) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp30
| c3_1(a1712) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp29
| c0_1(a1647) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp29
| c1_1(a1647) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp29
| c3_1(a1647) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp28
| c1_1(a1646) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp28
| c2_1(a1646) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp28
| c3_1(a1646) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp27
| c0_1(a1635) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp27
| c1_1(a1635) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp27
| c2_1(a1635) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f61,negated_conjecture,
( ~ hskp25
| c1_1(a1709) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp25
| c2_1(a1709) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp24
| c3_1(a1701) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f65,negated_conjecture,
( ~ hskp21
| c3_1(a1691) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( ~ hskp20
| c0_1(a1689) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( ~ hskp20
| c1_1(a1689) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp19
| c1_1(a1682) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp19
| c2_1(a1682) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp18
| c1_1(a1680) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp17
| c2_1(a1675) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp16
| c0_1(a1667) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp16
| c2_1(a1667) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp15
| c0_1(a1664) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp14
| c0_1(a1661) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f77,negated_conjecture,
( ~ hskp13
| c3_1(a1658) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp12
| c0_1(a1653) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp12
| c1_1(a1653) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp11
| c1_1(a1650) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp10
| c0_1(a1648) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp10
| c2_1(a1648) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f85,negated_conjecture,
( ~ hskp6
| c2_1(a1641) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp5
| c0_1(a1640) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp5
| c3_1(a1640) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp4
| c3_1(a1639) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ hskp3
| c3_1(a1638) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ hskp2
| c1_1(a1637) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp2
| c3_1(a1637) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp0
| c0_1(a1634) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ hskp0
| c3_1(a1634) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f95,negated_conjecture,
( ~ c0_1(a1709)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c0_1(a1701)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c1_1(a1701)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c1_1(a1699)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c2_1(a1699)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f101,negated_conjecture,
( ~ c0_1(a1697)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c2_1(a1697)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c3_1(a1697)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c1_1(a1691)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c2_1(a1689)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c3_1(a1682)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c0_1(a1680)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f109,negated_conjecture,
( ~ c0_1(a1675)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c1_1(a1675)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c1_1(a1667)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c1_1(a1664)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c2_1(a1664)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c1_1(a1661)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c3_1(a1661)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f117,negated_conjecture,
( ~ c3_1(a1653)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c0_1(a1650)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c3_1(a1650)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c3_1(a1648)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c0_1(a1644)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c1_1(a1644)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c3_1(a1644)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f129,negated_conjecture,
( ~ c3_1(a1641)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ c2_1(a1640)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ c1_1(a1639)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ c2_1(a1639)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ c0_1(a1638)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f135,negated_conjecture,
( ~ c0_1(a1637)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
( ~ c0_1(a1636)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( ~ c1_1(a1636)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
( ~ c2_1(a1636)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( ~ c1_1(a1634)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| hskp27
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| hskp2
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp10
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f145,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp0
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp16
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp16
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp2
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp29
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp13
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp0
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp29
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp29
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp28
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f161,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp4
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp29
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp20
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f175,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f179,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f183,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f187,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f190,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f192,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X2)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X2)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X2)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause197) ).
fof(f199,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f202,definition,
( spl0_1
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f203,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f202]) ).
fof(f205,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f206,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f208,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f211,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f212,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f213,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f200,f211,f208,f205,f202]) ).
fof(f215,definition,
( spl0_5
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f216,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f219,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f221,definition,
( spl0_7
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f222,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f223,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f199,f221,f208,f218,f215]) ).
fof(f225,definition,
( spl0_8
<=> ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f226,plain,
( ! [X2] :
( c1_1(X2)
| ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f229,definition,
( spl0_9
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f230,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,definition,
( spl0_10
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f233,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f234,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f197,f232,f208,f229,f225]) ).
fof(f236,definition,
( spl0_11
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f237,plain,
( ! [X2] :
( c1_1(X2)
| ~ c2_1(X2)
| c0_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,definition,
( spl0_12
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f240,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( spl0_11
| spl0_12
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f196,f232,f208,f239,f236]) ).
fof(f243,definition,
( spl0_13
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f244,plain,
( ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f246,definition,
( spl0_14
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f247,plain,
( ! [X1] :
( c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f248,plain,
( spl0_13
| spl0_14
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f195,f239,f208,f246,f243]) ).
fof(f250,definition,
( spl0_15
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f251,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,definition,
( spl0_16
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f254,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f255,plain,
( spl0_15
| spl0_16
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f194,f229,f208,f253,f250]) ).
fof(f257,definition,
( spl0_17
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f258,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( spl0_11
| spl0_14
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f193,f257,f208,f246,f236]) ).
fof(f261,definition,
( spl0_18
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f262,plain,
( ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( spl0_18
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f192,f221,f208,f218,f261]) ).
fof(f265,definition,
( spl0_19
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f266,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,definition,
( spl0_20
<=> ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f269,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f272,definition,
( spl0_21
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f274,plain,
( spl0_21
| spl0_7
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f190,f211,f208,f221,f272]) ).
fof(f276,definition,
( spl0_22
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f280,definition,
( spl0_23
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f282,plain,
( spl0_23
| spl0_12
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f188,f205,f208,f239,f280]) ).
fof(f284,definition,
( spl0_24
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f285,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f284]) ).
fof(f287,definition,
( spl0_25
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f288,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f289,plain,
( spl0_24
| spl0_15
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f187,f287,f208,f250,f284]) ).
fof(f291,definition,
( spl0_26
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f295,definition,
( spl0_27
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f298,definition,
( spl0_28
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f299,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f301,definition,
( spl0_29
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f302,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f305,definition,
( spl0_30
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f307,plain,
( spl0_30
| spl0_28
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f184,f301,f208,f298,f305]) ).
fof(f309,definition,
( spl0_31
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f311,plain,
( spl0_31
| spl0_20
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f183,f239,f208,f268,f309]) ).
fof(f313,definition,
( spl0_32
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f328,definition,
( spl0_36
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f330,plain,
( spl0_36
| spl0_1
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f179,f257,f208,f202,f328]) ).
fof(f332,definition,
( spl0_37
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f333,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f336,definition,
( spl0_38
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f338,plain,
( spl0_38
| spl0_5
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f177,f246,f208,f215,f336]) ).
fof(f340,definition,
( spl0_39
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f342,plain,
( spl0_39
| spl0_19
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f176,f257,f208,f265,f340]) ).
fof(f344,definition,
( spl0_40
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f346,plain,
( spl0_40
| spl0_19
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f175,f298,f208,f265,f344]) ).
fof(f353,plain,
( spl0_8
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f171,f253,f208,f225]) ).
fof(f355,definition,
( spl0_42
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f358,definition,
( spl0_43
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f359,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( spl0_42
| spl0_18
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f170,f358,f208,f261,f355]) ).
fof(f362,definition,
( spl0_44
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f365,plain,
( spl0_40
| spl0_15
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f168,f246,f208,f250,f344]) ).
fof(f367,definition,
( spl0_45
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f374,definition,
( spl0_47
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f380,definition,
( spl0_48
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f383,definition,
( spl0_49
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f385,plain,
( spl0_48
| spl0_49
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f163,f205,f208,f383,f380]) ).
fof(f387,definition,
( spl0_50
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f389,plain,
( spl0_50
| spl0_40
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f162,f205,f208,f344,f387]) ).
fof(f391,definition,
( spl0_51
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f393,plain,
( spl0_51
| spl0_42
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f161,f221,f208,f355,f391]) ).
fof(f395,definition,
( spl0_52
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f404,definition,
( spl0_54
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f406,plain,
( spl0_54
| spl0_23
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f157,f257,f208,f280,f404]) ).
fof(f407,plain,
( spl0_22
| spl0_40
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f156,f218,f208,f344,f276]) ).
fof(f408,plain,
( spl0_39
| spl0_40
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f155,f218,f208,f344,f340]) ).
fof(f409,plain,
( spl0_23
| spl0_45
| ~ spl0_3
| spl0_20 ),
inference(avatar_split_clause,[],[f154,f268,f208,f367,f280]) ).
fof(f411,definition,
( spl0_55
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f413,plain,
( spl0_38
| spl0_55
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f153,f253,f208,f411,f336]) ).
fof(f414,plain,
( spl0_32
| spl0_40
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f152,f253,f208,f344,f313]) ).
fof(f418,definition,
( spl0_56
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f421,definition,
( spl0_57
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f424,plain,
( spl0_22
| spl0_30
| ~ spl0_3
| spl0_37 ),
inference(avatar_split_clause,[],[f148,f332,f208,f305,f276]) ).
fof(f426,definition,
( spl0_58
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f429,definition,
( spl0_59
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f431,plain,
( spl0_58
| spl0_59
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f147,f202,f208,f429,f426]) ).
fof(f432,plain,
( spl0_45
| spl0_59
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f146,f246,f208,f429,f367]) ).
fof(f433,plain,
( spl0_23
| spl0_45
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f145,f225,f208,f367,f280]) ).
fof(f436,plain,
( spl0_52
| spl0_58
| spl0_15
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f142,f208,f250,f426,f395]) ).
fof(f437,plain,
( spl0_44
| spl0_30
| spl0_24
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f141,f208,f284,f305,f362]) ).
fof(f438,plain,
( spl0_52
| spl0_57
| spl0_24
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f140,f208,f284,f421,f395]) ).
fof(f441,definition,
( spl0_60
<=> c1_1(a1634) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f442,plain,
( ~ c1_1(a1634)
| spl0_60 ),
inference(avatar_component_clause,[],[f441]) ).
fof(f443,plain,
( ~ spl0_45
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f139,f441,f367]) ).
fof(f446,definition,
( spl0_61
<=> c2_1(a1636) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f447,plain,
( ~ c2_1(a1636)
| spl0_61 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f448,plain,
( ~ spl0_52
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f138,f446,f395]) ).
fof(f450,definition,
( spl0_62
<=> c1_1(a1636) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f451,plain,
( ~ c1_1(a1636)
| spl0_62 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f452,plain,
( ~ spl0_52
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f137,f450,f395]) ).
fof(f454,definition,
( spl0_63
<=> c0_1(a1636) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f455,plain,
( ~ c0_1(a1636)
| spl0_63 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f456,plain,
( ~ spl0_52
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f136,f454,f395]) ).
fof(f459,definition,
( spl0_64
<=> c0_1(a1637) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f460,plain,
( ~ c0_1(a1637)
| spl0_64 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f461,plain,
( ~ spl0_30
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f135,f459,f305]) ).
fof(f468,definition,
( spl0_66
<=> c0_1(a1638) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f469,plain,
( ~ c0_1(a1638)
| spl0_66 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f470,plain,
( ~ spl0_44
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f133,f468,f362]) ).
fof(f473,definition,
( spl0_67
<=> c2_1(a1639) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f475,plain,
( ~ spl0_42
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f132,f473,f355]) ).
fof(f477,definition,
( spl0_68
<=> c1_1(a1639) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f478,plain,
( ~ c1_1(a1639)
| spl0_68 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f479,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f131,f477,f355]) ).
fof(f482,definition,
( spl0_69
<=> c2_1(a1640) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f483,plain,
( ~ c2_1(a1640)
| spl0_69 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f484,plain,
( ~ spl0_32
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f130,f482,f313]) ).
fof(f487,definition,
( spl0_70
<=> c3_1(a1641) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f488,plain,
( ~ c3_1(a1641)
| spl0_70 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f489,plain,
( ~ spl0_56
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f129,f487,f418]) ).
fof(f514,definition,
( spl0_76
<=> c3_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f515,plain,
( ~ c3_1(a1644)
| spl0_76 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f516,plain,
( ~ spl0_22
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f123,f514,f276]) ).
fof(f518,definition,
( spl0_77
<=> c1_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f519,plain,
( ~ c1_1(a1644)
| spl0_77 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f520,plain,
( ~ spl0_22
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f122,f518,f276]) ).
fof(f522,definition,
( spl0_78
<=> c0_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f523,plain,
( ~ c0_1(a1644)
| spl0_78 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f524,plain,
( ~ spl0_22
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f121,f522,f276]) ).
fof(f527,definition,
( spl0_79
<=> c3_1(a1648) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f528,plain,
( ~ c3_1(a1648)
| spl0_79 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f529,plain,
( ~ spl0_58
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f120,f527,f426]) ).
fof(f532,definition,
( spl0_80
<=> c3_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f533,plain,
( ~ c3_1(a1650)
| spl0_80 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f534,plain,
( ~ spl0_38
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f119,f532,f336]) ).
fof(f536,definition,
( spl0_81
<=> c0_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f537,plain,
( ~ c0_1(a1650)
| spl0_81 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f538,plain,
( ~ spl0_38
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f118,f536,f336]) ).
fof(f541,definition,
( spl0_82
<=> c3_1(a1653) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f543,plain,
( ~ spl0_39
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f117,f541,f340]) ).
fof(f551,definition,
( spl0_84
<=> c3_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f552,plain,
( ~ c3_1(a1661)
| spl0_84 ),
inference(avatar_component_clause,[],[f551]) ).
fof(f553,plain,
( ~ spl0_36
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f115,f551,f328]) ).
fof(f555,definition,
( spl0_85
<=> c1_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f556,plain,
( ~ c1_1(a1661)
| spl0_85 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f557,plain,
( ~ spl0_36
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f114,f555,f328]) ).
fof(f560,definition,
( spl0_86
<=> c2_1(a1664) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f561,plain,
( ~ c2_1(a1664)
| spl0_86 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( ~ spl0_31
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f113,f560,f309]) ).
fof(f564,definition,
( spl0_87
<=> c1_1(a1664) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f565,plain,
( ~ c1_1(a1664)
| spl0_87 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f566,plain,
( ~ spl0_31
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f112,f564,f309]) ).
fof(f569,definition,
( spl0_88
<=> c1_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f570,plain,
( ~ c1_1(a1667)
| spl0_88 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f571,plain,
( ~ spl0_59
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f111,f569,f429]) ).
fof(f574,definition,
( spl0_89
<=> c1_1(a1675) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f575,plain,
( ~ c1_1(a1675)
| spl0_89 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( ~ spl0_27
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f110,f574,f295]) ).
fof(f578,definition,
( spl0_90
<=> c0_1(a1675) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f580,plain,
( ~ spl0_27
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f109,f578,f295]) ).
fof(f587,definition,
( spl0_92
<=> c0_1(a1680) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f588,plain,
( ~ c0_1(a1680)
| spl0_92 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f589,plain,
( ~ spl0_26
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f107,f587,f291]) ).
fof(f592,definition,
( spl0_93
<=> c3_1(a1682) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f593,plain,
( ~ c3_1(a1682)
| spl0_93 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f594,plain,
( ~ spl0_54
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f106,f592,f404]) ).
fof(f597,definition,
( spl0_94
<=> c2_1(a1689) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f598,plain,
( ~ c2_1(a1689)
| spl0_94 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f599,plain,
( ~ spl0_49
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f105,f597,f383]) ).
fof(f602,definition,
( spl0_95
<=> c1_1(a1691) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f603,plain,
( ~ c1_1(a1691)
| spl0_95 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f604,plain,
( ~ spl0_48
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f104,f602,f380]) ).
fof(f607,definition,
( spl0_96
<=> c3_1(a1697) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f608,plain,
( ~ c3_1(a1697)
| spl0_96 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f609,plain,
( ~ spl0_21
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f103,f607,f272]) ).
fof(f611,definition,
( spl0_97
<=> c2_1(a1697) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f612,plain,
( ~ c2_1(a1697)
| spl0_97 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f613,plain,
( ~ spl0_21
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f102,f611,f272]) ).
fof(f615,definition,
( spl0_98
<=> c0_1(a1697) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f616,plain,
( ~ c0_1(a1697)
| spl0_98 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f617,plain,
( ~ spl0_21
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f101,f615,f272]) ).
fof(f624,definition,
( spl0_100
<=> c2_1(a1699) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f625,plain,
( ~ c2_1(a1699)
| spl0_100 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f626,plain,
( ~ spl0_51
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f99,f624,f391]) ).
fof(f628,definition,
( spl0_101
<=> c1_1(a1699) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f629,plain,
( ~ c1_1(a1699)
| spl0_101 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( ~ spl0_51
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f98,f628,f391]) ).
fof(f633,definition,
( spl0_102
<=> c1_1(a1701) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f634,plain,
( ~ c1_1(a1701)
| spl0_102 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f635,plain,
( ~ spl0_50
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f97,f633,f387]) ).
fof(f637,definition,
( spl0_103
<=> c0_1(a1701) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f638,plain,
( ~ c0_1(a1701)
| spl0_103 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f639,plain,
( ~ spl0_50
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f96,f637,f387]) ).
fof(f642,definition,
( spl0_104
<=> c0_1(a1709) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f644,plain,
( ~ spl0_47
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f95,f642,f374]) ).
fof(f653,definition,
( spl0_107
<=> c3_1(a1634) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f654,plain,
( c3_1(a1634)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( spl0_107
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f93,f367,f653]) ).
fof(f657,definition,
( spl0_108
<=> c0_1(a1634) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f658,plain,
( c0_1(a1634)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f659,plain,
( spl0_108
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f92,f367,f657]) ).
fof(f661,definition,
( spl0_109
<=> c3_1(a1637) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f662,plain,
( c3_1(a1637)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f663,plain,
( spl0_109
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f91,f305,f661]) ).
fof(f665,definition,
( spl0_110
<=> c1_1(a1637) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f666,plain,
( c1_1(a1637)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f667,plain,
( spl0_110
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f90,f305,f665]) ).
fof(f669,definition,
( spl0_111
<=> c3_1(a1638) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f670,plain,
( c3_1(a1638)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f669]) ).
fof(f671,plain,
( spl0_111
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f89,f362,f669]) ).
fof(f673,definition,
( spl0_112
<=> c3_1(a1639) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f674,plain,
( c3_1(a1639)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f675,plain,
( spl0_112
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f88,f355,f673]) ).
fof(f677,definition,
( spl0_113
<=> c3_1(a1640) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f678,plain,
( c3_1(a1640)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f679,plain,
( spl0_113
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f87,f313,f677]) ).
fof(f681,definition,
( spl0_114
<=> c0_1(a1640) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f682,plain,
( c0_1(a1640)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f681]) ).
fof(f683,plain,
( spl0_114
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f86,f313,f681]) ).
fof(f685,definition,
( spl0_115
<=> c2_1(a1641) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f686,plain,
( c2_1(a1641)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f685]) ).
fof(f687,plain,
( spl0_115
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f85,f418,f685]) ).
fof(f697,definition,
( spl0_118
<=> c2_1(a1648) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f698,plain,
( c2_1(a1648)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f699,plain,
( spl0_118
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f82,f426,f697]) ).
fof(f701,definition,
( spl0_119
<=> c0_1(a1648) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f702,plain,
( c0_1(a1648)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f703,plain,
( spl0_119
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f81,f426,f701]) ).
fof(f705,definition,
( spl0_120
<=> c1_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f706,plain,
( c1_1(a1650)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f707,plain,
( spl0_120
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f80,f336,f705]) ).
fof(f709,definition,
( spl0_121
<=> c1_1(a1653) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f710,plain,
( c1_1(a1653)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f711,plain,
( spl0_121
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f79,f340,f709]) ).
fof(f713,definition,
( spl0_122
<=> c0_1(a1653) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f714,plain,
( c0_1(a1653)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f715,plain,
( spl0_122
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f78,f340,f713]) ).
fof(f717,definition,
( spl0_123
<=> c3_1(a1658) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f718,plain,
( c3_1(a1658)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f719,plain,
( spl0_123
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f77,f411,f717]) ).
fof(f725,definition,
( spl0_125
<=> c0_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f726,plain,
( c0_1(a1661)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f727,plain,
( spl0_125
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f75,f328,f725]) ).
fof(f729,definition,
( spl0_126
<=> c0_1(a1664) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f731,plain,
( spl0_126
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f74,f309,f729]) ).
fof(f733,definition,
( spl0_127
<=> c2_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f734,plain,
( c2_1(a1667)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( spl0_127
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f73,f429,f733]) ).
fof(f737,definition,
( spl0_128
<=> c0_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f738,plain,
( c0_1(a1667)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f739,plain,
( spl0_128
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f72,f429,f737]) ).
fof(f741,definition,
( spl0_129
<=> c2_1(a1675) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f743,plain,
( spl0_129
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f71,f295,f741]) ).
fof(f745,definition,
( spl0_130
<=> c1_1(a1680) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f746,plain,
( c1_1(a1680)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( spl0_130
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f70,f291,f745]) ).
fof(f749,definition,
( spl0_131
<=> c2_1(a1682) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f750,plain,
( c2_1(a1682)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f751,plain,
( spl0_131
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f69,f404,f749]) ).
fof(f753,definition,
( spl0_132
<=> c1_1(a1682) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f754,plain,
( c1_1(a1682)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f755,plain,
( spl0_132
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f68,f404,f753]) ).
fof(f757,definition,
( spl0_133
<=> c1_1(a1689) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f758,plain,
( c1_1(a1689)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( spl0_133
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f67,f383,f757]) ).
fof(f761,definition,
( spl0_134
<=> c0_1(a1689) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f762,plain,
( c0_1(a1689)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( spl0_134
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f66,f383,f761]) ).
fof(f765,definition,
( spl0_135
<=> c3_1(a1691) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f766,plain,
( c3_1(a1691)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f767,plain,
( spl0_135
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f65,f380,f765]) ).
fof(f773,definition,
( spl0_137
<=> c3_1(a1701) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f774,plain,
( c3_1(a1701)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f775,plain,
( spl0_137
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f63,f387,f773]) ).
fof(f777,definition,
( spl0_138
<=> c2_1(a1709) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f778,plain,
( c2_1(a1709)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f779,plain,
( spl0_138
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f62,f374,f777]) ).
fof(f781,definition,
( spl0_139
<=> c1_1(a1709) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f782,plain,
( c1_1(a1709)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f781]) ).
fof(f783,plain,
( spl0_139
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f61,f374,f781]) ).
fof(f793,definition,
( spl0_142
<=> c2_1(a1635) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f794,plain,
( c2_1(a1635)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f796,plain,
( spl0_142
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f58,f421,f793]) ).
fof(f798,definition,
( spl0_143
<=> c1_1(a1635) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f799,plain,
( c1_1(a1635)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f800,plain,
( spl0_143
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f57,f421,f798]) ).
fof(f802,definition,
( spl0_144
<=> c0_1(a1635) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f803,plain,
( c0_1(a1635)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f802]) ).
fof(f804,plain,
( spl0_144
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f56,f421,f802]) ).
fof(f806,definition,
( spl0_145
<=> c3_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f807,plain,
( c3_1(a1646)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,plain,
( spl0_145
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f55,f280,f806]) ).
fof(f811,definition,
( spl0_146
<=> c2_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f812,plain,
( c2_1(a1646)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f813,plain,
( spl0_146
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f54,f280,f811]) ).
fof(f815,definition,
( spl0_147
<=> c1_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f816,plain,
( c1_1(a1646)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f817,plain,
( spl0_147
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f53,f280,f815]) ).
fof(f819,definition,
( spl0_148
<=> c3_1(a1647) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f820,plain,
( c3_1(a1647)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f822,plain,
( spl0_148
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f52,f344,f819]) ).
fof(f824,definition,
( spl0_149
<=> c1_1(a1647) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f825,plain,
( c1_1(a1647)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f826,plain,
( spl0_149
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f51,f344,f824]) ).
fof(f828,definition,
( spl0_150
<=> c0_1(a1647) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f829,plain,
( c0_1(a1647)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f828]) ).
fof(f830,plain,
( spl0_150
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f50,f344,f828]) ).
fof(f832,definition,
( spl0_151
<=> c3_1(a1712) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f833,plain,
( c3_1(a1712)
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f832]) ).
fof(f835,definition,
( spl0_152
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f837,plain,
( spl0_151
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f49,f835,f832]) ).
fof(f839,definition,
( spl0_153
<=> c2_1(a1712) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f841,plain,
( spl0_153
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f48,f835,f839]) ).
fof(f843,definition,
( spl0_154
<=> c0_1(a1712) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f845,plain,
( spl0_154
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f47,f835,f843]) ).
fof(f848,plain,
( spl0_52
| spl0_27
| spl0_47 ),
inference(avatar_split_clause,[],[f44,f374,f295,f395]) ).
fof(f850,plain,
( spl0_52
| spl0_54
| spl0_31 ),
inference(avatar_split_clause,[],[f42,f309,f404,f395]) ).
fof(f854,plain,
( spl0_52
| spl0_32
| spl0_45 ),
inference(avatar_split_clause,[],[f39,f367,f313,f395]) ).
fof(f855,plain,
( spl0_38
| spl0_26
| spl0_58 ),
inference(avatar_split_clause,[],[f38,f426,f291,f336]) ).
fof(f857,plain,
( spl0_42
| spl0_56
| spl0_152 ),
inference(avatar_split_clause,[],[f37,f835,f418,f355]) ).
fof(f858,plain,
( spl0_50
| spl0_47
| spl0_39 ),
inference(avatar_split_clause,[],[f36,f340,f374,f387]) ).
fof(f859,plain,
( spl0_50
| spl0_32
| spl0_39 ),
inference(avatar_split_clause,[],[f35,f340,f313,f387]) ).
fof(f861,plain,
( spl0_152
| spl0_49
| spl0_57 ),
inference(avatar_split_clause,[],[f33,f421,f383,f835]) ).
fof(f883,plain,
( spl0_3
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f12,f383,f208]) ).
fof(f890,plain,
( spl0_3
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f5,f421,f208]) ).
fof(f893,plain,
( spl0_3
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f2,f835,f208]) ).
fof(f894,plain,
( spl0_36
| spl0_49 ),
inference(avatar_split_clause,[],[f1,f383,f328]) ).
fof(f895,plain,
( ~ c2_1(a1653)
| ~ c0_1(a1653)
| ~ spl0_2
| ~ spl0_121 ),
inference(resolution,[],[f206,f710]) ).
fof(f897,plain,
( ~ c2_1(a1653)
| ~ spl0_2
| ~ spl0_121
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f895,f714]) ).
fof(f902,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f226,f216]) ).
fof(f905,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_11 ),
inference(resolution,[],[f237,f216]) ).
fof(f908,plain,
( ~ c2_1(a1644)
| c0_1(a1644)
| ~ spl0_11
| spl0_77 ),
inference(resolution,[],[f237,f519]) ).
fof(f911,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f905]) ).
fof(f913,plain,
( ~ c2_1(a1644)
| ~ spl0_11
| spl0_77
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f908,f523]) ).
fof(f915,plain,
( c3_1(a1653)
| ~ c0_1(a1653)
| ~ spl0_12
| ~ spl0_121 ),
inference(resolution,[],[f240,f710]) ).
fof(f926,plain,
( spl0_20
| ~ spl0_5
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f911,f236,f215,f268]) ).
fof(f928,plain,
( ~ c0_1(a1648)
| ~ c2_1(a1648)
| ~ spl0_9
| spl0_79 ),
inference(resolution,[],[f230,f528]) ).
fof(f937,definition,
( spl0_155
<=> c2_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f938,plain,
( ~ c2_1(a1650)
| spl0_155 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f940,plain,
( c3_1(a1650)
| ~ c2_1(a1650)
| ~ spl0_7
| ~ spl0_120 ),
inference(resolution,[],[f706,f222]) ).
fof(f943,plain,
( ~ c2_1(a1650)
| ~ spl0_7
| spl0_80
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f940,f533]) ).
fof(f944,plain,
( ~ spl0_155
| ~ spl0_7
| spl0_80
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f943,f705,f532,f221,f937]) ).
fof(f946,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_5 ),
inference(resolution,[],[f203,f216]) ).
fof(f950,plain,
( c2_1(a1636)
| ~ c3_1(a1636)
| ~ spl0_1
| spl0_62 ),
inference(resolution,[],[f203,f451]) ).
fof(f951,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_1
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f946]) ).
fof(f952,plain,
( ~ c3_1(a1636)
| ~ spl0_1
| spl0_61
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f950,f447]) ).
fof(f954,plain,
( spl0_19
| ~ spl0_1
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f951,f215,f202,f265]) ).
fof(f955,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f244,f216]) ).
fof(f956,plain,
( ! [X0] :
( c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_5
| ~ spl0_13 ),
inference(resolution,[],[f955,f203]) ).
fof(f960,plain,
( c0_1(a1650)
| ~ spl0_5
| ~ spl0_13
| ~ spl0_120 ),
inference(resolution,[],[f955,f706]) ).
fof(f962,plain,
( $false
| ~ spl0_5
| ~ spl0_13
| spl0_81
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f960,f537]) ).
fof(f963,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_81
| ~ spl0_120 ),
inference(avatar_contradiction_clause,[],[f962]) ).
fof(f964,plain,
( spl0_19
| ~ spl0_1
| ~ spl0_5
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f956,f243,f215,f202,f265]) ).
fof(f965,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_7
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f333,f222]) ).
fof(f970,plain,
( ~ c2_1(a1641)
| ~ spl0_7
| ~ spl0_37
| spl0_70 ),
inference(resolution,[],[f965,f488]) ).
fof(f973,plain,
( $false
| ~ spl0_7
| ~ spl0_37
| spl0_70
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f970,f686]) ).
fof(f974,plain,
( ~ spl0_7
| ~ spl0_37
| spl0_70
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f973]) ).
fof(f981,definition,
( spl0_156
<=> c0_1(a1699) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f982,plain,
( ~ c0_1(a1699)
| spl0_156 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f986,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(resolution,[],[f219,f206]) ).
fof(f987,plain,
( ~ c0_1(a1634)
| ~ c3_1(a1634)
| ~ spl0_6
| spl0_60 ),
inference(resolution,[],[f219,f442]) ).
fof(f991,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f986]) ).
fof(f996,plain,
( ! [X2] :
( c1_1(X2)
| ~ c3_1(X2) )
| ~ spl0_6
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f226,f219]) ).
fof(f1001,definition,
( spl0_157
<=> c2_1(a1634) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1007,plain,
( ~ c0_1(a1667)
| ~ c3_1(a1667)
| ~ spl0_6
| spl0_88 ),
inference(resolution,[],[f570,f219]) ).
fof(f1012,definition,
( spl0_158
<=> c3_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1013,plain,
( ~ c3_1(a1667)
| spl0_158 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1033,plain,
( c3_1(a1650)
| c0_1(a1650)
| ~ spl0_13
| ~ spl0_120 ),
inference(resolution,[],[f244,f706]) ).
fof(f1035,plain,
( c0_1(a1650)
| ~ spl0_13
| spl0_80
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f1033,f533]) ).
fof(f1037,plain,
( $false
| ~ spl0_13
| spl0_80
| spl0_81
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f1035,f537]) ).
fof(f1038,plain,
( ~ spl0_13
| spl0_80
| spl0_81
| ~ spl0_120 ),
inference(avatar_contradiction_clause,[],[f1037]) ).
fof(f1046,plain,
( c2_1(a1699)
| ~ c0_1(a1699)
| ~ spl0_14
| spl0_101 ),
inference(resolution,[],[f247,f629]) ).
fof(f1050,plain,
( ~ c0_1(a1699)
| ~ spl0_14
| spl0_100
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f1046,f625]) ).
fof(f1051,plain,
( ~ spl0_156
| ~ spl0_14
| spl0_100
| spl0_101 ),
inference(avatar_split_clause,[],[f1050,f628,f624,f246,f981]) ).
fof(f1052,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_2
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f254,f206]) ).
fof(f1056,plain,
( ~ c2_1(a1646)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_147 ),
inference(resolution,[],[f1052,f816]) ).
fof(f1061,plain,
( $false
| ~ spl0_2
| ~ spl0_16
| ~ spl0_146
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f1056,f812]) ).
fof(f1062,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_146
| ~ spl0_147 ),
inference(avatar_contradiction_clause,[],[f1061]) ).
fof(f1068,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f254,f237]) ).
fof(f1069,plain,
( ~ c0_1(a1661)
| ~ c2_1(a1661)
| ~ spl0_9
| spl0_84 ),
inference(resolution,[],[f552,f230]) ).
fof(f1071,definition,
( spl0_159
<=> c2_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1072,plain,
( ~ c2_1(a1661)
| spl0_159 ),
inference(avatar_component_clause,[],[f1071]) ).
fof(f1075,plain,
( c2_1(a1661)
| ~ c0_1(a1661)
| ~ spl0_14
| spl0_85 ),
inference(resolution,[],[f556,f247]) ).
fof(f1088,definition,
( spl0_160
<=> c2_1(a1701) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1093,plain,
( c2_1(a1701)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1100,plain,
( c0_1(a1680)
| ~ spl0_5
| ~ spl0_13
| ~ spl0_130 ),
inference(resolution,[],[f955,f746]) ).
fof(f1103,plain,
( $false
| ~ spl0_5
| ~ spl0_13
| spl0_92
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1100,f588]) ).
fof(f1104,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_92
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f1103]) ).
fof(f1105,plain,
( ~ c0_1(a1667)
| ~ c2_1(a1667)
| ~ spl0_9
| spl0_158 ),
inference(resolution,[],[f1013,f230]) ).
fof(f1113,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f233,f230]) ).
fof(f1120,plain,
( ~ spl0_127
| ~ spl0_128
| ~ spl0_9
| spl0_158 ),
inference(avatar_split_clause,[],[f1105,f1012,f229,f737,f733]) ).
fof(f1156,plain,
( c0_1(a1646)
| ~ c3_1(a1646)
| ~ spl0_5
| ~ spl0_147 ),
inference(resolution,[],[f216,f816]) ).
fof(f1185,plain,
( c3_1(a1653)
| ~ spl0_12
| ~ spl0_121
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f915,f714]) ).
fof(f1188,definition,
( spl0_161
<=> c2_1(a1653) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1189,plain,
( ~ c2_1(a1653)
| spl0_161 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1193,plain,
( spl0_82
| ~ spl0_12
| ~ spl0_121
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1185,f713,f709,f239,f541]) ).
fof(f1210,plain,
( c0_1(a1646)
| ~ c2_1(a1646)
| ~ spl0_16
| ~ spl0_147 ),
inference(resolution,[],[f254,f816]) ).
fof(f1214,plain,
( c0_1(a1650)
| ~ c2_1(a1650)
| ~ spl0_16
| ~ spl0_120 ),
inference(resolution,[],[f254,f706]) ).
fof(f1215,plain,
( c0_1(a1646)
| ~ spl0_16
| ~ spl0_146
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f1210,f812]) ).
fof(f1216,plain,
( ! [X0] :
( c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_1
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f258,f203]) ).
fof(f1218,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(resolution,[],[f1216,f254]) ).
fof(f1222,plain,
( ~ c3_1(a1701)
| ~ spl0_1
| ~ spl0_17
| spl0_102 ),
inference(resolution,[],[f1216,f634]) ).
fof(f1231,plain,
( $false
| ~ spl0_1
| ~ spl0_17
| spl0_102
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f1222,f774]) ).
fof(f1232,plain,
( ~ spl0_1
| ~ spl0_17
| spl0_102
| ~ spl0_137 ),
inference(avatar_contradiction_clause,[],[f1231]) ).
fof(f1233,plain,
( spl0_20
| ~ spl0_1
| ~ spl0_16
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1218,f257,f253,f202,f268]) ).
fof(f1242,plain,
( c3_1(a1644)
| c0_1(a1644)
| ~ spl0_18
| spl0_77 ),
inference(resolution,[],[f262,f519]) ).
fof(f1243,plain,
( c3_1(a1636)
| c0_1(a1636)
| ~ spl0_18
| spl0_62 ),
inference(resolution,[],[f262,f451]) ).
fof(f1248,plain,
( c0_1(a1636)
| ~ spl0_1
| ~ spl0_18
| spl0_61
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f1243,f952]) ).
fof(f1249,plain,
( c0_1(a1644)
| ~ spl0_18
| spl0_76
| spl0_77 ),
inference(forward_subsumption_resolution,[],[f1242,f515]) ).
fof(f1254,plain,
( $false
| ~ spl0_1
| ~ spl0_18
| spl0_61
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f1248,f455]) ).
fof(f1255,plain,
( ~ spl0_1
| ~ spl0_18
| spl0_61
| spl0_62
| spl0_63 ),
inference(avatar_contradiction_clause,[],[f1254]) ).
fof(f1256,plain,
( $false
| ~ spl0_18
| spl0_76
| spl0_77
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f1249,f523]) ).
fof(f1257,plain,
( ~ spl0_18
| spl0_76
| spl0_77
| spl0_78 ),
inference(avatar_contradiction_clause,[],[f1256]) ).
fof(f1262,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_14
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f359,f247]) ).
fof(f1266,plain,
( ~ c0_1(a1661)
| ~ spl0_14
| ~ spl0_43
| spl0_159 ),
inference(resolution,[],[f1262,f1072]) ).
fof(f1274,plain,
( $false
| ~ spl0_14
| ~ spl0_43
| ~ spl0_125
| spl0_159 ),
inference(forward_subsumption_resolution,[],[f1266,f726]) ).
fof(f1275,plain,
( ~ spl0_14
| ~ spl0_43
| ~ spl0_125
| spl0_159 ),
inference(avatar_contradiction_clause,[],[f1274]) ).
fof(f1278,plain,
( c2_1(a1639)
| ~ c3_1(a1639)
| ~ spl0_1
| spl0_68 ),
inference(resolution,[],[f478,f203]) ).
fof(f1279,plain,
( c2_1(a1639)
| ~ c0_1(a1639)
| ~ spl0_14
| spl0_68 ),
inference(resolution,[],[f478,f247]) ).
fof(f1283,definition,
( spl0_162
<=> c0_1(a1639) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1284,plain,
( ~ c0_1(a1639)
| spl0_162 ),
inference(avatar_component_clause,[],[f1283]) ).
fof(f1309,definition,
( spl0_164
<=> c3_1(a1636) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1310,plain,
( ~ c3_1(a1636)
| spl0_164 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1319,plain,
( ~ c0_1(a1682)
| ~ c2_1(a1682)
| ~ spl0_9
| spl0_93 ),
inference(resolution,[],[f593,f230]) ).
fof(f1322,definition,
( spl0_165
<=> c0_1(a1682) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1324,plain,
( ~ spl0_131
| ~ spl0_165
| ~ spl0_9
| spl0_93 ),
inference(avatar_split_clause,[],[f1319,f592,f229,f1322,f749]) ).
fof(f1328,plain,
( c0_1(a1637)
| ~ c3_1(a1637)
| ~ spl0_5
| ~ spl0_110 ),
inference(resolution,[],[f666,f216]) ).
fof(f1336,plain,
( ~ spl0_118
| ~ spl0_119
| ~ spl0_9
| spl0_79 ),
inference(avatar_split_clause,[],[f928,f527,f229,f701,f697]) ).
fof(f1337,plain,
( c0_1(a1637)
| ~ spl0_5
| ~ spl0_109
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f1328,f662]) ).
fof(f1343,plain,
( spl0_64
| ~ spl0_5
| ~ spl0_109
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1337,f665,f661,f215,f459]) ).
fof(f1344,plain,
( c0_1(a1682)
| ~ c2_1(a1682)
| ~ spl0_16
| ~ spl0_132 ),
inference(resolution,[],[f754,f254]) ).
fof(f1346,plain,
( c3_1(a1682)
| ~ c2_1(a1682)
| ~ spl0_7
| ~ spl0_132 ),
inference(resolution,[],[f754,f222]) ).
fof(f1348,plain,
( ~ c2_1(a1682)
| ~ spl0_7
| spl0_93
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f1346,f593]) ).
fof(f1350,plain,
( c0_1(a1682)
| ~ spl0_16
| ~ spl0_131
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f1344,f750]) ).
fof(f1351,plain,
( $false
| ~ spl0_7
| spl0_93
| ~ spl0_131
| ~ spl0_132 ),
inference(forward_subsumption_resolution,[],[f1348,f750]) ).
fof(f1352,plain,
( ~ spl0_7
| spl0_93
| ~ spl0_131
| ~ spl0_132 ),
inference(avatar_contradiction_clause,[],[f1351]) ).
fof(f1355,plain,
( c2_1(a1664)
| ~ c0_1(a1664)
| ~ spl0_14
| spl0_87 ),
inference(resolution,[],[f565,f247]) ).
fof(f1362,plain,
( ~ c0_1(a1664)
| ~ spl0_14
| spl0_86
| spl0_87 ),
inference(forward_subsumption_resolution,[],[f1355,f561]) ).
fof(f1364,plain,
( ~ spl0_126
| ~ spl0_14
| spl0_86
| spl0_87 ),
inference(avatar_split_clause,[],[f1362,f564,f560,f246,f729]) ).
fof(f1366,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_4
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f212,f216]) ).
fof(f1368,plain,
( c3_1(a1667)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f1012]) ).
fof(f1380,plain,
( c0_1(a1709)
| ~ c2_1(a1709)
| ~ spl0_16
| ~ spl0_139 ),
inference(resolution,[],[f782,f254]) ).
fof(f1382,plain,
( c3_1(a1709)
| ~ c2_1(a1709)
| ~ spl0_7
| ~ spl0_139 ),
inference(resolution,[],[f782,f222]) ).
fof(f1385,plain,
( c3_1(a1709)
| ~ spl0_7
| ~ spl0_138
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f1382,f778]) ).
fof(f1395,definition,
( spl0_169
<=> c3_1(a1709) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1426,plain,
( ~ c3_1(a1637)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_110 ),
inference(resolution,[],[f1366,f666]) ).
fof(f1427,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_109
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f1426,f662]) ).
fof(f1428,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_109
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f1427]) ).
fof(f1439,plain,
( ~ spl0_161
| ~ spl0_2
| ~ spl0_121
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f897,f713,f709,f205,f1188]) ).
fof(f1449,definition,
( spl0_170
<=> c0_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1451,plain,
( ~ spl0_145
| spl0_170
| ~ spl0_5
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1156,f815,f215,f1449,f806]) ).
fof(f1515,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f251,f902]) ).
fof(f1557,plain,
( spl0_165
| ~ spl0_16
| ~ spl0_131
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1350,f753,f749,f253,f1322]) ).
fof(f1558,plain,
( ~ spl0_138
| spl0_104
| ~ spl0_16
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1380,f781,f253,f642,f777]) ).
fof(f1564,plain,
( ~ c2_1(a1675)
| c0_1(a1675)
| ~ spl0_11
| spl0_89 ),
inference(resolution,[],[f575,f237]) ).
fof(f1569,plain,
( spl0_90
| ~ spl0_129
| ~ spl0_11
| spl0_89 ),
inference(avatar_split_clause,[],[f1564,f574,f236,f741,f578]) ).
fof(f1570,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f233,f902]) ).
fof(f1585,plain,
( c0_1(a1709)
| ~ spl0_5
| ~ spl0_13
| ~ spl0_139 ),
inference(resolution,[],[f955,f782]) ).
fof(f1594,plain,
( spl0_104
| ~ spl0_5
| ~ spl0_13
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1585,f781,f243,f215,f642]) ).
fof(f1597,plain,
( ~ c2_1(a1682)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_132 ),
inference(resolution,[],[f1052,f754]) ).
fof(f1603,plain,
( ~ spl0_131
| ~ spl0_2
| ~ spl0_16
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1597,f753,f253,f205,f749]) ).
fof(f1642,plain,
( spl0_169
| ~ spl0_7
| ~ spl0_138
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1385,f781,f777,f221,f1395]) ).
fof(f1662,plain,
( c0_1(a1709)
| ~ c3_1(a1709)
| ~ spl0_5
| ~ spl0_139 ),
inference(resolution,[],[f782,f216]) ).
fof(f1698,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f222,f1570]) ).
fof(f1700,plain,
( ~ c2_1(a1709)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_10
| ~ spl0_139 ),
inference(resolution,[],[f1698,f782]) ).
fof(f1707,plain,
( ~ spl0_138
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_10
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1700,f781,f232,f225,f221,f215,f777]) ).
fof(f1730,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_8
| ~ spl0_15
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f302,f1515]) ).
fof(f1731,plain,
( ! [X0] : ~ c3_1(X0)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1730,f1570]) ).
fof(f1734,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29
| ~ spl0_123 ),
inference(resolution,[],[f1731,f718]) ).
fof(f1738,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29
| ~ spl0_107 ),
inference(resolution,[],[f1731,f654]) ).
fof(f1741,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f1738]) ).
fof(f1745,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f1734]) ).
fof(f1749,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_13
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f285,f955]) ).
fof(f1750,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_8
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f302,f902]) ).
fof(f1751,plain,
( ! [X0] : ~ c3_1(X0)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f1750,f1570]) ).
fof(f1754,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_123 ),
inference(resolution,[],[f1751,f718]) ).
fof(f1755,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_113 ),
inference(resolution,[],[f1751,f678]) ).
fof(f1758,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_107 ),
inference(resolution,[],[f1751,f654]) ).
fof(f1759,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f1758]) ).
fof(f1762,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_113 ),
inference(avatar_contradiction_clause,[],[f1755]) ).
fof(f1763,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f1754]) ).
fof(f1780,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f299,f206]) ).
fof(f1789,plain,
( ~ c2_1(a1709)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_139 ),
inference(resolution,[],[f1052,f782]) ).
fof(f1798,plain,
( c0_1(a1701)
| ~ spl0_11
| ~ spl0_16
| ~ spl0_160 ),
inference(resolution,[],[f1068,f1093]) ).
fof(f1806,plain,
( $false
| ~ spl0_11
| ~ spl0_16
| spl0_103
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f1798,f638]) ).
fof(f1807,plain,
( ~ spl0_11
| ~ spl0_16
| spl0_103
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f1806]) ).
fof(f1826,plain,
( c0_1(a1638)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_111 ),
inference(resolution,[],[f670,f902]) ).
fof(f1827,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| spl0_66
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f1826,f469]) ).
fof(f1828,plain,
( ~ spl0_5
| ~ spl0_8
| spl0_66
| ~ spl0_111 ),
inference(avatar_contradiction_clause,[],[f1827]) ).
fof(f1856,plain,
( ~ c0_1(a1653)
| ~ spl0_14
| ~ spl0_43
| spl0_161 ),
inference(resolution,[],[f1262,f1189]) ).
fof(f1859,plain,
( ~ c0_1(a1640)
| ~ spl0_14
| ~ spl0_43
| spl0_69 ),
inference(resolution,[],[f1262,f483]) ).
fof(f1868,plain,
( $false
| ~ spl0_14
| ~ spl0_43
| spl0_69
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f1859,f682]) ).
fof(f1869,plain,
( ~ spl0_14
| ~ spl0_43
| spl0_69
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f1868]) ).
fof(f1870,plain,
( $false
| ~ spl0_14
| ~ spl0_43
| ~ spl0_122
| spl0_161 ),
inference(forward_subsumption_resolution,[],[f1856,f714]) ).
fof(f1871,plain,
( ~ spl0_14
| ~ spl0_43
| ~ spl0_122
| spl0_161 ),
inference(avatar_contradiction_clause,[],[f1870]) ).
fof(f1879,plain,
( ~ c3_1(a1634)
| ~ spl0_6
| spl0_60
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f987,f658]) ).
fof(f1889,plain,
( ~ spl0_112
| spl0_67
| ~ spl0_1
| spl0_68 ),
inference(avatar_split_clause,[],[f1278,f477,f202,f473,f673]) ).
fof(f1894,plain,
( ~ spl0_107
| ~ spl0_6
| spl0_60
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1879,f657,f441,f218,f653]) ).
fof(f1908,plain,
( ~ c3_1(a1691)
| ~ spl0_6
| ~ spl0_8
| spl0_95 ),
inference(resolution,[],[f996,f603]) ).
fof(f1912,plain,
( ~ c3_1(a1639)
| ~ spl0_6
| ~ spl0_8
| spl0_68 ),
inference(resolution,[],[f996,f478]) ).
fof(f1919,plain,
( ~ spl0_112
| ~ spl0_6
| ~ spl0_8
| spl0_68 ),
inference(avatar_split_clause,[],[f1912,f477,f225,f218,f673]) ).
fof(f1923,plain,
( ~ c2_1(a1646)
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_145 ),
inference(resolution,[],[f1570,f807]) ).
fof(f1928,plain,
( $false
| ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_145
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f1923,f812]) ).
fof(f1929,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_145
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f1928]) ).
fof(f1954,plain,
( c0_1(a1636)
| ~ spl0_5
| ~ spl0_13
| ~ spl0_24
| spl0_61 ),
inference(resolution,[],[f1749,f447]) ).
fof(f1955,plain,
( $false
| ~ spl0_5
| ~ spl0_13
| ~ spl0_24
| spl0_61
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f1954,f455]) ).
fof(f1956,plain,
( ~ spl0_5
| ~ spl0_13
| ~ spl0_24
| spl0_61
| spl0_63 ),
inference(avatar_contradiction_clause,[],[f1955]) ).
fof(f1972,plain,
( ~ spl0_162
| spl0_67
| ~ spl0_14
| spl0_68 ),
inference(avatar_split_clause,[],[f1279,f477,f246,f473,f1283]) ).
fof(f2028,plain,
( c3_1(a1636)
| ~ spl0_18
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f1243,f455]) ).
fof(f2038,plain,
( spl0_164
| ~ spl0_18
| spl0_62
| spl0_63 ),
inference(avatar_split_clause,[],[f2028,f454,f450,f261,f1309]) ).
fof(f2054,plain,
( ~ c0_1(a1667)
| ~ spl0_2
| ~ spl0_28
| ~ spl0_127 ),
inference(resolution,[],[f1780,f734]) ).
fof(f2056,plain,
( ~ c0_1(a1648)
| ~ spl0_2
| ~ spl0_28
| ~ spl0_118 ),
inference(resolution,[],[f1780,f698]) ).
fof(f2057,plain,
( $false
| ~ spl0_2
| ~ spl0_28
| ~ spl0_118
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2056,f702]) ).
fof(f2058,plain,
( ~ spl0_2
| ~ spl0_28
| ~ spl0_118
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f2057]) ).
fof(f2061,plain,
( $false
| ~ spl0_2
| ~ spl0_28
| ~ spl0_127
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f2054,f738]) ).
fof(f2062,plain,
( ~ spl0_2
| ~ spl0_28
| ~ spl0_127
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f2061]) ).
fof(f2071,plain,
( ~ c0_1(a1646)
| ~ c2_1(a1646)
| ~ spl0_10
| ~ spl0_145 ),
inference(resolution,[],[f233,f807]) ).
fof(f2078,plain,
( ~ c0_1(a1634)
| ~ c2_1(a1634)
| ~ spl0_10
| ~ spl0_107 ),
inference(resolution,[],[f233,f654]) ).
fof(f2144,plain,
( ~ c2_1(a1650)
| ~ spl0_16
| spl0_81
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f1214,f537]) ).
fof(f2147,plain,
( ~ spl0_155
| ~ spl0_16
| spl0_81
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f2144,f705,f536,f253,f937]) ).
fof(f2178,plain,
( c2_1(a1634)
| ~ c0_1(a1634)
| ~ spl0_14
| spl0_60 ),
inference(resolution,[],[f247,f442]) ).
fof(f2185,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f258,f1052]) ).
fof(f2190,plain,
( ~ c2_1(a1701)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_137 ),
inference(resolution,[],[f2185,f774]) ).
fof(f2211,plain,
( ~ c2_1(a1661)
| ~ spl0_9
| spl0_84
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f1069,f726]) ).
fof(f2214,plain,
( ~ spl0_159
| ~ spl0_9
| spl0_84
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f2211,f725,f551,f229,f1071]) ).
fof(f2266,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_2
| ~ spl0_16
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f288,f1052]) ).
fof(f2267,plain,
( ~ c2_1(a1667)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_158 ),
inference(resolution,[],[f1368,f2185]) ).
fof(f2268,plain,
( $false
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_127
| ~ spl0_158 ),
inference(forward_subsumption_resolution,[],[f2267,f734]) ).
fof(f2269,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_127
| ~ spl0_158 ),
inference(avatar_contradiction_clause,[],[f2268]) ).
fof(f2293,plain,
( c2_1(a1701)
| c0_1(a1701)
| ~ spl0_24
| spl0_102 ),
inference(resolution,[],[f285,f634]) ).
fof(f2300,plain,
( c2_1(a1699)
| c0_1(a1699)
| ~ spl0_24
| spl0_101 ),
inference(resolution,[],[f285,f629]) ).
fof(f2301,plain,
( c2_1(a1636)
| c0_1(a1636)
| ~ spl0_24
| spl0_62 ),
inference(resolution,[],[f285,f451]) ).
fof(f2303,plain,
( c0_1(a1636)
| ~ spl0_24
| spl0_61
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f2301,f447]) ).
fof(f2304,plain,
( c0_1(a1699)
| ~ spl0_24
| spl0_100
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f2300,f625]) ).
fof(f2308,plain,
( $false
| ~ spl0_24
| spl0_61
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f2303,f455]) ).
fof(f2309,plain,
( ~ spl0_24
| spl0_61
| spl0_62
| spl0_63 ),
inference(avatar_contradiction_clause,[],[f2308]) ).
fof(f2310,plain,
( $false
| ~ spl0_24
| spl0_100
| spl0_101
| spl0_156 ),
inference(forward_subsumption_resolution,[],[f2304,f982]) ).
fof(f2311,plain,
( ~ spl0_24
| spl0_100
| spl0_101
| spl0_156 ),
inference(avatar_contradiction_clause,[],[f2310]) ).
fof(f2320,plain,
( ~ spl0_169
| spl0_104
| ~ spl0_5
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1662,f781,f215,f642,f1395]) ).
fof(f2340,plain,
( c0_1(a1650)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_25
| ~ spl0_120 ),
inference(resolution,[],[f2266,f706]) ).
fof(f2344,plain,
( spl0_81
| ~ spl0_2
| ~ spl0_16
| ~ spl0_25
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f2340,f705,f287,f253,f205,f536]) ).
fof(f2346,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f302,f2185]) ).
fof(f2347,plain,
( ~ c0_1(a1647)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_148 ),
inference(resolution,[],[f2346,f820]) ).
fof(f2357,plain,
( ~ c0_1(a1634)
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_107 ),
inference(resolution,[],[f2346,f654]) ).
fof(f2360,plain,
( $false
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_107
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f2357,f658]) ).
fof(f2361,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_107
| ~ spl0_108 ),
inference(avatar_contradiction_clause,[],[f2360]) ).
fof(f2372,plain,
( $false
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_148
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f2347,f829]) ).
fof(f2373,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_148
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f2372]) ).
fof(f2385,plain,
( c2_1(a1661)
| ~ spl0_14
| spl0_85
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f1075,f726]) ).
fof(f2389,plain,
( ~ spl0_108
| spl0_157
| ~ spl0_14
| spl0_60 ),
inference(avatar_split_clause,[],[f2178,f441,f246,f1001,f657]) ).
fof(f2391,plain,
( ~ c0_1(a1646)
| ~ spl0_10
| ~ spl0_145
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f2071,f812]) ).
fof(f2394,plain,
( spl0_170
| ~ spl0_16
| ~ spl0_146
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1215,f815,f811,f253,f1449]) ).
fof(f2396,plain,
( ~ spl0_157
| ~ spl0_108
| ~ spl0_10
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f2078,f653,f232,f657,f1001]) ).
fof(f2398,plain,
( spl0_159
| ~ spl0_14
| spl0_85
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f2385,f725,f555,f246,f1071]) ).
fof(f2399,plain,
( ~ spl0_170
| ~ spl0_10
| ~ spl0_145
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f2391,f811,f806,f232,f1449]) ).
fof(f2401,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f212,f240]) ).
fof(f2426,plain,
( ~ c0_1(a1647)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_149 ),
inference(resolution,[],[f2401,f825]) ).
fof(f2428,plain,
( ~ c0_1(a1635)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_143 ),
inference(resolution,[],[f2401,f799]) ).
fof(f2430,plain,
( ~ c0_1(a1689)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_133 ),
inference(resolution,[],[f2401,f758]) ).
fof(f2432,plain,
( ~ c0_1(a1653)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_121 ),
inference(resolution,[],[f2401,f710]) ).
fof(f2435,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_121
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f2432,f714]) ).
fof(f2436,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_121
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f2435]) ).
fof(f2437,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_133
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2430,f762]) ).
fof(f2438,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_133
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2437]) ).
fof(f2439,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_143
| ~ spl0_144 ),
inference(forward_subsumption_resolution,[],[f2428,f803]) ).
fof(f2440,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_143
| ~ spl0_144 ),
inference(avatar_contradiction_clause,[],[f2439]) ).
fof(f2442,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f2426,f829]) ).
fof(f2443,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_149
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f2442]) ).
fof(f2461,plain,
( ~ c3_1(a1647)
| ~ c0_1(a1647)
| ~ spl0_4
| ~ spl0_149 ),
inference(resolution,[],[f212,f825]) ).
fof(f2462,plain,
( ~ c3_1(a1646)
| ~ c0_1(a1646)
| ~ spl0_4
| ~ spl0_147 ),
inference(resolution,[],[f212,f816]) ).
fof(f2474,plain,
( ~ c0_1(a1646)
| ~ spl0_4
| ~ spl0_145
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f2462,f807]) ).
fof(f2475,plain,
( ~ c0_1(a1647)
| ~ spl0_4
| ~ spl0_148
| ~ spl0_149 ),
inference(forward_subsumption_resolution,[],[f2461,f820]) ).
fof(f2479,plain,
( ~ spl0_170
| ~ spl0_4
| ~ spl0_145
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f2474,f815,f806,f211,f1449]) ).
fof(f2480,plain,
( $false
| ~ spl0_4
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f2475,f829]) ).
fof(f2481,plain,
( ~ spl0_4
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f2480]) ).
fof(f2492,plain,
( ~ c3_1(a1667)
| ~ spl0_6
| spl0_88
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f1007,f738]) ).
fof(f2495,plain,
( $false
| ~ spl0_6
| ~ spl0_8
| spl0_95
| ~ spl0_135 ),
inference(forward_subsumption_resolution,[],[f1908,f766]) ).
fof(f2496,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_95
| ~ spl0_135 ),
inference(avatar_contradiction_clause,[],[f2495]) ).
fof(f2497,plain,
( ~ spl0_158
| ~ spl0_6
| spl0_88
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f2492,f737,f569,f218,f1012]) ).
fof(f2512,plain,
( ~ c0_1(a1689)
| ~ spl0_14
| ~ spl0_43
| spl0_94 ),
inference(resolution,[],[f1262,f598]) ).
fof(f2522,plain,
( ~ spl0_134
| ~ spl0_14
| ~ spl0_43
| spl0_94 ),
inference(avatar_split_clause,[],[f2512,f597,f358,f246,f761]) ).
fof(f2544,plain,
( c3_1(a1653)
| ~ c2_1(a1653)
| ~ spl0_7
| ~ spl0_121 ),
inference(resolution,[],[f222,f710]) ).
fof(f2547,plain,
( ~ spl0_161
| spl0_82
| ~ spl0_7
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f2544,f709,f221,f541,f1188]) ).
fof(f2550,plain,
( ~ c3_1(a1701)
| c0_1(a1701)
| ~ spl0_8
| spl0_102 ),
inference(resolution,[],[f226,f634]) ).
fof(f2558,plain,
( ~ c3_1(a1636)
| c0_1(a1636)
| ~ spl0_8
| spl0_62 ),
inference(resolution,[],[f226,f451]) ).
fof(f2559,plain,
( ~ c3_1(a1636)
| ~ spl0_8
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f2558,f455]) ).
fof(f2561,plain,
( c0_1(a1701)
| ~ spl0_8
| spl0_102
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f2550,f774]) ).
fof(f2562,plain,
( ~ spl0_164
| ~ spl0_8
| spl0_62
| spl0_63 ),
inference(avatar_split_clause,[],[f2559,f454,f450,f225,f1309]) ).
fof(f2569,plain,
( spl0_103
| ~ spl0_8
| spl0_102
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f2561,f773,f633,f225,f637]) ).
fof(f2570,plain,
( ~ c3_1(a1639)
| c0_1(a1639)
| ~ spl0_8
| spl0_68 ),
inference(resolution,[],[f478,f226]) ).
fof(f2571,plain,
( c0_1(a1639)
| ~ spl0_8
| spl0_68
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f2570,f674]) ).
fof(f2572,plain,
( $false
| ~ spl0_8
| spl0_68
| ~ spl0_112
| spl0_162 ),
inference(forward_subsumption_resolution,[],[f2571,f1284]) ).
fof(f2573,plain,
( ~ spl0_8
| spl0_68
| ~ spl0_112
| spl0_162 ),
inference(avatar_contradiction_clause,[],[f2572]) ).
fof(f2576,plain,
( spl0_10
| ~ spl0_2
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f991,f218,f205,f232]) ).
fof(f2597,plain,
( ~ c2_1(a1635)
| ~ c0_1(a1635)
| ~ spl0_2
| ~ spl0_143 ),
inference(resolution,[],[f206,f799]) ).
fof(f2604,plain,
( ~ c0_1(a1635)
| ~ spl0_2
| ~ spl0_142
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f2597,f794]) ).
fof(f2615,plain,
( ~ spl0_144
| ~ spl0_2
| ~ spl0_142
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f2604,f798,f793,f205,f802]) ).
fof(f2616,plain,
( ~ c0_1(a1712)
| ~ c2_1(a1712)
| ~ spl0_10
| ~ spl0_151 ),
inference(resolution,[],[f233,f833]) ).
fof(f2663,plain,
( c0_1(a1650)
| c2_1(a1650)
| ~ spl0_15
| spl0_80 ),
inference(resolution,[],[f251,f533]) ).
fof(f2667,plain,
( c0_1(a1697)
| c2_1(a1697)
| ~ spl0_15
| spl0_96 ),
inference(resolution,[],[f251,f608]) ).
fof(f2668,plain,
( c0_1(a1644)
| c2_1(a1644)
| ~ spl0_15
| spl0_76 ),
inference(resolution,[],[f251,f515]) ).
fof(f2669,plain,
( c0_1(a1636)
| c2_1(a1636)
| ~ spl0_15
| spl0_164 ),
inference(resolution,[],[f251,f1310]) ).
fof(f2670,plain,
( c2_1(a1636)
| ~ spl0_15
| spl0_63
| spl0_164 ),
inference(forward_subsumption_resolution,[],[f2669,f455]) ).
fof(f2671,plain,
( c2_1(a1644)
| ~ spl0_15
| spl0_76
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f2668,f523]) ).
fof(f2672,plain,
( c2_1(a1697)
| ~ spl0_15
| spl0_96
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f2667,f616]) ).
fof(f2675,plain,
( c2_1(a1650)
| ~ spl0_15
| spl0_80
| spl0_81 ),
inference(forward_subsumption_resolution,[],[f2663,f537]) ).
fof(f2676,plain,
( $false
| ~ spl0_15
| spl0_61
| spl0_63
| spl0_164 ),
inference(forward_subsumption_resolution,[],[f2670,f447]) ).
fof(f2677,plain,
( ~ spl0_15
| spl0_61
| spl0_63
| spl0_164 ),
inference(avatar_contradiction_clause,[],[f2676]) ).
fof(f2678,plain,
( $false
| ~ spl0_11
| ~ spl0_15
| spl0_76
| spl0_77
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f2671,f913]) ).
fof(f2679,plain,
( ~ spl0_11
| ~ spl0_15
| spl0_76
| spl0_77
| spl0_78 ),
inference(avatar_contradiction_clause,[],[f2678]) ).
fof(f2680,plain,
( $false
| ~ spl0_15
| spl0_96
| spl0_97
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f2672,f612]) ).
fof(f2681,plain,
( ~ spl0_15
| spl0_96
| spl0_97
| spl0_98 ),
inference(avatar_contradiction_clause,[],[f2680]) ).
fof(f2684,plain,
( $false
| ~ spl0_15
| spl0_80
| spl0_81
| spl0_155 ),
inference(forward_subsumption_resolution,[],[f2675,f938]) ).
fof(f2685,plain,
( ~ spl0_15
| spl0_80
| spl0_81
| spl0_155 ),
inference(avatar_contradiction_clause,[],[f2684]) ).
fof(f2702,plain,
( ~ c0_1(a1667)
| ~ spl0_9
| ~ spl0_10
| ~ spl0_127 ),
inference(resolution,[],[f1113,f734]) ).
fof(f2705,plain,
( $false
| ~ spl0_9
| ~ spl0_10
| ~ spl0_127
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f2702,f738]) ).
fof(f2706,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_127
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f2705]) ).
fof(f2742,plain,
( c2_1(a1639)
| c0_1(a1639)
| ~ spl0_19
| ~ spl0_112 ),
inference(resolution,[],[f266,f674]) ).
fof(f2753,plain,
( c2_1(a1639)
| ~ spl0_19
| ~ spl0_112
| spl0_162 ),
inference(forward_subsumption_resolution,[],[f2742,f1284]) ).
fof(f2755,plain,
( spl0_67
| ~ spl0_19
| ~ spl0_112
| spl0_162 ),
inference(avatar_split_clause,[],[f2753,f1283,f673,f265,f473]) ).
fof(f2759,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_19
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f269,f266]) ).
fof(f2772,plain,
( c0_1(a1638)
| ~ spl0_19
| ~ spl0_20
| ~ spl0_111 ),
inference(resolution,[],[f2759,f670]) ).
fof(f2773,plain,
( c0_1(a1637)
| ~ spl0_19
| ~ spl0_20
| ~ spl0_109 ),
inference(resolution,[],[f2759,f662]) ).
fof(f2774,plain,
( $false
| ~ spl0_19
| ~ spl0_20
| spl0_64
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f2773,f460]) ).
fof(f2775,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_64
| ~ spl0_109 ),
inference(avatar_contradiction_clause,[],[f2774]) ).
fof(f2776,plain,
( $false
| ~ spl0_19
| ~ spl0_20
| spl0_66
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f2772,f469]) ).
fof(f2777,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_66
| ~ spl0_111 ),
inference(avatar_contradiction_clause,[],[f2776]) ).
fof(f2795,plain,
( c2_1(a1650)
| c0_1(a1650)
| ~ spl0_25
| ~ spl0_120 ),
inference(resolution,[],[f288,f706]) ).
fof(f2802,plain,
( c0_1(a1650)
| ~ spl0_25
| ~ spl0_120
| spl0_155 ),
inference(forward_subsumption_resolution,[],[f2795,f938]) ).
fof(f2805,plain,
( $false
| ~ spl0_25
| spl0_81
| ~ spl0_120
| spl0_155 ),
inference(forward_subsumption_resolution,[],[f2802,f537]) ).
fof(f2806,plain,
( ~ spl0_25
| spl0_81
| ~ spl0_120
| spl0_155 ),
inference(avatar_contradiction_clause,[],[f2805]) ).
fof(f2814,plain,
( ~ spl0_153
| ~ spl0_154
| ~ spl0_10
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f2616,f832,f232,f843,f839]) ).
fof(f2821,plain,
( ~ spl0_138
| ~ spl0_2
| ~ spl0_16
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1789,f781,f253,f205,f777]) ).
fof(f2823,plain,
( ~ spl0_160
| ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f2190,f773,f257,f253,f205,f1088]) ).
fof(f2827,plain,
( spl0_103
| spl0_160
| ~ spl0_24
| spl0_102 ),
inference(avatar_split_clause,[],[f2293,f633,f284,f1088,f637]) ).
fof(f2829,plain,
( c2_1(a1636)
| ~ spl0_24
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f2301,f455]) ).
fof(f2830,plain,
( spl0_61
| ~ spl0_24
| spl0_62
| spl0_63 ),
inference(avatar_split_clause,[],[f2829,f454,f450,f284,f446]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f213]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f223]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f234]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f241]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f248]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_9
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f255]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_11
| spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f259]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_6
| spl0_7
| spl0_18 ),
inference(sat_conversion,[],[f263]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_4
| spl0_7
| spl0_21 ),
inference(sat_conversion,[],[f274]) ).
cnf(s13,plain,
( spl0_2
| ~ spl0_3
| spl0_12
| spl0_23 ),
inference(sat_conversion,[],[f282]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_15
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f289]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_28
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f307]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_12
| spl0_20
| spl0_31 ),
inference(sat_conversion,[],[f311]) ).
cnf(s22,plain,
( spl0_1
| ~ spl0_3
| spl0_17
| spl0_36 ),
inference(sat_conversion,[],[f330]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_5
| spl0_14
| spl0_38 ),
inference(sat_conversion,[],[f338]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_17
| spl0_19
| spl0_39 ),
inference(sat_conversion,[],[f342]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_19
| spl0_28
| spl0_40 ),
inference(sat_conversion,[],[f346]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_8
| spl0_16 ),
inference(sat_conversion,[],[f353]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_18
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f360]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_14
| spl0_15
| spl0_40 ),
inference(sat_conversion,[],[f365]) ).
cnf(s38,plain,
( spl0_2
| ~ spl0_3
| spl0_48
| spl0_49 ),
inference(sat_conversion,[],[f385]) ).
cnf(s39,plain,
( spl0_2
| ~ spl0_3
| spl0_40
| spl0_50 ),
inference(sat_conversion,[],[f389]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_7
| spl0_42
| spl0_51 ),
inference(sat_conversion,[],[f393]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_17
| spl0_23
| spl0_54 ),
inference(sat_conversion,[],[f406]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_6
| spl0_22
| spl0_40 ),
inference(sat_conversion,[],[f407]) ).
cnf(s46,plain,
( ~ spl0_3
| spl0_6
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f408]) ).
cnf(s47,plain,
( ~ spl0_3
| spl0_20
| spl0_23
| spl0_45 ),
inference(sat_conversion,[],[f409]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_16
| spl0_38
| spl0_55 ),
inference(sat_conversion,[],[f413]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_16
| spl0_32
| spl0_40 ),
inference(sat_conversion,[],[f414]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_22
| spl0_30
| spl0_37 ),
inference(sat_conversion,[],[f424]) ).
cnf(s54,plain,
( spl0_1
| ~ spl0_3
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f431]) ).
cnf(s55,plain,
( ~ spl0_3
| spl0_14
| spl0_45
| spl0_59 ),
inference(sat_conversion,[],[f432]) ).
cnf(s56,plain,
( ~ spl0_3
| spl0_8
| spl0_23
| spl0_45 ),
inference(sat_conversion,[],[f433]) ).
cnf(s59,plain,
( ~ spl0_3
| spl0_15
| spl0_52
| spl0_58 ),
inference(sat_conversion,[],[f436]) ).
cnf(s60,plain,
( ~ spl0_3
| spl0_24
| spl0_30
| spl0_44 ),
inference(sat_conversion,[],[f437]) ).
cnf(s61,plain,
( ~ spl0_3
| spl0_24
| spl0_52
| spl0_57 ),
inference(sat_conversion,[],[f438]) ).
cnf(s62,plain,
( ~ spl0_45
| ~ spl0_60 ),
inference(sat_conversion,[],[f443]) ).
cnf(s63,plain,
( ~ spl0_52
| ~ spl0_61 ),
inference(sat_conversion,[],[f448]) ).
cnf(s64,plain,
( ~ spl0_52
| ~ spl0_62 ),
inference(sat_conversion,[],[f452]) ).
cnf(s65,plain,
( ~ spl0_52
| ~ spl0_63 ),
inference(sat_conversion,[],[f456]) ).
cnf(s66,plain,
( ~ spl0_30
| ~ spl0_64 ),
inference(sat_conversion,[],[f461]) ).
cnf(s68,plain,
( ~ spl0_44
| ~ spl0_66 ),
inference(sat_conversion,[],[f470]) ).
cnf(s69,plain,
( ~ spl0_42
| ~ spl0_67 ),
inference(sat_conversion,[],[f475]) ).
cnf(s70,plain,
( ~ spl0_42
| ~ spl0_68 ),
inference(sat_conversion,[],[f479]) ).
cnf(s71,plain,
( ~ spl0_32
| ~ spl0_69 ),
inference(sat_conversion,[],[f484]) ).
cnf(s72,plain,
( ~ spl0_56
| ~ spl0_70 ),
inference(sat_conversion,[],[f489]) ).
cnf(s78,plain,
( ~ spl0_22
| ~ spl0_76 ),
inference(sat_conversion,[],[f516]) ).
cnf(s79,plain,
( ~ spl0_22
| ~ spl0_77 ),
inference(sat_conversion,[],[f520]) ).
cnf(s80,plain,
( ~ spl0_22
| ~ spl0_78 ),
inference(sat_conversion,[],[f524]) ).
cnf(s81,plain,
( ~ spl0_58
| ~ spl0_79 ),
inference(sat_conversion,[],[f529]) ).
cnf(s82,plain,
( ~ spl0_38
| ~ spl0_80 ),
inference(sat_conversion,[],[f534]) ).
cnf(s83,plain,
( ~ spl0_38
| ~ spl0_81 ),
inference(sat_conversion,[],[f538]) ).
cnf(s84,plain,
( ~ spl0_39
| ~ spl0_82 ),
inference(sat_conversion,[],[f543]) ).
cnf(s86,plain,
( ~ spl0_36
| ~ spl0_84 ),
inference(sat_conversion,[],[f553]) ).
cnf(s87,plain,
( ~ spl0_36
| ~ spl0_85 ),
inference(sat_conversion,[],[f557]) ).
cnf(s88,plain,
( ~ spl0_31
| ~ spl0_86 ),
inference(sat_conversion,[],[f562]) ).
cnf(s89,plain,
( ~ spl0_31
| ~ spl0_87 ),
inference(sat_conversion,[],[f566]) ).
cnf(s90,plain,
( ~ spl0_59
| ~ spl0_88 ),
inference(sat_conversion,[],[f571]) ).
cnf(s91,plain,
( ~ spl0_27
| ~ spl0_89 ),
inference(sat_conversion,[],[f576]) ).
cnf(s92,plain,
( ~ spl0_27
| ~ spl0_90 ),
inference(sat_conversion,[],[f580]) ).
cnf(s94,plain,
( ~ spl0_26
| ~ spl0_92 ),
inference(sat_conversion,[],[f589]) ).
cnf(s95,plain,
( ~ spl0_54
| ~ spl0_93 ),
inference(sat_conversion,[],[f594]) ).
cnf(s96,plain,
( ~ spl0_49
| ~ spl0_94 ),
inference(sat_conversion,[],[f599]) ).
cnf(s97,plain,
( ~ spl0_48
| ~ spl0_95 ),
inference(sat_conversion,[],[f604]) ).
cnf(s98,plain,
( ~ spl0_21
| ~ spl0_96 ),
inference(sat_conversion,[],[f609]) ).
cnf(s99,plain,
( ~ spl0_21
| ~ spl0_97 ),
inference(sat_conversion,[],[f613]) ).
cnf(s100,plain,
( ~ spl0_21
| ~ spl0_98 ),
inference(sat_conversion,[],[f617]) ).
cnf(s102,plain,
( ~ spl0_51
| ~ spl0_100 ),
inference(sat_conversion,[],[f626]) ).
cnf(s103,plain,
( ~ spl0_51
| ~ spl0_101 ),
inference(sat_conversion,[],[f630]) ).
cnf(s104,plain,
( ~ spl0_50
| ~ spl0_102 ),
inference(sat_conversion,[],[f635]) ).
cnf(s105,plain,
( ~ spl0_50
| ~ spl0_103 ),
inference(sat_conversion,[],[f639]) ).
cnf(s106,plain,
( ~ spl0_47
| ~ spl0_104 ),
inference(sat_conversion,[],[f644]) ).
cnf(s108,plain,
( ~ spl0_45
| spl0_107 ),
inference(sat_conversion,[],[f655]) ).
cnf(s109,plain,
( ~ spl0_45
| spl0_108 ),
inference(sat_conversion,[],[f659]) ).
cnf(s110,plain,
( ~ spl0_30
| spl0_109 ),
inference(sat_conversion,[],[f663]) ).
cnf(s111,plain,
( ~ spl0_30
| spl0_110 ),
inference(sat_conversion,[],[f667]) ).
cnf(s112,plain,
( ~ spl0_44
| spl0_111 ),
inference(sat_conversion,[],[f671]) ).
cnf(s113,plain,
( ~ spl0_42
| spl0_112 ),
inference(sat_conversion,[],[f675]) ).
cnf(s114,plain,
( ~ spl0_32
| spl0_113 ),
inference(sat_conversion,[],[f679]) ).
cnf(s115,plain,
( ~ spl0_32
| spl0_114 ),
inference(sat_conversion,[],[f683]) ).
cnf(s116,plain,
( ~ spl0_56
| spl0_115 ),
inference(sat_conversion,[],[f687]) ).
cnf(s119,plain,
( ~ spl0_58
| spl0_118 ),
inference(sat_conversion,[],[f699]) ).
cnf(s120,plain,
( ~ spl0_58
| spl0_119 ),
inference(sat_conversion,[],[f703]) ).
cnf(s121,plain,
( ~ spl0_38
| spl0_120 ),
inference(sat_conversion,[],[f707]) ).
cnf(s122,plain,
( ~ spl0_39
| spl0_121 ),
inference(sat_conversion,[],[f711]) ).
cnf(s123,plain,
( ~ spl0_39
| spl0_122 ),
inference(sat_conversion,[],[f715]) ).
cnf(s124,plain,
( ~ spl0_55
| spl0_123 ),
inference(sat_conversion,[],[f719]) ).
cnf(s126,plain,
( ~ spl0_36
| spl0_125 ),
inference(sat_conversion,[],[f727]) ).
cnf(s127,plain,
( ~ spl0_31
| spl0_126 ),
inference(sat_conversion,[],[f731]) ).
cnf(s128,plain,
( ~ spl0_59
| spl0_127 ),
inference(sat_conversion,[],[f735]) ).
cnf(s129,plain,
( ~ spl0_59
| spl0_128 ),
inference(sat_conversion,[],[f739]) ).
cnf(s130,plain,
( ~ spl0_27
| spl0_129 ),
inference(sat_conversion,[],[f743]) ).
cnf(s131,plain,
( ~ spl0_26
| spl0_130 ),
inference(sat_conversion,[],[f747]) ).
cnf(s132,plain,
( ~ spl0_54
| spl0_131 ),
inference(sat_conversion,[],[f751]) ).
cnf(s133,plain,
( ~ spl0_54
| spl0_132 ),
inference(sat_conversion,[],[f755]) ).
cnf(s134,plain,
( ~ spl0_49
| spl0_133 ),
inference(sat_conversion,[],[f759]) ).
cnf(s135,plain,
( ~ spl0_49
| spl0_134 ),
inference(sat_conversion,[],[f763]) ).
cnf(s136,plain,
( ~ spl0_48
| spl0_135 ),
inference(sat_conversion,[],[f767]) ).
cnf(s138,plain,
( ~ spl0_50
| spl0_137 ),
inference(sat_conversion,[],[f775]) ).
cnf(s139,plain,
( ~ spl0_47
| spl0_138 ),
inference(sat_conversion,[],[f779]) ).
cnf(s140,plain,
( ~ spl0_47
| spl0_139 ),
inference(sat_conversion,[],[f783]) ).
cnf(s143,plain,
( ~ spl0_57
| spl0_142 ),
inference(sat_conversion,[],[f796]) ).
cnf(s144,plain,
( ~ spl0_57
| spl0_143 ),
inference(sat_conversion,[],[f800]) ).
cnf(s145,plain,
( ~ spl0_57
| spl0_144 ),
inference(sat_conversion,[],[f804]) ).
cnf(s146,plain,
( ~ spl0_23
| spl0_145 ),
inference(sat_conversion,[],[f809]) ).
cnf(s147,plain,
( ~ spl0_23
| spl0_146 ),
inference(sat_conversion,[],[f813]) ).
cnf(s148,plain,
( ~ spl0_23
| spl0_147 ),
inference(sat_conversion,[],[f817]) ).
cnf(s149,plain,
( ~ spl0_40
| spl0_148 ),
inference(sat_conversion,[],[f822]) ).
cnf(s150,plain,
( ~ spl0_40
| spl0_149 ),
inference(sat_conversion,[],[f826]) ).
cnf(s151,plain,
( ~ spl0_40
| spl0_150 ),
inference(sat_conversion,[],[f830]) ).
cnf(s152,plain,
( spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f837]) ).
cnf(s153,plain,
( ~ spl0_152
| spl0_153 ),
inference(sat_conversion,[],[f841]) ).
cnf(s154,plain,
( ~ spl0_152
| spl0_154 ),
inference(sat_conversion,[],[f845]) ).
cnf(s157,plain,
( spl0_27
| spl0_47
| spl0_52 ),
inference(sat_conversion,[],[f848]) ).
cnf(s159,plain,
( spl0_31
| spl0_52
| spl0_54 ),
inference(sat_conversion,[],[f850]) ).
cnf(s162,plain,
( spl0_32
| spl0_45
| spl0_52 ),
inference(sat_conversion,[],[f854]) ).
cnf(s163,plain,
( spl0_26
| spl0_38
| spl0_58 ),
inference(sat_conversion,[],[f855]) ).
cnf(s164,plain,
( spl0_42
| spl0_56
| spl0_152 ),
inference(sat_conversion,[],[f857]) ).
cnf(s165,plain,
( spl0_39
| spl0_47
| spl0_50 ),
inference(sat_conversion,[],[f858]) ).
cnf(s166,plain,
( spl0_32
| spl0_39
| spl0_50 ),
inference(sat_conversion,[],[f859]) ).
cnf(s168,plain,
( spl0_49
| spl0_57
| spl0_152 ),
inference(sat_conversion,[],[f861]) ).
cnf(s189,plain,
( spl0_3
| ~ spl0_49 ),
inference(sat_conversion,[],[f883]) ).
cnf(s196,plain,
( spl0_3
| ~ spl0_57 ),
inference(sat_conversion,[],[f890]) ).
cnf(s199,plain,
( spl0_3
| ~ spl0_152 ),
inference(sat_conversion,[],[f893]) ).
cnf(s200,plain,
( spl0_36
| spl0_49 ),
inference(sat_conversion,[],[f894]) ).
cnf(s203,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_20 ),
inference(sat_conversion,[],[f926]) ).
cnf(s206,plain,
( ~ spl0_7
| spl0_80
| ~ spl0_120
| ~ spl0_155 ),
inference(sat_conversion,[],[f944]) ).
cnf(s207,plain,
( ~ spl0_1
| ~ spl0_5
| spl0_19 ),
inference(sat_conversion,[],[f954]) ).
cnf(s208,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_81
| ~ spl0_120 ),
inference(sat_conversion,[],[f963]) ).
cnf(s209,plain,
( ~ spl0_1
| ~ spl0_5
| ~ spl0_13
| spl0_19 ),
inference(sat_conversion,[],[f964]) ).
cnf(s210,plain,
( ~ spl0_7
| ~ spl0_37
| spl0_70
| ~ spl0_115 ),
inference(sat_conversion,[],[f974]) ).
cnf(s222,plain,
( ~ spl0_13
| spl0_80
| spl0_81
| ~ spl0_120 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s223,plain,
( ~ spl0_14
| spl0_100
| spl0_101
| ~ spl0_156 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s224,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s232,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_92
| ~ spl0_130 ),
inference(sat_conversion,[],[f1104]) ).
cnf(s239,plain,
( ~ spl0_9
| ~ spl0_127
| ~ spl0_128
| spl0_158 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s247,plain,
( ~ spl0_12
| spl0_82
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s250,plain,
( ~ spl0_1
| ~ spl0_17
| spl0_102
| ~ spl0_137 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s251,plain,
( ~ spl0_1
| ~ spl0_16
| ~ spl0_17
| spl0_20 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s252,plain,
( ~ spl0_1
| ~ spl0_18
| spl0_61
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s253,plain,
( ~ spl0_18
| spl0_76
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s257,plain,
( ~ spl0_14
| ~ spl0_43
| ~ spl0_125
| spl0_159 ),
inference(sat_conversion,[],[f1275]) ).
cnf(s273,plain,
( ~ spl0_9
| spl0_93
| ~ spl0_131
| ~ spl0_165 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s275,plain,
( ~ spl0_9
| spl0_79
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f1336]) ).
cnf(s277,plain,
( ~ spl0_5
| spl0_64
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s278,plain,
( ~ spl0_7
| spl0_93
| ~ spl0_131
| ~ spl0_132 ),
inference(sat_conversion,[],[f1352]) ).
cnf(s281,plain,
( ~ spl0_14
| spl0_86
| spl0_87
| ~ spl0_126 ),
inference(sat_conversion,[],[f1364]) ).
cnf(s301,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f1428]) ).
cnf(s308,plain,
( ~ spl0_2
| ~ spl0_121
| ~ spl0_122
| ~ spl0_161 ),
inference(sat_conversion,[],[f1439]) ).
cnf(s313,plain,
( ~ spl0_5
| ~ spl0_145
| ~ spl0_147
| spl0_170 ),
inference(sat_conversion,[],[f1451]) ).
cnf(s338,plain,
( ~ spl0_16
| ~ spl0_131
| ~ spl0_132
| spl0_165 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s339,plain,
( ~ spl0_16
| spl0_104
| ~ spl0_138
| ~ spl0_139 ),
inference(sat_conversion,[],[f1558]) ).
cnf(s345,plain,
( ~ spl0_11
| spl0_89
| spl0_90
| ~ spl0_129 ),
inference(sat_conversion,[],[f1569]) ).
cnf(s351,plain,
( ~ spl0_5
| ~ spl0_13
| spl0_104
| ~ spl0_139 ),
inference(sat_conversion,[],[f1594]) ).
cnf(s353,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_131
| ~ spl0_132 ),
inference(sat_conversion,[],[f1603]) ).
cnf(s369,plain,
( ~ spl0_7
| ~ spl0_138
| ~ spl0_139
| spl0_169 ),
inference(sat_conversion,[],[f1642]) ).
cnf(s387,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_10
| ~ spl0_138
| ~ spl0_139 ),
inference(sat_conversion,[],[f1707]) ).
cnf(s394,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29
| ~ spl0_107 ),
inference(sat_conversion,[],[f1741]) ).
cnf(s398,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_15
| ~ spl0_29
| ~ spl0_123 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s401,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_107 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s404,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_113 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s405,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_29
| ~ spl0_123 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s413,plain,
( ~ spl0_11
| ~ spl0_16
| spl0_103
| ~ spl0_160 ),
inference(sat_conversion,[],[f1807]) ).
cnf(s423,plain,
( ~ spl0_5
| ~ spl0_8
| spl0_66
| ~ spl0_111 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s437,plain,
( ~ spl0_14
| ~ spl0_43
| spl0_69
| ~ spl0_114 ),
inference(sat_conversion,[],[f1869]) ).
cnf(s439,plain,
( ~ spl0_14
| ~ spl0_43
| ~ spl0_122
| spl0_161 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s450,plain,
( ~ spl0_1
| spl0_67
| spl0_68
| ~ spl0_112 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s454,plain,
( ~ spl0_6
| spl0_60
| ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f1894]) ).
cnf(s461,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_68
| ~ spl0_112 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s465,plain,
( ~ spl0_5
| ~ spl0_8
| ~ spl0_10
| ~ spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f1929]) ).
cnf(s466,plain,
( ~ spl0_5
| ~ spl0_13
| ~ spl0_24
| spl0_61
| spl0_63 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s472,plain,
( ~ spl0_14
| spl0_67
| spl0_68
| ~ spl0_162 ),
inference(sat_conversion,[],[f1972]) ).
cnf(s503,plain,
( ~ spl0_18
| spl0_62
| spl0_63
| spl0_164 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s507,plain,
( ~ spl0_2
| ~ spl0_28
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s509,plain,
( ~ spl0_2
| ~ spl0_28
| ~ spl0_127
| ~ spl0_128 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s544,plain,
( ~ spl0_16
| spl0_81
| ~ spl0_120
| ~ spl0_155 ),
inference(sat_conversion,[],[f2147]) ).
cnf(s556,plain,
( ~ spl0_9
| spl0_84
| ~ spl0_125
| ~ spl0_159 ),
inference(sat_conversion,[],[f2214]) ).
cnf(s568,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_127
| ~ spl0_158 ),
inference(sat_conversion,[],[f2269]) ).
cnf(s572,plain,
( ~ spl0_24
| spl0_61
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f2309]) ).
cnf(s573,plain,
( ~ spl0_24
| spl0_100
| spl0_101
| spl0_156 ),
inference(sat_conversion,[],[f2311]) ).
cnf(s578,plain,
( ~ spl0_5
| spl0_104
| ~ spl0_139
| ~ spl0_169 ),
inference(sat_conversion,[],[f2320]) ).
cnf(s588,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_25
| spl0_81
| ~ spl0_120 ),
inference(sat_conversion,[],[f2344]) ).
cnf(s589,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f2361]) ).
cnf(s595,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_29
| ~ spl0_148
| ~ spl0_150 ),
inference(sat_conversion,[],[f2373]) ).
cnf(s612,plain,
( ~ spl0_14
| spl0_60
| ~ spl0_108
| spl0_157 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s618,plain,
( ~ spl0_16
| ~ spl0_146
| ~ spl0_147
| spl0_170 ),
inference(sat_conversion,[],[f2394]) ).
cnf(s620,plain,
( ~ spl0_10
| ~ spl0_107
| ~ spl0_108
| ~ spl0_157 ),
inference(sat_conversion,[],[f2396]) ).
cnf(s629,plain,
( ~ spl0_14
| spl0_85
| ~ spl0_125
| spl0_159 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s633,plain,
( ~ spl0_10
| ~ spl0_145
| ~ spl0_146
| ~ spl0_170 ),
inference(sat_conversion,[],[f2399]) ).
cnf(s645,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f2436]) ).
cnf(s646,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_133
| ~ spl0_134 ),
inference(sat_conversion,[],[f2438]) ).
cnf(s647,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_143
| ~ spl0_144 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s649,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f2443]) ).
cnf(s671,plain,
( ~ spl0_4
| ~ spl0_145
| ~ spl0_147
| ~ spl0_170 ),
inference(sat_conversion,[],[f2479]) ).
cnf(s672,plain,
( ~ spl0_4
| ~ spl0_148
| ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s694,plain,
( ~ spl0_6
| ~ spl0_8
| spl0_95
| ~ spl0_135 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s705,plain,
( ~ spl0_6
| spl0_88
| ~ spl0_128
| ~ spl0_158 ),
inference(sat_conversion,[],[f2497]) ).
cnf(s725,plain,
( ~ spl0_14
| ~ spl0_43
| spl0_94
| ~ spl0_134 ),
inference(sat_conversion,[],[f2522]) ).
cnf(s730,plain,
( ~ spl0_7
| spl0_82
| ~ spl0_121
| ~ spl0_161 ),
inference(sat_conversion,[],[f2547]) ).
cnf(s731,plain,
( ~ spl0_8
| spl0_62
| spl0_63
| ~ spl0_164 ),
inference(sat_conversion,[],[f2562]) ).
cnf(s737,plain,
( ~ spl0_8
| spl0_102
| spl0_103
| ~ spl0_137 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s740,plain,
( ~ spl0_8
| spl0_68
| ~ spl0_112
| spl0_162 ),
inference(sat_conversion,[],[f2573]) ).
cnf(s741,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_10 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s774,plain,
( ~ spl0_2
| ~ spl0_142
| ~ spl0_143
| ~ spl0_144 ),
inference(sat_conversion,[],[f2615]) ).
cnf(s781,plain,
( ~ spl0_15
| spl0_61
| spl0_63
| spl0_164 ),
inference(sat_conversion,[],[f2677]) ).
cnf(s782,plain,
( ~ spl0_11
| ~ spl0_15
| spl0_76
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f2679]) ).
cnf(s783,plain,
( ~ spl0_15
| spl0_96
| spl0_97
| spl0_98 ),
inference(sat_conversion,[],[f2681]) ).
cnf(s785,plain,
( ~ spl0_15
| spl0_80
| spl0_81
| spl0_155 ),
inference(sat_conversion,[],[f2685]) ).
cnf(s796,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_127
| ~ spl0_128 ),
inference(sat_conversion,[],[f2706]) ).
cnf(s804,plain,
( ~ spl0_19
| spl0_67
| ~ spl0_112
| spl0_162 ),
inference(sat_conversion,[],[f2755]) ).
cnf(s805,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_64
| ~ spl0_109 ),
inference(sat_conversion,[],[f2775]) ).
cnf(s806,plain,
( ~ spl0_19
| ~ spl0_20
| spl0_66
| ~ spl0_111 ),
inference(sat_conversion,[],[f2777]) ).
cnf(s812,plain,
( ~ spl0_25
| spl0_81
| ~ spl0_120
| spl0_155 ),
inference(sat_conversion,[],[f2806]) ).
cnf(s816,plain,
( ~ spl0_10
| ~ spl0_151
| ~ spl0_153
| ~ spl0_154 ),
inference(sat_conversion,[],[f2814]) ).
cnf(s821,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_138
| ~ spl0_139 ),
inference(sat_conversion,[],[f2821]) ).
cnf(s828,plain,
( ~ spl0_2
| ~ spl0_16
| ~ spl0_17
| ~ spl0_137
| ~ spl0_160 ),
inference(sat_conversion,[],[f2823]) ).
cnf(s834,plain,
( ~ spl0_24
| spl0_102
| spl0_103
| spl0_160 ),
inference(sat_conversion,[],[f2827]) ).
cnf(s838,plain,
( ~ spl0_24
| spl0_61
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f2830]) ).
cnf(s839,plain,
spl0_3,
inference(rat,[],[s168,s189,s196,s199]) ).
cnf(s840,plain,
( ~ spl0_23
| ~ spl0_10
| ~ spl0_16 ),
inference(rat,[],[s633,s618,s146,s147,s148]) ).
cnf(s842,plain,
( ~ spl0_23
| ~ spl0_16
| ~ spl0_4 ),
inference(rat,[],[s671,s618,s146,s147,s148]) ).
cnf(s844,plain,
( ~ spl0_40
| ~ spl0_12
| ~ spl0_4 ),
inference(rat,[],[s649,s150,s151]) ).
cnf(s845,plain,
( ~ spl0_12
| spl0_6
| ~ spl0_4 ),
inference(rat,[],[s645,s122,s123,s46,s844,s839]) ).
cnf(s846,plain,
( ~ spl0_40
| ~ spl0_4 ),
inference(rat,[],[s672,s149,s150,s151]) ).
cnf(s847,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s454,s62,s108,s109,s845,s56,s13,s842,s30,s737,s104,s105,s138,s39,s846,s1,s839]) ).
cnf(s848,plain,
( ~ spl0_45
| ~ spl0_6 ),
inference(rat,[],[s454,s62,s108,s109]) ).
cnf(s849,plain,
( ~ spl0_47
| ~ spl0_16
| ~ spl0_2 ),
inference(rat,[],[s821,s139,s140]) ).
cnf(s852,plain,
( ~ spl0_49
| ~ spl0_12
| ~ spl0_4 ),
inference(rat,[],[s646,s134,s135]) ).
cnf(s853,plain,
( ~ spl0_30
| ~ spl0_19
| ~ spl0_20 ),
inference(rat,[],[s805,s66,s110]) ).
cnf(s854,plain,
( ~ spl0_44
| ~ spl0_19
| ~ spl0_20 ),
inference(rat,[],[s806,s68,s112]) ).
cnf(s855,plain,
( ~ spl0_152
| ~ spl0_10 ),
inference(rat,[],[s816,s152,s153,s154]) ).
cnf(s856,plain,
( ~ spl0_12
| ~ spl0_4
| ~ spl0_2 ),
inference(rat,[],[s647,s144,s145,s168,s855,s852,s741,s845]) ).
cnf(s857,plain,
( ~ spl0_57
| ~ spl0_2 ),
inference(rat,[],[s774,s143,s144,s145]) ).
cnf(s858,plain,
( ~ spl0_42
| ~ spl0_6
| ~ spl0_8 ),
inference(rat,[],[s461,s70,s113]) ).
cnf(s859,plain,
( spl0_14
| ~ spl0_47
| spl0_12 ),
inference(rat,[],[s222,s82,s83,s121,s24,s351,s6,s140,s106,s839]) ).
cnf(s862,plain,
( ~ spl0_58
| ~ spl0_28
| ~ spl0_2 ),
inference(rat,[],[s507,s119,s120]) ).
cnf(s863,plain,
( ~ spl0_28
| spl0_1 ),
inference(rat,[],[s509,s128,s129,s54,s862,s847,s839]) ).
cnf(s864,plain,
( spl0_14
| spl0_5
| spl0_12 ),
inference(rat,[],[s222,s82,s83,s121,s24,s6,s839]) ).
cnf(s865,plain,
( ~ spl0_51
| ~ spl0_14
| ~ spl0_24 ),
inference(rat,[],[s223,s573,s102,s103]) ).
cnf(s866,plain,
( ~ spl0_20
| spl0_94
| ~ spl0_134
| spl0_42
| ~ spl0_10
| ~ spl0_113
| ~ spl0_8
| ~ spl0_19
| spl0_12
| spl0_28 ),
inference(rat,[],[s253,s78,s79,s80,s53,s210,s40,s865,s31,s725,s864,s404,s17,s60,s854,s853,s116,s72,s164,s855,s839]) ).
cnf(s867,plain,
( ~ spl0_6
| spl0_16
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s864,s281,s313,s671,s88,s89,s127,s146,s148,s18,s47,s866,s96,s135,s168,s855,s858,s848,s741,s857,s856,s847,s26,s863,s30,s114,s49,s846,s839]) ).
cnf(s868,plain,
( spl0_14
| spl0_76
| spl0_77
| spl0_78
| ~ spl0_113
| ~ spl0_8
| spl0_12
| ~ spl0_4
| spl0_28 ),
inference(rat,[],[s301,s110,s111,s17,s404,s5,s782,s864,s33,s846,s839]) ).
cnf(s869,plain,
( spl0_16
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s472,s740,s69,s70,s113,s31,s439,s868,s253,s308,s78,s79,s80,s122,s123,s45,s46,s867,s114,s49,s30,s863,s846,s856,s847,s839]) ).
cnf(s870,plain,
( ~ spl0_6
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s838,s63,s64,s65,s162,s114,s866,s60,s96,s135,s854,s853,s858,s168,s47,s56,s855,s848,s741,s857,s856,s847,s26,s863,s846,s842,s869,s839]) ).
cnf(s871,plain,
( ~ spl0_20
| ~ spl0_10
| spl0_32
| ~ spl0_5
| ~ spl0_13
| ~ spl0_8
| ~ spl0_19
| spl0_28 ),
inference(rat,[],[s466,s63,s65,s162,s108,s401,s17,s60,s854,s853,s839]) ).
cnf(s872,plain,
( spl0_14
| ~ spl0_8
| spl0_76
| spl0_77
| spl0_78
| spl0_23
| spl0_12
| ~ spl0_4
| spl0_28 ),
inference(rat,[],[s301,s110,s111,s17,s394,s108,s47,s871,s5,s114,s782,s868,s864,s33,s6,s26,s846,s839]) ).
cnf(s873,plain,
( ~ spl0_8
| spl0_161
| spl0_76
| spl0_77
| spl0_78
| ~ spl0_122
| spl0_23
| spl0_12
| ~ spl0_4
| spl0_28 ),
inference(rat,[],[s472,s740,s69,s70,s113,s31,s439,s872,s253,s839]) ).
cnf(s874,plain,
( spl0_14
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s301,s110,s111,s17,s589,s8,s782,s864,s33,s109,s108,s56,s873,s308,s122,s78,s79,s80,s45,s123,s46,s870,s846,s856,s847,s863,s842,s869,s839]) ).
cnf(s875,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s804,s472,s69,s70,s113,s31,s439,s874,s253,s308,s78,s79,s80,s122,s123,s45,s46,s870,s26,s846,s847,s863,s839]) ).
cnf(s876,plain,
( ~ spl0_21
| ~ spl0_15 ),
inference(rat,[],[s783,s98,s99,s100]) ).
cnf(s877,plain,
( ~ spl0_38
| ~ spl0_7
| ~ spl0_15 ),
inference(rat,[],[s785,s206,s82,s83,s121]) ).
cnf(s878,plain,
( ~ spl0_30
| ~ spl0_5 ),
inference(rat,[],[s277,s66,s110,s111]) ).
cnf(s879,plain,
( spl0_16
| ~ spl0_8
| ~ spl0_6
| spl0_14
| spl0_1 ),
inference(rat,[],[s17,s398,s878,s124,s24,s48,s877,s11,s876,s7,s863,s875,s796,s128,s741,s847,s129,s55,s848,s839]) ).
cnf(s880,plain,
( ~ spl0_50
| ~ spl0_8 ),
inference(rat,[],[s737,s104,s105,s138]) ).
cnf(s881,plain,
( ~ spl0_39
| ~ spl0_12 ),
inference(rat,[],[s247,s84,s122,s123]) ).
cnf(s882,plain,
( ~ spl0_8
| ~ spl0_6
| spl0_14
| spl0_39
| spl0_1 ),
inference(rat,[],[s165,s849,s880,s879,s847]) ).
cnf(s883,plain,
( ~ spl0_6
| spl0_14
| spl0_39
| spl0_1 ),
inference(rat,[],[s840,s56,s30,s882,s848,s741,s847,s839]) ).
cnf(s887,plain,
( ~ spl0_15
| ~ spl0_47
| spl0_14
| spl0_4 ),
inference(rat,[],[s578,s24,s369,s877,s11,s876,s140,s139,s106,s839]) ).
cnf(s888,plain,
( ~ spl0_58
| ~ spl0_9 ),
inference(rat,[],[s275,s81,s119,s120]) ).
cnf(s889,plain,
( ~ spl0_8
| spl0_14
| spl0_39
| spl0_1 ),
inference(rat,[],[s812,s206,s82,s83,s121,s24,s578,s369,s14,s9,s838,s503,s731,s63,s64,s65,s59,s888,s7,s887,s849,s106,s139,s140,s165,s880,s847,s875,s883,s839]) ).
cnf(s890,plain,
( ~ spl0_5
| spl0_14
| spl0_39
| spl0_1 ),
inference(rat,[],[s60,s834,s854,s413,s203,s25,s8,s595,s17,s878,s863,s151,s149,s46,s883,s105,s104,s165,s849,s30,s889,s847,s839]) ).
cnf(s891,plain,
( spl0_14
| spl0_39
| spl0_1 ),
inference(rat,[],[s8,s828,s413,s834,s14,s588,s877,s83,s121,s24,s2,s890,s104,s105,s138,s165,s849,s30,s889,s883,s847,s839]) ).
cnf(s896,plain,
( ~ spl0_31
| ~ spl0_14 ),
inference(rat,[],[s281,s88,s89,s127]) ).
cnf(s897,plain,
( ~ spl0_54
| ~ spl0_7 ),
inference(rat,[],[s278,s95,s132,s133]) ).
cnf(s898,plain,
( ~ spl0_15
| ~ spl0_8
| spl0_31
| spl0_4 ),
inference(rat,[],[s731,s781,s63,s64,s65,s159,s897,s11,s876,s839]) ).
cnf(s899,plain,
( spl0_16
| ~ spl0_14
| spl0_39
| spl0_4 ),
inference(rat,[],[s472,s740,s69,s70,s113,s31,s503,s731,s64,s65,s59,s888,s7,s898,s437,s71,s115,s166,s880,s30,s896,s839]) ).
cnf(s901,plain,
( ~ spl0_10
| spl0_8
| ~ spl0_16
| ~ spl0_14 ),
inference(rat,[],[s612,s620,s62,s108,s109,s56,s840,s839]) ).
cnf(s902,plain,
( spl0_39
| spl0_1 ),
inference(rat,[],[s556,s629,s86,s87,s126,s22,s568,s239,s128,s129,s54,s888,s4,s901,s880,s165,s849,s899,s891,s847,s875,s839]) ).
cnf(s903,plain,
( spl0_16
| spl0_43
| ~ spl0_14
| spl0_4 ),
inference(rat,[],[s472,s740,s69,s70,s113,s31,s503,s731,s64,s65,s59,s888,s7,s898,s30,s896,s839]) ).
cnf(s904,plain,
( ~ spl0_42
| ~ spl0_8
| ~ spl0_14 ),
inference(rat,[],[s472,s740,s69,s70,s113]) ).
cnf(s905,plain,
( ~ spl0_52
| ~ spl0_18
| ~ spl0_8 ),
inference(rat,[],[s503,s731,s64,s65]) ).
cnf(s906,plain,
( ~ spl0_8
| spl0_43
| ~ spl0_14
| spl0_57 ),
inference(rat,[],[s40,s897,s865,s159,s61,s905,s31,s904,s896,s839]) ).
cnf(s907,plain,
( ~ spl0_14
| spl0_1 ),
inference(rat,[],[s556,s629,s86,s87,s126,s22,s568,s239,s128,s129,s54,s888,s4,s901,s906,s903,s439,s857,s875,s308,s123,s847,s122,s902,s839]) ).
cnf(s909,plain,
( ~ spl0_27
| ~ spl0_11 ),
inference(rat,[],[s345,s91,s92,s130]) ).
cnf(s911,plain,
( ~ spl0_44
| ~ spl0_8
| ~ spl0_5 ),
inference(rat,[],[s423,s68,s112]) ).
cnf(s912,plain,
( ~ spl0_52
| ~ spl0_24 ),
inference(rat,[],[s572,s63,s64,s65]) ).
cnf(s913,plain,
( ~ spl0_8
| spl0_1 ),
inference(rat,[],[s162,s108,s114,s401,s404,s5,s909,s157,s912,s60,s911,s859,s17,s878,s864,s907,s881,s902,s863,s839]) ).
cnf(s914,plain,
( spl0_11
| spl0_1 ),
inference(rat,[],[s589,s108,s109,s56,s840,s8,s5,s847,s17,s878,s864,s907,s881,s902,s863,s30,s913,s839]) ).
cnf(s915,plain,
( ~ spl0_54
| spl0_1 ),
inference(rat,[],[s353,s132,s133,s847,s30,s913,s839]) ).
cnf(s916,plain,
spl0_1,
inference(rat,[],[s224,s147,s148,s44,s915,s595,s149,s151,s26,s854,s60,s912,s157,s909,s203,s914,s30,s913,s17,s878,s864,s859,s907,s881,s902,s863,s847,s839]) ).
cnf(s918,plain,
( ~ spl0_32
| ~ spl0_43
| ~ spl0_14 ),
inference(rat,[],[s437,s71,s115]) ).
cnf(s919,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_8 ),
inference(rat,[],[s439,s308,s122,s123,s166,s918,s906,s857,s880]) ).
cnf(s920,plain,
( ~ spl0_49
| ~ spl0_43
| ~ spl0_14 ),
inference(rat,[],[s725,s96,s135]) ).
cnf(s921,plain,
( spl0_16
| spl0_15
| spl0_4
| ~ spl0_14 ),
inference(rat,[],[s556,s257,s86,s126,s200,s920,s7,s903,s839]) ).
cnf(s922,plain,
( ~ spl0_47
| ~ spl0_16 ),
inference(rat,[],[s339,s106,s139,s140]) ).
cnf(s923,plain,
( ~ spl0_14
| ~ spl0_8 ),
inference(rat,[],[s694,s9,s97,s136,s730,s38,s439,s920,s31,s905,s157,s909,s5,s840,s13,s881,s84,s122,s123,s165,s922,s921,s898,s846,s39,s919,s904,s896,s880,s839]) ).
cnf(s924,plain,
~ spl0_42,
inference(rat,[],[s450,s69,s70,s113,s916]) ).
cnf(s925,plain,
( ~ spl0_7
| ~ spl0_10
| ~ spl0_25
| ~ spl0_138
| ~ spl0_139
| ~ spl0_8 ),
inference(rat,[],[s206,s812,s82,s83,s121,s24,s387,s923,s839]) ).
cnf(s926,plain,
( ~ spl0_10
| ~ spl0_25
| spl0_18
| ~ spl0_9
| ~ spl0_138
| ~ spl0_139
| ~ spl0_8 ),
inference(rat,[],[s796,s128,s129,s55,s848,s9,s925,s923,s839]) ).
cnf(s927,plain,
( ~ spl0_47
| ~ spl0_2
| spl0_16
| ~ spl0_8 ),
inference(rat,[],[s206,s812,s82,s83,s121,s24,s578,s369,s9,s741,s926,s14,s912,s905,s59,s888,s7,s887,s856,s859,s106,s139,s140,s923,s839]) ).
cnf(s928,plain,
( ~ spl0_26
| ~ spl0_5
| ~ spl0_13 ),
inference(rat,[],[s232,s94,s131]) ).
cnf(s929,plain,
( spl0_38
| ~ spl0_2
| spl0_16
| ~ spl0_8 ),
inference(rat,[],[s17,s405,s862,s124,s163,s48,s5,s909,s157,s912,s60,s911,s878,s928,s864,s6,s881,s165,s927,s880,s923,s839]) ).
cnf(s930,plain,
( ~ spl0_2
| spl0_16
| ~ spl0_8 ),
inference(rat,[],[s208,s83,s121,s929,s864,s6,s881,s165,s927,s880,s923,s839]) ).
cnf(s931,plain,
( ~ spl0_6
| ~ spl0_9
| spl0_14 ),
inference(rat,[],[s705,s239,s90,s128,s129,s55,s848,s839]) ).
cnf(s932,plain,
( ~ spl0_47
| spl0_16
| ~ spl0_8 ),
inference(rat,[],[s206,s812,s82,s83,s121,s24,s578,s369,s9,s931,s14,s912,s905,s59,s888,s7,s887,s106,s139,s140,s923,s846,s39,s930,s880,s839]) ).
cnf(s933,plain,
( spl0_16
| ~ spl0_8 ),
inference(rat,[],[s157,s909,s912,s5,s60,s465,s911,s878,s146,s147,s864,s13,s881,s165,s932,s930,s880,s923,s839]) ).
cnf(s934,plain,
( spl0_28
| ~ spl0_8 ),
inference(rat,[],[s114,s866,s871,s209,s6,s251,s8,s135,s96,s168,s857,s13,s840,s855,s5,s909,s157,s912,s60,s911,s878,s864,s923,s881,s165,s922,s933,s880,s924,s839,s916]) ).
cnf(s935,plain,
~ spl0_8,
inference(rat,[],[s208,s83,s121,s163,s862,s934,s13,s840,s5,s909,s157,s912,s60,s928,s911,s878,s864,s6,s881,s165,s922,s933,s923,s880,s839]) ).
cnf(s936,plain,
spl0_16,
inference(rat,[],[s30,s839,s935]) ).
cnf(s937,plain,
~ spl0_47,
inference(rat,[],[s922,s936]) ).
cnf(s940,plain,
( ~ spl0_43
| ~ spl0_14 ),
inference(rat,[],[s556,s257,s86,s126,s200,s920,s4,s901,s935,s839,s936]) ).
cnf(s941,plain,
( ~ spl0_52
| ~ spl0_18 ),
inference(rat,[],[s252,s63,s64,s65,s916]) ).
cnf(s942,plain,
~ spl0_14,
inference(rat,[],[s273,s338,s95,s132,s133,s159,s941,s31,s940,s4,s901,s896,s936,s839,s924,s935]) ).
cnf(s943,plain,
( ~ spl0_50
| ~ spl0_17 ),
inference(rat,[],[s250,s104,s138,s916]) ).
cnf(s944,plain,
( ~ spl0_2
| ~ spl0_107
| ~ spl0_108
| ~ spl0_58
| ~ spl0_17
| spl0_30 ),
inference(rat,[],[s589,s17,s862,s936,s839]) ).
cnf(s945,plain,
( spl0_11
| spl0_38 ),
inference(rat,[],[s13,s944,s108,s109,s56,s163,s840,s928,s5,s6,s881,s165,s943,s8,s878,s24,s839,s935,s936,s942,s937]) ).
cnf(s946,plain,
spl0_38,
inference(rat,[],[s912,s60,s157,s854,s909,s203,s945,s878,s207,s24,s839,s937,s916,s942]) ).
cnf(s947,plain,
spl0_120,
inference(rat,[],[s121,s946]) ).
cnf(s948,plain,
~ spl0_81,
inference(rat,[],[s83,s946]) ).
cnf(s949,plain,
~ spl0_80,
inference(rat,[],[s82,s946]) ).
cnf(s950,plain,
~ spl0_155,
inference(rat,[],[s544,s948,s936,s947]) ).
cnf(s951,plain,
~ spl0_13,
inference(rat,[],[s222,s947,s948,s949]) ).
cnf(s952,plain,
~ spl0_15,
inference(rat,[],[s785,s948,s950,s949]) ).
cnf(s953,plain,
~ spl0_25,
inference(rat,[],[s812,s948,s947,s950]) ).
cnf(s954,plain,
spl0_12,
inference(rat,[],[s6,s942,s839,s951]) ).
cnf(s956,plain,
spl0_24,
inference(rat,[],[s14,s952,s839,s953]) ).
cnf(s957,plain,
~ spl0_39,
inference(rat,[],[s881,s954]) ).
cnf(s962,plain,
~ spl0_52,
inference(rat,[],[s912,s956]) ).
cnf(s963,plain,
spl0_50,
inference(rat,[],[s165,s937,s957]) ).
cnf(s964,plain,
spl0_27,
inference(rat,[],[s157,s937,s962]) ).
cnf(s969,plain,
~ spl0_17,
inference(rat,[],[s943,s963]) ).
cnf(s973,plain,
~ spl0_11,
inference(rat,[],[s909,s964]) ).
cnf(s979,plain,
$false,
inference(rat,[],[s8,s942,s839,s973,s969]) ).
fof(f2831,plain,
$false,
inference(avatar_sat_refutation,[],[s979]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN481-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n004.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 16:15:07 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.66/1.00 % (497149)Input is clausal, will run a generic CNF schedule.
% 0.66/1.00 % (497158)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2502497161:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.66/1.00 % (497158)First to succeed.
% 0.66/1.00 % (497158)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-497149"
% 0.66/1.00 % (497155)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=913503901:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.66/1.00 % (497154)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=20069862:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.66/1.00 % (497156)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2727570848:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.66/1.00 % (497157)lrs+10_1_sil=8000:sp=occurrence:random_seed=3750361361:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.66/1.00 % (497159)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3630021420:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.66/1.00 % (497160)dis-21_1_sil=8000:lcm=predicate:random_seed=1914153322:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.66/1.00 % (497160)Also succeeded, but the first one will report.
% 0.66/1.00 % (497157)Also succeeded, but the first one will report.
% 0.66/1.00 % (497159)Also succeeded, but the first one will report.
% 0.66/1.00 % (497158)Refutation found. Thanks to Tanya!
% 0.66/1.00 % SZS status Unsatisfiable for theBenchmark
% 0.66/1.00 % SZS output start Proof for theBenchmark
% See solution above
% 2.82/1.19 % (497158)------------------------------
% 2.82/1.19 % (497158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.19 % (497158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.19 % (497158)CaDiCaL version: 2.1.3
% 2.82/1.19 % (497158)Termination reason: Refutation
% 2.82/1.19 % (497158)Time elapsed: 0.025 s
% 2.82/1.19 % (497158)Peak memory usage: 90 MB
% 2.82/1.19 % (497158)Instructions burned: 68 (million)
% 2.82/1.19 % (497158)------------------------------
% 2.82/1.19 % (497158)------------------------------
% 2.82/1.19 % (497149)Success in time 0.311 s
% 2.82/1.19 % Vampire exiting
%------------------------------------------------------------------------------