%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN489-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:57:49 PM UTC 2026
% Result : Unsatisfiable 0.64s 0.98s
% Output : Refutation 2.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f2,negated_conjecture,
( hskp23
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f4,negated_conjecture,
( ~ hskp30
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
fof(f8,negated_conjecture,
( ~ hskp26
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f13,negated_conjecture,
( ~ hskp21
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
fof(f35,negated_conjecture,
( hskp30
| hskp21
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f37,negated_conjecture,
( hskp21
| hskp2
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp6
| hskp19
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f41,negated_conjecture,
( ~ hskp31
| c0_1(a2597) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp31
| c1_1(a2597) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp31
| c3_1(a2597) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp30
| c0_1(a2558) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp30
| c1_1(a2558) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp30
| c2_1(a2558) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp29
| c1_1(a2556) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp29
| c2_1(a2556) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp29
| c3_1(a2556) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp28
| c0_1(a2529) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp28
| c2_1(a2529) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp28
| c3_1(a2529) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp27
| c1_1(a2614) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp26
| c0_1(a2601) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp26
| c3_1(a2601) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp25
| c0_1(a2564) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f57,negated_conjecture,
( ~ hskp24
| c0_1(a2555) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp24
| c2_1(a2555) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f59,negated_conjecture,
( ~ hskp23
| c0_1(a2553) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp22
| c2_1(a2552) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp21
| c0_1(a2551) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp21
| c1_1(a2551) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp20
| c2_1(a2549) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp19
| c0_1(a2548) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp19
| c3_1(a2548) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f68,negated_conjecture,
( ~ hskp17
| c3_1(a2541) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp16
| c0_1(a2540) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f71,negated_conjecture,
( ~ hskp13
| c1_1(a2534) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp11
| c1_1(a2531) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp11
| c2_1(a2531) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp10
| c3_1(a2528) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp9
| c1_1(a2526) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp9
| c3_1(a2526) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp8
| c0_1(a2525) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp8
| c2_1(a2525) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp7
| c1_1(a2524) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp7
| c3_1(a2524) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp6
| c0_1(a2523) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp6
| c1_1(a2523) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f85,negated_conjecture,
( ~ hskp4
| c2_1(a2521) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp4
| c3_1(a2521) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp2
| c1_1(a2518) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp1
| c2_1(a2517) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ c2_1(a2614)
| ~ hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c3_1(a2614)
| ~ hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c2_1(a2601)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c1_1(a2564)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c2_1(a2564)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c1_1(a2555)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c1_1(a2553)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f96,negated_conjecture,
( ~ c3_1(a2553)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c1_1(a2552)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c3_1(a2552)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c2_1(a2551)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c0_1(a2549)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c1_1(a2549)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f102,negated_conjecture,
( ~ c1_1(a2548)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause102) ).
fof(f104,negated_conjecture,
( ~ c1_1(a2541)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c2_1(a2541)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c2_1(a2540)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c3_1(a2540)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f110,negated_conjecture,
( ~ c0_1(a2536)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c1_1(a2536)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c3_1(a2536)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c0_1(a2534)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c2_1(a2534)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c1_1(a2533)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c2_1(a2533)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c3_1(a2533)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c3_1(a2531)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c0_1(a2528)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c1_1(a2528)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c0_1(a2526)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c3_1(a2525)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c2_1(a2524)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c3_1(a2523)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f126,negated_conjecture,
( ~ c1_1(a2521)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c0_1(a2519)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ c2_1(a2519)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ c3_1(a2519)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
( ~ c0_1(a2518)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f131,negated_conjecture,
( ~ c3_1(a2518)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ c0_1(a2517)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ c3_1(a2517)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f139,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp28
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f140,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp13
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp21
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp23
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f145,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp20
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp9
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f151,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp25
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp8
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f156,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp24
| hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp29
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp25
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f160,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp6
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp31
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f165,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause165) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f172,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f178,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f180,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f186,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c1_1(X1)
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f189,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f191,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause191) ).
fof(f192,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f194,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X1)
| hskp3 ),
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
| ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f197,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c1_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause197) ).
fof(f198,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause198) ).
fof(f199,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c3_1(X0)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| c2_1(X0)
| c1_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c3_1(X2)
| c1_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X2)
| c3_1(X1)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause204) ).
fof(f206,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f207,plain,
( ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f209,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f210,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f209]) ).
fof(f212,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f215,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f216,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f217,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f204,f215,f212,f209,f206]) ).
fof(f219,definition,
( spl0_5
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f220,plain,
( ! [X2] :
( c2_1(X2)
| ~ c3_1(X2)
| c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f222,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f223,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f225,definition,
( spl0_7
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f226,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f203,f225,f212,f222,f219]) ).
fof(f229,definition,
( spl0_8
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f230,plain,
( ! [X2] :
( c2_1(X2)
| ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f229]) ).
fof(f232,definition,
( spl0_9
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f233,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f234,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f202,f209,f212,f232,f229]) ).
fof(f236,definition,
( spl0_10
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f237,plain,
( ! [X2] :
( c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f236]) ).
fof(f239,definition,
( spl0_11
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f240,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f242,definition,
( spl0_12
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f243,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f244,plain,
( spl0_10
| spl0_11
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f201,f242,f212,f239,f236]) ).
fof(f246,definition,
( spl0_13
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f247,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,definition,
( spl0_14
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f250,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f252,definition,
( spl0_15
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f253,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( spl0_13
| spl0_14
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f200,f252,f212,f249,f246]) ).
fof(f255,plain,
( spl0_13
| spl0_1
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f199,f252,f212,f206,f246]) ).
fof(f257,definition,
( spl0_16
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f258,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( spl0_13
| spl0_16
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f198,f232,f212,f257,f246]) ).
fof(f261,definition,
( spl0_17
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f262,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( spl0_16
| spl0_5
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f197,f261,f212,f219,f257]) ).
fof(f265,definition,
( spl0_18
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f266,plain,
( ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,definition,
( spl0_19
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f269,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f268]) ).
fof(f270,plain,
( spl0_18
| spl0_19
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f196,f249,f212,f268,f265]) ).
fof(f272,definition,
( spl0_20
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f273,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c1_1(X2) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f272]) ).
fof(f275,definition,
( spl0_21
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f276,plain,
( ! [X1] :
( c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f278,definition,
( spl0_22
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f279,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f280,plain,
( spl0_20
| spl0_21
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f195,f278,f212,f275,f272]) ).
fof(f282,definition,
( spl0_23
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f284,plain,
( spl0_23
| spl0_22
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f194,f215,f212,f278,f282]) ).
fof(f289,definition,
( spl0_25
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f290,plain,
( ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_26
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f295,plain,
( spl0_26
| spl0_25
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f192,f215,f212,f289,f293]) ).
fof(f297,definition,
( spl0_27
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f299,plain,
( spl0_27
| spl0_14
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f191,f278,f212,f249,f297]) ).
fof(f301,definition,
( spl0_28
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f303,plain,
( spl0_28
| spl0_1
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f190,f209,f212,f206,f301]) ).
fof(f305,definition,
( spl0_29
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f308,definition,
( spl0_30
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f309,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f308]) ).
fof(f310,plain,
( spl0_29
| spl0_30
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f189,f209,f212,f308,f305]) ).
fof(f312,definition,
( spl0_31
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f315,definition,
( spl0_32
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f316,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl0_33
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f321,plain,
( spl0_33
| spl0_14
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f187,f222,f212,f249,f319]) ).
fof(f323,definition,
( spl0_34
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f326,definition,
( spl0_35
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f327,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f326]) ).
fof(f328,plain,
( spl0_34
| spl0_35
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f186,f232,f212,f326,f323]) ).
fof(f336,plain,
( spl0_33
| spl0_30
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f184,f222,f212,f308,f319]) ).
fof(f338,definition,
( spl0_38
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f340,plain,
( spl0_38
| spl0_11
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f183,f308,f212,f239,f338]) ).
fof(f342,definition,
( spl0_39
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f344,plain,
( spl0_39
| spl0_5
| ~ spl0_3
| spl0_32 ),
inference(avatar_split_clause,[],[f182,f315,f212,f219,f342]) ).
fof(f346,definition,
( spl0_40
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f349,definition,
( spl0_41
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f350,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f349]) ).
fof(f351,plain,
( spl0_40
| spl0_35
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f181,f349,f212,f326,f346]) ).
fof(f353,definition,
( spl0_42
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f355,plain,
( spl0_42
| spl0_16
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f180,f236,f212,f257,f353]) ).
fof(f357,definition,
( spl0_43
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f358,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f357]) ).
fof(f361,definition,
( spl0_44
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f363,plain,
( spl0_44
| spl0_21
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f178,f252,f212,f275,f361]) ).
fof(f369,plain,
( spl0_23
| spl0_13
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f175,f257,f212,f246,f282]) ).
fof(f371,definition,
( spl0_46
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f373,plain,
( spl0_46
| spl0_17
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f174,f308,f212,f261,f371]) ).
fof(f374,plain,
( spl0_38
| spl0_5
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f173,f308,f212,f219,f338]) ).
fof(f376,definition,
( spl0_47
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f378,plain,
( spl0_47
| spl0_10
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f172,f349,f212,f236,f376]) ).
fof(f384,definition,
( spl0_49
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f386,plain,
( spl0_49
| spl0_8
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f170,f219,f212,f229,f384]) ).
fof(f388,definition,
( spl0_50
<=> ! [X1] :
( ~ c1_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f389,plain,
( ! [X1] :
( c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f390,plain,
( spl0_29
| spl0_50
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f169,f349,f212,f388,f305]) ).
fof(f392,plain,
( spl0_46
| spl0_20
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f167,f232,f212,f272,f371]) ).
fof(f398,definition,
( spl0_52
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f401,definition,
( spl0_53
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f402,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f403,plain,
( spl0_52
| spl0_53
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f165,f349,f212,f401,f398]) ).
fof(f405,definition,
( spl0_54
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f407,plain,
( spl0_54
| spl0_53
| ~ spl0_3
| spl0_41 ),
inference(avatar_split_clause,[],[f164,f349,f212,f401,f405]) ).
fof(f409,definition,
( spl0_55
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f411,plain,
( spl0_55
| spl0_53
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f163,f236,f212,f401,f409]) ).
fof(f412,plain,
( spl0_52
| spl0_20
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f162,f246,f212,f272,f398]) ).
fof(f414,definition,
( spl0_56
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f417,definition,
( spl0_57
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f419,plain,
( spl0_56
| spl0_57
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f161,f225,f212,f417,f414]) ).
fof(f421,definition,
( spl0_58
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f423,plain,
( spl0_58
| spl0_26
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f160,f215,f212,f293,f421]) ).
fof(f426,definition,
( spl0_59
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f428,plain,
( spl0_58
| spl0_59
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f158,f252,f212,f426,f421]) ).
fof(f429,plain,
( spl0_29
| spl0_39
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f157,f222,f212,f342,f305]) ).
fof(f430,plain,
( spl0_59
| spl0_38
| ~ spl0_3
| spl0_43 ),
inference(avatar_split_clause,[],[f156,f357,f212,f338,f426]) ).
fof(f432,definition,
( spl0_60
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f435,plain,
( spl0_47
| spl0_55
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f154,f239,f212,f409,f376]) ).
fof(f437,definition,
( spl0_61
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f441,plain,
( spl0_23
| spl0_59
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f151,f232,f212,f426,f282]) ).
fof(f448,plain,
( spl0_31
| spl0_54
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f147,f308,f212,f405,f312]) ).
fof(f450,definition,
( spl0_63
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f453,plain,
( spl0_28
| spl0_58
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f145,f261,f212,f421,f301]) ).
fof(f456,plain,
( spl0_52
| spl0_56
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f142,f236,f212,f414,f398]) ).
fof(f457,plain,
( spl0_61
| spl0_33
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f141,f236,f212,f319,f437]) ).
fof(f458,plain,
( spl0_31
| spl0_42
| ~ spl0_3
| spl0_21 ),
inference(avatar_split_clause,[],[f140,f275,f212,f353,f312]) ).
fof(f459,plain,
( spl0_23
| spl0_27
| ~ spl0_3
| spl0_50 ),
inference(avatar_split_clause,[],[f139,f388,f212,f297,f282]) ).
fof(f477,definition,
( spl0_67
<=> c3_1(a2517) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f478,plain,
( ~ c3_1(a2517)
| spl0_67 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f479,plain,
( ~ spl0_52
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f133,f477,f398]) ).
fof(f481,definition,
( spl0_68
<=> c0_1(a2517) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f482,plain,
( ~ c0_1(a2517)
| spl0_68 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f483,plain,
( ~ spl0_52
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f132,f481,f398]) ).
fof(f486,definition,
( spl0_69
<=> c3_1(a2518) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f487,plain,
( ~ c3_1(a2518)
| spl0_69 ),
inference(avatar_component_clause,[],[f486]) ).
fof(f488,plain,
( ~ spl0_46
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f131,f486,f371]) ).
fof(f490,definition,
( spl0_70
<=> c0_1(a2518) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f491,plain,
( ~ c0_1(a2518)
| spl0_70 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f492,plain,
( ~ spl0_46
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f130,f490,f371]) ).
fof(f495,definition,
( spl0_71
<=> c3_1(a2519) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f496,plain,
( ~ c3_1(a2519)
| spl0_71 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f497,plain,
( ~ spl0_23
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f129,f495,f282]) ).
fof(f499,definition,
( spl0_72
<=> c2_1(a2519) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f500,plain,
( ~ c2_1(a2519)
| spl0_72 ),
inference(avatar_component_clause,[],[f499]) ).
fof(f501,plain,
( ~ spl0_23
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f128,f499,f282]) ).
fof(f503,definition,
( spl0_73
<=> c0_1(a2519) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f504,plain,
( ~ c0_1(a2519)
| spl0_73 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f505,plain,
( ~ spl0_23
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f127,f503,f282]) ).
fof(f508,definition,
( spl0_74
<=> c1_1(a2521) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f510,plain,
( ~ spl0_31
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f126,f508,f312]) ).
fof(f518,definition,
( spl0_76
<=> c3_1(a2523) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f519,plain,
( ~ c3_1(a2523)
| spl0_76 ),
inference(avatar_component_clause,[],[f518]) ).
fof(f520,plain,
( ~ spl0_26
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f124,f518,f293]) ).
fof(f523,definition,
( spl0_77
<=> c2_1(a2524) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f524,plain,
( ~ c2_1(a2524)
| spl0_77 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( ~ spl0_47
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f123,f523,f376]) ).
fof(f528,definition,
( spl0_78
<=> c3_1(a2525) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f529,plain,
( ~ c3_1(a2525)
| spl0_78 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f530,plain,
( ~ spl0_55
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f122,f528,f409]) ).
fof(f533,definition,
( spl0_79
<=> c0_1(a2526) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f534,plain,
( ~ c0_1(a2526)
| spl0_79 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f535,plain,
( ~ spl0_54
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f121,f533,f405]) ).
fof(f538,definition,
( spl0_80
<=> c1_1(a2528) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f539,plain,
( ~ c1_1(a2528)
| spl0_80 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( ~ spl0_29
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f120,f538,f305]) ).
fof(f542,definition,
( spl0_81
<=> c0_1(a2528) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f543,plain,
( ~ c0_1(a2528)
| spl0_81 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f544,plain,
( ~ spl0_29
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f119,f542,f305]) ).
fof(f547,definition,
( spl0_82
<=> c3_1(a2531) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f548,plain,
( ~ c3_1(a2531)
| spl0_82 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f549,plain,
( ~ spl0_49
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f118,f547,f384]) ).
fof(f552,definition,
( spl0_83
<=> c3_1(a2533) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f553,plain,
( ~ c3_1(a2533)
| spl0_83 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f554,plain,
( ~ spl0_44
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f117,f552,f361]) ).
fof(f556,definition,
( spl0_84
<=> c2_1(a2533) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f557,plain,
( ~ c2_1(a2533)
| spl0_84 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f558,plain,
( ~ spl0_44
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f116,f556,f361]) ).
fof(f560,definition,
( spl0_85
<=> c1_1(a2533) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f561,plain,
( ~ c1_1(a2533)
| spl0_85 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( ~ spl0_44
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f115,f560,f361]) ).
fof(f565,definition,
( spl0_86
<=> c2_1(a2534) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f566,plain,
( ~ c2_1(a2534)
| spl0_86 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f567,plain,
( ~ spl0_42
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f114,f565,f353]) ).
fof(f569,definition,
( spl0_87
<=> c0_1(a2534) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f570,plain,
( ~ c0_1(a2534)
| spl0_87 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f571,plain,
( ~ spl0_42
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f113,f569,f353]) ).
fof(f574,definition,
( spl0_88
<=> c3_1(a2536) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f575,plain,
( ~ c3_1(a2536)
| spl0_88 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f576,plain,
( ~ spl0_28
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f112,f574,f301]) ).
fof(f578,definition,
( spl0_89
<=> c1_1(a2536) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f579,plain,
( ~ c1_1(a2536)
| spl0_89 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f580,plain,
( ~ spl0_28
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f111,f578,f301]) ).
fof(f582,definition,
( spl0_90
<=> c0_1(a2536) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f583,plain,
( ~ c0_1(a2536)
| spl0_90 ),
inference(avatar_component_clause,[],[f582]) ).
fof(f584,plain,
( ~ spl0_28
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f110,f582,f301]) ).
fof(f596,definition,
( spl0_93
<=> c3_1(a2540) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f597,plain,
( ~ c3_1(a2540)
| spl0_93 ),
inference(avatar_component_clause,[],[f596]) ).
fof(f598,plain,
( ~ spl0_34
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f107,f596,f323]) ).
fof(f600,definition,
( spl0_94
<=> c2_1(a2540) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f601,plain,
( ~ c2_1(a2540)
| spl0_94 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f602,plain,
( ~ spl0_34
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f106,f600,f323]) ).
fof(f605,definition,
( spl0_95
<=> c2_1(a2541) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f606,plain,
( ~ c2_1(a2541)
| spl0_95 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f607,plain,
( ~ spl0_40
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f105,f605,f346]) ).
fof(f609,definition,
( spl0_96
<=> c1_1(a2541) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f610,plain,
( ~ c1_1(a2541)
| spl0_96 ),
inference(avatar_component_clause,[],[f609]) ).
fof(f611,plain,
( ~ spl0_40
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f104,f609,f346]) ).
fof(f619,definition,
( spl0_98
<=> c1_1(a2548) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f620,plain,
( ~ c1_1(a2548)
| spl0_98 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f621,plain,
( ~ spl0_63
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f102,f619,f450]) ).
fof(f624,definition,
( spl0_99
<=> c1_1(a2549) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f626,plain,
( ~ spl0_58
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f101,f624,f421]) ).
fof(f628,definition,
( spl0_100
<=> c0_1(a2549) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f629,plain,
( ~ c0_1(a2549)
| spl0_100 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( ~ spl0_58
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f100,f628,f421]) ).
fof(f633,definition,
( spl0_101
<=> c2_1(a2551) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f634,plain,
( ~ c2_1(a2551)
| spl0_101 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f635,plain,
( ~ spl0_33
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f99,f633,f319]) ).
fof(f638,definition,
( spl0_102
<=> c3_1(a2552) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f639,plain,
( ~ c3_1(a2552)
| spl0_102 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f640,plain,
( ~ spl0_61
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f98,f638,f437]) ).
fof(f642,definition,
( spl0_103
<=> c1_1(a2552) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f643,plain,
( ~ c1_1(a2552)
| spl0_103 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f644,plain,
( ~ spl0_61
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f97,f642,f437]) ).
fof(f647,definition,
( spl0_104
<=> c3_1(a2553) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f648,plain,
( ~ c3_1(a2553)
| spl0_104 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f649,plain,
( ~ spl0_56
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f96,f647,f414]) ).
fof(f651,definition,
( spl0_105
<=> c1_1(a2553) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f652,plain,
( ~ c1_1(a2553)
| spl0_105 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f653,plain,
( ~ spl0_56
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f95,f651,f414]) ).
fof(f656,definition,
( spl0_106
<=> c1_1(a2555) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f657,plain,
( ~ c1_1(a2555)
| spl0_106 ),
inference(avatar_component_clause,[],[f656]) ).
fof(f658,plain,
( ~ spl0_38
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f94,f656,f338]) ).
fof(f661,definition,
( spl0_107
<=> c2_1(a2564) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f662,plain,
( ~ c2_1(a2564)
| spl0_107 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f663,plain,
( ~ spl0_59
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f93,f661,f426]) ).
fof(f665,definition,
( spl0_108
<=> c1_1(a2564) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f666,plain,
( ~ c1_1(a2564)
| spl0_108 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f667,plain,
( ~ spl0_59
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f92,f665,f426]) ).
fof(f669,definition,
( spl0_109
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f672,definition,
( spl0_110
<=> c2_1(a2601) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f673,plain,
( ~ c2_1(a2601)
| spl0_110 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f674,plain,
( ~ spl0_109
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f91,f672,f669]) ).
fof(f676,definition,
( spl0_111
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f679,definition,
( spl0_112
<=> c3_1(a2614) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f680,plain,
( ~ c3_1(a2614)
| spl0_112 ),
inference(avatar_component_clause,[],[f679]) ).
fof(f681,plain,
( ~ spl0_111
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f90,f679,f676]) ).
fof(f683,definition,
( spl0_113
<=> c2_1(a2614) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f684,plain,
( ~ c2_1(a2614)
| spl0_113 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f685,plain,
( ~ spl0_111
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f89,f683,f676]) ).
fof(f687,definition,
( spl0_114
<=> c2_1(a2517) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f688,plain,
( c2_1(a2517)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f689,plain,
( spl0_114
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f88,f398,f687]) ).
fof(f691,definition,
( spl0_115
<=> c1_1(a2518) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f692,plain,
( c1_1(a2518)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f691]) ).
fof(f693,plain,
( spl0_115
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f87,f371,f691]) ).
fof(f695,definition,
( spl0_116
<=> c3_1(a2521) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f696,plain,
( c3_1(a2521)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f695]) ).
fof(f697,plain,
( spl0_116
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f86,f312,f695]) ).
fof(f699,definition,
( spl0_117
<=> c2_1(a2521) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f700,plain,
( c2_1(a2521)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f701,plain,
( spl0_117
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f85,f312,f699]) ).
fof(f711,definition,
( spl0_120
<=> c1_1(a2523) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f712,plain,
( c1_1(a2523)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f711]) ).
fof(f713,plain,
( spl0_120
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f82,f293,f711]) ).
fof(f715,definition,
( spl0_121
<=> c0_1(a2523) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f716,plain,
( c0_1(a2523)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f717,plain,
( spl0_121
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f81,f293,f715]) ).
fof(f719,definition,
( spl0_122
<=> c3_1(a2524) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f720,plain,
( c3_1(a2524)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f721,plain,
( spl0_122
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f80,f376,f719]) ).
fof(f723,definition,
( spl0_123
<=> c1_1(a2524) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f725,plain,
( spl0_123
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f79,f376,f723]) ).
fof(f727,definition,
( spl0_124
<=> c2_1(a2525) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f728,plain,
( c2_1(a2525)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( spl0_124
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f78,f409,f727]) ).
fof(f731,definition,
( spl0_125
<=> c0_1(a2525) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f733,plain,
( spl0_125
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f77,f409,f731]) ).
fof(f735,definition,
( spl0_126
<=> c3_1(a2526) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f736,plain,
( c3_1(a2526)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f735]) ).
fof(f737,plain,
( spl0_126
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f76,f405,f735]) ).
fof(f739,definition,
( spl0_127
<=> c1_1(a2526) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f740,plain,
( c1_1(a2526)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f739]) ).
fof(f741,plain,
( spl0_127
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f75,f405,f739]) ).
fof(f743,definition,
( spl0_128
<=> c3_1(a2528) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f744,plain,
( c3_1(a2528)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f745,plain,
( spl0_128
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f74,f305,f743]) ).
fof(f747,definition,
( spl0_129
<=> c2_1(a2531) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f748,plain,
( c2_1(a2531)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f749,plain,
( spl0_129
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f73,f384,f747]) ).
fof(f751,definition,
( spl0_130
<=> c1_1(a2531) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f752,plain,
( c1_1(a2531)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f751]) ).
fof(f753,plain,
( spl0_130
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f72,f384,f751]) ).
fof(f755,definition,
( spl0_131
<=> c1_1(a2534) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f756,plain,
( c1_1(a2534)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f757,plain,
( spl0_131
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f71,f353,f755]) ).
fof(f763,definition,
( spl0_133
<=> c0_1(a2540) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f764,plain,
( c0_1(a2540)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f765,plain,
( spl0_133
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f69,f323,f763]) ).
fof(f767,definition,
( spl0_134
<=> c3_1(a2541) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f768,plain,
( c3_1(a2541)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f767]) ).
fof(f769,plain,
( spl0_134
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f68,f346,f767]) ).
fof(f779,definition,
( spl0_137
<=> c3_1(a2548) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f780,plain,
( c3_1(a2548)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f781,plain,
( spl0_137
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f65,f450,f779]) ).
fof(f783,definition,
( spl0_138
<=> c0_1(a2548) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f784,plain,
( c0_1(a2548)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f785,plain,
( spl0_138
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f64,f450,f783]) ).
fof(f787,definition,
( spl0_139
<=> c2_1(a2549) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f788,plain,
( c2_1(a2549)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f789,plain,
( spl0_139
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f63,f421,f787]) ).
fof(f791,definition,
( spl0_140
<=> c1_1(a2551) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f792,plain,
( c1_1(a2551)
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f791]) ).
fof(f793,plain,
( spl0_140
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f62,f319,f791]) ).
fof(f795,definition,
( spl0_141
<=> c0_1(a2551) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f796,plain,
( c0_1(a2551)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f797,plain,
( spl0_141
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f61,f319,f795]) ).
fof(f799,definition,
( spl0_142
<=> c2_1(a2552) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f800,plain,
( c2_1(a2552)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f799]) ).
fof(f801,plain,
( spl0_142
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f60,f437,f799]) ).
fof(f803,definition,
( spl0_143
<=> c0_1(a2553) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f804,plain,
( c0_1(a2553)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f805,plain,
( spl0_143
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f59,f414,f803]) ).
fof(f807,definition,
( spl0_144
<=> c2_1(a2555) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f808,plain,
( c2_1(a2555)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f809,plain,
( spl0_144
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f58,f338,f807]) ).
fof(f811,definition,
( spl0_145
<=> c0_1(a2555) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f813,plain,
( spl0_145
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f57,f338,f811]) ).
fof(f815,definition,
( spl0_146
<=> c0_1(a2564) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f816,plain,
( c0_1(a2564)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f817,plain,
( spl0_146
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f56,f426,f815]) ).
fof(f819,definition,
( spl0_147
<=> c3_1(a2601) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f820,plain,
( c3_1(a2601)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f819]) ).
fof(f821,plain,
( spl0_147
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f55,f669,f819]) ).
fof(f823,definition,
( spl0_148
<=> c0_1(a2601) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f824,plain,
( c0_1(a2601)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f823]) ).
fof(f825,plain,
( spl0_148
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f54,f669,f823]) ).
fof(f827,definition,
( spl0_149
<=> c1_1(a2614) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f829,plain,
( spl0_149
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f53,f676,f827]) ).
fof(f831,definition,
( spl0_150
<=> c3_1(a2529) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f832,plain,
( c3_1(a2529)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f831]) ).
fof(f834,plain,
( spl0_150
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f52,f297,f831]) ).
fof(f836,definition,
( spl0_151
<=> c2_1(a2529) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f837,plain,
( c2_1(a2529)
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f838,plain,
( spl0_151
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f51,f297,f836]) ).
fof(f840,definition,
( spl0_152
<=> c0_1(a2529) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f842,plain,
( spl0_152
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f50,f297,f840]) ).
fof(f844,definition,
( spl0_153
<=> c3_1(a2556) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f847,plain,
( spl0_153
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f49,f342,f844]) ).
fof(f849,definition,
( spl0_154
<=> c2_1(a2556) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f850,plain,
( c2_1(a2556)
| ~ spl0_154 ),
inference(avatar_component_clause,[],[f849]) ).
fof(f851,plain,
( spl0_154
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f48,f342,f849]) ).
fof(f853,definition,
( spl0_155
<=> c1_1(a2556) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f854,plain,
( c1_1(a2556)
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f855,plain,
( spl0_155
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f47,f342,f853]) ).
fof(f857,definition,
( spl0_156
<=> c2_1(a2558) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f858,plain,
( c2_1(a2558)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f860,plain,
( spl0_156
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f46,f432,f857]) ).
fof(f862,definition,
( spl0_157
<=> c1_1(a2558) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f863,plain,
( c1_1(a2558)
| ~ spl0_157 ),
inference(avatar_component_clause,[],[f862]) ).
fof(f864,plain,
( spl0_157
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f45,f432,f862]) ).
fof(f866,definition,
( spl0_158
<=> c0_1(a2558) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f867,plain,
( c0_1(a2558)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f868,plain,
( spl0_158
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f44,f432,f866]) ).
fof(f870,definition,
( spl0_159
<=> c3_1(a2597) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f871,plain,
( c3_1(a2597)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f873,plain,
( spl0_159
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f43,f417,f870]) ).
fof(f875,definition,
( spl0_160
<=> c1_1(a2597) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f876,plain,
( c1_1(a2597)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f877,plain,
( spl0_160
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f42,f417,f875]) ).
fof(f879,definition,
( spl0_161
<=> c0_1(a2597) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f880,plain,
( c0_1(a2597)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f879]) ).
fof(f881,plain,
( spl0_161
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f41,f417,f879]) ).
fof(f885,plain,
( spl0_34
| spl0_63
| spl0_26 ),
inference(avatar_split_clause,[],[f38,f293,f450,f323]) ).
fof(f886,plain,
( spl0_58
| spl0_46
| spl0_33 ),
inference(avatar_split_clause,[],[f37,f319,f371,f421]) ).
fof(f889,plain,
( spl0_109
| spl0_33
| spl0_60 ),
inference(avatar_split_clause,[],[f35,f432,f319,f669]) ).
fof(f912,plain,
( spl0_3
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f13,f319,f212]) ).
fof(f917,plain,
( spl0_3
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f8,f669,f212]) ).
fof(f921,plain,
( spl0_3
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f4,f432,f212]) ).
fof(f923,plain,
( spl0_111
| spl0_56 ),
inference(avatar_split_clause,[],[f2,f414,f676]) ).
fof(f933,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_5
| ~ spl0_9 ),
inference(resolution,[],[f233,f220]) ).
fof(f934,plain,
( ! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_9 ),
inference(duplicate_literal_removal,[],[f933]) ).
fof(f936,plain,
( ! [X2] :
( c1_1(X2)
| ~ c0_1(X2) )
| ~ spl0_9
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f237,f233]) ).
fof(f943,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f327,f210]) ).
fof(f947,plain,
( ~ c0_1(a2533)
| c1_1(a2533)
| ~ spl0_10
| spl0_84 ),
inference(resolution,[],[f237,f557]) ).
fof(f950,plain,
( ~ c0_1(a2533)
| ~ spl0_10
| spl0_84
| spl0_85 ),
inference(forward_subsumption_resolution,[],[f947,f561]) ).
fof(f951,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1) )
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f240,f220]) ).
fof(f955,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_7
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f240,f226]) ).
fof(f958,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_7
| ~ spl0_8
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f230,f955]) ).
fof(f959,plain,
( c0_1(a2528)
| ~ spl0_7
| ~ spl0_8
| ~ spl0_11
| ~ spl0_128 ),
inference(resolution,[],[f958,f744]) ).
fof(f960,plain,
( $false
| ~ spl0_7
| ~ spl0_8
| ~ spl0_11
| spl0_81
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f959,f543]) ).
fof(f961,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_11
| spl0_81
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f960]) ).
fof(f964,plain,
( c1_1(a2528)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_128 ),
inference(resolution,[],[f951,f744]) ).
fof(f965,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| spl0_80
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f964,f539]) ).
fof(f966,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_80
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f965]) ).
fof(f971,definition,
( spl0_162
<=> c0_1(a2556) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f977,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_1
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f230,f207]) ).
fof(f978,plain,
( c0_1(a2528)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_128 ),
inference(resolution,[],[f977,f744]) ).
fof(f980,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| spl0_81
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f978,f543]) ).
fof(f981,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_81
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f980]) ).
fof(f991,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2) )
| ~ spl0_9
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f247,f233]) ).
fof(f1021,plain,
( c1_1(a2549)
| ~ spl0_9
| ~ spl0_13
| ~ spl0_139 ),
inference(resolution,[],[f991,f788]) ).
fof(f1044,plain,
( c1_1(a2521)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_116 ),
inference(resolution,[],[f696,f951]) ).
fof(f1064,plain,
( ~ c0_1(a2597)
| ~ c1_1(a2597)
| ~ spl0_2
| ~ spl0_159 ),
inference(resolution,[],[f871,f210]) ).
fof(f1073,plain,
( ~ c0_1(a2564)
| ~ spl0_9
| ~ spl0_10
| spl0_108 ),
inference(resolution,[],[f936,f666]) ).
fof(f1077,plain,
( $false
| ~ spl0_9
| ~ spl0_10
| spl0_108
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f1073,f816]) ).
fof(f1078,plain,
( ~ spl0_9
| ~ spl0_10
| spl0_108
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f1077]) ).
fof(f1085,plain,
( spl0_74
| ~ spl0_5
| ~ spl0_11
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1044,f695,f239,f219,f508]) ).
fof(f1086,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f253,f216]) ).
fof(f1127,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_4
| ~ spl0_15
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f309,f1086]) ).
fof(f1145,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_9
| ~ spl0_13
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f316,f991]) ).
fof(f1152,plain,
( ~ c0_1(a2548)
| ~ spl0_9
| ~ spl0_10
| spl0_98 ),
inference(resolution,[],[f620,f936]) ).
fof(f1153,plain,
( c1_1(a2548)
| ~ spl0_5
| ~ spl0_11
| ~ spl0_137 ),
inference(resolution,[],[f780,f951]) ).
fof(f1154,plain,
( $false
| ~ spl0_5
| ~ spl0_11
| spl0_98
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f1153,f620]) ).
fof(f1155,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_98
| ~ spl0_137 ),
inference(avatar_contradiction_clause,[],[f1154]) ).
fof(f1156,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_4
| ~ spl0_14
| ~ spl0_15
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f250,f1127]) ).
fof(f1158,plain,
( c3_1(a2531)
| ~ spl0_9
| ~ spl0_13
| ~ spl0_32
| ~ spl0_129 ),
inference(resolution,[],[f748,f1145]) ).
fof(f1164,plain,
( $false
| ~ spl0_9
| ~ spl0_13
| ~ spl0_32
| spl0_82
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f1158,f548]) ).
fof(f1165,plain,
( ~ spl0_9
| ~ spl0_13
| ~ spl0_32
| spl0_82
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f1164]) ).
fof(f1172,plain,
( $false
| ~ spl0_9
| ~ spl0_10
| spl0_98
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f1152,f784]) ).
fof(f1173,plain,
( ~ spl0_9
| ~ spl0_10
| spl0_98
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f1172]) ).
fof(f1175,plain,
( ~ c0_1(a2548)
| ~ spl0_4
| ~ spl0_14
| ~ spl0_15
| ~ spl0_30
| spl0_98 ),
inference(resolution,[],[f1156,f620]) ).
fof(f1179,plain,
( $false
| ~ spl0_4
| ~ spl0_14
| ~ spl0_15
| ~ spl0_30
| spl0_98
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f1175,f784]) ).
fof(f1180,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_15
| ~ spl0_30
| spl0_98
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f1179]) ).
fof(f1184,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_4
| ~ spl0_12
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f243,f1086]) ).
fof(f1187,plain,
( ! [X0] : ~ c0_1(X0)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f1184,f1127]) ).
fof(f1191,plain,
( c1_1(a2552)
| ~ spl0_9
| ~ spl0_13
| ~ spl0_142 ),
inference(resolution,[],[f800,f991]) ).
fof(f1192,plain,
( c1_1(a2552)
| ~ c0_1(a2552)
| ~ spl0_9
| ~ spl0_142 ),
inference(resolution,[],[f800,f233]) ).
fof(f1193,plain,
( ~ c0_1(a2552)
| ~ spl0_9
| spl0_103
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f1192,f643]) ).
fof(f1194,plain,
( $false
| ~ spl0_9
| ~ spl0_13
| spl0_103
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f1191,f643]) ).
fof(f1195,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_103
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f1194]) ).
fof(f1203,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_138 ),
inference(resolution,[],[f1187,f784]) ).
fof(f1204,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_133 ),
inference(resolution,[],[f1187,f764]) ).
fof(f1205,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_121 ),
inference(resolution,[],[f1187,f716]) ).
fof(f1206,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_121 ),
inference(avatar_contradiction_clause,[],[f1205]) ).
fof(f1207,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f1204]) ).
fof(f1208,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f1203]) ).
fof(f1216,definition,
( spl0_164
<=> c3_1(a2564) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1245,plain,
( ~ c0_1(a2597)
| ~ spl0_2
| ~ spl0_159
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f1064,f876]) ).
fof(f1250,plain,
( spl0_14
| ~ spl0_5
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f934,f232,f219,f249]) ).
fof(f1251,plain,
( ~ spl0_161
| ~ spl0_2
| ~ spl0_159
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f1245,f875,f870,f209,f879]) ).
fof(f1285,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_5
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f210,f951]) ).
fof(f1315,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f207,f216]) ).
fof(f1325,plain,
( ~ c0_1(a2601)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_11
| ~ spl0_147 ),
inference(resolution,[],[f820,f1285]) ).
fof(f1381,plain,
( ~ c3_1(a2558)
| ~ c0_1(a2558)
| ~ spl0_4
| ~ spl0_156 ),
inference(resolution,[],[f858,f216]) ).
fof(f1397,plain,
( ~ c0_1(a2529)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_151 ),
inference(resolution,[],[f837,f1086]) ).
fof(f1398,plain,
( ~ c3_1(a2529)
| ~ c0_1(a2529)
| ~ spl0_4
| ~ spl0_151 ),
inference(resolution,[],[f837,f216]) ).
fof(f1405,plain,
( ~ spl0_152
| ~ spl0_4
| ~ spl0_15
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f1397,f836,f252,f215,f840]) ).
fof(f1431,plain,
( c3_1(a2558)
| ~ c1_1(a2558)
| ~ spl0_32
| ~ spl0_156 ),
inference(resolution,[],[f316,f858]) ).
fof(f1436,plain,
( c3_1(a2517)
| ~ c1_1(a2517)
| ~ spl0_32
| ~ spl0_114 ),
inference(resolution,[],[f316,f688]) ).
fof(f1437,plain,
( ~ c1_1(a2517)
| ~ spl0_32
| spl0_67
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f1436,f478]) ).
fof(f1441,plain,
( ! [X0] :
( c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_32
| ~ spl0_41 ),
inference(forward_subsumption_resolution,[],[f350,f316]) ).
fof(f1442,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_11
| ~ spl0_147
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f1325,f824]) ).
fof(f1443,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_11
| ~ spl0_147
| ~ spl0_148 ),
inference(avatar_contradiction_clause,[],[f1442]) ).
fof(f1451,plain,
( ~ c1_1(a2518)
| ~ spl0_32
| ~ spl0_41
| spl0_69 ),
inference(resolution,[],[f1441,f487]) ).
fof(f1457,plain,
( $false
| ~ spl0_32
| ~ spl0_41
| spl0_69
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f1451,f692]) ).
fof(f1458,plain,
( ~ spl0_32
| ~ spl0_41
| spl0_69
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f1457]) ).
fof(f1468,plain,
( c3_1(a2614)
| ~ c1_1(a2614)
| ~ spl0_41
| spl0_113 ),
inference(resolution,[],[f350,f684]) ).
fof(f1471,plain,
( c3_1(a2551)
| ~ c1_1(a2551)
| ~ spl0_41
| spl0_101 ),
inference(resolution,[],[f350,f634]) ).
fof(f1475,plain,
( c3_1(a2534)
| ~ c1_1(a2534)
| ~ spl0_41
| spl0_86 ),
inference(resolution,[],[f350,f566]) ).
fof(f1478,plain,
( c3_1(a2519)
| ~ c1_1(a2519)
| ~ spl0_41
| spl0_72 ),
inference(resolution,[],[f350,f500]) ).
fof(f1480,plain,
( ~ c1_1(a2519)
| ~ spl0_41
| spl0_71
| spl0_72 ),
inference(forward_subsumption_resolution,[],[f1478,f496]) ).
fof(f1481,plain,
( c3_1(a2534)
| ~ spl0_41
| spl0_86
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f1475,f756]) ).
fof(f1485,definition,
( spl0_166
<=> c1_1(a2601) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1493,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_15
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f358,f1086]) ).
fof(f1494,plain,
( ~ c0_1(a2597)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_160 ),
inference(resolution,[],[f1493,f876]) ).
fof(f1498,plain,
( ~ c0_1(a2551)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_140 ),
inference(resolution,[],[f1493,f792]) ).
fof(f1550,plain,
( ~ c1_1(a2534)
| c0_1(a2534)
| ~ spl0_50
| spl0_86 ),
inference(resolution,[],[f389,f566]) ).
fof(f1557,plain,
( c0_1(a2534)
| ~ spl0_50
| spl0_86
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f1550,f756]) ).
fof(f1566,plain,
( $false
| ~ spl0_50
| spl0_86
| spl0_87
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f1557,f570]) ).
fof(f1567,plain,
( ~ spl0_50
| spl0_86
| spl0_87
| ~ spl0_131 ),
inference(avatar_contradiction_clause,[],[f1566]) ).
fof(f1573,plain,
( c3_1(a2614)
| c0_1(a2614)
| ~ spl0_53
| spl0_113 ),
inference(resolution,[],[f402,f684]) ).
fof(f1582,plain,
( c3_1(a2533)
| c0_1(a2533)
| ~ spl0_53
| spl0_84 ),
inference(resolution,[],[f402,f557]) ).
fof(f1583,plain,
( c3_1(a2519)
| c0_1(a2519)
| ~ spl0_53
| spl0_72 ),
inference(resolution,[],[f402,f500]) ).
fof(f1590,definition,
( spl0_168
<=> c0_1(a2614) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1598,plain,
( ~ c0_1(a2525)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_124 ),
inference(resolution,[],[f728,f1086]) ).
fof(f1603,definition,
( spl0_169
<=> c1_1(a2525) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1606,plain,
( ~ spl0_125
| ~ spl0_4
| ~ spl0_15
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f1598,f727,f252,f215,f731]) ).
fof(f1618,plain,
( spl0_168
| spl0_112
| ~ spl0_53
| spl0_113 ),
inference(avatar_split_clause,[],[f1573,f683,f401,f679,f1590]) ).
fof(f1623,definition,
( spl0_170
<=> c3_1(a2551) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1627,plain,
( c3_1(a2551)
| ~ spl0_170 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1638,plain,
( ~ c0_1(a2555)
| ~ spl0_4
| ~ spl0_15
| ~ spl0_144 ),
inference(resolution,[],[f808,f1086]) ).
fof(f1651,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f279,f233]) ).
fof(f1660,plain,
( ~ c1_1(a2526)
| ~ spl0_2
| ~ spl0_35
| ~ spl0_126 ),
inference(resolution,[],[f943,f736]) ).
fof(f1661,plain,
( ~ c1_1(a2524)
| ~ spl0_2
| ~ spl0_35
| ~ spl0_122 ),
inference(resolution,[],[f943,f720]) ).
fof(f1668,plain,
( $false
| ~ spl0_2
| ~ spl0_35
| ~ spl0_126
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f1660,f740]) ).
fof(f1669,plain,
( ~ spl0_2
| ~ spl0_35
| ~ spl0_126
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f1668]) ).
fof(f1725,plain,
( ~ c0_1(a2555)
| ~ spl0_9
| ~ spl0_10
| spl0_106 ),
inference(resolution,[],[f657,f936]) ).
fof(f1726,plain,
( ~ spl0_145
| ~ spl0_9
| ~ spl0_10
| spl0_106 ),
inference(avatar_split_clause,[],[f1725,f656,f236,f232,f811]) ).
fof(f1775,plain,
( ~ c3_1(a2541)
| c1_1(a2541)
| ~ spl0_5
| spl0_95 ),
inference(resolution,[],[f220,f606]) ).
fof(f1784,plain,
( c1_1(a2541)
| ~ spl0_5
| spl0_95
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f1775,f768]) ).
fof(f1788,plain,
( $false
| ~ spl0_5
| spl0_95
| spl0_96
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f1784,f610]) ).
fof(f1789,plain,
( ~ spl0_5
| spl0_95
| spl0_96
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f1788]) ).
fof(f1874,plain,
( ~ c1_1(a2614)
| c0_1(a2614)
| ~ spl0_21
| spl0_112 ),
inference(resolution,[],[f276,f680]) ).
fof(f1882,plain,
( ~ c1_1(a2518)
| c0_1(a2518)
| ~ spl0_21
| spl0_69 ),
inference(resolution,[],[f276,f487]) ).
fof(f1889,plain,
( c0_1(a2518)
| ~ spl0_21
| spl0_69
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f1882,f692]) ).
fof(f1893,plain,
( $false
| ~ spl0_21
| spl0_69
| spl0_70
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f1889,f491]) ).
fof(f1894,plain,
( ~ spl0_21
| spl0_69
| spl0_70
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f1893]) ).
fof(f1897,plain,
( ! [X1] :
( c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_5
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f290,f220]) ).
fof(f1914,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_9
| ~ spl0_22
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f309,f1651]) ).
fof(f1924,plain,
( ~ c0_1(a2525)
| ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_78 ),
inference(resolution,[],[f1914,f529]) ).
fof(f1925,plain,
( ~ c0_1(a2523)
| ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_76 ),
inference(resolution,[],[f1914,f519]) ).
fof(f1932,plain,
( $false
| ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_76
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f1925,f716]) ).
fof(f1933,plain,
( ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_76
| ~ spl0_121 ),
inference(avatar_contradiction_clause,[],[f1932]) ).
fof(f1945,plain,
( c0_1(a2558)
| ~ c3_1(a2558)
| ~ spl0_1
| ~ spl0_156 ),
inference(resolution,[],[f207,f858]) ).
fof(f1950,plain,
( c0_1(a2549)
| ~ c3_1(a2549)
| ~ spl0_1
| ~ spl0_139 ),
inference(resolution,[],[f207,f788]) ).
fof(f1956,plain,
( ~ c3_1(a2549)
| ~ spl0_1
| spl0_100
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f1950,f629]) ).
fof(f1958,definition,
( spl0_173
<=> c3_1(a2555) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1965,plain,
( ~ c3_1(a2558)
| ~ c1_1(a2558)
| ~ spl0_7
| ~ spl0_156 ),
inference(resolution,[],[f226,f858]) ).
fof(f1985,definition,
( spl0_175
<=> c3_1(a2558) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1986,plain,
( ~ c3_1(a2558)
| spl0_175 ),
inference(avatar_component_clause,[],[f1985]) ).
fof(f1993,plain,
( c3_1(a2552)
| ~ c0_1(a2552)
| ~ spl0_15
| ~ spl0_142 ),
inference(resolution,[],[f253,f800]) ).
fof(f1996,plain,
( c3_1(a2525)
| ~ c0_1(a2525)
| ~ spl0_15
| ~ spl0_124 ),
inference(resolution,[],[f253,f728]) ).
fof(f2009,plain,
( c0_1(a2517)
| ~ c1_1(a2517)
| ~ spl0_16
| ~ spl0_114 ),
inference(resolution,[],[f258,f688]) ).
fof(f2010,plain,
( ~ c1_1(a2517)
| ~ spl0_16
| spl0_68
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2009,f482]) ).
fof(f2018,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_15
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f309,f253]) ).
fof(f2022,plain,
( ~ c0_1(a2553)
| ~ spl0_15
| ~ spl0_30
| spl0_104 ),
inference(resolution,[],[f2018,f648]) ).
fof(f2025,plain,
( ~ c0_1(a2540)
| ~ spl0_15
| ~ spl0_30
| spl0_93 ),
inference(resolution,[],[f2018,f597]) ).
fof(f2028,plain,
( ~ c0_1(a2523)
| ~ spl0_15
| ~ spl0_30
| spl0_76 ),
inference(resolution,[],[f2018,f519]) ).
fof(f2035,plain,
( $false
| ~ spl0_15
| ~ spl0_30
| spl0_76
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f2028,f716]) ).
fof(f2036,plain,
( ~ spl0_15
| ~ spl0_30
| spl0_76
| ~ spl0_121 ),
inference(avatar_contradiction_clause,[],[f2035]) ).
fof(f2037,plain,
( $false
| ~ spl0_15
| ~ spl0_30
| spl0_93
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2025,f764]) ).
fof(f2038,plain,
( ~ spl0_15
| ~ spl0_30
| spl0_93
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f2037]) ).
fof(f2078,plain,
( ! [X1] :
( c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_5
| ~ spl0_25
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f309,f1897]) ).
fof(f2083,plain,
( ~ c0_1(a2601)
| ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_110 ),
inference(resolution,[],[f2078,f673]) ).
fof(f2084,plain,
( ~ c0_1(a2551)
| ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_101 ),
inference(resolution,[],[f2078,f634]) ).
fof(f2096,plain,
( $false
| ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_101
| ~ spl0_141 ),
inference(forward_subsumption_resolution,[],[f2084,f796]) ).
fof(f2097,plain,
( ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_101
| ~ spl0_141 ),
inference(avatar_contradiction_clause,[],[f2096]) ).
fof(f2098,plain,
( $false
| ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_110
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f2083,f824]) ).
fof(f2099,plain,
( ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_110
| ~ spl0_148 ),
inference(avatar_contradiction_clause,[],[f2098]) ).
fof(f2144,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_9
| ~ spl0_30 ),
inference(resolution,[],[f309,f233]) ).
fof(f2145,plain,
( c3_1(a2614)
| ~ c0_1(a2614)
| ~ spl0_30
| spl0_113 ),
inference(resolution,[],[f309,f684]) ).
fof(f2148,plain,
( c3_1(a2540)
| ~ c0_1(a2540)
| ~ spl0_30
| spl0_94 ),
inference(resolution,[],[f309,f601]) ).
fof(f2154,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_9
| ~ spl0_30 ),
inference(duplicate_literal_removal,[],[f2144]) ).
fof(f2155,plain,
( ~ c0_1(a2540)
| ~ spl0_30
| spl0_93
| spl0_94 ),
inference(forward_subsumption_resolution,[],[f2148,f597]) ).
fof(f2158,plain,
( ~ c0_1(a2614)
| ~ spl0_30
| spl0_112
| spl0_113 ),
inference(forward_subsumption_resolution,[],[f2145,f680]) ).
fof(f2159,plain,
( $false
| ~ spl0_30
| spl0_93
| spl0_94
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2155,f764]) ).
fof(f2160,plain,
( ~ spl0_30
| spl0_93
| spl0_94
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f2159]) ).
fof(f2202,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f243,f1315]) ).
fof(f2209,plain,
( spl0_17
| ~ spl0_9
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f2154,f308,f232,f261]) ).
fof(f2224,plain,
( ~ c3_1(a2558)
| ~ spl0_1
| ~ spl0_4
| ~ spl0_12
| ~ spl0_156 ),
inference(forward_subsumption_resolution,[],[f1945,f2202]) ).
fof(f2226,plain,
( ~ spl0_175
| ~ spl0_1
| ~ spl0_4
| ~ spl0_12
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f2224,f857,f242,f215,f206,f1985]) ).
fof(f2304,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_21
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f327,f276]) ).
fof(f2372,plain,
( spl0_99
| ~ spl0_9
| ~ spl0_13
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1021,f787,f246,f232,f624]) ).
fof(f2380,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_12
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f243,f309]) ).
fof(f2381,plain,
( ~ c3_1(a2558)
| ~ spl0_4
| ~ spl0_156
| ~ spl0_158 ),
inference(forward_subsumption_resolution,[],[f1381,f867]) ).
fof(f2383,plain,
( ~ spl0_175
| ~ spl0_4
| ~ spl0_156
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f2381,f866,f857,f215,f1985]) ).
fof(f2384,plain,
( c3_1(a2551)
| ~ c0_1(a2551)
| ~ spl0_30
| spl0_101 ),
inference(resolution,[],[f634,f309]) ).
fof(f2387,plain,
( c3_1(a2564)
| ~ c0_1(a2564)
| ~ spl0_30
| spl0_107 ),
inference(resolution,[],[f662,f309]) ).
fof(f2388,plain,
( ~ c3_1(a2564)
| c1_1(a2564)
| ~ spl0_5
| spl0_107 ),
inference(resolution,[],[f662,f220]) ).
fof(f2396,plain,
( spl0_108
| ~ spl0_164
| ~ spl0_5
| spl0_107 ),
inference(avatar_split_clause,[],[f2388,f661,f219,f1216,f665]) ).
fof(f2448,plain,
( c1_1(a2552)
| c0_1(a2552)
| ~ spl0_13
| ~ spl0_142 ),
inference(resolution,[],[f247,f800]) ).
fof(f2449,plain,
( c1_1(a2549)
| c0_1(a2549)
| ~ spl0_13
| ~ spl0_139 ),
inference(resolution,[],[f247,f788]) ).
fof(f2452,plain,
( c1_1(a2517)
| c0_1(a2517)
| ~ spl0_13
| ~ spl0_114 ),
inference(resolution,[],[f247,f688]) ).
fof(f2501,plain,
( ~ spl0_149
| spl0_112
| ~ spl0_41
| spl0_113 ),
inference(avatar_split_clause,[],[f1468,f683,f349,f679,f827]) ).
fof(f2508,plain,
( c0_1(a2534)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_41
| spl0_86
| ~ spl0_131 ),
inference(resolution,[],[f977,f1481]) ).
fof(f2509,plain,
( c0_1(a2526)
| ~ spl0_1
| ~ spl0_8
| ~ spl0_126 ),
inference(resolution,[],[f977,f736]) ).
fof(f2513,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| spl0_79
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f2509,f534]) ).
fof(f2514,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_79
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f2513]) ).
fof(f2515,plain,
( $false
| ~ spl0_1
| ~ spl0_8
| ~ spl0_41
| spl0_86
| spl0_87
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f2508,f570]) ).
fof(f2516,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_41
| spl0_86
| spl0_87
| ~ spl0_131 ),
inference(avatar_contradiction_clause,[],[f2515]) ).
fof(f2523,plain,
( ~ c3_1(a2558)
| ~ spl0_7
| ~ spl0_156
| ~ spl0_157 ),
inference(forward_subsumption_resolution,[],[f1965,f863]) ).
fof(f2532,plain,
( spl0_168
| ~ spl0_149
| ~ spl0_21
| spl0_112 ),
inference(avatar_split_clause,[],[f1874,f679,f275,f827,f1590]) ).
fof(f2538,plain,
( ~ spl0_175
| ~ spl0_7
| ~ spl0_156
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f2523,f862,f857,f225,f1985]) ).
fof(f2565,plain,
( c0_1(a2518)
| ~ spl0_21
| ~ spl0_35
| ~ spl0_115 ),
inference(resolution,[],[f2304,f692]) ).
fof(f2566,plain,
( $false
| ~ spl0_21
| ~ spl0_35
| spl0_70
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f2565,f491]) ).
fof(f2567,plain,
( ~ spl0_21
| ~ spl0_35
| spl0_70
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f2566]) ).
fof(f2607,plain,
( ~ spl0_123
| ~ spl0_2
| ~ spl0_35
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1661,f719,f326,f209,f723]) ).
fof(f2622,plain,
( ~ c3_1(a2521)
| ~ spl0_1
| ~ spl0_4
| ~ spl0_117 ),
inference(resolution,[],[f700,f1315]) ).
fof(f2623,plain,
( $false
| ~ spl0_1
| ~ spl0_4
| ~ spl0_116
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f2622,f696]) ).
fof(f2624,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_116
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f2623]) ).
fof(f2660,plain,
( ~ c0_1(a2564)
| c1_1(a2564)
| ~ spl0_10
| spl0_107 ),
inference(resolution,[],[f237,f662]) ).
fof(f2665,plain,
( ~ c0_1(a2564)
| ~ spl0_10
| spl0_107
| spl0_108 ),
inference(forward_subsumption_resolution,[],[f2660,f666]) ).
fof(f2683,plain,
( c0_1(a2556)
| ~ c1_1(a2556)
| ~ spl0_16
| ~ spl0_154 ),
inference(resolution,[],[f258,f850]) ).
fof(f2725,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f279,f258]) ).
fof(f2728,plain,
( ~ c1_1(a2558)
| ~ spl0_16
| ~ spl0_22
| ~ spl0_156 ),
inference(resolution,[],[f2725,f858]) ).
fof(f2729,plain,
( ~ c1_1(a2556)
| ~ spl0_16
| ~ spl0_22
| ~ spl0_154 ),
inference(resolution,[],[f2725,f850]) ).
fof(f2742,plain,
( $false
| ~ spl0_16
| ~ spl0_22
| ~ spl0_156
| ~ spl0_157 ),
inference(forward_subsumption_resolution,[],[f2728,f863]) ).
fof(f2743,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_156
| ~ spl0_157 ),
inference(avatar_contradiction_clause,[],[f2742]) ).
fof(f2754,plain,
( c0_1(a2552)
| c1_1(a2552)
| ~ spl0_20
| spl0_102 ),
inference(resolution,[],[f273,f639]) ).
fof(f2756,plain,
( c0_1(a2549)
| c1_1(a2549)
| ~ spl0_1
| ~ spl0_20
| spl0_100
| ~ spl0_139 ),
inference(resolution,[],[f273,f1956]) ).
fof(f2763,plain,
( c0_1(a2517)
| c1_1(a2517)
| ~ spl0_20
| spl0_67 ),
inference(resolution,[],[f273,f478]) ).
fof(f2764,plain,
( c0_1(a2536)
| c1_1(a2536)
| ~ spl0_20
| spl0_88 ),
inference(resolution,[],[f273,f575]) ).
fof(f2766,plain,
( c0_1(a2519)
| c1_1(a2519)
| ~ spl0_20
| spl0_71 ),
inference(resolution,[],[f273,f496]) ).
fof(f2769,plain,
( c1_1(a2519)
| ~ spl0_20
| spl0_71
| spl0_73 ),
inference(forward_subsumption_resolution,[],[f2766,f504]) ).
fof(f2771,plain,
( c1_1(a2536)
| ~ spl0_20
| spl0_88
| spl0_90 ),
inference(forward_subsumption_resolution,[],[f2764,f583]) ).
fof(f2772,plain,
( c1_1(a2517)
| ~ spl0_20
| spl0_67
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f2763,f482]) ).
fof(f2773,plain,
( c1_1(a2549)
| ~ spl0_1
| ~ spl0_20
| spl0_100
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f2756,f629]) ).
fof(f2781,plain,
( $false
| ~ spl0_20
| ~ spl0_41
| spl0_71
| spl0_72
| spl0_73 ),
inference(forward_subsumption_resolution,[],[f2769,f1480]) ).
fof(f2782,plain,
( ~ spl0_20
| ~ spl0_41
| spl0_71
| spl0_72
| spl0_73 ),
inference(avatar_contradiction_clause,[],[f2781]) ).
fof(f2785,plain,
( $false
| ~ spl0_20
| spl0_88
| spl0_89
| spl0_90 ),
inference(forward_subsumption_resolution,[],[f2771,f579]) ).
fof(f2786,plain,
( ~ spl0_20
| spl0_88
| spl0_89
| spl0_90 ),
inference(avatar_contradiction_clause,[],[f2785]) ).
fof(f2787,plain,
( $false
| ~ spl0_16
| ~ spl0_20
| spl0_67
| spl0_68
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2772,f2010]) ).
fof(f2788,plain,
( ~ spl0_16
| ~ spl0_20
| spl0_67
| spl0_68
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f2787]) ).
fof(f2797,plain,
( c1_1(a2549)
| ~ spl0_13
| spl0_100
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f2449,f629]) ).
fof(f2802,plain,
( c0_1(a2533)
| ~ spl0_53
| spl0_83
| spl0_84 ),
inference(forward_subsumption_resolution,[],[f1582,f553]) ).
fof(f2803,plain,
( c3_1(a2519)
| ~ spl0_53
| spl0_72
| spl0_73 ),
inference(forward_subsumption_resolution,[],[f1583,f504]) ).
fof(f2815,plain,
( spl0_99
| ~ spl0_13
| spl0_100
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f2797,f787,f628,f246,f624]) ).
fof(f2817,plain,
( $false
| ~ spl0_10
| ~ spl0_53
| spl0_83
| spl0_84
| spl0_85 ),
inference(forward_subsumption_resolution,[],[f2802,f950]) ).
fof(f2818,plain,
( ~ spl0_10
| ~ spl0_53
| spl0_83
| spl0_84
| spl0_85 ),
inference(avatar_contradiction_clause,[],[f2817]) ).
fof(f2825,plain,
( ~ c0_1(a2552)
| ~ spl0_15
| spl0_102
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f1993,f639]) ).
fof(f2827,plain,
( ~ c0_1(a2525)
| ~ spl0_15
| spl0_78
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f1996,f529]) ).
fof(f2839,plain,
( ~ spl0_140
| spl0_170
| ~ spl0_41
| spl0_101 ),
inference(avatar_split_clause,[],[f1471,f633,f349,f1623,f791]) ).
fof(f2890,plain,
( ~ c3_1(a2556)
| ~ c1_1(a2556)
| ~ spl0_7
| ~ spl0_154 ),
inference(resolution,[],[f226,f850]) ).
fof(f2903,plain,
( ~ c0_1(a2551)
| ~ c3_1(a2551)
| ~ spl0_12
| spl0_101 ),
inference(resolution,[],[f243,f634]) ).
fof(f2911,plain,
( ! [X1] :
( ~ c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f223,f210]) ).
fof(f2914,plain,
( ~ spl0_170
| ~ spl0_141
| ~ spl0_12
| spl0_101 ),
inference(avatar_split_clause,[],[f2903,f633,f242,f795,f1623]) ).
fof(f2915,plain,
( ~ c0_1(a2558)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_157 ),
inference(resolution,[],[f2911,f863]) ).
fof(f2916,plain,
( ~ c0_1(a2556)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_155 ),
inference(resolution,[],[f2911,f854]) ).
fof(f2917,plain,
( ~ c0_1(a2551)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_140 ),
inference(resolution,[],[f2911,f792]) ).
fof(f2926,plain,
( ~ spl0_141
| ~ spl0_2
| ~ spl0_6
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f2917,f791,f222,f209,f795]) ).
fof(f2927,plain,
( ~ spl0_162
| ~ spl0_2
| ~ spl0_6
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f2916,f853,f222,f209,f971]) ).
fof(f2943,plain,
( ~ spl0_158
| ~ spl0_2
| ~ spl0_6
| ~ spl0_157 ),
inference(avatar_split_clause,[],[f2915,f862,f222,f209,f866]) ).
fof(f2947,plain,
( ~ c0_1(a2601)
| ~ c3_1(a2601)
| ~ spl0_12
| spl0_110 ),
inference(resolution,[],[f673,f243]) ).
fof(f2971,plain,
( ~ spl0_125
| ~ spl0_15
| spl0_78
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f2827,f727,f528,f252,f731]) ).
fof(f2981,plain,
( ~ c0_1(a2601)
| ~ c1_1(a2601)
| ~ spl0_2
| ~ spl0_147 ),
inference(resolution,[],[f820,f210]) ).
fof(f2982,plain,
( ~ spl0_166
| ~ spl0_148
| ~ spl0_2
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f2981,f819,f209,f823,f1485]) ).
fof(f3011,plain,
( ~ c0_1(a2601)
| ~ spl0_12
| spl0_110
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f2947,f820]) ).
fof(f3012,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f250,f210]) ).
fof(f3031,plain,
( ~ spl0_148
| ~ spl0_12
| spl0_110
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3011,f819,f672,f242,f823]) ).
fof(f3047,plain,
( ~ c0_1(a2601)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_147 ),
inference(resolution,[],[f3012,f820]) ).
fof(f3057,plain,
( ~ spl0_148
| ~ spl0_2
| ~ spl0_14
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f3047,f819,f249,f209,f823]) ).
fof(f3058,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1
| ~ spl0_2
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f207,f3012]) ).
fof(f3069,plain,
( ~ c3_1(a2521)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_14
| ~ spl0_117 ),
inference(resolution,[],[f3058,f700]) ).
fof(f3072,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_14
| ~ spl0_116
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f3069,f696]) ).
fof(f3073,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_14
| ~ spl0_116
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f3072]) ).
fof(f3077,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_9
| ~ spl0_12
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f233,f2380]) ).
fof(f3085,plain,
( ~ c0_1(a2548)
| ~ spl0_9
| ~ spl0_12
| ~ spl0_30
| spl0_98 ),
inference(resolution,[],[f3077,f620]) ).
fof(f3092,plain,
( $false
| ~ spl0_9
| ~ spl0_12
| ~ spl0_30
| spl0_98
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f3085,f784]) ).
fof(f3093,plain,
( ~ spl0_9
| ~ spl0_12
| ~ spl0_30
| spl0_98
| ~ spl0_138 ),
inference(avatar_contradiction_clause,[],[f3092]) ).
fof(f3104,plain,
( $false
| ~ spl0_15
| ~ spl0_30
| spl0_104
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f2022,f804]) ).
fof(f3105,plain,
( ~ spl0_15
| ~ spl0_30
| spl0_104
| ~ spl0_143 ),
inference(avatar_contradiction_clause,[],[f3104]) ).
fof(f3120,plain,
( ~ spl0_155
| ~ spl0_16
| ~ spl0_22
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f2729,f849,f278,f257,f853]) ).
fof(f3127,plain,
( ~ spl0_125
| ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_78 ),
inference(avatar_split_clause,[],[f1924,f528,f308,f278,f232,f731]) ).
fof(f3144,plain,
( spl0_71
| ~ spl0_53
| spl0_72
| spl0_73 ),
inference(avatar_split_clause,[],[f2803,f503,f499,f401,f495]) ).
fof(f3159,plain,
( c1_1(a2552)
| ~ spl0_9
| ~ spl0_20
| spl0_102
| spl0_103
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f2754,f1193]) ).
fof(f3165,plain,
( spl0_99
| ~ spl0_1
| ~ spl0_20
| spl0_100
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f2773,f787,f628,f272,f206,f624]) ).
fof(f3174,plain,
( $false
| ~ spl0_9
| ~ spl0_20
| spl0_102
| spl0_103
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f3159,f643]) ).
fof(f3175,plain,
( ~ spl0_9
| ~ spl0_20
| spl0_102
| spl0_103
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f3174]) ).
fof(f3182,plain,
( ~ c3_1(a2555)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_144 ),
inference(resolution,[],[f955,f808]) ).
fof(f3191,plain,
( ~ spl0_173
| ~ spl0_7
| ~ spl0_11
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f3182,f807,f239,f225,f1958]) ).
fof(f3203,plain,
( c1_1(a2555)
| ~ c0_1(a2555)
| ~ spl0_9
| ~ spl0_144 ),
inference(resolution,[],[f233,f808]) ).
fof(f3206,plain,
( c1_1(a2525)
| ~ c0_1(a2525)
| ~ spl0_9
| ~ spl0_124 ),
inference(resolution,[],[f233,f728]) ).
fof(f3210,plain,
( ~ c0_1(a2551)
| ~ spl0_2
| ~ spl0_14
| ~ spl0_170 ),
inference(resolution,[],[f1627,f3012]) ).
fof(f3211,plain,
( ~ c0_1(a2551)
| ~ c1_1(a2551)
| ~ spl0_2
| ~ spl0_170 ),
inference(resolution,[],[f1627,f210]) ).
fof(f3213,plain,
( $false
| ~ spl0_2
| ~ spl0_14
| ~ spl0_141
| ~ spl0_170 ),
inference(forward_subsumption_resolution,[],[f3210,f796]) ).
fof(f3214,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_141
| ~ spl0_170 ),
inference(avatar_contradiction_clause,[],[f3213]) ).
fof(f3225,plain,
( ~ c1_1(a2558)
| ~ spl0_32
| ~ spl0_156
| spl0_175 ),
inference(forward_subsumption_resolution,[],[f1431,f1986]) ).
fof(f3228,plain,
( $false
| ~ spl0_32
| ~ spl0_156
| ~ spl0_157
| spl0_175 ),
inference(forward_subsumption_resolution,[],[f3225,f863]) ).
fof(f3229,plain,
( ~ spl0_32
| ~ spl0_156
| ~ spl0_157
| spl0_175 ),
inference(avatar_contradiction_clause,[],[f3228]) ).
fof(f3231,definition,
( spl0_182
<=> c0_1(a2552) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f3240,plain,
( c0_1(a2552)
| ~ spl0_13
| spl0_103
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f2448,f643]) ).
fof(f3242,plain,
( c0_1(a2517)
| ~ spl0_13
| ~ spl0_32
| spl0_67
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2452,f1437]) ).
fof(f3250,plain,
( spl0_182
| ~ spl0_13
| spl0_103
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f3240,f799,f642,f246,f3231]) ).
fof(f3251,plain,
( $false
| ~ spl0_13
| ~ spl0_32
| spl0_67
| spl0_68
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3242,f482]) ).
fof(f3252,plain,
( ~ spl0_13
| ~ spl0_32
| spl0_67
| spl0_68
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f3251]) ).
fof(f3257,plain,
( ~ spl0_182
| ~ spl0_15
| spl0_102
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f2825,f799,f638,f252,f3231]) ).
fof(f3279,plain,
( ~ c1_1(a2531)
| ~ spl0_16
| ~ spl0_22
| ~ spl0_129 ),
inference(resolution,[],[f2725,f748]) ).
fof(f3281,plain,
( $false
| ~ spl0_16
| ~ spl0_22
| ~ spl0_129
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f3279,f752]) ).
fof(f3282,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_129
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f3281]) ).
fof(f3287,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_16
| ~ spl0_22
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f389,f2725]) ).
fof(f3344,definition,
( spl0_183
<=> c1_1(a2517) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f3359,plain,
( ~ spl0_183
| ~ spl0_32
| spl0_67
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f1437,f687,f477,f315,f3344]) ).
fof(f3432,plain,
( ~ c0_1(a2553)
| c1_1(a2553)
| ~ spl0_17
| spl0_104 ),
inference(resolution,[],[f262,f648]) ).
fof(f3449,plain,
( c1_1(a2553)
| ~ spl0_17
| spl0_104
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f3432,f804]) ).
fof(f3454,plain,
( $false
| ~ spl0_17
| spl0_104
| spl0_105
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f3449,f652]) ).
fof(f3455,plain,
( ~ spl0_17
| spl0_104
| spl0_105
| ~ spl0_143 ),
inference(avatar_contradiction_clause,[],[f3454]) ).
fof(f3458,plain,
( ! [X2] :
( c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f230,f243]) ).
fof(f3488,plain,
( c0_1(a2518)
| ~ spl0_16
| ~ spl0_22
| ~ spl0_50
| ~ spl0_115 ),
inference(resolution,[],[f3287,f692]) ).
fof(f3489,plain,
( $false
| ~ spl0_16
| ~ spl0_22
| ~ spl0_50
| spl0_70
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f3488,f491]) ).
fof(f3490,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_50
| spl0_70
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f3489]) ).
fof(f3506,plain,
( ~ c3_1(a2524)
| ~ spl0_8
| ~ spl0_12
| spl0_77 ),
inference(resolution,[],[f3458,f524]) ).
fof(f3510,plain,
( $false
| ~ spl0_8
| ~ spl0_12
| spl0_77
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f3506,f720]) ).
fof(f3511,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_77
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f3510]) ).
fof(f3515,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f240,f2725]) ).
fof(f3516,plain,
( ~ c0_1(a2551)
| ~ spl0_2
| ~ spl0_140
| ~ spl0_170 ),
inference(forward_subsumption_resolution,[],[f3211,f792]) ).
fof(f3518,plain,
( ~ spl0_141
| ~ spl0_2
| ~ spl0_140
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f3516,f1623,f791,f209,f795]) ).
fof(f3531,plain,
( ~ c3_1(a2529)
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_151 ),
inference(resolution,[],[f3515,f837]) ).
fof(f3532,plain,
( ~ c3_1(a2555)
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_144 ),
inference(resolution,[],[f3515,f808]) ).
fof(f3536,plain,
( ~ c3_1(a2521)
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_117 ),
inference(resolution,[],[f3515,f700]) ).
fof(f3538,plain,
( $false
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_116
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f3536,f696]) ).
fof(f3539,plain,
( ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_116
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f3538]) ).
fof(f3541,plain,
( ~ spl0_173
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f3532,f807,f278,f257,f239,f1958]) ).
fof(f3542,plain,
( $false
| ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_150
| ~ spl0_151 ),
inference(forward_subsumption_resolution,[],[f3531,f832]) ).
fof(f3543,plain,
( ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_150
| ~ spl0_151 ),
inference(avatar_contradiction_clause,[],[f3542]) ).
fof(f3551,plain,
( ~ spl0_146
| ~ spl0_10
| spl0_107
| spl0_108 ),
inference(avatar_split_clause,[],[f2665,f665,f661,f236,f815]) ).
fof(f3559,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_8
| ~ spl0_16
| ~ spl0_22 ),
inference(resolution,[],[f230,f2725]) ).
fof(f3590,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f253,f237]) ).
fof(f3593,plain,
( c3_1(a2555)
| ~ c0_1(a2555)
| ~ spl0_15
| ~ spl0_144 ),
inference(resolution,[],[f253,f808]) ).
fof(f3599,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0) )
| ~ spl0_10
| ~ spl0_15 ),
inference(duplicate_literal_removal,[],[f3590]) ).
fof(f3603,plain,
( spl0_17
| ~ spl0_10
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f3599,f252,f236,f261]) ).
fof(f3619,plain,
( ~ c0_1(a2552)
| c1_1(a2552)
| ~ spl0_17
| spl0_102 ),
inference(resolution,[],[f262,f639]) ).
fof(f3623,plain,
( ~ c0_1(a2525)
| c1_1(a2525)
| ~ spl0_17
| spl0_78 ),
inference(resolution,[],[f262,f529]) ).
fof(f3638,plain,
( ! [X2] :
( ~ c2_1(X2)
| c3_1(X2) )
| ~ spl0_15
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f266,f253]) ).
fof(f3644,plain,
( c3_1(a2552)
| ~ spl0_15
| ~ spl0_18
| ~ spl0_142 ),
inference(resolution,[],[f3638,f800]) ).
fof(f3648,plain,
( c3_1(a2517)
| ~ spl0_15
| ~ spl0_18
| ~ spl0_114 ),
inference(resolution,[],[f3638,f688]) ).
fof(f3649,plain,
( $false
| ~ spl0_15
| ~ spl0_18
| spl0_67
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3648,f478]) ).
fof(f3650,plain,
( ~ spl0_15
| ~ spl0_18
| spl0_67
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f3649]) ).
fof(f3653,plain,
( $false
| ~ spl0_15
| ~ spl0_18
| spl0_102
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f3644,f639]) ).
fof(f3654,plain,
( ~ spl0_15
| ~ spl0_18
| spl0_102
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f3653]) ).
fof(f3656,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_16
| ~ spl0_19
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f269,f2725]) ).
fof(f3665,plain,
( c3_1(a2517)
| ~ spl0_16
| ~ spl0_19
| ~ spl0_22
| ~ spl0_114 ),
inference(resolution,[],[f3656,f688]) ).
fof(f3666,plain,
( $false
| ~ spl0_16
| ~ spl0_19
| ~ spl0_22
| spl0_67
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3665,f478]) ).
fof(f3667,plain,
( ~ spl0_16
| ~ spl0_19
| ~ spl0_22
| spl0_67
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f3666]) ).
fof(f3688,plain,
( ~ spl0_145
| ~ spl0_4
| ~ spl0_15
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1638,f807,f252,f215,f811]) ).
fof(f3689,plain,
( $false
| ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_160
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f1494,f880]) ).
fof(f3690,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_160
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f3689]) ).
fof(f3692,plain,
( ~ spl0_141
| ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f1498,f791,f357,f252,f215,f795]) ).
fof(f3717,plain,
( ~ spl0_168
| ~ spl0_30
| spl0_112
| spl0_113 ),
inference(avatar_split_clause,[],[f2158,f683,f679,f308,f1590]) ).
fof(f3721,plain,
( ~ spl0_145
| spl0_173
| ~ spl0_15
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f3593,f807,f252,f1958,f811]) ).
fof(f3750,plain,
( ~ spl0_155
| ~ spl0_153
| ~ spl0_7
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f2890,f849,f225,f844,f853]) ).
fof(f3763,plain,
( ~ spl0_155
| spl0_162
| ~ spl0_16
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f2683,f849,f257,f971,f853]) ).
fof(f3769,plain,
( spl0_35
| ~ spl0_8
| ~ spl0_16
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f3559,f278,f257,f229,f326]) ).
fof(f3779,plain,
( ~ c0_1(a2601)
| c1_1(a2601)
| ~ spl0_10
| spl0_110 ),
inference(resolution,[],[f673,f237]) ).
fof(f3782,plain,
( spl0_166
| ~ spl0_148
| ~ spl0_10
| spl0_110 ),
inference(avatar_split_clause,[],[f3779,f672,f236,f823,f1485]) ).
fof(f3823,plain,
( ~ c0_1(a2558)
| ~ c1_1(a2558)
| ~ spl0_6
| spl0_175 ),
inference(resolution,[],[f223,f1986]) ).
fof(f3824,plain,
( ~ c0_1(a2614)
| ~ c1_1(a2614)
| ~ spl0_6
| spl0_112 ),
inference(resolution,[],[f223,f680]) ).
fof(f3831,plain,
( ~ c0_1(a2525)
| ~ c1_1(a2525)
| ~ spl0_6
| spl0_78 ),
inference(resolution,[],[f223,f529]) ).
fof(f3832,plain,
( ~ c0_1(a2523)
| ~ c1_1(a2523)
| ~ spl0_6
| spl0_76 ),
inference(resolution,[],[f223,f519]) ).
fof(f3839,plain,
( ~ c1_1(a2523)
| ~ spl0_6
| spl0_76
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f3832,f716]) ).
fof(f3844,plain,
( ~ c0_1(a2558)
| ~ spl0_6
| ~ spl0_157
| spl0_175 ),
inference(forward_subsumption_resolution,[],[f3823,f863]) ).
fof(f3845,plain,
( $false
| ~ spl0_6
| spl0_76
| ~ spl0_120
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f3839,f712]) ).
fof(f3846,plain,
( ~ spl0_6
| spl0_76
| ~ spl0_120
| ~ spl0_121 ),
inference(avatar_contradiction_clause,[],[f3845]) ).
fof(f3849,plain,
( ~ spl0_158
| ~ spl0_6
| ~ spl0_157
| spl0_175 ),
inference(avatar_split_clause,[],[f3844,f1985,f862,f222,f866]) ).
fof(f3855,plain,
( ~ spl0_152
| ~ spl0_150
| ~ spl0_4
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f1398,f836,f215,f831,f840]) ).
fof(f3890,plain,
( spl0_169
| ~ spl0_125
| ~ spl0_17
| spl0_78 ),
inference(avatar_split_clause,[],[f3623,f528,f261,f731,f1603]) ).
fof(f3894,plain,
( ~ spl0_149
| ~ spl0_168
| ~ spl0_6
| spl0_112 ),
inference(avatar_split_clause,[],[f3824,f679,f222,f1590,f827]) ).
fof(f3895,plain,
( ~ spl0_169
| ~ spl0_125
| ~ spl0_6
| spl0_78 ),
inference(avatar_split_clause,[],[f3831,f528,f222,f731,f1603]) ).
fof(f3896,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_4
| ~ spl0_5
| ~ spl0_15 ),
inference(resolution,[],[f1086,f220]) ).
fof(f3909,plain,
( spl0_14
| ~ spl0_4
| ~ spl0_5
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f3896,f252,f219,f215,f249]) ).
fof(f3917,plain,
( ~ spl0_145
| spl0_106
| ~ spl0_9
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f3203,f807,f232,f656,f811]) ).
fof(f3918,plain,
( ~ spl0_125
| spl0_169
| ~ spl0_9
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f3206,f727,f232,f1603,f731]) ).
fof(f3922,plain,
( spl0_103
| spl0_182
| ~ spl0_20
| spl0_102 ),
inference(avatar_split_clause,[],[f2754,f638,f272,f3231,f642]) ).
fof(f3928,plain,
( spl0_183
| ~ spl0_20
| spl0_67
| spl0_68 ),
inference(avatar_split_clause,[],[f2772,f481,f477,f272,f3344]) ).
fof(f3931,plain,
( ~ spl0_141
| spl0_170
| ~ spl0_30
| spl0_101 ),
inference(avatar_split_clause,[],[f2384,f633,f308,f1623,f795]) ).
fof(f3932,plain,
( ~ spl0_146
| spl0_164
| ~ spl0_30
| spl0_107 ),
inference(avatar_split_clause,[],[f2387,f661,f308,f1216,f815]) ).
fof(f3935,plain,
( spl0_103
| ~ spl0_182
| ~ spl0_17
| spl0_102 ),
inference(avatar_split_clause,[],[f3619,f638,f261,f3231,f642]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f217]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f227]) ).
cnf(s3,plain,
( spl0_2
| ~ spl0_3
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f234]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_10
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f244]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f254]) ).
cnf(s6,plain,
( spl0_1
| ~ spl0_3
| spl0_13
| spl0_15 ),
inference(sat_conversion,[],[f255]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_9
| spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f259]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_5
| spl0_16
| spl0_17 ),
inference(sat_conversion,[],[f263]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_14
| spl0_18
| spl0_19 ),
inference(sat_conversion,[],[f270]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_20
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f280]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_4
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f284]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_4
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f295]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_14
| spl0_22
| spl0_27 ),
inference(sat_conversion,[],[f299]) ).
cnf(s15,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_28 ),
inference(sat_conversion,[],[f303]) ).
cnf(s16,plain,
( spl0_2
| ~ spl0_3
| spl0_29
| spl0_30 ),
inference(sat_conversion,[],[f310]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_6
| spl0_14
| spl0_33 ),
inference(sat_conversion,[],[f321]) ).
cnf(s19,plain,
( ~ spl0_3
| spl0_9
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f328]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_6
| spl0_30
| spl0_33 ),
inference(sat_conversion,[],[f336]) ).
cnf(s22,plain,
( ~ spl0_3
| spl0_11
| spl0_30
| spl0_38 ),
inference(sat_conversion,[],[f340]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_5
| spl0_32
| spl0_39 ),
inference(sat_conversion,[],[f344]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_35
| spl0_40
| spl0_41 ),
inference(sat_conversion,[],[f351]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_10
| spl0_16
| spl0_42 ),
inference(sat_conversion,[],[f355]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_15
| spl0_21
| spl0_44 ),
inference(sat_conversion,[],[f363]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_13
| spl0_16
| spl0_23 ),
inference(sat_conversion,[],[f369]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_17
| spl0_30
| spl0_46 ),
inference(sat_conversion,[],[f373]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_5
| spl0_30
| spl0_38 ),
inference(sat_conversion,[],[f374]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_10
| spl0_41
| spl0_47 ),
inference(sat_conversion,[],[f378]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_5
| spl0_8
| spl0_49 ),
inference(sat_conversion,[],[f386]) ).
cnf(s36,plain,
( ~ spl0_3
| spl0_29
| spl0_41
| spl0_50 ),
inference(sat_conversion,[],[f390]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_9
| spl0_20
| spl0_46 ),
inference(sat_conversion,[],[f392]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_41
| spl0_52
| spl0_53 ),
inference(sat_conversion,[],[f403]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_41
| spl0_53
| spl0_54 ),
inference(sat_conversion,[],[f407]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_10
| spl0_53
| spl0_55 ),
inference(sat_conversion,[],[f411]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_13
| spl0_20
| spl0_52 ),
inference(sat_conversion,[],[f412]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_7
| spl0_56
| spl0_57 ),
inference(sat_conversion,[],[f419]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_4
| spl0_26
| spl0_58 ),
inference(sat_conversion,[],[f423]) ).
cnf(s47,plain,
( ~ spl0_3
| spl0_15
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f428]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_6
| spl0_29
| spl0_39 ),
inference(sat_conversion,[],[f429]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_38
| spl0_43
| spl0_59 ),
inference(sat_conversion,[],[f430]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_11
| spl0_47
| spl0_55 ),
inference(sat_conversion,[],[f435]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_9
| spl0_23
| spl0_59 ),
inference(sat_conversion,[],[f441]) ).
cnf(s58,plain,
( ~ spl0_3
| spl0_30
| spl0_31
| spl0_54 ),
inference(sat_conversion,[],[f448]) ).
cnf(s60,plain,
( ~ spl0_3
| spl0_17
| spl0_28
| spl0_58 ),
inference(sat_conversion,[],[f453]) ).
cnf(s63,plain,
( ~ spl0_3
| spl0_10
| spl0_52
| spl0_56 ),
inference(sat_conversion,[],[f456]) ).
cnf(s64,plain,
( ~ spl0_3
| spl0_10
| spl0_33
| spl0_61 ),
inference(sat_conversion,[],[f457]) ).
cnf(s65,plain,
( ~ spl0_3
| spl0_21
| spl0_31
| spl0_42 ),
inference(sat_conversion,[],[f458]) ).
cnf(s66,plain,
( ~ spl0_3
| spl0_23
| spl0_27
| spl0_50 ),
inference(sat_conversion,[],[f459]) ).
cnf(s72,plain,
( ~ spl0_52
| ~ spl0_67 ),
inference(sat_conversion,[],[f479]) ).
cnf(s73,plain,
( ~ spl0_52
| ~ spl0_68 ),
inference(sat_conversion,[],[f483]) ).
cnf(s74,plain,
( ~ spl0_46
| ~ spl0_69 ),
inference(sat_conversion,[],[f488]) ).
cnf(s75,plain,
( ~ spl0_46
| ~ spl0_70 ),
inference(sat_conversion,[],[f492]) ).
cnf(s76,plain,
( ~ spl0_23
| ~ spl0_71 ),
inference(sat_conversion,[],[f497]) ).
cnf(s77,plain,
( ~ spl0_23
| ~ spl0_72 ),
inference(sat_conversion,[],[f501]) ).
cnf(s78,plain,
( ~ spl0_23
| ~ spl0_73 ),
inference(sat_conversion,[],[f505]) ).
cnf(s79,plain,
( ~ spl0_31
| ~ spl0_74 ),
inference(sat_conversion,[],[f510]) ).
cnf(s81,plain,
( ~ spl0_26
| ~ spl0_76 ),
inference(sat_conversion,[],[f520]) ).
cnf(s82,plain,
( ~ spl0_47
| ~ spl0_77 ),
inference(sat_conversion,[],[f525]) ).
cnf(s83,plain,
( ~ spl0_55
| ~ spl0_78 ),
inference(sat_conversion,[],[f530]) ).
cnf(s84,plain,
( ~ spl0_54
| ~ spl0_79 ),
inference(sat_conversion,[],[f535]) ).
cnf(s85,plain,
( ~ spl0_29
| ~ spl0_80 ),
inference(sat_conversion,[],[f540]) ).
cnf(s86,plain,
( ~ spl0_29
| ~ spl0_81 ),
inference(sat_conversion,[],[f544]) ).
cnf(s87,plain,
( ~ spl0_49
| ~ spl0_82 ),
inference(sat_conversion,[],[f549]) ).
cnf(s88,plain,
( ~ spl0_44
| ~ spl0_83 ),
inference(sat_conversion,[],[f554]) ).
cnf(s89,plain,
( ~ spl0_44
| ~ spl0_84 ),
inference(sat_conversion,[],[f558]) ).
cnf(s90,plain,
( ~ spl0_44
| ~ spl0_85 ),
inference(sat_conversion,[],[f562]) ).
cnf(s91,plain,
( ~ spl0_42
| ~ spl0_86 ),
inference(sat_conversion,[],[f567]) ).
cnf(s92,plain,
( ~ spl0_42
| ~ spl0_87 ),
inference(sat_conversion,[],[f571]) ).
cnf(s93,plain,
( ~ spl0_28
| ~ spl0_88 ),
inference(sat_conversion,[],[f576]) ).
cnf(s94,plain,
( ~ spl0_28
| ~ spl0_89 ),
inference(sat_conversion,[],[f580]) ).
cnf(s95,plain,
( ~ spl0_28
| ~ spl0_90 ),
inference(sat_conversion,[],[f584]) ).
cnf(s98,plain,
( ~ spl0_34
| ~ spl0_93 ),
inference(sat_conversion,[],[f598]) ).
cnf(s99,plain,
( ~ spl0_34
| ~ spl0_94 ),
inference(sat_conversion,[],[f602]) ).
cnf(s100,plain,
( ~ spl0_40
| ~ spl0_95 ),
inference(sat_conversion,[],[f607]) ).
cnf(s101,plain,
( ~ spl0_40
| ~ spl0_96 ),
inference(sat_conversion,[],[f611]) ).
cnf(s103,plain,
( ~ spl0_63
| ~ spl0_98 ),
inference(sat_conversion,[],[f621]) ).
cnf(s104,plain,
( ~ spl0_58
| ~ spl0_99 ),
inference(sat_conversion,[],[f626]) ).
cnf(s105,plain,
( ~ spl0_58
| ~ spl0_100 ),
inference(sat_conversion,[],[f630]) ).
cnf(s106,plain,
( ~ spl0_33
| ~ spl0_101 ),
inference(sat_conversion,[],[f635]) ).
cnf(s107,plain,
( ~ spl0_61
| ~ spl0_102 ),
inference(sat_conversion,[],[f640]) ).
cnf(s108,plain,
( ~ spl0_61
| ~ spl0_103 ),
inference(sat_conversion,[],[f644]) ).
cnf(s109,plain,
( ~ spl0_56
| ~ spl0_104 ),
inference(sat_conversion,[],[f649]) ).
cnf(s110,plain,
( ~ spl0_56
| ~ spl0_105 ),
inference(sat_conversion,[],[f653]) ).
cnf(s111,plain,
( ~ spl0_38
| ~ spl0_106 ),
inference(sat_conversion,[],[f658]) ).
cnf(s112,plain,
( ~ spl0_59
| ~ spl0_107 ),
inference(sat_conversion,[],[f663]) ).
cnf(s113,plain,
( ~ spl0_59
| ~ spl0_108 ),
inference(sat_conversion,[],[f667]) ).
cnf(s114,plain,
( ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f674]) ).
cnf(s115,plain,
( ~ spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f681]) ).
cnf(s116,plain,
( ~ spl0_111
| ~ spl0_113 ),
inference(sat_conversion,[],[f685]) ).
cnf(s117,plain,
( ~ spl0_52
| spl0_114 ),
inference(sat_conversion,[],[f689]) ).
cnf(s118,plain,
( ~ spl0_46
| spl0_115 ),
inference(sat_conversion,[],[f693]) ).
cnf(s119,plain,
( ~ spl0_31
| spl0_116 ),
inference(sat_conversion,[],[f697]) ).
cnf(s120,plain,
( ~ spl0_31
| spl0_117 ),
inference(sat_conversion,[],[f701]) ).
cnf(s123,plain,
( ~ spl0_26
| spl0_120 ),
inference(sat_conversion,[],[f713]) ).
cnf(s124,plain,
( ~ spl0_26
| spl0_121 ),
inference(sat_conversion,[],[f717]) ).
cnf(s125,plain,
( ~ spl0_47
| spl0_122 ),
inference(sat_conversion,[],[f721]) ).
cnf(s126,plain,
( ~ spl0_47
| spl0_123 ),
inference(sat_conversion,[],[f725]) ).
cnf(s127,plain,
( ~ spl0_55
| spl0_124 ),
inference(sat_conversion,[],[f729]) ).
cnf(s128,plain,
( ~ spl0_55
| spl0_125 ),
inference(sat_conversion,[],[f733]) ).
cnf(s129,plain,
( ~ spl0_54
| spl0_126 ),
inference(sat_conversion,[],[f737]) ).
cnf(s130,plain,
( ~ spl0_54
| spl0_127 ),
inference(sat_conversion,[],[f741]) ).
cnf(s131,plain,
( ~ spl0_29
| spl0_128 ),
inference(sat_conversion,[],[f745]) ).
cnf(s132,plain,
( ~ spl0_49
| spl0_129 ),
inference(sat_conversion,[],[f749]) ).
cnf(s133,plain,
( ~ spl0_49
| spl0_130 ),
inference(sat_conversion,[],[f753]) ).
cnf(s134,plain,
( ~ spl0_42
| spl0_131 ),
inference(sat_conversion,[],[f757]) ).
cnf(s136,plain,
( ~ spl0_34
| spl0_133 ),
inference(sat_conversion,[],[f765]) ).
cnf(s137,plain,
( ~ spl0_40
| spl0_134 ),
inference(sat_conversion,[],[f769]) ).
cnf(s140,plain,
( ~ spl0_63
| spl0_137 ),
inference(sat_conversion,[],[f781]) ).
cnf(s141,plain,
( ~ spl0_63
| spl0_138 ),
inference(sat_conversion,[],[f785]) ).
cnf(s142,plain,
( ~ spl0_58
| spl0_139 ),
inference(sat_conversion,[],[f789]) ).
cnf(s143,plain,
( ~ spl0_33
| spl0_140 ),
inference(sat_conversion,[],[f793]) ).
cnf(s144,plain,
( ~ spl0_33
| spl0_141 ),
inference(sat_conversion,[],[f797]) ).
cnf(s145,plain,
( ~ spl0_61
| spl0_142 ),
inference(sat_conversion,[],[f801]) ).
cnf(s146,plain,
( ~ spl0_56
| spl0_143 ),
inference(sat_conversion,[],[f805]) ).
cnf(s147,plain,
( ~ spl0_38
| spl0_144 ),
inference(sat_conversion,[],[f809]) ).
cnf(s148,plain,
( ~ spl0_38
| spl0_145 ),
inference(sat_conversion,[],[f813]) ).
cnf(s149,plain,
( ~ spl0_59
| spl0_146 ),
inference(sat_conversion,[],[f817]) ).
cnf(s150,plain,
( ~ spl0_109
| spl0_147 ),
inference(sat_conversion,[],[f821]) ).
cnf(s151,plain,
( ~ spl0_109
| spl0_148 ),
inference(sat_conversion,[],[f825]) ).
cnf(s152,plain,
( ~ spl0_111
| spl0_149 ),
inference(sat_conversion,[],[f829]) ).
cnf(s153,plain,
( ~ spl0_27
| spl0_150 ),
inference(sat_conversion,[],[f834]) ).
cnf(s154,plain,
( ~ spl0_27
| spl0_151 ),
inference(sat_conversion,[],[f838]) ).
cnf(s155,plain,
( ~ spl0_27
| spl0_152 ),
inference(sat_conversion,[],[f842]) ).
cnf(s156,plain,
( ~ spl0_39
| spl0_153 ),
inference(sat_conversion,[],[f847]) ).
cnf(s157,plain,
( ~ spl0_39
| spl0_154 ),
inference(sat_conversion,[],[f851]) ).
cnf(s158,plain,
( ~ spl0_39
| spl0_155 ),
inference(sat_conversion,[],[f855]) ).
cnf(s159,plain,
( ~ spl0_60
| spl0_156 ),
inference(sat_conversion,[],[f860]) ).
cnf(s160,plain,
( ~ spl0_60
| spl0_157 ),
inference(sat_conversion,[],[f864]) ).
cnf(s161,plain,
( ~ spl0_60
| spl0_158 ),
inference(sat_conversion,[],[f868]) ).
cnf(s162,plain,
( ~ spl0_57
| spl0_159 ),
inference(sat_conversion,[],[f873]) ).
cnf(s163,plain,
( ~ spl0_57
| spl0_160 ),
inference(sat_conversion,[],[f877]) ).
cnf(s164,plain,
( ~ spl0_57
| spl0_161 ),
inference(sat_conversion,[],[f881]) ).
cnf(s167,plain,
( spl0_26
| spl0_34
| spl0_63 ),
inference(sat_conversion,[],[f885]) ).
cnf(s168,plain,
( spl0_33
| spl0_46
| spl0_58 ),
inference(sat_conversion,[],[f886]) ).
cnf(s170,plain,
( spl0_33
| spl0_60
| spl0_109 ),
inference(sat_conversion,[],[f889]) ).
cnf(s192,plain,
( spl0_3
| ~ spl0_33 ),
inference(sat_conversion,[],[f912]) ).
cnf(s197,plain,
( spl0_3
| ~ spl0_109 ),
inference(sat_conversion,[],[f917]) ).
cnf(s201,plain,
( spl0_3
| ~ spl0_60 ),
inference(sat_conversion,[],[f921]) ).
cnf(s203,plain,
( spl0_56
| spl0_111 ),
inference(sat_conversion,[],[f923]) ).
cnf(s207,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_11
| spl0_81
| ~ spl0_128 ),
inference(sat_conversion,[],[f961]) ).
cnf(s208,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_80
| ~ spl0_128 ),
inference(sat_conversion,[],[f966]) ).
cnf(s211,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_81
| ~ spl0_128 ),
inference(sat_conversion,[],[f981]) ).
cnf(s228,plain,
( ~ spl0_9
| ~ spl0_10
| spl0_108
| ~ spl0_146 ),
inference(sat_conversion,[],[f1078]) ).
cnf(s230,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_74
| ~ spl0_116 ),
inference(sat_conversion,[],[f1085]) ).
cnf(s241,plain,
( ~ spl0_5
| ~ spl0_11
| spl0_98
| ~ spl0_137 ),
inference(sat_conversion,[],[f1155]) ).
cnf(s243,plain,
( ~ spl0_9
| ~ spl0_13
| ~ spl0_32
| spl0_82
| ~ spl0_129 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s245,plain,
( ~ spl0_9
| ~ spl0_10
| spl0_98
| ~ spl0_138 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s246,plain,
( ~ spl0_4
| ~ spl0_14
| ~ spl0_15
| ~ spl0_30
| spl0_98
| ~ spl0_138 ),
inference(sat_conversion,[],[f1180]) ).
cnf(s247,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_103
| ~ spl0_142 ),
inference(sat_conversion,[],[f1195]) ).
cnf(s248,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_121 ),
inference(sat_conversion,[],[f1206]) ).
cnf(s249,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_133 ),
inference(sat_conversion,[],[f1207]) ).
cnf(s250,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_15
| ~ spl0_30
| ~ spl0_138 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s272,plain,
( ~ spl0_5
| ~ spl0_9
| spl0_14 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s273,plain,
( ~ spl0_2
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161 ),
inference(sat_conversion,[],[f1251]) ).
cnf(s318,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f1405]) ).
cnf(s326,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_11
| ~ spl0_147
| ~ spl0_148 ),
inference(sat_conversion,[],[f1443]) ).
cnf(s327,plain,
( ~ spl0_32
| ~ spl0_41
| spl0_69
| ~ spl0_115 ),
inference(sat_conversion,[],[f1458]) ).
cnf(s342,plain,
( ~ spl0_50
| spl0_86
| spl0_87
| ~ spl0_131 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s348,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s351,plain,
( ~ spl0_53
| spl0_112
| spl0_113
| spl0_168 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s367,plain,
( ~ spl0_2
| ~ spl0_35
| ~ spl0_126
| ~ spl0_127 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s388,plain,
( ~ spl0_9
| ~ spl0_10
| spl0_106
| ~ spl0_145 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s400,plain,
( ~ spl0_5
| spl0_95
| spl0_96
| ~ spl0_134 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s417,plain,
( ~ spl0_21
| spl0_69
| spl0_70
| ~ spl0_115 ),
inference(sat_conversion,[],[f1894]) ).
cnf(s426,plain,
( ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_76
| ~ spl0_121 ),
inference(sat_conversion,[],[f1933]) ).
cnf(s439,plain,
( ~ spl0_15
| ~ spl0_30
| spl0_76
| ~ spl0_121 ),
inference(sat_conversion,[],[f2036]) ).
cnf(s440,plain,
( ~ spl0_15
| ~ spl0_30
| spl0_93
| ~ spl0_133 ),
inference(sat_conversion,[],[f2038]) ).
cnf(s452,plain,
( ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_101
| ~ spl0_141 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s453,plain,
( ~ spl0_5
| ~ spl0_25
| ~ spl0_30
| spl0_110
| ~ spl0_148 ),
inference(sat_conversion,[],[f2099]) ).
cnf(s479,plain,
( ~ spl0_30
| spl0_93
| spl0_94
| ~ spl0_133 ),
inference(sat_conversion,[],[f2160]) ).
cnf(s500,plain,
( ~ spl0_9
| spl0_17
| ~ spl0_30 ),
inference(sat_conversion,[],[f2209]) ).
cnf(s505,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_12
| ~ spl0_156
| ~ spl0_175 ),
inference(sat_conversion,[],[f2226]) ).
cnf(s529,plain,
( ~ spl0_9
| ~ spl0_13
| spl0_99
| ~ spl0_139 ),
inference(sat_conversion,[],[f2372]) ).
cnf(s537,plain,
( ~ spl0_4
| ~ spl0_156
| ~ spl0_158
| ~ spl0_175 ),
inference(sat_conversion,[],[f2383]) ).
cnf(s542,plain,
( ~ spl0_5
| spl0_107
| spl0_108
| ~ spl0_164 ),
inference(sat_conversion,[],[f2396]) ).
cnf(s585,plain,
( ~ spl0_41
| spl0_112
| spl0_113
| ~ spl0_149 ),
inference(sat_conversion,[],[f2501]) ).
cnf(s591,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_79
| ~ spl0_126 ),
inference(sat_conversion,[],[f2514]) ).
cnf(s592,plain,
( ~ spl0_1
| ~ spl0_8
| ~ spl0_41
| spl0_86
| spl0_87
| ~ spl0_131 ),
inference(sat_conversion,[],[f2516]) ).
cnf(s600,plain,
( ~ spl0_21
| spl0_112
| ~ spl0_149
| spl0_168 ),
inference(sat_conversion,[],[f2532]) ).
cnf(s605,plain,
( ~ spl0_7
| ~ spl0_156
| ~ spl0_157
| ~ spl0_175 ),
inference(sat_conversion,[],[f2538]) ).
cnf(s616,plain,
( ~ spl0_21
| ~ spl0_35
| spl0_70
| ~ spl0_115 ),
inference(sat_conversion,[],[f2567]) ).
cnf(s632,plain,
( ~ spl0_2
| ~ spl0_35
| ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s655,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f2624]) ).
cnf(s685,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_156
| ~ spl0_157 ),
inference(sat_conversion,[],[f2743]) ).
cnf(s687,plain,
( ~ spl0_20
| ~ spl0_41
| spl0_71
| spl0_72
| spl0_73 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s689,plain,
( ~ spl0_20
| spl0_88
| spl0_89
| spl0_90 ),
inference(sat_conversion,[],[f2786]) ).
cnf(s690,plain,
( ~ spl0_16
| ~ spl0_20
| spl0_67
| spl0_68
| ~ spl0_114 ),
inference(sat_conversion,[],[f2788]) ).
cnf(s701,plain,
( ~ spl0_13
| spl0_99
| spl0_100
| ~ spl0_139 ),
inference(sat_conversion,[],[f2815]) ).
cnf(s704,plain,
( ~ spl0_10
| ~ spl0_53
| spl0_83
| spl0_84
| spl0_85 ),
inference(sat_conversion,[],[f2818]) ).
cnf(s718,plain,
( ~ spl0_41
| spl0_101
| ~ spl0_140
| spl0_170 ),
inference(sat_conversion,[],[f2839]) ).
cnf(s750,plain,
( ~ spl0_12
| spl0_101
| ~ spl0_141
| ~ spl0_170 ),
inference(sat_conversion,[],[f2914]) ).
cnf(s752,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f2926]) ).
cnf(s753,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_155
| ~ spl0_162 ),
inference(sat_conversion,[],[f2927]) ).
cnf(s761,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_157
| ~ spl0_158 ),
inference(sat_conversion,[],[f2943]) ).
cnf(s775,plain,
( ~ spl0_15
| spl0_78
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f2971]) ).
cnf(s784,plain,
( ~ spl0_2
| ~ spl0_147
| ~ spl0_148
| ~ spl0_166 ),
inference(sat_conversion,[],[f2982]) ).
cnf(s806,plain,
( ~ spl0_12
| spl0_110
| ~ spl0_147
| ~ spl0_148 ),
inference(sat_conversion,[],[f3031]) ).
cnf(s819,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_147
| ~ spl0_148 ),
inference(sat_conversion,[],[f3057]) ).
cnf(s820,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_14
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f3073]) ).
cnf(s825,plain,
( ~ spl0_9
| ~ spl0_12
| ~ spl0_30
| spl0_98
| ~ spl0_138 ),
inference(sat_conversion,[],[f3093]) ).
cnf(s833,plain,
( ~ spl0_15
| ~ spl0_30
| spl0_104
| ~ spl0_143 ),
inference(sat_conversion,[],[f3105]) ).
cnf(s850,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_154
| ~ spl0_155 ),
inference(sat_conversion,[],[f3120]) ).
cnf(s859,plain,
( ~ spl0_9
| ~ spl0_22
| ~ spl0_30
| spl0_78
| ~ spl0_125 ),
inference(sat_conversion,[],[f3127]) ).
cnf(s871,plain,
( ~ spl0_53
| spl0_71
| spl0_72
| spl0_73 ),
inference(sat_conversion,[],[f3144]) ).
cnf(s899,plain,
( ~ spl0_1
| ~ spl0_20
| spl0_99
| spl0_100
| ~ spl0_139 ),
inference(sat_conversion,[],[f3165]) ).
cnf(s911,plain,
( ~ spl0_9
| ~ spl0_20
| spl0_102
| spl0_103
| ~ spl0_142 ),
inference(sat_conversion,[],[f3175]) ).
cnf(s918,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_144
| ~ spl0_173 ),
inference(sat_conversion,[],[f3191]) ).
cnf(s924,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_141
| ~ spl0_170 ),
inference(sat_conversion,[],[f3214]) ).
cnf(s941,plain,
( ~ spl0_32
| ~ spl0_156
| ~ spl0_157
| spl0_175 ),
inference(sat_conversion,[],[f3229]) ).
cnf(s962,plain,
( ~ spl0_13
| spl0_103
| ~ spl0_142
| spl0_182 ),
inference(sat_conversion,[],[f3250]) ).
cnf(s964,plain,
( ~ spl0_13
| ~ spl0_32
| spl0_67
| spl0_68
| ~ spl0_114 ),
inference(sat_conversion,[],[f3252]) ).
cnf(s968,plain,
( ~ spl0_15
| spl0_102
| ~ spl0_142
| ~ spl0_182 ),
inference(sat_conversion,[],[f3257]) ).
cnf(s998,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f3282]) ).
cnf(s1048,plain,
( ~ spl0_32
| spl0_67
| ~ spl0_114
| ~ spl0_183 ),
inference(sat_conversion,[],[f3359]) ).
cnf(s1071,plain,
( ~ spl0_17
| spl0_104
| spl0_105
| ~ spl0_143 ),
inference(sat_conversion,[],[f3455]) ).
cnf(s1100,plain,
( ~ spl0_16
| ~ spl0_22
| ~ spl0_50
| spl0_70
| ~ spl0_115 ),
inference(sat_conversion,[],[f3490]) ).
cnf(s1105,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_77
| ~ spl0_122 ),
inference(sat_conversion,[],[f3511]) ).
cnf(s1111,plain,
( ~ spl0_2
| ~ spl0_140
| ~ spl0_141
| ~ spl0_170 ),
inference(sat_conversion,[],[f3518]) ).
cnf(s1115,plain,
( ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f3539]) ).
cnf(s1117,plain,
( ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_144
| ~ spl0_173 ),
inference(sat_conversion,[],[f3541]) ).
cnf(s1118,plain,
( ~ spl0_11
| ~ spl0_16
| ~ spl0_22
| ~ spl0_150
| ~ spl0_151 ),
inference(sat_conversion,[],[f3543]) ).
cnf(s1122,plain,
( ~ spl0_10
| spl0_107
| spl0_108
| ~ spl0_146 ),
inference(sat_conversion,[],[f3551]) ).
cnf(s1141,plain,
( ~ spl0_10
| ~ spl0_15
| spl0_17 ),
inference(sat_conversion,[],[f3603]) ).
cnf(s1157,plain,
( ~ spl0_15
| ~ spl0_18
| spl0_67
| ~ spl0_114 ),
inference(sat_conversion,[],[f3650]) ).
cnf(s1159,plain,
( ~ spl0_15
| ~ spl0_18
| spl0_102
| ~ spl0_142 ),
inference(sat_conversion,[],[f3654]) ).
cnf(s1161,plain,
( ~ spl0_16
| ~ spl0_19
| ~ spl0_22
| spl0_67
| ~ spl0_114 ),
inference(sat_conversion,[],[f3667]) ).
cnf(s1181,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f3688]) ).
cnf(s1182,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_160
| ~ spl0_161 ),
inference(sat_conversion,[],[f3690]) ).
cnf(s1184,plain,
( ~ spl0_4
| ~ spl0_15
| ~ spl0_43
| ~ spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f3692]) ).
cnf(s1206,plain,
( ~ spl0_30
| spl0_112
| spl0_113
| ~ spl0_168 ),
inference(sat_conversion,[],[f3717]) ).
cnf(s1211,plain,
( ~ spl0_15
| ~ spl0_144
| ~ spl0_145
| spl0_173 ),
inference(sat_conversion,[],[f3721]) ).
cnf(s1250,plain,
( ~ spl0_7
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(sat_conversion,[],[f3750]) ).
cnf(s1267,plain,
( ~ spl0_16
| ~ spl0_154
| ~ spl0_155
| spl0_162 ),
inference(sat_conversion,[],[f3763]) ).
cnf(s1292,plain,
( ~ spl0_8
| ~ spl0_16
| ~ spl0_22
| spl0_35 ),
inference(sat_conversion,[],[f3769]) ).
cnf(s1315,plain,
( ~ spl0_10
| spl0_110
| ~ spl0_148
| spl0_166 ),
inference(sat_conversion,[],[f3782]) ).
cnf(s1326,plain,
( ~ spl0_6
| spl0_76
| ~ spl0_120
| ~ spl0_121 ),
inference(sat_conversion,[],[f3846]) ).
cnf(s1329,plain,
( ~ spl0_6
| ~ spl0_157
| ~ spl0_158
| spl0_175 ),
inference(sat_conversion,[],[f3849]) ).
cnf(s1344,plain,
( ~ spl0_4
| ~ spl0_150
| ~ spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s1395,plain,
( ~ spl0_17
| spl0_78
| ~ spl0_125
| spl0_169 ),
inference(sat_conversion,[],[f3890]) ).
cnf(s1403,plain,
( ~ spl0_6
| spl0_112
| ~ spl0_149
| ~ spl0_168 ),
inference(sat_conversion,[],[f3894]) ).
cnf(s1404,plain,
( ~ spl0_6
| spl0_78
| ~ spl0_125
| ~ spl0_169 ),
inference(sat_conversion,[],[f3895]) ).
cnf(s1424,plain,
( ~ spl0_4
| ~ spl0_5
| spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f3909]) ).
cnf(s1444,plain,
( ~ spl0_9
| spl0_106
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f3917]) ).
cnf(s1445,plain,
( ~ spl0_9
| ~ spl0_124
| ~ spl0_125
| spl0_169 ),
inference(sat_conversion,[],[f3918]) ).
cnf(s1453,plain,
( ~ spl0_20
| spl0_102
| spl0_103
| spl0_182 ),
inference(sat_conversion,[],[f3922]) ).
cnf(s1456,plain,
( ~ spl0_20
| spl0_67
| spl0_68
| spl0_183 ),
inference(sat_conversion,[],[f3928]) ).
cnf(s1465,plain,
( ~ spl0_30
| spl0_101
| ~ spl0_141
| spl0_170 ),
inference(sat_conversion,[],[f3931]) ).
cnf(s1473,plain,
( ~ spl0_30
| spl0_107
| ~ spl0_146
| spl0_164 ),
inference(sat_conversion,[],[f3932]) ).
cnf(s1476,plain,
( ~ spl0_17
| spl0_102
| spl0_103
| ~ spl0_182 ),
inference(sat_conversion,[],[f3935]) ).
cnf(s1483,plain,
spl0_3,
inference(rat,[],[s170,s192,s197,s201]) ).
cnf(s1484,plain,
( ~ spl0_38
| ~ spl0_15
| ~ spl0_4 ),
inference(rat,[],[s1181,s147,s148]) ).
cnf(s1485,plain,
( ~ spl0_30
| ~ spl0_15
| ~ spl0_4
| ~ spl0_12 ),
inference(rat,[],[s167,s124,s136,s141,s248,s249,s250]) ).
cnf(s1486,plain,
( ~ spl0_15
| ~ spl0_12
| spl0_5
| ~ spl0_4 ),
inference(rat,[],[s1485,s32,s1484,s1483]) ).
cnf(s1487,plain,
( ~ spl0_39
| ~ spl0_7 ),
inference(rat,[],[s1250,s156,s157,s158]) ).
cnf(s1488,plain,
( ~ spl0_55
| ~ spl0_15
| ~ spl0_4 ),
inference(rat,[],[s348,s127,s128]) ).
cnf(s1489,plain,
( ~ spl0_27
| ~ spl0_15
| ~ spl0_4 ),
inference(rat,[],[s318,s154,s155]) ).
cnf(s1490,plain,
( ~ spl0_23
| ~ spl0_53 ),
inference(rat,[],[s871,s76,s77,s78]) ).
cnf(s1491,plain,
( ~ spl0_34
| ~ spl0_30
| ~ spl0_15 ),
inference(rat,[],[s440,s98,s136]) ).
cnf(s1492,plain,
( ~ spl0_26
| ~ spl0_30
| ~ spl0_15 ),
inference(rat,[],[s439,s81,s124]) ).
cnf(s1493,plain,
( spl0_8
| ~ spl0_32
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s30,s1490,s998,s42,s14,s245,s246,s103,s141,s167,s1492,s1491,s1489,s1488,s32,s1484,s6,s243,s87,s132,s133,s3,s35,s1,s1483]) ).
cnf(s1494,plain,
( spl0_13
| spl0_11
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s1161,s7,s14,s9,s245,s246,s103,s141,s167,s1492,s1491,s4,s32,s1157,s1489,s1486,s1484,s72,s117,s6,s43,s1,s689,s93,s94,s95,s15,s1483]) ).
cnf(s1495,plain,
( ~ spl0_15
| spl0_11
| spl0_6
| spl0_5
| ~ spl0_4 ),
inference(rat,[],[s1122,s112,s113,s149,s49,s1184,s143,s144,s18,s246,s103,s141,s167,s1492,s1491,s4,s32,s1486,s1484,s1483]) ).
cnf(s1496,plain,
( ~ spl0_63
| ~ spl0_12
| ~ spl0_9
| ~ spl0_30 ),
inference(rat,[],[s825,s103,s141]) ).
cnf(s1497,plain,
( ~ spl0_34
| ~ spl0_30 ),
inference(rat,[],[s479,s98,s99,s136]) ).
cnf(s1498,plain,
( ~ spl0_63
| ~ spl0_9
| ~ spl0_30
| spl0_11 ),
inference(rat,[],[s4,s245,s1496,s103,s141,s1483]) ).
cnf(s1499,plain,
( ~ spl0_33
| ~ spl0_12
| ~ spl0_30 ),
inference(rat,[],[s750,s1465,s106,s144]) ).
cnf(s1500,plain,
( ~ spl0_61
| ~ spl0_9
| ~ spl0_13 ),
inference(rat,[],[s247,s108,s145]) ).
cnf(s1501,plain,
( spl0_10
| spl0_61
| ~ spl0_30
| spl0_11 ),
inference(rat,[],[s1499,s64,s4,s1483]) ).
cnf(s1502,plain,
( ~ spl0_27
| ~ spl0_4 ),
inference(rat,[],[s1344,s153,s154,s155]) ).
cnf(s1503,plain,
( ~ spl0_59
| ~ spl0_10
| ~ spl0_9 ),
inference(rat,[],[s228,s113,s149]) ).
cnf(s1504,plain,
( ~ spl0_9
| ~ spl0_30
| spl0_15
| ~ spl0_13
| spl0_11 ),
inference(rat,[],[s529,s104,s142,s47,s1503,s1501,s1500,s1483]) ).
cnf(s1505,plain,
( spl0_10
| spl0_41
| spl0_11
| ~ spl0_8 ),
inference(rat,[],[s1105,s82,s125,s33,s4,s1483]) ).
cnf(s1506,plain,
( ~ spl0_52
| ~ spl0_13
| ~ spl0_32 ),
inference(rat,[],[s964,s72,s73,s117]) ).
cnf(s1507,plain,
( ~ spl0_30
| spl0_15
| ~ spl0_13
| spl0_11
| ~ spl0_8
| ~ spl0_32
| spl0_20 ),
inference(rat,[],[s704,s88,s89,s90,s40,s1505,s27,s327,s616,s74,s75,s118,s19,s38,s1504,s1497,s1506,s1483]) ).
cnf(s1508,plain,
( spl0_6
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s704,s88,s89,s90,s40,s1505,s27,s327,s417,s74,s75,s118,s38,s1444,s111,s147,s148,s32,s1507,s1506,s1495,s1494,s207,s1493,s86,s131,s23,s48,s1487,s2,s1,s689,s93,s94,s95,s15,s1483]) ).
cnf(s1509,plain,
( spl0_13
| spl0_10
| ~ spl0_30
| spl0_2
| spl0_1 ),
inference(rat,[],[s1161,s9,s14,s246,s30,s103,s141,s1490,s167,s42,s1157,s1492,s1488,s72,s117,s6,s43,s689,s93,s94,s95,s15,s1502,s1,s1497,s1483]) ).
cnf(s1510,plain,
( ~ spl0_56
| ~ spl0_17 ),
inference(rat,[],[s1071,s109,s110,s146]) ).
cnf(s1511,plain,
( ~ spl0_9
| spl0_10
| ~ spl0_30
| ~ spl0_6
| spl0_20 ),
inference(rat,[],[s859,s83,s128,s42,s10,s351,s600,s1403,s115,s116,s152,s203,s1510,s500,s1483]) ).
cnf(s1512,plain,
( ~ spl0_32
| ~ spl0_22
| spl0_69
| spl0_70
| ~ spl0_115
| ~ spl0_13
| spl0_10
| spl0_5
| spl0_27 ),
inference(rat,[],[s1100,s66,s8,s1490,s1510,s40,s63,s327,s1506,s1483]) ).
cnf(s1513,plain,
( spl0_10
| ~ spl0_30
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s1395,s1404,s83,s128,s42,s1490,s66,s342,s91,s92,s134,s8,s25,s850,s157,s158,s23,s1512,s10,s616,s74,s75,s118,s19,s38,s1511,s1509,s689,s93,s94,s95,s15,s1502,s1,s1508,s1497,s1483]) ).
cnf(s1514,plain,
( ~ spl0_63
| ~ spl0_9
| ~ spl0_10 ),
inference(rat,[],[s245,s103,s141]) ).
cnf(s1515,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_30
| ~ spl0_6
| spl0_20 ),
inference(rat,[],[s426,s81,s124,s167,s1514,s10,s600,s1403,s115,s152,s203,s1510,s500,s1497,s1483]) ).
cnf(s1516,plain,
( spl0_13
| spl0_9
| ~ spl0_30
| spl0_2
| spl0_1 ),
inference(rat,[],[s246,s103,s141,s9,s167,s1161,s1157,s1492,s72,s117,s7,s6,s43,s1,s10,s616,s19,s1497,s75,s118,s38,s689,s93,s94,s95,s15,s1483]) ).
cnf(s1517,plain,
( ~ spl0_59
| ~ spl0_10 ),
inference(rat,[],[s1122,s112,s113,s149]) ).
cnf(s1518,plain,
( ~ spl0_32
| spl0_53
| ~ spl0_13
| spl0_69
| ~ spl0_115 ),
inference(rat,[],[s40,s327,s1506,s1483]) ).
cnf(s1519,plain,
( ~ spl0_15
| ~ spl0_160
| ~ spl0_161
| spl0_59
| ~ spl0_4 ),
inference(rat,[],[s49,s1182,s1484,s1483]) ).
cnf(s1520,plain,
( ~ spl0_30
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s701,s104,s105,s142,s47,s1519,s163,s164,s44,s1510,s8,s850,s1487,s157,s158,s23,s1518,s1490,s54,s1517,s1516,s10,s616,s74,s75,s118,s19,s38,s1515,s1513,s1497,s1,s689,s93,s94,s95,s15,s1508,s1483]) ).
cnf(s1521,plain,
( spl0_10
| ~ spl0_22
| spl0_69
| spl0_70
| ~ spl0_115
| ~ spl0_13
| ~ spl0_6
| spl0_5
| spl0_27 ),
inference(rat,[],[s1395,s1404,s83,s128,s42,s1490,s66,s342,s91,s92,s134,s8,s25,s850,s157,s158,s23,s1512,s1483]) ).
cnf(s1522,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s701,s104,s105,s142,s47,s1517,s1521,s10,s417,s74,s75,s118,s38,s6,s1444,s1484,s111,s147,s148,s32,s1520,s1508,s689,s93,s94,s95,s15,s1502,s1,s1483]) ).
cnf(s1523,plain,
( ~ spl0_9
| spl0_10
| ~ spl0_30
| spl0_20 ),
inference(rat,[],[s859,s83,s128,s42,s10,s351,s600,s1206,s115,s116,s152,s203,s1510,s500,s1483]) ).
cnf(s1524,plain,
( ~ spl0_59
| ~ spl0_30
| ~ spl0_5 ),
inference(rat,[],[s542,s1473,s112,s113,s149]) ).
cnf(s1525,plain,
( spl0_10
| ~ spl0_30
| spl0_2
| spl0_1 ),
inference(rat,[],[s701,s104,s105,s142,s47,s1488,s42,s1490,s54,s1523,s1509,s1,s689,s93,s94,s95,s15,s1524,s1522,s1483]) ).
cnf(s1526,plain,
( ~ spl0_9
| ~ spl0_10
| ~ spl0_30
| spl0_20 ),
inference(rat,[],[s10,s600,s1206,s426,s115,s116,s152,s81,s124,s203,s167,s1510,s1514,s500,s1497,s1483]) ).
cnf(s1527,plain,
( ~ spl0_15
| ~ spl0_30
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s246,s103,s141,s167,s1492,s1424,s1497]) ).
cnf(s1528,plain,
( ~ spl0_30
| spl0_2
| spl0_1 ),
inference(rat,[],[s701,s104,s105,s142,s47,s1527,s1516,s1526,s1525,s1524,s1,s689,s93,s94,s95,s15,s1522,s1483]) ).
cnf(s1529,plain,
( ~ spl0_33
| ~ spl0_41
| ~ spl0_12 ),
inference(rat,[],[s718,s750,s106,s143,s144]) ).
cnf(s1530,plain,
( ~ spl0_111
| ~ spl0_41 ),
inference(rat,[],[s585,s115,s116,s152]) ).
cnf(s1531,plain,
( ~ spl0_58
| ~ spl0_13 ),
inference(rat,[],[s701,s104,s105,s142]) ).
cnf(s1532,plain,
( ~ spl0_47
| ~ spl0_12
| ~ spl0_8 ),
inference(rat,[],[s1105,s82,s125]) ).
cnf(s1534,plain,
( ~ spl0_109
| ~ spl0_12 ),
inference(rat,[],[s806,s114,s150,s151]) ).
cnf(s1535,plain,
( spl0_10
| ~ spl0_8
| spl0_11
| spl0_30
| ~ spl0_4 ),
inference(rat,[],[s537,s1329,s159,s160,s161,s170,s1534,s21,s1529,s1505,s4,s1483]) ).
cnf(s1536,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s1517,s1535,s47,s1531,s3,s6,s1444,s1484,s111,s147,s148,s22,s208,s85,s131,s16,s1528,s1522,s1,s1483]) ).
cnf(s1537,plain,
( ~ spl0_60
| ~ spl0_6
| ~ spl0_2 ),
inference(rat,[],[s761,s160,s161]) ).
cnf(s1538,plain,
( ~ spl0_6
| spl0_109
| ~ spl0_2 ),
inference(rat,[],[s752,s143,s144,s170,s1537]) ).
cnf(s1539,plain,
( ~ spl0_40
| ~ spl0_5 ),
inference(rat,[],[s400,s100,s101,s137]) ).
cnf(s1540,plain,
( spl0_41
| spl0_40
| spl0_10
| ~ spl0_2 ),
inference(rat,[],[s632,s125,s126,s24,s33,s1483]) ).
cnf(s1541,plain,
( ~ spl0_12
| ~ spl0_41
| spl0_30
| ~ spl0_2 ),
inference(rat,[],[s21,s1538,s1529,s1534,s1483]) ).
cnf(s1542,plain,
( ~ spl0_109
| ~ spl0_11
| ~ spl0_5
| ~ spl0_2 ),
inference(rat,[],[s326,s150,s151]) ).
cnf(s1543,plain,
( ~ spl0_5
| spl0_30
| spl0_10
| ~ spl0_2 ),
inference(rat,[],[s1111,s718,s106,s143,s144,s21,s1538,s1542,s4,s1541,s1540,s1539,s1483]) ).
cnf(s1544,plain,
( ~ spl0_13
| ~ spl0_32
| ~ spl0_129
| ~ spl0_130
| spl0_5
| spl0_30
| spl0_10 ),
inference(rat,[],[s10,s689,s417,s93,s94,s95,s74,s75,s118,s998,s60,s31,s8,s1510,s63,s1506,s1531,s1483]) ).
cnf(s1545,plain,
( spl0_11
| spl0_30
| spl0_9
| spl0_10
| spl0_1 ),
inference(rat,[],[s775,s83,s127,s128,s42,s1490,s11,s998,s1484,s7,s6,s1544,s23,s132,s133,s1487,s35,s2,s1505,s1538,s1541,s1534,s4,s32,s1543,s1536,s1483]) ).
cnf(s1546,plain,
( ~ spl0_41
| ~ spl0_6
| spl0_5
| spl0_30
| ~ spl0_2 ),
inference(rat,[],[s1267,s753,s157,s158,s23,s327,s74,s118,s31,s8,s1510,s203,s1530,s1483]) ).
cnf(s1547,plain,
( ~ spl0_57
| ~ spl0_2 ),
inference(rat,[],[s273,s162,s163,s164]) ).
cnf(s1548,plain,
( ~ spl0_5
| spl0_10
| spl0_1 ),
inference(rat,[],[s1531,s47,s6,s833,s109,s146,s203,s1530,s1524,s1540,s1543,s1539,s1536,s1483]) ).
cnf(s1549,plain,
( ~ spl0_41
| spl0_30
| spl0_5
| ~ spl0_2 ),
inference(rat,[],[s1111,s718,s106,s143,s144,s21,s1546,s1483]) ).
cnf(s1550,plain,
( spl0_33
| ~ spl0_13
| ~ spl0_6
| ~ spl0_11
| spl0_5
| spl0_10 ),
inference(rat,[],[s1118,s153,s154,s1521,s10,s689,s93,s94,s95,s60,s8,s1476,s417,s962,s74,s75,s118,s107,s108,s145,s168,s64,s1531,s1483]) ).
cnf(s1551,plain,
( ~ spl0_33
| ~ spl0_6
| ~ spl0_2 ),
inference(rat,[],[s752,s143,s144]) ).
cnf(s1552,plain,
( ~ spl0_6
| spl0_30
| spl0_10
| spl0_1 ),
inference(rat,[],[s417,s74,s75,s118,s10,s38,s1453,s1117,s968,s1211,s7,s6,s107,s108,s145,s1550,s64,s1551,s1536,s1545,s1444,s111,s147,s148,s32,s1548,s1483]) ).
cnf(s1553,plain,
( spl0_30
| spl0_10
| spl0_1 ),
inference(rat,[],[s1544,s132,s133,s35,s207,s6,s86,s131,s1211,s23,s48,s918,s1487,s2,s1552,s1545,s1444,s111,s147,s148,s32,s1548,s1483]) ).
cnf(s1554,plain,
( ~ spl0_6
| spl0_10
| spl0_1 ),
inference(rat,[],[s616,s10,s75,s118,s1161,s38,s7,s19,s72,s117,s1523,s43,s9,s1453,s1159,s968,s6,s1550,s107,s108,s145,s4,s819,s64,s1534,s150,s151,s1551,s1538,s1536,s1548,s1497,s1553,s1483]) ).
cnf(s1555,plain,
( ~ spl0_60
| ~ spl0_32
| ~ spl0_7 ),
inference(rat,[],[s605,s941,s159,s160]) ).
cnf(s1556,plain,
( ~ spl0_12
| spl0_60
| ~ spl0_30 ),
inference(rat,[],[s170,s1534,s1499]) ).
cnf(s1557,plain,
( spl0_33
| spl0_60
| spl0_6
| ~ spl0_2 ),
inference(rat,[],[s819,s150,s151,s170,s18,s1483]) ).
cnf(s1558,plain,
( spl0_10
| spl0_1 ),
inference(rat,[],[s1465,s1111,s106,s143,s144,s1557,s1555,s23,s1487,s2,s1554,s1553,s1548,s1536,s1483]) ).
cnf(s1559,plain,
( ~ spl0_109
| spl0_1 ),
inference(rat,[],[s1315,s784,s114,s150,s151,s1536,s1558]) ).
cnf(s1560,plain,
( ~ spl0_54
| ~ spl0_35
| ~ spl0_2 ),
inference(rat,[],[s367,s129,s130]) ).
cnf(s1561,plain,
( spl0_30
| ~ spl0_5
| spl0_1 ),
inference(rat,[],[s388,s111,s148,s22,s54,s230,s1490,s79,s119,s41,s58,s1560,s24,s718,s1111,s106,s143,s144,s21,s1517,s1558,s1538,s1559,s1536,s1539,s1483]) ).
cnf(s1562,plain,
( spl0_15
| spl0_1 ),
inference(rat,[],[s1531,s47,s6,s1517,s1558,s1483]) ).
cnf(s1563,plain,
( ~ spl0_30
| spl0_1 ),
inference(rat,[],[s41,s1490,s1560,s54,s19,s1514,s167,s1492,s1497,s1536,s1517,s1530,s203,s1510,s1141,s1562,s1558,s1483]) ).
cnf(s1564,plain,
spl0_1,
inference(rat,[],[s998,s132,s133,s35,s1292,s10,s417,s74,s75,s118,s38,s1456,s7,s1048,s1506,s72,s73,s117,s1560,s40,s41,s1490,s54,s1444,s111,s147,s148,s32,s23,s1561,s1563,s1487,s1530,s44,s203,s1510,s1141,s1562,s1517,s1558,s1547,s1536,s1483]) ).
cnf(s1565,plain,
( spl0_30
| spl0_2
| ~ spl0_5 ),
inference(rat,[],[s1444,s111,s147,s148,s22,s3,s208,s211,s85,s86,s131,s16,s1483,s1564]) ).
cnf(s1566,plain,
( ~ spl0_60
| ~ spl0_22
| ~ spl0_16 ),
inference(rat,[],[s685,s159,s160]) ).
cnf(s1568,plain,
( ~ spl0_54
| ~ spl0_8 ),
inference(rat,[],[s591,s84,s129,s1564]) ).
cnf(s1569,plain,
( ~ spl0_63
| ~ spl0_11
| ~ spl0_5 ),
inference(rat,[],[s241,s103,s140]) ).
cnf(s1570,plain,
( ~ spl0_26
| ~ spl0_6 ),
inference(rat,[],[s1326,s81,s123,s124]) ).
cnf(s1571,plain,
( ~ spl0_6
| spl0_2
| spl0_10
| ~ spl0_5 ),
inference(rat,[],[s10,s1566,s616,s7,s75,s118,s1531,s38,s45,s687,s505,s1329,s76,s77,s78,s1505,s159,s160,s161,s19,s54,s3,s1556,s1498,s4,s1569,s167,s1570,s1497,s1524,s1565,s1483,s1564]) ).
cnf(s1572,plain,
( spl0_9
| ~ spl0_60
| spl0_11
| spl0_59
| spl0_34
| spl0_2
| spl0_10 ),
inference(rat,[],[s7,s1566,s1531,s10,s47,s616,s775,s75,s118,s83,s127,s128,s38,s51,s687,s76,s77,s78,s1532,s1505,s19,s54,s3,s4,s1483]) ).
cnf(s1573,plain,
( spl0_11
| spl0_59
| ~ spl0_30
| spl0_2
| spl0_10 ),
inference(rat,[],[s911,s1523,s1572,s107,s108,s145,s1556,s1501,s4,s1497,s1483]) ).
cnf(s1574,plain,
( ~ spl0_29
| ~ spl0_8 ),
inference(rat,[],[s211,s86,s131,s1564]) ).
cnf(s1575,plain,
( spl0_2
| spl0_10
| ~ spl0_5 ),
inference(rat,[],[s850,s157,s158,s48,s1574,s10,s616,s75,s118,s7,s19,s3,s38,s1523,s899,s1531,s104,s105,s142,s47,s1492,s167,s1569,s1573,s1571,s1524,s1497,s1565,s1483,s1564]) ).
cnf(s1576,plain,
( spl0_10
| ~ spl0_5 ),
inference(rat,[],[s718,s924,s106,s143,s144,s170,s1542,s4,s1556,s1566,s10,s616,s75,s118,s38,s7,s5,s899,s1531,s104,s105,s142,s19,s47,s500,s833,s1510,s109,s146,s203,s1530,s1524,s1497,s1540,s1543,s1575,s1539,s1483,s1564]) ).
cnf(s1577,plain,
( ~ spl0_109
| ~ spl0_2
| ~ spl0_10 ),
inference(rat,[],[s1315,s784,s114,s150,s151]) ).
cnf(s1578,plain,
( spl0_30
| ~ spl0_5 ),
inference(rat,[],[s272,s54,s820,s1490,s119,s120,s41,s58,s1560,s24,s718,s1111,s106,s143,s144,s21,s1538,s1577,s1565,s1539,s1517,s1576,s1483,s1564]) ).
cnf(s1579,plain,
( ~ spl0_42
| ~ spl0_41
| ~ spl0_8 ),
inference(rat,[],[s592,s91,s92,s134,s1564]) ).
cnf(s1580,plain,
( ~ spl0_109
| ~ spl0_25
| ~ spl0_5 ),
inference(rat,[],[s453,s114,s151,s1578]) ).
cnf(s1581,plain,
( ~ spl0_25
| spl0_60
| ~ spl0_5 ),
inference(rat,[],[s452,s106,s144,s170,s1580,s1578]) ).
cnf(s1582,plain,
( spl0_9
| spl0_2
| ~ spl0_5 ),
inference(rat,[],[s850,s157,s158,s48,s1570,s13,s1581,s655,s119,s120,s65,s1579,s1566,s7,s1531,s10,s47,s616,s833,s75,s118,s109,s146,s38,s203,s687,s1530,s41,s1490,s76,s77,s78,s1574,s1568,s19,s54,s3,s1517,s1576,s1497,s1578,s1483,s1564]) ).
cnf(s1583,plain,
( ~ spl0_9
| ~ spl0_5 ),
inference(rat,[],[s899,s104,s105,s142,s47,s1492,s167,s1526,s1514,s1517,s1576,s1497,s1578,s1564,s1483]) ).
cnf(s1584,plain,
~ spl0_5,
inference(rat,[],[s718,s924,s106,s143,s144,s170,s1566,s7,s5,s1531,s10,s47,s616,s833,s75,s118,s109,s146,s38,s203,s687,s1530,s41,s1577,s1560,s1490,s76,s77,s78,s1582,s19,s54,s1583,s1497,s1578,s1517,s1576,s1483]) ).
cnf(s1585,plain,
( spl0_2
| spl0_30 ),
inference(rat,[],[s1574,s3,s16,s1444,s111,s147,s148,s32,s1483,s1584]) ).
cnf(s1586,plain,
( ~ spl0_6
| spl0_10
| spl0_30 ),
inference(rat,[],[s417,s74,s75,s118,s38,s10,s1453,s1117,s968,s1211,s7,s5,s1550,s107,s108,s145,s4,s819,s64,s1534,s150,s151,s1551,s1538,s1444,s111,s147,s148,s32,s1585,s1483,s1584]) ).
cnf(s1587,plain,
( spl0_20
| spl0_22
| spl0_9 ),
inference(rat,[],[s417,s74,s75,s118,s10,s38,s1483]) ).
cnf(s1588,plain,
( ~ spl0_28
| ~ spl0_20 ),
inference(rat,[],[s689,s93,s94,s95]) ).
cnf(s1589,plain,
( ~ spl0_58
| ~ spl0_20 ),
inference(rat,[],[s899,s104,s105,s142,s1564]) ).
cnf(s1590,plain,
( spl0_10
| spl0_30 ),
inference(rat,[],[s690,s72,s73,s117,s63,s1510,s60,s1589,s1588,s1587,s998,s7,s1544,s132,s133,s35,s1574,s23,s48,s1487,s2,s1586,s1444,s111,s147,s148,s32,s1483,s1584]) ).
cnf(s1591,plain,
spl0_30,
inference(rat,[],[s1587,s998,s1456,s7,s132,s133,s1048,s964,s35,s23,s72,s73,s117,s1568,s1487,s40,s41,s2,s1490,s1538,s54,s1577,s1517,s1590,s1549,s1585,s1444,s111,s147,s148,s32,s1483,s1584]) ).
cnf(s1592,plain,
~ spl0_34,
inference(rat,[],[s1497,s1591]) ).
cnf(s1593,plain,
( ~ spl0_42
| ~ spl0_8 ),
inference(rat,[],[s36,s342,s1579,s91,s92,s134,s1574,s1483]) ).
cnf(s1594,plain,
( spl0_20
| spl0_10
| spl0_42
| spl0_9 ),
inference(rat,[],[s1115,s119,s120,s4,s65,s1556,s616,s1566,s75,s118,s1587,s38,s19,s25,s1483,s1591,s1592]) ).
cnf(s1595,plain,
( spl0_10
| spl0_42
| spl0_9 ),
inference(rat,[],[s690,s72,s73,s117,s63,s1510,s60,s1589,s1588,s1594,s25,s1483]) ).
cnf(s1596,plain,
( ~ spl0_8
| spl0_9 ),
inference(rat,[],[s850,s157,s158,s23,s327,s8,s74,s118,s1510,s1587,s38,s203,s687,s1530,s41,s1490,s76,s77,s78,s54,s1517,s1595,s1593,s1568,s1483,s1584]) ).
cnf(s1597,plain,
( spl0_16
| spl0_10
| spl0_9 ),
inference(rat,[],[s23,s1487,s1506,s44,s63,s1510,s7,s8,s1547,s3,s1596,s1483,s1584]) ).
cnf(s1598,plain,
( spl0_10
| spl0_9 ),
inference(rat,[],[s690,s72,s73,s117,s63,s1510,s60,s1589,s1588,s1587,s998,s1597,s133,s132,s35,s1596,s1483,s1584]) ).
cnf(s1599,plain,
spl0_9,
inference(rat,[],[s8,s998,s1510,s1587,s203,s687,s1530,s41,s1490,s76,s77,s78,s54,s1517,s1598,s1560,s132,s133,s3,s35,s1596,s19,s1483,s1584,s1592]) ).
cnf(s1600,plain,
spl0_17,
inference(rat,[],[s500,s1591,s1599]) ).
cnf(s1601,plain,
~ spl0_56,
inference(rat,[],[s1510,s1600]) ).
cnf(s1602,plain,
spl0_111,
inference(rat,[],[s203,s1601]) ).
cnf(s1604,plain,
~ spl0_113,
inference(rat,[],[s116,s1602]) ).
cnf(s1605,plain,
~ spl0_112,
inference(rat,[],[s115,s1602]) ).
cnf(s1606,plain,
~ spl0_41,
inference(rat,[],[s1530,s1602]) ).
cnf(s1607,plain,
~ spl0_168,
inference(rat,[],[s1206,s1591,s1604,s1605]) ).
cnf(s1610,plain,
~ spl0_53,
inference(rat,[],[s351,s1605,s1604,s1607]) ).
cnf(s1613,plain,
spl0_52,
inference(rat,[],[s40,s1606,s1483,s1610]) ).
cnf(s1621,plain,
spl0_114,
inference(rat,[],[s117,s1613]) ).
cnf(s1622,plain,
~ spl0_68,
inference(rat,[],[s73,s1613]) ).
cnf(s1623,plain,
~ spl0_67,
inference(rat,[],[s72,s1613]) ).
cnf(s1628,plain,
spl0_10,
inference(rat,[],[s2,s1487,s1404,s23,s1445,s1048,s83,s127,s128,s1456,s42,s1523,s1483,s1584,s1599,s1621,s1623,s1622,s1610,s1591]) ).
cnf(s1629,plain,
~ spl0_59,
inference(rat,[],[s1517,s1628]) ).
cnf(s1630,plain,
~ spl0_63,
inference(rat,[],[s1514,s1599,s1628]) ).
cnf(s1631,plain,
spl0_20,
inference(rat,[],[s1526,s1591,s1599,s1628]) ).
cnf(s1632,plain,
spl0_26,
inference(rat,[],[s167,s1592,s1630]) ).
cnf(s1634,plain,
~ spl0_58,
inference(rat,[],[s1589,s1631]) ).
cnf(s1640,plain,
~ spl0_15,
inference(rat,[],[s1492,s1591,s1632]) ).
cnf(s1642,plain,
$false,
inference(rat,[],[s47,s1629,s1483,s1634,s1640]) ).
fof(f3939,plain,
$false,
inference(avatar_sat_refutation,[],[s1642]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN489-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 16:16:17 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.98 % (2048113)Input is clausal, will run a generic CNF schedule.
% 0.64/0.98 % (2048122)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1141216248:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 0.64/0.98 % (2048122)First to succeed.
% 0.64/0.98 % (2048122)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2048113"
% 0.64/0.98 % (2048119)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3751504897:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 0.64/0.98 % (2048120)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3308393500:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 0.64/0.98 % (2048118)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2860814014:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 0.64/0.98 % (2048121)lrs+10_1_sil=8000:sp=occurrence:random_seed=2647543733:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 0.64/0.98 % (2048124)dis-21_1_sil=8000:lcm=predicate:random_seed=1435821557:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 0.64/0.98 % (2048123)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2109065695:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 0.64/0.98 % (2048124)Also succeeded, but the first one will report.
% 0.64/0.98 % (2048121)Also succeeded, but the first one will report.
% 0.64/0.98 % (2048123)Also succeeded, but the first one will report.
% 0.64/0.98 % (2048122)Refutation found. Thanks to Tanya!
% 0.64/0.98 % SZS status Unsatisfiable for theBenchmark
% 0.64/0.98 % SZS output start Proof for theBenchmark
% See solution above
% 2.94/1.18 % (2048122)------------------------------
% 2.94/1.18 % (2048122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.18 % (2048122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.18 % (2048122)CaDiCaL version: 2.1.3
% 2.94/1.18 % (2048122)Termination reason: Refutation
% 2.94/1.18 % (2048122)Time elapsed: 0.038 s
% 2.94/1.18 % (2048122)Peak memory usage: 91 MB
% 2.94/1.18 % (2048122)Instructions burned: 101 (million)
% 2.94/1.18 % (2048122)------------------------------
% 2.94/1.18 % (2048122)------------------------------
% 2.94/1.18 % (2048113)Success in time 0.331 s
% 2.94/1.18 % Vampire exiting
%------------------------------------------------------------------------------