%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN447+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:51:43 PM UTC 2026
% Result : Theorem 3.28s 1.14s
% Output : Refutation 4.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 169
% Syntax : Number of formulae : 926 ( 18 unt; 168 def)
% Number of atoms : 6663 ( 0 equ)
% Maximal formula atoms : 778 ( 7 avg)
% Number of connectives : 8883 (3146 ~;3715 |;1575 &)
% ( 168 <=>; 279 =>; 0 <=; 0 <~>)
% Maximal formula depth : 130 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 238 ( 237 usr; 234 prp; 0-1 aty)
% Number of functors : 64 ( 64 usr; 64 con; 0-0 aty)
% Number of variables : 610 ( 0 sgn 610 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a1020)
& ~ c1_1(a1020)
& ~ c2_1(a1020) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a1023)
& ~ c1_1(a1023)
& ~ c0_1(a1023) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1024)
& c1_1(a1024)
& ~ c3_1(a1024) ) )
& ( ~ hskp3
| ( ndr1_0
& ~ c0_1(a1025)
& ~ c3_1(a1025)
& ~ c2_1(a1025) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a1026)
& ~ c2_1(a1026)
& ~ c1_1(a1026) ) )
& ( ~ hskp5
| ( ndr1_0
& c1_1(a1027)
& c2_1(a1027)
& ~ c3_1(a1027) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c2_1(a1030)
& ~ c3_1(a1030)
& ~ c0_1(a1030) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a1035)
& c1_1(a1035)
& ~ c2_1(a1035) ) )
& ( ~ hskp8
| ( ndr1_0
& c0_1(a1036)
& ~ c3_1(a1036)
& ~ c1_1(a1036) ) )
& ( ~ hskp9
| ( ndr1_0
& ~ c1_1(a1038)
& c2_1(a1038)
& ~ c0_1(a1038) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a1039)
& ~ c2_1(a1039)
& ~ c0_1(a1039) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c3_1(a1041)
& c1_1(a1041)
& ~ c2_1(a1041) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c1_1(a1043)
& c0_1(a1043)
& ~ c3_1(a1043) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a1048)
& c3_1(a1048)
& ~ c2_1(a1048) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a1055)
& ~ c1_1(a1055)
& ~ c2_1(a1055) ) )
& ( ~ hskp15
| ( ndr1_0
& c3_1(a1059)
& c2_1(a1059)
& ~ c1_1(a1059) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1064)
& c0_1(a1064)
& ~ c3_1(a1064) ) )
& ( ~ hskp17
| ( ndr1_0
& ~ c0_1(a1077)
& c3_1(a1077)
& ~ c2_1(a1077) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a1078)
& c0_1(a1078)
& ~ c1_1(a1078) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a1079)
& ~ c0_1(a1079)
& ~ c2_1(a1079) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c0_1(a1080)
& ~ c2_1(a1080)
& ~ c1_1(a1080) ) )
& ( ~ hskp21
| ( ndr1_0
& ~ c3_1(a1082)
& ~ c2_1(a1082)
& ~ c0_1(a1082) ) )
& ( ~ hskp22
| ( ndr1_0
& c2_1(a1083)
& c3_1(a1083)
& ~ c1_1(a1083) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a1088)
& c3_1(a1088)
& ~ c2_1(a1088) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c2_1(a1089)
& c0_1(a1089)
& ~ c1_1(a1089) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c3_1(a1091)
& ~ c0_1(a1091)
& ~ c2_1(a1091) ) )
& ( ~ hskp26
| ( ndr1_0
& ~ c3_1(a1098)
& c1_1(a1098)
& ~ c0_1(a1098) ) )
& ( ~ hskp27
| ( ndr1_0
& c3_1(a1101)
& c1_1(a1101)
& ~ c0_1(a1101) ) )
& ( ~ hskp28
| ( ndr1_0
& ~ c0_1(a1102)
& c2_1(a1102)
& ~ c1_1(a1102) ) )
& ( ~ hskp29
| ( ndr1_0
& ~ c1_1(a1021)
& ~ c3_1(a1021)
& c2_1(a1021) ) )
& ( ~ hskp30
| ( ndr1_0
& ~ c2_1(a1022)
& c3_1(a1022)
& c1_1(a1022) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a1028)
& ~ c1_1(a1028)
& c3_1(a1028) ) )
& ( ~ hskp32
| ( ndr1_0
& ~ c0_1(a1029)
& c1_1(a1029)
& c2_1(a1029) ) )
& ( ~ hskp33
| ( ndr1_0
& c3_1(a1031)
& ~ c1_1(a1031)
& c2_1(a1031) ) )
& ( ~ hskp34
| ( ndr1_0
& ~ c2_1(a1032)
& ~ c1_1(a1032)
& c3_1(a1032) ) )
& ( ~ hskp35
| ( ndr1_0
& c0_1(a1033)
& c1_1(a1033)
& c3_1(a1033) ) )
& ( ~ hskp36
| ( ndr1_0
& c3_1(a1034)
& ~ c0_1(a1034)
& c1_1(a1034) ) )
& ( ~ hskp37
| ( ndr1_0
& ~ c1_1(a1037)
& c0_1(a1037)
& c3_1(a1037) ) )
& ( ~ hskp38
| ( ndr1_0
& c1_1(a1040)
& c3_1(a1040)
& c2_1(a1040) ) )
& ( ~ hskp39
| ( ndr1_0
& c0_1(a1042)
& ~ c1_1(a1042)
& c2_1(a1042) ) )
& ( ~ hskp40
| ( ndr1_0
& ~ c1_1(a1044)
& c3_1(a1044)
& c0_1(a1044) ) )
& ( ~ hskp41
| ( ndr1_0
& ~ c1_1(a1045)
& ~ c0_1(a1045)
& c3_1(a1045) ) )
& ( ~ hskp42
| ( ndr1_0
& ~ c2_1(a1046)
& c1_1(a1046)
& c0_1(a1046) ) )
& ( ~ hskp43
| ( ndr1_0
& c0_1(a1049)
& c2_1(a1049)
& c1_1(a1049) ) )
& ( ~ hskp44
| ( ndr1_0
& c1_1(a1051)
& ~ c2_1(a1051)
& c0_1(a1051) ) )
& ( ~ hskp45
| ( ndr1_0
& c0_1(a1052)
& c3_1(a1052)
& c2_1(a1052) ) )
& ( ~ hskp46
| ( ndr1_0
& ~ c1_1(a1053)
& ~ c2_1(a1053)
& c0_1(a1053) ) )
& ( ~ hskp47
| ( ndr1_0
& c2_1(a1056)
& c1_1(a1056)
& c3_1(a1056) ) )
& ( ~ hskp48
| ( ndr1_0
& c3_1(a1062)
& c2_1(a1062)
& c0_1(a1062) ) )
& ( ~ hskp49
| ( ndr1_0
& ~ c0_1(a1065)
& ~ c2_1(a1065)
& c1_1(a1065) ) )
& ( ~ hskp50
| ( ndr1_0
& ~ c0_1(a1069)
& c3_1(a1069)
& c1_1(a1069) ) )
& ( ~ hskp51
| ( ndr1_0
& c2_1(a1070)
& ~ c1_1(a1070)
& c0_1(a1070) ) )
& ( ~ hskp52
| ( ndr1_0
& c1_1(a1071)
& c0_1(a1071)
& c3_1(a1071) ) )
& ( ~ hskp53
| ( ndr1_0
& c1_1(a1073)
& c2_1(a1073)
& c0_1(a1073) ) )
& ( ~ hskp54
| ( ndr1_0
& c3_1(a1074)
& c0_1(a1074)
& c2_1(a1074) ) )
& ( ~ hskp55
| ( ndr1_0
& c1_1(a1081)
& ~ c0_1(a1081)
& c3_1(a1081) ) )
& ( ~ hskp56
| ( ndr1_0
& ~ c3_1(a1084)
& ~ c1_1(a1084)
& c0_1(a1084) ) )
& ( ~ hskp57
| ( ndr1_0
& c2_1(a1085)
& c0_1(a1085)
& c3_1(a1085) ) )
& ( ~ hskp58
| ( ndr1_0
& ~ c0_1(a1086)
& c2_1(a1086)
& c3_1(a1086) ) )
& ( ~ hskp59
| ( ndr1_0
& ~ c0_1(a1095)
& ~ c3_1(a1095)
& c1_1(a1095) ) )
& ( ~ hskp60
| ( ndr1_0
& c2_1(a1097)
& ~ c0_1(a1097)
& c3_1(a1097) ) )
& ( ~ hskp61
| ( ndr1_0
& ~ c3_1(a1099)
& ~ c0_1(a1099)
& c2_1(a1099) ) )
& ( ~ hskp62
| ( ndr1_0
& c2_1(a1103)
& c3_1(a1103)
& c1_1(a1103) ) )
& ( ~ hskp63
| ( ndr1_0
& ~ c2_1(a1105)
& c1_1(a1105)
& c3_1(a1105) ) )
& ( hskp0
| hskp29
| hskp30 )
& ( ! [X0] :
( ndr1_0
=> ( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) ) )
| hskp1 )
& ( hskp2
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) )
| ! [X3] :
( ndr1_0
=> ( ~ c0_1(X3)
| ~ c1_1(X3)
| ~ c3_1(X3) ) ) )
& ( ! [X4] :
( ndr1_0
=> ( c2_1(X4)
| c3_1(X4)
| c0_1(X4) ) )
| hskp3
| ! [X5] :
( ndr1_0
=> ( c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) ) )
& ( hskp4
| hskp5
| ! [X6] :
( ndr1_0
=> ( ~ c0_1(X6)
| ~ c2_1(X6)
| c3_1(X6) ) ) )
& ( hskp31
| ! [X7] :
( ndr1_0
=> ( ~ c0_1(X7)
| ~ c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( ~ c2_1(X8)
| c1_1(X8)
| c3_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( ~ c1_1(X9)
| ~ c0_1(X9)
| c3_1(X9) ) )
| hskp32
| hskp6 )
& ( hskp33
| ! [X10] :
( ndr1_0
=> ( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11) ) ) )
& ( ! [X12] :
( ndr1_0
=> ( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13) ) )
| hskp34 )
& ( ! [X14] :
( ndr1_0
=> ( c2_1(X14)
| c0_1(X14)
| c3_1(X14) ) )
| hskp35
| ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c2_1(X15)
| ~ c3_1(X15) ) ) )
& ( ! [X16] :
( ndr1_0
=> ( c2_1(X16)
| ~ c1_1(X16)
| c0_1(X16) ) )
| hskp36
| hskp7 )
& ( ! [X17] :
( ndr1_0
=> ( ~ c3_1(X17)
| ~ c1_1(X17)
| c0_1(X17) ) )
| hskp8
| hskp37 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c3_1(X18)
| c2_1(X18) ) )
| hskp9
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| ~ c3_1(X19)
| c1_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) )
| hskp10 )
& ( ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21) ) )
| hskp38
| ! [X22] :
( ndr1_0
=> ( ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22) ) ) )
& ( hskp11
| ! [X23] :
( ndr1_0
=> ( ~ c0_1(X23)
| ~ c3_1(X23)
| ~ c1_1(X23) ) )
| hskp39 )
& ( hskp12
| ! [X24] :
( ndr1_0
=> ( ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25) ) ) )
& ( hskp40
| hskp41
| ! [X26] :
( ndr1_0
=> ( ~ c0_1(X26)
| c1_1(X26)
| ~ c2_1(X26) ) ) )
& ( hskp42
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| c0_1(X27)
| ~ c2_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( ~ c1_1(X28)
| ~ c3_1(X28)
| c2_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( ~ c0_1(X29)
| c2_1(X29)
| ~ c1_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c1_1(X30)
| ~ c0_1(X30)
| ~ c3_1(X30) ) )
| hskp4 )
& ( ! [X31] :
( ndr1_0
=> ( ~ c0_1(X31)
| ~ c2_1(X31)
| c3_1(X31) ) )
| hskp13
| hskp43 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( ~ c0_1(X33)
| ~ c3_1(X33)
| ~ c2_1(X33) ) )
| hskp7 )
& ( ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| c3_1(X34)
| c2_1(X34) ) )
| hskp44
| hskp45 )
& ( hskp46
| hskp38
| hskp14 )
& ( ! [X35] :
( ndr1_0
=> ( ~ c0_1(X35)
| ~ c2_1(X35)
| c1_1(X35) ) )
| hskp47
| ! [X36] :
( ndr1_0
=> ( ~ c2_1(X36)
| ~ c0_1(X36)
| c3_1(X36) ) ) )
& ( hskp10
| ! [X37] :
( ndr1_0
=> ( ~ c1_1(X37)
| c0_1(X37)
| ~ c2_1(X37) ) )
| hskp43 )
& ( ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38) ) )
| hskp15
| hskp33 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| ~ c1_1(X39)
| c3_1(X39) ) )
| hskp36
| hskp48 )
& ( ! [X40] :
( ndr1_0
=> ( ~ c1_1(X40)
| c3_1(X40)
| c2_1(X40) ) )
| hskp42
| hskp16 )
& ( ! [X41] :
( ndr1_0
=> ( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c3_1(X42)
| c1_1(X42)
| c0_1(X42) ) )
| hskp49 )
& ( ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| c2_1(X43)
| c0_1(X43) ) )
| hskp1
| ! [X44] :
( ndr1_0
=> ( c1_1(X44)
| c2_1(X44)
| ~ c0_1(X44) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( c1_1(X45)
| c3_1(X45)
| c0_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47) ) ) )
& ( hskp7
| ! [X48] :
( ndr1_0
=> ( ~ c2_1(X48)
| ~ c1_1(X48)
| c3_1(X48) ) )
| hskp12 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c2_1(X49)
| ~ c1_1(X49) ) )
| hskp50
| hskp51 )
& ( ! [X50] :
( ndr1_0
=> ( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| c1_1(X52)
| c2_1(X52) ) ) )
& ( hskp52
| hskp34
| ! [X53] :
( ndr1_0
=> ( ~ c3_1(X53)
| c1_1(X53)
| ~ c0_1(X53) ) ) )
& ( ! [X54] :
( ndr1_0
=> ( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54) ) )
| hskp53
| ! [X55] :
( ndr1_0
=> ( ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55) ) ) )
& ( hskp54
| hskp47
| ! [X56] :
( ndr1_0
=> ( ~ c3_1(X56)
| ~ c2_1(X56)
| ~ c1_1(X56) ) ) )
& ( ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59) ) ) )
& ( hskp39
| hskp17
| hskp18 )
& ( hskp19
| ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| ~ c0_1(X60)
| c3_1(X60) ) )
| hskp20 )
& ( hskp55
| ! [X61] :
( ndr1_0
=> ( ~ c0_1(X61)
| c2_1(X61)
| c1_1(X61) ) )
| hskp21 )
& ( hskp22
| ! [X62] :
( ndr1_0
=> ( ~ c1_1(X62)
| c2_1(X62)
| ~ c3_1(X62) ) )
| hskp56 )
& ( ! [X63] :
( ndr1_0
=> ( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| c3_1(X64)
| c1_1(X64) ) )
| ! [X65] :
( ndr1_0
=> ( c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65) ) ) )
& ( ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67) ) )
| hskp57 )
& ( ! [X68] :
( ndr1_0
=> ( c2_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( ~ c3_1(X69)
| c1_1(X69)
| c2_1(X69) ) )
| hskp58 )
& ( hskp33
| hskp23
| ! [X70] :
( ndr1_0
=> ( ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c3_1(X70) ) ) )
& ( ! [X71] :
( ndr1_0
=> ( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| c0_1(X72)
| c3_1(X72) ) )
| hskp24 )
& ( ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73) ) )
| hskp36
| ! [X74] :
( ndr1_0
=> ( ~ c1_1(X74)
| c0_1(X74)
| ~ c3_1(X74) ) ) )
& ( ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75) ) )
| hskp25
| ! [X76] :
( ndr1_0
=> ( ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) ) )
& ( hskp51
| ! [X77] :
( ndr1_0
=> ( ~ c0_1(X77)
| ~ c3_1(X77)
| ~ c2_1(X77) ) )
| ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| ~ c0_1(X78)
| c2_1(X78) ) ) )
& ( hskp48
| ! [X79] :
( ndr1_0
=> ( c0_1(X79)
| c2_1(X79)
| c1_1(X79) ) )
| hskp14 )
& ( ! [X80] :
( ndr1_0
=> ( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81) ) )
| ! [X82] :
( ndr1_0
=> ( c0_1(X82)
| c1_1(X82)
| c2_1(X82) ) ) )
& ( ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83) ) )
| ! [X84] :
( ndr1_0
=> ( ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85) ) ) )
& ( ! [X86] :
( ndr1_0
=> ( ~ c3_1(X86)
| c2_1(X86)
| ~ c1_1(X86) ) )
| hskp59
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| c0_1(X87)
| c2_1(X87) ) ) )
& ( ! [X88] :
( ndr1_0
=> ( ~ c2_1(X88)
| ~ c3_1(X88)
| c0_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89) ) )
| hskp35 )
& ( ! [X90] :
( ndr1_0
=> ( ~ c0_1(X90)
| c1_1(X90)
| c2_1(X90) ) )
| hskp60
| hskp26 )
& ( ! [X91] :
( ndr1_0
=> ( ~ c3_1(X91)
| ~ c1_1(X91)
| c0_1(X91) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c1_1(X92)
| c3_1(X92)
| c2_1(X92) ) )
| hskp61 )
& ( hskp43
| hskp27
| hskp28 )
& ( hskp62
| hskp56
| hskp63 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a1020)
& ~ c1_1(a1020)
& ~ c2_1(a1020) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a1023)
& ~ c1_1(a1023)
& ~ c0_1(a1023) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1024)
& c1_1(a1024)
& ~ c3_1(a1024) ) )
& ( ~ hskp3
| ( ndr1_0
& ~ c0_1(a1025)
& ~ c3_1(a1025)
& ~ c2_1(a1025) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a1026)
& ~ c2_1(a1026)
& ~ c1_1(a1026) ) )
& ( ~ hskp5
| ( ndr1_0
& c1_1(a1027)
& c2_1(a1027)
& ~ c3_1(a1027) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c2_1(a1030)
& ~ c3_1(a1030)
& ~ c0_1(a1030) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a1035)
& c1_1(a1035)
& ~ c2_1(a1035) ) )
& ( ~ hskp8
| ( ndr1_0
& c0_1(a1036)
& ~ c3_1(a1036)
& ~ c1_1(a1036) ) )
& ( ~ hskp9
| ( ndr1_0
& ~ c1_1(a1038)
& c2_1(a1038)
& ~ c0_1(a1038) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a1039)
& ~ c2_1(a1039)
& ~ c0_1(a1039) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c3_1(a1041)
& c1_1(a1041)
& ~ c2_1(a1041) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c1_1(a1043)
& c0_1(a1043)
& ~ c3_1(a1043) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a1048)
& c3_1(a1048)
& ~ c2_1(a1048) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a1055)
& ~ c1_1(a1055)
& ~ c2_1(a1055) ) )
& ( ~ hskp15
| ( ndr1_0
& c3_1(a1059)
& c2_1(a1059)
& ~ c1_1(a1059) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1064)
& c0_1(a1064)
& ~ c3_1(a1064) ) )
& ( ~ hskp17
| ( ndr1_0
& ~ c0_1(a1077)
& c3_1(a1077)
& ~ c2_1(a1077) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a1078)
& c0_1(a1078)
& ~ c1_1(a1078) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a1079)
& ~ c0_1(a1079)
& ~ c2_1(a1079) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c0_1(a1080)
& ~ c2_1(a1080)
& ~ c1_1(a1080) ) )
& ( ~ hskp21
| ( ndr1_0
& ~ c3_1(a1082)
& ~ c2_1(a1082)
& ~ c0_1(a1082) ) )
& ( ~ hskp22
| ( ndr1_0
& c2_1(a1083)
& c3_1(a1083)
& ~ c1_1(a1083) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a1088)
& c3_1(a1088)
& ~ c2_1(a1088) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c2_1(a1089)
& c0_1(a1089)
& ~ c1_1(a1089) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c3_1(a1091)
& ~ c0_1(a1091)
& ~ c2_1(a1091) ) )
& ( ~ hskp26
| ( ndr1_0
& ~ c3_1(a1098)
& c1_1(a1098)
& ~ c0_1(a1098) ) )
& ( ~ hskp27
| ( ndr1_0
& c3_1(a1101)
& c1_1(a1101)
& ~ c0_1(a1101) ) )
& ( ~ hskp28
| ( ndr1_0
& ~ c0_1(a1102)
& c2_1(a1102)
& ~ c1_1(a1102) ) )
& ( ~ hskp29
| ( ndr1_0
& ~ c1_1(a1021)
& ~ c3_1(a1021)
& c2_1(a1021) ) )
& ( ~ hskp30
| ( ndr1_0
& ~ c2_1(a1022)
& c3_1(a1022)
& c1_1(a1022) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a1028)
& ~ c1_1(a1028)
& c3_1(a1028) ) )
& ( ~ hskp32
| ( ndr1_0
& ~ c0_1(a1029)
& c1_1(a1029)
& c2_1(a1029) ) )
& ( ~ hskp33
| ( ndr1_0
& c3_1(a1031)
& ~ c1_1(a1031)
& c2_1(a1031) ) )
& ( ~ hskp34
| ( ndr1_0
& ~ c2_1(a1032)
& ~ c1_1(a1032)
& c3_1(a1032) ) )
& ( ~ hskp35
| ( ndr1_0
& c0_1(a1033)
& c1_1(a1033)
& c3_1(a1033) ) )
& ( ~ hskp36
| ( ndr1_0
& c3_1(a1034)
& ~ c0_1(a1034)
& c1_1(a1034) ) )
& ( ~ hskp37
| ( ndr1_0
& ~ c1_1(a1037)
& c0_1(a1037)
& c3_1(a1037) ) )
& ( ~ hskp38
| ( ndr1_0
& c1_1(a1040)
& c3_1(a1040)
& c2_1(a1040) ) )
& ( ~ hskp39
| ( ndr1_0
& c0_1(a1042)
& ~ c1_1(a1042)
& c2_1(a1042) ) )
& ( ~ hskp40
| ( ndr1_0
& ~ c1_1(a1044)
& c3_1(a1044)
& c0_1(a1044) ) )
& ( ~ hskp41
| ( ndr1_0
& ~ c1_1(a1045)
& ~ c0_1(a1045)
& c3_1(a1045) ) )
& ( ~ hskp42
| ( ndr1_0
& ~ c2_1(a1046)
& c1_1(a1046)
& c0_1(a1046) ) )
& ( ~ hskp43
| ( ndr1_0
& c0_1(a1049)
& c2_1(a1049)
& c1_1(a1049) ) )
& ( ~ hskp44
| ( ndr1_0
& c1_1(a1051)
& ~ c2_1(a1051)
& c0_1(a1051) ) )
& ( ~ hskp45
| ( ndr1_0
& c0_1(a1052)
& c3_1(a1052)
& c2_1(a1052) ) )
& ( ~ hskp46
| ( ndr1_0
& ~ c1_1(a1053)
& ~ c2_1(a1053)
& c0_1(a1053) ) )
& ( ~ hskp47
| ( ndr1_0
& c2_1(a1056)
& c1_1(a1056)
& c3_1(a1056) ) )
& ( ~ hskp48
| ( ndr1_0
& c3_1(a1062)
& c2_1(a1062)
& c0_1(a1062) ) )
& ( ~ hskp49
| ( ndr1_0
& ~ c0_1(a1065)
& ~ c2_1(a1065)
& c1_1(a1065) ) )
& ( ~ hskp50
| ( ndr1_0
& ~ c0_1(a1069)
& c3_1(a1069)
& c1_1(a1069) ) )
& ( ~ hskp51
| ( ndr1_0
& c2_1(a1070)
& ~ c1_1(a1070)
& c0_1(a1070) ) )
& ( ~ hskp52
| ( ndr1_0
& c1_1(a1071)
& c0_1(a1071)
& c3_1(a1071) ) )
& ( ~ hskp53
| ( ndr1_0
& c1_1(a1073)
& c2_1(a1073)
& c0_1(a1073) ) )
& ( ~ hskp54
| ( ndr1_0
& c3_1(a1074)
& c0_1(a1074)
& c2_1(a1074) ) )
& ( ~ hskp55
| ( ndr1_0
& c1_1(a1081)
& ~ c0_1(a1081)
& c3_1(a1081) ) )
& ( ~ hskp56
| ( ndr1_0
& ~ c3_1(a1084)
& ~ c1_1(a1084)
& c0_1(a1084) ) )
& ( ~ hskp57
| ( ndr1_0
& c2_1(a1085)
& c0_1(a1085)
& c3_1(a1085) ) )
& ( ~ hskp58
| ( ndr1_0
& ~ c0_1(a1086)
& c2_1(a1086)
& c3_1(a1086) ) )
& ( ~ hskp59
| ( ndr1_0
& ~ c0_1(a1095)
& ~ c3_1(a1095)
& c1_1(a1095) ) )
& ( ~ hskp60
| ( ndr1_0
& c2_1(a1097)
& ~ c0_1(a1097)
& c3_1(a1097) ) )
& ( ~ hskp61
| ( ndr1_0
& ~ c3_1(a1099)
& ~ c0_1(a1099)
& c2_1(a1099) ) )
& ( ~ hskp62
| ( ndr1_0
& c2_1(a1103)
& c3_1(a1103)
& c1_1(a1103) ) )
& ( ~ hskp63
| ( ndr1_0
& ~ c2_1(a1105)
& c1_1(a1105)
& c3_1(a1105) ) )
& ( hskp0
| hskp29
| hskp30 )
& ( ! [X0] :
( ndr1_0
=> ( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) ) )
| hskp1 )
& ( hskp2
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) )
| ! [X3] :
( ndr1_0
=> ( ~ c0_1(X3)
| ~ c1_1(X3)
| ~ c3_1(X3) ) ) )
& ( ! [X4] :
( ndr1_0
=> ( c2_1(X4)
| c3_1(X4)
| c0_1(X4) ) )
| hskp3
| ! [X5] :
( ndr1_0
=> ( c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) ) )
& ( hskp4
| hskp5
| ! [X6] :
( ndr1_0
=> ( ~ c0_1(X6)
| ~ c2_1(X6)
| c3_1(X6) ) ) )
& ( hskp31
| ! [X7] :
( ndr1_0
=> ( ~ c0_1(X7)
| ~ c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( ~ c2_1(X8)
| c1_1(X8)
| c3_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( ~ c1_1(X9)
| ~ c0_1(X9)
| c3_1(X9) ) )
| hskp32
| hskp6 )
& ( hskp33
| ! [X10] :
( ndr1_0
=> ( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11) ) ) )
& ( ! [X12] :
( ndr1_0
=> ( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13) ) )
| hskp34 )
& ( ! [X14] :
( ndr1_0
=> ( c2_1(X14)
| c0_1(X14)
| c3_1(X14) ) )
| hskp35
| ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c2_1(X15)
| ~ c3_1(X15) ) ) )
& ( ! [X16] :
( ndr1_0
=> ( c2_1(X16)
| ~ c1_1(X16)
| c0_1(X16) ) )
| hskp36
| hskp7 )
& ( ! [X17] :
( ndr1_0
=> ( ~ c3_1(X17)
| ~ c1_1(X17)
| c0_1(X17) ) )
| hskp8
| hskp37 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c3_1(X18)
| c2_1(X18) ) )
| hskp9
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| ~ c3_1(X19)
| c1_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) )
| hskp10 )
& ( ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21) ) )
| hskp38
| ! [X22] :
( ndr1_0
=> ( ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22) ) ) )
& ( hskp11
| ! [X23] :
( ndr1_0
=> ( ~ c0_1(X23)
| ~ c3_1(X23)
| ~ c1_1(X23) ) )
| hskp39 )
& ( hskp12
| ! [X24] :
( ndr1_0
=> ( ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25) ) ) )
& ( hskp40
| hskp41
| ! [X26] :
( ndr1_0
=> ( ~ c0_1(X26)
| c1_1(X26)
| ~ c2_1(X26) ) ) )
& ( hskp42
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| c0_1(X27)
| ~ c2_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( ~ c1_1(X28)
| ~ c3_1(X28)
| c2_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( ~ c0_1(X29)
| c2_1(X29)
| ~ c1_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c1_1(X30)
| ~ c0_1(X30)
| ~ c3_1(X30) ) )
| hskp4 )
& ( ! [X31] :
( ndr1_0
=> ( ~ c0_1(X31)
| ~ c2_1(X31)
| c3_1(X31) ) )
| hskp13
| hskp43 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( ~ c0_1(X33)
| ~ c3_1(X33)
| ~ c2_1(X33) ) )
| hskp7 )
& ( ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| c3_1(X34)
| c2_1(X34) ) )
| hskp44
| hskp45 )
& ( hskp46
| hskp38
| hskp14 )
& ( ! [X35] :
( ndr1_0
=> ( ~ c0_1(X35)
| ~ c2_1(X35)
| c1_1(X35) ) )
| hskp47
| ! [X36] :
( ndr1_0
=> ( ~ c2_1(X36)
| ~ c0_1(X36)
| c3_1(X36) ) ) )
& ( hskp10
| ! [X37] :
( ndr1_0
=> ( ~ c1_1(X37)
| c0_1(X37)
| ~ c2_1(X37) ) )
| hskp43 )
& ( ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38) ) )
| hskp15
| hskp33 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| ~ c1_1(X39)
| c3_1(X39) ) )
| hskp36
| hskp48 )
& ( ! [X40] :
( ndr1_0
=> ( ~ c1_1(X40)
| c3_1(X40)
| c2_1(X40) ) )
| hskp42
| hskp16 )
& ( ! [X41] :
( ndr1_0
=> ( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c3_1(X42)
| c1_1(X42)
| c0_1(X42) ) )
| hskp49 )
& ( ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| c2_1(X43)
| c0_1(X43) ) )
| hskp1
| ! [X44] :
( ndr1_0
=> ( c1_1(X44)
| c2_1(X44)
| ~ c0_1(X44) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( c1_1(X45)
| c3_1(X45)
| c0_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47) ) ) )
& ( hskp7
| ! [X48] :
( ndr1_0
=> ( ~ c2_1(X48)
| ~ c1_1(X48)
| c3_1(X48) ) )
| hskp12 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c2_1(X49)
| ~ c1_1(X49) ) )
| hskp50
| hskp51 )
& ( ! [X50] :
( ndr1_0
=> ( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| c1_1(X52)
| c2_1(X52) ) ) )
& ( hskp52
| hskp34
| ! [X53] :
( ndr1_0
=> ( ~ c3_1(X53)
| c1_1(X53)
| ~ c0_1(X53) ) ) )
& ( ! [X54] :
( ndr1_0
=> ( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54) ) )
| hskp53
| ! [X55] :
( ndr1_0
=> ( ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55) ) ) )
& ( hskp54
| hskp47
| ! [X56] :
( ndr1_0
=> ( ~ c3_1(X56)
| ~ c2_1(X56)
| ~ c1_1(X56) ) ) )
& ( ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59) ) ) )
& ( hskp39
| hskp17
| hskp18 )
& ( hskp19
| ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| ~ c0_1(X60)
| c3_1(X60) ) )
| hskp20 )
& ( hskp55
| ! [X61] :
( ndr1_0
=> ( ~ c0_1(X61)
| c2_1(X61)
| c1_1(X61) ) )
| hskp21 )
& ( hskp22
| ! [X62] :
( ndr1_0
=> ( ~ c1_1(X62)
| c2_1(X62)
| ~ c3_1(X62) ) )
| hskp56 )
& ( ! [X63] :
( ndr1_0
=> ( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| c3_1(X64)
| c1_1(X64) ) )
| ! [X65] :
( ndr1_0
=> ( c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65) ) ) )
& ( ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67) ) )
| hskp57 )
& ( ! [X68] :
( ndr1_0
=> ( c2_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( ~ c3_1(X69)
| c1_1(X69)
| c2_1(X69) ) )
| hskp58 )
& ( hskp33
| hskp23
| ! [X70] :
( ndr1_0
=> ( ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c3_1(X70) ) ) )
& ( ! [X71] :
( ndr1_0
=> ( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| c0_1(X72)
| c3_1(X72) ) )
| hskp24 )
& ( ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73) ) )
| hskp36
| ! [X74] :
( ndr1_0
=> ( ~ c1_1(X74)
| c0_1(X74)
| ~ c3_1(X74) ) ) )
& ( ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75) ) )
| hskp25
| ! [X76] :
( ndr1_0
=> ( ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) ) )
& ( hskp51
| ! [X77] :
( ndr1_0
=> ( ~ c0_1(X77)
| ~ c3_1(X77)
| ~ c2_1(X77) ) )
| ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| ~ c0_1(X78)
| c2_1(X78) ) ) )
& ( hskp48
| ! [X79] :
( ndr1_0
=> ( c0_1(X79)
| c2_1(X79)
| c1_1(X79) ) )
| hskp14 )
& ( ! [X80] :
( ndr1_0
=> ( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81) ) )
| ! [X82] :
( ndr1_0
=> ( c0_1(X82)
| c1_1(X82)
| c2_1(X82) ) ) )
& ( ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83) ) )
| ! [X84] :
( ndr1_0
=> ( ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85) ) ) )
& ( ! [X86] :
( ndr1_0
=> ( ~ c3_1(X86)
| c2_1(X86)
| ~ c1_1(X86) ) )
| hskp59
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| c0_1(X87)
| c2_1(X87) ) ) )
& ( ! [X88] :
( ndr1_0
=> ( ~ c2_1(X88)
| ~ c3_1(X88)
| c0_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89) ) )
| hskp35 )
& ( ! [X90] :
( ndr1_0
=> ( ~ c0_1(X90)
| c1_1(X90)
| c2_1(X90) ) )
| hskp60
| hskp26 )
& ( ! [X91] :
( ndr1_0
=> ( ~ c3_1(X91)
| ~ c1_1(X91)
| c0_1(X91) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c1_1(X92)
| c3_1(X92)
| c2_1(X92) ) )
| hskp61 )
& ( hskp43
| hskp27
| hskp28 )
& ( hskp62
| hskp56
| hskp63 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a1020)
& ~ c1_1(a1020)
& ~ c2_1(a1020) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a1023)
& ~ c1_1(a1023)
& ~ c0_1(a1023) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1024)
& c1_1(a1024)
& ~ c3_1(a1024) ) )
& ( ~ hskp3
| ( ndr1_0
& ~ c0_1(a1025)
& ~ c3_1(a1025)
& ~ c2_1(a1025) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a1026)
& ~ c2_1(a1026)
& ~ c1_1(a1026) ) )
& ( ~ hskp5
| ( ndr1_0
& c1_1(a1027)
& c2_1(a1027)
& ~ c3_1(a1027) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c2_1(a1030)
& ~ c3_1(a1030)
& ~ c0_1(a1030) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a1035)
& c1_1(a1035)
& ~ c2_1(a1035) ) )
& ( ~ hskp8
| ( ndr1_0
& c0_1(a1036)
& ~ c3_1(a1036)
& ~ c1_1(a1036) ) )
& ( ~ hskp9
| ( ndr1_0
& ~ c1_1(a1038)
& c2_1(a1038)
& ~ c0_1(a1038) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a1039)
& ~ c2_1(a1039)
& ~ c0_1(a1039) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c3_1(a1041)
& c1_1(a1041)
& ~ c2_1(a1041) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c1_1(a1043)
& c0_1(a1043)
& ~ c3_1(a1043) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a1048)
& c3_1(a1048)
& ~ c2_1(a1048) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a1055)
& ~ c1_1(a1055)
& ~ c2_1(a1055) ) )
& ( ~ hskp15
| ( ndr1_0
& c3_1(a1059)
& c2_1(a1059)
& ~ c1_1(a1059) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1064)
& c0_1(a1064)
& ~ c3_1(a1064) ) )
& ( ~ hskp17
| ( ndr1_0
& ~ c0_1(a1077)
& c3_1(a1077)
& ~ c2_1(a1077) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a1078)
& c0_1(a1078)
& ~ c1_1(a1078) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a1079)
& ~ c0_1(a1079)
& ~ c2_1(a1079) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c0_1(a1080)
& ~ c2_1(a1080)
& ~ c1_1(a1080) ) )
& ( ~ hskp21
| ( ndr1_0
& ~ c3_1(a1082)
& ~ c2_1(a1082)
& ~ c0_1(a1082) ) )
& ( ~ hskp22
| ( ndr1_0
& c2_1(a1083)
& c3_1(a1083)
& ~ c1_1(a1083) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a1088)
& c3_1(a1088)
& ~ c2_1(a1088) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c2_1(a1089)
& c0_1(a1089)
& ~ c1_1(a1089) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c3_1(a1091)
& ~ c0_1(a1091)
& ~ c2_1(a1091) ) )
& ( ~ hskp26
| ( ndr1_0
& ~ c3_1(a1098)
& c1_1(a1098)
& ~ c0_1(a1098) ) )
& ( ~ hskp27
| ( ndr1_0
& c3_1(a1101)
& c1_1(a1101)
& ~ c0_1(a1101) ) )
& ( ~ hskp28
| ( ndr1_0
& ~ c0_1(a1102)
& c2_1(a1102)
& ~ c1_1(a1102) ) )
& ( ~ hskp29
| ( ndr1_0
& ~ c1_1(a1021)
& ~ c3_1(a1021)
& c2_1(a1021) ) )
& ( ~ hskp30
| ( ndr1_0
& ~ c2_1(a1022)
& c3_1(a1022)
& c1_1(a1022) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a1028)
& ~ c1_1(a1028)
& c3_1(a1028) ) )
& ( ~ hskp32
| ( ndr1_0
& ~ c0_1(a1029)
& c1_1(a1029)
& c2_1(a1029) ) )
& ( ~ hskp33
| ( ndr1_0
& c3_1(a1031)
& ~ c1_1(a1031)
& c2_1(a1031) ) )
& ( ~ hskp34
| ( ndr1_0
& ~ c2_1(a1032)
& ~ c1_1(a1032)
& c3_1(a1032) ) )
& ( ~ hskp35
| ( ndr1_0
& c0_1(a1033)
& c1_1(a1033)
& c3_1(a1033) ) )
& ( ~ hskp36
| ( ndr1_0
& c3_1(a1034)
& ~ c0_1(a1034)
& c1_1(a1034) ) )
& ( ~ hskp37
| ( ndr1_0
& ~ c1_1(a1037)
& c0_1(a1037)
& c3_1(a1037) ) )
& ( ~ hskp38
| ( ndr1_0
& c1_1(a1040)
& c3_1(a1040)
& c2_1(a1040) ) )
& ( ~ hskp39
| ( ndr1_0
& c0_1(a1042)
& ~ c1_1(a1042)
& c2_1(a1042) ) )
& ( ~ hskp40
| ( ndr1_0
& ~ c1_1(a1044)
& c3_1(a1044)
& c0_1(a1044) ) )
& ( ~ hskp41
| ( ndr1_0
& ~ c1_1(a1045)
& ~ c0_1(a1045)
& c3_1(a1045) ) )
& ( ~ hskp42
| ( ndr1_0
& ~ c2_1(a1046)
& c1_1(a1046)
& c0_1(a1046) ) )
& ( ~ hskp43
| ( ndr1_0
& c0_1(a1049)
& c2_1(a1049)
& c1_1(a1049) ) )
& ( ~ hskp44
| ( ndr1_0
& c1_1(a1051)
& ~ c2_1(a1051)
& c0_1(a1051) ) )
& ( ~ hskp45
| ( ndr1_0
& c0_1(a1052)
& c3_1(a1052)
& c2_1(a1052) ) )
& ( ~ hskp46
| ( ndr1_0
& ~ c1_1(a1053)
& ~ c2_1(a1053)
& c0_1(a1053) ) )
& ( ~ hskp47
| ( ndr1_0
& c2_1(a1056)
& c1_1(a1056)
& c3_1(a1056) ) )
& ( ~ hskp48
| ( ndr1_0
& c3_1(a1062)
& c2_1(a1062)
& c0_1(a1062) ) )
& ( ~ hskp49
| ( ndr1_0
& ~ c0_1(a1065)
& ~ c2_1(a1065)
& c1_1(a1065) ) )
& ( ~ hskp50
| ( ndr1_0
& ~ c0_1(a1069)
& c3_1(a1069)
& c1_1(a1069) ) )
& ( ~ hskp51
| ( ndr1_0
& c2_1(a1070)
& ~ c1_1(a1070)
& c0_1(a1070) ) )
& ( ~ hskp52
| ( ndr1_0
& c1_1(a1071)
& c0_1(a1071)
& c3_1(a1071) ) )
& ( ~ hskp53
| ( ndr1_0
& c1_1(a1073)
& c2_1(a1073)
& c0_1(a1073) ) )
& ( ~ hskp54
| ( ndr1_0
& c3_1(a1074)
& c0_1(a1074)
& c2_1(a1074) ) )
& ( ~ hskp55
| ( ndr1_0
& c1_1(a1081)
& ~ c0_1(a1081)
& c3_1(a1081) ) )
& ( ~ hskp56
| ( ndr1_0
& ~ c3_1(a1084)
& ~ c1_1(a1084)
& c0_1(a1084) ) )
& ( ~ hskp57
| ( ndr1_0
& c2_1(a1085)
& c0_1(a1085)
& c3_1(a1085) ) )
& ( ~ hskp58
| ( ndr1_0
& ~ c0_1(a1086)
& c2_1(a1086)
& c3_1(a1086) ) )
& ( ~ hskp59
| ( ndr1_0
& ~ c0_1(a1095)
& ~ c3_1(a1095)
& c1_1(a1095) ) )
& ( ~ hskp60
| ( ndr1_0
& c2_1(a1097)
& ~ c0_1(a1097)
& c3_1(a1097) ) )
& ( ~ hskp61
| ( ndr1_0
& ~ c3_1(a1099)
& ~ c0_1(a1099)
& c2_1(a1099) ) )
& ( ~ hskp62
| ( ndr1_0
& c2_1(a1103)
& c3_1(a1103)
& c1_1(a1103) ) )
& ( ~ hskp63
| ( ndr1_0
& ~ c2_1(a1105)
& c1_1(a1105)
& c3_1(a1105) ) )
& ( hskp0
| hskp29
| hskp30 )
& ( ! [X0] :
( ndr1_0
=> ( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) ) )
| hskp1 )
& ( hskp2
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) )
| ! [X3] :
( ndr1_0
=> ( ~ c0_1(X3)
| ~ c1_1(X3)
| ~ c3_1(X3) ) ) )
& ( ! [X4] :
( ndr1_0
=> ( c2_1(X4)
| c3_1(X4)
| c0_1(X4) ) )
| hskp3
| ! [X5] :
( ndr1_0
=> ( c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5) ) ) )
& ( hskp4
| hskp5
| ! [X6] :
( ndr1_0
=> ( ~ c0_1(X6)
| ~ c2_1(X6)
| c3_1(X6) ) ) )
& ( hskp31
| ! [X7] :
( ndr1_0
=> ( ~ c0_1(X7)
| ~ c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( ~ c2_1(X8)
| c1_1(X8)
| c3_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( ~ c1_1(X9)
| ~ c0_1(X9)
| c3_1(X9) ) )
| hskp32
| hskp6 )
& ( hskp33
| ! [X10] :
( ndr1_0
=> ( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11) ) ) )
& ( ! [X12] :
( ndr1_0
=> ( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13) ) )
| hskp34 )
& ( ! [X14] :
( ndr1_0
=> ( c2_1(X14)
| c0_1(X14)
| c3_1(X14) ) )
| hskp35
| ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c2_1(X15)
| ~ c3_1(X15) ) ) )
& ( ! [X16] :
( ndr1_0
=> ( c2_1(X16)
| ~ c1_1(X16)
| c0_1(X16) ) )
| hskp36
| hskp7 )
& ( ! [X17] :
( ndr1_0
=> ( ~ c3_1(X17)
| ~ c1_1(X17)
| c0_1(X17) ) )
| hskp8
| hskp37 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c3_1(X18)
| c2_1(X18) ) )
| hskp9
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| ~ c3_1(X19)
| c1_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c3_1(X20)
| c2_1(X20)
| c0_1(X20) ) )
| hskp10 )
& ( ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21) ) )
| hskp38
| ! [X22] :
( ndr1_0
=> ( ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22) ) ) )
& ( hskp11
| ! [X23] :
( ndr1_0
=> ( ~ c0_1(X23)
| ~ c3_1(X23)
| ~ c1_1(X23) ) )
| hskp39 )
& ( hskp12
| ! [X24] :
( ndr1_0
=> ( ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25) ) ) )
& ( hskp40
| hskp41
| ! [X26] :
( ndr1_0
=> ( ~ c0_1(X26)
| c1_1(X26)
| ~ c2_1(X26) ) ) )
& ( hskp42
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| c0_1(X27)
| ~ c2_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( ~ c1_1(X28)
| ~ c3_1(X28)
| c2_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( ~ c0_1(X29)
| c2_1(X29)
| ~ c1_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c1_1(X30)
| ~ c0_1(X30)
| ~ c3_1(X30) ) )
| hskp4 )
& ( ! [X31] :
( ndr1_0
=> ( ~ c0_1(X31)
| ~ c2_1(X31)
| c3_1(X31) ) )
| hskp13
| hskp43 )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( ~ c0_1(X33)
| ~ c3_1(X33)
| ~ c2_1(X33) ) )
| hskp7 )
& ( ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| c3_1(X34)
| c2_1(X34) ) )
| hskp44
| hskp45 )
& ( hskp46
| hskp38
| hskp14 )
& ( ! [X35] :
( ndr1_0
=> ( ~ c0_1(X35)
| ~ c2_1(X35)
| c1_1(X35) ) )
| hskp47
| ! [X36] :
( ndr1_0
=> ( ~ c2_1(X36)
| ~ c0_1(X36)
| c3_1(X36) ) ) )
& ( hskp10
| ! [X37] :
( ndr1_0
=> ( ~ c1_1(X37)
| c0_1(X37)
| ~ c2_1(X37) ) )
| hskp43 )
& ( ! [X38] :
( ndr1_0
=> ( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38) ) )
| hskp15
| hskp33 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| ~ c1_1(X39)
| c3_1(X39) ) )
| hskp36
| hskp48 )
& ( ! [X40] :
( ndr1_0
=> ( ~ c1_1(X40)
| c3_1(X40)
| c2_1(X40) ) )
| hskp42
| hskp16 )
& ( ! [X41] :
( ndr1_0
=> ( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c3_1(X42)
| c1_1(X42)
| c0_1(X42) ) )
| hskp49 )
& ( ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| c2_1(X43)
| c0_1(X43) ) )
| hskp1
| ! [X44] :
( ndr1_0
=> ( c1_1(X44)
| c2_1(X44)
| ~ c0_1(X44) ) ) )
& ( ! [X45] :
( ndr1_0
=> ( c1_1(X45)
| c3_1(X45)
| c0_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47) ) ) )
& ( hskp7
| ! [X48] :
( ndr1_0
=> ( ~ c2_1(X48)
| ~ c1_1(X48)
| c3_1(X48) ) )
| hskp12 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c2_1(X49)
| ~ c1_1(X49) ) )
| hskp50
| hskp51 )
& ( ! [X50] :
( ndr1_0
=> ( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| c1_1(X52)
| c2_1(X52) ) ) )
& ( hskp52
| hskp34
| ! [X53] :
( ndr1_0
=> ( ~ c3_1(X53)
| c1_1(X53)
| ~ c0_1(X53) ) ) )
& ( ! [X54] :
( ndr1_0
=> ( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54) ) )
| hskp53
| ! [X55] :
( ndr1_0
=> ( ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55) ) ) )
& ( hskp54
| hskp47
| ! [X56] :
( ndr1_0
=> ( ~ c3_1(X56)
| ~ c2_1(X56)
| ~ c1_1(X56) ) ) )
& ( ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59) ) ) )
& ( hskp39
| hskp17
| hskp18 )
& ( hskp19
| ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| ~ c0_1(X60)
| c3_1(X60) ) )
| hskp20 )
& ( hskp55
| ! [X61] :
( ndr1_0
=> ( ~ c0_1(X61)
| c2_1(X61)
| c1_1(X61) ) )
| hskp21 )
& ( hskp22
| ! [X62] :
( ndr1_0
=> ( ~ c1_1(X62)
| c2_1(X62)
| ~ c3_1(X62) ) )
| hskp56 )
& ( ! [X63] :
( ndr1_0
=> ( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| c3_1(X64)
| c1_1(X64) ) )
| ! [X65] :
( ndr1_0
=> ( c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65) ) ) )
& ( ! [X66] :
( ndr1_0
=> ( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67) ) )
| hskp57 )
& ( ! [X68] :
( ndr1_0
=> ( c2_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( ~ c3_1(X69)
| c1_1(X69)
| c2_1(X69) ) )
| hskp58 )
& ( hskp33
| hskp23
| ! [X70] :
( ndr1_0
=> ( ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c3_1(X70) ) ) )
& ( ! [X71] :
( ndr1_0
=> ( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| c0_1(X72)
| c3_1(X72) ) )
| hskp24 )
& ( ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73) ) )
| hskp36
| ! [X74] :
( ndr1_0
=> ( ~ c1_1(X74)
| c0_1(X74)
| ~ c3_1(X74) ) ) )
& ( ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75) ) )
| hskp25
| ! [X76] :
( ndr1_0
=> ( ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) ) )
& ( hskp51
| ! [X77] :
( ndr1_0
=> ( ~ c0_1(X77)
| ~ c3_1(X77)
| ~ c2_1(X77) ) )
| ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| ~ c0_1(X78)
| c2_1(X78) ) ) )
& ( hskp48
| ! [X79] :
( ndr1_0
=> ( c0_1(X79)
| c2_1(X79)
| c1_1(X79) ) )
| hskp14 )
& ( ! [X80] :
( ndr1_0
=> ( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81) ) )
| ! [X82] :
( ndr1_0
=> ( c0_1(X82)
| c1_1(X82)
| c2_1(X82) ) ) )
& ( ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83) ) )
| ! [X84] :
( ndr1_0
=> ( ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85) ) ) )
& ( ! [X86] :
( ndr1_0
=> ( ~ c3_1(X86)
| c2_1(X86)
| ~ c1_1(X86) ) )
| hskp59
| ! [X87] :
( ndr1_0
=> ( ~ c3_1(X87)
| c0_1(X87)
| c2_1(X87) ) ) )
& ( ! [X88] :
( ndr1_0
=> ( ~ c2_1(X88)
| ~ c3_1(X88)
| c0_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89) ) )
| hskp35 )
& ( ! [X90] :
( ndr1_0
=> ( ~ c0_1(X90)
| c1_1(X90)
| c2_1(X90) ) )
| hskp60
| hskp26 )
& ( ! [X91] :
( ndr1_0
=> ( ~ c3_1(X91)
| ~ c1_1(X91)
| c0_1(X91) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c1_1(X92)
| c3_1(X92)
| c2_1(X92) ) )
| hskp61 )
& ( hskp43
| hskp27
| hskp28 )
& ( hskp62
| hskp56
| hskp63 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a1020)
& ~ c1_1(a1020)
& ~ c2_1(a1020) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a1023)
& ~ c1_1(a1023)
& ~ c0_1(a1023) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1024)
& c1_1(a1024)
& ~ c3_1(a1024) ) )
& ( ~ hskp3
| ( ndr1_0
& ~ c0_1(a1025)
& ~ c3_1(a1025)
& ~ c2_1(a1025) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a1026)
& ~ c2_1(a1026)
& ~ c1_1(a1026) ) )
& ( ~ hskp5
| ( ndr1_0
& c1_1(a1027)
& c2_1(a1027)
& ~ c3_1(a1027) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c2_1(a1030)
& ~ c3_1(a1030)
& ~ c0_1(a1030) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a1035)
& c1_1(a1035)
& ~ c2_1(a1035) ) )
& ( ~ hskp8
| ( ndr1_0
& c0_1(a1036)
& ~ c3_1(a1036)
& ~ c1_1(a1036) ) )
& ( ~ hskp9
| ( ndr1_0
& ~ c1_1(a1038)
& c2_1(a1038)
& ~ c0_1(a1038) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a1039)
& ~ c2_1(a1039)
& ~ c0_1(a1039) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c3_1(a1041)
& c1_1(a1041)
& ~ c2_1(a1041) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c1_1(a1043)
& c0_1(a1043)
& ~ c3_1(a1043) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a1048)
& c3_1(a1048)
& ~ c2_1(a1048) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a1055)
& ~ c1_1(a1055)
& ~ c2_1(a1055) ) )
& ( ~ hskp15
| ( ndr1_0
& c3_1(a1059)
& c2_1(a1059)
& ~ c1_1(a1059) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1064)
& c0_1(a1064)
& ~ c3_1(a1064) ) )
& ( ~ hskp17
| ( ndr1_0
& ~ c0_1(a1077)
& c3_1(a1077)
& ~ c2_1(a1077) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a1078)
& c0_1(a1078)
& ~ c1_1(a1078) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a1079)
& ~ c0_1(a1079)
& ~ c2_1(a1079) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c0_1(a1080)
& ~ c2_1(a1080)
& ~ c1_1(a1080) ) )
& ( ~ hskp21
| ( ndr1_0
& ~ c3_1(a1082)
& ~ c2_1(a1082)
& ~ c0_1(a1082) ) )
& ( ~ hskp22
| ( ndr1_0
& c2_1(a1083)
& c3_1(a1083)
& ~ c1_1(a1083) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a1088)
& c3_1(a1088)
& ~ c2_1(a1088) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c2_1(a1089)
& c0_1(a1089)
& ~ c1_1(a1089) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c3_1(a1091)
& ~ c0_1(a1091)
& ~ c2_1(a1091) ) )
& ( ~ hskp26
| ( ndr1_0
& ~ c3_1(a1098)
& c1_1(a1098)
& ~ c0_1(a1098) ) )
& ( ~ hskp27
| ( ndr1_0
& c3_1(a1101)
& c1_1(a1101)
& ~ c0_1(a1101) ) )
& ( ~ hskp28
| ( ndr1_0
& ~ c0_1(a1102)
& c2_1(a1102)
& ~ c1_1(a1102) ) )
& ( ~ hskp29
| ( ndr1_0
& ~ c1_1(a1021)
& ~ c3_1(a1021)
& c2_1(a1021) ) )
& ( ~ hskp30
| ( ndr1_0
& ~ c2_1(a1022)
& c3_1(a1022)
& c1_1(a1022) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a1028)
& ~ c1_1(a1028)
& c3_1(a1028) ) )
& ( ~ hskp32
| ( ndr1_0
& ~ c0_1(a1029)
& c1_1(a1029)
& c2_1(a1029) ) )
& ( ~ hskp33
| ( ndr1_0
& c3_1(a1031)
& ~ c1_1(a1031)
& c2_1(a1031) ) )
& ( ~ hskp34
| ( ndr1_0
& ~ c2_1(a1032)
& ~ c1_1(a1032)
& c3_1(a1032) ) )
& ( ~ hskp35
| ( ndr1_0
& c0_1(a1033)
& c1_1(a1033)
& c3_1(a1033) ) )
& ( ~ hskp36
| ( ndr1_0
& c3_1(a1034)
& ~ c0_1(a1034)
& c1_1(a1034) ) )
& ( ~ hskp37
| ( ndr1_0
& ~ c1_1(a1037)
& c0_1(a1037)
& c3_1(a1037) ) )
& ( ~ hskp38
| ( ndr1_0
& c1_1(a1040)
& c3_1(a1040)
& c2_1(a1040) ) )
& ( ~ hskp39
| ( ndr1_0
& c0_1(a1042)
& ~ c1_1(a1042)
& c2_1(a1042) ) )
& ( ~ hskp40
| ( ndr1_0
& ~ c1_1(a1044)
& c3_1(a1044)
& c0_1(a1044) ) )
& ( ~ hskp41
| ( ndr1_0
& ~ c1_1(a1045)
& ~ c0_1(a1045)
& c3_1(a1045) ) )
& ( ~ hskp42
| ( ndr1_0
& ~ c2_1(a1046)
& c1_1(a1046)
& c0_1(a1046) ) )
& ( ~ hskp43
| ( ndr1_0
& c0_1(a1049)
& c2_1(a1049)
& c1_1(a1049) ) )
& ( ~ hskp44
| ( ndr1_0
& c1_1(a1051)
& ~ c2_1(a1051)
& c0_1(a1051) ) )
& ( ~ hskp45
| ( ndr1_0
& c0_1(a1052)
& c3_1(a1052)
& c2_1(a1052) ) )
& ( ~ hskp46
| ( ndr1_0
& ~ c1_1(a1053)
& ~ c2_1(a1053)
& c0_1(a1053) ) )
& ( ~ hskp47
| ( ndr1_0
& c2_1(a1056)
& c1_1(a1056)
& c3_1(a1056) ) )
& ( ~ hskp48
| ( ndr1_0
& c3_1(a1062)
& c2_1(a1062)
& c0_1(a1062) ) )
& ( ~ hskp49
| ( ndr1_0
& ~ c0_1(a1065)
& ~ c2_1(a1065)
& c1_1(a1065) ) )
& ( ~ hskp50
| ( ndr1_0
& ~ c0_1(a1069)
& c3_1(a1069)
& c1_1(a1069) ) )
& ( ~ hskp51
| ( ndr1_0
& c2_1(a1070)
& ~ c1_1(a1070)
& c0_1(a1070) ) )
& ( ~ hskp52
| ( ndr1_0
& c1_1(a1071)
& c0_1(a1071)
& c3_1(a1071) ) )
& ( ~ hskp53
| ( ndr1_0
& c1_1(a1073)
& c2_1(a1073)
& c0_1(a1073) ) )
& ( ~ hskp54
| ( ndr1_0
& c3_1(a1074)
& c0_1(a1074)
& c2_1(a1074) ) )
& ( ~ hskp55
| ( ndr1_0
& c1_1(a1081)
& ~ c0_1(a1081)
& c3_1(a1081) ) )
& ( ~ hskp56
| ( ndr1_0
& ~ c3_1(a1084)
& ~ c1_1(a1084)
& c0_1(a1084) ) )
& ( ~ hskp57
| ( ndr1_0
& c2_1(a1085)
& c0_1(a1085)
& c3_1(a1085) ) )
& ( ~ hskp58
| ( ndr1_0
& ~ c0_1(a1086)
& c2_1(a1086)
& c3_1(a1086) ) )
& ( ~ hskp59
| ( ndr1_0
& ~ c0_1(a1095)
& ~ c3_1(a1095)
& c1_1(a1095) ) )
& ( ~ hskp60
| ( ndr1_0
& c2_1(a1097)
& ~ c0_1(a1097)
& c3_1(a1097) ) )
& ( ~ hskp61
| ( ndr1_0
& ~ c3_1(a1099)
& ~ c0_1(a1099)
& c2_1(a1099) ) )
& ( ~ hskp62
| ( ndr1_0
& c2_1(a1103)
& c3_1(a1103)
& c1_1(a1103) ) )
& ( ~ hskp63
| ( ndr1_0
& ~ c2_1(a1105)
& c1_1(a1105)
& c3_1(a1105) ) )
& ( hskp0
| hskp29
| hskp30 )
& ( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0 )
| hskp1 )
& ( hskp2
| ! [X2] :
( c3_1(X2)
| c2_1(X2)
| c0_1(X2)
| ~ ndr1_0 )
| ! [X3] :
( ~ c0_1(X3)
| ~ c1_1(X3)
| ~ c3_1(X3)
| ~ ndr1_0 ) )
& ( ! [X4] :
( c2_1(X4)
| c3_1(X4)
| c0_1(X4)
| ~ ndr1_0 )
| hskp3
| ! [X5] :
( c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5)
| ~ ndr1_0 ) )
& ( hskp4
| hskp5
| ! [X6] :
( ~ c0_1(X6)
| ~ c2_1(X6)
| c3_1(X6)
| ~ ndr1_0 ) )
& ( hskp31
| ! [X7] :
( ~ c0_1(X7)
| ~ c1_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( ~ c2_1(X8)
| c1_1(X8)
| c3_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( ~ c1_1(X9)
| ~ c0_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| hskp32
| hskp6 )
& ( hskp33
| ! [X10] :
( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10)
| ~ ndr1_0 )
| ! [X11] :
( ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11)
| ~ ndr1_0 ) )
& ( ! [X12] :
( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13)
| ~ ndr1_0 )
| hskp34 )
& ( ! [X14] :
( c2_1(X14)
| c0_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| hskp35
| ! [X15] :
( c0_1(X15)
| c2_1(X15)
| ~ c3_1(X15)
| ~ ndr1_0 ) )
& ( ! [X16] :
( c2_1(X16)
| ~ c1_1(X16)
| c0_1(X16)
| ~ ndr1_0 )
| hskp36
| hskp7 )
& ( ! [X17] :
( ~ c3_1(X17)
| ~ c1_1(X17)
| c0_1(X17)
| ~ ndr1_0 )
| hskp8
| hskp37 )
& ( ! [X18] :
( c0_1(X18)
| c3_1(X18)
| c2_1(X18)
| ~ ndr1_0 )
| hskp9
| ! [X19] :
( c0_1(X19)
| ~ c3_1(X19)
| c1_1(X19)
| ~ ndr1_0 ) )
& ( ! [X20] :
( c3_1(X20)
| c2_1(X20)
| c0_1(X20)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X21] :
( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21)
| ~ ndr1_0 )
| hskp38
| ! [X22] :
( ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22)
| ~ ndr1_0 ) )
& ( hskp11
| ! [X23] :
( ~ c0_1(X23)
| ~ c3_1(X23)
| ~ c1_1(X23)
| ~ ndr1_0 )
| hskp39 )
& ( hskp12
| ! [X24] :
( ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25)
| ~ ndr1_0 ) )
& ( hskp40
| hskp41
| ! [X26] :
( ~ c0_1(X26)
| c1_1(X26)
| ~ c2_1(X26)
| ~ ndr1_0 ) )
& ( hskp42
| ! [X27] :
( c1_1(X27)
| c0_1(X27)
| ~ c2_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( ~ c1_1(X28)
| ~ c3_1(X28)
| c2_1(X28)
| ~ ndr1_0 ) )
& ( ! [X29] :
( ~ c0_1(X29)
| c2_1(X29)
| ~ c1_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( c1_1(X30)
| ~ c0_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X31] :
( ~ c0_1(X31)
| ~ c2_1(X31)
| c3_1(X31)
| ~ ndr1_0 )
| hskp13
| hskp43 )
& ( ! [X32] :
( c0_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 )
| ! [X33] :
( ~ c0_1(X33)
| ~ c3_1(X33)
| ~ c2_1(X33)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X34] :
( c1_1(X34)
| c3_1(X34)
| c2_1(X34)
| ~ ndr1_0 )
| hskp44
| hskp45 )
& ( hskp46
| hskp38
| hskp14 )
& ( ! [X35] :
( ~ c0_1(X35)
| ~ c2_1(X35)
| c1_1(X35)
| ~ ndr1_0 )
| hskp47
| ! [X36] :
( ~ c2_1(X36)
| ~ c0_1(X36)
| c3_1(X36)
| ~ ndr1_0 ) )
& ( hskp10
| ! [X37] :
( ~ c1_1(X37)
| c0_1(X37)
| ~ c2_1(X37)
| ~ ndr1_0 )
| hskp43 )
& ( ! [X38] :
( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38)
| ~ ndr1_0 )
| hskp15
| hskp33 )
& ( ! [X39] :
( c0_1(X39)
| ~ c1_1(X39)
| c3_1(X39)
| ~ ndr1_0 )
| hskp36
| hskp48 )
& ( ! [X40] :
( ~ c1_1(X40)
| c3_1(X40)
| c2_1(X40)
| ~ ndr1_0 )
| hskp42
| hskp16 )
& ( ! [X41] :
( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41)
| ~ ndr1_0 )
| ! [X42] :
( c3_1(X42)
| c1_1(X42)
| c0_1(X42)
| ~ ndr1_0 )
| hskp49 )
& ( ! [X43] :
( c3_1(X43)
| c2_1(X43)
| c0_1(X43)
| ~ ndr1_0 )
| hskp1
| ! [X44] :
( c1_1(X44)
| c2_1(X44)
| ~ c0_1(X44)
| ~ ndr1_0 ) )
& ( ! [X45] :
( c1_1(X45)
| c3_1(X45)
| c0_1(X45)
| ~ ndr1_0 )
| ! [X46] :
( c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 ) )
& ( hskp7
| ! [X48] :
( ~ c2_1(X48)
| ~ c1_1(X48)
| c3_1(X48)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X49] :
( c0_1(X49)
| ~ c2_1(X49)
| ~ c1_1(X49)
| ~ ndr1_0 )
| hskp50
| hskp51 )
& ( ! [X50] :
( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c3_1(X52)
| c1_1(X52)
| c2_1(X52)
| ~ ndr1_0 ) )
& ( hskp52
| hskp34
| ! [X53] :
( ~ c3_1(X53)
| c1_1(X53)
| ~ c0_1(X53)
| ~ ndr1_0 ) )
& ( ! [X54] :
( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54)
| ~ ndr1_0 )
| hskp53
| ! [X55] :
( ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55)
| ~ ndr1_0 ) )
& ( hskp54
| hskp47
| ! [X56] :
( ~ c3_1(X56)
| ~ c2_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0 ) )
& ( ! [X57] :
( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59)
| ~ ndr1_0 ) )
& ( hskp39
| hskp17
| hskp18 )
& ( hskp19
| ! [X60] :
( c1_1(X60)
| ~ c0_1(X60)
| c3_1(X60)
| ~ ndr1_0 )
| hskp20 )
& ( hskp55
| ! [X61] :
( ~ c0_1(X61)
| c2_1(X61)
| c1_1(X61)
| ~ ndr1_0 )
| hskp21 )
& ( hskp22
| ! [X62] :
( ~ c1_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0 )
| hskp56 )
& ( ! [X63] :
( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c0_1(X64)
| c3_1(X64)
| c1_1(X64)
| ~ ndr1_0 )
| ! [X65] :
( c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65)
| ~ ndr1_0 ) )
& ( ! [X66] :
( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66)
| ~ ndr1_0 )
| ! [X67] :
( ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67)
| ~ ndr1_0 )
| hskp57 )
& ( ! [X68] :
( c2_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( ~ c3_1(X69)
| c1_1(X69)
| c2_1(X69)
| ~ ndr1_0 )
| hskp58 )
& ( hskp33
| hskp23
| ! [X70] :
( ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 ) )
& ( ! [X71] :
( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0 )
| ! [X72] :
( c1_1(X72)
| c0_1(X72)
| c3_1(X72)
| ~ ndr1_0 )
| hskp24 )
& ( ! [X73] :
( ~ c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73)
| ~ ndr1_0 )
| hskp36
| ! [X74] :
( ~ c1_1(X74)
| c0_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 ) )
& ( ! [X75] :
( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75)
| ~ ndr1_0 )
| hskp25
| ! [X76] :
( ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 ) )
& ( hskp51
| ! [X77] :
( ~ c0_1(X77)
| ~ c3_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 )
| ! [X78] :
( c1_1(X78)
| ~ c0_1(X78)
| c2_1(X78)
| ~ ndr1_0 ) )
& ( hskp48
| ! [X79] :
( c0_1(X79)
| c2_1(X79)
| c1_1(X79)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X80] :
( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81)
| ~ ndr1_0 )
| ! [X82] :
( c0_1(X82)
| c1_1(X82)
| c2_1(X82)
| ~ ndr1_0 ) )
& ( ! [X83] :
( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83)
| ~ ndr1_0 )
| ! [X84] :
( ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0 ) )
& ( ! [X86] :
( ~ c3_1(X86)
| c2_1(X86)
| ~ c1_1(X86)
| ~ ndr1_0 )
| hskp59
| ! [X87] :
( ~ c3_1(X87)
| c0_1(X87)
| c2_1(X87)
| ~ ndr1_0 ) )
& ( ! [X88] :
( ~ c2_1(X88)
| ~ c3_1(X88)
| c0_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0 )
| hskp35 )
& ( ! [X90] :
( ~ c0_1(X90)
| c1_1(X90)
| c2_1(X90)
| ~ ndr1_0 )
| hskp60
| hskp26 )
& ( ! [X91] :
( ~ c3_1(X91)
| ~ c1_1(X91)
| c0_1(X91)
| ~ ndr1_0 )
| ! [X92] :
( ~ c1_1(X92)
| c3_1(X92)
| c2_1(X92)
| ~ ndr1_0 )
| hskp61 )
& ( hskp43
| hskp27
| hskp28 )
& ( hskp62
| hskp56
| hskp63 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a1020)
& ~ c1_1(a1020)
& ~ c2_1(a1020) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a1023)
& ~ c1_1(a1023)
& ~ c0_1(a1023) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a1024)
& c1_1(a1024)
& ~ c3_1(a1024) ) )
& ( ~ hskp3
| ( ndr1_0
& ~ c0_1(a1025)
& ~ c3_1(a1025)
& ~ c2_1(a1025) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a1026)
& ~ c2_1(a1026)
& ~ c1_1(a1026) ) )
& ( ~ hskp5
| ( ndr1_0
& c1_1(a1027)
& c2_1(a1027)
& ~ c3_1(a1027) ) )
& ( ~ hskp6
| ( ndr1_0
& ~ c2_1(a1030)
& ~ c3_1(a1030)
& ~ c0_1(a1030) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a1035)
& c1_1(a1035)
& ~ c2_1(a1035) ) )
& ( ~ hskp8
| ( ndr1_0
& c0_1(a1036)
& ~ c3_1(a1036)
& ~ c1_1(a1036) ) )
& ( ~ hskp9
| ( ndr1_0
& ~ c1_1(a1038)
& c2_1(a1038)
& ~ c0_1(a1038) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a1039)
& ~ c2_1(a1039)
& ~ c0_1(a1039) ) )
& ( ~ hskp11
| ( ndr1_0
& ~ c3_1(a1041)
& c1_1(a1041)
& ~ c2_1(a1041) ) )
& ( ~ hskp12
| ( ndr1_0
& ~ c1_1(a1043)
& c0_1(a1043)
& ~ c3_1(a1043) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a1048)
& c3_1(a1048)
& ~ c2_1(a1048) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a1055)
& ~ c1_1(a1055)
& ~ c2_1(a1055) ) )
& ( ~ hskp15
| ( ndr1_0
& c3_1(a1059)
& c2_1(a1059)
& ~ c1_1(a1059) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a1064)
& c0_1(a1064)
& ~ c3_1(a1064) ) )
& ( ~ hskp17
| ( ndr1_0
& ~ c0_1(a1077)
& c3_1(a1077)
& ~ c2_1(a1077) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a1078)
& c0_1(a1078)
& ~ c1_1(a1078) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a1079)
& ~ c0_1(a1079)
& ~ c2_1(a1079) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c0_1(a1080)
& ~ c2_1(a1080)
& ~ c1_1(a1080) ) )
& ( ~ hskp21
| ( ndr1_0
& ~ c3_1(a1082)
& ~ c2_1(a1082)
& ~ c0_1(a1082) ) )
& ( ~ hskp22
| ( ndr1_0
& c2_1(a1083)
& c3_1(a1083)
& ~ c1_1(a1083) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a1088)
& c3_1(a1088)
& ~ c2_1(a1088) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c2_1(a1089)
& c0_1(a1089)
& ~ c1_1(a1089) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c3_1(a1091)
& ~ c0_1(a1091)
& ~ c2_1(a1091) ) )
& ( ~ hskp26
| ( ndr1_0
& ~ c3_1(a1098)
& c1_1(a1098)
& ~ c0_1(a1098) ) )
& ( ~ hskp27
| ( ndr1_0
& c3_1(a1101)
& c1_1(a1101)
& ~ c0_1(a1101) ) )
& ( ~ hskp28
| ( ndr1_0
& ~ c0_1(a1102)
& c2_1(a1102)
& ~ c1_1(a1102) ) )
& ( ~ hskp29
| ( ndr1_0
& ~ c1_1(a1021)
& ~ c3_1(a1021)
& c2_1(a1021) ) )
& ( ~ hskp30
| ( ndr1_0
& ~ c2_1(a1022)
& c3_1(a1022)
& c1_1(a1022) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a1028)
& ~ c1_1(a1028)
& c3_1(a1028) ) )
& ( ~ hskp32
| ( ndr1_0
& ~ c0_1(a1029)
& c1_1(a1029)
& c2_1(a1029) ) )
& ( ~ hskp33
| ( ndr1_0
& c3_1(a1031)
& ~ c1_1(a1031)
& c2_1(a1031) ) )
& ( ~ hskp34
| ( ndr1_0
& ~ c2_1(a1032)
& ~ c1_1(a1032)
& c3_1(a1032) ) )
& ( ~ hskp35
| ( ndr1_0
& c0_1(a1033)
& c1_1(a1033)
& c3_1(a1033) ) )
& ( ~ hskp36
| ( ndr1_0
& c3_1(a1034)
& ~ c0_1(a1034)
& c1_1(a1034) ) )
& ( ~ hskp37
| ( ndr1_0
& ~ c1_1(a1037)
& c0_1(a1037)
& c3_1(a1037) ) )
& ( ~ hskp38
| ( ndr1_0
& c1_1(a1040)
& c3_1(a1040)
& c2_1(a1040) ) )
& ( ~ hskp39
| ( ndr1_0
& c0_1(a1042)
& ~ c1_1(a1042)
& c2_1(a1042) ) )
& ( ~ hskp40
| ( ndr1_0
& ~ c1_1(a1044)
& c3_1(a1044)
& c0_1(a1044) ) )
& ( ~ hskp41
| ( ndr1_0
& ~ c1_1(a1045)
& ~ c0_1(a1045)
& c3_1(a1045) ) )
& ( ~ hskp42
| ( ndr1_0
& ~ c2_1(a1046)
& c1_1(a1046)
& c0_1(a1046) ) )
& ( ~ hskp43
| ( ndr1_0
& c0_1(a1049)
& c2_1(a1049)
& c1_1(a1049) ) )
& ( ~ hskp44
| ( ndr1_0
& c1_1(a1051)
& ~ c2_1(a1051)
& c0_1(a1051) ) )
& ( ~ hskp45
| ( ndr1_0
& c0_1(a1052)
& c3_1(a1052)
& c2_1(a1052) ) )
& ( ~ hskp46
| ( ndr1_0
& ~ c1_1(a1053)
& ~ c2_1(a1053)
& c0_1(a1053) ) )
& ( ~ hskp47
| ( ndr1_0
& c2_1(a1056)
& c1_1(a1056)
& c3_1(a1056) ) )
& ( ~ hskp48
| ( ndr1_0
& c3_1(a1062)
& c2_1(a1062)
& c0_1(a1062) ) )
& ( ~ hskp49
| ( ndr1_0
& ~ c0_1(a1065)
& ~ c2_1(a1065)
& c1_1(a1065) ) )
& ( ~ hskp50
| ( ndr1_0
& ~ c0_1(a1069)
& c3_1(a1069)
& c1_1(a1069) ) )
& ( ~ hskp51
| ( ndr1_0
& c2_1(a1070)
& ~ c1_1(a1070)
& c0_1(a1070) ) )
& ( ~ hskp52
| ( ndr1_0
& c1_1(a1071)
& c0_1(a1071)
& c3_1(a1071) ) )
& ( ~ hskp53
| ( ndr1_0
& c1_1(a1073)
& c2_1(a1073)
& c0_1(a1073) ) )
& ( ~ hskp54
| ( ndr1_0
& c3_1(a1074)
& c0_1(a1074)
& c2_1(a1074) ) )
& ( ~ hskp55
| ( ndr1_0
& c1_1(a1081)
& ~ c0_1(a1081)
& c3_1(a1081) ) )
& ( ~ hskp56
| ( ndr1_0
& ~ c3_1(a1084)
& ~ c1_1(a1084)
& c0_1(a1084) ) )
& ( ~ hskp57
| ( ndr1_0
& c2_1(a1085)
& c0_1(a1085)
& c3_1(a1085) ) )
& ( ~ hskp58
| ( ndr1_0
& ~ c0_1(a1086)
& c2_1(a1086)
& c3_1(a1086) ) )
& ( ~ hskp59
| ( ndr1_0
& ~ c0_1(a1095)
& ~ c3_1(a1095)
& c1_1(a1095) ) )
& ( ~ hskp60
| ( ndr1_0
& c2_1(a1097)
& ~ c0_1(a1097)
& c3_1(a1097) ) )
& ( ~ hskp61
| ( ndr1_0
& ~ c3_1(a1099)
& ~ c0_1(a1099)
& c2_1(a1099) ) )
& ( ~ hskp62
| ( ndr1_0
& c2_1(a1103)
& c3_1(a1103)
& c1_1(a1103) ) )
& ( ~ hskp63
| ( ndr1_0
& ~ c2_1(a1105)
& c1_1(a1105)
& c3_1(a1105) ) )
& ( hskp0
| hskp29
| hskp30 )
& ( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0 )
| hskp1 )
& ( hskp2
| ! [X2] :
( c3_1(X2)
| c2_1(X2)
| c0_1(X2)
| ~ ndr1_0 )
| ! [X3] :
( ~ c0_1(X3)
| ~ c1_1(X3)
| ~ c3_1(X3)
| ~ ndr1_0 ) )
& ( ! [X4] :
( c2_1(X4)
| c3_1(X4)
| c0_1(X4)
| ~ ndr1_0 )
| hskp3
| ! [X5] :
( c1_1(X5)
| ~ c0_1(X5)
| c2_1(X5)
| ~ ndr1_0 ) )
& ( hskp4
| hskp5
| ! [X6] :
( ~ c0_1(X6)
| ~ c2_1(X6)
| c3_1(X6)
| ~ ndr1_0 ) )
& ( hskp31
| ! [X7] :
( ~ c0_1(X7)
| ~ c1_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( ~ c2_1(X8)
| c1_1(X8)
| c3_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( ~ c1_1(X9)
| ~ c0_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| hskp32
| hskp6 )
& ( hskp33
| ! [X10] :
( ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10)
| ~ ndr1_0 )
| ! [X11] :
( ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11)
| ~ ndr1_0 ) )
& ( ! [X12] :
( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13)
| ~ ndr1_0 )
| hskp34 )
& ( ! [X14] :
( c2_1(X14)
| c0_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| hskp35
| ! [X15] :
( c0_1(X15)
| c2_1(X15)
| ~ c3_1(X15)
| ~ ndr1_0 ) )
& ( ! [X16] :
( c2_1(X16)
| ~ c1_1(X16)
| c0_1(X16)
| ~ ndr1_0 )
| hskp36
| hskp7 )
& ( ! [X17] :
( ~ c3_1(X17)
| ~ c1_1(X17)
| c0_1(X17)
| ~ ndr1_0 )
| hskp8
| hskp37 )
& ( ! [X18] :
( c0_1(X18)
| c3_1(X18)
| c2_1(X18)
| ~ ndr1_0 )
| hskp9
| ! [X19] :
( c0_1(X19)
| ~ c3_1(X19)
| c1_1(X19)
| ~ ndr1_0 ) )
& ( ! [X20] :
( c3_1(X20)
| c2_1(X20)
| c0_1(X20)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X21] :
( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21)
| ~ ndr1_0 )
| hskp38
| ! [X22] :
( ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22)
| ~ ndr1_0 ) )
& ( hskp11
| ! [X23] :
( ~ c0_1(X23)
| ~ c3_1(X23)
| ~ c1_1(X23)
| ~ ndr1_0 )
| hskp39 )
& ( hskp12
| ! [X24] :
( ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25)
| ~ ndr1_0 ) )
& ( hskp40
| hskp41
| ! [X26] :
( ~ c0_1(X26)
| c1_1(X26)
| ~ c2_1(X26)
| ~ ndr1_0 ) )
& ( hskp42
| ! [X27] :
( c1_1(X27)
| c0_1(X27)
| ~ c2_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( ~ c1_1(X28)
| ~ c3_1(X28)
| c2_1(X28)
| ~ ndr1_0 ) )
& ( ! [X29] :
( ~ c0_1(X29)
| c2_1(X29)
| ~ c1_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( c1_1(X30)
| ~ c0_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X31] :
( ~ c0_1(X31)
| ~ c2_1(X31)
| c3_1(X31)
| ~ ndr1_0 )
| hskp13
| hskp43 )
& ( ! [X32] :
( c0_1(X32)
| ~ c2_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 )
| ! [X33] :
( ~ c0_1(X33)
| ~ c3_1(X33)
| ~ c2_1(X33)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X34] :
( c1_1(X34)
| c3_1(X34)
| c2_1(X34)
| ~ ndr1_0 )
| hskp44
| hskp45 )
& ( hskp46
| hskp38
| hskp14 )
& ( ! [X35] :
( ~ c0_1(X35)
| ~ c2_1(X35)
| c1_1(X35)
| ~ ndr1_0 )
| hskp47
| ! [X36] :
( ~ c2_1(X36)
| ~ c0_1(X36)
| c3_1(X36)
| ~ ndr1_0 ) )
& ( hskp10
| ! [X37] :
( ~ c1_1(X37)
| c0_1(X37)
| ~ c2_1(X37)
| ~ ndr1_0 )
| hskp43 )
& ( ! [X38] :
( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38)
| ~ ndr1_0 )
| hskp15
| hskp33 )
& ( ! [X39] :
( c0_1(X39)
| ~ c1_1(X39)
| c3_1(X39)
| ~ ndr1_0 )
| hskp36
| hskp48 )
& ( ! [X40] :
( ~ c1_1(X40)
| c3_1(X40)
| c2_1(X40)
| ~ ndr1_0 )
| hskp42
| hskp16 )
& ( ! [X41] :
( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41)
| ~ ndr1_0 )
| ! [X42] :
( c3_1(X42)
| c1_1(X42)
| c0_1(X42)
| ~ ndr1_0 )
| hskp49 )
& ( ! [X43] :
( c3_1(X43)
| c2_1(X43)
| c0_1(X43)
| ~ ndr1_0 )
| hskp1
| ! [X44] :
( c1_1(X44)
| c2_1(X44)
| ~ c0_1(X44)
| ~ ndr1_0 ) )
& ( ! [X45] :
( c1_1(X45)
| c3_1(X45)
| c0_1(X45)
| ~ ndr1_0 )
| ! [X46] :
( c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 ) )
& ( hskp7
| ! [X48] :
( ~ c2_1(X48)
| ~ c1_1(X48)
| c3_1(X48)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X49] :
( c0_1(X49)
| ~ c2_1(X49)
| ~ c1_1(X49)
| ~ ndr1_0 )
| hskp50
| hskp51 )
& ( ! [X50] :
( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c3_1(X52)
| c1_1(X52)
| c2_1(X52)
| ~ ndr1_0 ) )
& ( hskp52
| hskp34
| ! [X53] :
( ~ c3_1(X53)
| c1_1(X53)
| ~ c0_1(X53)
| ~ ndr1_0 ) )
& ( ! [X54] :
( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54)
| ~ ndr1_0 )
| hskp53
| ! [X55] :
( ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55)
| ~ ndr1_0 ) )
& ( hskp54
| hskp47
| ! [X56] :
( ~ c3_1(X56)
| ~ c2_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0 ) )
& ( ! [X57] :
( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59)
| ~ ndr1_0 ) )
& ( hskp39
| hskp17
| hskp18 )
& ( hskp19
| ! [X60] :
( c1_1(X60)
| ~ c0_1(X60)
| c3_1(X60)
| ~ ndr1_0 )
| hskp20 )
& ( hskp55
| ! [X61] :
( ~ c0_1(X61)
| c2_1(X61)
| c1_1(X61)
| ~ ndr1_0 )
| hskp21 )
& ( hskp22
| ! [X62] :
( ~ c1_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0 )
| hskp56 )
& ( ! [X63] :
( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c0_1(X64)
| c3_1(X64)
| c1_1(X64)
| ~ ndr1_0 )
| ! [X65] :
( c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65)
| ~ ndr1_0 ) )
& ( ! [X66] :
( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66)
| ~ ndr1_0 )
| ! [X67] :
( ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67)
| ~ ndr1_0 )
| hskp57 )
& ( ! [X68] :
( c2_1(X68)
| ~ c1_1(X68)
| ~ c3_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( ~ c3_1(X69)
| c1_1(X69)
| c2_1(X69)
| ~ ndr1_0 )
| hskp58 )
& ( hskp33
| hskp23
| ! [X70] :
( ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 ) )
& ( ! [X71] :
( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0 )
| ! [X72] :
( c1_1(X72)
| c0_1(X72)
| c3_1(X72)
| ~ ndr1_0 )
| hskp24 )
& ( ! [X73] :
( ~ c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73)
| ~ ndr1_0 )
| hskp36
| ! [X74] :
( ~ c1_1(X74)
| c0_1(X74)
| ~ c3_1(X74)
| ~ ndr1_0 ) )
& ( ! [X75] :
( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75)
| ~ ndr1_0 )
| hskp25
| ! [X76] :
( ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 ) )
& ( hskp51
| ! [X77] :
( ~ c0_1(X77)
| ~ c3_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 )
| ! [X78] :
( c1_1(X78)
| ~ c0_1(X78)
| c2_1(X78)
| ~ ndr1_0 ) )
& ( hskp48
| ! [X79] :
( c0_1(X79)
| c2_1(X79)
| c1_1(X79)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X80] :
( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81)
| ~ ndr1_0 )
| ! [X82] :
( c0_1(X82)
| c1_1(X82)
| c2_1(X82)
| ~ ndr1_0 ) )
& ( ! [X83] :
( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83)
| ~ ndr1_0 )
| ! [X84] :
( ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0 ) )
& ( ! [X86] :
( ~ c3_1(X86)
| c2_1(X86)
| ~ c1_1(X86)
| ~ ndr1_0 )
| hskp59
| ! [X87] :
( ~ c3_1(X87)
| c0_1(X87)
| c2_1(X87)
| ~ ndr1_0 ) )
& ( ! [X88] :
( ~ c2_1(X88)
| ~ c3_1(X88)
| c0_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c2_1(X89)
| c3_1(X89)
| ~ c1_1(X89)
| ~ ndr1_0 )
| hskp35 )
& ( ! [X90] :
( ~ c0_1(X90)
| c1_1(X90)
| c2_1(X90)
| ~ ndr1_0 )
| hskp60
| hskp26 )
& ( ! [X91] :
( ~ c3_1(X91)
| ~ c1_1(X91)
| c0_1(X91)
| ~ ndr1_0 )
| ! [X92] :
( ~ c1_1(X92)
| c3_1(X92)
| c2_1(X92)
| ~ ndr1_0 )
| hskp61 )
& ( hskp43
| hskp27
| hskp28 )
& ( hskp62
| hskp56
| hskp63 ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
( hskp62
| hskp56
| hskp63 ),
inference(cnf_transformation,[],[f5]) ).
fof(f7,plain,
( hskp43
| hskp27
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f12,plain,
! [X83,X84,X85] :
( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83)
| ~ ndr1_0
| ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84)
| ~ ndr1_0
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f13,plain,
! [X82,X80,X81] :
( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0
| c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81)
| ~ ndr1_0
| c0_1(X82)
| c1_1(X82)
| c2_1(X82)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f16,plain,
! [X76,X75] :
( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75)
| ~ ndr1_0
| hskp25
| ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f18,plain,
! [X72,X71] :
( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0
| c1_1(X72)
| c0_1(X72)
| c3_1(X72)
| ~ ndr1_0
| hskp24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f19,plain,
! [X70] :
( hskp33
| hskp23
| ~ c0_1(X70)
| ~ c2_1(X70)
| ~ c3_1(X70)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f21,plain,
! [X66,X67] :
( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66)
| ~ ndr1_0
| ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67)
| ~ ndr1_0
| hskp57 ),
inference(cnf_transformation,[],[f5]) ).
fof(f22,plain,
! [X65,X63,X64] :
( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63)
| ~ ndr1_0
| c0_1(X64)
| c3_1(X64)
| c1_1(X64)
| ~ ndr1_0
| c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X62] :
( hskp22
| ~ c1_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0
| hskp56 ),
inference(cnf_transformation,[],[f5]) ).
fof(f24,plain,
! [X61] :
( hskp55
| ~ c0_1(X61)
| c2_1(X61)
| c1_1(X61)
| ~ ndr1_0
| hskp21 ),
inference(cnf_transformation,[],[f5]) ).
fof(f25,plain,
! [X60] :
( hskp19
| c1_1(X60)
| ~ c0_1(X60)
| c3_1(X60)
| ~ ndr1_0
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X58,X59,X57] :
( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0
| c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58)
| ~ ndr1_0
| ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f28,plain,
! [X56] :
( hskp54
| hskp47
| ~ c3_1(X56)
| ~ c2_1(X56)
| ~ c1_1(X56)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f29,plain,
! [X54,X55] :
( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54)
| ~ ndr1_0
| hskp53
| ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f31,plain,
! [X50,X51,X52] :
( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50)
| ~ ndr1_0
| ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51)
| ~ ndr1_0
| c3_1(X52)
| c1_1(X52)
| c2_1(X52)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f34,plain,
! [X46,X47,X45] :
( c1_1(X45)
| c3_1(X45)
| c0_1(X45)
| ~ ndr1_0
| c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46)
| ~ ndr1_0
| c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X41,X42] :
( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41)
| ~ ndr1_0
| c3_1(X42)
| c1_1(X42)
| c0_1(X42)
| ~ ndr1_0
| hskp49 ),
inference(cnf_transformation,[],[f5]) ).
fof(f38,plain,
! [X39] :
( c0_1(X39)
| ~ c1_1(X39)
| c3_1(X39)
| ~ ndr1_0
| hskp36
| hskp48 ),
inference(cnf_transformation,[],[f5]) ).
fof(f39,plain,
! [X38] :
( ~ c3_1(X38)
| c2_1(X38)
| c0_1(X38)
| ~ ndr1_0
| hskp15
| hskp33 ),
inference(cnf_transformation,[],[f5]) ).
fof(f40,plain,
! [X37] :
( hskp10
| ~ c1_1(X37)
| c0_1(X37)
| ~ c2_1(X37)
| ~ ndr1_0
| hskp43 ),
inference(cnf_transformation,[],[f5]) ).
fof(f42,plain,
( hskp46
| hskp38
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f49,plain,
! [X24,X25] :
( hskp12
| ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24)
| ~ ndr1_0
| ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f51,plain,
! [X21,X22] :
( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21)
| ~ ndr1_0
| hskp38
| ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f52,plain,
! [X20] :
( c3_1(X20)
| c2_1(X20)
| c0_1(X20)
| ~ ndr1_0
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f54,plain,
! [X17] :
( ~ c3_1(X17)
| ~ c1_1(X17)
| c0_1(X17)
| ~ ndr1_0
| hskp8
| hskp37 ),
inference(cnf_transformation,[],[f5]) ).
fof(f57,plain,
! [X12,X13] :
( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12)
| ~ ndr1_0
| c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13)
| ~ ndr1_0
| hskp34 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X10,X11] :
( hskp33
| ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10)
| ~ ndr1_0
| ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f59,plain,
! [X9] :
( ~ c1_1(X9)
| ~ c0_1(X9)
| c3_1(X9)
| ~ ndr1_0
| hskp32
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f66,plain,
( ~ hskp63
| c3_1(a1105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f67,plain,
( ~ hskp63
| c1_1(a1105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f68,plain,
( ~ hskp63
| ~ c2_1(a1105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f69,plain,
( ~ hskp63
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f70,plain,
( ~ hskp62
| c1_1(a1103) ),
inference(cnf_transformation,[],[f5]) ).
fof(f71,plain,
( ~ hskp62
| c3_1(a1103) ),
inference(cnf_transformation,[],[f5]) ).
fof(f72,plain,
( ~ hskp62
| c2_1(a1103) ),
inference(cnf_transformation,[],[f5]) ).
fof(f73,plain,
( ~ hskp62
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
( ~ hskp57
| c3_1(a1085) ),
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
( ~ hskp57
| c0_1(a1085) ),
inference(cnf_transformation,[],[f5]) ).
fof(f92,plain,
( ~ hskp57
| c2_1(a1085) ),
inference(cnf_transformation,[],[f5]) ).
fof(f94,plain,
( ~ hskp56
| c0_1(a1084) ),
inference(cnf_transformation,[],[f5]) ).
fof(f95,plain,
( ~ hskp56
| ~ c1_1(a1084) ),
inference(cnf_transformation,[],[f5]) ).
fof(f96,plain,
( ~ hskp56
| ~ c3_1(a1084) ),
inference(cnf_transformation,[],[f5]) ).
fof(f97,plain,
( ~ hskp56
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f98,plain,
( ~ hskp55
| c3_1(a1081) ),
inference(cnf_transformation,[],[f5]) ).
fof(f99,plain,
( ~ hskp55
| ~ c0_1(a1081) ),
inference(cnf_transformation,[],[f5]) ).
fof(f100,plain,
( ~ hskp55
| c1_1(a1081) ),
inference(cnf_transformation,[],[f5]) ).
fof(f102,plain,
( ~ hskp54
| c2_1(a1074) ),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
( ~ hskp54
| c0_1(a1074) ),
inference(cnf_transformation,[],[f5]) ).
fof(f104,plain,
( ~ hskp54
| c3_1(a1074) ),
inference(cnf_transformation,[],[f5]) ).
fof(f106,plain,
( ~ hskp53
| c0_1(a1073) ),
inference(cnf_transformation,[],[f5]) ).
fof(f107,plain,
( ~ hskp53
| c2_1(a1073) ),
inference(cnf_transformation,[],[f5]) ).
fof(f108,plain,
( ~ hskp53
| c1_1(a1073) ),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
( ~ hskp49
| c1_1(a1065) ),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
( ~ hskp49
| ~ c2_1(a1065) ),
inference(cnf_transformation,[],[f5]) ).
fof(f124,plain,
( ~ hskp49
| ~ c0_1(a1065) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
( ~ hskp48
| c0_1(a1062) ),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
( ~ hskp48
| c2_1(a1062) ),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( ~ hskp48
| c3_1(a1062) ),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
( ~ hskp47
| c1_1(a1056) ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( ~ hskp47
| c2_1(a1056) ),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
( ~ hskp46
| c0_1(a1053) ),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
( ~ hskp46
| ~ c2_1(a1053) ),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
( ~ hskp46
| ~ c1_1(a1053) ),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
( ~ hskp43
| c1_1(a1049) ),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
( ~ hskp43
| c2_1(a1049) ),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
( ~ hskp43
| c0_1(a1049) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp38
| c2_1(a1040) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp38
| c3_1(a1040) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp38
| c1_1(a1040) ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( ~ hskp37
| c3_1(a1037) ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( ~ hskp37
| c0_1(a1037) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( ~ hskp37
| ~ c1_1(a1037) ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( ~ hskp36
| c1_1(a1034) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( ~ hskp36
| ~ c0_1(a1034) ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( ~ hskp36
| c3_1(a1034) ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( ~ hskp34
| c3_1(a1032) ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( ~ hskp34
| ~ c1_1(a1032) ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( ~ hskp34
| ~ c2_1(a1032) ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( ~ hskp33
| c2_1(a1031) ),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
( ~ hskp33
| ~ c1_1(a1031) ),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
( ~ hskp33
| c3_1(a1031) ),
inference(cnf_transformation,[],[f5]) ).
fof(f190,plain,
( ~ hskp32
| c2_1(a1029) ),
inference(cnf_transformation,[],[f5]) ).
fof(f191,plain,
( ~ hskp32
| c1_1(a1029) ),
inference(cnf_transformation,[],[f5]) ).
fof(f192,plain,
( ~ hskp32
| ~ c0_1(a1029) ),
inference(cnf_transformation,[],[f5]) ).
fof(f206,plain,
( ~ hskp28
| ~ c1_1(a1102) ),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
( ~ hskp28
| c2_1(a1102) ),
inference(cnf_transformation,[],[f5]) ).
fof(f208,plain,
( ~ hskp28
| ~ c0_1(a1102) ),
inference(cnf_transformation,[],[f5]) ).
fof(f210,plain,
( ~ hskp27
| ~ c0_1(a1101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f211,plain,
( ~ hskp27
| c1_1(a1101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f212,plain,
( ~ hskp27
| c3_1(a1101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f218,plain,
( ~ hskp25
| ~ c2_1(a1091) ),
inference(cnf_transformation,[],[f5]) ).
fof(f219,plain,
( ~ hskp25
| ~ c0_1(a1091) ),
inference(cnf_transformation,[],[f5]) ).
fof(f220,plain,
( ~ hskp25
| ~ c3_1(a1091) ),
inference(cnf_transformation,[],[f5]) ).
fof(f222,plain,
( ~ hskp24
| ~ c1_1(a1089) ),
inference(cnf_transformation,[],[f5]) ).
fof(f223,plain,
( ~ hskp24
| c0_1(a1089) ),
inference(cnf_transformation,[],[f5]) ).
fof(f224,plain,
( ~ hskp24
| ~ c2_1(a1089) ),
inference(cnf_transformation,[],[f5]) ).
fof(f226,plain,
( ~ hskp23
| ~ c2_1(a1088) ),
inference(cnf_transformation,[],[f5]) ).
fof(f227,plain,
( ~ hskp23
| c3_1(a1088) ),
inference(cnf_transformation,[],[f5]) ).
fof(f228,plain,
( ~ hskp23
| c1_1(a1088) ),
inference(cnf_transformation,[],[f5]) ).
fof(f230,plain,
( ~ hskp22
| ~ c1_1(a1083) ),
inference(cnf_transformation,[],[f5]) ).
fof(f231,plain,
( ~ hskp22
| c3_1(a1083) ),
inference(cnf_transformation,[],[f5]) ).
fof(f232,plain,
( ~ hskp22
| c2_1(a1083) ),
inference(cnf_transformation,[],[f5]) ).
fof(f234,plain,
( ~ hskp21
| ~ c0_1(a1082) ),
inference(cnf_transformation,[],[f5]) ).
fof(f235,plain,
( ~ hskp21
| ~ c2_1(a1082) ),
inference(cnf_transformation,[],[f5]) ).
fof(f236,plain,
( ~ hskp21
| ~ c3_1(a1082) ),
inference(cnf_transformation,[],[f5]) ).
fof(f238,plain,
( ~ hskp20
| ~ c1_1(a1080) ),
inference(cnf_transformation,[],[f5]) ).
fof(f239,plain,
( ~ hskp20
| ~ c2_1(a1080) ),
inference(cnf_transformation,[],[f5]) ).
fof(f240,plain,
( ~ hskp20
| ~ c0_1(a1080) ),
inference(cnf_transformation,[],[f5]) ).
fof(f242,plain,
( ~ hskp19
| ~ c2_1(a1079) ),
inference(cnf_transformation,[],[f5]) ).
fof(f243,plain,
( ~ hskp19
| ~ c0_1(a1079) ),
inference(cnf_transformation,[],[f5]) ).
fof(f244,plain,
( ~ hskp19
| c1_1(a1079) ),
inference(cnf_transformation,[],[f5]) ).
fof(f258,plain,
( ~ hskp15
| ~ c1_1(a1059) ),
inference(cnf_transformation,[],[f5]) ).
fof(f259,plain,
( ~ hskp15
| c2_1(a1059) ),
inference(cnf_transformation,[],[f5]) ).
fof(f260,plain,
( ~ hskp15
| c3_1(a1059) ),
inference(cnf_transformation,[],[f5]) ).
fof(f262,plain,
( ~ hskp14
| ~ c2_1(a1055) ),
inference(cnf_transformation,[],[f5]) ).
fof(f263,plain,
( ~ hskp14
| ~ c1_1(a1055) ),
inference(cnf_transformation,[],[f5]) ).
fof(f264,plain,
( ~ hskp14
| ~ c0_1(a1055) ),
inference(cnf_transformation,[],[f5]) ).
fof(f270,plain,
( ~ hskp12
| ~ c3_1(a1043) ),
inference(cnf_transformation,[],[f5]) ).
fof(f271,plain,
( ~ hskp12
| c0_1(a1043) ),
inference(cnf_transformation,[],[f5]) ).
fof(f272,plain,
( ~ hskp12
| ~ c1_1(a1043) ),
inference(cnf_transformation,[],[f5]) ).
fof(f278,plain,
( ~ hskp10
| ~ c0_1(a1039) ),
inference(cnf_transformation,[],[f5]) ).
fof(f279,plain,
( ~ hskp10
| ~ c2_1(a1039) ),
inference(cnf_transformation,[],[f5]) ).
fof(f280,plain,
( ~ hskp10
| c1_1(a1039) ),
inference(cnf_transformation,[],[f5]) ).
fof(f286,plain,
( ~ hskp8
| ~ c1_1(a1036) ),
inference(cnf_transformation,[],[f5]) ).
fof(f287,plain,
( ~ hskp8
| ~ c3_1(a1036) ),
inference(cnf_transformation,[],[f5]) ).
fof(f288,plain,
( ~ hskp8
| c0_1(a1036) ),
inference(cnf_transformation,[],[f5]) ).
fof(f294,plain,
( ~ hskp6
| ~ c0_1(a1030) ),
inference(cnf_transformation,[],[f5]) ).
fof(f295,plain,
( ~ hskp6
| ~ c3_1(a1030) ),
inference(cnf_transformation,[],[f5]) ).
fof(f296,plain,
( ~ hskp6
| ~ c2_1(a1030) ),
inference(cnf_transformation,[],[f5]) ).
fof(f325,plain,
! [X83,X84,X85] :
( ~ c1_1(X83)
| ~ c0_1(X83)
| ~ c2_1(X83)
| ~ ndr1_0
| ~ c2_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84)
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ c2_1(X85) ),
inference(duplicate_literal_removal,[],[f12]) ).
fof(f326,plain,
! [X82,X80,X81] :
( c0_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0
| c3_1(X81)
| c1_1(X81)
| ~ c2_1(X81)
| c0_1(X82)
| c1_1(X82)
| c2_1(X82) ),
inference(duplicate_literal_removal,[],[f13]) ).
fof(f328,plain,
! [X76,X75] :
( c2_1(X75)
| ~ c1_1(X75)
| c0_1(X75)
| ~ ndr1_0
| hskp25
| ~ c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ),
inference(duplicate_literal_removal,[],[f16]) ).
fof(f330,plain,
! [X72,X71] :
( c0_1(X71)
| ~ c1_1(X71)
| ~ c3_1(X71)
| ~ ndr1_0
| c1_1(X72)
| c0_1(X72)
| c3_1(X72)
| hskp24 ),
inference(duplicate_literal_removal,[],[f18]) ).
fof(f332,plain,
! [X66,X67] :
( ~ c0_1(X66)
| ~ c3_1(X66)
| c2_1(X66)
| ~ ndr1_0
| ~ c2_1(X67)
| ~ c3_1(X67)
| c1_1(X67)
| hskp57 ),
inference(duplicate_literal_removal,[],[f21]) ).
fof(f333,plain,
! [X65,X63,X64] :
( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63)
| ~ ndr1_0
| c0_1(X64)
| c3_1(X64)
| c1_1(X64)
| c3_1(X65)
| ~ c1_1(X65)
| c2_1(X65) ),
inference(duplicate_literal_removal,[],[f22]) ).
fof(f334,plain,
! [X58,X59,X57] :
( ~ c2_1(X57)
| ~ c1_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0
| c3_1(X58)
| ~ c0_1(X58)
| c1_1(X58)
| ~ c0_1(X59)
| ~ c1_1(X59)
| c3_1(X59) ),
inference(duplicate_literal_removal,[],[f27]) ).
fof(f335,plain,
! [X54,X55] :
( ~ c2_1(X54)
| ~ c3_1(X54)
| ~ c0_1(X54)
| ~ ndr1_0
| hskp53
| ~ c3_1(X55)
| c1_1(X55)
| ~ c2_1(X55) ),
inference(duplicate_literal_removal,[],[f29]) ).
fof(f336,plain,
! [X50,X51,X52] :
( ~ c2_1(X50)
| c0_1(X50)
| c1_1(X50)
| ~ ndr1_0
| ~ c0_1(X51)
| c3_1(X51)
| c1_1(X51)
| c3_1(X52)
| c1_1(X52)
| c2_1(X52) ),
inference(duplicate_literal_removal,[],[f31]) ).
fof(f337,plain,
! [X46,X47,X45] :
( c1_1(X45)
| c3_1(X45)
| c0_1(X45)
| ~ ndr1_0
| c0_1(X46)
| ~ c2_1(X46)
| c1_1(X46)
| c3_1(X47)
| c1_1(X47)
| ~ c2_1(X47) ),
inference(duplicate_literal_removal,[],[f34]) ).
fof(f339,plain,
! [X41,X42] :
( ~ c3_1(X41)
| c2_1(X41)
| ~ c0_1(X41)
| ~ ndr1_0
| c3_1(X42)
| c1_1(X42)
| c0_1(X42)
| hskp49 ),
inference(duplicate_literal_removal,[],[f36]) ).
fof(f344,plain,
! [X24,X25] :
( hskp12
| ~ c2_1(X24)
| ~ c1_1(X24)
| ~ c0_1(X24)
| ~ ndr1_0
| ~ c3_1(X25)
| c2_1(X25)
| ~ c0_1(X25) ),
inference(duplicate_literal_removal,[],[f49]) ).
fof(f345,plain,
! [X21,X22] :
( ~ c3_1(X21)
| c2_1(X21)
| ~ c0_1(X21)
| ~ ndr1_0
| hskp38
| ~ c0_1(X22)
| ~ c3_1(X22)
| c1_1(X22) ),
inference(duplicate_literal_removal,[],[f51]) ).
fof(f348,plain,
! [X12,X13] :
( c2_1(X12)
| ~ c1_1(X12)
| c3_1(X12)
| ~ ndr1_0
| c3_1(X13)
| c1_1(X13)
| ~ c0_1(X13)
| hskp34 ),
inference(duplicate_literal_removal,[],[f57]) ).
fof(f349,plain,
! [X10,X11] :
( hskp33
| ~ c1_1(X10)
| c2_1(X10)
| c0_1(X10)
| ~ ndr1_0
| ~ c1_1(X11)
| ~ c3_1(X11)
| ~ c2_1(X11) ),
inference(duplicate_literal_removal,[],[f58]) ).
fof(f355,definition,
( spl0_1
<=> hskp63 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f358,definition,
( spl0_2
<=> hskp56 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f361,definition,
( spl0_3
<=> hskp62 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f363,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f6,f361,f358,f355]) ).
fof(f365,definition,
( spl0_4
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f368,definition,
( spl0_5
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f371,definition,
( spl0_6
<=> hskp43 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f373,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f7,f371,f368,f365]) ).
fof(f378,definition,
( spl0_8
<=> ! [X92] :
( ~ c1_1(X92)
| c2_1(X92)
| c3_1(X92) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f379,plain,
( ! [X92] :
( c3_1(X92)
| c2_1(X92)
| ~ c1_1(X92) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f381,definition,
( spl0_9
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f384,definition,
( spl0_10
<=> ! [X91] :
( ~ c3_1(X91)
| c0_1(X91)
| ~ c1_1(X91) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f385,plain,
( ! [X91] :
( ~ c3_1(X91)
| c0_1(X91)
| ~ c1_1(X91) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f394,definition,
( spl0_13
<=> ! [X90] :
( ~ c0_1(X90)
| c2_1(X90)
| c1_1(X90) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f395,plain,
( ! [X90] :
( c1_1(X90)
| c2_1(X90)
| ~ c0_1(X90) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f401,definition,
( spl0_15
<=> ! [X88] :
( ~ c2_1(X88)
| c0_1(X88)
| ~ c3_1(X88) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f402,plain,
( ! [X88] :
( ~ c3_1(X88)
| c0_1(X88)
| ~ c2_1(X88) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f401]) ).
fof(f405,definition,
( spl0_16
<=> ! [X87] :
( ~ c3_1(X87)
| c2_1(X87)
| c0_1(X87) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f406,plain,
( ! [X87] :
( ~ c3_1(X87)
| c2_1(X87)
| c0_1(X87) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f411,definition,
( spl0_18
<=> ! [X86] :
( ~ c3_1(X86)
| ~ c1_1(X86)
| c2_1(X86) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f412,plain,
( ! [X86] :
( ~ c3_1(X86)
| ~ c1_1(X86)
| c2_1(X86) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f415,definition,
( spl0_19
<=> ! [X85] :
( ~ c0_1(X85)
| ~ c2_1(X85)
| ~ c1_1(X85) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f416,plain,
( ! [X85] :
( ~ c1_1(X85)
| ~ c2_1(X85)
| ~ c0_1(X85) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f415]) ).
fof(f418,definition,
( spl0_20
<=> ! [X84] :
( ~ c2_1(X84)
| ~ c3_1(X84)
| ~ c0_1(X84) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f419,plain,
( ! [X84] :
( ~ c3_1(X84)
| ~ c2_1(X84)
| ~ c0_1(X84) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( spl0_19
| spl0_20
| ~ spl0_9
| spl0_19 ),
inference(avatar_split_clause,[],[f325,f415,f381,f418,f415]) ).
fof(f422,definition,
( spl0_21
<=> ! [X82] :
( c0_1(X82)
| c2_1(X82)
| c1_1(X82) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f423,plain,
( ! [X82] :
( c1_1(X82)
| c2_1(X82)
| c0_1(X82) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f425,definition,
( spl0_22
<=> ! [X81] :
( c3_1(X81)
| ~ c2_1(X81)
| c1_1(X81) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f426,plain,
( ! [X81] :
( c3_1(X81)
| ~ c2_1(X81)
| c1_1(X81) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f425]) ).
fof(f427,plain,
( spl0_21
| spl0_22
| ~ spl0_9
| spl0_15 ),
inference(avatar_split_clause,[],[f326,f401,f381,f425,f422]) ).
fof(f429,definition,
( spl0_23
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f432,definition,
( spl0_24
<=> hskp48 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f440,definition,
( spl0_26
<=> ! [X76] :
( ~ c2_1(X76)
| ~ c3_1(X76)
| ~ c1_1(X76) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f441,plain,
( ! [X76] :
( ~ c3_1(X76)
| ~ c2_1(X76)
| ~ c1_1(X76) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f443,definition,
( spl0_27
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f446,definition,
( spl0_28
<=> ! [X75] :
( c2_1(X75)
| c0_1(X75)
| ~ c1_1(X75) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f447,plain,
( ! [X75] :
( ~ c1_1(X75)
| c0_1(X75)
| c2_1(X75) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f446]) ).
fof(f448,plain,
( spl0_26
| spl0_27
| ~ spl0_9
| spl0_28 ),
inference(avatar_split_clause,[],[f328,f446,f381,f443,f440]) ).
fof(f450,definition,
( spl0_29
<=> hskp36 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f454,definition,
( spl0_30
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f457,definition,
( spl0_31
<=> ! [X72] :
( c1_1(X72)
| c3_1(X72)
| c0_1(X72) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f458,plain,
( ! [X72] :
( c3_1(X72)
| c1_1(X72)
| c0_1(X72) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f457]) ).
fof(f459,plain,
( spl0_30
| spl0_31
| ~ spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f330,f384,f381,f457,f454]) ).
fof(f461,definition,
( spl0_32
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f464,definition,
( spl0_33
<=> hskp33 ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f466,plain,
( ~ spl0_9
| spl0_20
| spl0_32
| spl0_33 ),
inference(avatar_split_clause,[],[f19,f464,f461,f418,f381]) ).
fof(f475,definition,
( spl0_36
<=> hskp57 ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f478,definition,
( spl0_37
<=> ! [X67] :
( ~ c2_1(X67)
| c1_1(X67)
| ~ c3_1(X67) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f479,plain,
( ! [X67] :
( ~ c3_1(X67)
| c1_1(X67)
| ~ c2_1(X67) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f481,definition,
( spl0_38
<=> ! [X66] :
( ~ c0_1(X66)
| c2_1(X66)
| ~ c3_1(X66) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f482,plain,
( ! [X66] :
( ~ c3_1(X66)
| c2_1(X66)
| ~ c0_1(X66) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f481]) ).
fof(f483,plain,
( spl0_36
| spl0_37
| ~ spl0_9
| spl0_38 ),
inference(avatar_split_clause,[],[f332,f481,f381,f478,f475]) ).
fof(f484,plain,
( spl0_8
| spl0_31
| ~ spl0_9
| spl0_28 ),
inference(avatar_split_clause,[],[f333,f446,f381,f457,f378]) ).
fof(f486,definition,
( spl0_39
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f488,plain,
( spl0_2
| ~ spl0_9
| spl0_18
| spl0_39 ),
inference(avatar_split_clause,[],[f23,f486,f411,f381,f358]) ).
fof(f490,definition,
( spl0_40
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f493,definition,
( spl0_41
<=> hskp55 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f495,plain,
( spl0_40
| ~ spl0_9
| spl0_13
| spl0_41 ),
inference(avatar_split_clause,[],[f24,f493,f394,f381,f490]) ).
fof(f497,definition,
( spl0_42
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f500,definition,
( spl0_43
<=> ! [X60] :
( c1_1(X60)
| c3_1(X60)
| ~ c0_1(X60) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f501,plain,
( ! [X60] :
( c3_1(X60)
| c1_1(X60)
| ~ c0_1(X60) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f503,definition,
( spl0_44
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f505,plain,
( spl0_42
| ~ spl0_9
| spl0_43
| spl0_44 ),
inference(avatar_split_clause,[],[f25,f503,f500,f381,f497]) ).
fof(f517,definition,
( spl0_48
<=> ! [X59] :
( ~ c0_1(X59)
| c3_1(X59)
| ~ c1_1(X59) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f518,plain,
( ! [X59] :
( c3_1(X59)
| ~ c0_1(X59)
| ~ c1_1(X59) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f519,plain,
( spl0_48
| spl0_43
| ~ spl0_9
| spl0_26 ),
inference(avatar_split_clause,[],[f334,f440,f381,f500,f517]) ).
fof(f521,definition,
( spl0_49
<=> hskp47 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f524,definition,
( spl0_50
<=> hskp54 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f526,plain,
( ~ spl0_9
| spl0_26
| spl0_49
| spl0_50 ),
inference(avatar_split_clause,[],[f28,f524,f521,f440,f381]) ).
fof(f528,definition,
( spl0_51
<=> hskp53 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f530,plain,
( spl0_37
| spl0_51
| ~ spl0_9
| spl0_20 ),
inference(avatar_split_clause,[],[f335,f418,f381,f528,f478]) ).
fof(f532,definition,
( spl0_52
<=> ! [X53] :
( ~ c3_1(X53)
| ~ c0_1(X53)
| c1_1(X53) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f533,plain,
( ! [X53] :
( ~ c3_1(X53)
| ~ c0_1(X53)
| c1_1(X53) )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f535,definition,
( spl0_53
<=> hskp34 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f542,definition,
( spl0_55
<=> ! [X52] :
( c3_1(X52)
| c2_1(X52)
| c1_1(X52) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f543,plain,
( ! [X52] :
( c3_1(X52)
| c2_1(X52)
| c1_1(X52) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f545,definition,
( spl0_56
<=> ! [X50] :
( ~ c2_1(X50)
| c1_1(X50)
| c0_1(X50) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f546,plain,
( ! [X50] :
( c1_1(X50)
| ~ c2_1(X50)
| c0_1(X50) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( spl0_55
| spl0_43
| ~ spl0_9
| spl0_56 ),
inference(avatar_split_clause,[],[f336,f545,f381,f500,f542]) ).
fof(f552,definition,
( spl0_58
<=> ! [X49] :
( c0_1(X49)
| ~ c1_1(X49)
| ~ c2_1(X49) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f553,plain,
( ! [X49] :
( ~ c1_1(X49)
| c0_1(X49)
| ~ c2_1(X49) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f556,definition,
( spl0_59
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f565,plain,
( spl0_22
| spl0_56
| ~ spl0_9
| spl0_31 ),
inference(avatar_split_clause,[],[f337,f457,f381,f545,f425]) ).
fof(f570,definition,
( spl0_63
<=> ! [X43] :
( c3_1(X43)
| c0_1(X43)
| c2_1(X43) ) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f571,plain,
( ! [X43] :
( c3_1(X43)
| c0_1(X43)
| c2_1(X43) )
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f574,definition,
( spl0_64
<=> hskp49 ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f576,plain,
( spl0_64
| spl0_31
| ~ spl0_9
| spl0_38 ),
inference(avatar_split_clause,[],[f339,f481,f381,f457,f574]) ).
fof(f585,definition,
( spl0_67
<=> ! [X39] :
( c0_1(X39)
| c3_1(X39)
| ~ c1_1(X39) ) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f586,plain,
( ! [X39] :
( c3_1(X39)
| c0_1(X39)
| ~ c1_1(X39) )
| ~ spl0_67 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f587,plain,
( spl0_24
| spl0_29
| ~ spl0_9
| spl0_67 ),
inference(avatar_split_clause,[],[f38,f585,f381,f450,f432]) ).
fof(f589,definition,
( spl0_68
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f591,plain,
( spl0_33
| spl0_68
| ~ spl0_9
| spl0_16 ),
inference(avatar_split_clause,[],[f39,f405,f381,f589,f464]) ).
fof(f593,definition,
( spl0_69
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f595,plain,
( spl0_6
| ~ spl0_9
| spl0_58
| spl0_69 ),
inference(avatar_split_clause,[],[f40,f593,f552,f381,f371]) ).
fof(f604,definition,
( spl0_72
<=> hskp38 ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f607,definition,
( spl0_73
<=> hskp46 ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f609,plain,
( spl0_23
| spl0_72
| spl0_73 ),
inference(avatar_split_clause,[],[f42,f607,f604,f429]) ).
fof(f637,plain,
( spl0_38
| ~ spl0_9
| spl0_19
| spl0_59 ),
inference(avatar_split_clause,[],[f344,f556,f415,f381,f481]) ).
fof(f645,plain,
( spl0_52
| spl0_72
| ~ spl0_9
| spl0_38 ),
inference(avatar_split_clause,[],[f345,f481,f381,f604,f532]) ).
fof(f646,plain,
( spl0_69
| ~ spl0_9
| spl0_63 ),
inference(avatar_split_clause,[],[f52,f570,f381,f593]) ).
fof(f655,definition,
( spl0_85
<=> hskp37 ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f658,definition,
( spl0_86
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f660,plain,
( spl0_85
| spl0_86
| ~ spl0_9
| spl0_10 ),
inference(avatar_split_clause,[],[f54,f384,f381,f658,f655]) ).
fof(f663,plain,
( spl0_53
| spl0_43
| ~ spl0_9
| spl0_8 ),
inference(avatar_split_clause,[],[f348,f378,f381,f500,f535]) ).
fof(f664,plain,
( spl0_26
| ~ spl0_9
| spl0_28
| spl0_33 ),
inference(avatar_split_clause,[],[f349,f464,f446,f381,f440]) ).
fof(f666,definition,
( spl0_87
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f669,definition,
( spl0_88
<=> hskp32 ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f671,plain,
( spl0_87
| spl0_88
| ~ spl0_9
| spl0_48 ),
inference(avatar_split_clause,[],[f59,f517,f381,f669,f666]) ).
fof(f700,definition,
( spl0_96
<=> c3_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f701,plain,
( c3_1(a1105)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f700]) ).
fof(f703,plain,
( spl0_96
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f66,f355,f700]) ).
fof(f705,definition,
( spl0_97
<=> c1_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f706,plain,
( c1_1(a1105)
| ~ spl0_97 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f707,plain,
( spl0_97
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f67,f355,f705]) ).
fof(f709,definition,
( spl0_98
<=> c2_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f711,plain,
( ~ spl0_98
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f68,f355,f709]) ).
fof(f713,plain,
( spl0_9
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f69,f355,f381]) ).
fof(f715,definition,
( spl0_99
<=> c1_1(a1103) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f716,plain,
( c1_1(a1103)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f718,plain,
( spl0_99
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f70,f361,f715]) ).
fof(f720,definition,
( spl0_100
<=> c3_1(a1103) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f721,plain,
( c3_1(a1103)
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f720]) ).
fof(f722,plain,
( spl0_100
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f71,f361,f720]) ).
fof(f724,definition,
( spl0_101
<=> c2_1(a1103) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f726,plain,
( spl0_101
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f72,f361,f724]) ).
fof(f727,plain,
( spl0_9
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f73,f361,f381]) ).
fof(f785,definition,
( spl0_114
<=> c3_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f786,plain,
( c3_1(a1085)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f788,plain,
( spl0_114
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f90,f475,f785]) ).
fof(f790,definition,
( spl0_115
<=> c0_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f792,plain,
( spl0_115
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f91,f475,f790]) ).
fof(f794,definition,
( spl0_116
<=> c2_1(a1085) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f796,plain,
( spl0_116
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f92,f475,f794]) ).
fof(f799,definition,
( spl0_117
<=> c0_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f802,plain,
( spl0_117
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f94,f358,f799]) ).
fof(f804,definition,
( spl0_118
<=> c1_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f805,plain,
( ~ c1_1(a1084)
| spl0_118 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f806,plain,
( ~ spl0_118
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f95,f358,f804]) ).
fof(f808,definition,
( spl0_119
<=> c3_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f809,plain,
( ~ c3_1(a1084)
| spl0_119 ),
inference(avatar_component_clause,[],[f808]) ).
fof(f810,plain,
( ~ spl0_119
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f96,f358,f808]) ).
fof(f811,plain,
( spl0_9
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f97,f358,f381]) ).
fof(f813,definition,
( spl0_120
<=> c3_1(a1081) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f814,plain,
( c3_1(a1081)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f816,plain,
( spl0_120
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f98,f493,f813]) ).
fof(f818,definition,
( spl0_121
<=> c0_1(a1081) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f820,plain,
( ~ spl0_121
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f99,f493,f818]) ).
fof(f822,definition,
( spl0_122
<=> c1_1(a1081) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f823,plain,
( c1_1(a1081)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f822]) ).
fof(f824,plain,
( spl0_122
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f100,f493,f822]) ).
fof(f827,definition,
( spl0_123
<=> c2_1(a1074) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f830,plain,
( spl0_123
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f102,f524,f827]) ).
fof(f832,definition,
( spl0_124
<=> c0_1(a1074) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f834,plain,
( spl0_124
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f103,f524,f832]) ).
fof(f836,definition,
( spl0_125
<=> c3_1(a1074) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f837,plain,
( c3_1(a1074)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f838,plain,
( spl0_125
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f104,f524,f836]) ).
fof(f841,definition,
( spl0_126
<=> c0_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f844,plain,
( spl0_126
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f106,f528,f841]) ).
fof(f846,definition,
( spl0_127
<=> c2_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f848,plain,
( spl0_127
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f107,f528,f846]) ).
fof(f850,definition,
( spl0_128
<=> c1_1(a1073) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f851,plain,
( c1_1(a1073)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f850]) ).
fof(f852,plain,
( spl0_128
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f108,f528,f850]) ).
fof(f897,definition,
( spl0_138
<=> c1_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f898,plain,
( c1_1(a1065)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f900,plain,
( spl0_138
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f122,f574,f897]) ).
fof(f902,definition,
( spl0_139
<=> c2_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f904,plain,
( ~ spl0_139
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f123,f574,f902]) ).
fof(f906,definition,
( spl0_140
<=> c0_1(a1065) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f908,plain,
( ~ spl0_140
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f124,f574,f906]) ).
fof(f911,definition,
( spl0_141
<=> c0_1(a1062) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f914,plain,
( spl0_141
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f126,f432,f911]) ).
fof(f916,definition,
( spl0_142
<=> c2_1(a1062) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f918,plain,
( spl0_142
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f127,f432,f916]) ).
fof(f920,definition,
( spl0_143
<=> c3_1(a1062) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f921,plain,
( c3_1(a1062)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f920]) ).
fof(f922,plain,
( spl0_143
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f128,f432,f920]) ).
fof(f930,definition,
( spl0_145
<=> c1_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f931,plain,
( c1_1(a1056)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f930]) ).
fof(f932,plain,
( spl0_145
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f131,f521,f930]) ).
fof(f934,definition,
( spl0_146
<=> c2_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f936,plain,
( spl0_146
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f132,f521,f934]) ).
fof(f939,definition,
( spl0_147
<=> c0_1(a1053) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f942,plain,
( spl0_147
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f134,f607,f939]) ).
fof(f944,definition,
( spl0_148
<=> c2_1(a1053) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f946,plain,
( ~ spl0_148
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f135,f607,f944]) ).
fof(f948,definition,
( spl0_149
<=> c1_1(a1053) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f949,plain,
( ~ c1_1(a1053)
| spl0_149 ),
inference(avatar_component_clause,[],[f948]) ).
fof(f950,plain,
( ~ spl0_149
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f136,f607,f948]) ).
fof(f981,definition,
( spl0_156
<=> c1_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f982,plain,
( c1_1(a1049)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f984,plain,
( spl0_156
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f146,f371,f981]) ).
fof(f986,definition,
( spl0_157
<=> c2_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f988,plain,
( spl0_157
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f147,f371,f986]) ).
fof(f990,definition,
( spl0_158
<=> c0_1(a1049) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f992,plain,
( spl0_158
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f148,f371,f990]) ).
fof(f1051,definition,
( spl0_171
<=> c2_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f1054,plain,
( spl0_171
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f166,f604,f1051]) ).
fof(f1056,definition,
( spl0_172
<=> c3_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f1057,plain,
( c3_1(a1040)
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f1056]) ).
fof(f1058,plain,
( spl0_172
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f167,f604,f1056]) ).
fof(f1060,definition,
( spl0_173
<=> c1_1(a1040) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1062,plain,
( spl0_173
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f168,f604,f1060]) ).
fof(f1065,definition,
( spl0_174
<=> c3_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1066,plain,
( c3_1(a1037)
| ~ spl0_174 ),
inference(avatar_component_clause,[],[f1065]) ).
fof(f1068,plain,
( spl0_174
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f170,f655,f1065]) ).
fof(f1070,definition,
( spl0_175
<=> c0_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1072,plain,
( spl0_175
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f171,f655,f1070]) ).
fof(f1074,definition,
( spl0_176
<=> c1_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f1075,plain,
( ~ c1_1(a1037)
| spl0_176 ),
inference(avatar_component_clause,[],[f1074]) ).
fof(f1076,plain,
( ~ spl0_176
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f172,f655,f1074]) ).
fof(f1079,definition,
( spl0_177
<=> c1_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f1082,plain,
( spl0_177
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f174,f450,f1079]) ).
fof(f1084,definition,
( spl0_178
<=> c0_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1086,plain,
( ~ spl0_178
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f175,f450,f1084]) ).
fof(f1088,definition,
( spl0_179
<=> c3_1(a1034) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1089,plain,
( c3_1(a1034)
| ~ spl0_179 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1090,plain,
( spl0_179
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f176,f450,f1088]) ).
fof(f1107,definition,
( spl0_183
<=> c3_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1108,plain,
( c3_1(a1032)
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1107]) ).
fof(f1110,plain,
( spl0_183
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f182,f535,f1107]) ).
fof(f1112,definition,
( spl0_184
<=> c1_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1113,plain,
( ~ c1_1(a1032)
| spl0_184 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1114,plain,
( ~ spl0_184
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f183,f535,f1112]) ).
fof(f1116,definition,
( spl0_185
<=> c2_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_185])],[avatar_definition]) ).
fof(f1118,plain,
( ~ spl0_185
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f184,f535,f1116]) ).
fof(f1121,definition,
( spl0_186
<=> c2_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f1124,plain,
( spl0_186
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f186,f464,f1121]) ).
fof(f1126,definition,
( spl0_187
<=> c1_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f1127,plain,
( ~ c1_1(a1031)
| spl0_187 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1128,plain,
( ~ spl0_187
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f187,f464,f1126]) ).
fof(f1130,definition,
( spl0_188
<=> c3_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f1131,plain,
( c3_1(a1031)
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f1130]) ).
fof(f1132,plain,
( spl0_188
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f188,f464,f1130]) ).
fof(f1135,definition,
( spl0_189
<=> c2_1(a1029) ),
introduced(definition,[new_symbols(definition,[spl0_189])],[avatar_definition]) ).
fof(f1138,plain,
( spl0_189
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f190,f669,f1135]) ).
fof(f1140,definition,
( spl0_190
<=> c1_1(a1029) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f1141,plain,
( c1_1(a1029)
| ~ spl0_190 ),
inference(avatar_component_clause,[],[f1140]) ).
fof(f1142,plain,
( spl0_190
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f191,f669,f1140]) ).
fof(f1144,definition,
( spl0_191
<=> c0_1(a1029) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1146,plain,
( ~ spl0_191
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f192,f669,f1144]) ).
fof(f1191,definition,
( spl0_201
<=> c1_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_201])],[avatar_definition]) ).
fof(f1192,plain,
( ~ c1_1(a1102)
| spl0_201 ),
inference(avatar_component_clause,[],[f1191]) ).
fof(f1194,plain,
( ~ spl0_201
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f206,f365,f1191]) ).
fof(f1196,definition,
( spl0_202
<=> c2_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_202])],[avatar_definition]) ).
fof(f1198,plain,
( spl0_202
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f207,f365,f1196]) ).
fof(f1200,definition,
( spl0_203
<=> c0_1(a1102) ),
introduced(definition,[new_symbols(definition,[spl0_203])],[avatar_definition]) ).
fof(f1202,plain,
( ~ spl0_203
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f208,f365,f1200]) ).
fof(f1205,definition,
( spl0_204
<=> c0_1(a1101) ),
introduced(definition,[new_symbols(definition,[spl0_204])],[avatar_definition]) ).
fof(f1208,plain,
( ~ spl0_204
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f210,f368,f1205]) ).
fof(f1210,definition,
( spl0_205
<=> c1_1(a1101) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f1212,plain,
( spl0_205
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f211,f368,f1210]) ).
fof(f1214,definition,
( spl0_206
<=> c3_1(a1101) ),
introduced(definition,[new_symbols(definition,[spl0_206])],[avatar_definition]) ).
fof(f1215,plain,
( c3_1(a1101)
| ~ spl0_206 ),
inference(avatar_component_clause,[],[f1214]) ).
fof(f1216,plain,
( spl0_206
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f212,f368,f1214]) ).
fof(f1233,definition,
( spl0_210
<=> c2_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f1236,plain,
( ~ spl0_210
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f218,f443,f1233]) ).
fof(f1238,definition,
( spl0_211
<=> c0_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_211])],[avatar_definition]) ).
fof(f1240,plain,
( ~ spl0_211
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f219,f443,f1238]) ).
fof(f1242,definition,
( spl0_212
<=> c3_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_212])],[avatar_definition]) ).
fof(f1243,plain,
( ~ c3_1(a1091)
| spl0_212 ),
inference(avatar_component_clause,[],[f1242]) ).
fof(f1244,plain,
( ~ spl0_212
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f220,f443,f1242]) ).
fof(f1247,definition,
( spl0_213
<=> c1_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f1248,plain,
( ~ c1_1(a1089)
| spl0_213 ),
inference(avatar_component_clause,[],[f1247]) ).
fof(f1250,plain,
( ~ spl0_213
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f222,f454,f1247]) ).
fof(f1252,definition,
( spl0_214
<=> c0_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1254,plain,
( spl0_214
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f223,f454,f1252]) ).
fof(f1256,definition,
( spl0_215
<=> c2_1(a1089) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1258,plain,
( ~ spl0_215
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f224,f454,f1256]) ).
fof(f1261,definition,
( spl0_216
<=> c2_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1264,plain,
( ~ spl0_216
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f226,f461,f1261]) ).
fof(f1266,definition,
( spl0_217
<=> c3_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_217])],[avatar_definition]) ).
fof(f1267,plain,
( c3_1(a1088)
| ~ spl0_217 ),
inference(avatar_component_clause,[],[f1266]) ).
fof(f1268,plain,
( spl0_217
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f227,f461,f1266]) ).
fof(f1270,definition,
( spl0_218
<=> c1_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_218])],[avatar_definition]) ).
fof(f1271,plain,
( c1_1(a1088)
| ~ spl0_218 ),
inference(avatar_component_clause,[],[f1270]) ).
fof(f1272,plain,
( spl0_218
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f228,f461,f1270]) ).
fof(f1275,definition,
( spl0_219
<=> c1_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_219])],[avatar_definition]) ).
fof(f1276,plain,
( ~ c1_1(a1083)
| spl0_219 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1278,plain,
( ~ spl0_219
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f230,f486,f1275]) ).
fof(f1280,definition,
( spl0_220
<=> c3_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_220])],[avatar_definition]) ).
fof(f1281,plain,
( c3_1(a1083)
| ~ spl0_220 ),
inference(avatar_component_clause,[],[f1280]) ).
fof(f1282,plain,
( spl0_220
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f231,f486,f1280]) ).
fof(f1284,definition,
( spl0_221
<=> c2_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_221])],[avatar_definition]) ).
fof(f1286,plain,
( spl0_221
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f232,f486,f1284]) ).
fof(f1289,definition,
( spl0_222
<=> c0_1(a1082) ),
introduced(definition,[new_symbols(definition,[spl0_222])],[avatar_definition]) ).
fof(f1292,plain,
( ~ spl0_222
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f234,f490,f1289]) ).
fof(f1294,definition,
( spl0_223
<=> c2_1(a1082) ),
introduced(definition,[new_symbols(definition,[spl0_223])],[avatar_definition]) ).
fof(f1296,plain,
( ~ spl0_223
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f235,f490,f1294]) ).
fof(f1298,definition,
( spl0_224
<=> c3_1(a1082) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f1299,plain,
( ~ c3_1(a1082)
| spl0_224 ),
inference(avatar_component_clause,[],[f1298]) ).
fof(f1300,plain,
( ~ spl0_224
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f236,f490,f1298]) ).
fof(f1303,definition,
( spl0_225
<=> c1_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_225])],[avatar_definition]) ).
fof(f1304,plain,
( ~ c1_1(a1080)
| spl0_225 ),
inference(avatar_component_clause,[],[f1303]) ).
fof(f1306,plain,
( ~ spl0_225
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f238,f497,f1303]) ).
fof(f1308,definition,
( spl0_226
<=> c2_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_226])],[avatar_definition]) ).
fof(f1310,plain,
( ~ spl0_226
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f239,f497,f1308]) ).
fof(f1312,definition,
( spl0_227
<=> c0_1(a1080) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f1314,plain,
( ~ spl0_227
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f240,f497,f1312]) ).
fof(f1317,definition,
( spl0_228
<=> c2_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f1320,plain,
( ~ spl0_228
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f242,f503,f1317]) ).
fof(f1322,definition,
( spl0_229
<=> c0_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_229])],[avatar_definition]) ).
fof(f1324,plain,
( ~ spl0_229
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f243,f503,f1322]) ).
fof(f1326,definition,
( spl0_230
<=> c1_1(a1079) ),
introduced(definition,[new_symbols(definition,[spl0_230])],[avatar_definition]) ).
fof(f1327,plain,
( c1_1(a1079)
| ~ spl0_230 ),
inference(avatar_component_clause,[],[f1326]) ).
fof(f1328,plain,
( spl0_230
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f244,f503,f1326]) ).
fof(f1373,definition,
( spl0_240
<=> c1_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_240])],[avatar_definition]) ).
fof(f1374,plain,
( ~ c1_1(a1059)
| spl0_240 ),
inference(avatar_component_clause,[],[f1373]) ).
fof(f1376,plain,
( ~ spl0_240
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f258,f589,f1373]) ).
fof(f1378,definition,
( spl0_241
<=> c2_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_241])],[avatar_definition]) ).
fof(f1380,plain,
( spl0_241
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f259,f589,f1378]) ).
fof(f1382,definition,
( spl0_242
<=> c3_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f1383,plain,
( c3_1(a1059)
| ~ spl0_242 ),
inference(avatar_component_clause,[],[f1382]) ).
fof(f1384,plain,
( spl0_242
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f260,f589,f1382]) ).
fof(f1387,definition,
( spl0_243
<=> c2_1(a1055) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f1390,plain,
( ~ spl0_243
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f262,f429,f1387]) ).
fof(f1392,definition,
( spl0_244
<=> c1_1(a1055) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f1393,plain,
( ~ c1_1(a1055)
| spl0_244 ),
inference(avatar_component_clause,[],[f1392]) ).
fof(f1394,plain,
( ~ spl0_244
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f263,f429,f1392]) ).
fof(f1396,definition,
( spl0_245
<=> c0_1(a1055) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f1398,plain,
( ~ spl0_245
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f264,f429,f1396]) ).
fof(f1415,definition,
( spl0_249
<=> c3_1(a1043) ),
introduced(definition,[new_symbols(definition,[spl0_249])],[avatar_definition]) ).
fof(f1416,plain,
( ~ c3_1(a1043)
| spl0_249 ),
inference(avatar_component_clause,[],[f1415]) ).
fof(f1418,plain,
( ~ spl0_249
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f270,f556,f1415]) ).
fof(f1420,definition,
( spl0_250
<=> c0_1(a1043) ),
introduced(definition,[new_symbols(definition,[spl0_250])],[avatar_definition]) ).
fof(f1422,plain,
( spl0_250
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f271,f556,f1420]) ).
fof(f1424,definition,
( spl0_251
<=> c1_1(a1043) ),
introduced(definition,[new_symbols(definition,[spl0_251])],[avatar_definition]) ).
fof(f1426,plain,
( ~ spl0_251
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f272,f556,f1424]) ).
fof(f1443,definition,
( spl0_255
<=> c0_1(a1039) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f1446,plain,
( ~ spl0_255
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f278,f593,f1443]) ).
fof(f1448,definition,
( spl0_256
<=> c2_1(a1039) ),
introduced(definition,[new_symbols(definition,[spl0_256])],[avatar_definition]) ).
fof(f1450,plain,
( ~ spl0_256
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f279,f593,f1448]) ).
fof(f1452,definition,
( spl0_257
<=> c1_1(a1039) ),
introduced(definition,[new_symbols(definition,[spl0_257])],[avatar_definition]) ).
fof(f1453,plain,
( c1_1(a1039)
| ~ spl0_257 ),
inference(avatar_component_clause,[],[f1452]) ).
fof(f1454,plain,
( spl0_257
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f280,f593,f1452]) ).
fof(f1471,definition,
( spl0_261
<=> c1_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_261])],[avatar_definition]) ).
fof(f1474,plain,
( ~ spl0_261
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f286,f658,f1471]) ).
fof(f1476,definition,
( spl0_262
<=> c3_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_262])],[avatar_definition]) ).
fof(f1477,plain,
( ~ c3_1(a1036)
| spl0_262 ),
inference(avatar_component_clause,[],[f1476]) ).
fof(f1478,plain,
( ~ spl0_262
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f287,f658,f1476]) ).
fof(f1480,definition,
( spl0_263
<=> c0_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_263])],[avatar_definition]) ).
fof(f1482,plain,
( spl0_263
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f288,f658,f1480]) ).
fof(f1499,definition,
( spl0_267
<=> c0_1(a1030) ),
introduced(definition,[new_symbols(definition,[spl0_267])],[avatar_definition]) ).
fof(f1502,plain,
( ~ spl0_267
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f294,f666,f1499]) ).
fof(f1504,definition,
( spl0_268
<=> c3_1(a1030) ),
introduced(definition,[new_symbols(definition,[spl0_268])],[avatar_definition]) ).
fof(f1505,plain,
( ~ c3_1(a1030)
| spl0_268 ),
inference(avatar_component_clause,[],[f1504]) ).
fof(f1506,plain,
( ~ spl0_268
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f295,f666,f1504]) ).
fof(f1508,definition,
( spl0_269
<=> c2_1(a1030) ),
introduced(definition,[new_symbols(definition,[spl0_269])],[avatar_definition]) ).
fof(f1510,plain,
( ~ spl0_269
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f296,f666,f1508]) ).
fof(f1596,plain,
( c0_1(a1103)
| ~ c1_1(a1103)
| ~ spl0_10
| ~ spl0_100 ),
inference(resolution,[],[f385,f721]) ).
fof(f1608,definition,
( spl0_289
<=> c0_1(a1103) ),
introduced(definition,[new_symbols(definition,[spl0_289])],[avatar_definition]) ).
fof(f1610,plain,
( ~ spl0_99
| spl0_289
| ~ spl0_10
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f1596,f720,f384,f1608,f715]) ).
fof(f1617,definition,
( spl0_290
<=> c2_1(a1037) ),
introduced(definition,[new_symbols(definition,[spl0_290])],[avatar_definition]) ).
fof(f1626,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_8
| ~ spl0_16 ),
inference(resolution,[],[f406,f379]) ).
fof(f1631,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_8
| ~ spl0_16 ),
inference(duplicate_literal_removal,[],[f1626]) ).
fof(f1634,plain,
( spl0_28
| ~ spl0_8
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f1631,f405,f378,f446]) ).
fof(f1652,plain,
( ~ c2_1(a1049)
| ~ c0_1(a1049)
| ~ spl0_19
| ~ spl0_156 ),
inference(resolution,[],[f416,f982]) ).
fof(f1660,plain,
( ~ spl0_158
| ~ spl0_157
| ~ spl0_19
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f1652,f981,f415,f986,f990]) ).
fof(f1669,plain,
( ~ c2_1(a1037)
| ~ c0_1(a1037)
| ~ spl0_20
| ~ spl0_174 ),
inference(resolution,[],[f419,f1066]) ).
fof(f1675,plain,
( ~ spl0_175
| ~ spl0_290
| ~ spl0_20
| ~ spl0_174 ),
inference(avatar_split_clause,[],[f1669,f1065,f418,f1617,f1070]) ).
fof(f1678,definition,
( spl0_294
<=> c0_1(a1031) ),
introduced(definition,[new_symbols(definition,[spl0_294])],[avatar_definition]) ).
fof(f1695,definition,
( spl0_296
<=> c2_1(a1084) ),
introduced(definition,[new_symbols(definition,[spl0_296])],[avatar_definition]) ).
fof(f1706,plain,
( ~ c2_1(a1103)
| ~ c1_1(a1103)
| ~ spl0_26
| ~ spl0_100 ),
inference(resolution,[],[f441,f721]) ).
fof(f1708,plain,
( ~ spl0_99
| ~ spl0_101
| ~ spl0_26
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f1706,f720,f440,f724,f715]) ).
fof(f1762,plain,
( c1_1(a1031)
| ~ c2_1(a1031)
| ~ spl0_37
| ~ spl0_188 ),
inference(resolution,[],[f479,f1131]) ).
fof(f1765,plain,
( c1_1(a1037)
| ~ c2_1(a1037)
| ~ spl0_37
| ~ spl0_174 ),
inference(resolution,[],[f479,f1066]) ).
fof(f1775,plain,
( ~ spl0_290
| spl0_176
| ~ spl0_37
| ~ spl0_174 ),
inference(avatar_split_clause,[],[f1765,f1065,f478,f1074,f1617]) ).
fof(f1777,plain,
( ~ spl0_186
| spl0_187
| ~ spl0_37
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f1762,f1130,f478,f1126,f1121]) ).
fof(f1784,plain,
( c2_1(a1037)
| ~ c0_1(a1037)
| ~ spl0_38
| ~ spl0_174 ),
inference(resolution,[],[f482,f1066]) ).
fof(f1789,plain,
( ~ spl0_175
| spl0_290
| ~ spl0_38
| ~ spl0_174 ),
inference(avatar_split_clause,[],[f1784,f1065,f481,f1617,f1070]) ).
fof(f1807,plain,
( ~ c2_1(a1081)
| ~ c1_1(a1081)
| ~ spl0_26
| ~ spl0_120 ),
inference(resolution,[],[f814,f441]) ).
fof(f1810,definition,
( spl0_301
<=> c2_1(a1081) ),
introduced(definition,[new_symbols(definition,[spl0_301])],[avatar_definition]) ).
fof(f1814,plain,
( ~ spl0_122
| ~ spl0_301
| ~ spl0_26
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1807,f813,f440,f1810,f822]) ).
fof(f1827,plain,
( ~ c2_1(a1059)
| ~ c0_1(a1059)
| ~ spl0_20
| ~ spl0_242 ),
inference(resolution,[],[f1383,f419]) ).
fof(f1829,definition,
( spl0_302
<=> c0_1(a1059) ),
introduced(definition,[new_symbols(definition,[spl0_302])],[avatar_definition]) ).
fof(f1832,plain,
( ~ spl0_302
| ~ spl0_241
| ~ spl0_20
| ~ spl0_242 ),
inference(avatar_split_clause,[],[f1827,f1382,f418,f1378,f1829]) ).
fof(f1866,definition,
( spl0_304
<=> c2_1(a1036) ),
introduced(definition,[new_symbols(definition,[spl0_304])],[avatar_definition]) ).
fof(f1889,plain,
( c1_1(a1059)
| ~ c2_1(a1059)
| ~ spl0_37
| ~ spl0_242 ),
inference(resolution,[],[f479,f1383]) ).
fof(f1899,plain,
( ~ spl0_241
| spl0_240
| ~ spl0_37
| ~ spl0_242 ),
inference(avatar_split_clause,[],[f1889,f1382,f478,f1373,f1378]) ).
fof(f1909,definition,
( spl0_306
<=> c0_1(a1105) ),
introduced(definition,[new_symbols(definition,[spl0_306])],[avatar_definition]) ).
fof(f1940,plain,
( c2_1(a1037)
| ~ c0_1(a1037)
| ~ spl0_13
| spl0_176 ),
inference(resolution,[],[f395,f1075]) ).
fof(f1947,plain,
( ~ spl0_175
| spl0_290
| ~ spl0_13
| spl0_176 ),
inference(avatar_split_clause,[],[f1940,f1074,f394,f1617,f1070]) ).
fof(f2002,plain,
( ~ c1_1(a1105)
| c2_1(a1105)
| ~ spl0_18
| ~ spl0_96 ),
inference(resolution,[],[f412,f701]) ).
fof(f2004,plain,
( spl0_98
| ~ spl0_97
| ~ spl0_18
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f2002,f700,f411,f705,f709]) ).
fof(f2015,plain,
( ~ c2_1(a1103)
| ~ c0_1(a1103)
| ~ spl0_19
| ~ spl0_99 ),
inference(resolution,[],[f716,f416]) ).
fof(f2017,plain,
( c1_1(a1083)
| ~ c2_1(a1083)
| ~ spl0_37
| ~ spl0_220 ),
inference(resolution,[],[f1281,f479]) ).
fof(f2021,definition,
( spl0_309
<=> c0_1(a1083) ),
introduced(definition,[new_symbols(definition,[spl0_309])],[avatar_definition]) ).
fof(f2026,plain,
( ~ spl0_221
| spl0_219
| ~ spl0_37
| ~ spl0_220 ),
inference(avatar_split_clause,[],[f2017,f1280,f478,f1275,f1284]) ).
fof(f2065,plain,
( c0_1(a1034)
| ~ c1_1(a1034)
| ~ spl0_10
| ~ spl0_179 ),
inference(resolution,[],[f385,f1089]) ).
fof(f2070,plain,
( ~ spl0_177
| spl0_178
| ~ spl0_10
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f2065,f1088,f384,f1084,f1079]) ).
fof(f2118,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_15
| ~ spl0_22 ),
inference(resolution,[],[f402,f426]) ).
fof(f2120,plain,
( c0_1(a1083)
| ~ c2_1(a1083)
| ~ spl0_15
| ~ spl0_220 ),
inference(resolution,[],[f402,f1281]) ).
fof(f2126,plain,
( ! [X0] :
( c0_1(X0)
| ~ c2_1(X0)
| c1_1(X0) )
| ~ spl0_15
| ~ spl0_22 ),
inference(duplicate_literal_removal,[],[f2118]) ).
fof(f2129,plain,
( ~ spl0_221
| spl0_309
| ~ spl0_15
| ~ spl0_220 ),
inference(avatar_split_clause,[],[f2120,f1280,f401,f2021,f1284]) ).
fof(f2130,plain,
( spl0_56
| ~ spl0_15
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f2126,f425,f401,f545]) ).
fof(f2173,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_31 ),
inference(resolution,[],[f458,f402]) ).
fof(f2175,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_16
| ~ spl0_31 ),
inference(resolution,[],[f458,f406]) ).
fof(f2176,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_31
| ~ spl0_37 ),
inference(resolution,[],[f458,f479]) ).
fof(f2186,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_31
| ~ spl0_37 ),
inference(duplicate_literal_removal,[],[f2176]) ).
fof(f2187,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_16
| ~ spl0_31 ),
inference(duplicate_literal_removal,[],[f2175]) ).
fof(f2189,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_15
| ~ spl0_31 ),
inference(duplicate_literal_removal,[],[f2173]) ).
fof(f2192,plain,
( spl0_56
| ~ spl0_31
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f2186,f478,f457,f545]) ).
fof(f2193,plain,
( spl0_56
| ~ spl0_15
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f2189,f457,f401,f545]) ).
fof(f2219,plain,
( c1_1(a1036)
| ~ c0_1(a1036)
| ~ spl0_43
| spl0_262 ),
inference(resolution,[],[f501,f1477]) ).
fof(f2223,plain,
( c1_1(a1084)
| ~ c0_1(a1084)
| ~ spl0_43
| spl0_119 ),
inference(resolution,[],[f501,f809]) ).
fof(f2249,definition,
( spl0_310
<=> c0_1(a1032) ),
introduced(definition,[new_symbols(definition,[spl0_310])],[avatar_definition]) ).
fof(f2305,plain,
( c2_1(a1088)
| c0_1(a1088)
| ~ spl0_16
| ~ spl0_217 ),
inference(resolution,[],[f1267,f406]) ).
fof(f2310,definition,
( spl0_311
<=> c0_1(a1088) ),
introduced(definition,[new_symbols(definition,[spl0_311])],[avatar_definition]) ).
fof(f2313,plain,
( spl0_311
| spl0_216
| ~ spl0_16
| ~ spl0_217 ),
inference(avatar_split_clause,[],[f2305,f1266,f405,f1261,f2310]) ).
fof(f2328,plain,
( c2_1(a1032)
| ~ c0_1(a1032)
| ~ spl0_13
| spl0_184 ),
inference(resolution,[],[f395,f1113]) ).
fof(f2338,plain,
( ~ spl0_310
| spl0_185
| ~ spl0_13
| spl0_184 ),
inference(avatar_split_clause,[],[f2328,f1112,f394,f1116,f2249]) ).
fof(f2379,definition,
( spl0_314
<=> c0_1(a1056) ),
introduced(definition,[new_symbols(definition,[spl0_314])],[avatar_definition]) ).
fof(f2391,definition,
( spl0_315
<=> c1_1(a1091) ),
introduced(definition,[new_symbols(definition,[spl0_315])],[avatar_definition]) ).
fof(f2421,plain,
( ~ spl0_289
| ~ spl0_101
| ~ spl0_19
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f2015,f715,f415,f724,f1608]) ).
fof(f2423,plain,
( ~ spl0_263
| spl0_261
| ~ spl0_43
| spl0_262 ),
inference(avatar_split_clause,[],[f2219,f1476,f500,f1471,f1480]) ).
fof(f2439,plain,
( c0_1(a1101)
| ~ c1_1(a1101)
| ~ spl0_10
| ~ spl0_206 ),
inference(resolution,[],[f385,f1215]) ).
fof(f2447,plain,
( c0_1(a1105)
| ~ c1_1(a1105)
| ~ spl0_10
| ~ spl0_96 ),
inference(resolution,[],[f385,f701]) ).
fof(f2449,plain,
( ~ spl0_97
| spl0_306
| ~ spl0_10
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f2447,f700,f384,f1909,f705]) ).
fof(f2454,plain,
( ~ spl0_205
| spl0_204
| ~ spl0_10
| ~ spl0_206 ),
inference(avatar_split_clause,[],[f2439,f1214,f384,f1205,f1210]) ).
fof(f2469,plain,
( ~ c2_1(a1056)
| ~ c0_1(a1056)
| ~ spl0_19
| ~ spl0_145 ),
inference(resolution,[],[f416,f931]) ).
fof(f2471,plain,
( ~ c2_1(a1073)
| ~ c0_1(a1073)
| ~ spl0_19
| ~ spl0_128 ),
inference(resolution,[],[f416,f851]) ).
fof(f2481,plain,
( ~ spl0_126
| ~ spl0_127
| ~ spl0_19
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f2471,f850,f415,f846,f841]) ).
fof(f2482,plain,
( ~ spl0_314
| ~ spl0_146
| ~ spl0_19
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f2469,f930,f415,f934,f2379]) ).
fof(f2545,plain,
( ~ c2_1(a1083)
| ~ c0_1(a1083)
| ~ spl0_20
| ~ spl0_220 ),
inference(resolution,[],[f419,f1281]) ).
fof(f2548,plain,
( ~ c2_1(a1031)
| ~ c0_1(a1031)
| ~ spl0_20
| ~ spl0_188 ),
inference(resolution,[],[f419,f1131]) ).
fof(f2550,plain,
( ~ c2_1(a1062)
| ~ c0_1(a1062)
| ~ spl0_20
| ~ spl0_143 ),
inference(resolution,[],[f419,f921]) ).
fof(f2551,plain,
( ~ c2_1(a1074)
| ~ c0_1(a1074)
| ~ spl0_20
| ~ spl0_125 ),
inference(resolution,[],[f419,f837]) ).
fof(f2552,plain,
( ~ c2_1(a1085)
| ~ c0_1(a1085)
| ~ spl0_20
| ~ spl0_114 ),
inference(resolution,[],[f419,f786]) ).
fof(f2555,plain,
( ~ spl0_115
| ~ spl0_116
| ~ spl0_20
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f2552,f785,f418,f794,f790]) ).
fof(f2558,plain,
( ~ spl0_124
| ~ spl0_123
| ~ spl0_20
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f2551,f836,f418,f827,f832]) ).
fof(f2561,plain,
( ~ spl0_141
| ~ spl0_142
| ~ spl0_20
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f2550,f920,f418,f916,f911]) ).
fof(f2563,plain,
( ~ spl0_294
| ~ spl0_186
| ~ spl0_20
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f2548,f1130,f418,f1121,f1678]) ).
fof(f2565,plain,
( ~ spl0_309
| ~ spl0_221
| ~ spl0_20
| ~ spl0_220 ),
inference(avatar_split_clause,[],[f2545,f1280,f418,f1284,f2021]) ).
fof(f2571,plain,
( ~ c2_1(a1036)
| c1_1(a1036)
| ~ spl0_22
| spl0_262 ),
inference(resolution,[],[f426,f1477]) ).
fof(f2577,plain,
( ~ c2_1(a1084)
| c1_1(a1084)
| ~ spl0_22
| spl0_119 ),
inference(resolution,[],[f426,f809]) ).
fof(f2581,plain,
( spl0_118
| ~ spl0_296
| ~ spl0_22
| spl0_119 ),
inference(avatar_split_clause,[],[f2577,f808,f425,f1695,f804]) ).
fof(f2586,plain,
( spl0_261
| ~ spl0_304
| ~ spl0_22
| spl0_262 ),
inference(avatar_split_clause,[],[f2571,f1476,f425,f1866,f1471]) ).
fof(f2596,plain,
( ~ c2_1(a1040)
| ~ c1_1(a1040)
| ~ spl0_26
| ~ spl0_172 ),
inference(resolution,[],[f441,f1057]) ).
fof(f2608,plain,
( ~ spl0_173
| ~ spl0_171
| ~ spl0_26
| ~ spl0_172 ),
inference(avatar_split_clause,[],[f2596,f1056,f440,f1051,f1060]) ).
fof(f2612,plain,
( c0_1(a1088)
| c2_1(a1088)
| ~ spl0_28
| ~ spl0_218 ),
inference(resolution,[],[f447,f1271]) ).
fof(f2623,plain,
( c0_1(a1105)
| c2_1(a1105)
| ~ spl0_28
| ~ spl0_97 ),
inference(resolution,[],[f447,f706]) ).
fof(f2624,plain,
( spl0_98
| spl0_306
| ~ spl0_28
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f2623,f705,f446,f1909,f709]) ).
fof(f2628,plain,
( spl0_216
| spl0_311
| ~ spl0_28
| ~ spl0_218 ),
inference(avatar_split_clause,[],[f2612,f1270,f446,f2310,f1261]) ).
fof(f2634,plain,
( c2_1(a1088)
| ~ c0_1(a1088)
| ~ spl0_38
| ~ spl0_217 ),
inference(resolution,[],[f482,f1267]) ).
fof(f2641,plain,
( c2_1(a1105)
| ~ c0_1(a1105)
| ~ spl0_38
| ~ spl0_96 ),
inference(resolution,[],[f482,f701]) ).
fof(f2643,plain,
( ~ spl0_306
| spl0_98
| ~ spl0_38
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f2641,f700,f481,f709,f1909]) ).
fof(f2648,plain,
( ~ spl0_311
| spl0_216
| ~ spl0_38
| ~ spl0_217 ),
inference(avatar_split_clause,[],[f2634,f1266,f481,f1261,f2310]) ).
fof(f2659,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_20
| ~ spl0_48 ),
inference(resolution,[],[f518,f419]) ).
fof(f2671,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_20
| ~ spl0_48 ),
inference(duplicate_literal_removal,[],[f2659]) ).
fof(f2697,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_38
| ~ spl0_55 ),
inference(resolution,[],[f543,f482]) ).
fof(f2701,plain,
( c2_1(a1036)
| c1_1(a1036)
| ~ spl0_55
| spl0_262 ),
inference(resolution,[],[f543,f1477]) ).
fof(f2704,plain,
( c2_1(a1091)
| c1_1(a1091)
| ~ spl0_55
| spl0_212 ),
inference(resolution,[],[f543,f1243]) ).
fof(f2707,plain,
( c2_1(a1084)
| c1_1(a1084)
| ~ spl0_55
| spl0_119 ),
inference(resolution,[],[f543,f809]) ).
fof(f2710,plain,
( ! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_38
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f2697]) ).
fof(f2712,plain,
( spl0_118
| spl0_296
| ~ spl0_55
| spl0_119 ),
inference(avatar_split_clause,[],[f2707,f808,f542,f1695,f804]) ).
fof(f2714,plain,
( spl0_315
| spl0_210
| ~ spl0_55
| spl0_212 ),
inference(avatar_split_clause,[],[f2704,f1242,f542,f1233,f2391]) ).
fof(f2717,plain,
( spl0_261
| spl0_304
| ~ spl0_55
| spl0_262 ),
inference(avatar_split_clause,[],[f2701,f1476,f542,f1866,f1471]) ).
fof(f2718,plain,
( spl0_13
| ~ spl0_38
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f2710,f542,f481,f394]) ).
fof(f2726,plain,
( ~ c2_1(a1059)
| c0_1(a1059)
| ~ spl0_56
| spl0_240 ),
inference(resolution,[],[f546,f1374]) ).
fof(f2729,plain,
( ~ c2_1(a1083)
| c0_1(a1083)
| ~ spl0_56
| spl0_219 ),
inference(resolution,[],[f546,f1276]) ).
fof(f2731,plain,
( ~ c2_1(a1102)
| c0_1(a1102)
| ~ spl0_56
| spl0_201 ),
inference(resolution,[],[f546,f1192]) ).
fof(f2733,plain,
( ~ c2_1(a1031)
| c0_1(a1031)
| ~ spl0_56
| spl0_187 ),
inference(resolution,[],[f546,f1127]) ).
fof(f2750,plain,
( spl0_294
| ~ spl0_186
| ~ spl0_56
| spl0_187 ),
inference(avatar_split_clause,[],[f2733,f1126,f545,f1121,f1678]) ).
fof(f2754,plain,
( spl0_203
| ~ spl0_202
| ~ spl0_56
| spl0_201 ),
inference(avatar_split_clause,[],[f2731,f1191,f545,f1196,f1200]) ).
fof(f2755,plain,
( spl0_309
| ~ spl0_221
| ~ spl0_56
| spl0_219 ),
inference(avatar_split_clause,[],[f2729,f1275,f545,f1284,f2021]) ).
fof(f2756,plain,
( spl0_302
| ~ spl0_241
| ~ spl0_56
| spl0_240 ),
inference(avatar_split_clause,[],[f2726,f1373,f545,f1378,f1829]) ).
fof(f2785,plain,
( c0_1(a1029)
| ~ c2_1(a1029)
| ~ spl0_58
| ~ spl0_190 ),
inference(resolution,[],[f553,f1141]) ).
fof(f2789,plain,
( c0_1(a1056)
| ~ c2_1(a1056)
| ~ spl0_58
| ~ spl0_145 ),
inference(resolution,[],[f553,f931]) ).
fof(f2791,plain,
( c0_1(a1081)
| ~ c2_1(a1081)
| ~ spl0_58
| ~ spl0_122 ),
inference(resolution,[],[f553,f823]) ).
fof(f2800,plain,
( ~ spl0_146
| spl0_314
| ~ spl0_58
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f2789,f930,f552,f2379,f934]) ).
fof(f2802,plain,
( ~ spl0_189
| spl0_191
| ~ spl0_58
| ~ spl0_190 ),
inference(avatar_split_clause,[],[f2785,f1140,f552,f1144,f1135]) ).
fof(f2869,plain,
( c0_1(a1082)
| c2_1(a1082)
| ~ spl0_63
| spl0_224 ),
inference(resolution,[],[f571,f1299]) ).
fof(f2885,plain,
( c0_1(a1039)
| c2_1(a1039)
| ~ spl0_28
| ~ spl0_257 ),
inference(resolution,[],[f1453,f447]) ).
fof(f2888,plain,
( spl0_256
| spl0_255
| ~ spl0_28
| ~ spl0_257 ),
inference(avatar_split_clause,[],[f2885,f1452,f446,f1443,f1448]) ).
fof(f2898,plain,
( spl0_21
| ~ spl0_16
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f2187,f457,f405,f422]) ).
fof(f2914,plain,
( c2_1(a1032)
| ~ c0_1(a1032)
| ~ spl0_38
| ~ spl0_183 ),
inference(resolution,[],[f1108,f482]) ).
fof(f2915,plain,
( ~ c0_1(a1032)
| c1_1(a1032)
| ~ spl0_52
| ~ spl0_183 ),
inference(resolution,[],[f1108,f533]) ).
fof(f2916,plain,
( spl0_184
| ~ spl0_310
| ~ spl0_52
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f2915,f1107,f532,f2249,f1112]) ).
fof(f2917,plain,
( ~ spl0_310
| spl0_185
| ~ spl0_38
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f2914,f1107,f481,f1116,f2249]) ).
fof(f2957,plain,
( spl0_223
| spl0_222
| ~ spl0_63
| spl0_224 ),
inference(avatar_split_clause,[],[f2869,f1298,f570,f1289,f1294]) ).
fof(f2976,plain,
( c2_1(a1091)
| ~ c1_1(a1091)
| ~ spl0_8
| spl0_212 ),
inference(resolution,[],[f379,f1243]) ).
fof(f2987,plain,
( ~ spl0_315
| spl0_210
| ~ spl0_8
| spl0_212 ),
inference(avatar_split_clause,[],[f2976,f1242,f378,f1233,f2391]) ).
fof(f2999,plain,
( c2_1(a1089)
| ~ c0_1(a1089)
| ~ spl0_13
| spl0_213 ),
inference(resolution,[],[f395,f1248]) ).
fof(f3006,plain,
( c2_1(a1053)
| ~ c0_1(a1053)
| ~ spl0_13
| spl0_149 ),
inference(resolution,[],[f395,f949]) ).
fof(f3008,plain,
( c2_1(a1084)
| ~ c0_1(a1084)
| ~ spl0_13
| spl0_118 ),
inference(resolution,[],[f395,f805]) ).
fof(f3011,plain,
( ~ spl0_117
| spl0_296
| ~ spl0_13
| spl0_118 ),
inference(avatar_split_clause,[],[f3008,f804,f394,f1695,f799]) ).
fof(f3012,plain,
( ~ spl0_147
| spl0_148
| ~ spl0_13
| spl0_149 ),
inference(avatar_split_clause,[],[f3006,f948,f394,f944,f939]) ).
fof(f3015,plain,
( ~ spl0_214
| spl0_215
| ~ spl0_13
| spl0_213 ),
inference(avatar_split_clause,[],[f2999,f1247,f394,f1256,f1252]) ).
fof(f3025,plain,
( c0_1(a1079)
| c2_1(a1079)
| ~ spl0_28
| ~ spl0_230 ),
inference(resolution,[],[f447,f1327]) ).
fof(f3034,plain,
( c0_1(a1065)
| c2_1(a1065)
| ~ spl0_28
| ~ spl0_138 ),
inference(resolution,[],[f447,f898]) ).
fof(f3035,plain,
( c0_1(a1081)
| c2_1(a1081)
| ~ spl0_28
| ~ spl0_122 ),
inference(resolution,[],[f447,f823]) ).
fof(f3042,plain,
( spl0_301
| spl0_121
| ~ spl0_28
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f3035,f822,f446,f818,f1810]) ).
fof(f3043,plain,
( spl0_139
| spl0_140
| ~ spl0_28
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f3034,f897,f446,f906,f902]) ).
fof(f3045,plain,
( spl0_228
| spl0_229
| ~ spl0_28
| ~ spl0_230 ),
inference(avatar_split_clause,[],[f3025,f1326,f446,f1322,f1317]) ).
fof(f3079,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_26
| ~ spl0_67 ),
inference(resolution,[],[f586,f441]) ).
fof(f3092,plain,
( ! [X0] :
( c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_26
| ~ spl0_67 ),
inference(duplicate_literal_removal,[],[f3079]) ).
fof(f3103,plain,
( spl0_58
| ~ spl0_26
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f3092,f585,f440,f552]) ).
fof(f3108,plain,
( ~ spl0_301
| spl0_121
| ~ spl0_58
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f2791,f822,f552,f818,f1810]) ).
fof(f3110,plain,
( c0_1(a1030)
| c2_1(a1030)
| ~ spl0_63
| spl0_268 ),
inference(resolution,[],[f1505,f571]) ).
fof(f3118,plain,
( spl0_269
| spl0_267
| ~ spl0_63
| spl0_268 ),
inference(avatar_split_clause,[],[f3110,f1504,f570,f1499,f1508]) ).
fof(f3120,plain,
( spl0_19
| ~ spl0_20
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f2671,f517,f418,f415]) ).
fof(f3141,plain,
( ~ spl0_117
| spl0_118
| ~ spl0_43
| spl0_119 ),
inference(avatar_split_clause,[],[f2223,f808,f500,f804,f799]) ).
fof(f3178,plain,
( ~ c2_1(a1103)
| ~ c0_1(a1103)
| ~ spl0_20
| ~ spl0_100 ),
inference(resolution,[],[f721,f419]) ).
fof(f3180,plain,
( ~ spl0_289
| ~ spl0_101
| ~ spl0_20
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f3178,f720,f418,f724,f1608]) ).
fof(f3258,plain,
( c2_1(a1055)
| c0_1(a1055)
| ~ spl0_21
| spl0_244 ),
inference(resolution,[],[f423,f1393]) ).
fof(f3260,plain,
( c2_1(a1080)
| c0_1(a1080)
| ~ spl0_21
| spl0_225 ),
inference(resolution,[],[f423,f1304]) ).
fof(f3265,plain,
( c2_1(a1032)
| c0_1(a1032)
| ~ spl0_21
| spl0_184 ),
inference(resolution,[],[f423,f1113]) ).
fof(f3273,plain,
( spl0_310
| spl0_185
| ~ spl0_21
| spl0_184 ),
inference(avatar_split_clause,[],[f3265,f1112,f422,f1116,f2249]) ).
fof(f3274,plain,
( spl0_227
| spl0_226
| ~ spl0_21
| spl0_225 ),
inference(avatar_split_clause,[],[f3260,f1303,f422,f1308,f1312]) ).
fof(f3275,plain,
( spl0_245
| spl0_243
| ~ spl0_21
| spl0_244 ),
inference(avatar_split_clause,[],[f3258,f1392,f422,f1387,f1396]) ).
fof(f3286,plain,
( c1_1(a1091)
| c0_1(a1091)
| ~ spl0_31
| spl0_212 ),
inference(resolution,[],[f458,f1243]) ).
fof(f3292,plain,
( spl0_211
| spl0_315
| ~ spl0_31
| spl0_212 ),
inference(avatar_split_clause,[],[f3286,f1242,f457,f2391,f1238]) ).
fof(f3316,plain,
( c1_1(a1043)
| ~ c0_1(a1043)
| ~ spl0_43
| spl0_249 ),
inference(resolution,[],[f501,f1416]) ).
fof(f3326,plain,
( ~ spl0_250
| spl0_251
| ~ spl0_43
| spl0_249 ),
inference(avatar_split_clause,[],[f3316,f1415,f500,f1424,f1420]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f363]) ).
cnf(s2,plain,
( spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f373]) ).
cnf(s7,plain,
( spl0_19
| ~ spl0_9
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f420]) ).
cnf(s8,plain,
( ~ spl0_9
| spl0_19
| spl0_20 ),
inference(rat,[],[s7]) ).
cnf(s9,plain,
( ~ spl0_9
| spl0_15
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f427]) ).
cnf(s12,plain,
( ~ spl0_9
| spl0_26
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f448]) ).
cnf(s14,plain,
( ~ spl0_9
| spl0_10
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f459]) ).
cnf(s15,plain,
( ~ spl0_9
| spl0_20
| spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f466]) ).
cnf(s17,plain,
( ~ spl0_9
| spl0_36
| spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f483]) ).
cnf(s18,plain,
( spl0_8
| ~ spl0_9
| spl0_28
| spl0_31 ),
inference(sat_conversion,[],[f484]) ).
cnf(s19,plain,
( spl0_2
| ~ spl0_9
| spl0_18
| spl0_39 ),
inference(sat_conversion,[],[f488]) ).
cnf(s20,plain,
( ~ spl0_9
| spl0_13
| spl0_40
| spl0_41 ),
inference(sat_conversion,[],[f495]) ).
cnf(s21,plain,
( ~ spl0_9
| spl0_42
| spl0_43
| spl0_44 ),
inference(sat_conversion,[],[f505]) ).
cnf(s23,plain,
( ~ spl0_9
| spl0_26
| spl0_43
| spl0_48 ),
inference(sat_conversion,[],[f519]) ).
cnf(s24,plain,
( ~ spl0_9
| spl0_26
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f526]) ).
cnf(s25,plain,
( ~ spl0_9
| spl0_20
| spl0_37
| spl0_51 ),
inference(sat_conversion,[],[f530]) ).
cnf(s27,plain,
( ~ spl0_9
| spl0_43
| spl0_55
| spl0_56 ),
inference(sat_conversion,[],[f547]) ).
cnf(s30,plain,
( ~ spl0_9
| spl0_22
| spl0_31
| spl0_56 ),
inference(sat_conversion,[],[f565]) ).
cnf(s32,plain,
( ~ spl0_9
| spl0_31
| spl0_38
| spl0_64 ),
inference(sat_conversion,[],[f576]) ).
cnf(s34,plain,
( ~ spl0_9
| spl0_24
| spl0_29
| spl0_67 ),
inference(sat_conversion,[],[f587]) ).
cnf(s35,plain,
( ~ spl0_9
| spl0_16
| spl0_33
| spl0_68 ),
inference(sat_conversion,[],[f591]) ).
cnf(s36,plain,
( spl0_6
| ~ spl0_9
| spl0_58
| spl0_69 ),
inference(sat_conversion,[],[f595]) ).
cnf(s38,plain,
( spl0_23
| spl0_72
| spl0_73 ),
inference(sat_conversion,[],[f609]) ).
cnf(s45,plain,
( ~ spl0_9
| spl0_19
| spl0_38
| spl0_59 ),
inference(sat_conversion,[],[f637]) ).
cnf(s47,plain,
( ~ spl0_9
| spl0_38
| spl0_52
| spl0_72 ),
inference(sat_conversion,[],[f645]) ).
cnf(s48,plain,
( ~ spl0_9
| spl0_63
| spl0_69 ),
inference(sat_conversion,[],[f646]) ).
cnf(s50,plain,
( ~ spl0_9
| spl0_10
| spl0_85
| spl0_86 ),
inference(sat_conversion,[],[f660]) ).
cnf(s53,plain,
( spl0_8
| ~ spl0_9
| spl0_43
| spl0_53 ),
inference(sat_conversion,[],[f663]) ).
cnf(s54,plain,
( ~ spl0_9
| spl0_26
| spl0_28
| spl0_33 ),
inference(sat_conversion,[],[f664]) ).
cnf(s55,plain,
( ~ spl0_9
| spl0_48
| spl0_87
| spl0_88 ),
inference(sat_conversion,[],[f671]) ).
cnf(s62,plain,
( ~ spl0_1
| spl0_96 ),
inference(sat_conversion,[],[f703]) ).
cnf(s63,plain,
( ~ spl0_1
| spl0_97 ),
inference(sat_conversion,[],[f707]) ).
cnf(s64,plain,
( ~ spl0_1
| ~ spl0_98 ),
inference(sat_conversion,[],[f711]) ).
cnf(s65,plain,
( ~ spl0_1
| spl0_9 ),
inference(sat_conversion,[],[f713]) ).
cnf(s66,plain,
( ~ spl0_3
| spl0_99 ),
inference(sat_conversion,[],[f718]) ).
cnf(s67,plain,
( ~ spl0_3
| spl0_100 ),
inference(sat_conversion,[],[f722]) ).
cnf(s68,plain,
( ~ spl0_3
| spl0_101 ),
inference(sat_conversion,[],[f726]) ).
cnf(s69,plain,
( ~ spl0_3
| spl0_9 ),
inference(sat_conversion,[],[f727]) ).
cnf(s86,plain,
( ~ spl0_36
| spl0_114 ),
inference(sat_conversion,[],[f788]) ).
cnf(s87,plain,
( ~ spl0_36
| spl0_115 ),
inference(sat_conversion,[],[f792]) ).
cnf(s88,plain,
( ~ spl0_36
| spl0_116 ),
inference(sat_conversion,[],[f796]) ).
cnf(s90,plain,
( ~ spl0_2
| spl0_117 ),
inference(sat_conversion,[],[f802]) ).
cnf(s91,plain,
( ~ spl0_2
| ~ spl0_118 ),
inference(sat_conversion,[],[f806]) ).
cnf(s92,plain,
( ~ spl0_2
| ~ spl0_119 ),
inference(sat_conversion,[],[f810]) ).
cnf(s93,plain,
( ~ spl0_2
| spl0_9 ),
inference(sat_conversion,[],[f811]) ).
cnf(s94,plain,
( ~ spl0_41
| spl0_120 ),
inference(sat_conversion,[],[f816]) ).
cnf(s95,plain,
( ~ spl0_41
| ~ spl0_121 ),
inference(sat_conversion,[],[f820]) ).
cnf(s96,plain,
( ~ spl0_41
| spl0_122 ),
inference(sat_conversion,[],[f824]) ).
cnf(s98,plain,
( ~ spl0_50
| spl0_123 ),
inference(sat_conversion,[],[f830]) ).
cnf(s99,plain,
( ~ spl0_50
| spl0_124 ),
inference(sat_conversion,[],[f834]) ).
cnf(s100,plain,
( ~ spl0_50
| spl0_125 ),
inference(sat_conversion,[],[f838]) ).
cnf(s102,plain,
( ~ spl0_51
| spl0_126 ),
inference(sat_conversion,[],[f844]) ).
cnf(s103,plain,
( ~ spl0_51
| spl0_127 ),
inference(sat_conversion,[],[f848]) ).
cnf(s104,plain,
( ~ spl0_51
| spl0_128 ),
inference(sat_conversion,[],[f852]) ).
cnf(s118,plain,
( ~ spl0_64
| spl0_138 ),
inference(sat_conversion,[],[f900]) ).
cnf(s119,plain,
( ~ spl0_64
| ~ spl0_139 ),
inference(sat_conversion,[],[f904]) ).
cnf(s120,plain,
( ~ spl0_64
| ~ spl0_140 ),
inference(sat_conversion,[],[f908]) ).
cnf(s122,plain,
( ~ spl0_24
| spl0_141 ),
inference(sat_conversion,[],[f914]) ).
cnf(s123,plain,
( ~ spl0_24
| spl0_142 ),
inference(sat_conversion,[],[f918]) ).
cnf(s124,plain,
( ~ spl0_24
| spl0_143 ),
inference(sat_conversion,[],[f922]) ).
cnf(s127,plain,
( ~ spl0_49
| spl0_145 ),
inference(sat_conversion,[],[f932]) ).
cnf(s128,plain,
( ~ spl0_49
| spl0_146 ),
inference(sat_conversion,[],[f936]) ).
cnf(s130,plain,
( ~ spl0_73
| spl0_147 ),
inference(sat_conversion,[],[f942]) ).
cnf(s131,plain,
( ~ spl0_73
| ~ spl0_148 ),
inference(sat_conversion,[],[f946]) ).
cnf(s132,plain,
( ~ spl0_73
| ~ spl0_149 ),
inference(sat_conversion,[],[f950]) ).
cnf(s142,plain,
( ~ spl0_6
| spl0_156 ),
inference(sat_conversion,[],[f984]) ).
cnf(s143,plain,
( ~ spl0_6
| spl0_157 ),
inference(sat_conversion,[],[f988]) ).
cnf(s144,plain,
( ~ spl0_6
| spl0_158 ),
inference(sat_conversion,[],[f992]) ).
cnf(s162,plain,
( ~ spl0_72
| spl0_171 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s163,plain,
( ~ spl0_72
| spl0_172 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s164,plain,
( ~ spl0_72
| spl0_173 ),
inference(sat_conversion,[],[f1062]) ).
cnf(s166,plain,
( ~ spl0_85
| spl0_174 ),
inference(sat_conversion,[],[f1068]) ).
cnf(s167,plain,
( ~ spl0_85
| spl0_175 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s168,plain,
( ~ spl0_85
| ~ spl0_176 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s170,plain,
( ~ spl0_29
| spl0_177 ),
inference(sat_conversion,[],[f1082]) ).
cnf(s171,plain,
( ~ spl0_29
| ~ spl0_178 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s172,plain,
( ~ spl0_29
| spl0_179 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s178,plain,
( ~ spl0_53
| spl0_183 ),
inference(sat_conversion,[],[f1110]) ).
cnf(s179,plain,
( ~ spl0_53
| ~ spl0_184 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s180,plain,
( ~ spl0_53
| ~ spl0_185 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s182,plain,
( ~ spl0_33
| spl0_186 ),
inference(sat_conversion,[],[f1124]) ).
cnf(s183,plain,
( ~ spl0_33
| ~ spl0_187 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s184,plain,
( ~ spl0_33
| spl0_188 ),
inference(sat_conversion,[],[f1132]) ).
cnf(s186,plain,
( ~ spl0_88
| spl0_189 ),
inference(sat_conversion,[],[f1138]) ).
cnf(s187,plain,
( ~ spl0_88
| spl0_190 ),
inference(sat_conversion,[],[f1142]) ).
cnf(s188,plain,
( ~ spl0_88
| ~ spl0_191 ),
inference(sat_conversion,[],[f1146]) ).
cnf(s202,plain,
( ~ spl0_4
| ~ spl0_201 ),
inference(sat_conversion,[],[f1194]) ).
cnf(s203,plain,
( ~ spl0_4
| spl0_202 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s204,plain,
( ~ spl0_4
| ~ spl0_203 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s206,plain,
( ~ spl0_5
| ~ spl0_204 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s207,plain,
( ~ spl0_5
| spl0_205 ),
inference(sat_conversion,[],[f1212]) ).
cnf(s208,plain,
( ~ spl0_5
| spl0_206 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s214,plain,
( ~ spl0_27
| ~ spl0_210 ),
inference(sat_conversion,[],[f1236]) ).
cnf(s215,plain,
( ~ spl0_27
| ~ spl0_211 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s216,plain,
( ~ spl0_27
| ~ spl0_212 ),
inference(sat_conversion,[],[f1244]) ).
cnf(s218,plain,
( ~ spl0_30
| ~ spl0_213 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s219,plain,
( ~ spl0_30
| spl0_214 ),
inference(sat_conversion,[],[f1254]) ).
cnf(s220,plain,
( ~ spl0_30
| ~ spl0_215 ),
inference(sat_conversion,[],[f1258]) ).
cnf(s222,plain,
( ~ spl0_32
| ~ spl0_216 ),
inference(sat_conversion,[],[f1264]) ).
cnf(s223,plain,
( ~ spl0_32
| spl0_217 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s224,plain,
( ~ spl0_32
| spl0_218 ),
inference(sat_conversion,[],[f1272]) ).
cnf(s226,plain,
( ~ spl0_39
| ~ spl0_219 ),
inference(sat_conversion,[],[f1278]) ).
cnf(s227,plain,
( ~ spl0_39
| spl0_220 ),
inference(sat_conversion,[],[f1282]) ).
cnf(s228,plain,
( ~ spl0_39
| spl0_221 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s230,plain,
( ~ spl0_40
| ~ spl0_222 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s231,plain,
( ~ spl0_40
| ~ spl0_223 ),
inference(sat_conversion,[],[f1296]) ).
cnf(s232,plain,
( ~ spl0_40
| ~ spl0_224 ),
inference(sat_conversion,[],[f1300]) ).
cnf(s234,plain,
( ~ spl0_42
| ~ spl0_225 ),
inference(sat_conversion,[],[f1306]) ).
cnf(s235,plain,
( ~ spl0_42
| ~ spl0_226 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s236,plain,
( ~ spl0_42
| ~ spl0_227 ),
inference(sat_conversion,[],[f1314]) ).
cnf(s238,plain,
( ~ spl0_44
| ~ spl0_228 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s239,plain,
( ~ spl0_44
| ~ spl0_229 ),
inference(sat_conversion,[],[f1324]) ).
cnf(s240,plain,
( ~ spl0_44
| spl0_230 ),
inference(sat_conversion,[],[f1328]) ).
cnf(s254,plain,
( ~ spl0_68
| ~ spl0_240 ),
inference(sat_conversion,[],[f1376]) ).
cnf(s255,plain,
( ~ spl0_68
| spl0_241 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s256,plain,
( ~ spl0_68
| spl0_242 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s258,plain,
( ~ spl0_23
| ~ spl0_243 ),
inference(sat_conversion,[],[f1390]) ).
cnf(s259,plain,
( ~ spl0_23
| ~ spl0_244 ),
inference(sat_conversion,[],[f1394]) ).
cnf(s260,plain,
( ~ spl0_23
| ~ spl0_245 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s266,plain,
( ~ spl0_59
| ~ spl0_249 ),
inference(sat_conversion,[],[f1418]) ).
cnf(s267,plain,
( ~ spl0_59
| spl0_250 ),
inference(sat_conversion,[],[f1422]) ).
cnf(s268,plain,
( ~ spl0_59
| ~ spl0_251 ),
inference(sat_conversion,[],[f1426]) ).
cnf(s274,plain,
( ~ spl0_69
| ~ spl0_255 ),
inference(sat_conversion,[],[f1446]) ).
cnf(s275,plain,
( ~ spl0_69
| ~ spl0_256 ),
inference(sat_conversion,[],[f1450]) ).
cnf(s276,plain,
( ~ spl0_69
| spl0_257 ),
inference(sat_conversion,[],[f1454]) ).
cnf(s282,plain,
( ~ spl0_86
| ~ spl0_261 ),
inference(sat_conversion,[],[f1474]) ).
cnf(s283,plain,
( ~ spl0_86
| ~ spl0_262 ),
inference(sat_conversion,[],[f1478]) ).
cnf(s284,plain,
( ~ spl0_86
| spl0_263 ),
inference(sat_conversion,[],[f1482]) ).
cnf(s290,plain,
( ~ spl0_87
| ~ spl0_267 ),
inference(sat_conversion,[],[f1502]) ).
cnf(s291,plain,
( ~ spl0_87
| ~ spl0_268 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s292,plain,
( ~ spl0_87
| ~ spl0_269 ),
inference(sat_conversion,[],[f1510]) ).
cnf(s320,plain,
( ~ spl0_10
| ~ spl0_99
| ~ spl0_100
| spl0_289 ),
inference(sat_conversion,[],[f1610]) ).
cnf(s324,plain,
( ~ spl0_8
| ~ spl0_16
| spl0_28 ),
inference(sat_conversion,[],[f1634]) ).
cnf(s328,plain,
( ~ spl0_19
| ~ spl0_156
| ~ spl0_157
| ~ spl0_158 ),
inference(sat_conversion,[],[f1660]) ).
cnf(s331,plain,
( ~ spl0_20
| ~ spl0_174
| ~ spl0_175
| ~ spl0_290 ),
inference(sat_conversion,[],[f1675]) ).
cnf(s337,plain,
( ~ spl0_26
| ~ spl0_99
| ~ spl0_100
| ~ spl0_101 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s351,plain,
( ~ spl0_37
| ~ spl0_174
| spl0_176
| ~ spl0_290 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s352,plain,
( ~ spl0_37
| ~ spl0_186
| spl0_187
| ~ spl0_188 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s353,plain,
( ~ spl0_38
| ~ spl0_174
| ~ spl0_175
| spl0_290 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s363,plain,
( ~ spl0_26
| ~ spl0_120
| ~ spl0_122
| ~ spl0_301 ),
inference(sat_conversion,[],[f1814]) ).
cnf(s366,plain,
( ~ spl0_20
| ~ spl0_241
| ~ spl0_242
| ~ spl0_302 ),
inference(sat_conversion,[],[f1832]) ).
cnf(s376,plain,
( ~ spl0_37
| spl0_240
| ~ spl0_241
| ~ spl0_242 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s389,plain,
( ~ spl0_13
| ~ spl0_175
| spl0_176
| spl0_290 ),
inference(sat_conversion,[],[f1947]) ).
cnf(s407,plain,
( ~ spl0_18
| ~ spl0_96
| ~ spl0_97
| spl0_98 ),
inference(sat_conversion,[],[f2004]) ).
cnf(s416,plain,
( ~ spl0_37
| spl0_219
| ~ spl0_220
| ~ spl0_221 ),
inference(sat_conversion,[],[f2026]) ).
cnf(s434,plain,
( ~ spl0_10
| ~ spl0_177
| spl0_178
| ~ spl0_179 ),
inference(sat_conversion,[],[f2070]) ).
cnf(s466,plain,
( ~ spl0_15
| ~ spl0_220
| ~ spl0_221
| spl0_309 ),
inference(sat_conversion,[],[f2129]) ).
cnf(s467,plain,
( ~ spl0_15
| ~ spl0_22
| spl0_56 ),
inference(sat_conversion,[],[f2130]) ).
cnf(s481,plain,
( ~ spl0_31
| ~ spl0_37
| spl0_56 ),
inference(sat_conversion,[],[f2192]) ).
cnf(s482,plain,
( ~ spl0_15
| ~ spl0_31
| spl0_56 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s536,plain,
( ~ spl0_16
| spl0_216
| ~ spl0_217
| spl0_311 ),
inference(sat_conversion,[],[f2313]) ).
cnf(s541,plain,
( ~ spl0_13
| spl0_184
| spl0_185
| ~ spl0_310 ),
inference(sat_conversion,[],[f2338]) ).
cnf(s584,plain,
( ~ spl0_19
| ~ spl0_99
| ~ spl0_101
| ~ spl0_289 ),
inference(sat_conversion,[],[f2421]) ).
cnf(s586,plain,
( ~ spl0_43
| spl0_261
| spl0_262
| ~ spl0_263 ),
inference(sat_conversion,[],[f2423]) ).
cnf(s596,plain,
( ~ spl0_10
| ~ spl0_96
| ~ spl0_97
| spl0_306 ),
inference(sat_conversion,[],[f2449]) ).
cnf(s599,plain,
( ~ spl0_10
| spl0_204
| ~ spl0_205
| ~ spl0_206 ),
inference(sat_conversion,[],[f2454]) ).
cnf(s603,plain,
( ~ spl0_19
| ~ spl0_126
| ~ spl0_127
| ~ spl0_128 ),
inference(sat_conversion,[],[f2481]) ).
cnf(s604,plain,
( ~ spl0_19
| ~ spl0_145
| ~ spl0_146
| ~ spl0_314 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s654,plain,
( ~ spl0_20
| ~ spl0_114
| ~ spl0_115
| ~ spl0_116 ),
inference(sat_conversion,[],[f2555]) ).
cnf(s655,plain,
( ~ spl0_20
| ~ spl0_123
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f2558]) ).
cnf(s656,plain,
( ~ spl0_20
| ~ spl0_141
| ~ spl0_142
| ~ spl0_143 ),
inference(sat_conversion,[],[f2561]) ).
cnf(s658,plain,
( ~ spl0_20
| ~ spl0_186
| ~ spl0_188
| ~ spl0_294 ),
inference(sat_conversion,[],[f2563]) ).
cnf(s660,plain,
( ~ spl0_20
| ~ spl0_220
| ~ spl0_221
| ~ spl0_309 ),
inference(sat_conversion,[],[f2565]) ).
cnf(s664,plain,
( ~ spl0_22
| spl0_118
| spl0_119
| ~ spl0_296 ),
inference(sat_conversion,[],[f2581]) ).
cnf(s668,plain,
( ~ spl0_22
| spl0_261
| spl0_262
| ~ spl0_304 ),
inference(sat_conversion,[],[f2586]) ).
cnf(s674,plain,
( ~ spl0_26
| ~ spl0_171
| ~ spl0_172
| ~ spl0_173 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s676,plain,
( ~ spl0_28
| ~ spl0_97
| spl0_98
| spl0_306 ),
inference(sat_conversion,[],[f2624]) ).
cnf(s680,plain,
( ~ spl0_28
| spl0_216
| ~ spl0_218
| spl0_311 ),
inference(sat_conversion,[],[f2628]) ).
cnf(s682,plain,
( ~ spl0_38
| ~ spl0_96
| spl0_98
| ~ spl0_306 ),
inference(sat_conversion,[],[f2643]) ).
cnf(s686,plain,
( ~ spl0_38
| spl0_216
| ~ spl0_217
| ~ spl0_311 ),
inference(sat_conversion,[],[f2648]) ).
cnf(s705,plain,
( ~ spl0_55
| spl0_118
| spl0_119
| spl0_296 ),
inference(sat_conversion,[],[f2712]) ).
cnf(s707,plain,
( ~ spl0_55
| spl0_210
| spl0_212
| spl0_315 ),
inference(sat_conversion,[],[f2714]) ).
cnf(s710,plain,
( ~ spl0_55
| spl0_261
| spl0_262
| spl0_304 ),
inference(sat_conversion,[],[f2717]) ).
cnf(s711,plain,
( spl0_13
| ~ spl0_38
| ~ spl0_55 ),
inference(sat_conversion,[],[f2718]) ).
cnf(s717,plain,
( ~ spl0_56
| ~ spl0_186
| spl0_187
| spl0_294 ),
inference(sat_conversion,[],[f2750]) ).
cnf(s719,plain,
( ~ spl0_56
| spl0_201
| ~ spl0_202
| spl0_203 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s720,plain,
( ~ spl0_56
| spl0_219
| ~ spl0_221
| spl0_309 ),
inference(sat_conversion,[],[f2755]) ).
cnf(s721,plain,
( ~ spl0_56
| spl0_240
| ~ spl0_241
| spl0_302 ),
inference(sat_conversion,[],[f2756]) ).
cnf(s735,plain,
( ~ spl0_58
| ~ spl0_145
| ~ spl0_146
| spl0_314 ),
inference(sat_conversion,[],[f2800]) ).
cnf(s736,plain,
( ~ spl0_58
| ~ spl0_189
| ~ spl0_190
| spl0_191 ),
inference(sat_conversion,[],[f2802]) ).
cnf(s762,plain,
( ~ spl0_28
| spl0_255
| spl0_256
| ~ spl0_257 ),
inference(sat_conversion,[],[f2888]) ).
cnf(s772,plain,
( ~ spl0_16
| spl0_21
| ~ spl0_31 ),
inference(sat_conversion,[],[f2898]) ).
cnf(s784,plain,
( ~ spl0_52
| ~ spl0_183
| spl0_184
| ~ spl0_310 ),
inference(sat_conversion,[],[f2916]) ).
cnf(s785,plain,
( ~ spl0_38
| ~ spl0_183
| spl0_185
| ~ spl0_310 ),
inference(sat_conversion,[],[f2917]) ).
cnf(s832,plain,
( ~ spl0_63
| spl0_222
| spl0_223
| spl0_224 ),
inference(sat_conversion,[],[f2957]) ).
cnf(s838,plain,
( ~ spl0_8
| spl0_210
| spl0_212
| ~ spl0_315 ),
inference(sat_conversion,[],[f2987]) ).
cnf(s845,plain,
( ~ spl0_13
| ~ spl0_117
| spl0_118
| spl0_296 ),
inference(sat_conversion,[],[f3011]) ).
cnf(s846,plain,
( ~ spl0_13
| ~ spl0_147
| spl0_148
| spl0_149 ),
inference(sat_conversion,[],[f3012]) ).
cnf(s849,plain,
( ~ spl0_13
| spl0_213
| ~ spl0_214
| spl0_215 ),
inference(sat_conversion,[],[f3015]) ).
cnf(s852,plain,
( ~ spl0_28
| spl0_121
| ~ spl0_122
| spl0_301 ),
inference(sat_conversion,[],[f3042]) ).
cnf(s853,plain,
( ~ spl0_28
| ~ spl0_138
| spl0_139
| spl0_140 ),
inference(sat_conversion,[],[f3043]) ).
cnf(s855,plain,
( ~ spl0_28
| spl0_228
| spl0_229
| ~ spl0_230 ),
inference(sat_conversion,[],[f3045]) ).
cnf(s865,plain,
( ~ spl0_26
| spl0_58
| ~ spl0_67 ),
inference(sat_conversion,[],[f3103]) ).
cnf(s870,plain,
( ~ spl0_58
| spl0_121
| ~ spl0_122
| ~ spl0_301 ),
inference(sat_conversion,[],[f3108]) ).
cnf(s872,plain,
( ~ spl0_63
| spl0_267
| spl0_268
| spl0_269 ),
inference(sat_conversion,[],[f3118]) ).
cnf(s874,plain,
( spl0_19
| ~ spl0_20
| ~ spl0_48 ),
inference(sat_conversion,[],[f3120]) ).
cnf(s898,plain,
( ~ spl0_43
| ~ spl0_117
| spl0_118
| spl0_119 ),
inference(sat_conversion,[],[f3141]) ).
cnf(s934,plain,
( ~ spl0_20
| ~ spl0_100
| ~ spl0_101
| ~ spl0_289 ),
inference(sat_conversion,[],[f3180]) ).
cnf(s964,plain,
( ~ spl0_21
| spl0_184
| spl0_185
| spl0_310 ),
inference(sat_conversion,[],[f3273]) ).
cnf(s965,plain,
( ~ spl0_21
| spl0_225
| spl0_226
| spl0_227 ),
inference(sat_conversion,[],[f3274]) ).
cnf(s966,plain,
( ~ spl0_21
| spl0_243
| spl0_244
| spl0_245 ),
inference(sat_conversion,[],[f3275]) ).
cnf(s969,plain,
( ~ spl0_31
| spl0_211
| spl0_212
| spl0_315 ),
inference(sat_conversion,[],[f3292]) ).
cnf(s975,plain,
( ~ spl0_43
| spl0_249
| ~ spl0_250
| spl0_251 ),
inference(sat_conversion,[],[f3326]) ).
cnf(s978,plain,
( ~ spl0_24
| ~ spl0_20 ),
inference(rat,[],[s656,s122,s123,s124]) ).
cnf(s979,plain,
( ~ spl0_50
| ~ spl0_20 ),
inference(rat,[],[s655,s98,s99,s100]) ).
cnf(s981,plain,
( ~ spl0_86
| ~ spl0_43 ),
inference(rat,[],[s586,s282,s283,s284]) ).
cnf(s982,plain,
( spl0_19
| ~ spl0_3 ),
inference(rat,[],[s975,s266,s267,s268,s45,s353,s331,s166,s167,s50,s981,s23,s320,s874,s934,s8,s69,s337,s66,s67,s68]) ).
cnf(s983,plain,
( ~ spl0_36
| ~ spl0_20 ),
inference(rat,[],[s654,s86,s87,s88]) ).
cnf(s984,plain,
( ~ spl0_86
| ~ spl0_38
| spl0_56
| spl0_210
| spl0_212
| ~ spl0_9 ),
inference(rat,[],[s541,s964,s9,s179,s180,s482,s53,s30,s838,s668,s711,s707,s710,s27,s981,s282,s283]) ).
cnf(s985,plain,
( spl0_28
| ~ spl0_20
| ~ spl0_3 ),
inference(rat,[],[s353,s331,s166,s167,s50,s984,s17,s717,s352,s658,s182,s183,s184,s214,s216,s54,s12,s69,s337,s320,s584,s982,s68,s67,s66,s983]) ).
cnf(s986,plain,
( ~ spl0_69
| ~ spl0_28 ),
inference(rat,[],[s762,s274,s275,s276]) ).
cnf(s987,plain,
( ~ spl0_6
| ~ spl0_19 ),
inference(rat,[],[s142,s328,s143,s144]) ).
cnf(s988,plain,
( ~ spl0_20
| ~ spl0_3 ),
inference(rat,[],[s735,s604,s36,s127,s128,s986,s24,s985,s979,s69,s337,s66,s67,s68,s987,s982]) ).
cnf(s990,plain,
( ~ spl0_51
| ~ spl0_19 ),
inference(rat,[],[s603,s102,s103,s104]) ).
cnf(s991,plain,
( ~ spl0_32
| ~ spl0_38
| ~ spl0_28 ),
inference(rat,[],[s686,s680,s222,s223,s224]) ).
cnf(s992,plain,
( ~ spl0_33
| ~ spl0_37 ),
inference(rat,[],[s352,s182,s183,s184]) ).
cnf(s994,plain,
( ~ spl0_68
| ~ spl0_37 ),
inference(rat,[],[s376,s254,s255,s256]) ).
cnf(s995,plain,
( ~ spl0_23
| ~ spl0_21 ),
inference(rat,[],[s966,s258,s259,s260]) ).
cnf(s996,plain,
( ~ spl0_41
| ~ spl0_3 ),
inference(rat,[],[s852,s870,s95,s96,s36,s986,s54,s992,s25,s990,s988,s337,s66,s67,s68,s69,s987,s982]) ).
cnf(s997,plain,
( ~ spl0_40
| ~ spl0_63 ),
inference(rat,[],[s832,s230,s231,s232]) ).
cnf(s998,plain,
( ~ spl0_30
| ~ spl0_13 ),
inference(rat,[],[s849,s218,s219,s220]) ).
cnf(s1004,plain,
( ~ spl0_44
| ~ spl0_28 ),
inference(rat,[],[s855,s238,s239,s240]) ).
cnf(s1005,plain,
( ~ spl0_42
| ~ spl0_21 ),
inference(rat,[],[s965,s234,s235,s236]) ).
cnf(s1006,plain,
~ spl0_3,
inference(rat,[],[s351,s389,s166,s167,s168,s50,s981,s21,s1005,s1004,s772,s14,s998,s20,s997,s996,s35,s994,s48,s986,s54,s992,s25,s990,s988,s320,s584,s982,s337,s66,s67,s68,s69]) ).
cnf(s1007,plain,
( ~ spl0_64
| ~ spl0_28 ),
inference(rat,[],[s853,s118,s119,s120]) ).
cnf(s1008,plain,
( spl0_20
| spl0_21
| ~ spl0_28
| ~ spl0_9 ),
inference(rat,[],[s32,s772,s991,s35,s15,s994,s992,s25,s990,s8,s1007]) ).
cnf(s1009,plain,
( ~ spl0_68
| ~ spl0_56
| ~ spl0_20 ),
inference(rat,[],[s721,s366,s254,s255,s256]) ).
cnf(s1010,plain,
( ~ spl0_31
| ~ spl0_15
| ~ spl0_20
| spl0_21
| ~ spl0_9 ),
inference(rat,[],[s717,s658,s182,s183,s184,s35,s1009,s772,s482]) ).
cnf(s1013,plain,
( ~ spl0_217
| spl0_216
| ~ spl0_16
| ~ spl0_38 ),
inference(rat,[],[s686,s536]) ).
cnf(s1014,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(rat,[],[s599,s206,s207,s208]) ).
cnf(s1015,plain,
( ~ spl0_4
| ~ spl0_56 ),
inference(rat,[],[s719,s202,s203,s204]) ).
cnf(s1024,plain,
( ~ spl0_72
| ~ spl0_26 ),
inference(rat,[],[s674,s162,s163,s164]) ).
cnf(s1026,plain,
( ~ spl0_88
| ~ spl0_58 ),
inference(rat,[],[s736,s186,s187,s188]) ).
cnf(s1027,plain,
( ~ spl0_87
| ~ spl0_63 ),
inference(rat,[],[s872,s290,s291,s292]) ).
cnf(s1028,plain,
( ~ spl0_13
| ~ spl0_28
| ~ spl0_2 ),
inference(rat,[],[s434,s170,s171,s172,s34,s865,s1026,s55,s23,s874,s987,s2,s1015,s1014,s14,s30,s1010,s9,s664,s845,s998,s978,s1008,s1005,s21,s1004,s898,s90,s91,s92,s1027,s48,s986,s93]) ).
cnf(s1029,plain,
( ~ spl0_28
| ~ spl0_2 ),
inference(rat,[],[s987,s874,s36,s23,s870,s363,s852,s94,s95,s96,s20,s1028,s1008,s1005,s997,s21,s48,s1004,s986,s93,s898,s90,s91,s92]) ).
cnf(s1030,plain,
( ~ spl0_56
| spl0_16
| ~ spl0_20
| ~ spl0_9 ),
inference(rat,[],[s717,s658,s182,s183,s184,s35,s1009]) ).
cnf(s1031,plain,
( ~ spl0_15
| spl0_21
| ~ spl0_20
| ~ spl0_2 ),
inference(rat,[],[s467,s30,s1030,s324,s18,s1010,s93,s1029]) ).
cnf(s1032,plain,
( spl0_21
| ~ spl0_20
| ~ spl0_2 ),
inference(rat,[],[s18,s772,s324,s1030,s27,s705,s664,s9,s1031,s93,s898,s90,s91,s92,s1029]) ).
cnf(s1035,plain,
( ~ spl0_53
| ~ spl0_20
| ~ spl0_2 ),
inference(rat,[],[s54,s1024,s992,s47,s17,s785,s784,s964,s178,s179,s180,s93,s1029,s983,s1032]) ).
cnf(s1036,plain,
( ~ spl0_73
| ~ spl0_13 ),
inference(rat,[],[s846,s130,s131,s132]) ).
cnf(s1037,plain,
( ~ spl0_20
| ~ spl0_2 ),
inference(rat,[],[s969,s838,s214,s215,s216,s12,s1024,s38,s1036,s711,s17,s481,s30,s664,s705,s27,s1030,s324,s53,s1035,s995,s1032,s983,s93,s898,s90,s91,s92,s1029]) ).
cnf(s1038,plain,
~ spl0_2,
inference(rat,[],[s784,s964,s772,s178,s179,s180,s47,s18,s53,s1013,s324,s222,s223,s1024,s35,s15,s54,s994,s992,s25,s990,s8,s1037,s1029,s898,s90,s91,s92,s93]) ).
cnf(s1039,plain,
spl0_1,
inference(rat,[],[s1,s1006,s1038]) ).
cnf(s1040,plain,
spl0_9,
inference(rat,[],[s65,s1039]) ).
cnf(s1041,plain,
~ spl0_98,
inference(rat,[],[s64,s1039]) ).
cnf(s1042,plain,
spl0_97,
inference(rat,[],[s63,s1039]) ).
cnf(s1043,plain,
spl0_96,
inference(rat,[],[s62,s1039]) ).
cnf(s1044,plain,
~ spl0_18,
inference(rat,[],[s407,s1041,s1042,s1043]) ).
cnf(s1045,plain,
spl0_39,
inference(rat,[],[s19,s1038,s1040,s1044]) ).
cnf(s1046,plain,
spl0_221,
inference(rat,[],[s228,s1045]) ).
cnf(s1047,plain,
spl0_220,
inference(rat,[],[s227,s1045]) ).
cnf(s1048,plain,
~ spl0_219,
inference(rat,[],[s226,s1045]) ).
cnf(s1049,plain,
~ spl0_37,
inference(rat,[],[s416,s1046,s1047,s1048]) ).
cnf(s1050,plain,
( ~ spl0_85
| ~ spl0_20 ),
inference(rat,[],[s353,s331,s166,s167,s17,s983,s1049,s1040]) ).
cnf(s1051,plain,
~ spl0_20,
inference(rat,[],[s984,s214,s216,s12,s1024,s38,s995,s9,s1036,s668,s711,s710,s27,s981,s282,s283,s50,s1050,s596,s676,s682,s720,s466,s17,s660,s983,s1040,s1042,s1043,s1041,s1046,s1048,s1047,s1049]) ).
cnf(s1052,plain,
spl0_19,
inference(rat,[],[s8,s1040,s1051]) ).
cnf(s1053,plain,
spl0_51,
inference(rat,[],[s25,s1049,s1040,s1051]) ).
cnf(s1055,plain,
$false,
inference(rat,[],[s990,s1052,s1053]) ).
fof(f3327,plain,
$false,
inference(avatar_sat_refutation,[],[s1055]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN447+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.17 % Computer : n019.cluster.edu
% 0.12/0.17 % Model : x86_64 x86_64
% 0.12/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.17 % Memory : 8046.5625MB
% 0.12/0.17 % OS : Linux 6.8.0-71-generic
% 0.12/0.17 % CPULimit : 300
% 0.12/0.17 % WCLimit : 300
% 0.12/0.17 % DateTime : Mon Sep 28 16:04:07 UTC 2026
% 0.12/0.17 % CPUTime :
% 0.12/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.21 Running first-order theorem proving
% 0.12/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.28/1.14 % (4122767)Detected formulas, will run a generic FOF schedule.
% 3.28/1.14 % (4122776)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=858551507:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.28/1.14 % (4122777)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2219563939:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.28/1.14 % (4122773)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=132428252:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.28/1.14 % (4122772)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=3722476745:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.28/1.14 % (4122774)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1863073652:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.28/1.14 % (4122778)dis-21_1_sil=8000:lcm=predicate:random_seed=1819528202:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.28/1.14 % (4122775)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2801356436:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.28/1.14 % (4122776)Instruction limit reached!
% 3.28/1.14 % (4122776)------------------------------
% 3.28/1.14 % (4122776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.14 % (4122776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.14 % (4122776)CaDiCaL version: 2.1.3
% 3.28/1.14 % (4122776)Termination reason: Instruction limit
% 3.28/1.14 % (4122776)Termination phase: Saturation
% 3.28/1.14 % (4122776)Time elapsed: 0.030 s
% 3.28/1.14 % (4122776)Peak memory usage: 88 MB
% 3.28/1.14 % (4122776)Instructions burned: 119 (million)
% 3.28/1.14 % (4122778)First to succeed.
% 3.28/1.14 % (4122778)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4122767"
% 3.28/1.14 % (4122775)Instruction limit reached!
% 3.28/1.14 % (4122775)------------------------------
% 3.28/1.14 % (4122775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.28/1.14 % (4122775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.28/1.14 % (4122775)CaDiCaL version: 2.1.3
% 3.28/1.14 % (4122775)Termination reason: Instruction limit
% 3.28/1.14 % (4122775)Termination phase: Saturation
% 3.28/1.14 % (4122775)Time elapsed: 0.069 s
% 3.28/1.14 % (4122775)Peak memory usage: 90 MB
% 3.28/1.14 % (4122775)Instructions burned: 110 (million)
% 3.28/1.14 % (4122777)Also succeeded, but the first one will report.
% 3.28/1.14 % (4122786)lrs+10_1_sil=8000:sp=occurrence:random_seed=191819746:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 3.28/1.14 % (4122786)Also succeeded, but the first one will report.
% 3.28/1.14 % (4122787)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2525533247:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 3.28/1.14 % (4122778)Refutation found. Thanks to Tanya!
% 3.28/1.14 % SZS status Theorem for theBenchmark
% 3.28/1.14 % SZS output start Proof for theBenchmark
% See solution above
% 4.04/1.34 % (4122778)------------------------------
% 4.04/1.34 % (4122778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.04/1.34 % (4122778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.34 % (4122778)CaDiCaL version: 2.1.3
% 4.04/1.34 % (4122778)Termination reason: Refutation
% 4.04/1.34 % (4122778)Time elapsed: 0.052 s
% 4.04/1.34 % (4122778)Peak memory usage: 91 MB
% 4.04/1.34 % (4122778)Instructions burned: 86 (million)
% 4.04/1.34 % (4122778)------------------------------
% 4.04/1.34 % (4122778)------------------------------
% 4.04/1.34 % (4122767)Success in time 0.486 s
% 4.04/1.34 % Vampire exiting
%------------------------------------------------------------------------------