%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN451-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 : n009.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:08:50 PM UTC 2026
% Result : Unsatisfiable 0.43s 0.27s
% Output : Refutation 0.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 205
% Syntax : Number of formulae : 753 ( 40 unt; 113 def)
% Number of atoms : 2347 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 2760 (1166 ~;1481 |; 0 &)
% ( 113 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 139 ( 138 usr; 135 prp; 0-1 aty)
% Number of functors : 20 ( 20 usr; 20 con; 0-0 aty)
% Number of variables : 170 ( 0 sgn 170 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp0
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f6,negated_conjecture,
( ~ hskp24
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
fof(f7,negated_conjecture,
( ~ hskp23
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
fof(f17,negated_conjecture,
( ~ hskp13
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
fof(f32,negated_conjecture,
( hskp23
| hskp24
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f34,negated_conjecture,
( hskp0
| hskp5
| hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f45,negated_conjecture,
( ~ hskp25
| c0_1(a729) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp25
| c2_1(a729) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp25
| c3_1(a729) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp24
| c0_1(a802) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp23
| c0_1(a798) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp23
| c1_1(a798) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f52,negated_conjecture,
( ~ hskp21
| c0_1(a793) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp21
| c3_1(a793) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp20
| c2_1(a779) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp19
| c2_1(a777) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp18
| c1_1(a775) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f59,negated_conjecture,
( ~ hskp16
| c0_1(a764) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp16
| c2_1(a764) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f64,negated_conjecture,
( ~ hskp13
| c2_1(a759) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp13
| c3_1(a759) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f68,negated_conjecture,
( ~ hskp9
| c3_1(a746) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp8
| c3_1(a744) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp7
| c1_1(a741) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp7
| c3_1(a741) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f73,negated_conjecture,
( ~ hskp5
| c2_1(a735) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp5
| c3_1(a735) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp4
| c1_1(a734) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp3
| c2_1(a733) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp1
| c1_1(a731) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp1
| c3_1(a731) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp0
| c0_1(a730) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp0
| c3_1(a730) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ c2_1(a802)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ c3_1(a802)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ c3_1(a798)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f86,negated_conjecture,
( ~ c2_1(a793)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ c1_1(a779)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ c3_1(a779)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c0_1(a777)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c3_1(a777)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c2_1(a775)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c3_1(a775)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f94,negated_conjecture,
( ~ c3_1(a764)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f98,negated_conjecture,
( ~ c1_1(a759)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f100,negated_conjecture,
( ~ c0_1(a749)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c1_1(a749)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c3_1(a749)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f103,negated_conjecture,
( ~ c0_1(a748)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c1_1(a748)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c2_1(a748)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c0_1(a746)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c2_1(a746)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c0_1(a744)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c1_1(a744)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c0_1(a741)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f113,negated_conjecture,
( ~ c0_1(a735)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c0_1(a734)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c3_1(a734)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c0_1(a733)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c1_1(a733)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c0_1(a732)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c2_1(a732)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f121,negated_conjecture,
( ~ c2_1(a731)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c1_1(a730)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| hskp0
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c3_1(X0)
| hskp4
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f128,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp1
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f135,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp25
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp16
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f140,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp5
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp18
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f146,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f149,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause149) ).
fof(f150,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause150) ).
fof(f151,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f156,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f171,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c3_1(X2)
| c2_1(X0)
| c0_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X2)
| c2_1(X1)
| c3_1(X1)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f175,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_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',clause175) ).
fof(f176,plain,
( ~ hskp0
| hskp8 ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f179,plain,
( hskp24
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f193,plain,
( hskp23
| ~ hskp24
| hskp13 ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f195,plain,
( ~ hskp0
| hskp5
| ~ hskp19 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f202,plain,
( hskp25
| ~ c0_1(a729) ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f203,plain,
( hskp25
| c2_1(a729) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f204,plain,
( hskp25
| ~ c3_1(a729) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f205,plain,
( hskp24
| ~ c0_1(a802) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f206,plain,
( ~ hskp23
| ~ c0_1(a798) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f208,plain,
( hskp21
| ~ c0_1(a793) ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f209,plain,
( hskp21
| ~ c3_1(a793) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f210,plain,
( hskp20
| c2_1(a779) ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f211,plain,
( hskp19
| c2_1(a777) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f212,plain,
( hskp18
| c1_1(a775) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f213,plain,
( ~ hskp16
| ~ c0_1(a764) ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f217,plain,
( ~ hskp13
| ~ c3_1(a759) ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f220,plain,
( ~ hskp9
| ~ c3_1(a746) ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f221,plain,
( ~ hskp8
| ~ c3_1(a744) ),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f222,plain,
( ~ hskp7
| ~ c3_1(a741) ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f224,plain,
( ~ hskp5
| ~ c3_1(a735) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f225,plain,
( hskp3
| c2_1(a733) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f226,plain,
( ~ hskp1
| ~ c3_1(a731) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f227,plain,
( hskp0
| ~ c0_1(a730) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f228,plain,
( hskp0
| ~ c3_1(a730) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f229,plain,
( ~ c2_1(a802)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f230,plain,
( c3_1(a802)
| hskp24 ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f231,plain,
( c3_1(a798)
| ~ hskp23 ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f234,plain,
( ~ c2_1(a793)
| hskp21 ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f235,plain,
( ~ c1_1(a779)
| hskp20 ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f236,plain,
( c3_1(a779)
| hskp20 ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f237,plain,
( c0_1(a777)
| hskp19 ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f238,plain,
( c3_1(a777)
| hskp19 ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f239,plain,
( ~ c2_1(a775)
| hskp18 ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f240,plain,
( c3_1(a775)
| hskp18 ),
inference(consistent_polarity_flipping,[],[f92]) ).
fof(f242,plain,
( c3_1(a764)
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f247,plain,
( c0_1(a749)
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f248,plain,
( c3_1(a749)
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f249,plain,
( c0_1(a748)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f250,plain,
( ~ c1_1(a748)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f251,plain,
( ~ c2_1(a748)
| hskp10 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f252,plain,
( c0_1(a746)
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f253,plain,
( c0_1(a744)
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f108]) ).
fof(f254,plain,
( c0_1(a741)
| ~ hskp7 ),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f257,plain,
( c0_1(a735)
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f258,plain,
( c0_1(a734)
| ~ hskp4 ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f259,plain,
( c3_1(a734)
| ~ hskp4 ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f260,plain,
( c0_1(a733)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f261,plain,
( ~ c1_1(a733)
| hskp3 ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f262,plain,
( c0_1(a732)
| ~ hskp2 ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f264,plain,
( ~ c1_1(a730)
| hskp0 ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f265,plain,
! [X0] :
( ~ ndr1_0
| ~ c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ hskp0
| hskp1 ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f266,plain,
! [X0] :
( ~ ndr1_0
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| hskp4
| hskp5 ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f270,plain,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| c1_1(X0)
| hskp1
| hskp2 ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f277,plain,
! [X0] :
( c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| ~ c3_1(X0)
| ~ hskp25
| hskp9 ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f278,plain,
! [X0] :
( c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| ~ c3_1(X0)
| hskp16
| ~ hskp3 ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f282,plain,
! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp5
| ~ hskp20 ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f283,plain,
! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ hskp18
| hskp11 ),
inference(consistent_polarity_flipping,[],[f141]) ).
fof(f285,plain,
! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ hskp21 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f288,plain,
! [X0,X1] :
( c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0)
| c2_1(X0)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1)
| hskp2 ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f291,plain,
! [X0,X1] :
( c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| ~ c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| ~ hskp25 ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f292,plain,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c0_1(X1)
| c1_1(X1)
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f293,plain,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X1)
| c1_1(X1)
| hskp7 ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f294,plain,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X1)
| c2_1(X1)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f296,plain,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1)
| c1_1(X1)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f298,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X0)
| ~ c0_1(X1)
| c2_1(X1)
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f299,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| ~ c0_1(X1)
| c2_1(X1)
| hskp11 ),
inference(consistent_polarity_flipping,[],[f157]) ).
fof(f300,plain,
! [X0,X1] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| ~ c0_1(X1)
| ~ c3_1(X1)
| hskp13 ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f301,plain,
! [X0,X1] :
( c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| ~ c0_1(X1)
| hskp2 ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f302,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c3_1(X1)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp11 ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f303,plain,
! [X0,X1] :
( c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| hskp5 ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f304,plain,
! [X0,X1] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| ~ c3_1(X1)
| ~ hskp18 ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f309,plain,
! [X0,X1] :
( c0_1(X0)
| ~ c2_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| hskp1 ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f310,plain,
! [X2,X0,X1] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f313,plain,
! [X2,X0,X1] :
( c0_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f314,plain,
! [X2,X0,X1] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X1)
| c3_1(X2)
| c2_1(X0)
| ~ c0_1(X1)
| ~ c0_1(X2)
| c2_1(X2) ),
inference(consistent_polarity_flipping,[],[f172]) ).
fof(f315,plain,
! [X2,X0,X1] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| ~ c2_1(X2)
| c2_1(X1)
| ~ c3_1(X1)
| c1_1(X2)
| ~ c3_1(X2) ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f317,plain,
! [X2,X0,X1] :
( c0_1(X0)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c3_1(X1)
| ~ c2_1(X2)
| c3_1(X2)
| c2_1(X0)
| c1_1(X1)
| ~ c0_1(X2) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f319,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| ~ c0_1(X2)
| c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f320,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c0_1(X2)
| c3_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f319]) ).
fof(f322,definition,
( spl0_2
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f323,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| c3_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f325,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f329,definition,
( spl0_4
<=> ! [X0] :
( c0_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f330,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f331,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f317,f329,f325,f322,f319]) ).
fof(f333,definition,
( spl0_5
<=> ! [X2] :
( c3_1(X2)
| c2_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f334,plain,
( ! [X2] :
( c2_1(X2)
| c3_1(X2)
| ~ c0_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f340,definition,
( spl0_7
<=> ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f341,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2)
| c1_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f343,definition,
( spl0_8
<=> ! [X1] :
( c0_1(X1)
| ~ c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f344,plain,
( ! [X1] :
( c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f343]) ).
fof(f346,definition,
( spl0_9
<=> ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f347,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f348,plain,
( spl0_7
| spl0_8
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f315,f346,f325,f343,f340]) ).
fof(f350,definition,
( spl0_10
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f351,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,definition,
( spl0_11
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f354,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f353]) ).
fof(f355,plain,
( spl0_5
| spl0_10
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f314,f353,f325,f350,f333]) ).
fof(f357,definition,
( spl0_12
<=> ! [X2] :
( ~ c0_1(X2)
| ~ c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f358,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c0_1(X2)
| c1_1(X2) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f360,definition,
( spl0_13
<=> ! [X1] :
( c0_1(X1)
| c2_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f361,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f360]) ).
fof(f363,definition,
( spl0_14
<=> ! [X0] :
( c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f364,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f363]) ).
fof(f365,plain,
( spl0_12
| spl0_13
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f313,f363,f325,f360,f357]) ).
fof(f368,definition,
( spl0_15
<=> ! [X2] :
( c3_1(X2)
| c1_1(X2)
| ~ c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f369,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2)
| ~ c0_1(X2) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f375,definition,
( spl0_17
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f376,plain,
( ! [X2] :
( c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,definition,
( spl0_18
<=> ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f379,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f380,plain,
( spl0_17
| spl0_18
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f310,f346,f325,f378,f375]) ).
fof(f382,definition,
( spl0_19
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f386,definition,
( spl0_20
<=> ! [X1] :
( c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f387,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f386]) ).
fof(f389,definition,
( spl0_21
<=> ! [X0] :
( c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f390,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f389]) ).
fof(f391,plain,
( spl0_19
| spl0_20
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f309,f389,f325,f386,f382]) ).
fof(f393,definition,
( spl0_22
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f397,definition,
( spl0_23
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f398,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f405,definition,
( spl0_25
<=> ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f406,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1)
| c1_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f418,definition,
( spl0_28
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f419,plain,
( ! [X1] :
( c2_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f422,definition,
( spl0_29
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f425,plain,
( ~ spl0_29
| spl0_7
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f304,f353,f325,f340,f422]) ).
fof(f427,definition,
( spl0_30
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f431,definition,
( spl0_31
<=> ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f432,plain,
( ! [X0] :
( c3_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f433,plain,
( spl0_30
| spl0_7
| ~ spl0_3
| spl0_31 ),
inference(avatar_split_clause,[],[f303,f431,f325,f340,f427]) ).
fof(f435,definition,
( spl0_32
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f439,definition,
( spl0_33
<=> ! [X1] :
( c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f440,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f439]) ).
fof(f441,plain,
( spl0_32
| spl0_33
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f302,f353,f325,f439,f435]) ).
fof(f443,definition,
( spl0_34
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f446,plain,
( spl0_34
| spl0_10
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f301,f405,f325,f350,f443]) ).
fof(f448,definition,
( spl0_35
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f452,definition,
( spl0_36
<=> ! [X1] :
( ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f453,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f454,plain,
( spl0_35
| spl0_36
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f300,f360,f325,f452,f448]) ).
fof(f455,plain,
( spl0_32
| spl0_28
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f299,f353,f325,f418,f435]) ).
fof(f457,definition,
( spl0_37
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f460,plain,
( ~ spl0_37
| spl0_28
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f298,f319,f325,f418,f457]) ).
fof(f462,definition,
( spl0_38
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f469,plain,
( spl0_30
| spl0_15
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f296,f397,f325,f368,f427]) ).
fof(f478,plain,
( spl0_30
| spl0_28
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f294,f452,f325,f418,f427]) ).
fof(f480,definition,
( spl0_42
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f483,plain,
( spl0_42
| spl0_15
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f293,f378,f325,f368,f480]) ).
fof(f485,definition,
( spl0_43
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f489,definition,
( spl0_44
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f490,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( ~ spl0_43
| spl0_44
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f292,f418,f325,f489,f485]) ).
fof(f493,definition,
( spl0_45
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f496,plain,
( ~ spl0_45
| spl0_17
| ~ spl0_3
| spl0_31 ),
inference(avatar_split_clause,[],[f291,f431,f325,f375,f493]) ).
fof(f498,definition,
( spl0_46
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f506,definition,
( spl0_48
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f510,plain,
( spl0_34
| spl0_12
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f288,f333,f325,f357,f443]) ).
fof(f522,definition,
( spl0_51
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f525,plain,
( ~ spl0_51
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f285,f389,f325,f522]) ).
fof(f530,plain,
( spl0_32
| ~ spl0_29
| ~ spl0_3
| spl0_20 ),
inference(avatar_split_clause,[],[f283,f386,f325,f422,f435]) ).
fof(f532,definition,
( spl0_53
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f535,plain,
( ~ spl0_53
| spl0_30
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f282,f322,f325,f427,f532]) ).
fof(f537,definition,
( spl0_54
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f547,plain,
( ~ spl0_48
| spl0_22
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f278,f343,f325,f393,f506]) ).
fof(f549,definition,
( spl0_56
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f552,plain,
( spl0_56
| ~ spl0_45
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f277,f343,f325,f493,f549]) ).
fof(f567,plain,
( spl0_34
| spl0_19
| ~ spl0_3
| spl0_44 ),
inference(avatar_split_clause,[],[f270,f489,f325,f382,f443]) ).
fof(f574,plain,
( spl0_30
| spl0_38
| spl0_12
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f266,f325,f357,f462,f427]) ).
fof(f575,plain,
( spl0_19
| ~ spl0_43
| spl0_17
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f265,f325,f375,f485,f382]) ).
fof(f577,definition,
( spl0_60
<=> c1_1(a730) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f580,plain,
( spl0_43
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f264,f577,f485]) ).
fof(f582,definition,
( spl0_61
<=> c2_1(a731) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f584,plain,
( ~ c2_1(a731)
| spl0_61 ),
inference(avatar_component_clause,[],[f582]) ).
fof(f585,plain,
( ~ spl0_19
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f121,f582,f382]) ).
fof(f592,definition,
( spl0_63
<=> c2_1(a732) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f594,plain,
( ~ c2_1(a732)
| spl0_63 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f595,plain,
( ~ spl0_34
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f119,f592,f443]) ).
fof(f597,definition,
( spl0_64
<=> c0_1(a732) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f600,plain,
( ~ spl0_34
| spl0_64 ),
inference(avatar_split_clause,[],[f262,f597,f443]) ).
fof(f602,definition,
( spl0_65
<=> c1_1(a733) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f605,plain,
( spl0_48
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f261,f602,f506]) ).
fof(f607,definition,
( spl0_66
<=> c0_1(a733) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f610,plain,
( spl0_48
| spl0_66 ),
inference(avatar_split_clause,[],[f260,f607,f506]) ).
fof(f612,definition,
( spl0_67
<=> c3_1(a734) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f614,plain,
( c3_1(a734)
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f612]) ).
fof(f615,plain,
( ~ spl0_38
| spl0_67 ),
inference(avatar_split_clause,[],[f259,f612,f462]) ).
fof(f617,definition,
( spl0_68
<=> c0_1(a734) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f620,plain,
( ~ spl0_38
| spl0_68 ),
inference(avatar_split_clause,[],[f258,f617,f462]) ).
fof(f622,definition,
( spl0_69
<=> c0_1(a735) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f625,plain,
( ~ spl0_30
| spl0_69 ),
inference(avatar_split_clause,[],[f257,f622,f427]) ).
fof(f637,definition,
( spl0_72
<=> c0_1(a741) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f640,plain,
( ~ spl0_42
| spl0_72 ),
inference(avatar_split_clause,[],[f254,f637,f480]) ).
fof(f642,definition,
( spl0_73
<=> c1_1(a744) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f644,plain,
( ~ c1_1(a744)
| spl0_73 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f645,plain,
( ~ spl0_46
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f109,f642,f498]) ).
fof(f647,definition,
( spl0_74
<=> c0_1(a744) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f650,plain,
( ~ spl0_46
| spl0_74 ),
inference(avatar_split_clause,[],[f253,f647,f498]) ).
fof(f652,definition,
( spl0_75
<=> c2_1(a746) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f654,plain,
( ~ c2_1(a746)
| spl0_75 ),
inference(avatar_component_clause,[],[f652]) ).
fof(f655,plain,
( ~ spl0_56
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f107,f652,f549]) ).
fof(f657,definition,
( spl0_76
<=> c0_1(a746) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f660,plain,
( ~ spl0_56
| spl0_76 ),
inference(avatar_split_clause,[],[f252,f657,f549]) ).
fof(f662,definition,
( spl0_77
<=> c2_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f664,plain,
( ~ c2_1(a748)
| spl0_77 ),
inference(avatar_component_clause,[],[f662]) ).
fof(f665,plain,
( spl0_37
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f251,f662,f457]) ).
fof(f667,definition,
( spl0_78
<=> c1_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f670,plain,
( spl0_37
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f250,f667,f457]) ).
fof(f672,definition,
( spl0_79
<=> c0_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f675,plain,
( spl0_37
| spl0_79 ),
inference(avatar_split_clause,[],[f249,f672,f457]) ).
fof(f677,definition,
( spl0_80
<=> c3_1(a749) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f679,plain,
( c3_1(a749)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f677]) ).
fof(f680,plain,
( ~ spl0_32
| spl0_80 ),
inference(avatar_split_clause,[],[f248,f677,f435]) ).
fof(f682,definition,
( spl0_81
<=> c1_1(a749) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f685,plain,
( ~ spl0_32
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f101,f682,f435]) ).
fof(f687,definition,
( spl0_82
<=> c0_1(a749) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f690,plain,
( ~ spl0_32
| spl0_82 ),
inference(avatar_split_clause,[],[f247,f687,f435]) ).
fof(f697,definition,
( spl0_84
<=> c1_1(a759) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f700,plain,
( ~ spl0_35
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f98,f697,f448]) ).
fof(f717,definition,
( spl0_88
<=> c3_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f719,plain,
( c3_1(a764)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f720,plain,
( ~ spl0_22
| spl0_88 ),
inference(avatar_split_clause,[],[f242,f717,f393]) ).
fof(f727,definition,
( spl0_90
<=> c3_1(a775) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f729,plain,
( c3_1(a775)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f730,plain,
( spl0_29
| spl0_90 ),
inference(avatar_split_clause,[],[f240,f727,f422]) ).
fof(f732,definition,
( spl0_91
<=> c2_1(a775) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f734,plain,
( ~ c2_1(a775)
| spl0_91 ),
inference(avatar_component_clause,[],[f732]) ).
fof(f735,plain,
( spl0_29
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f239,f732,f422]) ).
fof(f737,definition,
( spl0_92
<=> c3_1(a777) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f739,plain,
( c3_1(a777)
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f740,plain,
( spl0_54
| spl0_92 ),
inference(avatar_split_clause,[],[f238,f737,f537]) ).
fof(f742,definition,
( spl0_93
<=> c0_1(a777) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f745,plain,
( spl0_54
| spl0_93 ),
inference(avatar_split_clause,[],[f237,f742,f537]) ).
fof(f747,definition,
( spl0_94
<=> c3_1(a779) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f750,plain,
( spl0_53
| spl0_94 ),
inference(avatar_split_clause,[],[f236,f747,f532]) ).
fof(f752,definition,
( spl0_95
<=> c1_1(a779) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f755,plain,
( spl0_53
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f235,f752,f532]) ).
fof(f757,definition,
( spl0_96
<=> c2_1(a793) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f759,plain,
( ~ c2_1(a793)
| spl0_96 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f760,plain,
( spl0_51
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f234,f757,f522]) ).
fof(f772,definition,
( spl0_99
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f776,definition,
( spl0_100
<=> c3_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f778,plain,
( c3_1(a798)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,plain,
( ~ spl0_99
| spl0_100 ),
inference(avatar_split_clause,[],[f231,f776,f772]) ).
fof(f781,definition,
( spl0_101
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f785,definition,
( spl0_102
<=> c3_1(a802) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f788,plain,
( spl0_101
| spl0_102 ),
inference(avatar_split_clause,[],[f230,f785,f781]) ).
fof(f790,definition,
( spl0_103
<=> c2_1(a802) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f792,plain,
( ~ c2_1(a802)
| spl0_103 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f793,plain,
( spl0_101
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f229,f790,f781]) ).
fof(f795,definition,
( spl0_104
<=> c3_1(a730) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f797,plain,
( ~ c3_1(a730)
| spl0_104 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f798,plain,
( ~ spl0_104
| spl0_43 ),
inference(avatar_split_clause,[],[f228,f485,f795]) ).
fof(f800,definition,
( spl0_105
<=> c0_1(a730) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f803,plain,
( ~ spl0_105
| spl0_43 ),
inference(avatar_split_clause,[],[f227,f485,f800]) ).
fof(f805,definition,
( spl0_106
<=> c3_1(a731) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f807,plain,
( ~ c3_1(a731)
| spl0_106 ),
inference(avatar_component_clause,[],[f805]) ).
fof(f808,plain,
( ~ spl0_106
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f226,f382,f805]) ).
fof(f810,definition,
( spl0_107
<=> c1_1(a731) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f813,plain,
( spl0_107
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f77,f382,f810]) ).
fof(f815,definition,
( spl0_108
<=> c2_1(a733) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f817,plain,
( c2_1(a733)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f818,plain,
( spl0_108
| spl0_48 ),
inference(avatar_split_clause,[],[f225,f506,f815]) ).
fof(f820,definition,
( spl0_109
<=> c1_1(a734) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f823,plain,
( spl0_109
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f75,f462,f820]) ).
fof(f825,definition,
( spl0_110
<=> c3_1(a735) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f827,plain,
( ~ c3_1(a735)
| spl0_110 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f828,plain,
( ~ spl0_110
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f224,f427,f825]) ).
fof(f830,definition,
( spl0_111
<=> c2_1(a735) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f832,plain,
( c2_1(a735)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f830]) ).
fof(f833,plain,
( spl0_111
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f73,f427,f830]) ).
fof(f840,definition,
( spl0_113
<=> c3_1(a741) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f842,plain,
( ~ c3_1(a741)
| spl0_113 ),
inference(avatar_component_clause,[],[f840]) ).
fof(f843,plain,
( ~ spl0_113
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f222,f480,f840]) ).
fof(f845,definition,
( spl0_114
<=> c1_1(a741) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f848,plain,
( spl0_114
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f70,f480,f845]) ).
fof(f850,definition,
( spl0_115
<=> c3_1(a744) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f852,plain,
( ~ c3_1(a744)
| spl0_115 ),
inference(avatar_component_clause,[],[f850]) ).
fof(f853,plain,
( ~ spl0_115
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f221,f498,f850]) ).
fof(f855,definition,
( spl0_116
<=> c3_1(a746) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f858,plain,
( ~ spl0_116
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f220,f549,f855]) ).
fof(f870,definition,
( spl0_119
<=> c3_1(a759) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f873,plain,
( ~ spl0_119
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f217,f448,f870]) ).
fof(f875,definition,
( spl0_120
<=> c2_1(a759) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f877,plain,
( c2_1(a759)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f878,plain,
( spl0_120
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f64,f448,f875]) ).
fof(f895,definition,
( spl0_124
<=> c2_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f897,plain,
( c2_1(a764)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f898,plain,
( spl0_124
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f60,f393,f895]) ).
fof(f900,definition,
( spl0_125
<=> c0_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f903,plain,
( ~ spl0_125
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f213,f393,f900]) ).
fof(f915,definition,
( spl0_128
<=> c1_1(a775) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f918,plain,
( spl0_128
| spl0_29 ),
inference(avatar_split_clause,[],[f212,f422,f915]) ).
fof(f920,definition,
( spl0_129
<=> c2_1(a777) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f922,plain,
( c2_1(a777)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f923,plain,
( spl0_129
| spl0_54 ),
inference(avatar_split_clause,[],[f211,f537,f920]) ).
fof(f925,definition,
( spl0_130
<=> c2_1(a779) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f927,plain,
( c2_1(a779)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f928,plain,
( spl0_130
| spl0_53 ),
inference(avatar_split_clause,[],[f210,f532,f925]) ).
fof(f930,definition,
( spl0_131
<=> c3_1(a793) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f933,plain,
( ~ spl0_131
| spl0_51 ),
inference(avatar_split_clause,[],[f209,f522,f930]) ).
fof(f935,definition,
( spl0_132
<=> c0_1(a793) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f938,plain,
( ~ spl0_132
| spl0_51 ),
inference(avatar_split_clause,[],[f208,f522,f935]) ).
fof(f945,definition,
( spl0_134
<=> c1_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f948,plain,
( spl0_134
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f50,f772,f945]) ).
fof(f950,definition,
( spl0_135
<=> c0_1(a798) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f953,plain,
( ~ spl0_135
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f206,f772,f950]) ).
fof(f955,definition,
( spl0_136
<=> c0_1(a802) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f958,plain,
( ~ spl0_136
| spl0_101 ),
inference(avatar_split_clause,[],[f205,f781,f955]) ).
fof(f960,definition,
( spl0_137
<=> c3_1(a729) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f962,plain,
( ~ c3_1(a729)
| spl0_137 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f963,plain,
( ~ spl0_137
| spl0_45 ),
inference(avatar_split_clause,[],[f204,f493,f960]) ).
fof(f965,definition,
( spl0_138
<=> c2_1(a729) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f967,plain,
( c2_1(a729)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f968,plain,
( spl0_138
| spl0_45 ),
inference(avatar_split_clause,[],[f203,f493,f965]) ).
fof(f970,definition,
( spl0_139
<=> c0_1(a729) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f973,plain,
( ~ spl0_139
| spl0_45 ),
inference(avatar_split_clause,[],[f202,f493,f970]) ).
fof(f1020,plain,
( ~ spl0_54
| spl0_30
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f195,f485,f427,f537]) ).
fof(f1022,plain,
( spl0_35
| ~ spl0_101
| spl0_99 ),
inference(avatar_split_clause,[],[f193,f772,f781,f448]) ).
fof(f1037,plain,
( spl0_3
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f17,f448,f325]) ).
fof(f1047,plain,
( spl0_3
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f7,f772,f325]) ).
fof(f1048,plain,
( spl0_3
| spl0_101 ),
inference(avatar_split_clause,[],[f179,f781,f325]) ).
fof(f1053,plain,
( spl0_46
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f176,f485,f498]) ).
fof(f1055,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_2
| ~ spl0_5 ),
inference(resolution,[],[f334,f323]) ).
fof(f1074,plain,
( c3_1(a731)
| ~ c0_1(a731)
| ~ spl0_5
| spl0_61 ),
inference(resolution,[],[f334,f584]) ).
fof(f1077,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_2
| ~ spl0_5 ),
inference(duplicate_literal_removal,[],[f1055]) ).
fof(f1079,definition,
( spl0_149
<=> c0_1(a731) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1082,plain,
( ~ spl0_149
| spl0_106
| ~ spl0_5
| spl0_61 ),
inference(avatar_split_clause,[],[f1074,f582,f333,f805,f1079]) ).
fof(f1094,definition,
( spl0_152
<=> c0_1(a775) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1117,plain,
( ~ c3_1(a802)
| c0_1(a802)
| ~ spl0_8
| spl0_103 ),
inference(resolution,[],[f344,f792]) ).
fof(f1141,definition,
( spl0_157
<=> c3_1(a733) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1142,plain,
( c3_1(a733)
| ~ spl0_157 ),
inference(avatar_component_clause,[],[f1141]) ).
fof(f1172,plain,
( spl0_136
| ~ spl0_102
| ~ spl0_8
| spl0_103 ),
inference(avatar_split_clause,[],[f1117,f790,f343,f785,f955]) ).
fof(f1173,plain,
( c1_1(a759)
| c3_1(a759)
| ~ spl0_2
| ~ spl0_120 ),
inference(resolution,[],[f877,f323]) ).
fof(f1184,plain,
( ~ c3_1(a775)
| c0_1(a775)
| ~ spl0_8
| spl0_91 ),
inference(resolution,[],[f344,f734]) ).
fof(f1202,definition,
( spl0_163
<=> c1_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1221,plain,
( ~ c0_1(a741)
| ~ c1_1(a741)
| ~ spl0_10
| spl0_113 ),
inference(resolution,[],[f351,f842]) ).
fof(f1223,plain,
( ~ c0_1(a735)
| ~ c1_1(a735)
| ~ spl0_10
| spl0_110 ),
inference(resolution,[],[f351,f827]) ).
fof(f1226,plain,
( ~ c0_1(a731)
| ~ c1_1(a731)
| ~ spl0_10
| spl0_106 ),
inference(resolution,[],[f351,f807]) ).
fof(f1231,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_9
| ~ spl0_11 ),
inference(resolution,[],[f354,f347]) ).
fof(f1250,plain,
( ~ c1_1(a731)
| c3_1(a731)
| ~ spl0_11
| spl0_61 ),
inference(resolution,[],[f354,f584]) ).
fof(f1254,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0) )
| ~ spl0_9
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f1231]) ).
fof(f1256,definition,
( spl0_164
<=> c1_1(a732) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1262,definition,
( spl0_165
<=> c1_1(a735) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1267,definition,
( spl0_166
<=> c1_1(a777) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1268,plain,
( c1_1(a777)
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f1267]) ).
fof(f1282,definition,
( spl0_169
<=> c1_1(a729) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1283,plain,
( c1_1(a729)
| ~ spl0_169 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1287,plain,
( spl0_152
| ~ spl0_90
| ~ spl0_8
| spl0_91 ),
inference(avatar_split_clause,[],[f1184,f732,f343,f727,f1094]) ).
fof(f1289,plain,
( spl0_106
| ~ spl0_107
| ~ spl0_11
| spl0_61 ),
inference(avatar_split_clause,[],[f1250,f582,f353,f810,f805]) ).
fof(f1307,plain,
( ~ c1_1(a746)
| c3_1(a746)
| ~ spl0_11
| spl0_75 ),
inference(resolution,[],[f354,f654]) ).
fof(f1324,definition,
( spl0_170
<=> c1_1(a746) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1328,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_9
| ~ spl0_13 ),
inference(resolution,[],[f361,f347]) ).
fof(f1350,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_9
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f1328]) ).
fof(f1359,plain,
( c0_1(a729)
| ~ c1_1(a729)
| ~ spl0_14
| spl0_137 ),
inference(resolution,[],[f364,f962]) ).
fof(f1416,plain,
( c1_1(a744)
| ~ c0_1(a744)
| ~ spl0_15
| spl0_115 ),
inference(resolution,[],[f369,f852]) ).
fof(f1446,plain,
( ~ spl0_165
| ~ spl0_69
| ~ spl0_10
| spl0_110 ),
inference(avatar_split_clause,[],[f1223,f825,f350,f622,f1262]) ).
fof(f1453,plain,
( c0_1(a798)
| ~ c1_1(a798)
| ~ spl0_20
| ~ spl0_100 ),
inference(resolution,[],[f387,f778]) ).
fof(f1477,plain,
( ~ spl0_134
| spl0_135
| ~ spl0_20
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f1453,f776,f386,f950,f945]) ).
fof(f1483,plain,
( ~ c3_1(a777)
| ~ c0_1(a777)
| ~ spl0_18
| ~ spl0_129 ),
inference(resolution,[],[f922,f379]) ).
fof(f1495,plain,
( c0_1(a793)
| c3_1(a793)
| ~ spl0_4
| spl0_96 ),
inference(resolution,[],[f330,f759]) ).
fof(f1505,plain,
( c0_1(a731)
| c3_1(a731)
| ~ spl0_4
| spl0_61 ),
inference(resolution,[],[f330,f584]) ).
fof(f1510,plain,
( spl0_106
| spl0_149
| ~ spl0_4
| spl0_61 ),
inference(avatar_split_clause,[],[f1505,f582,f329,f1079,f805]) ).
fof(f1522,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(resolution,[],[f320,f354]) ).
fof(f1531,plain,
( ~ c0_1(a735)
| c3_1(a735)
| ~ spl0_1
| ~ spl0_111 ),
inference(resolution,[],[f320,f832]) ).
fof(f1533,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f1522]) ).
fof(f1562,plain,
( c0_1(a764)
| ~ c1_1(a764)
| ~ spl0_20
| ~ spl0_88 ),
inference(resolution,[],[f387,f719]) ).
fof(f1581,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_23
| ~ spl0_28 ),
inference(resolution,[],[f419,f398]) ).
fof(f1588,plain,
( ~ c1_1(a775)
| ~ c0_1(a775)
| ~ spl0_28
| spl0_91 ),
inference(resolution,[],[f419,f734]) ).
fof(f1598,plain,
( ~ c1_1(a732)
| ~ c0_1(a732)
| ~ spl0_28
| spl0_63 ),
inference(resolution,[],[f419,f594]) ).
fof(f1601,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_23
| ~ spl0_28 ),
inference(duplicate_literal_removal,[],[f1581]) ).
fof(f1629,plain,
( c1_1(a730)
| c0_1(a730)
| ~ spl0_31
| spl0_104 ),
inference(resolution,[],[f432,f797]) ).
fof(f1635,plain,
( spl0_105
| spl0_60
| ~ spl0_31
| spl0_104 ),
inference(avatar_split_clause,[],[f1629,f795,f431,f577,f800]) ).
fof(f1658,plain,
( ~ c3_1(a779)
| c1_1(a779)
| ~ spl0_7
| ~ spl0_130 ),
inference(resolution,[],[f341,f927]) ).
fof(f1670,plain,
( spl0_110
| ~ spl0_69
| ~ spl0_1
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1531,f830,f319,f622,f825]) ).
fof(f1712,plain,
( ~ spl0_74
| spl0_73
| ~ spl0_15
| spl0_115 ),
inference(avatar_split_clause,[],[f1416,f850,f368,f642,f647]) ).
fof(f1724,plain,
( ~ spl0_93
| ~ spl0_92
| ~ spl0_18
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1483,f920,f378,f737,f742]) ).
fof(f1771,plain,
( c0_1(a731)
| ~ c1_1(a731)
| ~ spl0_14
| spl0_106 ),
inference(resolution,[],[f364,f807]) ).
fof(f1802,plain,
( c0_1(a775)
| ~ c1_1(a775)
| ~ spl0_13
| spl0_91 ),
inference(resolution,[],[f361,f734]) ).
fof(f1813,plain,
( ~ c0_1(a746)
| c1_1(a746)
| ~ spl0_17
| spl0_75 ),
inference(resolution,[],[f376,f654]) ).
fof(f1814,plain,
( ~ c0_1(a748)
| c1_1(a748)
| ~ spl0_17
| spl0_77 ),
inference(resolution,[],[f376,f664]) ).
fof(f1815,plain,
( spl0_78
| ~ spl0_79
| ~ spl0_17
| spl0_77 ),
inference(avatar_split_clause,[],[f1814,f662,f375,f672,f667]) ).
fof(f1880,plain,
( ~ c3_1(a733)
| ~ c0_1(a733)
| ~ spl0_18
| ~ spl0_108 ),
inference(resolution,[],[f379,f817]) ).
fof(f1911,plain,
( ~ c0_1(a733)
| c1_1(a733)
| ~ spl0_12
| ~ spl0_157 ),
inference(resolution,[],[f358,f1142]) ).
fof(f1913,plain,
( ~ c0_1(a749)
| c1_1(a749)
| ~ spl0_12
| ~ spl0_80 ),
inference(resolution,[],[f358,f679]) ).
fof(f1916,plain,
( spl0_15
| ~ spl0_2
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f1077,f333,f322,f368]) ).
fof(f1917,plain,
( spl0_119
| spl0_84
| ~ spl0_2
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1173,f875,f322,f697,f870]) ).
fof(f1918,plain,
( spl0_95
| ~ spl0_94
| ~ spl0_7
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1658,f925,f340,f747,f752]) ).
fof(f1946,plain,
( ~ spl0_107
| ~ spl0_149
| ~ spl0_10
| spl0_106 ),
inference(avatar_split_clause,[],[f1226,f805,f350,f1079,f810]) ).
fof(f1978,plain,
( c1_1(a729)
| c3_1(a729)
| ~ spl0_2
| ~ spl0_138 ),
inference(resolution,[],[f323,f967]) ).
fof(f1993,plain,
( c1_1(a735)
| c3_1(a735)
| ~ spl0_2
| ~ spl0_111 ),
inference(resolution,[],[f323,f832]) ).
fof(f1994,plain,
( c1_1(a733)
| c3_1(a733)
| ~ spl0_2
| ~ spl0_108 ),
inference(resolution,[],[f323,f817]) ).
fof(f2026,plain,
( ~ spl0_66
| ~ spl0_157
| ~ spl0_18
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1880,f815,f378,f1141,f607]) ).
fof(f2038,plain,
( ~ spl0_128
| spl0_152
| ~ spl0_13
| spl0_91 ),
inference(avatar_split_clause,[],[f1802,f732,f360,f1094,f915]) ).
fof(f2048,plain,
( spl0_137
| spl0_169
| ~ spl0_2
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1978,f965,f322,f1282,f960]) ).
fof(f2060,plain,
( spl0_157
| spl0_65
| ~ spl0_2
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1994,f815,f322,f602,f1141]) ).
fof(f2064,plain,
( spl0_116
| ~ spl0_170
| ~ spl0_11
| spl0_75 ),
inference(avatar_split_clause,[],[f1307,f652,f353,f1324,f855]) ).
fof(f2078,plain,
( c0_1(a731)
| ~ c1_1(a731)
| ~ spl0_13
| spl0_61 ),
inference(resolution,[],[f584,f361]) ).
fof(f2109,plain,
( c0_1(a729)
| ~ spl0_9
| ~ spl0_13
| ~ spl0_169 ),
inference(resolution,[],[f1350,f1283]) ).
fof(f2126,plain,
( spl0_139
| ~ spl0_9
| ~ spl0_13
| ~ spl0_169 ),
inference(avatar_split_clause,[],[f2109,f1282,f360,f346,f970]) ).
fof(f2129,plain,
( spl0_170
| ~ spl0_76
| ~ spl0_17
| spl0_75 ),
inference(avatar_split_clause,[],[f1813,f652,f375,f657,f1324]) ).
fof(f2134,plain,
( ~ spl0_107
| spl0_149
| ~ spl0_13
| spl0_61 ),
inference(avatar_split_clause,[],[f2078,f582,f360,f1079,f810]) ).
fof(f2137,plain,
( spl0_81
| ~ spl0_82
| ~ spl0_12
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f1913,f677,f357,f687,f682]) ).
fof(f2139,plain,
( spl0_65
| ~ spl0_66
| ~ spl0_12
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f1911,f1141,f357,f607,f602]) ).
fof(f2140,plain,
( ~ spl0_152
| ~ spl0_128
| ~ spl0_28
| spl0_91 ),
inference(avatar_split_clause,[],[f1588,f732,f418,f915,f1094]) ).
fof(f2167,plain,
( ~ c0_1(a777)
| ~ spl0_23
| ~ spl0_28
| ~ spl0_166 ),
inference(resolution,[],[f1601,f1268]) ).
fof(f2184,plain,
( ~ spl0_93
| ~ spl0_23
| ~ spl0_28
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f2167,f1267,f418,f397,f742]) ).
fof(f2207,plain,
( ~ c3_1(a764)
| c1_1(a764)
| ~ spl0_7
| ~ spl0_124 ),
inference(resolution,[],[f341,f897]) ).
fof(f2221,plain,
( ~ c0_1(a777)
| c1_1(a777)
| ~ spl0_12
| ~ spl0_92 ),
inference(resolution,[],[f358,f739]) ).
fof(f2238,plain,
( spl0_166
| ~ spl0_93
| ~ spl0_12
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f2221,f737,f357,f742,f1267]) ).
fof(f2270,plain,
( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_2
| ~ spl0_25 ),
inference(resolution,[],[f406,f323]) ).
fof(f2286,plain,
( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_2
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f2270]) ).
fof(f2295,plain,
( spl0_31
| ~ spl0_2
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f2286,f405,f322,f431]) ).
fof(f2300,plain,
( ! [X0] :
( c3_1(X0)
| c1_1(X0)
| c1_1(X0)
| c3_1(X0) )
| ~ spl0_2
| ~ spl0_33 ),
inference(resolution,[],[f440,f323]) ).
fof(f2315,plain,
( ! [X0] :
( c3_1(X0)
| c1_1(X0) )
| ~ spl0_2
| ~ spl0_33 ),
inference(duplicate_literal_removal,[],[f2300]) ).
fof(f2333,plain,
( c1_1(a730)
| ~ spl0_2
| ~ spl0_33
| spl0_104 ),
inference(resolution,[],[f2315,f797]) ).
fof(f2334,plain,
( spl0_60
| ~ spl0_2
| ~ spl0_33
| spl0_104 ),
inference(avatar_split_clause,[],[f2333,f795,f439,f322,f577]) ).
fof(f2341,plain,
( spl0_14
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1254,f353,f346,f363]) ).
fof(f2352,plain,
( ~ spl0_163
| spl0_125
| ~ spl0_20
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f1562,f717,f386,f900,f1202]) ).
fof(f2371,plain,
( spl0_163
| ~ spl0_88
| ~ spl0_7
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f2207,f895,f340,f717,f1202]) ).
fof(f2373,plain,
( ~ spl0_169
| spl0_139
| ~ spl0_14
| spl0_137 ),
inference(avatar_split_clause,[],[f1359,f960,f363,f970,f1282]) ).
fof(f2378,plain,
( ~ spl0_107
| spl0_149
| ~ spl0_14
| spl0_106 ),
inference(avatar_split_clause,[],[f1771,f805,f363,f1079,f810]) ).
fof(f2471,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_4
| ~ spl0_21 ),
inference(resolution,[],[f390,f330]) ).
fof(f2474,plain,
( c3_1(a729)
| c0_1(a729)
| ~ spl0_21
| ~ spl0_138 ),
inference(resolution,[],[f390,f967]) ).
fof(f2489,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0) )
| ~ spl0_4
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f2471]) ).
fof(f2496,plain,
( spl0_139
| spl0_137
| ~ spl0_21
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f2474,f965,f389,f960,f970]) ).
fof(f2498,plain,
( spl0_10
| ~ spl0_1
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1533,f353,f319,f350]) ).
fof(f2514,plain,
( ~ spl0_114
| ~ spl0_72
| ~ spl0_10
| spl0_113 ),
inference(avatar_split_clause,[],[f1221,f840,f350,f637,f845]) ).
fof(f2606,plain,
( ~ c1_1(a775)
| ~ c0_1(a775)
| ~ spl0_36
| ~ spl0_90 ),
inference(resolution,[],[f453,f729]) ).
fof(f2614,plain,
( ~ c1_1(a734)
| ~ c0_1(a734)
| ~ spl0_36
| ~ spl0_67 ),
inference(resolution,[],[f453,f614]) ).
fof(f2622,plain,
( ~ spl0_68
| ~ spl0_109
| ~ spl0_36
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f2614,f612,f452,f820,f617]) ).
fof(f2627,plain,
( ~ spl0_152
| ~ spl0_128
| ~ spl0_36
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f2606,f727,f452,f915,f1094]) ).
fof(f2635,plain,
( ~ spl0_64
| ~ spl0_164
| ~ spl0_28
| spl0_63 ),
inference(avatar_split_clause,[],[f1598,f592,f418,f1256,f597]) ).
fof(f2637,plain,
( spl0_110
| spl0_165
| ~ spl0_2
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f1993,f830,f322,f1262,f825]) ).
fof(f2694,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_7
| ~ spl0_17 ),
inference(resolution,[],[f376,f341]) ).
fof(f2701,plain,
( ~ c0_1(a732)
| c1_1(a732)
| ~ spl0_17
| spl0_63 ),
inference(resolution,[],[f376,f594]) ).
fof(f2702,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f2694]) ).
fof(f2704,plain,
( spl0_164
| ~ spl0_64
| ~ spl0_17
| spl0_63 ),
inference(avatar_split_clause,[],[f2701,f592,f375,f597,f1256]) ).
fof(f2706,plain,
( spl0_12
| ~ spl0_7
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f2702,f375,f340,f357]) ).
fof(f2707,plain,
( spl0_131
| spl0_132
| ~ spl0_4
| spl0_96 ),
inference(avatar_split_clause,[],[f1495,f757,f329,f935,f930]) ).
fof(f2749,plain,
( c0_1(a730)
| ~ spl0_4
| ~ spl0_21
| spl0_104 ),
inference(resolution,[],[f2489,f797]) ).
fof(f2752,plain,
( spl0_105
| ~ spl0_4
| ~ spl0_21
| spl0_104 ),
inference(avatar_split_clause,[],[f2749,f795,f389,f329,f800]) ).
fof(f2776,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_17
| ~ spl0_44 ),
inference(resolution,[],[f490,f376]) ).
fof(f2804,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_17
| ~ spl0_44 ),
inference(duplicate_literal_removal,[],[f2776]) ).
fof(f2810,plain,
( ~ c0_1(a744)
| ~ spl0_17
| ~ spl0_44
| spl0_73 ),
inference(resolution,[],[f2804,f644]) ).
fof(f2816,plain,
( ~ spl0_74
| ~ spl0_17
| ~ spl0_44
| spl0_73 ),
inference(avatar_split_clause,[],[f2810,f642,f489,f375,f647]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f331]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f348]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_5
| spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f355]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_12
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f365]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_9
| spl0_17
| spl0_18 ),
inference(sat_conversion,[],[f380]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_19
| spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f391]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_7
| spl0_11
| ~ spl0_29 ),
inference(sat_conversion,[],[f425]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_7
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f433]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_11
| spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f441]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_10
| spl0_25
| spl0_34 ),
inference(sat_conversion,[],[f446]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_13
| spl0_35
| spl0_36 ),
inference(sat_conversion,[],[f454]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_11
| spl0_28
| spl0_32 ),
inference(sat_conversion,[],[f455]) ).
cnf(s20,plain,
( spl0_1
| ~ spl0_3
| spl0_28
| ~ spl0_37 ),
inference(sat_conversion,[],[f460]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_15
| spl0_23
| spl0_30 ),
inference(sat_conversion,[],[f469]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_28
| spl0_30
| spl0_36 ),
inference(sat_conversion,[],[f478]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_15
| spl0_18
| spl0_42 ),
inference(sat_conversion,[],[f483]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_28
| ~ spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f491]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_17
| spl0_31
| ~ spl0_45 ),
inference(sat_conversion,[],[f496]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_5
| spl0_12
| spl0_34 ),
inference(sat_conversion,[],[f510]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_21
| ~ spl0_51 ),
inference(sat_conversion,[],[f525]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_20
| ~ spl0_29
| spl0_32 ),
inference(sat_conversion,[],[f530]) ).
cnf(s36,plain,
( spl0_2
| ~ spl0_3
| spl0_30
| ~ spl0_53 ),
inference(sat_conversion,[],[f535]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_8
| spl0_22
| ~ spl0_48 ),
inference(sat_conversion,[],[f547]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_8
| ~ spl0_45
| spl0_56 ),
inference(sat_conversion,[],[f552]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_19
| spl0_34
| spl0_44 ),
inference(sat_conversion,[],[f567]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_12
| spl0_30
| spl0_38 ),
inference(sat_conversion,[],[f574]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_17
| spl0_19
| ~ spl0_43 ),
inference(sat_conversion,[],[f575]) ).
cnf(s54,plain,
( spl0_43
| ~ spl0_60 ),
inference(sat_conversion,[],[f580]) ).
cnf(s55,plain,
( ~ spl0_19
| ~ spl0_61 ),
inference(sat_conversion,[],[f585]) ).
cnf(s57,plain,
( ~ spl0_34
| ~ spl0_63 ),
inference(sat_conversion,[],[f595]) ).
cnf(s58,plain,
( ~ spl0_34
| spl0_64 ),
inference(sat_conversion,[],[f600]) ).
cnf(s59,plain,
( spl0_48
| ~ spl0_65 ),
inference(sat_conversion,[],[f605]) ).
cnf(s60,plain,
( spl0_48
| spl0_66 ),
inference(sat_conversion,[],[f610]) ).
cnf(s61,plain,
( ~ spl0_38
| spl0_67 ),
inference(sat_conversion,[],[f615]) ).
cnf(s62,plain,
( ~ spl0_38
| spl0_68 ),
inference(sat_conversion,[],[f620]) ).
cnf(s63,plain,
( ~ spl0_30
| spl0_69 ),
inference(sat_conversion,[],[f625]) ).
cnf(s66,plain,
( ~ spl0_42
| spl0_72 ),
inference(sat_conversion,[],[f640]) ).
cnf(s67,plain,
( ~ spl0_46
| ~ spl0_73 ),
inference(sat_conversion,[],[f645]) ).
cnf(s68,plain,
( ~ spl0_46
| spl0_74 ),
inference(sat_conversion,[],[f650]) ).
cnf(s69,plain,
( ~ spl0_56
| ~ spl0_75 ),
inference(sat_conversion,[],[f655]) ).
cnf(s70,plain,
( ~ spl0_56
| spl0_76 ),
inference(sat_conversion,[],[f660]) ).
cnf(s71,plain,
( spl0_37
| ~ spl0_77 ),
inference(sat_conversion,[],[f665]) ).
cnf(s72,plain,
( spl0_37
| ~ spl0_78 ),
inference(sat_conversion,[],[f670]) ).
cnf(s73,plain,
( spl0_37
| spl0_79 ),
inference(sat_conversion,[],[f675]) ).
cnf(s74,plain,
( ~ spl0_32
| spl0_80 ),
inference(sat_conversion,[],[f680]) ).
cnf(s75,plain,
( ~ spl0_32
| ~ spl0_81 ),
inference(sat_conversion,[],[f685]) ).
cnf(s76,plain,
( ~ spl0_32
| spl0_82 ),
inference(sat_conversion,[],[f690]) ).
cnf(s78,plain,
( ~ spl0_35
| ~ spl0_84 ),
inference(sat_conversion,[],[f700]) ).
cnf(s82,plain,
( ~ spl0_22
| spl0_88 ),
inference(sat_conversion,[],[f720]) ).
cnf(s84,plain,
( spl0_29
| spl0_90 ),
inference(sat_conversion,[],[f730]) ).
cnf(s85,plain,
( spl0_29
| ~ spl0_91 ),
inference(sat_conversion,[],[f735]) ).
cnf(s86,plain,
( spl0_54
| spl0_92 ),
inference(sat_conversion,[],[f740]) ).
cnf(s87,plain,
( spl0_54
| spl0_93 ),
inference(sat_conversion,[],[f745]) ).
cnf(s88,plain,
( spl0_53
| spl0_94 ),
inference(sat_conversion,[],[f750]) ).
cnf(s89,plain,
( spl0_53
| ~ spl0_95 ),
inference(sat_conversion,[],[f755]) ).
cnf(s90,plain,
( spl0_51
| ~ spl0_96 ),
inference(sat_conversion,[],[f760]) ).
cnf(s93,plain,
( ~ spl0_99
| spl0_100 ),
inference(sat_conversion,[],[f779]) ).
cnf(s94,plain,
( spl0_101
| spl0_102 ),
inference(sat_conversion,[],[f788]) ).
cnf(s95,plain,
( spl0_101
| ~ spl0_103 ),
inference(sat_conversion,[],[f793]) ).
cnf(s96,plain,
( spl0_43
| ~ spl0_104 ),
inference(sat_conversion,[],[f798]) ).
cnf(s97,plain,
( spl0_43
| ~ spl0_105 ),
inference(sat_conversion,[],[f803]) ).
cnf(s98,plain,
( ~ spl0_19
| ~ spl0_106 ),
inference(sat_conversion,[],[f808]) ).
cnf(s99,plain,
( ~ spl0_19
| spl0_107 ),
inference(sat_conversion,[],[f813]) ).
cnf(s100,plain,
( spl0_48
| spl0_108 ),
inference(sat_conversion,[],[f818]) ).
cnf(s101,plain,
( ~ spl0_38
| spl0_109 ),
inference(sat_conversion,[],[f823]) ).
cnf(s102,plain,
( ~ spl0_30
| ~ spl0_110 ),
inference(sat_conversion,[],[f828]) ).
cnf(s103,plain,
( ~ spl0_30
| spl0_111 ),
inference(sat_conversion,[],[f833]) ).
cnf(s105,plain,
( ~ spl0_42
| ~ spl0_113 ),
inference(sat_conversion,[],[f843]) ).
cnf(s106,plain,
( ~ spl0_42
| spl0_114 ),
inference(sat_conversion,[],[f848]) ).
cnf(s107,plain,
( ~ spl0_46
| ~ spl0_115 ),
inference(sat_conversion,[],[f853]) ).
cnf(s108,plain,
( ~ spl0_56
| ~ spl0_116 ),
inference(sat_conversion,[],[f858]) ).
cnf(s111,plain,
( ~ spl0_35
| ~ spl0_119 ),
inference(sat_conversion,[],[f873]) ).
cnf(s112,plain,
( ~ spl0_35
| spl0_120 ),
inference(sat_conversion,[],[f878]) ).
cnf(s116,plain,
( ~ spl0_22
| spl0_124 ),
inference(sat_conversion,[],[f898]) ).
cnf(s117,plain,
( ~ spl0_22
| ~ spl0_125 ),
inference(sat_conversion,[],[f903]) ).
cnf(s120,plain,
( spl0_29
| spl0_128 ),
inference(sat_conversion,[],[f918]) ).
cnf(s121,plain,
( spl0_54
| spl0_129 ),
inference(sat_conversion,[],[f923]) ).
cnf(s122,plain,
( spl0_53
| spl0_130 ),
inference(sat_conversion,[],[f928]) ).
cnf(s123,plain,
( spl0_51
| ~ spl0_131 ),
inference(sat_conversion,[],[f933]) ).
cnf(s124,plain,
( spl0_51
| ~ spl0_132 ),
inference(sat_conversion,[],[f938]) ).
cnf(s126,plain,
( ~ spl0_99
| spl0_134 ),
inference(sat_conversion,[],[f948]) ).
cnf(s127,plain,
( ~ spl0_99
| ~ spl0_135 ),
inference(sat_conversion,[],[f953]) ).
cnf(s128,plain,
( spl0_101
| ~ spl0_136 ),
inference(sat_conversion,[],[f958]) ).
cnf(s129,plain,
( spl0_45
| ~ spl0_137 ),
inference(sat_conversion,[],[f963]) ).
cnf(s130,plain,
( spl0_45
| spl0_138 ),
inference(sat_conversion,[],[f968]) ).
cnf(s131,plain,
( spl0_45
| ~ spl0_139 ),
inference(sat_conversion,[],[f973]) ).
cnf(s142,plain,
( spl0_30
| ~ spl0_43
| ~ spl0_54 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s144,plain,
( spl0_35
| spl0_99
| ~ spl0_101 ),
inference(sat_conversion,[],[f1022]) ).
cnf(s159,plain,
( spl0_3
| ~ spl0_35 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s169,plain,
( spl0_3
| ~ spl0_99 ),
inference(sat_conversion,[],[f1047]) ).
cnf(s170,plain,
( spl0_3
| spl0_101 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s175,plain,
( ~ spl0_43
| spl0_46 ),
inference(sat_conversion,[],[f1053]) ).
cnf(s176,plain,
( ~ spl0_5
| spl0_61
| spl0_106
| ~ spl0_149 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s192,plain,
( ~ spl0_8
| ~ spl0_102
| spl0_103
| spl0_136 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s203,plain,
( ~ spl0_8
| ~ spl0_90
| spl0_91
| spl0_152 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s205,plain,
( ~ spl0_11
| spl0_61
| spl0_106
| ~ spl0_107 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s215,plain,
( ~ spl0_10
| ~ spl0_69
| spl0_110
| ~ spl0_165 ),
inference(sat_conversion,[],[f1446]) ).
cnf(s222,plain,
( ~ spl0_20
| ~ spl0_100
| ~ spl0_134
| spl0_135 ),
inference(sat_conversion,[],[f1477]) ).
cnf(s227,plain,
( ~ spl0_4
| spl0_61
| spl0_106
| spl0_149 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s242,plain,
( ~ spl0_31
| spl0_60
| spl0_104
| spl0_105 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s264,plain,
( ~ spl0_1
| ~ spl0_69
| spl0_110
| ~ spl0_111 ),
inference(sat_conversion,[],[f1670]) ).
cnf(s292,plain,
( ~ spl0_15
| spl0_73
| ~ spl0_74
| spl0_115 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s304,plain,
( ~ spl0_18
| ~ spl0_92
| ~ spl0_93
| ~ spl0_129 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s312,plain,
( ~ spl0_17
| spl0_77
| spl0_78
| ~ spl0_79 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s334,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_15 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s335,plain,
( ~ spl0_2
| spl0_84
| spl0_119
| ~ spl0_120 ),
inference(sat_conversion,[],[f1917]) ).
cnf(s336,plain,
( ~ spl0_7
| ~ spl0_94
| spl0_95
| ~ spl0_130 ),
inference(sat_conversion,[],[f1918]) ).
cnf(s365,plain,
( ~ spl0_10
| spl0_106
| ~ spl0_107
| ~ spl0_149 ),
inference(sat_conversion,[],[f1946]) ).
cnf(s406,plain,
( ~ spl0_18
| ~ spl0_66
| ~ spl0_108
| ~ spl0_157 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s418,plain,
( ~ spl0_13
| spl0_91
| ~ spl0_128
| spl0_152 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s428,plain,
( ~ spl0_2
| spl0_137
| ~ spl0_138
| spl0_169 ),
inference(sat_conversion,[],[f2048]) ).
cnf(s440,plain,
( ~ spl0_2
| spl0_65
| ~ spl0_108
| spl0_157 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s444,plain,
( ~ spl0_11
| spl0_75
| spl0_116
| ~ spl0_170 ),
inference(sat_conversion,[],[f2064]) ).
cnf(s462,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_139
| ~ spl0_169 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s465,plain,
( ~ spl0_17
| spl0_75
| ~ spl0_76
| spl0_170 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s470,plain,
( ~ spl0_13
| spl0_61
| ~ spl0_107
| spl0_149 ),
inference(sat_conversion,[],[f2134]) ).
cnf(s473,plain,
( ~ spl0_12
| ~ spl0_80
| spl0_81
| ~ spl0_82 ),
inference(sat_conversion,[],[f2137]) ).
cnf(s475,plain,
( ~ spl0_12
| spl0_65
| ~ spl0_66
| ~ spl0_157 ),
inference(sat_conversion,[],[f2139]) ).
cnf(s476,plain,
( ~ spl0_28
| spl0_91
| ~ spl0_128
| ~ spl0_152 ),
inference(sat_conversion,[],[f2140]) ).
cnf(s485,plain,
( ~ spl0_23
| ~ spl0_28
| ~ spl0_93
| ~ spl0_166 ),
inference(sat_conversion,[],[f2184]) ).
cnf(s491,plain,
( ~ spl0_12
| ~ spl0_92
| ~ spl0_93
| spl0_166 ),
inference(sat_conversion,[],[f2238]) ).
cnf(s501,plain,
( ~ spl0_2
| ~ spl0_25
| spl0_31 ),
inference(sat_conversion,[],[f2295]) ).
cnf(s507,plain,
( ~ spl0_2
| ~ spl0_33
| spl0_60
| spl0_104 ),
inference(sat_conversion,[],[f2334]) ).
cnf(s514,plain,
( ~ spl0_9
| ~ spl0_11
| spl0_14 ),
inference(sat_conversion,[],[f2341]) ).
cnf(s526,plain,
( ~ spl0_20
| ~ spl0_88
| spl0_125
| ~ spl0_163 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s545,plain,
( ~ spl0_7
| ~ spl0_88
| ~ spl0_124
| spl0_163 ),
inference(sat_conversion,[],[f2371]) ).
cnf(s548,plain,
( ~ spl0_14
| spl0_137
| spl0_139
| ~ spl0_169 ),
inference(sat_conversion,[],[f2373]) ).
cnf(s553,plain,
( ~ spl0_14
| spl0_106
| ~ spl0_107
| spl0_149 ),
inference(sat_conversion,[],[f2378]) ).
cnf(s572,plain,
( ~ spl0_21
| spl0_137
| ~ spl0_138
| spl0_139 ),
inference(sat_conversion,[],[f2496]) ).
cnf(s574,plain,
( ~ spl0_1
| spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f2498]) ).
cnf(s590,plain,
( ~ spl0_10
| ~ spl0_72
| spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f2514]) ).
cnf(s600,plain,
( ~ spl0_36
| ~ spl0_67
| ~ spl0_68
| ~ spl0_109 ),
inference(sat_conversion,[],[f2622]) ).
cnf(s605,plain,
( ~ spl0_36
| ~ spl0_90
| ~ spl0_128
| ~ spl0_152 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s616,plain,
( ~ spl0_28
| spl0_63
| ~ spl0_64
| ~ spl0_164 ),
inference(sat_conversion,[],[f2635]) ).
cnf(s618,plain,
( ~ spl0_2
| spl0_110
| ~ spl0_111
| spl0_165 ),
inference(sat_conversion,[],[f2637]) ).
cnf(s624,plain,
( ~ spl0_17
| spl0_63
| ~ spl0_64
| spl0_164 ),
inference(sat_conversion,[],[f2704]) ).
cnf(s626,plain,
( ~ spl0_7
| spl0_12
| ~ spl0_17 ),
inference(sat_conversion,[],[f2706]) ).
cnf(s627,plain,
( ~ spl0_4
| spl0_96
| spl0_131
| spl0_132 ),
inference(sat_conversion,[],[f2707]) ).
cnf(s639,plain,
( ~ spl0_4
| ~ spl0_21
| spl0_104
| spl0_105 ),
inference(sat_conversion,[],[f2752]) ).
cnf(s648,plain,
( ~ spl0_17
| ~ spl0_44
| spl0_73
| ~ spl0_74 ),
inference(sat_conversion,[],[f2816]) ).
cnf(s650,plain,
spl0_3,
inference(rat,[],[s144,s159,s169,s170]) ).
cnf(s651,plain,
( spl0_51
| ~ spl0_4 ),
inference(rat,[],[s627,s90,s123,s124]) ).
cnf(s653,plain,
( spl0_43
| ~ spl0_4 ),
inference(rat,[],[s639,s96,s97,s33,s651,s650]) ).
cnf(s654,plain,
( spl0_19
| ~ spl0_43 ),
inference(rat,[],[s616,s624,s57,s58,s48,s26,s648,s53,s68,s67,s175,s650]) ).
cnf(s655,plain,
~ spl0_4,
inference(rat,[],[s4,s176,s205,s365,s227,s55,s98,s99,s654,s653,s650]) ).
cnf(s656,plain,
( spl0_54
| ~ spl0_18 ),
inference(rat,[],[s304,s86,s87,s121]) ).
cnf(s657,plain,
( spl0_48
| ~ spl0_18
| ~ spl0_2 ),
inference(rat,[],[s440,s406,s59,s60,s100]) ).
cnf(s659,plain,
( spl0_101
| ~ spl0_8 ),
inference(rat,[],[s192,s94,s95,s128]) ).
cnf(s660,plain,
( ~ spl0_99
| ~ spl0_20 ),
inference(rat,[],[s222,s93,s126,s127]) ).
cnf(s661,plain,
( ~ spl0_35
| ~ spl0_2 ),
inference(rat,[],[s335,s78,s111,s112]) ).
cnf(s662,plain,
( spl0_17
| spl0_19
| ~ spl0_11
| ~ spl0_2 ),
inference(rat,[],[s526,s545,s82,s116,s117,s40,s3,s657,s659,s8,s144,s514,s660,s548,s9,s428,s572,s129,s130,s131,s27,s661,s242,s54,s96,s97,s654,s650]) ).
cnf(s663,plain,
( spl0_37
| ~ spl0_17 ),
inference(rat,[],[s312,s71,s72,s73]) ).
cnf(s664,plain,
( spl0_29
| ~ spl0_8
| ~ spl0_28 ),
inference(rat,[],[s203,s476,s84,s85,s120]) ).
cnf(s665,plain,
( ~ spl0_32
| ~ spl0_12 ),
inference(rat,[],[s473,s74,s75,s76]) ).
cnf(s666,plain,
( ~ spl0_8
| spl0_32
| ~ spl0_28
| spl0_35 ),
inference(rat,[],[s660,s35,s144,s664,s659,s650]) ).
cnf(s667,plain,
( ~ spl0_34
| ~ spl0_28
| ~ spl0_17 ),
inference(rat,[],[s616,s624,s57,s58]) ).
cnf(s668,plain,
( ~ spl0_30
| ~ spl0_10
| ~ spl0_2 ),
inference(rat,[],[s215,s618,s63,s102,s103]) ).
cnf(s673,plain,
( ~ spl0_22
| ~ spl0_20
| ~ spl0_7 ),
inference(rat,[],[s526,s545,s82,s116,s117]) ).
cnf(s675,plain,
( spl0_19
| spl0_12
| spl0_17
| ~ spl0_2 ),
inference(rat,[],[s40,s673,s657,s3,s8,s659,s462,s144,s5,s660,s548,s9,s428,s572,s129,s130,s131,s27,s242,s54,s96,s97,s654,s661,s650]) ).
cnf(s677,plain,
( spl0_149
| spl0_61
| spl0_106
| ~ spl0_107
| spl0_12 ),
inference(rat,[],[s5,s470,s553,s650]) ).
cnf(s678,plain,
( spl0_12
| spl0_17
| spl0_11
| ~ spl0_2 ),
inference(rat,[],[s4,s176,s365,s677,s55,s98,s99,s675,s650]) ).
cnf(s679,plain,
( spl0_43
| ~ spl0_33
| ~ spl0_2 ),
inference(rat,[],[s507,s54,s96]) ).
cnf(s680,plain,
( ~ spl0_12
| spl0_11
| ~ spl0_2 ),
inference(rat,[],[s491,s485,s86,s87,s22,s142,s668,s4,s334,s292,s67,s68,s107,s175,s679,s19,s16,s665,s650]) ).
cnf(s681,plain,
( spl0_31
| spl0_34
| spl0_7
| ~ spl0_2 ),
inference(rat,[],[s668,s17,s15,s501,s650]) ).
cnf(s682,plain,
( spl0_43
| ~ spl0_31 ),
inference(rat,[],[s242,s54,s96,s97]) ).
cnf(s683,plain,
( spl0_11
| spl0_1 ),
inference(rat,[],[s292,s67,s68,s107,s175,s682,s681,s334,s30,s667,s20,s626,s663,s678,s680,s1,s650,s655]) ).
cnf(s684,plain,
( ~ spl0_19
| ~ spl0_11 ),
inference(rat,[],[s205,s55,s98,s99]) ).
cnf(s685,plain,
( ~ spl0_56
| spl0_1 ),
inference(rat,[],[s465,s444,s69,s70,s108,s662,s684,s683,s1,s650,s655]) ).
cnf(s686,plain,
spl0_1,
inference(rat,[],[s475,s440,s59,s60,s100,s40,s673,s9,s572,s129,s130,s131,s41,s685,s666,s665,s626,s681,s667,s20,s663,s682,s662,s654,s684,s683,s661,s1,s650,s655]) ).
cnf(s687,plain,
( ~ spl0_11
| spl0_17
| ~ spl0_2 ),
inference(rat,[],[s662,s684]) ).
cnf(s688,plain,
( spl0_17
| ~ spl0_2 ),
inference(rat,[],[s678,s680,s687]) ).
cnf(s689,plain,
( ~ spl0_8
| ~ spl0_36
| spl0_32
| spl0_35 ),
inference(rat,[],[s605,s203,s84,s85,s120,s35,s660,s144,s659,s650]) ).
cnf(s690,plain,
( spl0_48
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s475,s440,s59,s60,s100]) ).
cnf(s691,plain,
( spl0_45
| ~ spl0_21 ),
inference(rat,[],[s572,s129,s130,s131]) ).
cnf(s692,plain,
( ~ spl0_56
| ~ spl0_11
| ~ spl0_17 ),
inference(rat,[],[s465,s444,s69,s70,s108]) ).
cnf(s693,plain,
( spl0_8
| spl0_56
| ~ spl0_48
| ~ spl0_7
| spl0_19 ),
inference(rat,[],[s9,s691,s673,s41,s40,s650]) ).
cnf(s694,plain,
( ~ spl0_11
| ~ spl0_2 ),
inference(rat,[],[s24,s689,s666,s693,s692,s690,s665,s626,s15,s682,s654,s668,s684,s574,s661,s688,s650,s686]) ).
cnf(s695,plain,
~ spl0_30,
inference(rat,[],[s264,s63,s102,s103,s686]) ).
cnf(s696,plain,
~ spl0_2,
inference(rat,[],[s418,s476,s18,s24,s600,s61,s62,s101,s52,s85,s120,s14,s626,s680,s694,s688,s661,s650,s695]) ).
cnf(s697,plain,
~ spl0_53,
inference(rat,[],[s36,s696,s650,s695]) ).
cnf(s698,plain,
spl0_130,
inference(rat,[],[s122,s697]) ).
cnf(s699,plain,
~ spl0_95,
inference(rat,[],[s89,s697]) ).
cnf(s700,plain,
spl0_94,
inference(rat,[],[s88,s697]) ).
cnf(s701,plain,
~ spl0_7,
inference(rat,[],[s336,s698,s699,s700]) ).
cnf(s702,plain,
spl0_31,
inference(rat,[],[s15,s650,s695,s701]) ).
cnf(s703,plain,
spl0_43,
inference(rat,[],[s682,s702]) ).
cnf(s704,plain,
spl0_46,
inference(rat,[],[s175,s703]) ).
cnf(s705,plain,
spl0_19,
inference(rat,[],[s654,s703]) ).
cnf(s706,plain,
~ spl0_54,
inference(rat,[],[s142,s695,s703]) ).
cnf(s707,plain,
~ spl0_115,
inference(rat,[],[s107,s704]) ).
cnf(s708,plain,
spl0_74,
inference(rat,[],[s68,s704]) ).
cnf(s709,plain,
~ spl0_73,
inference(rat,[],[s67,s704]) ).
cnf(s710,plain,
spl0_107,
inference(rat,[],[s99,s705]) ).
cnf(s711,plain,
~ spl0_106,
inference(rat,[],[s98,s705]) ).
cnf(s712,plain,
~ spl0_61,
inference(rat,[],[s55,s705]) ).
cnf(s713,plain,
~ spl0_11,
inference(rat,[],[s684,s705]) ).
cnf(s715,plain,
spl0_93,
inference(rat,[],[s87,s706]) ).
cnf(s716,plain,
spl0_92,
inference(rat,[],[s86,s706]) ).
cnf(s717,plain,
~ spl0_18,
inference(rat,[],[s656,s706]) ).
cnf(s718,plain,
~ spl0_15,
inference(rat,[],[s292,s707,s709,s708]) ).
cnf(s720,plain,
spl0_42,
inference(rat,[],[s25,s650,s717,s718]) ).
cnf(s721,plain,
spl0_23,
inference(rat,[],[s22,s695,s650,s718]) ).
cnf(s725,plain,
spl0_114,
inference(rat,[],[s106,s720]) ).
cnf(s726,plain,
~ spl0_113,
inference(rat,[],[s105,s720]) ).
cnf(s727,plain,
spl0_72,
inference(rat,[],[s66,s720]) ).
cnf(s728,plain,
~ spl0_10,
inference(rat,[],[s590,s725,s726,s727]) ).
cnf(s729,plain,
spl0_5,
inference(rat,[],[s4,s713,s650,s728]) ).
cnf(s730,plain,
~ spl0_149,
inference(rat,[],[s176,s712,s711,s729]) ).
cnf(s733,plain,
spl0_12,
inference(rat,[],[s677,s712,s710,s711,s730]) ).
cnf(s736,plain,
~ spl0_32,
inference(rat,[],[s665,s733]) ).
cnf(s737,plain,
spl0_166,
inference(rat,[],[s491,s715,s716,s733]) ).
cnf(s743,plain,
spl0_28,
inference(rat,[],[s19,s650,s713,s736]) ).
cnf(s744,plain,
$false,
inference(rat,[],[s485,s715,s721,s743,s737]) ).
fof(f2818,plain,
$false,
inference(avatar_sat_refutation,[],[s744]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN451-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.16 % Computer : n009.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:04:45 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.16 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.43/0.27 % (3187013)Will run a generic schedule for satisfiability detection.
% 0.43/0.27 % (3187018)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3340205729_2999 on theBenchmark for (2999ds/0Mi)
% 0.43/0.27 % Detected minimum model sizes of [1]
% 0.43/0.27 % Detected maximum model sizes of [29]
% 0.43/0.27 % TRYING [1]
% 0.43/0.27 % TRYING [2]
% 0.43/0.27 % TRYING [3]
% 0.43/0.27 % (3187019)% WARNING: option uhcvi not known.
% 0.43/0.27 % TRYING [4]
% 0.43/0.27 % (3187021)dis+10_1_sil=32000:sp=arity:random_seed=853623526:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.43/0.27 % (3187020)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4042681652:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.43/0.27 % (3187022)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=621658363:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.43/0.27 % (3187024)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2393542699:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.43/0.27 % (3187023)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2621923961:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.43/0.27 % (3187019)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=384763162:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.43/0.27 % TRYING [5]
% 0.43/0.27 % (3187024) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3187013-3187024"...
% 0.43/0.27 % (3187024)...printing done.
% 0.43/0.27 % (3187024)Refutation found. Thanks to Tanya!
% 0.43/0.27 % SZS status Unsatisfiable for theBenchmark
% 0.43/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.43/0.28 % (3187024)------------------------------
% 0.43/0.28 % (3187024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.28 % (3187024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.28 % (3187024)CaDiCaL version: 2.1.3
% 0.43/0.28 % (3187024)Termination reason: Refutation
% 0.43/0.28 % (3187024)Time elapsed: 0.036 s
% 0.43/0.28 % (3187024)Peak memory usage: 13 MB
% 0.43/0.28 % (3187024)Instructions burned: 55 (million)
% 0.43/0.28 % (3187013)Success in time 0.071 s
% 0.43/0.28 % Vampire exiting
%------------------------------------------------------------------------------