%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN483-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:13:23 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.25s
% Output : Refutation 0.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 236
% Syntax : Number of formulae : 911 ( 24 unt; 126 def)
% Number of atoms : 2973 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3685 (1623 ~;1936 |; 0 &)
% ( 126 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 154 ( 153 usr; 150 prp; 0-1 aty)
% Number of functors : 22 ( 22 usr; 22 con; 0-0 aty)
% Number of variables : 194 ( 0 sgn 194 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( ~ hskp29
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f3,negated_conjecture,
( ~ hskp27
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
fof(f29,negated_conjecture,
( ~ hskp1
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
fof(f31,negated_conjecture,
( hskp29
| hskp27
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
fof(f32,negated_conjecture,
( hskp8
| hskp17
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
( hskp8
| hskp10
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f34,negated_conjecture,
( hskp18
| hskp10
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( hskp18
| hskp22
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( hskp18
| hskp1
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp10
| hskp28
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f41,negated_conjecture,
( ~ hskp29
| c0_1(a1885) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp29
| c1_1(a1885) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp29
| c2_1(a1885) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp28
| c1_1(a1878) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp28
| c2_1(a1878) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp28
| c3_1(a1878) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp27
| c0_1(a1877) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp27
| c2_1(a1877) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp27
| c3_1(a1877) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp26
| c0_1(a1858) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp26
| c1_1(a1858) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp26
| c3_1(a1858) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f55,negated_conjecture,
( ~ hskp24
| c3_1(a1919) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp23
| c0_1(a1911) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp22
| c0_1(a1899) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp21
| c3_1(a1898) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f60,negated_conjecture,
( ~ hskp18
| c0_1(a1875) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp18
| c1_1(a1875) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp17
| c0_1(a1874) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp17
| c2_1(a1874) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp16
| c2_1(a1872) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp16
| c3_1(a1872) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( ~ hskp15
| c1_1(a1870) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f69,negated_conjecture,
( ~ hskp12
| c3_1(a1866) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp10
| c0_1(a1864) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp10
| c3_1(a1864) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp9
| c2_1(a1863) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp8
| c0_1(a1862) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp8
| c1_1(a1862) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f76,negated_conjecture,
( ~ hskp6
| c1_1(a1860) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp5
| c2_1(a1857) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f82,negated_conjecture,
( ~ hskp1
| c1_1(a1853) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp1
| c3_1(a1853) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ hskp0
| c1_1(a1852) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ hskp0
| c3_1(a1852) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f87,negated_conjecture,
( ~ c1_1(a1919)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ c2_1(a1919)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c1_1(a1911)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c3_1(a1911)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c2_1(a1899)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c3_1(a1899)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c0_1(a1898)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c1_1(a1898)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f100,negated_conjecture,
( ~ c3_1(a1875)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c1_1(a1874)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c0_1(a1872)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c0_1(a1870)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c3_1(a1870)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f106,negated_conjecture,
( ~ c1_1(a1867)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c2_1(a1867)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c3_1(a1867)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c0_1(a1866)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c2_1(a1866)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f114,negated_conjecture,
( ~ c1_1(a1864)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c1_1(a1863)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c3_1(a1863)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c2_1(a1862)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f120,negated_conjecture,
( ~ c0_1(a1860)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c2_1(a1860)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c0_1(a1857)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c3_1(a1857)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f125,negated_conjecture,
( ~ c0_1(a1855)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c1_1(a1855)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c2_1(a1855)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f129,negated_conjecture,
( ~ c0_1(a1853)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ c2_1(a1852)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f136,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp22
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp1
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp9
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp8
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp8
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp26
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f155,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp26
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp27
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f158,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp26
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| hskp0
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f171,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f176,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f178,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X1)
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f186,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X1)
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c1_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause191) ).
fof(f192,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f193,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X2)
| c3_1(X0)
| c2_1(X1)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c1_1(X1)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| c2_1(X1)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f213,plain,
( ~ hskp8
| hskp17
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f214,plain,
( ~ hskp8
| hskp10
| ~ hskp24 ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f215,plain,
( ~ hskp18
| hskp10
| ~ hskp15 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f216,plain,
( ~ hskp18
| hskp22
| hskp12 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f217,plain,
( ~ hskp18
| hskp1
| hskp6 ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f221,plain,
( ~ hskp29
| ~ c2_1(a1885) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f222,plain,
( ~ hskp28
| ~ c2_1(a1878) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f223,plain,
( ~ hskp27
| ~ c2_1(a1877) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f224,plain,
( hskp26
| c0_1(a1858) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f225,plain,
( hskp26
| c1_1(a1858) ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f226,plain,
( hskp26
| c3_1(a1858) ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f229,plain,
( hskp24
| c3_1(a1919) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f230,plain,
( hskp23
| c0_1(a1911) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f231,plain,
( hskp21
| c3_1(a1898) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f233,plain,
( hskp18
| c0_1(a1875) ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f234,plain,
( hskp18
| c1_1(a1875) ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f235,plain,
( ~ hskp17
| ~ c2_1(a1874) ),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f236,plain,
( hskp16
| ~ c2_1(a1872) ),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f237,plain,
( hskp16
| c3_1(a1872) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f238,plain,
( hskp15
| c1_1(a1870) ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f241,plain,
( hskp9
| ~ c2_1(a1863) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f242,plain,
( hskp8
| c0_1(a1862) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f243,plain,
( hskp8
| c1_1(a1862) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f245,plain,
( hskp5
| ~ c2_1(a1857) ),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f250,plain,
( ~ c1_1(a1919)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f251,plain,
( c2_1(a1919)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f252,plain,
( ~ c1_1(a1911)
| hskp23 ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f253,plain,
( ~ c3_1(a1911)
| hskp23 ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f254,plain,
( c2_1(a1899)
| ~ hskp22 ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f255,plain,
( ~ c0_1(a1898)
| hskp21 ),
inference(consistent_polarity_flipping,[],[f93]) ).
fof(f256,plain,
( ~ c1_1(a1898)
| hskp21 ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f259,plain,
( ~ c3_1(a1875)
| hskp18 ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f260,plain,
( ~ c0_1(a1872)
| hskp16 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f261,plain,
( ~ c0_1(a1870)
| hskp15 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f262,plain,
( ~ c3_1(a1870)
| hskp15 ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f264,plain,
( c2_1(a1867)
| ~ hskp13 ),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f265,plain,
( c2_1(a1866)
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f267,plain,
( ~ c1_1(a1863)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f268,plain,
( ~ c3_1(a1863)
| hskp9 ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f269,plain,
( c2_1(a1862)
| hskp8 ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f272,plain,
( c2_1(a1860)
| ~ hskp6 ),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f273,plain,
( ~ c0_1(a1857)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f274,plain,
( ~ c3_1(a1857)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f275,plain,
( ~ c0_1(a1855)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f276,plain,
( ~ c1_1(a1855)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f277,plain,
( c2_1(a1855)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f279,plain,
( c2_1(a1852)
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f285,plain,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| hskp22
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f292,plain,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| ~ c2_1(X0)
| hskp1
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f296,plain,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ c2_1(X0)
| ~ hskp9
| hskp13 ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f297,plain,
! [X0] :
( c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| ~ hskp8
| ~ hskp23 ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f301,plain,
! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ hskp8
| ~ hskp18 ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f302,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ hskp26
| ~ hskp23 ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f304,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ hskp26
| hskp10 ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f305,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| hskp27
| hskp22 ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f307,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ hskp26
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f308,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| hskp0
| ~ hskp24 ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f312,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1)
| hskp1 ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f317,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| ~ c2_1(X1)
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f320,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X0)
| c0_1(X1)
| ~ c2_1(X1)
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f323,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| c0_1(X1)
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f324,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| ~ hskp15 ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f325,plain,
! [X0,X1] :
( c2_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp27 ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f326,plain,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f177]) ).
fof(f327,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1)
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f328,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X0)
| c0_1(X1)
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f329,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X1)
| hskp27 ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f330,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| ~ hskp21 ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f331,plain,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X0)
| c1_1(X1)
| ~ hskp18 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f332,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X1)
| ~ hskp24 ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f335,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f336,plain,
! [X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X1)
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f337,plain,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c1_1(X2)
| ~ c2_1(X2)
| c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f338,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f189]) ).
fof(f339,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| ~ c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f340,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f341,plain,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| c2_1(X2)
| ~ c3_1(X2)
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f342,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c1_1(X2)
| c3_1(X0)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f343,plain,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X2)
| ~ c3_1(X2)
| ~ c2_1(X0)
| c1_1(X1)
| c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f344,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c2_1(X1)
| ~ c3_1(X1)
| c2_1(X2)
| c1_1(X1)
| c1_1(X2)
| c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f195]) ).
fof(f345,plain,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f196]) ).
fof(f347,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f348,plain,
( ! [X2] :
( c3_1(X2)
| ~ c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f347]) ).
fof(f350,definition,
( spl0_2
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f351,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f357,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f358,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f359,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f345,f357,f353,f350,f347]) ).
fof(f361,definition,
( spl0_5
<=> ! [X2] :
( c2_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f362,plain,
( ! [X2] :
( c3_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f364,definition,
( spl0_6
<=> ! [X1] :
( c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f365,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c2_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f367,definition,
( spl0_7
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f368,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f369,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f344,f367,f353,f364,f361]) ).
fof(f371,definition,
( spl0_8
<=> ! [X2] :
( c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f372,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| c2_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f371]) ).
fof(f374,definition,
( spl0_9
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f375,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f376,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f343,f350,f353,f374,f371]) ).
fof(f378,definition,
( spl0_10
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f379,plain,
( ! [X2] :
( c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f381,definition,
( spl0_11
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f382,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f381]) ).
fof(f384,definition,
( spl0_12
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f385,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f386,plain,
( spl0_10
| spl0_11
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f342,f384,f353,f381,f378]) ).
fof(f387,plain,
( spl0_8
| spl0_6
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f341,f378,f353,f364,f371]) ).
fof(f389,definition,
( spl0_13
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f390,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c1_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f392,definition,
( spl0_14
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f393,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f394,plain,
( spl0_13
| spl0_5
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f340,f392,f353,f361,f389]) ).
fof(f396,definition,
( spl0_15
<=> ! [X2] :
( c0_1(X2)
| ~ c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f397,plain,
( ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| c1_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f399,definition,
( spl0_16
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f400,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,definition,
( spl0_17
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f403,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f402]) ).
fof(f404,plain,
( spl0_15
| spl0_16
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f339,f402,f353,f399,f396]) ).
fof(f406,definition,
( spl0_18
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f407,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f406]) ).
fof(f408,plain,
( spl0_15
| spl0_16
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f338,f406,f353,f399,f396]) ).
fof(f410,definition,
( spl0_19
<=> ! [X2] :
( c1_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f411,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2)
| ~ c2_1(X2) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f410]) ).
fof(f412,plain,
( spl0_19
| spl0_9
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f337,f378,f353,f374,f410]) ).
fof(f414,definition,
( spl0_20
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f418,definition,
( spl0_21
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f419,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( ~ spl0_20
| spl0_2
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f336,f418,f353,f350,f414]) ).
fof(f422,definition,
( spl0_22
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f426,definition,
( spl0_23
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f427,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f428,plain,
( spl0_22
| spl0_11
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f335,f426,f353,f381,f422]) ).
fof(f430,definition,
( spl0_24
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f440,definition,
( spl0_26
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f443,plain,
( ~ spl0_26
| spl0_1
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f332,f418,f353,f347,f440]) ).
fof(f445,definition,
( spl0_27
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f448,plain,
( ~ spl0_27
| spl0_6
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f331,f381,f353,f364,f445]) ).
fof(f450,definition,
( spl0_28
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f454,definition,
( spl0_29
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f455,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f456,plain,
( ~ spl0_28
| spl0_29
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f330,f367,f353,f454,f450]) ).
fof(f458,definition,
( spl0_30
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f461,plain,
( spl0_30
| spl0_8
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f329,f384,f353,f371,f458]) ).
fof(f462,plain,
( ~ spl0_20
| spl0_13
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f328,f381,f353,f389,f414]) ).
fof(f464,definition,
( spl0_31
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f468,definition,
( spl0_32
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f469,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f470,plain,
( ~ spl0_31
| spl0_32
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f327,f418,f353,f468,f464]) ).
fof(f472,definition,
( spl0_33
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f475,plain,
( ~ spl0_33
| spl0_29
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f326,f350,f353,f454,f472]) ).
fof(f476,plain,
( spl0_30
| spl0_8
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f325,f361,f353,f371,f458]) ).
fof(f478,definition,
( spl0_34
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f481,plain,
( ~ spl0_34
| spl0_8
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f324,f454,f353,f371,f478]) ).
fof(f483,definition,
( spl0_35
<=> ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f484,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f483]) ).
fof(f485,plain,
( ~ spl0_31
| spl0_16
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f323,f483,f353,f399,f464]) ).
fof(f503,definition,
( spl0_40
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f506,plain,
( ~ spl0_40
| spl0_32
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f320,f381,f353,f468,f503]) ).
fof(f516,definition,
( spl0_43
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f521,definition,
( spl0_44
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f524,plain,
( ~ spl0_44
| spl0_35
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f317,f347,f353,f483,f521]) ).
fof(f533,definition,
( spl0_47
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f543,definition,
( spl0_49
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f546,plain,
( spl0_49
| spl0_15
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f312,f483,f353,f396,f543]) ).
fof(f548,definition,
( spl0_50
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f556,definition,
( spl0_52
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f561,definition,
( spl0_53
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f565,plain,
( ~ spl0_26
| spl0_50
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f308,f367,f353,f548,f440]) ).
fof(f566,plain,
( ~ spl0_40
| ~ spl0_52
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f307,f367,f353,f556,f503]) ).
fof(f573,definition,
( spl0_55
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f576,plain,
( spl0_55
| spl0_30
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f305,f402,f353,f458,f573]) ).
fof(f577,plain,
( spl0_22
| ~ spl0_52
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f304,f381,f353,f556,f422]) ).
fof(f580,definition,
( spl0_56
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f583,plain,
( ~ spl0_56
| ~ spl0_52
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f302,f374,f353,f556,f580]) ).
fof(f584,plain,
( ~ spl0_27
| ~ spl0_31
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f301,f406,f353,f464,f445]) ).
fof(f588,plain,
( ~ spl0_56
| ~ spl0_31
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f297,f361,f353,f464,f580]) ).
fof(f590,definition,
( spl0_57
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f593,plain,
( spl0_57
| ~ spl0_44
| ~ spl0_3
| spl0_35 ),
inference(avatar_split_clause,[],[f296,f483,f353,f521,f590]) ).
fof(f597,plain,
( ~ spl0_44
| spl0_49
| ~ spl0_3
| spl0_32 ),
inference(avatar_split_clause,[],[f292,f468,f353,f543,f521]) ).
fof(f609,definition,
( spl0_60
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f615,plain,
( ~ spl0_20
| spl0_55
| spl0_19
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f285,f353,f410,f573,f414]) ).
fof(f626,definition,
( spl0_62
<=> c2_1(a1852) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f628,plain,
( c2_1(a1852)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f629,plain,
( ~ spl0_50
| spl0_62 ),
inference(avatar_split_clause,[],[f279,f626,f548]) ).
fof(f631,definition,
( spl0_63
<=> c0_1(a1853) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f634,plain,
( ~ spl0_49
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f129,f631,f543]) ).
fof(f641,definition,
( spl0_65
<=> c2_1(a1855) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f643,plain,
( c2_1(a1855)
| ~ spl0_65 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f644,plain,
( spl0_40
| spl0_65 ),
inference(avatar_split_clause,[],[f277,f641,f503]) ).
fof(f646,definition,
( spl0_66
<=> c1_1(a1855) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f649,plain,
( spl0_40
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f276,f646,f503]) ).
fof(f651,definition,
( spl0_67
<=> c0_1(a1855) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f654,plain,
( spl0_40
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f275,f651,f503]) ).
fof(f661,definition,
( spl0_69
<=> c3_1(a1857) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f663,plain,
( ~ c3_1(a1857)
| spl0_69 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f664,plain,
( spl0_33
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f274,f661,f472]) ).
fof(f666,definition,
( spl0_70
<=> c0_1(a1857) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f669,plain,
( spl0_33
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f273,f666,f472]) ).
fof(f671,definition,
( spl0_71
<=> c2_1(a1860) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f673,plain,
( c2_1(a1860)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
( ~ spl0_43
| spl0_71 ),
inference(avatar_split_clause,[],[f272,f671,f516]) ).
fof(f676,definition,
( spl0_72
<=> c0_1(a1860) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f679,plain,
( ~ spl0_43
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f120,f676,f516]) ).
fof(f691,definition,
( spl0_75
<=> c2_1(a1862) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f693,plain,
( c2_1(a1862)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f694,plain,
( spl0_31
| spl0_75 ),
inference(avatar_split_clause,[],[f269,f691,f464]) ).
fof(f696,definition,
( spl0_76
<=> c3_1(a1863) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f698,plain,
( ~ c3_1(a1863)
| spl0_76 ),
inference(avatar_component_clause,[],[f696]) ).
fof(f699,plain,
( spl0_44
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f268,f696,f521]) ).
fof(f701,definition,
( spl0_77
<=> c1_1(a1863) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f704,plain,
( spl0_44
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f267,f701,f521]) ).
fof(f706,definition,
( spl0_78
<=> c1_1(a1864) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f709,plain,
( ~ spl0_22
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f114,f706,f422]) ).
fof(f726,definition,
( spl0_82
<=> c2_1(a1866) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f728,plain,
( c2_1(a1866)
| ~ spl0_82 ),
inference(avatar_component_clause,[],[f726]) ).
fof(f729,plain,
( ~ spl0_60
| spl0_82 ),
inference(avatar_split_clause,[],[f265,f726,f609]) ).
fof(f731,definition,
( spl0_83
<=> c0_1(a1866) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f734,plain,
( ~ spl0_60
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f109,f731,f609]) ).
fof(f736,definition,
( spl0_84
<=> c3_1(a1867) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f738,plain,
( ~ c3_1(a1867)
| spl0_84 ),
inference(avatar_component_clause,[],[f736]) ).
fof(f739,plain,
( ~ spl0_57
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f108,f736,f590]) ).
fof(f741,definition,
( spl0_85
<=> c2_1(a1867) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f743,plain,
( c2_1(a1867)
| ~ spl0_85 ),
inference(avatar_component_clause,[],[f741]) ).
fof(f744,plain,
( ~ spl0_57
| spl0_85 ),
inference(avatar_split_clause,[],[f264,f741,f590]) ).
fof(f746,definition,
( spl0_86
<=> c1_1(a1867) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f749,plain,
( ~ spl0_57
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f106,f746,f590]) ).
fof(f756,definition,
( spl0_88
<=> c3_1(a1870) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f758,plain,
( ~ c3_1(a1870)
| spl0_88 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f759,plain,
( spl0_34
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f262,f756,f478]) ).
fof(f761,definition,
( spl0_89
<=> c0_1(a1870) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f764,plain,
( spl0_34
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f261,f761,f478]) ).
fof(f766,definition,
( spl0_90
<=> c0_1(a1872) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f769,plain,
( spl0_20
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f260,f766,f414]) ).
fof(f771,definition,
( spl0_91
<=> c1_1(a1874) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f773,plain,
( ~ c1_1(a1874)
| spl0_91 ),
inference(avatar_component_clause,[],[f771]) ).
fof(f774,plain,
( ~ spl0_47
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f101,f771,f533]) ).
fof(f776,definition,
( spl0_92
<=> c3_1(a1875) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f778,plain,
( ~ c3_1(a1875)
| spl0_92 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,plain,
( spl0_27
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f259,f776,f445]) ).
fof(f806,definition,
( spl0_98
<=> c1_1(a1898) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f809,plain,
( spl0_28
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f256,f806,f450]) ).
fof(f811,definition,
( spl0_99
<=> c0_1(a1898) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f814,plain,
( spl0_28
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f255,f811,f450]) ).
fof(f816,definition,
( spl0_100
<=> c3_1(a1899) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f818,plain,
( ~ c3_1(a1899)
| spl0_100 ),
inference(avatar_component_clause,[],[f816]) ).
fof(f819,plain,
( ~ spl0_55
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f92,f816,f573]) ).
fof(f821,definition,
( spl0_101
<=> c2_1(a1899) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f824,plain,
( ~ spl0_55
| spl0_101 ),
inference(avatar_split_clause,[],[f254,f821,f573]) ).
fof(f826,definition,
( spl0_102
<=> c3_1(a1911) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f828,plain,
( ~ c3_1(a1911)
| spl0_102 ),
inference(avatar_component_clause,[],[f826]) ).
fof(f829,plain,
( spl0_56
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f253,f826,f580]) ).
fof(f831,definition,
( spl0_103
<=> c1_1(a1911) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f834,plain,
( spl0_56
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f252,f831,f580]) ).
fof(f836,definition,
( spl0_104
<=> c2_1(a1919) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f838,plain,
( c2_1(a1919)
| ~ spl0_104 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f839,plain,
( spl0_26
| spl0_104 ),
inference(avatar_split_clause,[],[f251,f836,f440]) ).
fof(f841,definition,
( spl0_105
<=> c1_1(a1919) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f844,plain,
( spl0_26
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f250,f841,f440]) ).
fof(f855,definition,
( spl0_108
<=> c3_1(a1852) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f857,plain,
( c3_1(a1852)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f855]) ).
fof(f858,plain,
( spl0_108
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f85,f548,f855]) ).
fof(f860,definition,
( spl0_109
<=> c1_1(a1852) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f863,plain,
( spl0_109
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f84,f548,f860]) ).
fof(f865,definition,
( spl0_110
<=> c3_1(a1853) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f867,plain,
( c3_1(a1853)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f868,plain,
( spl0_110
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f83,f543,f865]) ).
fof(f870,definition,
( spl0_111
<=> c1_1(a1853) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f873,plain,
( spl0_111
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f82,f543,f870]) ).
fof(f895,definition,
( spl0_116
<=> c2_1(a1857) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f897,plain,
( ~ c2_1(a1857)
| spl0_116 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f898,plain,
( ~ spl0_116
| spl0_33 ),
inference(avatar_split_clause,[],[f245,f472,f895]) ).
fof(f900,definition,
( spl0_117
<=> c1_1(a1860) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f903,plain,
( spl0_117
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f76,f516,f900]) ).
fof(f910,definition,
( spl0_119
<=> c1_1(a1862) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f912,plain,
( c1_1(a1862)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f910]) ).
fof(f913,plain,
( spl0_119
| spl0_31 ),
inference(avatar_split_clause,[],[f243,f464,f910]) ).
fof(f915,definition,
( spl0_120
<=> c0_1(a1862) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f918,plain,
( spl0_120
| spl0_31 ),
inference(avatar_split_clause,[],[f242,f464,f915]) ).
fof(f920,definition,
( spl0_121
<=> c2_1(a1863) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f923,plain,
( ~ spl0_121
| spl0_44 ),
inference(avatar_split_clause,[],[f241,f521,f920]) ).
fof(f925,definition,
( spl0_122
<=> c3_1(a1864) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f927,plain,
( c3_1(a1864)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f928,plain,
( spl0_122
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f71,f422,f925]) ).
fof(f930,definition,
( spl0_123
<=> c0_1(a1864) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f933,plain,
( spl0_123
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f70,f422,f930]) ).
fof(f935,definition,
( spl0_124
<=> c3_1(a1866) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f937,plain,
( c3_1(a1866)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f935]) ).
fof(f938,plain,
( spl0_124
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f69,f609,f935]) ).
fof(f950,definition,
( spl0_127
<=> c1_1(a1870) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f953,plain,
( spl0_127
| spl0_34 ),
inference(avatar_split_clause,[],[f238,f478,f950]) ).
fof(f955,definition,
( spl0_128
<=> c3_1(a1872) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f957,plain,
( c3_1(a1872)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f958,plain,
( spl0_128
| spl0_20 ),
inference(avatar_split_clause,[],[f237,f414,f955]) ).
fof(f960,definition,
( spl0_129
<=> c2_1(a1872) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f962,plain,
( ~ c2_1(a1872)
| spl0_129 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f963,plain,
( ~ spl0_129
| spl0_20 ),
inference(avatar_split_clause,[],[f236,f414,f960]) ).
fof(f965,definition,
( spl0_130
<=> c2_1(a1874) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f967,plain,
( ~ c2_1(a1874)
| spl0_130 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,plain,
( ~ spl0_130
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f235,f533,f965]) ).
fof(f970,definition,
( spl0_131
<=> c0_1(a1874) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f973,plain,
( spl0_131
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f62,f533,f970]) ).
fof(f975,definition,
( spl0_132
<=> c1_1(a1875) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f977,plain,
( c1_1(a1875)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f975]) ).
fof(f978,plain,
( spl0_132
| spl0_27 ),
inference(avatar_split_clause,[],[f234,f445,f975]) ).
fof(f980,definition,
( spl0_133
<=> c0_1(a1875) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f983,plain,
( spl0_133
| spl0_27 ),
inference(avatar_split_clause,[],[f233,f445,f980]) ).
fof(f990,definition,
( spl0_135
<=> c3_1(a1898) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f992,plain,
( c3_1(a1898)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f993,plain,
( spl0_135
| spl0_28 ),
inference(avatar_split_clause,[],[f231,f450,f990]) ).
fof(f995,definition,
( spl0_136
<=> c0_1(a1899) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f998,plain,
( spl0_136
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f57,f573,f995]) ).
fof(f1000,definition,
( spl0_137
<=> c0_1(a1911) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1003,plain,
( spl0_137
| spl0_56 ),
inference(avatar_split_clause,[],[f230,f580,f1000]) ).
fof(f1005,definition,
( spl0_138
<=> c3_1(a1919) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1007,plain,
( c3_1(a1919)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1005]) ).
fof(f1008,plain,
( spl0_138
| spl0_26 ),
inference(avatar_split_clause,[],[f229,f440,f1005]) ).
fof(f1020,definition,
( spl0_141
<=> c3_1(a1858) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1022,plain,
( c3_1(a1858)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f1020]) ).
fof(f1023,plain,
( spl0_141
| spl0_52 ),
inference(avatar_split_clause,[],[f226,f556,f1020]) ).
fof(f1025,definition,
( spl0_142
<=> c1_1(a1858) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1028,plain,
( spl0_142
| spl0_52 ),
inference(avatar_split_clause,[],[f225,f556,f1025]) ).
fof(f1030,definition,
( spl0_143
<=> c0_1(a1858) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1033,plain,
( spl0_143
| spl0_52 ),
inference(avatar_split_clause,[],[f224,f556,f1030]) ).
fof(f1035,definition,
( spl0_144
<=> c3_1(a1877) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1037,plain,
( c3_1(a1877)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f1035]) ).
fof(f1038,plain,
( spl0_144
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f49,f458,f1035]) ).
fof(f1040,definition,
( spl0_145
<=> c2_1(a1877) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1042,plain,
( ~ c2_1(a1877)
| spl0_145 ),
inference(avatar_component_clause,[],[f1040]) ).
fof(f1043,plain,
( ~ spl0_145
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f223,f458,f1040]) ).
fof(f1045,definition,
( spl0_146
<=> c0_1(a1877) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1048,plain,
( spl0_146
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f47,f458,f1045]) ).
fof(f1050,definition,
( spl0_147
<=> c3_1(a1878) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1052,plain,
( c3_1(a1878)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1050]) ).
fof(f1053,plain,
( spl0_147
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f46,f561,f1050]) ).
fof(f1055,definition,
( spl0_148
<=> c2_1(a1878) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1058,plain,
( ~ spl0_148
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f222,f561,f1055]) ).
fof(f1060,definition,
( spl0_149
<=> c1_1(a1878) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1063,plain,
( spl0_149
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f44,f561,f1060]) ).
fof(f1065,definition,
( spl0_150
<=> c2_1(a1885) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1067,plain,
( ~ c2_1(a1885)
| spl0_150 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1068,plain,
( ~ spl0_150
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f221,f430,f1065]) ).
fof(f1070,definition,
( spl0_151
<=> c1_1(a1885) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1073,plain,
( spl0_151
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f42,f430,f1070]) ).
fof(f1075,definition,
( spl0_152
<=> c0_1(a1885) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1078,plain,
( spl0_152
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f41,f430,f1075]) ).
fof(f1082,plain,
( spl0_50
| spl0_53
| spl0_22 ),
inference(avatar_split_clause,[],[f37,f422,f561,f548]) ).
fof(f1083,plain,
( spl0_43
| spl0_49
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f217,f445,f543,f516]) ).
fof(f1084,plain,
( spl0_60
| spl0_55
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f216,f445,f573,f609]) ).
fof(f1085,plain,
( ~ spl0_34
| spl0_22
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f215,f445,f422,f478]) ).
fof(f1086,plain,
( ~ spl0_26
| spl0_22
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f214,f464,f422,f440]) ).
fof(f1087,plain,
( ~ spl0_20
| spl0_47
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f213,f464,f533,f414]) ).
fof(f1088,plain,
( spl0_49
| spl0_30
| spl0_24 ),
inference(avatar_split_clause,[],[f31,f430,f458,f543]) ).
fof(f1090,plain,
( spl0_3
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f29,f543,f353]) ).
fof(f1116,plain,
( spl0_3
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f3,f458,f353]) ).
fof(f1118,plain,
( spl0_3
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f1,f430,f353]) ).
fof(f1119,plain,
( ~ c2_1(a1853)
| ~ c1_1(a1853)
| ~ spl0_2
| ~ spl0_110 ),
inference(resolution,[],[f351,f867]) ).
fof(f1123,definition,
( spl0_153
<=> c1_1(a1866) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1128,definition,
( spl0_154
<=> c2_1(a1853) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1129,plain,
( c2_1(a1853)
| ~ spl0_154 ),
inference(avatar_component_clause,[],[f1128]) ).
fof(f1130,plain,
( ~ c2_1(a1853)
| spl0_154 ),
inference(avatar_component_clause,[],[f1128]) ).
fof(f1167,definition,
( spl0_157
<=> c1_1(a1857) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1178,definition,
( spl0_159
<=> c2_1(a1870) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1179,plain,
( ~ c2_1(a1870)
| spl0_159 ),
inference(avatar_component_clause,[],[f1178]) ).
fof(f1180,plain,
( c2_1(a1870)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f1178]) ).
fof(f1183,definition,
( spl0_160
<=> c1_1(a1872) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1188,definition,
( spl0_161
<=> c2_1(a1875) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1189,plain,
( ~ c2_1(a1875)
| spl0_161 ),
inference(avatar_component_clause,[],[f1188]) ).
fof(f1193,definition,
( spl0_162
<=> c2_1(a1898) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1195,plain,
( c2_1(a1898)
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f1193]) ).
fof(f1198,definition,
( spl0_163
<=> c1_1(a1899) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1209,definition,
( spl0_165
<=> c2_1(a1858) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1211,plain,
( c2_1(a1858)
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f1209]) ).
fof(f1214,definition,
( spl0_166
<=> c1_1(a1877) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1216,plain,
( c1_1(a1877)
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1219,plain,
( ~ c0_1(a1885)
| ~ c1_1(a1885)
| ~ spl0_7
| spl0_150 ),
inference(resolution,[],[f368,f1067]) ).
fof(f1221,plain,
( ~ c0_1(a1877)
| ~ c1_1(a1877)
| ~ spl0_7
| spl0_145 ),
inference(resolution,[],[f368,f1042]) ).
fof(f1229,plain,
( ~ c0_1(a1875)
| ~ c1_1(a1875)
| ~ spl0_7
| spl0_161 ),
inference(resolution,[],[f368,f1189]) ).
fof(f1251,plain,
( c1_1(a1877)
| ~ c0_1(a1877)
| ~ spl0_9
| ~ spl0_144 ),
inference(resolution,[],[f375,f1037]) ).
fof(f1256,plain,
( ~ spl0_146
| spl0_166
| ~ spl0_9
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1251,f1035,f374,f1214,f1045]) ).
fof(f1257,plain,
( ~ spl0_166
| ~ spl0_146
| ~ spl0_7
| spl0_145 ),
inference(avatar_split_clause,[],[f1221,f1040,f367,f1045,f1214]) ).
fof(f1258,plain,
( ~ c2_1(a1852)
| ~ c1_1(a1852)
| ~ spl0_2
| ~ spl0_108 ),
inference(resolution,[],[f857,f351]) ).
fof(f1259,plain,
( ~ spl0_109
| ~ spl0_62
| ~ spl0_2
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1258,f855,f350,f626,f860]) ).
fof(f1261,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_2
| ~ spl0_10 ),
inference(resolution,[],[f379,f351]) ).
fof(f1270,plain,
( ~ c1_1(a1870)
| ~ c2_1(a1870)
| ~ spl0_10
| spl0_88 ),
inference(resolution,[],[f379,f758]) ).
fof(f1279,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_2
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f1261]) ).
fof(f1282,plain,
( ~ c1_1(a1862)
| ~ spl0_2
| ~ spl0_10
| ~ spl0_75 ),
inference(resolution,[],[f1279,f693]) ).
fof(f1285,plain,
( ~ spl0_119
| ~ spl0_2
| ~ spl0_10
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1282,f691,f378,f350,f910]) ).
fof(f1288,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(resolution,[],[f382,f368]) ).
fof(f1291,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_7
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f1288]) ).
fof(f1294,plain,
( c0_1(a1872)
| ~ c1_1(a1872)
| ~ spl0_13
| ~ spl0_128 ),
inference(resolution,[],[f390,f957]) ).
fof(f1295,plain,
( c0_1(a1866)
| ~ c1_1(a1866)
| ~ spl0_13
| ~ spl0_124 ),
inference(resolution,[],[f390,f937]) ).
fof(f1297,plain,
( c0_1(a1853)
| ~ c1_1(a1853)
| ~ spl0_13
| ~ spl0_110 ),
inference(resolution,[],[f390,f867]) ).
fof(f1298,plain,
( c0_1(a1852)
| ~ c1_1(a1852)
| ~ spl0_13
| ~ spl0_108 ),
inference(resolution,[],[f390,f857]) ).
fof(f1319,definition,
( spl0_167
<=> c0_1(a1867) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1340,definition,
( spl0_171
<=> c0_1(a1919) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1356,definition,
( spl0_173
<=> c0_1(a1852) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1368,plain,
( ~ c2_1(a1864)
| ~ c0_1(a1864)
| ~ spl0_17
| ~ spl0_122 ),
inference(resolution,[],[f403,f927]) ).
fof(f1374,definition,
( spl0_174
<=> c2_1(a1864) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1376,plain,
( ~ c2_1(a1864)
| spl0_174 ),
inference(avatar_component_clause,[],[f1374]) ).
fof(f1383,plain,
( c1_1(a1877)
| ~ c0_1(a1877)
| ~ spl0_18
| spl0_145 ),
inference(resolution,[],[f407,f1042]) ).
fof(f1391,plain,
( c1_1(a1874)
| ~ c0_1(a1874)
| ~ spl0_18
| spl0_130 ),
inference(resolution,[],[f407,f967]) ).
fof(f1395,plain,
( c1_1(a1864)
| ~ c0_1(a1864)
| ~ spl0_18
| spl0_174 ),
inference(resolution,[],[f407,f1376]) ).
fof(f1408,plain,
( ~ spl0_123
| spl0_78
| ~ spl0_18
| spl0_174 ),
inference(avatar_split_clause,[],[f1395,f1374,f406,f706,f930]) ).
fof(f1414,plain,
( ~ spl0_146
| spl0_166
| ~ spl0_18
| spl0_145 ),
inference(avatar_split_clause,[],[f1383,f1040,f406,f1214,f1045]) ).
fof(f1419,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_6
| ~ spl0_14 ),
inference(resolution,[],[f365,f393]) ).
fof(f1429,plain,
( ! [X0] :
( c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_6
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f1419]) ).
fof(f1445,plain,
( c0_1(a1872)
| ~ c1_1(a1872)
| ~ spl0_16
| spl0_129 ),
inference(resolution,[],[f400,f962]) ).
fof(f1446,plain,
( c0_1(a1870)
| ~ c1_1(a1870)
| ~ spl0_16
| spl0_159 ),
inference(resolution,[],[f400,f1179]) ).
fof(f1452,plain,
( c0_1(a1857)
| ~ c1_1(a1857)
| ~ spl0_16
| spl0_116 ),
inference(resolution,[],[f400,f897]) ).
fof(f1455,plain,
( c0_1(a1853)
| ~ c1_1(a1853)
| ~ spl0_16
| spl0_154 ),
inference(resolution,[],[f400,f1130]) ).
fof(f1461,plain,
( ~ spl0_111
| spl0_63
| ~ spl0_16
| spl0_154 ),
inference(avatar_split_clause,[],[f1455,f1128,f399,f631,f870]) ).
fof(f1462,plain,
( ~ spl0_127
| spl0_89
| ~ spl0_16
| spl0_159 ),
inference(avatar_split_clause,[],[f1446,f1178,f399,f761,f950]) ).
fof(f1465,plain,
( ~ spl0_131
| spl0_91
| ~ spl0_18
| spl0_130 ),
inference(avatar_split_clause,[],[f1391,f965,f406,f771,f970]) ).
fof(f1471,plain,
( ~ c1_1(a1875)
| ~ c2_1(a1875)
| ~ spl0_10
| spl0_92 ),
inference(resolution,[],[f778,f379]) ).
fof(f1481,plain,
( c1_1(a1919)
| ~ c0_1(a1919)
| ~ spl0_9
| ~ spl0_138 ),
inference(resolution,[],[f375,f1007]) ).
fof(f1484,plain,
( c1_1(a1864)
| ~ c0_1(a1864)
| ~ spl0_9
| ~ spl0_122 ),
inference(resolution,[],[f375,f927]) ).
fof(f1492,plain,
( c1_1(a1899)
| ~ c2_1(a1899)
| ~ spl0_19
| spl0_100 ),
inference(resolution,[],[f411,f818]) ).
fof(f1502,plain,
( c1_1(a1867)
| ~ c2_1(a1867)
| ~ spl0_19
| spl0_84 ),
inference(resolution,[],[f411,f738]) ).
fof(f1512,plain,
( ~ c0_1(a1877)
| c2_1(a1877)
| ~ spl0_21
| ~ spl0_144 ),
inference(resolution,[],[f419,f1037]) ).
fof(f1516,plain,
( ~ c0_1(a1864)
| c2_1(a1864)
| ~ spl0_21
| ~ spl0_122 ),
inference(resolution,[],[f419,f927]) ).
fof(f1522,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_29 ),
inference(resolution,[],[f455,f375]) ).
fof(f1526,plain,
( ~ c0_1(a1911)
| c1_1(a1911)
| ~ spl0_29
| spl0_102 ),
inference(resolution,[],[f455,f828]) ).
fof(f1527,plain,
( ~ c0_1(a1899)
| c1_1(a1899)
| ~ spl0_29
| spl0_100 ),
inference(resolution,[],[f455,f818]) ).
fof(f1540,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_29 ),
inference(duplicate_literal_removal,[],[f1522]) ).
fof(f1568,plain,
( ~ c2_1(a1919)
| c1_1(a1919)
| ~ spl0_35
| ~ spl0_138 ),
inference(resolution,[],[f484,f1007]) ).
fof(f1569,plain,
( ~ c2_1(a1898)
| c1_1(a1898)
| ~ spl0_35
| ~ spl0_135 ),
inference(resolution,[],[f484,f992]) ).
fof(f1571,plain,
( ~ c2_1(a1866)
| c1_1(a1866)
| ~ spl0_35
| ~ spl0_124 ),
inference(resolution,[],[f484,f937]) ).
fof(f1572,plain,
( ~ c2_1(a1864)
| c1_1(a1864)
| ~ spl0_35
| ~ spl0_122 ),
inference(resolution,[],[f484,f927]) ).
fof(f1577,plain,
( spl0_78
| ~ spl0_174
| ~ spl0_35
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1572,f925,f483,f1374,f706]) ).
fof(f1579,plain,
( spl0_98
| ~ spl0_162
| ~ spl0_35
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1569,f990,f483,f1193,f806]) ).
fof(f1611,plain,
( ~ c1_1(a1858)
| ~ spl0_2
| ~ spl0_10
| ~ spl0_165 ),
inference(resolution,[],[f1211,f1279]) ).
fof(f1619,plain,
( ~ c0_1(a1874)
| ~ spl0_9
| ~ spl0_29
| spl0_91 ),
inference(resolution,[],[f1540,f773]) ).
fof(f1631,plain,
( ~ spl0_131
| ~ spl0_9
| ~ spl0_29
| spl0_91 ),
inference(avatar_split_clause,[],[f1619,f771,f454,f374,f970]) ).
fof(f1638,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_2 ),
inference(resolution,[],[f348,f351]) ).
fof(f1650,plain,
( ~ c0_1(a1867)
| ~ c2_1(a1867)
| ~ spl0_1
| spl0_84 ),
inference(resolution,[],[f348,f738]) ).
fof(f1652,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_2 ),
inference(duplicate_literal_removal,[],[f1638]) ).
fof(f1654,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_5
| ~ spl0_9 ),
inference(resolution,[],[f362,f375]) ).
fof(f1669,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_5
| ~ spl0_9 ),
inference(duplicate_literal_removal,[],[f1654]) ).
fof(f1673,plain,
( c0_1(a1898)
| c1_1(a1898)
| ~ spl0_15
| ~ spl0_162 ),
inference(resolution,[],[f397,f1195]) ).
fof(f1679,plain,
( c0_1(a1867)
| c1_1(a1867)
| ~ spl0_15
| ~ spl0_85 ),
inference(resolution,[],[f397,f743]) ).
fof(f1681,plain,
( c0_1(a1855)
| c1_1(a1855)
| ~ spl0_15
| ~ spl0_65 ),
inference(resolution,[],[f397,f643]) ).
fof(f1697,plain,
( ~ spl0_85
| spl0_86
| ~ spl0_19
| spl0_84 ),
inference(avatar_split_clause,[],[f1502,f736,f410,f746,f741]) ).
fof(f1704,plain,
( ~ spl0_142
| ~ spl0_2
| ~ spl0_10
| ~ spl0_165 ),
inference(avatar_split_clause,[],[f1611,f1209,f378,f350,f1025]) ).
fof(f1712,plain,
( ~ spl0_151
| ~ spl0_152
| ~ spl0_7
| spl0_150 ),
inference(avatar_split_clause,[],[f1219,f1065,f367,f1075,f1070]) ).
fof(f1716,plain,
( ~ spl0_132
| ~ spl0_133
| ~ spl0_7
| spl0_161 ),
inference(avatar_split_clause,[],[f1229,f1188,f367,f980,f975]) ).
fof(f1731,plain,
( spl0_18
| ~ spl0_5
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1669,f374,f361,f406]) ).
fof(f1737,plain,
( spl0_105
| ~ spl0_104
| ~ spl0_35
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1568,f1005,f483,f836,f841]) ).
fof(f1742,plain,
( spl0_11
| ~ spl0_1
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f1652,f350,f347,f381]) ).
fof(f1750,plain,
( c0_1(a1866)
| c1_1(a1866)
| ~ spl0_15
| ~ spl0_82 ),
inference(resolution,[],[f728,f397]) ).
fof(f1755,plain,
( c0_1(a1919)
| c1_1(a1919)
| ~ spl0_15
| ~ spl0_104 ),
inference(resolution,[],[f838,f397]) ).
fof(f1760,plain,
( ~ c2_1(a1858)
| ~ c1_1(a1858)
| ~ spl0_2
| ~ spl0_141 ),
inference(resolution,[],[f1022,f351]) ).
fof(f1798,plain,
( ~ c0_1(a1877)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_166 ),
inference(resolution,[],[f1291,f1216]) ).
fof(f1802,plain,
( ~ c0_1(a1875)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_132 ),
inference(resolution,[],[f1291,f977]) ).
fof(f1809,plain,
( ~ c0_1(a1862)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_119 ),
inference(resolution,[],[f1291,f912]) ).
fof(f1817,plain,
( ~ spl0_120
| ~ spl0_7
| ~ spl0_11
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1809,f910,f381,f367,f915]) ).
fof(f1819,plain,
( ~ spl0_133
| ~ spl0_7
| ~ spl0_11
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1802,f975,f381,f367,f980]) ).
fof(f1821,plain,
( ~ spl0_146
| ~ spl0_7
| ~ spl0_11
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f1798,f1214,f381,f367,f1045]) ).
fof(f1823,plain,
( ~ spl0_159
| ~ spl0_127
| ~ spl0_10
| spl0_88 ),
inference(avatar_split_clause,[],[f1270,f756,f378,f950,f1178]) ).
fof(f1831,plain,
( ~ spl0_160
| spl0_90
| ~ spl0_16
| spl0_129 ),
inference(avatar_split_clause,[],[f1445,f960,f399,f766,f1183]) ).
fof(f1834,plain,
( ~ spl0_157
| spl0_70
| ~ spl0_16
| spl0_116 ),
inference(avatar_split_clause,[],[f1452,f895,f399,f666,f1167]) ).
fof(f1842,plain,
( spl0_18
| ~ spl0_6
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1429,f392,f364,f406]) ).
fof(f1853,plain,
( ~ spl0_153
| spl0_83
| ~ spl0_13
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1295,f935,f389,f731,f1123]) ).
fof(f1855,plain,
( spl0_98
| spl0_99
| ~ spl0_15
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f1673,f1193,f396,f811,f806]) ).
fof(f1858,plain,
( spl0_103
| ~ spl0_137
| ~ spl0_29
| spl0_102 ),
inference(avatar_split_clause,[],[f1526,f826,f454,f1000,f831]) ).
fof(f1865,plain,
( ~ c0_1(a1858)
| ~ c1_1(a1858)
| ~ spl0_4
| ~ spl0_141 ),
inference(resolution,[],[f358,f1022]) ).
fof(f1878,plain,
( ~ spl0_142
| ~ spl0_143
| ~ spl0_4
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f1865,f1020,f357,f1030,f1025]) ).
fof(f1885,plain,
( c1_1(a1898)
| c2_1(a1898)
| ~ spl0_6
| ~ spl0_135 ),
inference(resolution,[],[f365,f992]) ).
fof(f1887,plain,
( c1_1(a1872)
| c2_1(a1872)
| ~ spl0_6
| ~ spl0_128 ),
inference(resolution,[],[f365,f957]) ).
fof(f1891,plain,
( c1_1(a1864)
| c2_1(a1864)
| ~ spl0_6
| ~ spl0_122 ),
inference(resolution,[],[f365,f927]) ).
fof(f1900,plain,
( c0_1(a1898)
| c2_1(a1898)
| ~ spl0_8
| ~ spl0_135 ),
inference(resolution,[],[f372,f992]) ).
fof(f1902,plain,
( c0_1(a1872)
| c2_1(a1872)
| ~ spl0_8
| ~ spl0_128 ),
inference(resolution,[],[f372,f957]) ).
fof(f1916,plain,
( ~ c1_1(a1899)
| ~ c2_1(a1899)
| ~ spl0_10
| spl0_100 ),
inference(resolution,[],[f379,f818]) ).
fof(f1938,plain,
( ~ c0_1(a1862)
| ~ c1_1(a1862)
| ~ spl0_11
| ~ spl0_75 ),
inference(resolution,[],[f382,f693]) ).
fof(f1946,plain,
( ~ spl0_119
| ~ spl0_120
| ~ spl0_11
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1938,f691,f381,f915,f910]) ).
fof(f1950,plain,
( ~ spl0_85
| ~ spl0_167
| ~ spl0_1
| spl0_84 ),
inference(avatar_split_clause,[],[f1650,f736,f347,f1319,f741]) ).
fof(f1964,plain,
( ~ spl0_171
| spl0_105
| ~ spl0_9
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1481,f1005,f374,f841,f1340]) ).
fof(f1965,plain,
( ~ spl0_123
| spl0_78
| ~ spl0_9
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1484,f925,f374,f706,f930]) ).
fof(f1969,plain,
( ~ spl0_123
| ~ spl0_174
| ~ spl0_17
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1368,f925,f402,f1374,f930]) ).
fof(f1971,plain,
( ~ spl0_161
| ~ spl0_132
| ~ spl0_10
| spl0_92 ),
inference(avatar_split_clause,[],[f1471,f776,f378,f975,f1188]) ).
fof(f1994,plain,
( ~ c0_1(a1899)
| ~ c2_1(a1899)
| ~ spl0_1
| spl0_100 ),
inference(resolution,[],[f348,f818]) ).
fof(f2004,plain,
( c2_1(a1863)
| c1_1(a1863)
| ~ spl0_5
| spl0_76 ),
inference(resolution,[],[f362,f698]) ).
fof(f2005,plain,
( c2_1(a1857)
| c1_1(a1857)
| ~ spl0_5
| spl0_69 ),
inference(resolution,[],[f362,f663]) ).
fof(f2030,plain,
( ~ c0_1(a1899)
| ~ c1_1(a1899)
| ~ spl0_12
| spl0_100 ),
inference(resolution,[],[f385,f818]) ).
fof(f2031,plain,
( ~ c0_1(a1875)
| ~ c1_1(a1875)
| ~ spl0_12
| spl0_92 ),
inference(resolution,[],[f385,f778]) ).
fof(f2039,plain,
( ~ spl0_132
| ~ spl0_133
| ~ spl0_12
| spl0_92 ),
inference(avatar_split_clause,[],[f2031,f776,f384,f980,f975]) ).
fof(f2060,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_17 ),
inference(resolution,[],[f403,f348]) ).
fof(f2077,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f2060]) ).
fof(f2088,plain,
( ~ c0_1(a1852)
| ~ spl0_1
| ~ spl0_17
| ~ spl0_62 ),
inference(resolution,[],[f2077,f628]) ).
fof(f2116,plain,
( ~ c1_1(a1878)
| c2_1(a1878)
| ~ spl0_23
| ~ spl0_147 ),
inference(resolution,[],[f427,f1052]) ).
fof(f2117,plain,
( ~ c1_1(a1877)
| c2_1(a1877)
| ~ spl0_23
| ~ spl0_144 ),
inference(resolution,[],[f427,f1037]) ).
fof(f2118,plain,
( ~ c1_1(a1858)
| c2_1(a1858)
| ~ spl0_23
| ~ spl0_141 ),
inference(resolution,[],[f427,f1022]) ).
fof(f2121,plain,
( ~ c1_1(a1872)
| c2_1(a1872)
| ~ spl0_23
| ~ spl0_128 ),
inference(resolution,[],[f427,f957]) ).
fof(f2133,plain,
( spl0_145
| ~ spl0_166
| ~ spl0_23
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2117,f1035,f426,f1214,f1040]) ).
fof(f2139,plain,
( ~ c1_1(a1870)
| c0_1(a1870)
| ~ spl0_32
| ~ spl0_159 ),
inference(resolution,[],[f469,f1180]) ).
fof(f2141,plain,
( ~ c1_1(a1866)
| c0_1(a1866)
| ~ spl0_32
| ~ spl0_82 ),
inference(resolution,[],[f469,f728]) ).
fof(f2143,plain,
( ~ c1_1(a1860)
| c0_1(a1860)
| ~ spl0_32
| ~ spl0_71 ),
inference(resolution,[],[f469,f673]) ).
fof(f2144,plain,
( ~ c1_1(a1853)
| c0_1(a1853)
| ~ spl0_32
| ~ spl0_154 ),
inference(resolution,[],[f469,f1129]) ).
fof(f2152,plain,
( spl0_63
| ~ spl0_111
| ~ spl0_32
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f2144,f1128,f468,f870,f631]) ).
fof(f2153,plain,
( spl0_72
| ~ spl0_117
| ~ spl0_32
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f2143,f671,f468,f900,f676]) ).
fof(f2154,plain,
( spl0_83
| ~ spl0_153
| ~ spl0_32
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f2141,f726,f468,f1123,f731]) ).
fof(f2156,plain,
( spl0_89
| ~ spl0_127
| ~ spl0_32
| ~ spl0_159 ),
inference(avatar_split_clause,[],[f2139,f1178,f468,f950,f761]) ).
fof(f2160,plain,
( spl0_162
| spl0_98
| ~ spl0_6
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1885,f990,f364,f806,f1193]) ).
fof(f2162,plain,
( spl0_174
| spl0_78
| ~ spl0_6
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1891,f925,f364,f706,f1374]) ).
fof(f2168,plain,
( spl0_162
| spl0_99
| ~ spl0_8
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1900,f990,f371,f811,f1193]) ).
fof(f2175,plain,
( spl0_98
| spl0_99
| ~ spl0_15
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f1673,f1193,f396,f811,f806]) ).
fof(f2177,plain,
( spl0_86
| spl0_167
| ~ spl0_15
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f1679,f741,f396,f1319,f746]) ).
fof(f2180,plain,
( spl0_153
| spl0_83
| ~ spl0_15
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f1750,f726,f396,f731,f1123]) ).
fof(f2189,plain,
( spl0_148
| ~ spl0_149
| ~ spl0_23
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f2116,f1050,f426,f1060,f1055]) ).
fof(f2193,plain,
( ~ spl0_173
| ~ spl0_1
| ~ spl0_17
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f2088,f626,f402,f347,f1356]) ).
fof(f2202,plain,
( ~ spl0_111
| ~ spl0_154
| ~ spl0_2
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1119,f865,f350,f1128,f870]) ).
fof(f2207,plain,
( ~ spl0_142
| ~ spl0_165
| ~ spl0_2
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f1760,f1020,f350,f1209,f1025]) ).
fof(f2208,plain,
( ~ spl0_163
| ~ spl0_136
| ~ spl0_12
| spl0_100 ),
inference(avatar_split_clause,[],[f2030,f816,f384,f995,f1198]) ).
fof(f2210,plain,
( ~ spl0_101
| spl0_163
| ~ spl0_19
| spl0_100 ),
inference(avatar_split_clause,[],[f1492,f816,f410,f1198,f821]) ).
fof(f2211,plain,
( spl0_163
| ~ spl0_136
| ~ spl0_29
| spl0_100 ),
inference(avatar_split_clause,[],[f1527,f816,f454,f995,f1198]) ).
fof(f2213,plain,
( spl0_129
| spl0_160
| ~ spl0_6
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1887,f955,f364,f1183,f960]) ).
fof(f2218,plain,
( ~ spl0_101
| ~ spl0_136
| ~ spl0_1
| spl0_100 ),
inference(avatar_split_clause,[],[f1994,f816,f347,f995,f821]) ).
fof(f2222,plain,
( spl0_129
| spl0_90
| ~ spl0_8
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1902,f955,f371,f766,f960]) ).
fof(f2226,plain,
( ~ spl0_101
| ~ spl0_163
| ~ spl0_10
| spl0_100 ),
inference(avatar_split_clause,[],[f1916,f816,f378,f1198,f821]) ).
fof(f2227,plain,
( ~ spl0_160
| spl0_90
| ~ spl0_13
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1294,f955,f389,f766,f1183]) ).
fof(f2229,plain,
( ~ spl0_111
| spl0_63
| ~ spl0_13
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f1297,f865,f389,f631,f870]) ).
fof(f2230,plain,
( ~ spl0_109
| spl0_173
| ~ spl0_13
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1298,f855,f389,f1356,f860]) ).
fof(f2232,plain,
( spl0_165
| ~ spl0_142
| ~ spl0_23
| ~ spl0_141 ),
inference(avatar_split_clause,[],[f2118,f1020,f426,f1025,f1209]) ).
fof(f2233,plain,
( spl0_129
| ~ spl0_160
| ~ spl0_23
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f2121,f955,f426,f1183,f960]) ).
fof(f2236,plain,
( spl0_98
| ~ spl0_162
| ~ spl0_35
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1569,f990,f483,f1193,f806]) ).
fof(f2237,plain,
( spl0_153
| ~ spl0_82
| ~ spl0_35
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1571,f935,f483,f726,f1123]) ).
fof(f2249,plain,
( spl0_77
| spl0_121
| ~ spl0_5
| spl0_76 ),
inference(avatar_split_clause,[],[f2004,f696,f361,f920,f701]) ).
fof(f2250,plain,
( spl0_157
| spl0_116
| ~ spl0_5
| spl0_69 ),
inference(avatar_split_clause,[],[f2005,f661,f361,f895,f1167]) ).
fof(f2259,plain,
( spl0_66
| spl0_67
| ~ spl0_15
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f1681,f641,f396,f651,f646]) ).
fof(f2260,plain,
( spl0_105
| spl0_171
| ~ spl0_15
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f1755,f836,f396,f1340,f841]) ).
fof(f2263,plain,
( spl0_145
| ~ spl0_146
| ~ spl0_21
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1512,f1035,f418,f1045,f1040]) ).
fof(f2268,plain,
( spl0_174
| ~ spl0_123
| ~ spl0_21
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1516,f925,f418,f930,f1374]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f359]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f369]) ).
cnf(s3,plain,
( spl0_2
| ~ spl0_3
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f376]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f386]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_6
| spl0_8
| spl0_10 ),
inference(sat_conversion,[],[f387]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_5
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f394]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_15
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f404]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_15
| spl0_16
| spl0_18 ),
inference(sat_conversion,[],[f408]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_9
| spl0_10
| spl0_19 ),
inference(sat_conversion,[],[f412]) ).
cnf(s10,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f420]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_11
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f428]) ).
cnf(s14,plain,
( spl0_1
| ~ spl0_3
| spl0_21
| ~ spl0_26 ),
inference(sat_conversion,[],[f443]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_6
| spl0_11
| ~ spl0_27 ),
inference(sat_conversion,[],[f448]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f456]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_8
| spl0_12
| spl0_30 ),
inference(sat_conversion,[],[f461]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_11
| spl0_13
| ~ spl0_20 ),
inference(sat_conversion,[],[f462]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_21
| ~ spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f470]) ).
cnf(s20,plain,
( spl0_2
| ~ spl0_3
| spl0_29
| ~ spl0_33 ),
inference(sat_conversion,[],[f475]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_5
| spl0_8
| spl0_30 ),
inference(sat_conversion,[],[f476]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_8
| spl0_29
| ~ spl0_34 ),
inference(sat_conversion,[],[f481]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_16
| ~ spl0_31
| spl0_35 ),
inference(sat_conversion,[],[f485]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_11
| spl0_32
| ~ spl0_40 ),
inference(sat_conversion,[],[f506]) ).
cnf(s29,plain,
( spl0_1
| ~ spl0_3
| spl0_35
| ~ spl0_44 ),
inference(sat_conversion,[],[f524]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_15
| spl0_35
| spl0_49 ),
inference(sat_conversion,[],[f546]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_26
| spl0_50 ),
inference(sat_conversion,[],[f565]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_40
| ~ spl0_52 ),
inference(sat_conversion,[],[f566]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_17
| spl0_30
| spl0_55 ),
inference(sat_conversion,[],[f576]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_11
| spl0_22
| ~ spl0_52 ),
inference(sat_conversion,[],[f577]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_9
| ~ spl0_52
| ~ spl0_56 ),
inference(sat_conversion,[],[f583]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_18
| ~ spl0_27
| ~ spl0_31 ),
inference(sat_conversion,[],[f584]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_5
| ~ spl0_31
| ~ spl0_56 ),
inference(sat_conversion,[],[f588]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_35
| ~ spl0_44
| spl0_57 ),
inference(sat_conversion,[],[f593]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_32
| ~ spl0_44
| spl0_49 ),
inference(sat_conversion,[],[f597]) ).
cnf(s61,plain,
( ~ spl0_3
| spl0_19
| ~ spl0_20
| spl0_55 ),
inference(sat_conversion,[],[f615]) ).
cnf(s67,plain,
( ~ spl0_50
| spl0_62 ),
inference(sat_conversion,[],[f629]) ).
cnf(s68,plain,
( ~ spl0_49
| ~ spl0_63 ),
inference(sat_conversion,[],[f634]) ).
cnf(s70,plain,
( spl0_40
| spl0_65 ),
inference(sat_conversion,[],[f644]) ).
cnf(s71,plain,
( spl0_40
| ~ spl0_66 ),
inference(sat_conversion,[],[f649]) ).
cnf(s72,plain,
( spl0_40
| ~ spl0_67 ),
inference(sat_conversion,[],[f654]) ).
cnf(s74,plain,
( spl0_33
| ~ spl0_69 ),
inference(sat_conversion,[],[f664]) ).
cnf(s75,plain,
( spl0_33
| ~ spl0_70 ),
inference(sat_conversion,[],[f669]) ).
cnf(s76,plain,
( ~ spl0_43
| spl0_71 ),
inference(sat_conversion,[],[f674]) ).
cnf(s77,plain,
( ~ spl0_43
| ~ spl0_72 ),
inference(sat_conversion,[],[f679]) ).
cnf(s80,plain,
( spl0_31
| spl0_75 ),
inference(sat_conversion,[],[f694]) ).
cnf(s81,plain,
( spl0_44
| ~ spl0_76 ),
inference(sat_conversion,[],[f699]) ).
cnf(s82,plain,
( spl0_44
| ~ spl0_77 ),
inference(sat_conversion,[],[f704]) ).
cnf(s83,plain,
( ~ spl0_22
| ~ spl0_78 ),
inference(sat_conversion,[],[f709]) ).
cnf(s87,plain,
( ~ spl0_60
| spl0_82 ),
inference(sat_conversion,[],[f729]) ).
cnf(s88,plain,
( ~ spl0_60
| ~ spl0_83 ),
inference(sat_conversion,[],[f734]) ).
cnf(s89,plain,
( ~ spl0_57
| ~ spl0_84 ),
inference(sat_conversion,[],[f739]) ).
cnf(s90,plain,
( ~ spl0_57
| spl0_85 ),
inference(sat_conversion,[],[f744]) ).
cnf(s91,plain,
( ~ spl0_57
| ~ spl0_86 ),
inference(sat_conversion,[],[f749]) ).
cnf(s93,plain,
( spl0_34
| ~ spl0_88 ),
inference(sat_conversion,[],[f759]) ).
cnf(s94,plain,
( spl0_34
| ~ spl0_89 ),
inference(sat_conversion,[],[f764]) ).
cnf(s95,plain,
( spl0_20
| ~ spl0_90 ),
inference(sat_conversion,[],[f769]) ).
cnf(s96,plain,
( ~ spl0_47
| ~ spl0_91 ),
inference(sat_conversion,[],[f774]) ).
cnf(s97,plain,
( spl0_27
| ~ spl0_92 ),
inference(sat_conversion,[],[f779]) ).
cnf(s103,plain,
( spl0_28
| ~ spl0_98 ),
inference(sat_conversion,[],[f809]) ).
cnf(s104,plain,
( spl0_28
| ~ spl0_99 ),
inference(sat_conversion,[],[f814]) ).
cnf(s105,plain,
( ~ spl0_55
| ~ spl0_100 ),
inference(sat_conversion,[],[f819]) ).
cnf(s106,plain,
( ~ spl0_55
| spl0_101 ),
inference(sat_conversion,[],[f824]) ).
cnf(s107,plain,
( spl0_56
| ~ spl0_102 ),
inference(sat_conversion,[],[f829]) ).
cnf(s108,plain,
( spl0_56
| ~ spl0_103 ),
inference(sat_conversion,[],[f834]) ).
cnf(s109,plain,
( spl0_26
| spl0_104 ),
inference(sat_conversion,[],[f839]) ).
cnf(s110,plain,
( spl0_26
| ~ spl0_105 ),
inference(sat_conversion,[],[f844]) ).
cnf(s112,plain,
( ~ spl0_50
| spl0_108 ),
inference(sat_conversion,[],[f858]) ).
cnf(s113,plain,
( ~ spl0_50
| spl0_109 ),
inference(sat_conversion,[],[f863]) ).
cnf(s114,plain,
( ~ spl0_49
| spl0_110 ),
inference(sat_conversion,[],[f868]) ).
cnf(s115,plain,
( ~ spl0_49
| spl0_111 ),
inference(sat_conversion,[],[f873]) ).
cnf(s120,plain,
( spl0_33
| ~ spl0_116 ),
inference(sat_conversion,[],[f898]) ).
cnf(s121,plain,
( ~ spl0_43
| spl0_117 ),
inference(sat_conversion,[],[f903]) ).
cnf(s123,plain,
( spl0_31
| spl0_119 ),
inference(sat_conversion,[],[f913]) ).
cnf(s124,plain,
( spl0_31
| spl0_120 ),
inference(sat_conversion,[],[f918]) ).
cnf(s125,plain,
( spl0_44
| ~ spl0_121 ),
inference(sat_conversion,[],[f923]) ).
cnf(s126,plain,
( ~ spl0_22
| spl0_122 ),
inference(sat_conversion,[],[f928]) ).
cnf(s127,plain,
( ~ spl0_22
| spl0_123 ),
inference(sat_conversion,[],[f933]) ).
cnf(s128,plain,
( ~ spl0_60
| spl0_124 ),
inference(sat_conversion,[],[f938]) ).
cnf(s131,plain,
( spl0_34
| spl0_127 ),
inference(sat_conversion,[],[f953]) ).
cnf(s132,plain,
( spl0_20
| spl0_128 ),
inference(sat_conversion,[],[f958]) ).
cnf(s133,plain,
( spl0_20
| ~ spl0_129 ),
inference(sat_conversion,[],[f963]) ).
cnf(s134,plain,
( ~ spl0_47
| ~ spl0_130 ),
inference(sat_conversion,[],[f968]) ).
cnf(s135,plain,
( ~ spl0_47
| spl0_131 ),
inference(sat_conversion,[],[f973]) ).
cnf(s136,plain,
( spl0_27
| spl0_132 ),
inference(sat_conversion,[],[f978]) ).
cnf(s137,plain,
( spl0_27
| spl0_133 ),
inference(sat_conversion,[],[f983]) ).
cnf(s139,plain,
( spl0_28
| spl0_135 ),
inference(sat_conversion,[],[f993]) ).
cnf(s140,plain,
( ~ spl0_55
| spl0_136 ),
inference(sat_conversion,[],[f998]) ).
cnf(s141,plain,
( spl0_56
| spl0_137 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s142,plain,
( spl0_26
| spl0_138 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s145,plain,
( spl0_52
| spl0_141 ),
inference(sat_conversion,[],[f1023]) ).
cnf(s146,plain,
( spl0_52
| spl0_142 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s147,plain,
( spl0_52
| spl0_143 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s148,plain,
( ~ spl0_30
| spl0_144 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s149,plain,
( ~ spl0_30
| ~ spl0_145 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s150,plain,
( ~ spl0_30
| spl0_146 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s151,plain,
( ~ spl0_53
| spl0_147 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s152,plain,
( ~ spl0_53
| ~ spl0_148 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s153,plain,
( ~ spl0_53
| spl0_149 ),
inference(sat_conversion,[],[f1063]) ).
cnf(s154,plain,
( ~ spl0_24
| ~ spl0_150 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s155,plain,
( ~ spl0_24
| spl0_151 ),
inference(sat_conversion,[],[f1073]) ).
cnf(s156,plain,
( ~ spl0_24
| spl0_152 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s160,plain,
( spl0_22
| spl0_50
| spl0_53 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s161,plain,
( ~ spl0_27
| spl0_43
| spl0_49 ),
inference(sat_conversion,[],[f1083]) ).
cnf(s162,plain,
( ~ spl0_27
| spl0_55
| spl0_60 ),
inference(sat_conversion,[],[f1084]) ).
cnf(s163,plain,
( spl0_22
| ~ spl0_27
| ~ spl0_34 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s164,plain,
( spl0_22
| ~ spl0_26
| ~ spl0_31 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s165,plain,
( ~ spl0_20
| ~ spl0_31
| spl0_47 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s166,plain,
( spl0_24
| spl0_30
| spl0_49 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s168,plain,
( spl0_3
| ~ spl0_49 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s194,plain,
( spl0_3
| ~ spl0_30 ),
inference(sat_conversion,[],[f1116]) ).
cnf(s196,plain,
( spl0_3
| ~ spl0_24 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s220,plain,
( ~ spl0_9
| ~ spl0_144
| ~ spl0_146
| spl0_166 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s221,plain,
( ~ spl0_7
| spl0_145
| ~ spl0_146
| ~ spl0_166 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s222,plain,
( ~ spl0_2
| ~ spl0_62
| ~ spl0_108
| ~ spl0_109 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s223,plain,
( ~ spl0_2
| ~ spl0_10
| ~ spl0_75
| ~ spl0_119 ),
inference(sat_conversion,[],[f1285]) ).
cnf(s235,plain,
( ~ spl0_18
| spl0_78
| ~ spl0_123
| spl0_174 ),
inference(sat_conversion,[],[f1408]) ).
cnf(s239,plain,
( ~ spl0_18
| spl0_145
| ~ spl0_146
| spl0_166 ),
inference(sat_conversion,[],[f1414]) ).
cnf(s241,plain,
( ~ spl0_16
| spl0_63
| ~ spl0_111
| spl0_154 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s242,plain,
( ~ spl0_16
| spl0_89
| ~ spl0_127
| spl0_159 ),
inference(sat_conversion,[],[f1462]) ).
cnf(s245,plain,
( ~ spl0_18
| spl0_91
| spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f1465]) ).
cnf(s259,plain,
( ~ spl0_35
| spl0_78
| ~ spl0_122
| ~ spl0_174 ),
inference(sat_conversion,[],[f1577]) ).
cnf(s261,plain,
( ~ spl0_35
| spl0_98
| ~ spl0_135
| ~ spl0_162 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s279,plain,
( ~ spl0_9
| ~ spl0_29
| spl0_91
| ~ spl0_131 ),
inference(sat_conversion,[],[f1631]) ).
cnf(s297,plain,
( ~ spl0_19
| spl0_84
| ~ spl0_85
| spl0_86 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s304,plain,
( ~ spl0_2
| ~ spl0_10
| ~ spl0_142
| ~ spl0_165 ),
inference(sat_conversion,[],[f1704]) ).
cnf(s311,plain,
( ~ spl0_7
| spl0_150
| ~ spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s315,plain,
( ~ spl0_7
| ~ spl0_132
| ~ spl0_133
| spl0_161 ),
inference(sat_conversion,[],[f1716]) ).
cnf(s330,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_18 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s336,plain,
( ~ spl0_35
| ~ spl0_104
| spl0_105
| ~ spl0_138 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s341,plain,
( ~ spl0_1
| ~ spl0_2
| spl0_11 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s359,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_119
| ~ spl0_120 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s361,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f1819]) ).
cnf(s363,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_146
| ~ spl0_166 ),
inference(sat_conversion,[],[f1821]) ).
cnf(s365,plain,
( ~ spl0_10
| spl0_88
| ~ spl0_127
| ~ spl0_159 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s373,plain,
( ~ spl0_16
| spl0_90
| spl0_129
| ~ spl0_160 ),
inference(sat_conversion,[],[f1831]) ).
cnf(s376,plain,
( ~ spl0_16
| spl0_70
| spl0_116
| ~ spl0_157 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s384,plain,
( ~ spl0_6
| ~ spl0_14
| spl0_18 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s395,plain,
( ~ spl0_13
| spl0_83
| ~ spl0_124
| ~ spl0_153 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s397,plain,
( ~ spl0_15
| spl0_98
| spl0_99
| ~ spl0_162 ),
inference(sat_conversion,[],[f1855]) ).
cnf(s400,plain,
( ~ spl0_29
| spl0_102
| spl0_103
| ~ spl0_137 ),
inference(sat_conversion,[],[f1858]) ).
cnf(s407,plain,
( ~ spl0_4
| ~ spl0_141
| ~ spl0_142
| ~ spl0_143 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s414,plain,
( ~ spl0_11
| ~ spl0_75
| ~ spl0_119
| ~ spl0_120 ),
inference(sat_conversion,[],[f1946]) ).
cnf(s418,plain,
( ~ spl0_1
| spl0_84
| ~ spl0_85
| ~ spl0_167 ),
inference(sat_conversion,[],[f1950]) ).
cnf(s432,plain,
( ~ spl0_9
| spl0_105
| ~ spl0_138
| ~ spl0_171 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s433,plain,
( ~ spl0_9
| spl0_78
| ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s441,plain,
( ~ spl0_17
| ~ spl0_122
| ~ spl0_123
| ~ spl0_174 ),
inference(sat_conversion,[],[f1969]) ).
cnf(s443,plain,
( ~ spl0_10
| spl0_92
| ~ spl0_132
| ~ spl0_161 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s446,plain,
( ~ spl0_12
| spl0_92
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f2039]) ).
cnf(s449,plain,
( ~ spl0_23
| ~ spl0_144
| spl0_145
| ~ spl0_166 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s451,plain,
( ~ spl0_32
| spl0_63
| ~ spl0_111
| ~ spl0_154 ),
inference(sat_conversion,[],[f2152]) ).
cnf(s452,plain,
( ~ spl0_32
| ~ spl0_71
| spl0_72
| ~ spl0_117 ),
inference(sat_conversion,[],[f2153]) ).
cnf(s453,plain,
( ~ spl0_32
| ~ spl0_82
| spl0_83
| ~ spl0_153 ),
inference(sat_conversion,[],[f2154]) ).
cnf(s455,plain,
( ~ spl0_32
| spl0_89
| ~ spl0_127
| ~ spl0_159 ),
inference(sat_conversion,[],[f2156]) ).
cnf(s459,plain,
( ~ spl0_6
| spl0_98
| ~ spl0_135
| spl0_162 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s461,plain,
( ~ spl0_6
| spl0_78
| ~ spl0_122
| spl0_174 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s467,plain,
( ~ spl0_8
| spl0_99
| ~ spl0_135
| spl0_162 ),
inference(sat_conversion,[],[f2168]) ).
cnf(s474,plain,
( ~ spl0_15
| spl0_98
| spl0_99
| ~ spl0_162 ),
inference(sat_conversion,[],[f2175]) ).
cnf(s476,plain,
( ~ spl0_15
| ~ spl0_85
| spl0_86
| spl0_167 ),
inference(sat_conversion,[],[f2177]) ).
cnf(s479,plain,
( ~ spl0_15
| ~ spl0_82
| spl0_83
| spl0_153 ),
inference(sat_conversion,[],[f2180]) ).
cnf(s488,plain,
( ~ spl0_23
| ~ spl0_147
| spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f2189]) ).
cnf(s492,plain,
( ~ spl0_1
| ~ spl0_17
| ~ spl0_62
| ~ spl0_173 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s501,plain,
( ~ spl0_2
| ~ spl0_110
| ~ spl0_111
| ~ spl0_154 ),
inference(sat_conversion,[],[f2202]) ).
cnf(s506,plain,
( ~ spl0_2
| ~ spl0_141
| ~ spl0_142
| ~ spl0_165 ),
inference(sat_conversion,[],[f2207]) ).
cnf(s507,plain,
( ~ spl0_12
| spl0_100
| ~ spl0_136
| ~ spl0_163 ),
inference(sat_conversion,[],[f2208]) ).
cnf(s509,plain,
( ~ spl0_19
| spl0_100
| ~ spl0_101
| spl0_163 ),
inference(sat_conversion,[],[f2210]) ).
cnf(s510,plain,
( ~ spl0_29
| spl0_100
| ~ spl0_136
| spl0_163 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s512,plain,
( ~ spl0_6
| ~ spl0_128
| spl0_129
| spl0_160 ),
inference(sat_conversion,[],[f2213]) ).
cnf(s516,plain,
( ~ spl0_1
| spl0_100
| ~ spl0_101
| ~ spl0_136 ),
inference(sat_conversion,[],[f2218]) ).
cnf(s524,plain,
( ~ spl0_8
| spl0_90
| ~ spl0_128
| spl0_129 ),
inference(sat_conversion,[],[f2222]) ).
cnf(s528,plain,
( ~ spl0_10
| spl0_100
| ~ spl0_101
| ~ spl0_163 ),
inference(sat_conversion,[],[f2226]) ).
cnf(s529,plain,
( ~ spl0_13
| spl0_90
| ~ spl0_128
| ~ spl0_160 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s531,plain,
( ~ spl0_13
| spl0_63
| ~ spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f2229]) ).
cnf(s532,plain,
( ~ spl0_13
| ~ spl0_108
| ~ spl0_109
| spl0_173 ),
inference(sat_conversion,[],[f2230]) ).
cnf(s534,plain,
( ~ spl0_23
| ~ spl0_141
| ~ spl0_142
| spl0_165 ),
inference(sat_conversion,[],[f2232]) ).
cnf(s535,plain,
( ~ spl0_23
| ~ spl0_128
| spl0_129
| ~ spl0_160 ),
inference(sat_conversion,[],[f2233]) ).
cnf(s538,plain,
( ~ spl0_35
| spl0_98
| ~ spl0_135
| ~ spl0_162 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s539,plain,
( ~ spl0_35
| ~ spl0_82
| ~ spl0_124
| spl0_153 ),
inference(sat_conversion,[],[f2237]) ).
cnf(s551,plain,
( ~ spl0_5
| spl0_76
| spl0_77
| spl0_121 ),
inference(sat_conversion,[],[f2249]) ).
cnf(s552,plain,
( ~ spl0_5
| spl0_69
| spl0_116
| spl0_157 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s561,plain,
( ~ spl0_15
| ~ spl0_65
| spl0_66
| spl0_67 ),
inference(sat_conversion,[],[f2259]) ).
cnf(s562,plain,
( ~ spl0_15
| ~ spl0_104
| spl0_105
| spl0_171 ),
inference(sat_conversion,[],[f2260]) ).
cnf(s566,plain,
( ~ spl0_21
| ~ spl0_144
| spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f2263]) ).
cnf(s571,plain,
( ~ spl0_21
| ~ spl0_122
| ~ spl0_123
| spl0_174 ),
inference(sat_conversion,[],[f2268]) ).
cnf(s574,plain,
spl0_3,
inference(rat,[],[s166,s168,s194,s196]) ).
cnf(s575,plain,
( spl0_8
| ~ spl0_7
| spl0_5
| spl0_2 ),
inference(rat,[],[s220,s221,s148,s149,s150,s3,s21,s574]) ).
cnf(s576,plain,
( ~ spl0_30
| ~ spl0_9
| ~ spl0_7 ),
inference(rat,[],[s220,s221,s148,s149,s150]) ).
cnf(s578,plain,
( spl0_11
| ~ spl0_7
| spl0_6 ),
inference(rat,[],[s4,s443,s446,s315,s97,s136,s137,s15,s574]) ).
cnf(s580,plain,
( spl0_27
| ~ spl0_11
| ~ spl0_7 ),
inference(rat,[],[s361,s136,s137]) ).
cnf(s581,plain,
( spl0_31
| ~ spl0_11
| ~ spl0_7 ),
inference(rat,[],[s359,s123,s124]) ).
cnf(s582,plain,
( ~ spl0_47
| ~ spl0_18 ),
inference(rat,[],[s245,s96,s134,s135]) ).
cnf(s583,plain,
( spl0_6
| spl0_5
| spl0_2 ),
inference(rat,[],[s524,s95,s132,s133,s165,s582,s45,s581,s580,s578,s575,s2,s574]) ).
cnf(s584,plain,
( spl0_20
| ~ spl0_8 ),
inference(rat,[],[s524,s95,s132,s133]) ).
cnf(s585,plain,
( ~ spl0_11
| ~ spl0_20
| ~ spl0_7 ),
inference(rat,[],[s582,s165,s45,s581,s580,s574]) ).
cnf(s586,plain,
( spl0_27
| spl0_11
| ~ spl0_7 ),
inference(rat,[],[s4,s443,s446,s315,s97,s136,s137,s574]) ).
cnf(s587,plain,
( ~ spl0_31
| ~ spl0_27
| ~ spl0_20 ),
inference(rat,[],[s582,s45,s165,s574]) ).
cnf(s588,plain,
( ~ spl0_49
| ~ spl0_13 ),
inference(rat,[],[s531,s68,s114,s115]) ).
cnf(s589,plain,
( ~ spl0_24
| ~ spl0_7 ),
inference(rat,[],[s311,s154,s155,s156]) ).
cnf(s590,plain,
( ~ spl0_7
| spl0_5
| spl0_2 ),
inference(rat,[],[s566,s148,s149,s150,s166,s589,s588,s18,s585,s10,s584,s575,s574]) ).
cnf(s591,plain,
( ~ spl0_31
| ~ spl0_8
| spl0_7
| ~ spl0_6
| spl0_5 ),
inference(rat,[],[s34,s474,s538,s467,s588,s103,s104,s139,s6,s16,s384,s400,s582,s107,s108,s141,s165,s49,s584,s574]) ).
cnf(s592,plain,
( spl0_31
| ~ spl0_11 ),
inference(rat,[],[s414,s80,s123,s124]) ).
cnf(s593,plain,
( ~ spl0_31
| spl0_7
| ~ spl0_6
| spl0_5 ),
inference(rat,[],[s242,s23,s455,s261,s459,s19,s103,s139,s94,s131,s566,s16,s22,s148,s149,s150,s400,s21,s107,s108,s141,s591,s49,s574]) ).
cnf(s596,plain,
( ~ spl0_43
| ~ spl0_32 ),
inference(rat,[],[s452,s76,s77,s121]) ).
cnf(s597,plain,
( spl0_28
| spl0_49
| ~ spl0_8 ),
inference(rat,[],[s34,s538,s397,s467,s103,s104,s139,s574]) ).
cnf(s598,plain,
( ~ spl0_55
| ~ spl0_29
| spl0_11 ),
inference(rat,[],[s4,s507,s528,s510,s105,s106,s140,s574]) ).
cnf(s600,plain,
( ~ spl0_60
| ~ spl0_15
| ~ spl0_13 ),
inference(rat,[],[s479,s395,s87,s88,s128]) ).
cnf(s601,plain,
( spl0_56
| ~ spl0_29 ),
inference(rat,[],[s400,s107,s108,s141]) ).
cnf(s602,plain,
( spl0_52
| ~ spl0_4 ),
inference(rat,[],[s407,s145,s146,s147]) ).
cnf(s603,plain,
( spl0_5
| ~ spl0_52
| spl0_2 ),
inference(rat,[],[s18,s588,s584,s34,s3,s561,s259,s433,s461,s70,s71,s72,s83,s126,s127,s39,s42,s592,s593,s590,s583,s574]) ).
cnf(s604,plain,
( spl0_11
| ~ spl0_21
| ~ spl0_20
| spl0_15
| ~ spl0_52 ),
inference(rat,[],[s34,s259,s571,s588,s83,s126,s127,s18,s42,s574]) ).
cnf(s605,plain,
( spl0_18
| spl0_15
| ~ spl0_52
| spl0_2 ),
inference(rat,[],[s552,s376,s74,s75,s120,s20,s601,s44,s8,s330,s603,s574]) ).
cnf(s606,plain,
( ~ spl0_20
| spl0_15
| ~ spl0_52
| spl0_2 ),
inference(rat,[],[s592,s604,s165,s10,s582,s605,s574]) ).
cnf(s607,plain,
( ~ spl0_22
| ~ spl0_9 ),
inference(rat,[],[s433,s83,s126,s127]) ).
cnf(s608,plain,
( spl0_44
| ~ spl0_5 ),
inference(rat,[],[s551,s81,s82,s125]) ).
cnf(s609,plain,
( ~ spl0_22
| ~ spl0_21
| ~ spl0_35 ),
inference(rat,[],[s259,s571,s83,s126,s127]) ).
cnf(s610,plain,
( ~ spl0_20
| ~ spl0_35
| ~ spl0_52
| spl0_2 ),
inference(rat,[],[s561,s70,s71,s72,s39,s585,s42,s609,s606,s10,s574]) ).
cnf(s611,plain,
( ~ spl0_35
| spl0_2
| ~ spl0_52 ),
inference(rat,[],[s336,s109,s110,s142,s164,s592,s42,s607,s3,s584,s610,s574]) ).
cnf(s612,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s611,s29,s608,s603,s602,s1,s574]) ).
cnf(s613,plain,
( spl0_27
| ~ spl0_12 ),
inference(rat,[],[s446,s97,s136,s137]) ).
cnf(s614,plain,
( ~ spl0_60
| ~ spl0_13 ),
inference(rat,[],[s34,s539,s395,s600,s87,s88,s128,s588,s574]) ).
cnf(s615,plain,
( spl0_7
| spl0_5
| spl0_60
| ~ spl0_28
| spl0_11
| ~ spl0_2 ),
inference(rat,[],[s4,s613,s223,s162,s80,s123,s598,s593,s16,s2,s574]) ).
cnf(s616,plain,
( ~ spl0_7
| spl0_11
| ~ spl0_20
| ~ spl0_2 ),
inference(rat,[],[s509,s507,s9,s4,s223,s105,s106,s140,s80,s123,s576,s162,s587,s166,s586,s589,s588,s614,s18,s574]) ).
cnf(s617,plain,
( spl0_31
| ~ spl0_10
| ~ spl0_2 ),
inference(rat,[],[s223,s80,s123]) ).
cnf(s618,plain,
( spl0_11
| ~ spl0_8
| spl0_1 ),
inference(rat,[],[s336,s109,s110,s142,s14,s609,s11,s534,s304,s145,s146,s44,s279,s96,s135,s165,s617,s4,s613,s29,s162,s608,s601,s598,s615,s16,s616,s614,s597,s588,s18,s612,s584,s574]) ).
cnf(s619,plain,
( spl0_5
| ~ spl0_31
| spl0_7 ),
inference(rat,[],[s593,s2,s574]) ).
cnf(s620,plain,
( spl0_26
| ~ spl0_35 ),
inference(rat,[],[s336,s109,s110,s142]) ).
cnf(s621,plain,
( ~ spl0_8
| spl0_1 ),
inference(rat,[],[s609,s14,s164,s620,s29,s608,s619,s592,s585,s618,s584,s574]) ).
cnf(s622,plain,
( ~ spl0_20
| spl0_35
| spl0_5
| spl0_11
| ~ spl0_2 ),
inference(rat,[],[s397,s459,s103,s104,s139,s615,s34,s2,s614,s588,s616,s18,s574]) ).
cnf(s623,plain,
( spl0_40
| ~ spl0_15 ),
inference(rat,[],[s561,s70,s71,s72]) ).
cnf(s624,plain,
( ~ spl0_60
| ~ spl0_32
| ~ spl0_15 ),
inference(rat,[],[s453,s479,s87,s88]) ).
cnf(s625,plain,
( spl0_7
| spl0_90
| ~ spl0_128
| spl0_129
| spl0_5
| spl0_11
| ~ spl0_2 ),
inference(rat,[],[s397,s459,s103,s104,s139,s615,s624,s26,s623,s7,s441,s461,s83,s126,s127,s11,s373,s535,s512,s2,s574]) ).
cnf(s626,plain,
( spl0_5
| spl0_11
| spl0_1 ),
inference(rat,[],[s6,s384,s529,s239,s512,s221,s578,s625,s95,s132,s133,s622,s620,s14,s566,s148,s149,s150,s21,s612,s621,s574]) ).
cnf(s627,plain,
( spl0_11
| spl0_1 ),
inference(rat,[],[s506,s534,s145,s146,s11,s42,s609,s14,s620,s29,s608,s626,s612,s574]) ).
cnf(s628,plain,
( spl0_5
| spl0_1 ),
inference(rat,[],[s239,s45,s221,s580,s149,s150,s619,s21,s621,s592,s627,s574]) ).
cnf(s629,plain,
spl0_1,
inference(rat,[],[s609,s164,s14,s620,s29,s608,s628,s592,s627,s574]) ).
cnf(s630,plain,
( spl0_8
| spl0_5
| spl0_11 ),
inference(rat,[],[s449,s220,s11,s148,s149,s150,s607,s21,s3,s341,s574,s629]) ).
cnf(s631,plain,
( ~ spl0_30
| ~ spl0_21 ),
inference(rat,[],[s566,s148,s149,s150]) ).
cnf(s632,plain,
( ~ spl0_22
| ~ spl0_17
| ~ spl0_21 ),
inference(rat,[],[s441,s571,s126,s127]) ).
cnf(s636,plain,
( ~ spl0_50
| ~ spl0_17
| ~ spl0_13 ),
inference(rat,[],[s492,s532,s67,s112,s113,s629]) ).
cnf(s637,plain,
( spl0_5
| spl0_11 ),
inference(rat,[],[s488,s151,s152,s153,s160,s636,s11,s632,s41,s631,s598,s16,s597,s588,s18,s10,s584,s630,s590,s341,s574,s629]) ).
cnf(s638,plain,
( ~ spl0_30
| ~ spl0_23
| ~ spl0_18 ),
inference(rat,[],[s449,s239,s148,s149,s150]) ).
cnf(s639,plain,
( spl0_20
| ~ spl0_6
| ~ spl0_23 ),
inference(rat,[],[s512,s535,s132,s133]) ).
cnf(s640,plain,
( spl0_8
| spl0_11 ),
inference(rat,[],[s596,s161,s54,s588,s18,s639,s15,s613,s17,s638,s11,s607,s330,s3,s341,s608,s637,s574,s629]) ).
cnf(s641,plain,
spl0_11,
inference(rat,[],[s488,s151,s152,s153,s160,s11,s636,s632,s41,s598,s16,s589,s166,s597,s588,s631,s18,s10,s584,s640,s341,s574,s629]) ).
cnf(s642,plain,
spl0_31,
inference(rat,[],[s592,s641]) ).
cnf(s643,plain,
( spl0_5
| spl0_8 ),
inference(rat,[],[s239,s363,s45,s149,s150,s580,s21,s619,s641,s574,s642]) ).
cnf(s645,plain,
( ~ spl0_50
| ~ spl0_2 ),
inference(rat,[],[s222,s67,s112,s113]) ).
cnf(s646,plain,
( spl0_35
| ~ spl0_2
| ~ spl0_44 ),
inference(rat,[],[s241,s501,s68,s114,s115,s34,s476,s418,s89,s90,s91,s50,s23,s574,s629,s642]) ).
cnf(s647,plain,
( ~ spl0_2
| ~ spl0_44 ),
inference(rat,[],[s235,s45,s259,s580,s83,s126,s127,s38,s164,s620,s646,s645,s574,s642,s641]) ).
cnf(s648,plain,
spl0_8,
inference(rat,[],[s365,s242,s93,s94,s131,s163,s613,s17,s631,s19,s451,s241,s5,s68,s115,s512,s34,s373,s562,s23,s432,s95,s132,s133,s620,s109,s110,s142,s165,s164,s582,s607,s330,s3,s647,s608,s643,s574,s642]) ).
cnf(s649,plain,
spl0_20,
inference(rat,[],[s584,s648]) ).
cnf(s650,plain,
~ spl0_7,
inference(rat,[],[s585,s641,s649]) ).
cnf(s653,plain,
spl0_5,
inference(rat,[],[s619,s642,s650]) ).
cnf(s662,plain,
spl0_44,
inference(rat,[],[s608,s653]) ).
cnf(s666,plain,
~ spl0_2,
inference(rat,[],[s647,s662]) ).
cnf(s668,plain,
spl0_21,
inference(rat,[],[s10,s574,s649,s666]) ).
cnf(s669,plain,
~ spl0_30,
inference(rat,[],[s631,s668]) ).
cnf(s670,plain,
~ spl0_55,
inference(rat,[],[s516,s105,s106,s140,s629]) ).
cnf(s671,plain,
spl0_19,
inference(rat,[],[s61,s649,s574,s670]) ).
cnf(s672,plain,
spl0_17,
inference(rat,[],[s41,s574,s669,s670]) ).
cnf(s673,plain,
~ spl0_22,
inference(rat,[],[s632,s668,s672]) ).
cnf(s674,plain,
~ spl0_26,
inference(rat,[],[s164,s642,s673]) ).
cnf(s678,plain,
~ spl0_35,
inference(rat,[],[s620,s674]) ).
cnf(s682,plain,
spl0_57,
inference(rat,[],[s50,s574,s662,s678]) ).
cnf(s685,plain,
~ spl0_86,
inference(rat,[],[s91,s682]) ).
cnf(s686,plain,
spl0_85,
inference(rat,[],[s90,s682]) ).
cnf(s687,plain,
~ spl0_84,
inference(rat,[],[s89,s682]) ).
cnf(s696,plain,
$false,
inference(rat,[],[s297,s685,s671,s686,s687]) ).
fof(f2271,plain,
$false,
inference(avatar_sat_refutation,[],[s696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN483-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.16 % Computer : n002.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Mon Sep 28 16:17:52 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 Running first-order model finding
% 0.09/0.19 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.25 % (484108)Will run a generic schedule for satisfiability detection.
% 0.09/0.25 % (484115)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2207109617:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.09/0.25 % (484114)% WARNING: option uhcvi not known.
% 0.09/0.25 % (484113)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1837913842_2999 on theBenchmark for (2999ds/0Mi)
% 0.09/0.25 % (484114)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=577353351:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.09/0.25 % (484118)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=376292156:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.09/0.25 % (484116)dis+10_1_sil=32000:sp=arity:random_seed=587006195:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.09/0.25 % (484119)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=206771536:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.09/0.25 % (484117)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1002608389:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.09/0.25 % Detected minimum model sizes of [1]
% 0.09/0.25 % Detected maximum model sizes of [30]
% 0.09/0.25 % TRYING [1]
% 0.09/0.25 % TRYING [2]
% 0.09/0.25 % TRYING [3]
% 0.09/0.25 % TRYING [4]
% 0.09/0.25 % (484119) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-484108-484119"...
% 0.09/0.25 % (484119)...printing done.
% 0.09/0.25 % (484119)Refutation found. Thanks to Tanya!
% 0.09/0.25 % SZS status Unsatisfiable for theBenchmark
% 0.09/0.25 % SZS output start Proof for theBenchmark
% See solution above
% 0.56/0.26 % (484119)------------------------------
% 0.56/0.26 % (484119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.56/0.26 % (484119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.56/0.26 % (484119)CaDiCaL version: 2.1.3
% 0.56/0.26 % (484119)Termination reason: Refutation
% 0.56/0.26 % (484119)Time elapsed: 0.032 s
% 0.56/0.26 % (484119)Peak memory usage: 13 MB
% 0.56/0.26 % (484119)Instructions burned: 50 (million)
% 0.56/0.26 % (484108)Success in time 0.058 s
% 0.56/0.26 % Vampire exiting
%------------------------------------------------------------------------------