%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN457-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 02:09:03 PM UTC 2026
% Result : Unsatisfiable 0.44s 0.31s
% Output : Refutation 0.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 270
% Syntax : Number of formulae : 956 ( 39 unt; 154 def)
% Number of atoms : 2819 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 3235 (1372 ~;1709 |; 0 &)
% ( 154 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 192 ( 191 usr; 188 prp; 0-1 aty)
% Number of functors : 29 ( 29 usr; 29 con; 0-0 aty)
% Number of variables : 150 ( 0 sgn 150 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,negated_conjecture,
( ~ hskp65
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
fof(f12,negated_conjecture,
( ~ hskp64
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
fof(f53,negated_conjecture,
( ~ hskp23
| ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
fof(f78,negated_conjecture,
( hskp47
| hskp2
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
fof(f81,negated_conjecture,
( hskp23
| hskp64
| hskp65 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
fof(f83,negated_conjecture,
( hskp29
| hskp52
| hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
fof(f87,negated_conjecture,
( ~ hskp74
| c0_1(a1717) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp74
| c2_1(a1717) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ hskp73
| c2_1(a1716) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ hskp73
| c0_1(a1716) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ hskp72
| c1_1(a1715) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ hskp72
| c3_1(a1715) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
fof(f100,negated_conjecture,
( ~ hskp67
| c1_1(a1702) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ hskp67
| c2_1(a1702) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ hskp67
| c3_1(a1702) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause102) ).
fof(f106,negated_conjecture,
( ~ hskp63
| c2_1(a1676) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ hskp63
| c3_1(a1676) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause107) ).
fof(f110,negated_conjecture,
( ~ hskp61
| c3_1(a1674) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ hskp60
| c3_1(a1673) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ hskp60
| c2_1(a1673) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ hskp59
| c3_1(a1669) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ hskp59
| c0_1(a1669) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ hskp58
| c3_1(a1668) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause115) ).
fof(f120,negated_conjecture,
( ~ hskp55
| c1_1(a1661) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause120) ).
fof(f123,negated_conjecture,
( ~ hskp53
| c2_1(a1656) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ hskp53
| c0_1(a1656) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ hskp52
| c0_1(a1654) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ hskp52
| c2_1(a1654) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ hskp52
| c3_1(a1654) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause127) ).
fof(f135,negated_conjecture,
( ~ hskp48
| c0_1(a1649) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
( ~ hskp47
| c3_1(a1644) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause136) ).
fof(f148,negated_conjecture,
( ~ hskp40
| c1_1(a1725) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause148) ).
fof(f149,negated_conjecture,
( ~ hskp40
| c3_1(a1725) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
( ~ hskp39
| c3_1(a1721) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
( ~ hskp38
| c3_1(a1718) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
( ~ hskp37
| c2_1(a1714) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
( ~ hskp37
| c0_1(a1714) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause153) ).
fof(f161,negated_conjecture,
( ~ hskp29
| c2_1(a1695) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
( ~ hskp29
| c0_1(a1695) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause162) ).
fof(f173,negated_conjecture,
( ~ hskp13
| c0_1(a1667) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
( ~ hskp13
| c3_1(a1667) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
( ~ hskp12
| c2_1(a1666) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
( ~ hskp12
| c3_1(a1666) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause176) ).
fof(f178,negated_conjecture,
( ~ hskp7
| c3_1(a1655) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
( ~ hskp7
| c0_1(a1655) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause179) ).
fof(f182,negated_conjecture,
( ~ hskp3
| c0_1(a1646) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause182) ).
fof(f187,negated_conjecture,
( ~ c3_1(a1717)
| ~ hskp74 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
( ~ c3_1(a1716)
| ~ hskp73 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
( ~ c2_1(a1715)
| ~ hskp72 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause189) ).
fof(f201,negated_conjecture,
( ~ c0_1(a1676)
| ~ hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause201) ).
fof(f203,negated_conjecture,
( ~ c1_1(a1674)
| ~ hskp61 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
( ~ c2_1(a1674)
| ~ hskp61 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
( ~ c1_1(a1673)
| ~ hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
( ~ c2_1(a1669)
| ~ hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
( ~ c0_1(a1668)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
( ~ c1_1(a1668)
| ~ hskp58 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause208) ).
fof(f211,negated_conjecture,
( ~ c2_1(a1661)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause211) ).
fof(f212,negated_conjecture,
( ~ c3_1(a1661)
| ~ hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause212) ).
fof(f214,negated_conjecture,
( ~ c3_1(a1656)
| ~ hskp53 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause214) ).
fof(f217,negated_conjecture,
( ~ c3_1(a1649)
| ~ hskp48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause217) ).
fof(f218,negated_conjecture,
( ~ c2_1(a1649)
| ~ hskp48 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause218) ).
fof(f219,negated_conjecture,
( ~ c1_1(a1644)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause219) ).
fof(f220,negated_conjecture,
( ~ c0_1(a1644)
| ~ hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause220) ).
fof(f228,negated_conjecture,
( ~ c2_1(a1725)
| ~ hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause228) ).
fof(f229,negated_conjecture,
( ~ c1_1(a1721)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause229) ).
fof(f230,negated_conjecture,
( ~ c0_1(a1721)
| ~ hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause230) ).
fof(f231,negated_conjecture,
( ~ c2_1(a1718)
| ~ hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause231) ).
fof(f233,negated_conjecture,
( ~ c1_1(a1714)
| ~ hskp37 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause233) ).
fof(f248,negated_conjecture,
( ~ c3_1(a1695)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause248) ).
fof(f254,negated_conjecture,
( ~ c3_1(a1691)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause254) ).
fof(f255,negated_conjecture,
( ~ c1_1(a1691)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause255) ).
fof(f256,negated_conjecture,
( ~ c2_1(a1691)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause256) ).
fof(f275,negated_conjecture,
( ~ c0_1(a1678)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause275) ).
fof(f276,negated_conjecture,
( ~ c1_1(a1678)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause276) ).
fof(f277,negated_conjecture,
( ~ c2_1(a1678)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause277) ).
fof(f278,negated_conjecture,
( ~ c0_1(a1677)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause278) ).
fof(f279,negated_conjecture,
( ~ c2_1(a1677)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause279) ).
fof(f280,negated_conjecture,
( ~ c1_1(a1677)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause280) ).
fof(f284,negated_conjecture,
( ~ c1_1(a1667)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause284) ).
fof(f285,negated_conjecture,
( ~ c1_1(a1666)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause285) ).
fof(f292,negated_conjecture,
( ~ c3_1(a1660)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause292) ).
fof(f293,negated_conjecture,
( ~ c0_1(a1660)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause293) ).
fof(f294,negated_conjecture,
( ~ c1_1(a1660)
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause294) ).
fof(f297,negated_conjecture,
( ~ c2_1(a1655)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause297) ).
fof(f298,negated_conjecture,
( ~ c1_1(a1650)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause298) ).
fof(f299,negated_conjecture,
( ~ c2_1(a1650)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause299) ).
fof(f300,negated_conjecture,
( ~ c3_1(a1650)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause300) ).
fof(f305,negated_conjecture,
( ~ c1_1(a1646)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause305) ).
fof(f306,negated_conjecture,
( ~ c2_1(a1646)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause306) ).
fof(f307,negated_conjecture,
( ~ c1_1(a1645)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause307) ).
fof(f308,negated_conjecture,
( ~ c0_1(a1645)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause308) ).
fof(f309,negated_conjecture,
( ~ c3_1(a1645)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause309) ).
fof(f314,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c3_1(X0)
| c0_1(X0)
| c2_1(X0)
| hskp37
| hskp72 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause314) ).
fof(f316,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp58
| hskp59 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause316) ).
fof(f323,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp48
| hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause323) ).
fof(f324,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp52
| hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause324) ).
fof(f325,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp9
| hskp55 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause325) ).
fof(f328,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp16
| hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause328) ).
fof(f332,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| hskp12
| hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause332) ).
fof(f333,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| hskp74
| hskp38 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause333) ).
fof(f337,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp60 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause337) ).
fof(f346,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause346) ).
fof(f347,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X0)
| c3_1(X0)
| c2_1(X1)
| hskp61 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause347) ).
fof(f349,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| hskp67 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause349) ).
fof(f351,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp73 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause351) ).
fof(f352,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| hskp47 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause352) ).
fof(f353,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| hskp39 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause353) ).
fof(f354,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp40 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause354) ).
fof(f355,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp63 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause355) ).
fof(f356,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X0)
| hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause356) ).
fof(f357,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X1)
| hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause357) ).
fof(f359,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause359) ).
fof(f361,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c1_1(X1)
| c2_1(X2)
| c3_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause361) ).
fof(f362,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c2_1(X0)
| c2_1(X1)
| c0_1(X1)
| c1_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause362) ).
fof(f363,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c0_1(X0)
| c1_1(X0)
| c1_1(X1)
| c3_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause363) ).
fof(f364,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X2)
| c2_1(X0)
| c1_1(X0)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause364) ).
fof(f375,plain,
( ~ hskp65
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f376,plain,
( ~ hskp64
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f417,plain,
( hskp23
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f441,plain,
( hskp47
| hskp2
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f444,plain,
( ~ hskp23
| hskp64
| hskp65 ),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f446,plain,
( hskp29
| ~ hskp52
| hskp53 ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f450,plain,
( hskp74
| c0_1(a1717) ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f451,plain,
( hskp74
| c2_1(a1717) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f452,plain,
( hskp73
| c2_1(a1716) ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f453,plain,
( hskp73
| c0_1(a1716) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f454,plain,
( hskp72
| ~ c1_1(a1715) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f455,plain,
( hskp72
| ~ c3_1(a1715) ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f461,plain,
( ~ hskp67
| ~ c1_1(a1702) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f462,plain,
( ~ hskp67
| ~ c3_1(a1702) ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f464,plain,
( hskp63
| c2_1(a1676) ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f465,plain,
( hskp63
| ~ c3_1(a1676) ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f467,plain,
( ~ hskp61
| ~ c3_1(a1674) ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f468,plain,
( ~ hskp60
| ~ c3_1(a1673) ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f469,plain,
( hskp59
| ~ c3_1(a1669) ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f470,plain,
( hskp59
| c0_1(a1669) ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f471,plain,
( ~ hskp58
| ~ c3_1(a1668) ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f476,plain,
( ~ hskp55
| ~ c1_1(a1661) ),
inference(consistent_polarity_flipping,[],[f120]) ).
fof(f479,plain,
( hskp52
| c0_1(a1654) ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f480,plain,
( hskp52
| c2_1(a1654) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f481,plain,
( hskp52
| ~ c3_1(a1654) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f488,plain,
( hskp48
| c0_1(a1649) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f489,plain,
( ~ hskp47
| ~ c3_1(a1644) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f495,plain,
( ~ hskp40
| ~ c1_1(a1725) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f496,plain,
( ~ hskp40
| ~ c3_1(a1725) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f497,plain,
( ~ hskp39
| ~ c3_1(a1721) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f498,plain,
( ~ hskp38
| ~ c3_1(a1718) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f512,plain,
( ~ hskp13
| ~ c3_1(a1667) ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f513,plain,
( hskp12
| c2_1(a1666) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f514,plain,
( hskp12
| ~ c3_1(a1666) ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f516,plain,
( hskp7
| ~ c3_1(a1655) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f517,plain,
( hskp7
| c0_1(a1655) ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f520,plain,
( hskp3
| c0_1(a1646) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f524,plain,
( c3_1(a1717)
| hskp74 ),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f525,plain,
( c3_1(a1716)
| hskp73 ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f526,plain,
( ~ c2_1(a1715)
| hskp72 ),
inference(consistent_polarity_flipping,[],[f189]) ).
fof(f537,plain,
( ~ c0_1(a1676)
| hskp63 ),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f539,plain,
( c1_1(a1674)
| ~ hskp61 ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f540,plain,
( c1_1(a1673)
| ~ hskp60 ),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f541,plain,
( ~ c2_1(a1669)
| hskp59 ),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f542,plain,
( c1_1(a1668)
| ~ hskp58 ),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f545,plain,
( c3_1(a1661)
| ~ hskp55 ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f546,plain,
( c3_1(a1656)
| ~ hskp53 ),
inference(consistent_polarity_flipping,[],[f214]) ).
fof(f547,plain,
( c3_1(a1649)
| hskp48 ),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f548,plain,
( ~ c2_1(a1649)
| hskp48 ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f549,plain,
( c1_1(a1644)
| ~ hskp47 ),
inference(consistent_polarity_flipping,[],[f219]) ).
fof(f557,plain,
( c1_1(a1721)
| ~ hskp39 ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f558,plain,
( c1_1(a1714)
| ~ hskp37 ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f569,plain,
( c3_1(a1695)
| ~ hskp29 ),
inference(consistent_polarity_flipping,[],[f248]) ).
fof(f575,plain,
( c3_1(a1691)
| ~ hskp26 ),
inference(consistent_polarity_flipping,[],[f254]) ).
fof(f576,plain,
( c1_1(a1691)
| ~ hskp26 ),
inference(consistent_polarity_flipping,[],[f255]) ).
fof(f593,plain,
( ~ c0_1(a1678)
| hskp17 ),
inference(consistent_polarity_flipping,[],[f275]) ).
fof(f594,plain,
( c1_1(a1678)
| hskp17 ),
inference(consistent_polarity_flipping,[],[f276]) ).
fof(f595,plain,
( ~ c2_1(a1678)
| hskp17 ),
inference(consistent_polarity_flipping,[],[f277]) ).
fof(f596,plain,
( c1_1(a1677)
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f280]) ).
fof(f600,plain,
( c1_1(a1667)
| ~ hskp13 ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f601,plain,
( c1_1(a1666)
| hskp12 ),
inference(consistent_polarity_flipping,[],[f285]) ).
fof(f605,plain,
( c3_1(a1660)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f292]) ).
fof(f606,plain,
( ~ c0_1(a1660)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f293]) ).
fof(f607,plain,
( c1_1(a1660)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f294]) ).
fof(f610,plain,
( ~ c2_1(a1655)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f297]) ).
fof(f611,plain,
( c1_1(a1650)
| ~ hskp6 ),
inference(consistent_polarity_flipping,[],[f298]) ).
fof(f612,plain,
( c3_1(a1650)
| ~ hskp6 ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f614,plain,
( c1_1(a1646)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f305]) ).
fof(f615,plain,
( ~ c2_1(a1646)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f306]) ).
fof(f616,plain,
( c1_1(a1645)
| ~ hskp2 ),
inference(consistent_polarity_flipping,[],[f307]) ).
fof(f617,plain,
( c3_1(a1645)
| ~ hskp2 ),
inference(consistent_polarity_flipping,[],[f309]) ).
fof(f620,plain,
! [X0] :
( ndr1_0
| ~ c3_1(X0)
| c0_1(X0)
| c2_1(X0)
| hskp37
| ~ hskp72 ),
inference(consistent_polarity_flipping,[],[f314]) ).
fof(f622,plain,
! [X0] :
( ~ c0_1(X0)
| ndr1_0
| ~ c1_1(X0)
| c2_1(X0)
| hskp58
| ~ hskp59 ),
inference(consistent_polarity_flipping,[],[f316]) ).
fof(f629,plain,
! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| c2_1(X0)
| ~ hskp48
| hskp6 ),
inference(consistent_polarity_flipping,[],[f323]) ).
fof(f630,plain,
! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ndr1_0
| ~ c3_1(X0)
| ~ hskp52
| ~ hskp7 ),
inference(consistent_polarity_flipping,[],[f324]) ).
fof(f631,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c3_1(X0)
| ~ hskp9
| hskp55 ),
inference(consistent_polarity_flipping,[],[f325]) ).
fof(f634,plain,
! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c1_1(X0)
| hskp16
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f328]) ).
fof(f638,plain,
! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ndr1_0
| ~ hskp12
| hskp13 ),
inference(consistent_polarity_flipping,[],[f332]) ).
fof(f639,plain,
! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ndr1_0
| ~ hskp74
| hskp38 ),
inference(consistent_polarity_flipping,[],[f333]) ).
fof(f643,plain,
! [X0,X1] :
( ~ c2_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X1)
| ~ c1_1(X1)
| hskp60 ),
inference(consistent_polarity_flipping,[],[f337]) ).
fof(f652,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c1_1(X0)
| c0_1(X1)
| ~ c1_1(X1)
| hskp29 ),
inference(consistent_polarity_flipping,[],[f346]) ).
fof(f653,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ c3_1(X0)
| c2_1(X1)
| hskp61 ),
inference(consistent_polarity_flipping,[],[f347]) ).
fof(f655,plain,
! [X0,X1] :
( c3_1(X0)
| ~ c0_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X0)
| ~ c1_1(X1)
| hskp67 ),
inference(consistent_polarity_flipping,[],[f349]) ).
fof(f657,plain,
! [X0,X1] :
( c3_1(X0)
| ~ c2_1(X0)
| ndr1_0
| c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| c0_1(X1)
| ~ hskp73 ),
inference(consistent_polarity_flipping,[],[f351]) ).
fof(f658,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| hskp47 ),
inference(consistent_polarity_flipping,[],[f352]) ).
fof(f659,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| hskp39 ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f660,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c1_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| hskp40 ),
inference(consistent_polarity_flipping,[],[f354]) ).
fof(f661,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c1_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1)
| ~ hskp63 ),
inference(consistent_polarity_flipping,[],[f355]) ).
fof(f662,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c3_1(X0)
| ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X0)
| hskp26 ),
inference(consistent_polarity_flipping,[],[f356]) ).
fof(f663,plain,
! [X0,X1] :
( c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| hskp13 ),
inference(consistent_polarity_flipping,[],[f357]) ).
fof(f665,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X2)
| ~ c1_1(X2)
| ~ c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f359]) ).
fof(f667,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0)
| ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1)
| c2_1(X2)
| ~ c3_1(X2)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f361]) ).
fof(f668,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c3_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c2_1(X2)
| c3_1(X2)
| c2_1(X0)
| c2_1(X1)
| c0_1(X1)
| ~ c1_1(X2) ),
inference(consistent_polarity_flipping,[],[f362]) ).
fof(f669,plain,
! [X2,X0,X1] :
( c3_1(X0)
| ndr1_0
| ~ c0_1(X1)
| c3_1(X1)
| c1_1(X2)
| ~ c2_1(X2)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X1)
| ~ c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f363]) ).
fof(f670,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ndr1_0
| c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| c3_1(X2)
| c2_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X2)
| c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f364]) ).
fof(f672,definition,
( spl0_1
<=> ! [X2] :
( c3_1(X2)
| c2_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f673,plain,
( ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c3_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f675,definition,
( spl0_2
<=> ! [X1] :
( c3_1(X1)
| c1_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f676,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f678,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f682,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f683,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f684,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f670,f682,f678,f675,f672]) ).
fof(f686,definition,
( spl0_5
<=> ! [X2] :
( c1_1(X2)
| ~ c3_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f687,plain,
( ! [X2] :
( c1_1(X2)
| ~ c3_1(X2)
| ~ c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f689,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f690,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f692,definition,
( spl0_7
<=> ! [X0] :
( c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f693,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f694,plain,
( spl0_5
| spl0_6
| spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f669,f692,f678,f689,f686]) ).
fof(f696,definition,
( spl0_8
<=> ! [X2] :
( ~ c2_1(X2)
| ~ c1_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f697,plain,
( ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| c3_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f699,definition,
( spl0_9
<=> ! [X1] :
( c3_1(X1)
| c0_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f700,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1)
| c3_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f702,definition,
( spl0_10
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f703,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f704,plain,
( spl0_8
| spl0_9
| spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f668,f702,f678,f699,f696]) ).
fof(f706,definition,
( spl0_11
<=> ! [X2] :
( c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f707,plain,
( ! [X2] :
( c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f709,definition,
( spl0_12
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f710,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f712,definition,
( spl0_13
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f713,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f714,plain,
( spl0_11
| spl0_12
| spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f667,f712,f678,f709,f706]) ).
fof(f720,definition,
( spl0_15
<=> ! [X2] :
( c2_1(X2)
| ~ c3_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f721,plain,
( ! [X2] :
( ~ c1_1(X2)
| ~ c3_1(X2)
| c2_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f723,definition,
( spl0_16
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f724,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,definition,
( spl0_17
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f727,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f728,plain,
( spl0_15
| spl0_16
| spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f665,f726,f678,f723,f720]) ).
fof(f737,definition,
( spl0_20
<=> ! [X0] :
( c1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f738,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f741,definition,
( spl0_21
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f744,plain,
( spl0_21
| spl0_20
| spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f663,f675,f678,f737,f741]) ).
fof(f746,definition,
( spl0_22
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f749,plain,
( spl0_22
| spl0_13
| spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f662,f696,f678,f712,f746]) ).
fof(f751,definition,
( spl0_23
<=> hskp63 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f755,definition,
( spl0_24
<=> ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f756,plain,
( ! [X0] :
( c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( ~ spl0_23
| spl0_6
| spl0_3
| spl0_24 ),
inference(avatar_split_clause,[],[f661,f755,f678,f689,f751]) ).
fof(f759,definition,
( spl0_25
<=> hskp40 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f763,definition,
( spl0_26
<=> ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f764,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f765,plain,
( spl0_25
| spl0_26
| spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f660,f675,f678,f763,f759]) ).
fof(f767,definition,
( spl0_27
<=> hskp39 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f771,definition,
( spl0_28
<=> ! [X1] :
( c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f772,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f773,plain,
( spl0_27
| spl0_28
| spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f659,f702,f678,f771,f767]) ).
fof(f775,definition,
( spl0_29
<=> hskp47 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f779,definition,
( spl0_30
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f780,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( spl0_29
| spl0_2
| spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f658,f779,f678,f675,f775]) ).
fof(f783,definition,
( spl0_31
<=> hskp73 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f787,definition,
( spl0_32
<=> ! [X1] :
( c1_1(X1)
| c0_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f788,plain,
( ! [X1] :
( c1_1(X1)
| c0_1(X1)
| c3_1(X1) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f789,plain,
( ~ spl0_31
| spl0_32
| spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f657,f696,f678,f787,f783]) ).
fof(f796,definition,
( spl0_34
<=> hskp67 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f799,plain,
( spl0_34
| spl0_8
| spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f655,f689,f678,f696,f796]) ).
fof(f806,definition,
( spl0_36
<=> hskp61 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f810,definition,
( spl0_37
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f811,plain,
( ! [X1] :
( c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f810]) ).
fof(f812,plain,
( spl0_36
| spl0_37
| spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f653,f779,f678,f810,f806]) ).
fof(f814,definition,
( spl0_38
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f817,plain,
( spl0_38
| spl0_7
| spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f652,f689,f678,f692,f814]) ).
fof(f824,definition,
( spl0_40
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f874,definition,
( spl0_52
<=> hskp60 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f877,plain,
( spl0_52
| spl0_7
| spl0_3
| spl0_26 ),
inference(avatar_split_clause,[],[f643,f763,f678,f692,f874]) ).
fof(f897,definition,
( spl0_57
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f901,definition,
( spl0_58
<=> hskp74 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f904,plain,
( spl0_57
| ~ spl0_58
| spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f639,f712,f678,f901,f897]) ).
fof(f906,definition,
( spl0_59
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f909,plain,
( spl0_21
| ~ spl0_59
| spl0_3
| spl0_24 ),
inference(avatar_split_clause,[],[f638,f755,f678,f906,f741]) ).
fof(f934,definition,
( spl0_65
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f938,definition,
( spl0_66
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f941,plain,
( ~ spl0_65
| spl0_66
| spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f634,f689,f678,f938,f934]) ).
fof(f953,definition,
( spl0_69
<=> hskp55 ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f957,definition,
( spl0_70
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f960,plain,
( spl0_69
| ~ spl0_70
| spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f631,f726,f678,f957,f953]) ).
fof(f962,definition,
( spl0_71
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f966,definition,
( spl0_72
<=> hskp52 ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f969,plain,
( ~ spl0_71
| ~ spl0_72
| spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f630,f726,f678,f966,f962]) ).
fof(f971,definition,
( spl0_73
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f975,definition,
( spl0_74
<=> hskp48 ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f978,plain,
( spl0_73
| ~ spl0_74
| spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f629,f702,f678,f975,f971]) ).
fof(f1018,definition,
( spl0_83
<=> hskp59 ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f1022,definition,
( spl0_84
<=> hskp58 ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f1025,plain,
( ~ spl0_83
| spl0_84
| spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f622,f682,f678,f1022,f1018]) ).
fof(f1036,definition,
( spl0_87
<=> hskp72 ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f1040,definition,
( spl0_88
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f1043,plain,
( ~ spl0_87
| spl0_88
| spl0_11
| spl0_3 ),
inference(avatar_split_clause,[],[f620,f678,f706,f1040,f1036]) ).
fof(f1069,definition,
( spl0_94
<=> c3_1(a1645) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f1072,plain,
( ~ spl0_40
| spl0_94 ),
inference(avatar_split_clause,[],[f617,f1069,f824]) ).
fof(f1074,definition,
( spl0_95
<=> c0_1(a1645) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f1077,plain,
( ~ spl0_40
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f308,f1074,f824]) ).
fof(f1079,definition,
( spl0_96
<=> c1_1(a1645) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f1081,plain,
( c1_1(a1645)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1082,plain,
( ~ spl0_40
| spl0_96 ),
inference(avatar_split_clause,[],[f616,f1079,f824]) ).
fof(f1084,definition,
( spl0_97
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f1088,definition,
( spl0_98
<=> c2_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f1091,plain,
( spl0_97
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f615,f1088,f1084]) ).
fof(f1093,definition,
( spl0_99
<=> c1_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f1095,plain,
( c1_1(a1646)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1096,plain,
( spl0_97
| spl0_99 ),
inference(avatar_split_clause,[],[f614,f1093,f1084]) ).
fof(f1118,definition,
( spl0_104
<=> c3_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f1121,plain,
( ~ spl0_73
| spl0_104 ),
inference(avatar_split_clause,[],[f612,f1118,f971]) ).
fof(f1123,definition,
( spl0_105
<=> c2_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f1126,plain,
( ~ spl0_73
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f299,f1123,f971]) ).
fof(f1128,definition,
( spl0_106
<=> c1_1(a1650) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f1130,plain,
( c1_1(a1650)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f1128]) ).
fof(f1131,plain,
( ~ spl0_73
| spl0_106 ),
inference(avatar_split_clause,[],[f611,f1128,f971]) ).
fof(f1133,definition,
( spl0_107
<=> c2_1(a1655) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f1135,plain,
( ~ c2_1(a1655)
| spl0_107 ),
inference(avatar_component_clause,[],[f1133]) ).
fof(f1136,plain,
( spl0_71
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f610,f1133,f962]) ).
fof(f1152,definition,
( spl0_111
<=> c1_1(a1660) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f1154,plain,
( c1_1(a1660)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f1152]) ).
fof(f1155,plain,
( spl0_70
| spl0_111 ),
inference(avatar_split_clause,[],[f607,f1152,f957]) ).
fof(f1157,definition,
( spl0_112
<=> c0_1(a1660) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f1160,plain,
( spl0_70
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f606,f1157,f957]) ).
fof(f1162,definition,
( spl0_113
<=> c3_1(a1660) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f1165,plain,
( spl0_70
| spl0_113 ),
inference(avatar_split_clause,[],[f605,f1162,f957]) ).
fof(f1197,definition,
( spl0_120
<=> c1_1(a1666) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1199,plain,
( c1_1(a1666)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f1197]) ).
fof(f1200,plain,
( spl0_59
| spl0_120 ),
inference(avatar_split_clause,[],[f601,f1197,f906]) ).
fof(f1202,definition,
( spl0_121
<=> c1_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1204,plain,
( c1_1(a1667)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1205,plain,
( ~ spl0_21
| spl0_121 ),
inference(avatar_split_clause,[],[f600,f1202,f741]) ).
fof(f1230,definition,
( spl0_127
<=> c1_1(a1677) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f1232,plain,
( c1_1(a1677)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f1230]) ).
fof(f1233,plain,
( ~ spl0_66
| spl0_127 ),
inference(avatar_split_clause,[],[f596,f1230,f938]) ).
fof(f1235,definition,
( spl0_128
<=> c2_1(a1677) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f1237,plain,
( ~ c2_1(a1677)
| spl0_128 ),
inference(avatar_component_clause,[],[f1235]) ).
fof(f1238,plain,
( ~ spl0_66
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f279,f1235,f938]) ).
fof(f1240,definition,
( spl0_129
<=> c0_1(a1677) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f1243,plain,
( ~ spl0_66
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f278,f1240,f938]) ).
fof(f1245,definition,
( spl0_130
<=> c2_1(a1678) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f1247,plain,
( ~ c2_1(a1678)
| spl0_130 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1248,plain,
( spl0_65
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f595,f1245,f934]) ).
fof(f1250,definition,
( spl0_131
<=> c1_1(a1678) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1252,plain,
( c1_1(a1678)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f1250]) ).
fof(f1253,plain,
( spl0_65
| spl0_131 ),
inference(avatar_split_clause,[],[f594,f1250,f934]) ).
fof(f1255,definition,
( spl0_132
<=> c0_1(a1678) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1258,plain,
( spl0_65
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f593,f1255,f934]) ).
fof(f1320,definition,
( spl0_145
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1354,definition,
( spl0_152
<=> c2_1(a1691) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1356,plain,
( ~ c2_1(a1691)
| spl0_152 ),
inference(avatar_component_clause,[],[f1354]) ).
fof(f1357,plain,
( ~ spl0_22
| ~ spl0_152 ),
inference(avatar_split_clause,[],[f256,f1354,f746]) ).
fof(f1359,definition,
( spl0_153
<=> c1_1(a1691) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1361,plain,
( c1_1(a1691)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f1359]) ).
fof(f1362,plain,
( ~ spl0_22
| spl0_153 ),
inference(avatar_split_clause,[],[f576,f1359,f746]) ).
fof(f1364,definition,
( spl0_154
<=> c3_1(a1691) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1367,plain,
( ~ spl0_22
| spl0_154 ),
inference(avatar_split_clause,[],[f575,f1364,f746]) ).
fof(f1402,definition,
( spl0_162
<=> c3_1(a1695) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1405,plain,
( ~ spl0_38
| spl0_162 ),
inference(avatar_split_clause,[],[f569,f1402,f814]) ).
fof(f1485,definition,
( spl0_179
<=> c1_1(a1714) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1487,plain,
( c1_1(a1714)
| ~ spl0_179 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1488,plain,
( ~ spl0_88
| spl0_179 ),
inference(avatar_split_clause,[],[f558,f1485,f1040]) ).
fof(f1495,definition,
( spl0_181
<=> c2_1(a1718) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1497,plain,
( ~ c2_1(a1718)
| spl0_181 ),
inference(avatar_component_clause,[],[f1495]) ).
fof(f1498,plain,
( ~ spl0_57
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f231,f1495,f897]) ).
fof(f1500,definition,
( spl0_182
<=> c0_1(a1721) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f1503,plain,
( ~ spl0_27
| ~ spl0_182 ),
inference(avatar_split_clause,[],[f230,f1500,f767]) ).
fof(f1505,definition,
( spl0_183
<=> c1_1(a1721) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1507,plain,
( c1_1(a1721)
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1505]) ).
fof(f1508,plain,
( ~ spl0_27
| spl0_183 ),
inference(avatar_split_clause,[],[f557,f1505,f767]) ).
fof(f1510,definition,
( spl0_184
<=> c2_1(a1725) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1512,plain,
( ~ c2_1(a1725)
| spl0_184 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1513,plain,
( ~ spl0_25
| ~ spl0_184 ),
inference(avatar_split_clause,[],[f228,f1510,f759]) ).
fof(f1558,definition,
( spl0_194
<=> c0_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_194])],[avatar_definition]) ).
fof(f1561,plain,
( ~ spl0_29
| ~ spl0_194 ),
inference(avatar_split_clause,[],[f220,f1558,f775]) ).
fof(f1563,definition,
( spl0_195
<=> c1_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_195])],[avatar_definition]) ).
fof(f1565,plain,
( c1_1(a1644)
| ~ spl0_195 ),
inference(avatar_component_clause,[],[f1563]) ).
fof(f1566,plain,
( ~ spl0_29
| spl0_195 ),
inference(avatar_split_clause,[],[f549,f1563,f775]) ).
fof(f1568,definition,
( spl0_196
<=> c2_1(a1649) ),
introduced(definition,[new_symbols(definition,[spl0_196])],[avatar_definition]) ).
fof(f1570,plain,
( ~ c2_1(a1649)
| spl0_196 ),
inference(avatar_component_clause,[],[f1568]) ).
fof(f1571,plain,
( spl0_74
| ~ spl0_196 ),
inference(avatar_split_clause,[],[f548,f1568,f975]) ).
fof(f1573,definition,
( spl0_197
<=> c3_1(a1649) ),
introduced(definition,[new_symbols(definition,[spl0_197])],[avatar_definition]) ).
fof(f1576,plain,
( spl0_74
| spl0_197 ),
inference(avatar_split_clause,[],[f547,f1573,f975]) ).
fof(f1588,definition,
( spl0_200
<=> hskp53 ),
introduced(definition,[new_symbols(definition,[spl0_200])],[avatar_definition]) ).
fof(f1592,definition,
( spl0_201
<=> c3_1(a1656) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f1595,plain,
( ~ spl0_200
| spl0_201 ),
inference(avatar_split_clause,[],[f546,f1592,f1588]) ).
fof(f1606,definition,
( spl0_204
<=> c3_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f1609,plain,
( ~ spl0_69
| spl0_204 ),
inference(avatar_split_clause,[],[f545,f1606,f953]) ).
fof(f1611,definition,
( spl0_205
<=> c2_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1613,plain,
( ~ c2_1(a1661)
| spl0_205 ),
inference(avatar_component_clause,[],[f1611]) ).
fof(f1614,plain,
( ~ spl0_69
| ~ spl0_205 ),
inference(avatar_split_clause,[],[f211,f1611,f953]) ).
fof(f1626,definition,
( spl0_208
<=> c1_1(a1668) ),
introduced(definition,[new_symbols(definition,[spl0_208])],[avatar_definition]) ).
fof(f1628,plain,
( c1_1(a1668)
| ~ spl0_208 ),
inference(avatar_component_clause,[],[f1626]) ).
fof(f1629,plain,
( ~ spl0_84
| spl0_208 ),
inference(avatar_split_clause,[],[f542,f1626,f1022]) ).
fof(f1631,definition,
( spl0_209
<=> c0_1(a1668) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f1634,plain,
( ~ spl0_84
| ~ spl0_209 ),
inference(avatar_split_clause,[],[f207,f1631,f1022]) ).
fof(f1636,definition,
( spl0_210
<=> c2_1(a1669) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f1638,plain,
( ~ c2_1(a1669)
| spl0_210 ),
inference(avatar_component_clause,[],[f1636]) ).
fof(f1639,plain,
( spl0_83
| ~ spl0_210 ),
inference(avatar_split_clause,[],[f541,f1636,f1018]) ).
fof(f1641,definition,
( spl0_211
<=> c1_1(a1673) ),
introduced(definition,[new_symbols(definition,[spl0_211])],[avatar_definition]) ).
fof(f1643,plain,
( c1_1(a1673)
| ~ spl0_211 ),
inference(avatar_component_clause,[],[f1641]) ).
fof(f1644,plain,
( ~ spl0_52
| spl0_211 ),
inference(avatar_split_clause,[],[f540,f1641,f874]) ).
fof(f1646,definition,
( spl0_212
<=> c2_1(a1674) ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f1648,plain,
( ~ c2_1(a1674)
| spl0_212 ),
inference(avatar_component_clause,[],[f1646]) ).
fof(f1649,plain,
( ~ spl0_36
| ~ spl0_212 ),
inference(avatar_split_clause,[],[f204,f1646,f806]) ).
fof(f1651,definition,
( spl0_213
<=> c1_1(a1674) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1653,plain,
( c1_1(a1674)
| ~ spl0_213 ),
inference(avatar_component_clause,[],[f1651]) ).
fof(f1654,plain,
( ~ spl0_36
| spl0_213 ),
inference(avatar_split_clause,[],[f539,f1651,f806]) ).
fof(f1661,definition,
( spl0_215
<=> c0_1(a1676) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1664,plain,
( spl0_23
| ~ spl0_215 ),
inference(avatar_split_clause,[],[f537,f1661,f751]) ).
fof(f1666,definition,
( spl0_216
<=> hskp64 ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1680,definition,
( spl0_219
<=> hskp65 ),
introduced(definition,[new_symbols(definition,[spl0_219])],[avatar_definition]) ).
fof(f1733,definition,
( spl0_230
<=> c2_1(a1715) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1735,plain,
( ~ c2_1(a1715)
| spl0_230 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1736,plain,
( spl0_87
| ~ spl0_230 ),
inference(avatar_split_clause,[],[f526,f1733,f1036]) ).
fof(f1738,definition,
( spl0_231
<=> c3_1(a1716) ),
introduced(definition,[new_symbols(definition,[spl0_231])],[avatar_definition]) ).
fof(f1741,plain,
( spl0_31
| spl0_231 ),
inference(avatar_split_clause,[],[f525,f1738,f783]) ).
fof(f1743,definition,
( spl0_232
<=> c3_1(a1717) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f1746,plain,
( spl0_58
| spl0_232 ),
inference(avatar_split_clause,[],[f524,f1743,f901]) ).
fof(f1768,definition,
( spl0_237
<=> c0_1(a1646) ),
introduced(definition,[new_symbols(definition,[spl0_237])],[avatar_definition]) ).
fof(f1771,plain,
( spl0_237
| spl0_97 ),
inference(avatar_split_clause,[],[f520,f1084,f1768]) ).
fof(f1783,definition,
( spl0_240
<=> c0_1(a1655) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1786,plain,
( spl0_240
| spl0_71 ),
inference(avatar_split_clause,[],[f517,f962,f1783]) ).
fof(f1788,definition,
( spl0_241
<=> c3_1(a1655) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1790,plain,
( ~ c3_1(a1655)
| spl0_241 ),
inference(avatar_component_clause,[],[f1788]) ).
fof(f1791,plain,
( ~ spl0_241
| spl0_71 ),
inference(avatar_split_clause,[],[f516,f962,f1788]) ).
fof(f1798,definition,
( spl0_243
<=> c3_1(a1666) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f1801,plain,
( ~ spl0_243
| spl0_59 ),
inference(avatar_split_clause,[],[f514,f906,f1798]) ).
fof(f1803,definition,
( spl0_244
<=> c2_1(a1666) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f1806,plain,
( spl0_244
| spl0_59 ),
inference(avatar_split_clause,[],[f513,f906,f1803]) ).
fof(f1808,definition,
( spl0_245
<=> c3_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f1811,plain,
( ~ spl0_245
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f512,f741,f1808]) ).
fof(f1813,definition,
( spl0_246
<=> c0_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_246])],[avatar_definition]) ).
fof(f1816,plain,
( spl0_246
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f173,f741,f1813]) ).
fof(f1868,definition,
( spl0_257
<=> c0_1(a1695) ),
introduced(definition,[new_symbols(definition,[spl0_257])],[avatar_definition]) ).
fof(f1871,plain,
( spl0_257
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f162,f814,f1868]) ).
fof(f1873,definition,
( spl0_258
<=> c2_1(a1695) ),
introduced(definition,[new_symbols(definition,[spl0_258])],[avatar_definition]) ).
fof(f1875,plain,
( c2_1(a1695)
| ~ spl0_258 ),
inference(avatar_component_clause,[],[f1873]) ).
fof(f1876,plain,
( spl0_258
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f161,f814,f1873]) ).
fof(f1913,definition,
( spl0_266
<=> c0_1(a1714) ),
introduced(definition,[new_symbols(definition,[spl0_266])],[avatar_definition]) ).
fof(f1916,plain,
( spl0_266
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f153,f1040,f1913]) ).
fof(f1918,definition,
( spl0_267
<=> c2_1(a1714) ),
introduced(definition,[new_symbols(definition,[spl0_267])],[avatar_definition]) ).
fof(f1921,plain,
( spl0_267
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f152,f1040,f1918]) ).
fof(f1923,definition,
( spl0_268
<=> c3_1(a1718) ),
introduced(definition,[new_symbols(definition,[spl0_268])],[avatar_definition]) ).
fof(f1926,plain,
( ~ spl0_268
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f498,f897,f1923]) ).
fof(f1928,definition,
( spl0_269
<=> c3_1(a1721) ),
introduced(definition,[new_symbols(definition,[spl0_269])],[avatar_definition]) ).
fof(f1931,plain,
( ~ spl0_269
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f497,f767,f1928]) ).
fof(f1933,definition,
( spl0_270
<=> c3_1(a1725) ),
introduced(definition,[new_symbols(definition,[spl0_270])],[avatar_definition]) ).
fof(f1936,plain,
( ~ spl0_270
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f496,f759,f1933]) ).
fof(f1938,definition,
( spl0_271
<=> c1_1(a1725) ),
introduced(definition,[new_symbols(definition,[spl0_271])],[avatar_definition]) ).
fof(f1940,plain,
( ~ c1_1(a1725)
| spl0_271 ),
inference(avatar_component_clause,[],[f1938]) ).
fof(f1941,plain,
( ~ spl0_271
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f495,f759,f1938]) ).
fof(f2002,definition,
( spl0_284
<=> c3_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_284])],[avatar_definition]) ).
fof(f2005,plain,
( ~ spl0_284
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f489,f775,f2002]) ).
fof(f2007,definition,
( spl0_285
<=> c0_1(a1649) ),
introduced(definition,[new_symbols(definition,[spl0_285])],[avatar_definition]) ).
fof(f2010,plain,
( spl0_285
| spl0_74 ),
inference(avatar_split_clause,[],[f488,f975,f2007]) ).
fof(f2047,definition,
( spl0_293
<=> c3_1(a1654) ),
introduced(definition,[new_symbols(definition,[spl0_293])],[avatar_definition]) ).
fof(f2049,plain,
( ~ c3_1(a1654)
| spl0_293 ),
inference(avatar_component_clause,[],[f2047]) ).
fof(f2050,plain,
( ~ spl0_293
| spl0_72 ),
inference(avatar_split_clause,[],[f481,f966,f2047]) ).
fof(f2052,definition,
( spl0_294
<=> c2_1(a1654) ),
introduced(definition,[new_symbols(definition,[spl0_294])],[avatar_definition]) ).
fof(f2054,plain,
( c2_1(a1654)
| ~ spl0_294 ),
inference(avatar_component_clause,[],[f2052]) ).
fof(f2055,plain,
( spl0_294
| spl0_72 ),
inference(avatar_split_clause,[],[f480,f966,f2052]) ).
fof(f2057,definition,
( spl0_295
<=> c0_1(a1654) ),
introduced(definition,[new_symbols(definition,[spl0_295])],[avatar_definition]) ).
fof(f2060,plain,
( spl0_295
| spl0_72 ),
inference(avatar_split_clause,[],[f479,f966,f2057]) ).
fof(f2062,definition,
( spl0_296
<=> c0_1(a1656) ),
introduced(definition,[new_symbols(definition,[spl0_296])],[avatar_definition]) ).
fof(f2065,plain,
( spl0_296
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f124,f1588,f2062]) ).
fof(f2067,definition,
( spl0_297
<=> c2_1(a1656) ),
introduced(definition,[new_symbols(definition,[spl0_297])],[avatar_definition]) ).
fof(f2069,plain,
( c2_1(a1656)
| ~ spl0_297 ),
inference(avatar_component_clause,[],[f2067]) ).
fof(f2070,plain,
( spl0_297
| ~ spl0_200 ),
inference(avatar_split_clause,[],[f123,f1588,f2067]) ).
fof(f2082,definition,
( spl0_300
<=> c1_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_300])],[avatar_definition]) ).
fof(f2084,plain,
( ~ c1_1(a1661)
| spl0_300 ),
inference(avatar_component_clause,[],[f2082]) ).
fof(f2085,plain,
( ~ spl0_300
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f476,f953,f2082]) ).
fof(f2107,definition,
( spl0_305
<=> c3_1(a1668) ),
introduced(definition,[new_symbols(definition,[spl0_305])],[avatar_definition]) ).
fof(f2110,plain,
( ~ spl0_305
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f471,f1022,f2107]) ).
fof(f2112,definition,
( spl0_306
<=> c0_1(a1669) ),
introduced(definition,[new_symbols(definition,[spl0_306])],[avatar_definition]) ).
fof(f2115,plain,
( spl0_306
| spl0_83 ),
inference(avatar_split_clause,[],[f470,f1018,f2112]) ).
fof(f2117,definition,
( spl0_307
<=> c3_1(a1669) ),
introduced(definition,[new_symbols(definition,[spl0_307])],[avatar_definition]) ).
fof(f2120,plain,
( ~ spl0_307
| spl0_83 ),
inference(avatar_split_clause,[],[f469,f1018,f2117]) ).
fof(f2122,definition,
( spl0_308
<=> c2_1(a1673) ),
introduced(definition,[new_symbols(definition,[spl0_308])],[avatar_definition]) ).
fof(f2125,plain,
( spl0_308
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f112,f874,f2122]) ).
fof(f2127,definition,
( spl0_309
<=> c3_1(a1673) ),
introduced(definition,[new_symbols(definition,[spl0_309])],[avatar_definition]) ).
fof(f2130,plain,
( ~ spl0_309
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f468,f874,f2127]) ).
fof(f2132,definition,
( spl0_310
<=> c3_1(a1674) ),
introduced(definition,[new_symbols(definition,[spl0_310])],[avatar_definition]) ).
fof(f2135,plain,
( ~ spl0_310
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f467,f806,f2132]) ).
fof(f2147,definition,
( spl0_313
<=> c3_1(a1676) ),
introduced(definition,[new_symbols(definition,[spl0_313])],[avatar_definition]) ).
fof(f2150,plain,
( ~ spl0_313
| spl0_23 ),
inference(avatar_split_clause,[],[f465,f751,f2147]) ).
fof(f2152,definition,
( spl0_314
<=> c2_1(a1676) ),
introduced(definition,[new_symbols(definition,[spl0_314])],[avatar_definition]) ).
fof(f2154,plain,
( c2_1(a1676)
| ~ spl0_314 ),
inference(avatar_component_clause,[],[f2152]) ).
fof(f2155,plain,
( spl0_314
| spl0_23 ),
inference(avatar_split_clause,[],[f464,f751,f2152]) ).
fof(f2172,definition,
( spl0_318
<=> c3_1(a1702) ),
introduced(definition,[new_symbols(definition,[spl0_318])],[avatar_definition]) ).
fof(f2174,plain,
( ~ c3_1(a1702)
| spl0_318 ),
inference(avatar_component_clause,[],[f2172]) ).
fof(f2175,plain,
( ~ spl0_318
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f462,f796,f2172]) ).
fof(f2177,definition,
( spl0_319
<=> c2_1(a1702) ),
introduced(definition,[new_symbols(definition,[spl0_319])],[avatar_definition]) ).
fof(f2180,plain,
( spl0_319
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f101,f796,f2177]) ).
fof(f2182,definition,
( spl0_320
<=> c1_1(a1702) ),
introduced(definition,[new_symbols(definition,[spl0_320])],[avatar_definition]) ).
fof(f2184,plain,
( ~ c1_1(a1702)
| spl0_320 ),
inference(avatar_component_clause,[],[f2182]) ).
fof(f2185,plain,
( ~ spl0_320
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f461,f796,f2182]) ).
fof(f2222,definition,
( spl0_328
<=> c3_1(a1715) ),
introduced(definition,[new_symbols(definition,[spl0_328])],[avatar_definition]) ).
fof(f2225,plain,
( ~ spl0_328
| spl0_87 ),
inference(avatar_split_clause,[],[f455,f1036,f2222]) ).
fof(f2227,definition,
( spl0_329
<=> c1_1(a1715) ),
introduced(definition,[new_symbols(definition,[spl0_329])],[avatar_definition]) ).
fof(f2229,plain,
( ~ c1_1(a1715)
| spl0_329 ),
inference(avatar_component_clause,[],[f2227]) ).
fof(f2230,plain,
( ~ spl0_329
| spl0_87 ),
inference(avatar_split_clause,[],[f454,f1036,f2227]) ).
fof(f2232,definition,
( spl0_330
<=> c0_1(a1716) ),
introduced(definition,[new_symbols(definition,[spl0_330])],[avatar_definition]) ).
fof(f2235,plain,
( spl0_330
| spl0_31 ),
inference(avatar_split_clause,[],[f453,f783,f2232]) ).
fof(f2237,definition,
( spl0_331
<=> c2_1(a1716) ),
introduced(definition,[new_symbols(definition,[spl0_331])],[avatar_definition]) ).
fof(f2239,plain,
( c2_1(a1716)
| ~ spl0_331 ),
inference(avatar_component_clause,[],[f2237]) ).
fof(f2240,plain,
( spl0_331
| spl0_31 ),
inference(avatar_split_clause,[],[f452,f783,f2237]) ).
fof(f2242,definition,
( spl0_332
<=> c2_1(a1717) ),
introduced(definition,[new_symbols(definition,[spl0_332])],[avatar_definition]) ).
fof(f2244,plain,
( c2_1(a1717)
| ~ spl0_332 ),
inference(avatar_component_clause,[],[f2242]) ).
fof(f2245,plain,
( spl0_332
| spl0_58 ),
inference(avatar_split_clause,[],[f451,f901,f2242]) ).
fof(f2247,definition,
( spl0_333
<=> c0_1(a1717) ),
introduced(definition,[new_symbols(definition,[spl0_333])],[avatar_definition]) ).
fof(f2250,plain,
( spl0_333
| spl0_58 ),
inference(avatar_split_clause,[],[f450,f901,f2247]) ).
fof(f2262,plain,
( spl0_200
| ~ spl0_72
| spl0_38 ),
inference(avatar_split_clause,[],[f446,f814,f966,f1588]) ).
fof(f2264,plain,
( spl0_219
| spl0_216
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f444,f1320,f1666,f1680]) ).
fof(f2267,plain,
( ~ spl0_97
| spl0_40
| spl0_29 ),
inference(avatar_split_clause,[],[f441,f775,f824,f1084]) ).
fof(f2292,plain,
( ~ spl0_3
| spl0_145 ),
inference(avatar_split_clause,[],[f417,f1320,f678]) ).
fof(f2333,plain,
( ~ spl0_3
| ~ spl0_216 ),
inference(avatar_split_clause,[],[f376,f1666,f678]) ).
fof(f2334,plain,
( ~ spl0_3
| ~ spl0_219 ),
inference(avatar_split_clause,[],[f375,f1680,f678]) ).
fof(f2420,definition,
( spl0_340
<=> c0_1(a1691) ),
introduced(definition,[new_symbols(definition,[spl0_340])],[avatar_definition]) ).
fof(f2455,definition,
( spl0_347
<=> c0_1(a1725) ),
introduced(definition,[new_symbols(definition,[spl0_347])],[avatar_definition]) ).
fof(f2475,definition,
( spl0_351
<=> c0_1(a1661) ),
introduced(definition,[new_symbols(definition,[spl0_351])],[avatar_definition]) ).
fof(f2485,definition,
( spl0_353
<=> c0_1(a1674) ),
introduced(definition,[new_symbols(definition,[spl0_353])],[avatar_definition]) ).
fof(f2490,definition,
( spl0_354
<=> c0_1(a1702) ),
introduced(definition,[new_symbols(definition,[spl0_354])],[avatar_definition]) ).
fof(f2495,definition,
( spl0_355
<=> c0_1(a1715) ),
introduced(definition,[new_symbols(definition,[spl0_355])],[avatar_definition]) ).
fof(f2560,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(resolution,[],[f690,f676]) ).
fof(f2564,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_6 ),
inference(duplicate_literal_removal,[],[f2560]) ).
fof(f2593,plain,
( ~ c0_1(a1654)
| ~ spl0_2
| ~ spl0_6
| spl0_293 ),
inference(resolution,[],[f2564,f2049]) ).
fof(f2617,plain,
( ~ c0_1(a1655)
| ~ spl0_2
| ~ spl0_6
| spl0_241 ),
inference(resolution,[],[f2564,f1790]) ).
fof(f2647,plain,
( ~ c0_1(a1674)
| c3_1(a1674)
| ~ spl0_10
| spl0_212 ),
inference(resolution,[],[f703,f1648]) ).
fof(f2649,plain,
( ~ c0_1(a1669)
| c3_1(a1669)
| ~ spl0_10
| spl0_210 ),
inference(resolution,[],[f703,f1638]) ).
fof(f2673,plain,
( ~ c0_1(a1655)
| c3_1(a1655)
| ~ spl0_10
| spl0_107 ),
inference(resolution,[],[f703,f1135]) ).
fof(f2730,plain,
( c0_1(a1691)
| ~ c3_1(a1691)
| ~ spl0_11
| spl0_152 ),
inference(resolution,[],[f707,f1356]) ).
fof(f2739,definition,
( spl0_358
<=> c3_1(a1677) ),
introduced(definition,[new_symbols(definition,[spl0_358])],[avatar_definition]) ).
fof(f2744,definition,
( spl0_359
<=> c3_1(a1678) ),
introduced(definition,[new_symbols(definition,[spl0_359])],[avatar_definition]) ).
fof(f2780,definition,
( spl0_366
<=> c3_1(a1714) ),
introduced(definition,[new_symbols(definition,[spl0_366])],[avatar_definition]) ).
fof(f2813,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f713,f703]) ).
fof(f2819,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_10
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f2813]) ).
fof(f2829,plain,
( ~ c3_1(a1695)
| ~ c0_1(a1695)
| ~ spl0_17
| ~ spl0_258 ),
inference(resolution,[],[f727,f1875]) ).
fof(f2832,plain,
( ~ spl0_257
| ~ spl0_162
| ~ spl0_17
| ~ spl0_258 ),
inference(avatar_split_clause,[],[f2829,f1873,f726,f1402,f1868]) ).
fof(f2833,plain,
( spl0_241
| ~ spl0_240
| ~ spl0_10
| spl0_107 ),
inference(avatar_split_clause,[],[f2673,f1133,f702,f1783,f1788]) ).
fof(f2848,definition,
( spl0_372
<=> c2_1(a1645) ),
introduced(definition,[new_symbols(definition,[spl0_372])],[avatar_definition]) ).
fof(f2849,plain,
( ~ c2_1(a1645)
| spl0_372 ),
inference(avatar_component_clause,[],[f2848]) ).
fof(f2853,definition,
( spl0_373
<=> c2_1(a1660) ),
introduced(definition,[new_symbols(definition,[spl0_373])],[avatar_definition]) ).
fof(f2854,plain,
( ~ c2_1(a1660)
| spl0_373 ),
inference(avatar_component_clause,[],[f2853]) ).
fof(f2950,plain,
( ~ c0_1(a1702)
| ~ spl0_10
| ~ spl0_13
| spl0_318 ),
inference(resolution,[],[f2819,f2174]) ).
fof(f2965,plain,
( ~ c0_1(a1654)
| ~ spl0_10
| ~ spl0_13
| spl0_293 ),
inference(resolution,[],[f2819,f2049]) ).
fof(f3013,plain,
( ~ spl0_295
| ~ spl0_10
| ~ spl0_13
| spl0_293 ),
inference(avatar_split_clause,[],[f2965,f2047,f712,f702,f2057]) ).
fof(f3019,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_6
| ~ spl0_20 ),
inference(resolution,[],[f738,f690]) ).
fof(f3020,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_4
| ~ spl0_20 ),
inference(resolution,[],[f738,f683]) ).
fof(f3021,plain,
( c2_1(a1715)
| c3_1(a1715)
| ~ spl0_20
| spl0_329 ),
inference(resolution,[],[f738,f2229]) ).
fof(f3045,plain,
( c2_1(a1725)
| c3_1(a1725)
| ~ spl0_20
| spl0_271 ),
inference(resolution,[],[f738,f1940]) ).
fof(f3075,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f3020]) ).
fof(f3076,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_6
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f3019]) ).
fof(f3108,definition,
( spl0_377
<=> c2_1(a1667) ),
introduced(definition,[new_symbols(definition,[spl0_377])],[avatar_definition]) ).
fof(f3143,plain,
( spl0_270
| spl0_184
| ~ spl0_20
| spl0_271 ),
inference(avatar_split_clause,[],[f3045,f1938,f737,f1510,f1933]) ).
fof(f3153,definition,
( spl0_384
<=> c2_1(a1644) ),
introduced(definition,[new_symbols(definition,[spl0_384])],[avatar_definition]) ).
fof(f3205,plain,
( spl0_328
| spl0_230
| ~ spl0_20
| spl0_329 ),
inference(avatar_split_clause,[],[f3021,f2227,f737,f1733,f2222]) ).
fof(f3260,plain,
( c3_1(a1677)
| c0_1(a1677)
| ~ spl0_7
| ~ spl0_127 ),
inference(resolution,[],[f1232,f693]) ).
fof(f3263,plain,
( spl0_129
| spl0_358
| ~ spl0_7
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f3260,f1230,f692,f2739,f1240]) ).
fof(f3300,plain,
( ~ c2_1(a1714)
| c3_1(a1714)
| ~ spl0_8
| ~ spl0_179 ),
inference(resolution,[],[f1487,f697]) ).
fof(f3301,plain,
( ~ c0_1(a1714)
| ~ c2_1(a1714)
| ~ spl0_12
| ~ spl0_179 ),
inference(resolution,[],[f1487,f710]) ).
fof(f3303,plain,
( ~ c0_1(a1714)
| c3_1(a1714)
| ~ spl0_6
| ~ spl0_179 ),
inference(resolution,[],[f1487,f690]) ).
fof(f3305,plain,
( spl0_366
| ~ spl0_266
| ~ spl0_6
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f3303,f1485,f689,f1913,f2780]) ).
fof(f3306,plain,
( ~ spl0_267
| ~ spl0_266
| ~ spl0_12
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f3301,f1485,f709,f1913,f1918]) ).
fof(f3307,plain,
( spl0_366
| ~ spl0_267
| ~ spl0_8
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f3300,f1485,f696,f1918,f2780]) ).
fof(f3411,plain,
( ~ c0_1(a1715)
| c3_1(a1715)
| ~ spl0_10
| spl0_230 ),
inference(resolution,[],[f1735,f703]) ).
fof(f3439,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_20 ),
inference(resolution,[],[f673,f738]) ).
fof(f3445,plain,
( c2_1(a1644)
| c3_1(a1644)
| ~ spl0_1
| ~ spl0_195 ),
inference(resolution,[],[f673,f1565]) ).
fof(f3461,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_20 ),
inference(duplicate_literal_removal,[],[f3439]) ).
fof(f3480,plain,
( ~ c0_1(a1646)
| c2_1(a1646)
| ~ spl0_4
| ~ spl0_99 ),
inference(resolution,[],[f683,f1095]) ).
fof(f3507,plain,
( c3_1(a1718)
| ~ spl0_1
| ~ spl0_20
| spl0_181 ),
inference(resolution,[],[f3461,f1497]) ).
fof(f3526,plain,
( spl0_268
| ~ spl0_1
| ~ spl0_20
| spl0_181 ),
inference(avatar_split_clause,[],[f3507,f1495,f737,f672,f1923]) ).
fof(f3538,plain,
( ~ c0_1(a1691)
| c2_1(a1691)
| ~ spl0_4
| ~ spl0_153 ),
inference(resolution,[],[f1361,f683]) ).
fof(f3594,plain,
( c0_1(a1725)
| c3_1(a1725)
| ~ spl0_9
| spl0_184 ),
inference(resolution,[],[f700,f1512]) ).
fof(f3646,plain,
( c0_1(a1660)
| ~ c3_1(a1660)
| ~ spl0_11
| spl0_373 ),
inference(resolution,[],[f707,f2854]) ).
fof(f3647,plain,
( c0_1(a1645)
| ~ c3_1(a1645)
| ~ spl0_11
| spl0_372 ),
inference(resolution,[],[f707,f2849]) ).
fof(f3648,plain,
( ~ spl0_94
| spl0_95
| ~ spl0_11
| spl0_372 ),
inference(avatar_split_clause,[],[f3647,f2848,f706,f1074,f1069]) ).
fof(f3649,plain,
( ~ spl0_113
| spl0_112
| ~ spl0_11
| spl0_373 ),
inference(avatar_split_clause,[],[f3646,f2853,f706,f1157,f1162]) ).
fof(f3687,plain,
( c0_1(a1677)
| c2_1(a1677)
| ~ spl0_16
| ~ spl0_127 ),
inference(resolution,[],[f724,f1232]) ).
fof(f3694,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_8
| ~ spl0_24 ),
inference(resolution,[],[f756,f697]) ).
fof(f3696,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_6
| ~ spl0_24 ),
inference(resolution,[],[f756,f690]) ).
fof(f3700,plain,
( c3_1(a1702)
| ~ c2_1(a1702)
| ~ spl0_24
| spl0_320 ),
inference(resolution,[],[f756,f2184]) ).
fof(f3732,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_6
| ~ spl0_24 ),
inference(duplicate_literal_removal,[],[f3696]) ).
fof(f3734,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_8
| ~ spl0_24 ),
inference(duplicate_literal_removal,[],[f3694]) ).
fof(f3757,plain,
( ~ spl0_319
| spl0_318
| ~ spl0_24
| spl0_320 ),
inference(avatar_split_clause,[],[f3700,f2182,f755,f2172,f2177]) ).
fof(f3761,plain,
( spl0_13
| ~ spl0_6
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f3732,f755,f689,f712]) ).
fof(f3772,plain,
( spl0_152
| ~ spl0_340
| ~ spl0_4
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f3538,f1359,f682,f2420,f1354]) ).
fof(f3776,plain,
( ~ c0_1(a1667)
| c2_1(a1667)
| ~ spl0_4
| ~ spl0_121 ),
inference(resolution,[],[f1204,f683]) ).
fof(f3778,plain,
( ~ c0_1(a1667)
| c3_1(a1667)
| ~ spl0_6
| ~ spl0_121 ),
inference(resolution,[],[f1204,f690]) ).
fof(f3885,plain,
( ~ spl0_354
| ~ spl0_10
| ~ spl0_13
| spl0_318 ),
inference(avatar_split_clause,[],[f2950,f2172,f712,f702,f2490]) ).
fof(f3981,plain,
( c3_1(a1654)
| ~ spl0_8
| ~ spl0_24
| ~ spl0_294 ),
inference(resolution,[],[f3734,f2054]) ).
fof(f4021,plain,
( spl0_293
| ~ spl0_8
| ~ spl0_24
| ~ spl0_294 ),
inference(avatar_split_clause,[],[f3981,f2052,f755,f696,f2047]) ).
fof(f4043,plain,
( c3_1(a1668)
| c0_1(a1668)
| ~ spl0_7
| ~ spl0_208 ),
inference(resolution,[],[f693,f1628]) ).
fof(f4046,plain,
( c3_1(a1644)
| c0_1(a1644)
| ~ spl0_7
| ~ spl0_195 ),
inference(resolution,[],[f693,f1565]) ).
fof(f4050,plain,
( c3_1(a1721)
| c0_1(a1721)
| ~ spl0_7
| ~ spl0_183 ),
inference(resolution,[],[f693,f1507]) ).
fof(f4100,plain,
( ~ c3_1(a1717)
| ~ c0_1(a1717)
| ~ spl0_17
| ~ spl0_332 ),
inference(resolution,[],[f727,f2244]) ).
fof(f4101,plain,
( ~ c3_1(a1716)
| ~ c0_1(a1716)
| ~ spl0_17
| ~ spl0_331 ),
inference(resolution,[],[f727,f2239]) ).
fof(f4119,plain,
( ~ c3_1(a1656)
| ~ c0_1(a1656)
| ~ spl0_17
| ~ spl0_297 ),
inference(resolution,[],[f727,f2069]) ).
fof(f4163,plain,
( ~ spl0_296
| ~ spl0_201
| ~ spl0_17
| ~ spl0_297 ),
inference(avatar_split_clause,[],[f4119,f2067,f726,f1592,f2062]) ).
fof(f4180,plain,
( ~ spl0_154
| spl0_340
| ~ spl0_11
| spl0_152 ),
inference(avatar_split_clause,[],[f2730,f1354,f706,f2420,f1364]) ).
fof(f4187,plain,
( spl0_10
| ~ spl0_6
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f3076,f737,f689,f702]) ).
fof(f4188,plain,
( spl0_10
| ~ spl0_4
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f3075,f737,f682,f702]) ).
fof(f4190,plain,
( c3_1(a1678)
| c0_1(a1678)
| ~ spl0_7
| ~ spl0_131 ),
inference(resolution,[],[f1252,f693]) ).
fof(f4200,plain,
( c3_1(a1702)
| ~ c0_1(a1702)
| ~ spl0_2
| spl0_320 ),
inference(resolution,[],[f676,f2184]) ).
fof(f4274,plain,
( ~ c2_1(a1644)
| c3_1(a1644)
| ~ spl0_8
| ~ spl0_195 ),
inference(resolution,[],[f697,f1565]) ).
fof(f4288,plain,
( ~ c2_1(a1667)
| c3_1(a1667)
| ~ spl0_8
| ~ spl0_121 ),
inference(resolution,[],[f697,f1204]) ).
fof(f4334,plain,
( ~ c3_1(a1677)
| c2_1(a1677)
| ~ spl0_15
| ~ spl0_127 ),
inference(resolution,[],[f721,f1232]) ).
fof(f4337,plain,
( ~ c3_1(a1650)
| c2_1(a1650)
| ~ spl0_15
| ~ spl0_106 ),
inference(resolution,[],[f721,f1130]) ).
fof(f4339,plain,
( spl0_105
| ~ spl0_104
| ~ spl0_15
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f4337,f1128,f720,f1118,f1123]) ).
fof(f4342,plain,
( spl0_128
| spl0_129
| ~ spl0_16
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f3687,f1230,f723,f1240,f1235]) ).
fof(f4356,plain,
( c0_1(a1674)
| c2_1(a1674)
| ~ spl0_16
| ~ spl0_213 ),
inference(resolution,[],[f724,f1653]) ).
fof(f4385,plain,
( c0_1(a1678)
| c2_1(a1678)
| ~ spl0_16
| ~ spl0_131 ),
inference(resolution,[],[f724,f1252]) ).
fof(f4399,plain,
( ~ spl0_295
| ~ spl0_2
| ~ spl0_6
| spl0_293 ),
inference(avatar_split_clause,[],[f2593,f2047,f689,f675,f2057]) ).
fof(f4401,plain,
( ~ spl0_240
| ~ spl0_2
| ~ spl0_6
| spl0_241 ),
inference(avatar_split_clause,[],[f2617,f1788,f689,f675,f1783]) ).
fof(f4422,plain,
( spl0_128
| ~ spl0_358
| ~ spl0_15
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f4334,f1230,f720,f2739,f1235]) ).
fof(f4485,plain,
( ~ c3_1(a1691)
| c2_1(a1691)
| ~ spl0_15
| ~ spl0_153 ),
inference(resolution,[],[f721,f1361]) ).
fof(f4488,plain,
( ~ c3_1(a1678)
| c2_1(a1678)
| ~ spl0_15
| ~ spl0_131 ),
inference(resolution,[],[f721,f1252]) ).
fof(f4540,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_5
| ~ spl0_26 ),
inference(resolution,[],[f764,f687]) ).
fof(f4559,plain,
( ~ c3_1(a1714)
| ~ c2_1(a1714)
| ~ spl0_26
| ~ spl0_179 ),
inference(resolution,[],[f764,f1487]) ).
fof(f4578,plain,
( ~ c3_1(a1660)
| ~ c2_1(a1660)
| ~ spl0_26
| ~ spl0_111 ),
inference(resolution,[],[f764,f1154]) ).
fof(f4579,plain,
( ~ c3_1(a1645)
| ~ c2_1(a1645)
| ~ spl0_26
| ~ spl0_96 ),
inference(resolution,[],[f764,f1081]) ).
fof(f4580,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_26 ),
inference(duplicate_literal_removal,[],[f4540]) ).
fof(f4584,plain,
( ~ spl0_373
| ~ spl0_113
| ~ spl0_26
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f4578,f1152,f763,f1162,f2853]) ).
fof(f4599,plain,
( ~ spl0_267
| ~ spl0_366
| ~ spl0_26
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f4559,f1485,f763,f2780,f1918]) ).
fof(f4615,plain,
( ~ c2_1(a1673)
| c3_1(a1673)
| ~ spl0_8
| ~ spl0_211 ),
inference(resolution,[],[f1643,f697]) ).
fof(f4632,plain,
( ~ spl0_372
| ~ spl0_94
| ~ spl0_26
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f4579,f1079,f763,f1069,f2848]) ).
fof(f4692,plain,
( ~ c2_1(a1666)
| c3_1(a1666)
| ~ spl0_8
| ~ spl0_120 ),
inference(resolution,[],[f1199,f697]) ).
fof(f4744,plain,
( c0_1(a1661)
| ~ c3_1(a1661)
| ~ spl0_11
| spl0_205 ),
inference(resolution,[],[f707,f1613]) ).
fof(f4802,plain,
( ~ c3_1(a1695)
| ~ spl0_5
| ~ spl0_26
| ~ spl0_258 ),
inference(resolution,[],[f4580,f1875]) ).
fof(f4819,plain,
( ~ spl0_162
| ~ spl0_5
| ~ spl0_26
| ~ spl0_258 ),
inference(avatar_split_clause,[],[f4802,f1873,f763,f686,f1402]) ).
fof(f4831,plain,
( spl0_284
| spl0_384
| ~ spl0_1
| ~ spl0_195 ),
inference(avatar_split_clause,[],[f3445,f1563,f672,f3153,f2002]) ).
fof(f4848,plain,
( spl0_245
| ~ spl0_246
| ~ spl0_6
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f3778,f1202,f689,f1813,f1808]) ).
fof(f4852,plain,
( spl0_310
| ~ spl0_353
| ~ spl0_10
| spl0_212 ),
inference(avatar_split_clause,[],[f2647,f1646,f702,f2485,f2132]) ).
fof(f4854,plain,
( spl0_307
| ~ spl0_306
| ~ spl0_10
| spl0_210 ),
inference(avatar_split_clause,[],[f2649,f1636,f702,f2112,f2117]) ).
fof(f4870,plain,
( spl0_212
| spl0_353
| ~ spl0_16
| ~ spl0_213 ),
inference(avatar_split_clause,[],[f4356,f1651,f723,f2485,f1646]) ).
fof(f4877,plain,
( spl0_130
| spl0_132
| ~ spl0_16
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f4385,f1250,f723,f1255,f1245]) ).
fof(f5139,plain,
( c0_1(a1676)
| c3_1(a1676)
| ~ spl0_28
| ~ spl0_314 ),
inference(resolution,[],[f772,f2154]) ).
fof(f5205,plain,
( spl0_313
| spl0_215
| ~ spl0_28
| ~ spl0_314 ),
inference(avatar_split_clause,[],[f5139,f2152,f771,f1661,f2147]) ).
fof(f5219,plain,
( ~ c0_1(a1649)
| ~ c3_1(a1649)
| ~ spl0_30
| spl0_196 ),
inference(resolution,[],[f780,f1570]) ).
fof(f5234,plain,
( ~ c0_1(a1691)
| ~ c3_1(a1691)
| ~ spl0_30
| spl0_152 ),
inference(resolution,[],[f780,f1356]) ).
fof(f5243,plain,
( ~ spl0_154
| ~ spl0_340
| ~ spl0_30
| spl0_152 ),
inference(avatar_split_clause,[],[f5234,f1354,f779,f2420,f1364]) ).
fof(f5258,plain,
( ~ spl0_197
| ~ spl0_285
| ~ spl0_30
| spl0_196 ),
inference(avatar_split_clause,[],[f5219,f1568,f779,f2007,f1573]) ).
fof(f5275,plain,
( c0_1(a1715)
| c3_1(a1715)
| ~ spl0_32
| spl0_329 ),
inference(resolution,[],[f788,f2229]) ).
fof(f5277,plain,
( c0_1(a1702)
| c3_1(a1702)
| ~ spl0_32
| spl0_320 ),
inference(resolution,[],[f788,f2184]) ).
fof(f5329,plain,
( c2_1(a1661)
| ~ c0_1(a1661)
| ~ spl0_37
| spl0_300 ),
inference(resolution,[],[f811,f2084]) ).
fof(f5338,plain,
( c2_1(a1725)
| ~ c0_1(a1725)
| ~ spl0_37
| spl0_271 ),
inference(resolution,[],[f811,f1940]) ).
fof(f5367,plain,
( ~ spl0_347
| spl0_184
| ~ spl0_37
| spl0_271 ),
inference(avatar_split_clause,[],[f5338,f1938,f810,f1510,f2455]) ).
fof(f5371,plain,
( ~ spl0_351
| spl0_205
| ~ spl0_37
| spl0_300 ),
inference(avatar_split_clause,[],[f5329,f2082,f810,f1611,f2475]) ).
fof(f5384,plain,
( ~ spl0_354
| spl0_318
| ~ spl0_2
| spl0_320 ),
inference(avatar_split_clause,[],[f4200,f2182,f675,f2172,f2490]) ).
fof(f5395,plain,
( spl0_98
| ~ spl0_237
| ~ spl0_4
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f3480,f1093,f682,f1768,f1088]) ).
fof(f5399,plain,
( spl0_377
| ~ spl0_246
| ~ spl0_4
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f3776,f1202,f682,f1813,f3108]) ).
fof(f5441,plain,
( spl0_209
| spl0_305
| ~ spl0_7
| ~ spl0_208 ),
inference(avatar_split_clause,[],[f4043,f1626,f692,f2107,f1631]) ).
fof(f5442,plain,
( spl0_194
| spl0_284
| ~ spl0_7
| ~ spl0_195 ),
inference(avatar_split_clause,[],[f4046,f1563,f692,f2002,f1558]) ).
fof(f5443,plain,
( spl0_182
| spl0_269
| ~ spl0_7
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f4050,f1505,f692,f1928,f1500]) ).
fof(f5450,plain,
( spl0_132
| spl0_359
| ~ spl0_7
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f4190,f1250,f692,f2744,f1255]) ).
fof(f5453,plain,
( ~ spl0_333
| ~ spl0_232
| ~ spl0_17
| ~ spl0_332 ),
inference(avatar_split_clause,[],[f4100,f2242,f726,f1743,f2247]) ).
fof(f5454,plain,
( ~ spl0_330
| ~ spl0_231
| ~ spl0_17
| ~ spl0_331 ),
inference(avatar_split_clause,[],[f4101,f2237,f726,f1738,f2232]) ).
fof(f5456,plain,
( spl0_328
| spl0_355
| ~ spl0_32
| spl0_329 ),
inference(avatar_split_clause,[],[f5275,f2227,f787,f2495,f2222]) ).
fof(f5457,plain,
( spl0_318
| spl0_354
| ~ spl0_32
| spl0_320 ),
inference(avatar_split_clause,[],[f5277,f2182,f787,f2490,f2172]) ).
fof(f5470,plain,
( spl0_328
| ~ spl0_355
| ~ spl0_10
| spl0_230 ),
inference(avatar_split_clause,[],[f3411,f1733,f702,f2495,f2222]) ).
fof(f5482,plain,
( spl0_284
| ~ spl0_384
| ~ spl0_8
| ~ spl0_195 ),
inference(avatar_split_clause,[],[f4274,f1563,f696,f3153,f2002]) ).
fof(f5521,plain,
( spl0_270
| spl0_347
| ~ spl0_9
| spl0_184 ),
inference(avatar_split_clause,[],[f3594,f1510,f699,f2455,f1933]) ).
fof(f5545,plain,
( ~ spl0_204
| spl0_351
| ~ spl0_11
| spl0_205 ),
inference(avatar_split_clause,[],[f4744,f1611,f706,f2475,f1606]) ).
fof(f5573,plain,
( spl0_152
| ~ spl0_154
| ~ spl0_15
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f4485,f1359,f720,f1364,f1354]) ).
fof(f5574,plain,
( spl0_130
| ~ spl0_359
| ~ spl0_15
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f4488,f1250,f720,f2744,f1245]) ).
fof(f5586,plain,
( ~ c0_1(a1674)
| c2_1(a1674)
| ~ spl0_4
| ~ spl0_213 ),
inference(resolution,[],[f683,f1653]) ).
fof(f5650,plain,
( c0_1(a1674)
| c3_1(a1674)
| ~ spl0_9
| spl0_212 ),
inference(resolution,[],[f700,f1648]) ).
fof(f5670,plain,
( c0_1(a1678)
| c3_1(a1678)
| ~ spl0_9
| spl0_130 ),
inference(resolution,[],[f700,f1247]) ).
fof(f5675,plain,
( spl0_359
| spl0_132
| ~ spl0_9
| spl0_130 ),
inference(avatar_split_clause,[],[f5670,f1245,f699,f1255,f2744]) ).
fof(f5682,plain,
( spl0_212
| ~ spl0_353
| ~ spl0_4
| ~ spl0_213 ),
inference(avatar_split_clause,[],[f5586,f1651,f682,f2485,f1646]) ).
fof(f5707,plain,
( spl0_245
| ~ spl0_377
| ~ spl0_8
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f4288,f1202,f696,f3108,f1808]) ).
fof(f5714,plain,
( spl0_243
| ~ spl0_244
| ~ spl0_8
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f4692,f1197,f696,f1803,f1798]) ).
fof(f5717,plain,
( spl0_309
| ~ spl0_308
| ~ spl0_8
| ~ spl0_211 ),
inference(avatar_split_clause,[],[f4615,f1641,f696,f2122,f2127]) ).
fof(f5723,plain,
( spl0_310
| spl0_353
| ~ spl0_9
| spl0_212 ),
inference(avatar_split_clause,[],[f5650,f1646,f699,f2485,f2132]) ).
fof(f5786,plain,
( c0_1(a1677)
| c3_1(a1677)
| ~ spl0_9
| spl0_128 ),
inference(resolution,[],[f700,f1237]) ).
fof(f5789,plain,
( spl0_358
| spl0_129
| ~ spl0_9
| spl0_128 ),
inference(avatar_split_clause,[],[f5786,f1235,f699,f1240,f2739]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f684]) ).
cnf(s2,plain,
( spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f694]) ).
cnf(s3,plain,
( spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f704]) ).
cnf(s4,plain,
( spl0_3
| spl0_11
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f714]) ).
cnf(s6,plain,
( spl0_3
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f728]) ).
cnf(s8,plain,
( spl0_2
| spl0_3
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f744]) ).
cnf(s9,plain,
( spl0_3
| spl0_8
| spl0_13
| spl0_22 ),
inference(sat_conversion,[],[f749]) ).
cnf(s10,plain,
( spl0_3
| spl0_6
| ~ spl0_23
| spl0_24 ),
inference(sat_conversion,[],[f757]) ).
cnf(s11,plain,
( spl0_2
| spl0_3
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f765]) ).
cnf(s12,plain,
( spl0_3
| spl0_10
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f773]) ).
cnf(s13,plain,
( spl0_2
| spl0_3
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f781]) ).
cnf(s14,plain,
( spl0_3
| spl0_8
| ~ spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f789]) ).
cnf(s16,plain,
( spl0_3
| spl0_6
| spl0_8
| spl0_34 ),
inference(sat_conversion,[],[f799]) ).
cnf(s18,plain,
( spl0_3
| spl0_30
| spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f812]) ).
cnf(s19,plain,
( spl0_3
| spl0_6
| spl0_7
| spl0_38 ),
inference(sat_conversion,[],[f817]) ).
cnf(s28,plain,
( spl0_3
| spl0_7
| spl0_26
| spl0_52 ),
inference(sat_conversion,[],[f877]) ).
cnf(s32,plain,
( spl0_3
| spl0_13
| spl0_57
| ~ spl0_58 ),
inference(sat_conversion,[],[f904]) ).
cnf(s33,plain,
( spl0_3
| spl0_21
| spl0_24
| ~ spl0_59 ),
inference(sat_conversion,[],[f909]) ).
cnf(s37,plain,
( spl0_3
| spl0_6
| ~ spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f941]) ).
cnf(s40,plain,
( spl0_3
| spl0_17
| spl0_69
| ~ spl0_70 ),
inference(sat_conversion,[],[f960]) ).
cnf(s41,plain,
( spl0_3
| spl0_17
| ~ spl0_71
| ~ spl0_72 ),
inference(sat_conversion,[],[f969]) ).
cnf(s42,plain,
( spl0_3
| spl0_10
| spl0_73
| ~ spl0_74 ),
inference(sat_conversion,[],[f978]) ).
cnf(s49,plain,
( spl0_3
| spl0_4
| ~ spl0_83
| spl0_84 ),
inference(sat_conversion,[],[f1025]) ).
cnf(s51,plain,
( spl0_3
| spl0_11
| ~ spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s56,plain,
( ~ spl0_40
| spl0_94 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s57,plain,
( ~ spl0_40
| ~ spl0_95 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s58,plain,
( ~ spl0_40
| spl0_96 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s59,plain,
( spl0_97
| ~ spl0_98 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s60,plain,
( spl0_97
| spl0_99 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s65,plain,
( ~ spl0_73
| spl0_104 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s66,plain,
( ~ spl0_73
| ~ spl0_105 ),
inference(sat_conversion,[],[f1126]) ).
cnf(s67,plain,
( ~ spl0_73
| spl0_106 ),
inference(sat_conversion,[],[f1131]) ).
cnf(s68,plain,
( spl0_71
| ~ spl0_107 ),
inference(sat_conversion,[],[f1136]) ).
cnf(s71,plain,
( spl0_70
| spl0_111 ),
inference(sat_conversion,[],[f1155]) ).
cnf(s72,plain,
( spl0_70
| ~ spl0_112 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s73,plain,
( spl0_70
| spl0_113 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s80,plain,
( spl0_59
| spl0_120 ),
inference(sat_conversion,[],[f1200]) ).
cnf(s81,plain,
( ~ spl0_21
| spl0_121 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s85,plain,
( ~ spl0_66
| spl0_127 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s86,plain,
( ~ spl0_66
| ~ spl0_128 ),
inference(sat_conversion,[],[f1238]) ).
cnf(s87,plain,
( ~ spl0_66
| ~ spl0_129 ),
inference(sat_conversion,[],[f1243]) ).
cnf(s88,plain,
( spl0_65
| ~ spl0_130 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s89,plain,
( spl0_65
| spl0_131 ),
inference(sat_conversion,[],[f1253]) ).
cnf(s90,plain,
( spl0_65
| ~ spl0_132 ),
inference(sat_conversion,[],[f1258]) ).
cnf(s109,plain,
( ~ spl0_22
| ~ spl0_152 ),
inference(sat_conversion,[],[f1357]) ).
cnf(s110,plain,
( ~ spl0_22
| spl0_153 ),
inference(sat_conversion,[],[f1362]) ).
cnf(s111,plain,
( ~ spl0_22
| spl0_154 ),
inference(sat_conversion,[],[f1367]) ).
cnf(s117,plain,
( ~ spl0_38
| spl0_162 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s132,plain,
( ~ spl0_88
| spl0_179 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s134,plain,
( ~ spl0_57
| ~ spl0_181 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s135,plain,
( ~ spl0_27
| ~ spl0_182 ),
inference(sat_conversion,[],[f1503]) ).
cnf(s136,plain,
( ~ spl0_27
| spl0_183 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s137,plain,
( ~ spl0_25
| ~ spl0_184 ),
inference(sat_conversion,[],[f1513]) ).
cnf(s145,plain,
( ~ spl0_29
| ~ spl0_194 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s146,plain,
( ~ spl0_29
| spl0_195 ),
inference(sat_conversion,[],[f1566]) ).
cnf(s147,plain,
( spl0_74
| ~ spl0_196 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s148,plain,
( spl0_74
| spl0_197 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s151,plain,
( ~ spl0_200
| spl0_201 ),
inference(sat_conversion,[],[f1595]) ).
cnf(s153,plain,
( ~ spl0_69
| spl0_204 ),
inference(sat_conversion,[],[f1609]) ).
cnf(s154,plain,
( ~ spl0_69
| ~ spl0_205 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s157,plain,
( ~ spl0_84
| spl0_208 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s158,plain,
( ~ spl0_84
| ~ spl0_209 ),
inference(sat_conversion,[],[f1634]) ).
cnf(s159,plain,
( spl0_83
| ~ spl0_210 ),
inference(sat_conversion,[],[f1639]) ).
cnf(s160,plain,
( ~ spl0_52
| spl0_211 ),
inference(sat_conversion,[],[f1644]) ).
cnf(s161,plain,
( ~ spl0_36
| ~ spl0_212 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s162,plain,
( ~ spl0_36
| spl0_213 ),
inference(sat_conversion,[],[f1654]) ).
cnf(s164,plain,
( spl0_23
| ~ spl0_215 ),
inference(sat_conversion,[],[f1664]) ).
cnf(s176,plain,
( spl0_87
| ~ spl0_230 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s177,plain,
( spl0_31
| spl0_231 ),
inference(sat_conversion,[],[f1741]) ).
cnf(s178,plain,
( spl0_58
| spl0_232 ),
inference(sat_conversion,[],[f1746]) ).
cnf(s183,plain,
( spl0_97
| spl0_237 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s186,plain,
( spl0_71
| spl0_240 ),
inference(sat_conversion,[],[f1786]) ).
cnf(s187,plain,
( spl0_71
| ~ spl0_241 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s189,plain,
( spl0_59
| ~ spl0_243 ),
inference(sat_conversion,[],[f1801]) ).
cnf(s190,plain,
( spl0_59
| spl0_244 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s191,plain,
( ~ spl0_21
| ~ spl0_245 ),
inference(sat_conversion,[],[f1811]) ).
cnf(s192,plain,
( ~ spl0_21
| spl0_246 ),
inference(sat_conversion,[],[f1816]) ).
cnf(s203,plain,
( ~ spl0_38
| spl0_257 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s204,plain,
( ~ spl0_38
| spl0_258 ),
inference(sat_conversion,[],[f1876]) ).
cnf(s212,plain,
( ~ spl0_88
| spl0_266 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s213,plain,
( ~ spl0_88
| spl0_267 ),
inference(sat_conversion,[],[f1921]) ).
cnf(s214,plain,
( ~ spl0_57
| ~ spl0_268 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s215,plain,
( ~ spl0_27
| ~ spl0_269 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s216,plain,
( ~ spl0_25
| ~ spl0_270 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s217,plain,
( ~ spl0_25
| ~ spl0_271 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s229,plain,
( ~ spl0_29
| ~ spl0_284 ),
inference(sat_conversion,[],[f2005]) ).
cnf(s230,plain,
( spl0_74
| spl0_285 ),
inference(sat_conversion,[],[f2010]) ).
cnf(s238,plain,
( spl0_72
| ~ spl0_293 ),
inference(sat_conversion,[],[f2050]) ).
cnf(s239,plain,
( spl0_72
| spl0_294 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s240,plain,
( spl0_72
| spl0_295 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s241,plain,
( ~ spl0_200
| spl0_296 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s242,plain,
( ~ spl0_200
| spl0_297 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s245,plain,
( ~ spl0_69
| ~ spl0_300 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s250,plain,
( ~ spl0_84
| ~ spl0_305 ),
inference(sat_conversion,[],[f2110]) ).
cnf(s251,plain,
( spl0_83
| spl0_306 ),
inference(sat_conversion,[],[f2115]) ).
cnf(s252,plain,
( spl0_83
| ~ spl0_307 ),
inference(sat_conversion,[],[f2120]) ).
cnf(s253,plain,
( ~ spl0_52
| spl0_308 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s254,plain,
( ~ spl0_52
| ~ spl0_309 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s255,plain,
( ~ spl0_36
| ~ spl0_310 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s258,plain,
( spl0_23
| ~ spl0_313 ),
inference(sat_conversion,[],[f2150]) ).
cnf(s259,plain,
( spl0_23
| spl0_314 ),
inference(sat_conversion,[],[f2155]) ).
cnf(s263,plain,
( ~ spl0_34
| ~ spl0_318 ),
inference(sat_conversion,[],[f2175]) ).
cnf(s264,plain,
( ~ spl0_34
| spl0_319 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s265,plain,
( ~ spl0_34
| ~ spl0_320 ),
inference(sat_conversion,[],[f2185]) ).
cnf(s273,plain,
( spl0_87
| ~ spl0_328 ),
inference(sat_conversion,[],[f2225]) ).
cnf(s274,plain,
( spl0_87
| ~ spl0_329 ),
inference(sat_conversion,[],[f2230]) ).
cnf(s275,plain,
( spl0_31
| spl0_330 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s276,plain,
( spl0_31
| spl0_331 ),
inference(sat_conversion,[],[f2240]) ).
cnf(s277,plain,
( spl0_58
| spl0_332 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s278,plain,
( spl0_58
| spl0_333 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s282,plain,
( spl0_38
| ~ spl0_72
| spl0_200 ),
inference(sat_conversion,[],[f2262]) ).
cnf(s284,plain,
( ~ spl0_145
| spl0_216
| spl0_219 ),
inference(sat_conversion,[],[f2264]) ).
cnf(s287,plain,
( spl0_29
| spl0_40
| ~ spl0_97 ),
inference(sat_conversion,[],[f2267]) ).
cnf(s312,plain,
( ~ spl0_3
| spl0_145 ),
inference(sat_conversion,[],[f2292]) ).
cnf(s353,plain,
( ~ spl0_3
| ~ spl0_216 ),
inference(sat_conversion,[],[f2333]) ).
cnf(s354,plain,
( ~ spl0_3
| ~ spl0_219 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s404,plain,
( ~ spl0_17
| ~ spl0_162
| ~ spl0_257
| ~ spl0_258 ),
inference(sat_conversion,[],[f2832]) ).
cnf(s405,plain,
( ~ spl0_10
| spl0_107
| ~ spl0_240
| spl0_241 ),
inference(sat_conversion,[],[f2833]) ).
cnf(s417,plain,
( ~ spl0_10
| ~ spl0_13
| spl0_293
| ~ spl0_295 ),
inference(sat_conversion,[],[f3013]) ).
cnf(s447,plain,
( ~ spl0_20
| spl0_184
| spl0_270
| spl0_271 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s469,plain,
( ~ spl0_20
| spl0_230
| spl0_328
| spl0_329 ),
inference(sat_conversion,[],[f3205]) ).
cnf(s481,plain,
( ~ spl0_7
| ~ spl0_127
| spl0_129
| spl0_358 ),
inference(sat_conversion,[],[f3263]) ).
cnf(s495,plain,
( ~ spl0_6
| ~ spl0_179
| ~ spl0_266
| spl0_366 ),
inference(sat_conversion,[],[f3305]) ).
cnf(s496,plain,
( ~ spl0_12
| ~ spl0_179
| ~ spl0_266
| ~ spl0_267 ),
inference(sat_conversion,[],[f3306]) ).
cnf(s497,plain,
( ~ spl0_8
| ~ spl0_179
| ~ spl0_267
| spl0_366 ),
inference(sat_conversion,[],[f3307]) ).
cnf(s566,plain,
( ~ spl0_1
| ~ spl0_20
| spl0_181
| spl0_268 ),
inference(sat_conversion,[],[f3526]) ).
cnf(s591,plain,
( ~ spl0_11
| ~ spl0_94
| spl0_95
| spl0_372 ),
inference(sat_conversion,[],[f3648]) ).
cnf(s592,plain,
( ~ spl0_11
| spl0_112
| ~ spl0_113
| spl0_373 ),
inference(sat_conversion,[],[f3649]) ).
cnf(s628,plain,
( ~ spl0_24
| spl0_318
| ~ spl0_319
| spl0_320 ),
inference(sat_conversion,[],[f3757]) ).
cnf(s632,plain,
( ~ spl0_6
| spl0_13
| ~ spl0_24 ),
inference(sat_conversion,[],[f3761]) ).
cnf(s638,plain,
( ~ spl0_4
| spl0_152
| ~ spl0_153
| ~ spl0_340 ),
inference(sat_conversion,[],[f3772]) ).
cnf(s707,plain,
( ~ spl0_10
| ~ spl0_13
| spl0_318
| ~ spl0_354 ),
inference(sat_conversion,[],[f3885]) ).
cnf(s711,plain,
( ~ spl0_8
| ~ spl0_24
| spl0_293
| ~ spl0_294 ),
inference(sat_conversion,[],[f4021]) ).
cnf(s736,plain,
( ~ spl0_17
| ~ spl0_201
| ~ spl0_296
| ~ spl0_297 ),
inference(sat_conversion,[],[f4163]) ).
cnf(s754,plain,
( ~ spl0_11
| spl0_152
| ~ spl0_154
| spl0_340 ),
inference(sat_conversion,[],[f4180]) ).
cnf(s761,plain,
( ~ spl0_6
| spl0_10
| ~ spl0_20 ),
inference(sat_conversion,[],[f4187]) ).
cnf(s762,plain,
( ~ spl0_4
| spl0_10
| ~ spl0_20 ),
inference(sat_conversion,[],[f4188]) ).
cnf(s764,plain,
( ~ spl0_15
| ~ spl0_104
| spl0_105
| ~ spl0_106 ),
inference(sat_conversion,[],[f4339]) ).
cnf(s767,plain,
( ~ spl0_16
| ~ spl0_127
| spl0_128
| spl0_129 ),
inference(sat_conversion,[],[f4342]) ).
cnf(s778,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_293
| ~ spl0_295 ),
inference(sat_conversion,[],[f4399]) ).
cnf(s780,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_240
| spl0_241 ),
inference(sat_conversion,[],[f4401]) ).
cnf(s801,plain,
( ~ spl0_15
| ~ spl0_127
| spl0_128
| ~ spl0_358 ),
inference(sat_conversion,[],[f4422]) ).
cnf(s803,plain,
( ~ spl0_26
| ~ spl0_111
| ~ spl0_113
| ~ spl0_373 ),
inference(sat_conversion,[],[f4584]) ).
cnf(s818,plain,
( ~ spl0_26
| ~ spl0_179
| ~ spl0_267
| ~ spl0_366 ),
inference(sat_conversion,[],[f4599]) ).
cnf(s848,plain,
( ~ spl0_26
| ~ spl0_94
| ~ spl0_96
| ~ spl0_372 ),
inference(sat_conversion,[],[f4632]) ).
cnf(s909,plain,
( ~ spl0_5
| ~ spl0_26
| ~ spl0_162
| ~ spl0_258 ),
inference(sat_conversion,[],[f4819]) ).
cnf(s921,plain,
( ~ spl0_1
| ~ spl0_195
| spl0_284
| spl0_384 ),
inference(sat_conversion,[],[f4831]) ).
cnf(s945,plain,
( ~ spl0_6
| ~ spl0_121
| spl0_245
| ~ spl0_246 ),
inference(sat_conversion,[],[f4848]) ).
cnf(s949,plain,
( ~ spl0_10
| spl0_212
| spl0_310
| ~ spl0_353 ),
inference(sat_conversion,[],[f4852]) ).
cnf(s951,plain,
( ~ spl0_10
| spl0_210
| ~ spl0_306
| spl0_307 ),
inference(sat_conversion,[],[f4854]) ).
cnf(s967,plain,
( ~ spl0_16
| spl0_212
| ~ spl0_213
| spl0_353 ),
inference(sat_conversion,[],[f4870]) ).
cnf(s974,plain,
( ~ spl0_16
| spl0_130
| ~ spl0_131
| spl0_132 ),
inference(sat_conversion,[],[f4877]) ).
cnf(s1029,plain,
( ~ spl0_28
| spl0_215
| spl0_313
| ~ spl0_314 ),
inference(sat_conversion,[],[f5205]) ).
cnf(s1036,plain,
( ~ spl0_30
| spl0_152
| ~ spl0_154
| ~ spl0_340 ),
inference(sat_conversion,[],[f5243]) ).
cnf(s1051,plain,
( ~ spl0_30
| spl0_196
| ~ spl0_197
| ~ spl0_285 ),
inference(sat_conversion,[],[f5258]) ).
cnf(s1079,plain,
( ~ spl0_37
| spl0_184
| spl0_271
| ~ spl0_347 ),
inference(sat_conversion,[],[f5367]) ).
cnf(s1083,plain,
( ~ spl0_37
| spl0_205
| spl0_300
| ~ spl0_351 ),
inference(sat_conversion,[],[f5371]) ).
cnf(s1096,plain,
( ~ spl0_2
| spl0_318
| spl0_320
| ~ spl0_354 ),
inference(sat_conversion,[],[f5384]) ).
cnf(s1107,plain,
( ~ spl0_4
| spl0_98
| ~ spl0_99
| ~ spl0_237 ),
inference(sat_conversion,[],[f5395]) ).
cnf(s1111,plain,
( ~ spl0_4
| ~ spl0_121
| ~ spl0_246
| spl0_377 ),
inference(sat_conversion,[],[f5399]) ).
cnf(s1159,plain,
( ~ spl0_7
| ~ spl0_208
| spl0_209
| spl0_305 ),
inference(sat_conversion,[],[f5441]) ).
cnf(s1160,plain,
( ~ spl0_7
| spl0_194
| ~ spl0_195
| spl0_284 ),
inference(sat_conversion,[],[f5442]) ).
cnf(s1161,plain,
( ~ spl0_7
| spl0_182
| ~ spl0_183
| spl0_269 ),
inference(sat_conversion,[],[f5443]) ).
cnf(s1168,plain,
( ~ spl0_7
| ~ spl0_131
| spl0_132
| spl0_359 ),
inference(sat_conversion,[],[f5450]) ).
cnf(s1171,plain,
( ~ spl0_17
| ~ spl0_232
| ~ spl0_332
| ~ spl0_333 ),
inference(sat_conversion,[],[f5453]) ).
cnf(s1172,plain,
( ~ spl0_17
| ~ spl0_231
| ~ spl0_330
| ~ spl0_331 ),
inference(sat_conversion,[],[f5454]) ).
cnf(s1174,plain,
( ~ spl0_32
| spl0_328
| spl0_329
| spl0_355 ),
inference(sat_conversion,[],[f5456]) ).
cnf(s1175,plain,
( ~ spl0_32
| spl0_318
| spl0_320
| spl0_354 ),
inference(sat_conversion,[],[f5457]) ).
cnf(s1188,plain,
( ~ spl0_10
| spl0_230
| spl0_328
| ~ spl0_355 ),
inference(sat_conversion,[],[f5470]) ).
cnf(s1200,plain,
( ~ spl0_8
| ~ spl0_195
| spl0_284
| ~ spl0_384 ),
inference(sat_conversion,[],[f5482]) ).
cnf(s1239,plain,
( ~ spl0_9
| spl0_184
| spl0_270
| spl0_347 ),
inference(sat_conversion,[],[f5521]) ).
cnf(s1263,plain,
( ~ spl0_11
| ~ spl0_204
| spl0_205
| spl0_351 ),
inference(sat_conversion,[],[f5545]) ).
cnf(s1291,plain,
( ~ spl0_15
| spl0_152
| ~ spl0_153
| ~ spl0_154 ),
inference(sat_conversion,[],[f5573]) ).
cnf(s1292,plain,
( ~ spl0_15
| spl0_130
| ~ spl0_131
| ~ spl0_359 ),
inference(sat_conversion,[],[f5574]) ).
cnf(s1306,plain,
( ~ spl0_9
| spl0_130
| spl0_132
| spl0_359 ),
inference(sat_conversion,[],[f5675]) ).
cnf(s1313,plain,
( ~ spl0_4
| spl0_212
| ~ spl0_213
| ~ spl0_353 ),
inference(sat_conversion,[],[f5682]) ).
cnf(s1338,plain,
( ~ spl0_8
| ~ spl0_121
| spl0_245
| ~ spl0_377 ),
inference(sat_conversion,[],[f5707]) ).
cnf(s1345,plain,
( ~ spl0_8
| ~ spl0_120
| spl0_243
| ~ spl0_244 ),
inference(sat_conversion,[],[f5714]) ).
cnf(s1348,plain,
( ~ spl0_8
| ~ spl0_211
| ~ spl0_308
| spl0_309 ),
inference(sat_conversion,[],[f5717]) ).
cnf(s1354,plain,
( ~ spl0_9
| spl0_212
| spl0_310
| spl0_353 ),
inference(sat_conversion,[],[f5723]) ).
cnf(s1356,plain,
( ~ spl0_9
| spl0_128
| spl0_129
| spl0_358 ),
inference(sat_conversion,[],[f5789]) ).
cnf(s1362,plain,
( spl0_97
| ~ spl0_4 ),
inference(rat,[],[s1107,s59,s60,s183]) ).
cnf(s1367,plain,
( spl0_65
| ~ spl0_16 ),
inference(rat,[],[s974,s88,s89,s90]) ).
cnf(s1368,plain,
( ~ spl0_16
| spl0_6
| spl0_3 ),
inference(rat,[],[s767,s85,s86,s87,s37,s1367]) ).
cnf(s1369,plain,
( spl0_65
| ~ spl0_15
| ~ spl0_7 ),
inference(rat,[],[s1292,s1168,s88,s89,s90]) ).
cnf(s1370,plain,
( ~ spl0_15
| ~ spl0_7
| spl0_6
| spl0_3 ),
inference(rat,[],[s481,s801,s85,s86,s87,s37,s1369]) ).
cnf(s1374,plain,
( spl0_58
| ~ spl0_17 ),
inference(rat,[],[s1171,s178,s277,s278]) ).
cnf(s1375,plain,
( spl0_71
| ~ spl0_10 ),
inference(rat,[],[s405,s68,s186,s187]) ).
cnf(s1376,plain,
( spl0_74
| ~ spl0_30 ),
inference(rat,[],[s1051,s147,s148,s230]) ).
cnf(s1377,plain,
( spl0_83
| ~ spl0_10 ),
inference(rat,[],[s951,s159,s251,s252]) ).
cnf(s1379,plain,
( spl0_87
| ~ spl0_32
| ~ spl0_10 ),
inference(rat,[],[s1188,s1174,s176,s273,s274]) ).
cnf(s1380,plain,
( ~ spl0_32
| spl0_11
| ~ spl0_10
| ~ spl0_34
| spl0_3 ),
inference(rat,[],[s496,s132,s212,s213,s51,s1379,s4,s707,s1175,s265,s263]) ).
cnf(s1381,plain,
( spl0_31
| ~ spl0_17 ),
inference(rat,[],[s177,s1172,s275,s276]) ).
cnf(s1382,plain,
( ~ spl0_10
| ~ spl0_32
| ~ spl0_34
| spl0_8
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s638,s754,s109,s110,s111,s9,s707,s1380,s1175,s265,s263]) ).
cnf(s1383,plain,
( ~ spl0_27
| ~ spl0_7 ),
inference(rat,[],[s1161,s135,s136,s215]) ).
cnf(s1384,plain,
( spl0_8
| ~ spl0_10
| ~ spl0_31
| spl0_6
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s1382,s14,s16]) ).
cnf(s1385,plain,
( ~ spl0_21
| ~ spl0_8
| ~ spl0_4 ),
inference(rat,[],[s1111,s1338,s81,s191,s192]) ).
cnf(s1386,plain,
( spl0_59
| ~ spl0_8 ),
inference(rat,[],[s1345,s80,s189,s190]) ).
cnf(s1391,plain,
( ~ spl0_25
| ~ spl0_20 ),
inference(rat,[],[s447,s137,s216,s217]) ).
cnf(s1392,plain,
( ~ spl0_88
| ~ spl0_26
| ~ spl0_8 ),
inference(rat,[],[s818,s497,s132,s213]) ).
cnf(s1393,plain,
( ~ spl0_40
| ~ spl0_11
| ~ spl0_26 ),
inference(rat,[],[s848,s591,s56,s57,s58]) ).
cnf(s1394,plain,
( ~ spl0_29
| ~ spl0_7 ),
inference(rat,[],[s1160,s145,s146,s229]) ).
cnf(s1395,plain,
( ~ spl0_8
| ~ spl0_40
| ~ spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s469,s176,s273,s274,s51,s1393,s1392,s11,s1391,s8,s1385]) ).
cnf(s1396,plain,
( spl0_6
| spl0_5
| ~ spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s1029,s164,s258,s259,s10,s628,s12,s263,s264,s265,s1384,s16,s1395,s287,s1394,s1383,s1381,s6,s1370,s1368,s2,s1362]) ).
cnf(s1397,plain,
( ~ spl0_21
| ~ spl0_6 ),
inference(rat,[],[s945,s81,s191,s192]) ).
cnf(s1398,plain,
( ~ spl0_88
| ~ spl0_26
| ~ spl0_6 ),
inference(rat,[],[s818,s495,s132,s212,s213]) ).
cnf(s1399,plain,
( ~ spl0_22
| ~ spl0_11
| ~ spl0_4 ),
inference(rat,[],[s638,s754,s109,s110,s111]) ).
cnf(s1403,plain,
( spl0_87
| ~ spl0_20 ),
inference(rat,[],[s469,s176,s273,s274]) ).
cnf(s1407,plain,
( spl0_70
| ~ spl0_11
| ~ spl0_26 ),
inference(rat,[],[s803,s592,s71,s72,s73]) ).
cnf(s1409,plain,
( spl0_72
| ~ spl0_13
| ~ spl0_10 ),
inference(rat,[],[s417,s238,s240]) ).
cnf(s1410,plain,
( ~ spl0_200
| ~ spl0_17 ),
inference(rat,[],[s736,s151,s241,s242]) ).
cnf(s1411,plain,
( ~ spl0_17
| ~ spl0_72 ),
inference(rat,[],[s404,s117,s203,s204,s282,s1410]) ).
cnf(s1412,plain,
( ~ spl0_72
| ~ spl0_71
| spl0_3 ),
inference(rat,[],[s41,s1411]) ).
cnf(s1413,plain,
( spl0_13
| spl0_22
| ~ spl0_6
| spl0_3 ),
inference(rat,[],[s33,s1386,s632,s9,s1397]) ).
cnf(s1414,plain,
( ~ spl0_72
| ~ spl0_71
| spl0_3 ),
inference(rat,[],[s1411,s41]) ).
cnf(s1415,plain,
( ~ spl0_6
| ~ spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s1414,s1375,s1409,s762,s1413,s1399,s51,s1403,s1398,s11,s1391,s8,s1397]) ).
cnf(s1416,plain,
( ~ spl0_8
| spl0_72
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s33,s711,s1386,s1385,s239,s238]) ).
cnf(s1417,plain,
( ~ spl0_10
| spl0_6
| ~ spl0_4
| spl0_3 ),
inference(rat,[],[s1291,s6,s109,s110,s111,s1381,s9,s1384,s1416,s1409,s1412,s1375,s1368]) ).
cnf(s1418,plain,
( ~ spl0_22
| ~ spl0_15 ),
inference(rat,[],[s1291,s109,s110,s111]) ).
cnf(s1419,plain,
( ~ spl0_73
| ~ spl0_15 ),
inference(rat,[],[s764,s65,s66,s67]) ).
cnf(s1420,plain,
( ~ spl0_4
| spl0_3
| spl0_2 ),
inference(rat,[],[s1313,s1354,s161,s162,s255,s18,s1376,s42,s1419,s1079,s1239,s137,s216,s217,s11,s6,s909,s404,s117,s203,s204,s19,s1383,s12,s1029,s164,s258,s259,s10,s628,s263,s264,s265,s3,s16,s1385,s8,s762,s1417,s1396,s1368,s1415]) ).
cnf(s1421,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s1420,s1]) ).
cnf(s1422,plain,
~ spl0_3,
inference(rat,[],[s284,s312,s353,s354]) ).
cnf(s1423,plain,
( ~ spl0_10
| spl0_6 ),
inference(rat,[],[s1348,s9,s160,s253,s254,s1418,s28,s6,s909,s404,s117,s203,s204,s2,s19,s1159,s157,s158,s250,s1409,s49,s1412,s1417,s1377,s1375,s1368,s1422]) ).
cnf(s1424,plain,
( spl0_8
| ~ spl0_31
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s1096,s1175,s263,s265,s14,s16,s1422]) ).
cnf(s1425,plain,
( ~ spl0_17
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s404,s117,s203,s204,s19,s1383,s12,s1029,s164,s258,s259,s10,s711,s1424,s238,s239,s1411,s1381,s1423,s1422]) ).
cnf(s1429,plain,
( spl0_65
| ~ spl0_9
| ~ spl0_15 ),
inference(rat,[],[s1292,s1306,s88,s89,s90]) ).
cnf(s1430,plain,
( spl0_6
| ~ spl0_2 ),
inference(rat,[],[s801,s1356,s85,s86,s87,s37,s1429,s3,s1348,s160,s253,s254,s28,s909,s117,s204,s2,s19,s1370,s6,s1425,s1423,s1368,s1422]) ).
cnf(s1431,plain,
( spl0_72
| ~ spl0_2 ),
inference(rat,[],[s778,s238,s240,s1430]) ).
cnf(s1432,plain,
~ spl0_2,
inference(rat,[],[s780,s186,s187,s1414,s1431,s1430,s1422]) ).
cnf(s1434,plain,
spl0_1,
inference(rat,[],[s1421,s1422,s1432]) ).
cnf(s1435,plain,
( spl0_8
| spl0_6 ),
inference(rat,[],[s801,s1356,s85,s86,s87,s37,s1429,s6,s404,s117,s203,s204,s19,s1383,s12,s1029,s164,s258,s259,s10,s628,s263,s264,s265,s3,s16,s1368,s1423,s1422]) ).
cnf(s1436,plain,
( ~ spl0_17
| spl0_6 ),
inference(rat,[],[s404,s117,s203,s204,s19,s1383,s12,s1029,s164,s258,s259,s10,s711,s238,s239,s1411,s1423,s1435,s1422]) ).
cnf(s1437,plain,
spl0_6,
inference(rat,[],[s1200,s921,s146,s229,s13,s1376,s42,s1419,s6,s1436,s1435,s1423,s1368,s1434,s1432,s1422]) ).
cnf(s1438,plain,
~ spl0_21,
inference(rat,[],[s1397,s1437]) ).
cnf(s1439,plain,
spl0_20,
inference(rat,[],[s8,s1422,s1432,s1438]) ).
cnf(s1440,plain,
~ spl0_25,
inference(rat,[],[s1391,s1439]) ).
cnf(s1441,plain,
spl0_10,
inference(rat,[],[s761,s1437,s1439]) ).
cnf(s1442,plain,
spl0_87,
inference(rat,[],[s1403,s1439]) ).
cnf(s1443,plain,
spl0_26,
inference(rat,[],[s11,s1422,s1432,s1440]) ).
cnf(s1444,plain,
spl0_71,
inference(rat,[],[s1375,s1441]) ).
cnf(s1446,plain,
~ spl0_88,
inference(rat,[],[s1398,s1437,s1443]) ).
cnf(s1448,plain,
~ spl0_72,
inference(rat,[],[s1412,s1422,s1444]) ).
cnf(s1450,plain,
spl0_11,
inference(rat,[],[s51,s1442,s1422,s1446]) ).
cnf(s1454,plain,
~ spl0_13,
inference(rat,[],[s1409,s1441,s1448]) ).
cnf(s1459,plain,
spl0_70,
inference(rat,[],[s1407,s1443,s1450]) ).
cnf(s1462,plain,
spl0_22,
inference(rat,[],[s1413,s1422,s1437,s1454]) ).
cnf(s1465,plain,
spl0_154,
inference(rat,[],[s111,s1462]) ).
cnf(s1467,plain,
~ spl0_152,
inference(rat,[],[s109,s1462]) ).
cnf(s1468,plain,
~ spl0_15,
inference(rat,[],[s1418,s1462]) ).
cnf(s1473,plain,
spl0_340,
inference(rat,[],[s754,s1467,s1450,s1465]) ).
cnf(s1475,plain,
~ spl0_30,
inference(rat,[],[s1036,s1467,s1465,s1473]) ).
cnf(s1484,plain,
~ spl0_57,
inference(rat,[],[s566,s134,s214,s1434,s1439]) ).
cnf(s1485,plain,
~ spl0_58,
inference(rat,[],[s32,s1454,s1422,s1484]) ).
cnf(s1489,plain,
~ spl0_17,
inference(rat,[],[s1374,s1485]) ).
cnf(s1491,plain,
spl0_16,
inference(rat,[],[s6,s1422,s1468,s1489]) ).
cnf(s1492,plain,
spl0_69,
inference(rat,[],[s40,s1459,s1422,s1489]) ).
cnf(s1494,plain,
~ spl0_300,
inference(rat,[],[s245,s1492]) ).
cnf(s1495,plain,
~ spl0_205,
inference(rat,[],[s154,s1492]) ).
cnf(s1496,plain,
spl0_204,
inference(rat,[],[s153,s1492]) ).
cnf(s1497,plain,
spl0_351,
inference(rat,[],[s1263,s1495,s1450,s1496]) ).
cnf(s1498,plain,
~ spl0_37,
inference(rat,[],[s1083,s1495,s1494,s1497]) ).
cnf(s1500,plain,
spl0_36,
inference(rat,[],[s18,s1422,s1475,s1498]) ).
cnf(s1504,plain,
~ spl0_310,
inference(rat,[],[s255,s1500]) ).
cnf(s1505,plain,
spl0_213,
inference(rat,[],[s162,s1500]) ).
cnf(s1506,plain,
~ spl0_212,
inference(rat,[],[s161,s1500]) ).
cnf(s1508,plain,
spl0_353,
inference(rat,[],[s967,s1505,s1491,s1506]) ).
cnf(s1509,plain,
$false,
inference(rat,[],[s949,s1504,s1441,s1508,s1506]) ).
fof(f5795,plain,
$false,
inference(avatar_sat_refutation,[],[s1509]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN457-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n019.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 16:06:03 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.44/0.31 % (4125266)Will run a generic schedule for satisfiability detection.
% 0.44/0.31 % (4125273)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2820872219:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.44/0.31 % (4125271)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2013299056_2999 on theBenchmark for (2999ds/0Mi)
% 0.44/0.31 % (4125274)dis+10_1_sil=32000:sp=arity:random_seed=1623682712:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.44/0.31 % (4125277)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2587672604:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.44/0.31 % (4125275)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1667974008:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.44/0.31 % (4125276)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=26878984:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.44/0.31 % (4125272)% WARNING: option uhcvi not known.
% 0.44/0.31 % (4125272)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1314314902:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.44/0.31 % Detected minimum model sizes of [1]
% 0.44/0.31 % Detected maximum model sizes of [76]
% 0.44/0.31 % TRYING [1]
% 0.44/0.31 % TRYING [2]
% 0.44/0.31 % TRYING [3]
% 0.44/0.31 % TRYING [4]
% 0.44/0.31 % TRYING [5]
% 0.44/0.31 % (4125277) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-4125266-4125277"...
% 0.44/0.31 % (4125274)Instruction limit reached!
% 0.44/0.31 % (4125274)------------------------------
% 0.44/0.31 % (4125274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.31 % (4125274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.31 % (4125274)CaDiCaL version: 2.1.3
% 0.44/0.31 % (4125274)Termination reason: Instruction limit
% 0.44/0.31 % (4125274)Termination phase: Saturation
% 0.44/0.31 % (4125274)Time elapsed: 0.063 s
% 0.44/0.31 % (4125274)Peak memory usage: 13 MB
% 0.44/0.31 % (4125274)Instructions burned: 104 (million)
% 0.44/0.31 % (4125277)...printing done.
% 0.44/0.31 % (4125277)Refutation found. Thanks to Tanya!
% 0.44/0.31 % SZS status Unsatisfiable for theBenchmark
% 0.44/0.31 % SZS output start Proof for theBenchmark
% See solution above
% 0.44/0.33 % (4125277)------------------------------
% 0.44/0.33 % (4125277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.33 % (4125277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.33 % (4125277)CaDiCaL version: 2.1.3
% 0.44/0.33 % (4125277)Termination reason: Refutation
% 0.44/0.33 % (4125277)Time elapsed: 0.069 s
% 0.44/0.33 % (4125277)Peak memory usage: 14 MB
% 0.44/0.33 % (4125277)Instructions burned: 115 (million)
% 0.44/0.33 % (4125266)Success in time 0.107 s
% 0.44/0.33 % Vampire exiting
%------------------------------------------------------------------------------