%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SYN911-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 11:06:46 EDT 2022
% Result : Satisfiable 1.30s 1.51s
% Output : FiniteModel 1.30s
% Verified :
% SZS Type : FiniteModel
% Domain size : 3
% Comments :
%------------------------------------------------------------------------------
% domain size is 3
fof(domain,fi_domain,
! [X] :
( X = "1"
| X = "2"
| X = "3" ) ).
fof(skc41,fi_functors,
skc41 = "1" ).
fof(skc43,fi_functors,
skc43 = "1" ).
fof(skc44,fi_functors,
skc44 = "2" ).
fof(skc45,fi_functors,
skc45 = "3" ).
fof(skc46,fi_functors,
skc46 = "1" ).
fof(skc47,fi_functors,
skc47 = "3" ).
fof(skc48,fi_functors,
skc48 = "3" ).
fof(skc49,fi_functors,
skc49 = "3" ).
fof(skc50,fi_functors,
skc50 = "1" ).
fof(skc51,fi_functors,
skc51 = "3" ).
fof(skc52,fi_functors,
skc52 = "1" ).
fof(skc53,fi_functors,
skc53 = "1" ).
fof(skc54,fi_functors,
skc54 = "1" ).
fof(skc55,fi_functors,
skc55 = "3" ).
fof(skc56,fi_functors,
skc56 = "1" ).
fof(skc57,fi_functors,
skc57 = "1" ).
fof(skc58,fi_functors,
skc58 = "1" ).
fof(skc59,fi_functors,
skc59 = "3" ).
fof(skc61,fi_functors,
skc61 = "1" ).
fof(skc63,fi_functors,
skc63 = "1" ).
fof(skc67,fi_functors,
skc67 = "1" ).
fof(skc68,fi_functors,
skc68 = "1" ).
fof(skc72,fi_functors,
skc72 = "1" ).
fof(skc74,fi_functors,
skc74 = "1" ).
fof(skc75,fi_functors,
skc75 = "1" ).
fof(skc76,fi_functors,
skc76 = "1" ).
fof(skc78,fi_functors,
skc78 = "1" ).
fof(skc79,fi_functors,
skc79 = "1" ).
fof(skc81,fi_functors,
skc81 = "2" ).
fof(skf100,fi_functors,
( skf100("1") = "1"
& skf100("2") = "3"
& skf100("3") = "2" ) ).
fof(skf101,fi_functors,
( skf101("1") = "2"
& skf101("2") = "3"
& skf101("3") = "1" ) ).
fof(skf51,fi_functors,
( skf51("1") = "1"
& skf51("2") = "3"
& skf51("3") = "2" ) ).
fof(skf52,fi_functors,
( skf52("1") = "3"
& skf52("2") = "3"
& skf52("3") = "3" ) ).
fof(skf53,fi_functors,
( skf53("1") = "1"
& skf53("2") = "3"
& skf53("3") = "3" ) ).
fof(skf54,fi_functors,
( skf54("1") = "3"
& skf54("2") = "3"
& skf54("3") = "3" ) ).
fof(skf55,fi_functors,
( skf55("1") = "2"
& skf55("2") = "3"
& skf55("3") = "1" ) ).
fof(skf56,fi_functors,
( skf56("1") = "1"
& skf56("2") = "3"
& skf56("3") = "3" ) ).
fof(skf57,fi_functors,
( skf57("1") = "1"
& skf57("2") = "3"
& skf57("3") = "3" ) ).
fof(skf58,fi_functors,
( skf58("1") = "1"
& skf58("2") = "3"
& skf58("3") = "1" ) ).
fof(skf59,fi_functors,
( skf59("1") = "2"
& skf59("2") = "3"
& skf59("3") = "2" ) ).
fof(skf60,fi_functors,
( skf60("1") = "1"
& skf60("2") = "3"
& skf60("3") = "3" ) ).
fof(skf61,fi_functors,
( skf61("1") = "1"
& skf61("2") = "3"
& skf61("3") = "3" ) ).
fof(skf62,fi_functors,
( skf62("1") = "2"
& skf62("2") = "3"
& skf62("3") = "3" ) ).
fof(skf63,fi_functors,
( skf63("1") = "2"
& skf63("2") = "3"
& skf63("3") = "2" ) ).
fof(skf64,fi_functors,
( skf64("1") = "3"
& skf64("2") = "2"
& skf64("3") = "2" ) ).
fof(skf65,fi_functors,
( skf65("1") = "3"
& skf65("2") = "2"
& skf65("3") = "2" ) ).
fof(skf66,fi_functors,
( skf66("1") = "3"
& skf66("2") = "2"
& skf66("3") = "2" ) ).
fof(skf67,fi_functors,
( skf67("1") = "1"
& skf67("2") = "2"
& skf67("3") = "1" ) ).
fof(skf68,fi_functors,
( skf68("1") = "1"
& skf68("2") = "2"
& skf68("3") = "2" ) ).
fof(skf69,fi_functors,
( skf69("1") = "3"
& skf69("2") = "2"
& skf69("3") = "2" ) ).
fof(skf70,fi_functors,
( skf70("1") = "2"
& skf70("2") = "2"
& skf70("3") = "2" ) ).
fof(skf71,fi_functors,
( skf71("1") = "1"
& skf71("2") = "2"
& skf71("3") = "2" ) ).
fof(skf72,fi_functors,
( skf72("1") = "1"
& skf72("2") = "2"
& skf72("3") = "1" ) ).
fof(skf73,fi_functors,
( skf73("1") = "2"
& skf73("2") = "2"
& skf73("3") = "2" ) ).
fof(skf74,fi_functors,
( skf74("1") = "1"
& skf74("2") = "2"
& skf74("3") = "2" ) ).
fof(skf75,fi_functors,
( skf75("1") = "2"
& skf75("2") = "2"
& skf75("3") = "2" ) ).
fof(skf76,fi_functors,
( skf76("1") = "2"
& skf76("2") = "2"
& skf76("3") = "2" ) ).
fof(skf77,fi_functors,
( skf77("1") = "3"
& skf77("2") = "2"
& skf77("3") = "2" ) ).
fof(skf78,fi_functors,
( skf78("1") = "3"
& skf78("2") = "2"
& skf78("3") = "2" ) ).
fof(skf79,fi_functors,
( skf79("1") = "1"
& skf79("2") = "2"
& skf79("3") = "2" ) ).
fof(skf80,fi_functors,
( skf80("1") = "2"
& skf80("2") = "2"
& skf80("3") = "2" ) ).
fof(skf81,fi_functors,
( skf81("1") = "1"
& skf81("2") = "2"
& skf81("3") = "2" ) ).
fof(skf82,fi_functors,
( skf82("1") = "2"
& skf82("2") = "2"
& skf82("3") = "2" ) ).
fof(skf83,fi_functors,
( skf83("1") = "3"
& skf83("2") = "2"
& skf83("3") = "2" ) ).
fof(skf84,fi_functors,
( skf84("1") = "1"
& skf84("2") = "2"
& skf84("3") = "2" ) ).
fof(skf85,fi_functors,
( skf85("1") = "3"
& skf85("2") = "2"
& skf85("3") = "2" ) ).
fof(skf86,fi_functors,
( skf86("1") = "1"
& skf86("2") = "2"
& skf86("3") = "2" ) ).
fof(skf87,fi_functors,
( skf87("1") = "1"
& skf87("2") = "2"
& skf87("3") = "2" ) ).
fof(skf88,fi_functors,
( skf88("1") = "1"
& skf88("2") = "3"
& skf88("3") = "2" ) ).
fof(skf89,fi_functors,
( skf89("1") = "1"
& skf89("2") = "3"
& skf89("3") = "2" ) ).
fof(skf90,fi_functors,
( skf90("1") = "1"
& skf90("2") = "3"
& skf90("3") = "2" ) ).
fof(skf91,fi_functors,
( skf91("1") = "1"
& skf91("2") = "3"
& skf91("3") = "2" ) ).
fof(skf92,fi_functors,
( skf92("1") = "1"
& skf92("2") = "3"
& skf92("3") = "2" ) ).
fof(skf93,fi_functors,
( skf93("1") = "1"
& skf93("2") = "3"
& skf93("3") = "2" ) ).
fof(skf94,fi_functors,
( skf94("1") = "1"
& skf94("2") = "3"
& skf94("3") = "2" ) ).
fof(skf95,fi_functors,
( skf95("1") = "1"
& skf95("2") = "3"
& skf95("3") = "2" ) ).
fof(skf96,fi_functors,
( skf96("1") = "1"
& skf96("2") = "3"
& skf96("3") = "2" ) ).
fof(skf97,fi_functors,
( skf97("1") = "1"
& skf97("2") = "3"
& skf97("3") = "2" ) ).
fof(skf98,fi_functors,
( skf98("1") = "1"
& skf98("2") = "3"
& skf98("3") = "2" ) ).
fof(skf99,fi_functors,
( skf99("1") = "1"
& skf99("2") = "3"
& skf99("3") = "2" ) ).
fof(ssPv1,fi_predicates,
( ( ssPv1("1")
<=> $false )
& ( ssPv1("2")
<=> $true )
& ( ssPv1("3")
<=> $true ) ) ).
fof(ssPv10,fi_predicates,
! [X1] :
( ssPv10(X1)
<=> $false ) ).
fof(ssPv11,fi_predicates,
( ( ssPv11("1")
<=> $true )
& ( ssPv11("2")
<=> $true )
& ( ssPv11("3")
<=> $true ) ) ).
fof(ssPv12,fi_predicates,
( ( ssPv12("1")
<=> $false )
& ( ssPv12("2")
<=> $false )
& ( ssPv12("3")
<=> $false ) ) ).
fof(ssPv13,fi_predicates,
( ( ssPv13("1")
<=> $false )
& ( ssPv13("2")
<=> $true )
& ( ssPv13("3")
<=> $false ) ) ).
fof(ssPv14,fi_predicates,
( ( ssPv14("1")
<=> $true )
& ( ssPv14("2")
<=> $true )
& ( ssPv14("3")
<=> $false ) ) ).
fof(ssPv15,fi_predicates,
( ( ssPv15("1")
<=> $true )
& ( ssPv15("2")
<=> $true )
& ( ssPv15("3")
<=> $false ) ) ).
fof(ssPv16,fi_predicates,
( ( ssPv16("1")
<=> $true )
& ( ssPv16("2")
<=> $true )
& ( ssPv16("3")
<=> $false ) ) ).
fof(ssPv17,fi_predicates,
! [X1] :
( ssPv17(X1)
<=> $false ) ).
fof(ssPv18,fi_predicates,
! [X1] :
( ssPv18(X1)
<=> $false ) ).
fof(ssPv19,fi_predicates,
( ( ssPv19("1")
<=> $true )
& ( ssPv19("2")
<=> $true )
& ( ssPv19("3")
<=> $true ) ) ).
fof(ssPv2,fi_predicates,
! [X1] :
( ssPv2(X1)
<=> $true ) ).
fof(ssPv20,fi_predicates,
( ( ssPv20("1")
<=> $true )
& ( ssPv20("2")
<=> $false )
& ( ssPv20("3")
<=> $false ) ) ).
fof(ssPv21,fi_predicates,
( ( ssPv21("1")
<=> $true )
& ( ssPv21("2")
<=> $true )
& ( ssPv21("3")
<=> $false ) ) ).
fof(ssPv22,fi_predicates,
( ( ssPv22("1")
<=> $true )
& ( ssPv22("2")
<=> $true )
& ( ssPv22("3")
<=> $false ) ) ).
fof(ssPv23,fi_predicates,
( ( ssPv23("1")
<=> $true )
& ( ssPv23("2")
<=> $true )
& ( ssPv23("3")
<=> $false ) ) ).
fof(ssPv24,fi_predicates,
( ( ssPv24("1")
<=> $true )
& ( ssPv24("2")
<=> $true )
& ( ssPv24("3")
<=> $false ) ) ).
fof(ssPv25,fi_predicates,
( ( ssPv25("1")
<=> $true )
& ( ssPv25("2")
<=> $false )
& ( ssPv25("3")
<=> $false ) ) ).
fof(ssPv26,fi_predicates,
( ( ssPv26("1")
<=> $true )
& ( ssPv26("2")
<=> $true )
& ( ssPv26("3")
<=> $true ) ) ).
fof(ssPv27,fi_predicates,
( ( ssPv27("1")
<=> $false )
& ( ssPv27("2")
<=> $false )
& ( ssPv27("3")
<=> $false ) ) ).
fof(ssPv28,fi_predicates,
( ( ssPv28("1")
<=> $false )
& ( ssPv28("2")
<=> $false )
& ( ssPv28("3")
<=> $false ) ) ).
fof(ssPv3,fi_predicates,
( ( ssPv3("1")
<=> $true )
& ( ssPv3("2")
<=> $false )
& ( ssPv3("3")
<=> $false ) ) ).
fof(ssPv4,fi_predicates,
( ( ssPv4("1")
<=> $false )
& ( ssPv4("2")
<=> $false )
& ( ssPv4("3")
<=> $false ) ) ).
fof(ssPv5,fi_predicates,
( ( ssPv5("1")
<=> $false )
& ( ssPv5("2")
<=> $true )
& ( ssPv5("3")
<=> $false ) ) ).
fof(ssPv6,fi_predicates,
( ( ssPv6("1")
<=> $true )
& ( ssPv6("2")
<=> $true )
& ( ssPv6("3")
<=> $false ) ) ).
fof(ssPv7,fi_predicates,
( ( ssPv7("1")
<=> $false )
& ( ssPv7("2")
<=> $true )
& ( ssPv7("3")
<=> $false ) ) ).
fof(ssPv8,fi_predicates,
( ( ssPv8("1")
<=> $true )
& ( ssPv8("2")
<=> $true )
& ( ssPv8("3")
<=> $false ) ) ).
fof(ssPv9,fi_predicates,
( ( ssPv9("1")
<=> $true )
& ( ssPv9("2")
<=> $true )
& ( ssPv9("3")
<=> $true ) ) ).
fof(ssRr,fi_predicates,
( ( ssRr("1","1")
<=> $true )
& ( ssRr("1","2")
<=> $false )
& ( ssRr("1","3")
<=> $false )
& ( ssRr("2","1")
<=> $false )
& ( ssRr("2","2")
<=> $true )
& ( ssRr("2","3")
<=> $true )
& ( ssRr("3","1")
<=> $false )
& ( ssRr("3","2")
<=> $true )
& ( ssRr("3","3")
<=> $false ) ) ).
fof(ssSkC0,fi_predicates,
( ssSkC0
<=> $false ) ).
fof(ssSkC1,fi_predicates,
( ssSkC1
<=> $false ) ).
fof(ssSkC10,fi_predicates,
( ssSkC10
<=> $false ) ).
fof(ssSkC11,fi_predicates,
( ssSkC11
<=> $false ) ).
fof(ssSkC12,fi_predicates,
( ssSkC12
<=> $false ) ).
fof(ssSkC13,fi_predicates,
( ssSkC13
<=> $false ) ).
fof(ssSkC14,fi_predicates,
( ssSkC14
<=> $false ) ).
fof(ssSkC15,fi_predicates,
( ssSkC15
<=> $false ) ).
fof(ssSkC16,fi_predicates,
( ssSkC16
<=> $false ) ).
fof(ssSkC17,fi_predicates,
( ssSkC17
<=> $false ) ).
fof(ssSkC18,fi_predicates,
( ssSkC18
<=> $false ) ).
fof(ssSkC19,fi_predicates,
( ssSkC19
<=> $false ) ).
fof(ssSkC2,fi_predicates,
( ssSkC2
<=> $false ) ).
fof(ssSkC20,fi_predicates,
( ssSkC20
<=> $false ) ).
fof(ssSkC21,fi_predicates,
( ssSkC21
<=> $false ) ).
fof(ssSkC22,fi_predicates,
( ssSkC22
<=> $false ) ).
fof(ssSkC23,fi_predicates,
( ssSkC23
<=> $false ) ).
fof(ssSkC24,fi_predicates,
( ssSkC24
<=> $false ) ).
fof(ssSkC25,fi_predicates,
( ssSkC25
<=> $false ) ).
fof(ssSkC26,fi_predicates,
( ssSkC26
<=> $false ) ).
fof(ssSkC27,fi_predicates,
( ssSkC27
<=> $false ) ).
fof(ssSkC28,fi_predicates,
( ssSkC28
<=> $false ) ).
fof(ssSkC29,fi_predicates,
( ssSkC29
<=> $false ) ).
fof(ssSkC3,fi_predicates,
( ssSkC3
<=> $false ) ).
fof(ssSkC30,fi_predicates,
( ssSkC30
<=> $false ) ).
fof(ssSkC31,fi_predicates,
( ssSkC31
<=> $false ) ).
fof(ssSkC32,fi_predicates,
( ssSkC32
<=> $false ) ).
fof(ssSkC33,fi_predicates,
( ssSkC33
<=> $false ) ).
fof(ssSkC34,fi_predicates,
( ssSkC34
<=> $false ) ).
fof(ssSkC35,fi_predicates,
( ssSkC35
<=> $false ) ).
fof(ssSkC36,fi_predicates,
( ssSkC36
<=> $false ) ).
fof(ssSkC37,fi_predicates,
( ssSkC37
<=> $false ) ).
fof(ssSkC38,fi_predicates,
( ssSkC38
<=> $false ) ).
fof(ssSkC39,fi_predicates,
( ssSkC39
<=> $false ) ).
fof(ssSkC4,fi_predicates,
( ssSkC4
<=> $false ) ).
fof(ssSkC40,fi_predicates,
( ssSkC40
<=> $false ) ).
fof(ssSkC5,fi_predicates,
( ssSkC5
<=> $false ) ).
fof(ssSkC6,fi_predicates,
( ssSkC6
<=> $false ) ).
fof(ssSkC7,fi_predicates,
( ssSkC7
<=> $false ) ).
fof(ssSkC8,fi_predicates,
( ssSkC8
<=> $false ) ).
fof(ssSkC9,fi_predicates,
( ssSkC9
<=> $false ) ).
fof(ssSkP0,fi_predicates,
( ( ssSkP0("1","1")
<=> $true )
& ( ssSkP0("1","2")
<=> $true )
& ( ssSkP0("1","3")
<=> $true )
& ( ssSkP0("2","1")
<=> $false )
& ( ssSkP0("2","2")
<=> $true )
& ( ssSkP0("2","3")
<=> $true )
& ( ssSkP0("3","1")
<=> $false )
& ( ssSkP0("3","2")
<=> $true )
& ( ssSkP0("3","3")
<=> $true ) ) ).
fof(ssSkP1,fi_predicates,
( ( ssSkP1("1","1")
<=> $true )
& ( ssSkP1("1","2")
<=> $true )
& ( ssSkP1("1","3")
<=> $true )
& ( ssSkP1("2","1")
<=> $false )
& ( ssSkP1("2","2")
<=> $true )
& ( ssSkP1("2","3")
<=> $true )
& ( ssSkP1("3","1")
<=> $false )
& ( ssSkP1("3","2")
<=> $true )
& ( ssSkP1("3","3")
<=> $true ) ) ).
fof(ssSkP10,fi_predicates,
( ( ssSkP10("1")
<=> $true )
& ( ssSkP10("2")
<=> $false )
& ( ssSkP10("3")
<=> $false ) ) ).
fof(ssSkP100,fi_predicates,
( ( ssSkP100("1")
<=> $true )
& ( ssSkP100("2")
<=> $true )
& ( ssSkP100("3")
<=> $true ) ) ).
fof(ssSkP1000,fi_predicates,
( ( ssSkP1000("1")
<=> $false )
& ( ssSkP1000("2")
<=> $false )
& ( ssSkP1000("3")
<=> $false ) ) ).
fof(ssSkP1001,fi_predicates,
( ( ssSkP1001("1")
<=> $false )
& ( ssSkP1001("2")
<=> $false )
& ( ssSkP1001("3")
<=> $false ) ) ).
fof(ssSkP1002,fi_predicates,
( ( ssSkP1002("1")
<=> $false )
& ( ssSkP1002("2")
<=> $false )
& ( ssSkP1002("3")
<=> $false ) ) ).
fof(ssSkP1003,fi_predicates,
( ( ssSkP1003("1")
<=> $false )
& ( ssSkP1003("2")
<=> $false )
& ( ssSkP1003("3")
<=> $false ) ) ).
fof(ssSkP1004,fi_predicates,
( ( ssSkP1004("1")
<=> $false )
& ( ssSkP1004("2")
<=> $false )
& ( ssSkP1004("3")
<=> $false ) ) ).
fof(ssSkP1005,fi_predicates,
( ( ssSkP1005("1")
<=> $true )
& ( ssSkP1005("2")
<=> $true )
& ( ssSkP1005("3")
<=> $true ) ) ).
fof(ssSkP1006,fi_predicates,
( ( ssSkP1006("1")
<=> $true )
& ( ssSkP1006("2")
<=> $true )
& ( ssSkP1006("3")
<=> $true ) ) ).
fof(ssSkP1007,fi_predicates,
( ( ssSkP1007("1")
<=> $true )
& ( ssSkP1007("2")
<=> $true )
& ( ssSkP1007("3")
<=> $true ) ) ).
fof(ssSkP1008,fi_predicates,
( ( ssSkP1008("1")
<=> $true )
& ( ssSkP1008("2")
<=> $true )
& ( ssSkP1008("3")
<=> $true ) ) ).
fof(ssSkP1009,fi_predicates,
( ( ssSkP1009("1")
<=> $true )
& ( ssSkP1009("2")
<=> $true )
& ( ssSkP1009("3")
<=> $true ) ) ).
fof(ssSkP101,fi_predicates,
( ( ssSkP101("1")
<=> $false )
& ( ssSkP101("2")
<=> $true )
& ( ssSkP101("3")
<=> $false ) ) ).
fof(ssSkP1010,fi_predicates,
( ( ssSkP1010("1")
<=> $true )
& ( ssSkP1010("2")
<=> $true )
& ( ssSkP1010("3")
<=> $false ) ) ).
fof(ssSkP1011,fi_predicates,
( ( ssSkP1011("1")
<=> $true )
& ( ssSkP1011("2")
<=> $true )
& ( ssSkP1011("3")
<=> $true ) ) ).
fof(ssSkP1012,fi_predicates,
( ( ssSkP1012("1")
<=> $true )
& ( ssSkP1012("2")
<=> $true )
& ( ssSkP1012("3")
<=> $true ) ) ).
fof(ssSkP1013,fi_predicates,
( ( ssSkP1013("1")
<=> $true )
& ( ssSkP1013("2")
<=> $true )
& ( ssSkP1013("3")
<=> $true ) ) ).
fof(ssSkP1014,fi_predicates,
( ( ssSkP1014("1")
<=> $true )
& ( ssSkP1014("2")
<=> $true )
& ( ssSkP1014("3")
<=> $true ) ) ).
fof(ssSkP1015,fi_predicates,
( ( ssSkP1015("1")
<=> $true )
& ( ssSkP1015("2")
<=> $true )
& ( ssSkP1015("3")
<=> $true ) ) ).
fof(ssSkP1016,fi_predicates,
( ( ssSkP1016("1")
<=> $true )
& ( ssSkP1016("2")
<=> $true )
& ( ssSkP1016("3")
<=> $true ) ) ).
fof(ssSkP1017,fi_predicates,
( ( ssSkP1017("1")
<=> $true )
& ( ssSkP1017("2")
<=> $true )
& ( ssSkP1017("3")
<=> $true ) ) ).
fof(ssSkP1018,fi_predicates,
( ( ssSkP1018("1")
<=> $true )
& ( ssSkP1018("2")
<=> $false )
& ( ssSkP1018("3")
<=> $false ) ) ).
fof(ssSkP1019,fi_predicates,
( ( ssSkP1019("1")
<=> $true )
& ( ssSkP1019("2")
<=> $false )
& ( ssSkP1019("3")
<=> $false ) ) ).
fof(ssSkP102,fi_predicates,
( ( ssSkP102("1","1")
<=> $true )
& ( ssSkP102("1","2")
<=> $true )
& ( ssSkP102("1","3")
<=> $true )
& ( ssSkP102("2","1")
<=> $true )
& ( ssSkP102("2","2")
<=> $true )
& ( ssSkP102("2","3")
<=> $true )
& ( ssSkP102("3","1")
<=> $true )
& ( ssSkP102("3","2")
<=> $true )
& ( ssSkP102("3","3")
<=> $true ) ) ).
fof(ssSkP1020,fi_predicates,
( ( ssSkP1020("1")
<=> $true )
& ( ssSkP1020("2")
<=> $false )
& ( ssSkP1020("3")
<=> $false ) ) ).
fof(ssSkP1021,fi_predicates,
( ( ssSkP1021("1")
<=> $true )
& ( ssSkP1021("2")
<=> $false )
& ( ssSkP1021("3")
<=> $false ) ) ).
fof(ssSkP1022,fi_predicates,
( ( ssSkP1022("1")
<=> $true )
& ( ssSkP1022("2")
<=> $false )
& ( ssSkP1022("3")
<=> $false ) ) ).
fof(ssSkP1023,fi_predicates,
( ( ssSkP1023("1")
<=> $true )
& ( ssSkP1023("2")
<=> $false )
& ( ssSkP1023("3")
<=> $false ) ) ).
fof(ssSkP1024,fi_predicates,
( ( ssSkP1024("1")
<=> $true )
& ( ssSkP1024("2")
<=> $false )
& ( ssSkP1024("3")
<=> $false ) ) ).
fof(ssSkP1025,fi_predicates,
! [X1,X2] :
( ssSkP1025(X1,X2)
<=> $true ) ).
fof(ssSkP1026,fi_predicates,
! [X1,X2] :
( ssSkP1026(X1,X2)
<=> $true ) ).
fof(ssSkP1027,fi_predicates,
! [X1] :
( ssSkP1027(X1)
<=> $true ) ).
fof(ssSkP1028,fi_predicates,
! [X1] :
( ssSkP1028(X1)
<=> $true ) ).
fof(ssSkP1029,fi_predicates,
! [X1] :
( ssSkP1029(X1)
<=> $true ) ).
fof(ssSkP103,fi_predicates,
( ( ssSkP103("1","1")
<=> $true )
& ( ssSkP103("1","2")
<=> $true )
& ( ssSkP103("1","3")
<=> $true )
& ( ssSkP103("2","1")
<=> $true )
& ( ssSkP103("2","2")
<=> $true )
& ( ssSkP103("2","3")
<=> $true )
& ( ssSkP103("3","1")
<=> $true )
& ( ssSkP103("3","2")
<=> $true )
& ( ssSkP103("3","3")
<=> $true ) ) ).
fof(ssSkP1030,fi_predicates,
! [X1] :
( ssSkP1030(X1)
<=> $true ) ).
fof(ssSkP1031,fi_predicates,
! [X1] :
( ssSkP1031(X1)
<=> $true ) ).
fof(ssSkP1032,fi_predicates,
! [X1] :
( ssSkP1032(X1)
<=> $true ) ).
fof(ssSkP1033,fi_predicates,
! [X1] :
( ssSkP1033(X1)
<=> $true ) ).
fof(ssSkP1034,fi_predicates,
! [X1] :
( ssSkP1034(X1)
<=> $true ) ).
fof(ssSkP1035,fi_predicates,
! [X1] :
( ssSkP1035(X1)
<=> $true ) ).
fof(ssSkP1036,fi_predicates,
! [X1] :
( ssSkP1036(X1)
<=> $true ) ).
fof(ssSkP1037,fi_predicates,
! [X1] :
( ssSkP1037(X1)
<=> $true ) ).
fof(ssSkP1038,fi_predicates,
! [X1] :
( ssSkP1038(X1)
<=> $true ) ).
fof(ssSkP1039,fi_predicates,
! [X1] :
( ssSkP1039(X1)
<=> $true ) ).
fof(ssSkP104,fi_predicates,
( ( ssSkP104("1")
<=> $false )
& ( ssSkP104("2")
<=> $true )
& ( ssSkP104("3")
<=> $true ) ) ).
fof(ssSkP1040,fi_predicates,
! [X1] :
( ssSkP1040(X1)
<=> $true ) ).
fof(ssSkP1041,fi_predicates,
! [X1] :
( ssSkP1041(X1)
<=> $true ) ).
fof(ssSkP1042,fi_predicates,
! [X1] :
( ssSkP1042(X1)
<=> $true ) ).
fof(ssSkP1043,fi_predicates,
! [X1] :
( ssSkP1043(X1)
<=> $true ) ).
fof(ssSkP1044,fi_predicates,
! [X1] :
( ssSkP1044(X1)
<=> $true ) ).
fof(ssSkP1045,fi_predicates,
! [X1] :
( ssSkP1045(X1)
<=> $true ) ).
fof(ssSkP1046,fi_predicates,
! [X1] :
( ssSkP1046(X1)
<=> $true ) ).
fof(ssSkP1047,fi_predicates,
! [X1] :
( ssSkP1047(X1)
<=> $true ) ).
fof(ssSkP1048,fi_predicates,
! [X1] :
( ssSkP1048(X1)
<=> $true ) ).
fof(ssSkP1049,fi_predicates,
! [X1] :
( ssSkP1049(X1)
<=> $true ) ).
fof(ssSkP105,fi_predicates,
( ( ssSkP105("1")
<=> $false )
& ( ssSkP105("2")
<=> $true )
& ( ssSkP105("3")
<=> $false ) ) ).
fof(ssSkP1050,fi_predicates,
! [X1] :
( ssSkP1050(X1)
<=> $true ) ).
fof(ssSkP1051,fi_predicates,
! [X1] :
( ssSkP1051(X1)
<=> $true ) ).
fof(ssSkP1052,fi_predicates,
! [X1] :
( ssSkP1052(X1)
<=> $true ) ).
fof(ssSkP1053,fi_predicates,
! [X1] :
( ssSkP1053(X1)
<=> $true ) ).
fof(ssSkP1054,fi_predicates,
! [X1] :
( ssSkP1054(X1)
<=> $true ) ).
fof(ssSkP1055,fi_predicates,
! [X1] :
( ssSkP1055(X1)
<=> $true ) ).
fof(ssSkP1056,fi_predicates,
! [X1] :
( ssSkP1056(X1)
<=> $true ) ).
fof(ssSkP1057,fi_predicates,
( ( ssSkP1057("1","1")
<=> $true )
& ( ssSkP1057("1","2")
<=> $true )
& ( ssSkP1057("1","3")
<=> $true )
& ( ssSkP1057("2","1")
<=> $true )
& ( ssSkP1057("2","2")
<=> $true )
& ( ssSkP1057("2","3")
<=> $true )
& ( ssSkP1057("3","1")
<=> $true )
& ( ssSkP1057("3","2")
<=> $true )
& ( ssSkP1057("3","3")
<=> $true ) ) ).
fof(ssSkP1058,fi_predicates,
( ( ssSkP1058("1","1")
<=> $true )
& ( ssSkP1058("1","2")
<=> $true )
& ( ssSkP1058("1","3")
<=> $true )
& ( ssSkP1058("2","1")
<=> $true )
& ( ssSkP1058("2","2")
<=> $true )
& ( ssSkP1058("2","3")
<=> $true )
& ( ssSkP1058("3","1")
<=> $true )
& ( ssSkP1058("3","2")
<=> $true )
& ( ssSkP1058("3","3")
<=> $true ) ) ).
fof(ssSkP1059,fi_predicates,
( ( ssSkP1059("1")
<=> $false )
& ( ssSkP1059("2")
<=> $false )
& ( ssSkP1059("3")
<=> $false ) ) ).
fof(ssSkP106,fi_predicates,
( ( ssSkP106("1")
<=> $false )
& ( ssSkP106("2")
<=> $true )
& ( ssSkP106("3")
<=> $true ) ) ).
fof(ssSkP1060,fi_predicates,
( ( ssSkP1060("1")
<=> $false )
& ( ssSkP1060("2")
<=> $false )
& ( ssSkP1060("3")
<=> $false ) ) ).
fof(ssSkP1061,fi_predicates,
( ( ssSkP1061("1")
<=> $false )
& ( ssSkP1061("2")
<=> $false )
& ( ssSkP1061("3")
<=> $false ) ) ).
fof(ssSkP1062,fi_predicates,
( ( ssSkP1062("1")
<=> $false )
& ( ssSkP1062("2")
<=> $false )
& ( ssSkP1062("3")
<=> $false ) ) ).
fof(ssSkP1063,fi_predicates,
( ( ssSkP1063("1")
<=> $false )
& ( ssSkP1063("2")
<=> $false )
& ( ssSkP1063("3")
<=> $false ) ) ).
fof(ssSkP1064,fi_predicates,
( ( ssSkP1064("1")
<=> $false )
& ( ssSkP1064("2")
<=> $false )
& ( ssSkP1064("3")
<=> $false ) ) ).
fof(ssSkP1065,fi_predicates,
( ( ssSkP1065("1")
<=> $true )
& ( ssSkP1065("2")
<=> $true )
& ( ssSkP1065("3")
<=> $true ) ) ).
fof(ssSkP1066,fi_predicates,
( ( ssSkP1066("1")
<=> $true )
& ( ssSkP1066("2")
<=> $true )
& ( ssSkP1066("3")
<=> $true ) ) ).
fof(ssSkP1067,fi_predicates,
( ( ssSkP1067("1")
<=> $true )
& ( ssSkP1067("2")
<=> $true )
& ( ssSkP1067("3")
<=> $true ) ) ).
fof(ssSkP1068,fi_predicates,
( ( ssSkP1068("1")
<=> $true )
& ( ssSkP1068("2")
<=> $true )
& ( ssSkP1068("3")
<=> $true ) ) ).
fof(ssSkP1069,fi_predicates,
( ( ssSkP1069("1")
<=> $true )
& ( ssSkP1069("2")
<=> $true )
& ( ssSkP1069("3")
<=> $true ) ) ).
fof(ssSkP107,fi_predicates,
( ( ssSkP107("1")
<=> $false )
& ( ssSkP107("2")
<=> $true )
& ( ssSkP107("3")
<=> $true ) ) ).
fof(ssSkP1070,fi_predicates,
( ( ssSkP1070("1")
<=> $true )
& ( ssSkP1070("2")
<=> $true )
& ( ssSkP1070("3")
<=> $true ) ) ).
fof(ssSkP1071,fi_predicates,
( ( ssSkP1071("1")
<=> $false )
& ( ssSkP1071("2")
<=> $true )
& ( ssSkP1071("3")
<=> $true ) ) ).
fof(ssSkP1072,fi_predicates,
( ( ssSkP1072("1")
<=> $true )
& ( ssSkP1072("2")
<=> $true )
& ( ssSkP1072("3")
<=> $true ) ) ).
fof(ssSkP1073,fi_predicates,
( ( ssSkP1073("1")
<=> $true )
& ( ssSkP1073("2")
<=> $true )
& ( ssSkP1073("3")
<=> $true ) ) ).
fof(ssSkP1074,fi_predicates,
( ( ssSkP1074("1")
<=> $true )
& ( ssSkP1074("2")
<=> $true )
& ( ssSkP1074("3")
<=> $true ) ) ).
fof(ssSkP1075,fi_predicates,
( ( ssSkP1075("1")
<=> $true )
& ( ssSkP1075("2")
<=> $true )
& ( ssSkP1075("3")
<=> $true ) ) ).
fof(ssSkP1076,fi_predicates,
( ( ssSkP1076("1")
<=> $true )
& ( ssSkP1076("2")
<=> $true )
& ( ssSkP1076("3")
<=> $true ) ) ).
fof(ssSkP1077,fi_predicates,
( ( ssSkP1077("1")
<=> $true )
& ( ssSkP1077("2")
<=> $true )
& ( ssSkP1077("3")
<=> $true ) ) ).
fof(ssSkP1078,fi_predicates,
( ( ssSkP1078("1")
<=> $true )
& ( ssSkP1078("2")
<=> $true )
& ( ssSkP1078("3")
<=> $true ) ) ).
fof(ssSkP1079,fi_predicates,
( ( ssSkP1079("1")
<=> $true )
& ( ssSkP1079("2")
<=> $true )
& ( ssSkP1079("3")
<=> $true ) ) ).
fof(ssSkP108,fi_predicates,
( ( ssSkP108("1")
<=> $false )
& ( ssSkP108("2")
<=> $true )
& ( ssSkP108("3")
<=> $true ) ) ).
fof(ssSkP1080,fi_predicates,
( ( ssSkP1080("1")
<=> $true )
& ( ssSkP1080("2")
<=> $true )
& ( ssSkP1080("3")
<=> $true ) ) ).
fof(ssSkP1081,fi_predicates,
( ( ssSkP1081("1")
<=> $true )
& ( ssSkP1081("2")
<=> $true )
& ( ssSkP1081("3")
<=> $true ) ) ).
fof(ssSkP1082,fi_predicates,
( ( ssSkP1082("1")
<=> $true )
& ( ssSkP1082("2")
<=> $true )
& ( ssSkP1082("3")
<=> $true ) ) ).
fof(ssSkP1083,fi_predicates,
( ( ssSkP1083("1")
<=> $true )
& ( ssSkP1083("2")
<=> $true )
& ( ssSkP1083("3")
<=> $true ) ) ).
fof(ssSkP1084,fi_predicates,
( ( ssSkP1084("1")
<=> $true )
& ( ssSkP1084("2")
<=> $true )
& ( ssSkP1084("3")
<=> $true ) ) ).
fof(ssSkP1085,fi_predicates,
( ( ssSkP1085("1")
<=> $true )
& ( ssSkP1085("2")
<=> $true )
& ( ssSkP1085("3")
<=> $true ) ) ).
fof(ssSkP1086,fi_predicates,
( ( ssSkP1086("1")
<=> $true )
& ( ssSkP1086("2")
<=> $false )
& ( ssSkP1086("3")
<=> $false ) ) ).
fof(ssSkP1087,fi_predicates,
( ( ssSkP1087("1","1")
<=> $true )
& ( ssSkP1087("1","2")
<=> $true )
& ( ssSkP1087("1","3")
<=> $true )
& ( ssSkP1087("2","1")
<=> $true )
& ( ssSkP1087("2","2")
<=> $true )
& ( ssSkP1087("2","3")
<=> $true )
& ( ssSkP1087("3","1")
<=> $true )
& ( ssSkP1087("3","2")
<=> $true )
& ( ssSkP1087("3","3")
<=> $true ) ) ).
fof(ssSkP1088,fi_predicates,
( ( ssSkP1088("1","1")
<=> $true )
& ( ssSkP1088("1","2")
<=> $true )
& ( ssSkP1088("1","3")
<=> $true )
& ( ssSkP1088("2","1")
<=> $true )
& ( ssSkP1088("2","2")
<=> $true )
& ( ssSkP1088("2","3")
<=> $true )
& ( ssSkP1088("3","1")
<=> $true )
& ( ssSkP1088("3","2")
<=> $true )
& ( ssSkP1088("3","3")
<=> $true ) ) ).
fof(ssSkP1089,fi_predicates,
( ( ssSkP1089("1")
<=> $false )
& ( ssSkP1089("2")
<=> $true )
& ( ssSkP1089("3")
<=> $true ) ) ).
fof(ssSkP109,fi_predicates,
( ( ssSkP109("1")
<=> $false )
& ( ssSkP109("2")
<=> $true )
& ( ssSkP109("3")
<=> $true ) ) ).
fof(ssSkP1090,fi_predicates,
( ( ssSkP1090("1")
<=> $false )
& ( ssSkP1090("2")
<=> $true )
& ( ssSkP1090("3")
<=> $true ) ) ).
fof(ssSkP1091,fi_predicates,
( ( ssSkP1091("1")
<=> $false )
& ( ssSkP1091("2")
<=> $true )
& ( ssSkP1091("3")
<=> $true ) ) ).
fof(ssSkP1092,fi_predicates,
( ( ssSkP1092("1")
<=> $false )
& ( ssSkP1092("2")
<=> $true )
& ( ssSkP1092("3")
<=> $true ) ) ).
fof(ssSkP1093,fi_predicates,
( ( ssSkP1093("1")
<=> $false )
& ( ssSkP1093("2")
<=> $true )
& ( ssSkP1093("3")
<=> $true ) ) ).
fof(ssSkP1094,fi_predicates,
( ( ssSkP1094("1")
<=> $true )
& ( ssSkP1094("2")
<=> $true )
& ( ssSkP1094("3")
<=> $true ) ) ).
fof(ssSkP1095,fi_predicates,
( ( ssSkP1095("1")
<=> $true )
& ( ssSkP1095("2")
<=> $true )
& ( ssSkP1095("3")
<=> $true ) ) ).
fof(ssSkP1096,fi_predicates,
( ( ssSkP1096("1")
<=> $true )
& ( ssSkP1096("2")
<=> $true )
& ( ssSkP1096("3")
<=> $true ) ) ).
fof(ssSkP1097,fi_predicates,
( ( ssSkP1097("1")
<=> $true )
& ( ssSkP1097("2")
<=> $true )
& ( ssSkP1097("3")
<=> $true ) ) ).
fof(ssSkP1098,fi_predicates,
( ( ssSkP1098("1")
<=> $true )
& ( ssSkP1098("2")
<=> $true )
& ( ssSkP1098("3")
<=> $true ) ) ).
fof(ssSkP1099,fi_predicates,
( ( ssSkP1099("1")
<=> $true )
& ( ssSkP1099("2")
<=> $true )
& ( ssSkP1099("3")
<=> $true ) ) ).
fof(ssSkP11,fi_predicates,
( ( ssSkP11("1")
<=> $true )
& ( ssSkP11("2")
<=> $false )
& ( ssSkP11("3")
<=> $false ) ) ).
fof(ssSkP110,fi_predicates,
( ( ssSkP110("1")
<=> $false )
& ( ssSkP110("2")
<=> $true )
& ( ssSkP110("3")
<=> $true ) ) ).
fof(ssSkP1100,fi_predicates,
( ( ssSkP1100("1")
<=> $true )
& ( ssSkP1100("2")
<=> $true )
& ( ssSkP1100("3")
<=> $true ) ) ).
fof(ssSkP1101,fi_predicates,
( ( ssSkP1101("1")
<=> $true )
& ( ssSkP1101("2")
<=> $true )
& ( ssSkP1101("3")
<=> $true ) ) ).
fof(ssSkP1102,fi_predicates,
( ( ssSkP1102("1")
<=> $true )
& ( ssSkP1102("2")
<=> $true )
& ( ssSkP1102("3")
<=> $true ) ) ).
fof(ssSkP1103,fi_predicates,
( ( ssSkP1103("1")
<=> $true )
& ( ssSkP1103("2")
<=> $true )
& ( ssSkP1103("3")
<=> $true ) ) ).
fof(ssSkP1104,fi_predicates,
( ( ssSkP1104("1")
<=> $false )
& ( ssSkP1104("2")
<=> $true )
& ( ssSkP1104("3")
<=> $true ) ) ).
fof(ssSkP1105,fi_predicates,
( ( ssSkP1105("1")
<=> $true )
& ( ssSkP1105("2")
<=> $true )
& ( ssSkP1105("3")
<=> $true ) ) ).
fof(ssSkP1106,fi_predicates,
( ( ssSkP1106("1")
<=> $true )
& ( ssSkP1106("2")
<=> $true )
& ( ssSkP1106("3")
<=> $true ) ) ).
fof(ssSkP1107,fi_predicates,
( ( ssSkP1107("1")
<=> $true )
& ( ssSkP1107("2")
<=> $true )
& ( ssSkP1107("3")
<=> $true ) ) ).
fof(ssSkP1108,fi_predicates,
( ( ssSkP1108("1")
<=> $true )
& ( ssSkP1108("2")
<=> $true )
& ( ssSkP1108("3")
<=> $true ) ) ).
fof(ssSkP1109,fi_predicates,
( ( ssSkP1109("1")
<=> $true )
& ( ssSkP1109("2")
<=> $true )
& ( ssSkP1109("3")
<=> $true ) ) ).
fof(ssSkP111,fi_predicates,
( ( ssSkP111("1")
<=> $false )
& ( ssSkP111("2")
<=> $true )
& ( ssSkP111("3")
<=> $true ) ) ).
fof(ssSkP1110,fi_predicates,
( ( ssSkP1110("1")
<=> $true )
& ( ssSkP1110("2")
<=> $true )
& ( ssSkP1110("3")
<=> $true ) ) ).
fof(ssSkP1111,fi_predicates,
( ( ssSkP1111("1")
<=> $true )
& ( ssSkP1111("2")
<=> $true )
& ( ssSkP1111("3")
<=> $true ) ) ).
fof(ssSkP1112,fi_predicates,
( ( ssSkP1112("1")
<=> $true )
& ( ssSkP1112("2")
<=> $true )
& ( ssSkP1112("3")
<=> $true ) ) ).
fof(ssSkP1113,fi_predicates,
( ( ssSkP1113("1")
<=> $true )
& ( ssSkP1113("2")
<=> $true )
& ( ssSkP1113("3")
<=> $true ) ) ).
fof(ssSkP1114,fi_predicates,
( ( ssSkP1114("1")
<=> $true )
& ( ssSkP1114("2")
<=> $true )
& ( ssSkP1114("3")
<=> $true ) ) ).
fof(ssSkP1115,fi_predicates,
( ( ssSkP1115("1")
<=> $true )
& ( ssSkP1115("2")
<=> $true )
& ( ssSkP1115("3")
<=> $true ) ) ).
fof(ssSkP1116,fi_predicates,
( ( ssSkP1116("1")
<=> $true )
& ( ssSkP1116("2")
<=> $true )
& ( ssSkP1116("3")
<=> $true ) ) ).
fof(ssSkP1117,fi_predicates,
( ( ssSkP1117("1")
<=> $true )
& ( ssSkP1117("2")
<=> $true )
& ( ssSkP1117("3")
<=> $true ) ) ).
fof(ssSkP1118,fi_predicates,
( ( ssSkP1118("1")
<=> $true )
& ( ssSkP1118("2")
<=> $true )
& ( ssSkP1118("3")
<=> $true ) ) ).
fof(ssSkP1119,fi_predicates,
( ( ssSkP1119("1")
<=> $true )
& ( ssSkP1119("2")
<=> $false )
& ( ssSkP1119("3")
<=> $false ) ) ).
fof(ssSkP112,fi_predicates,
( ( ssSkP112("1")
<=> $false )
& ( ssSkP112("2")
<=> $true )
& ( ssSkP112("3")
<=> $true ) ) ).
fof(ssSkP1120,fi_predicates,
! [X1,X2] :
( ssSkP1120(X1,X2)
<=> $true ) ).
fof(ssSkP1121,fi_predicates,
! [X1,X2] :
( ssSkP1121(X1,X2)
<=> $true ) ).
fof(ssSkP1122,fi_predicates,
! [X1] :
( ssSkP1122(X1)
<=> $true ) ).
fof(ssSkP1123,fi_predicates,
! [X1] :
( ssSkP1123(X1)
<=> $true ) ).
fof(ssSkP1124,fi_predicates,
! [X1] :
( ssSkP1124(X1)
<=> $true ) ).
fof(ssSkP1125,fi_predicates,
! [X1] :
( ssSkP1125(X1)
<=> $true ) ).
fof(ssSkP1126,fi_predicates,
! [X1] :
( ssSkP1126(X1)
<=> $true ) ).
fof(ssSkP1127,fi_predicates,
! [X1] :
( ssSkP1127(X1)
<=> $true ) ).
fof(ssSkP1128,fi_predicates,
! [X1] :
( ssSkP1128(X1)
<=> $true ) ).
fof(ssSkP1129,fi_predicates,
! [X1] :
( ssSkP1129(X1)
<=> $true ) ).
fof(ssSkP113,fi_predicates,
( ( ssSkP113("1")
<=> $false )
& ( ssSkP113("2")
<=> $true )
& ( ssSkP113("3")
<=> $true ) ) ).
fof(ssSkP1130,fi_predicates,
! [X1] :
( ssSkP1130(X1)
<=> $true ) ).
fof(ssSkP1131,fi_predicates,
! [X1] :
( ssSkP1131(X1)
<=> $true ) ).
fof(ssSkP1132,fi_predicates,
! [X1] :
( ssSkP1132(X1)
<=> $true ) ).
fof(ssSkP1133,fi_predicates,
! [X1] :
( ssSkP1133(X1)
<=> $true ) ).
fof(ssSkP1134,fi_predicates,
! [X1] :
( ssSkP1134(X1)
<=> $true ) ).
fof(ssSkP1135,fi_predicates,
! [X1] :
( ssSkP1135(X1)
<=> $true ) ).
fof(ssSkP1136,fi_predicates,
! [X1] :
( ssSkP1136(X1)
<=> $true ) ).
fof(ssSkP1137,fi_predicates,
! [X1] :
( ssSkP1137(X1)
<=> $true ) ).
fof(ssSkP1138,fi_predicates,
! [X1] :
( ssSkP1138(X1)
<=> $true ) ).
fof(ssSkP1139,fi_predicates,
! [X1] :
( ssSkP1139(X1)
<=> $true ) ).
fof(ssSkP114,fi_predicates,
( ( ssSkP114("1")
<=> $false )
& ( ssSkP114("2")
<=> $true )
& ( ssSkP114("3")
<=> $true ) ) ).
fof(ssSkP1140,fi_predicates,
! [X1] :
( ssSkP1140(X1)
<=> $true ) ).
fof(ssSkP1141,fi_predicates,
! [X1] :
( ssSkP1141(X1)
<=> $true ) ).
fof(ssSkP1142,fi_predicates,
! [X1] :
( ssSkP1142(X1)
<=> $true ) ).
fof(ssSkP1143,fi_predicates,
! [X1] :
( ssSkP1143(X1)
<=> $true ) ).
fof(ssSkP1144,fi_predicates,
! [X1] :
( ssSkP1144(X1)
<=> $true ) ).
fof(ssSkP1145,fi_predicates,
! [X1] :
( ssSkP1145(X1)
<=> $true ) ).
fof(ssSkP1146,fi_predicates,
! [X1] :
( ssSkP1146(X1)
<=> $true ) ).
fof(ssSkP1147,fi_predicates,
! [X1] :
( ssSkP1147(X1)
<=> $true ) ).
fof(ssSkP1148,fi_predicates,
! [X1] :
( ssSkP1148(X1)
<=> $true ) ).
fof(ssSkP1149,fi_predicates,
! [X1] :
( ssSkP1149(X1)
<=> $true ) ).
fof(ssSkP115,fi_predicates,
( ( ssSkP115("1")
<=> $false )
& ( ssSkP115("2")
<=> $true )
& ( ssSkP115("3")
<=> $true ) ) ).
fof(ssSkP1150,fi_predicates,
! [X1] :
( ssSkP1150(X1)
<=> $true ) ).
fof(ssSkP1151,fi_predicates,
! [X1] :
( ssSkP1151(X1)
<=> $true ) ).
fof(ssSkP1152,fi_predicates,
( ( ssSkP1152("1")
<=> $true )
& ( ssSkP1152("2")
<=> $true )
& ( ssSkP1152("3")
<=> $true ) ) ).
fof(ssSkP1153,fi_predicates,
( ( ssSkP1153("1","1")
<=> $true )
& ( ssSkP1153("1","2")
<=> $false )
& ( ssSkP1153("1","3")
<=> $false )
& ( ssSkP1153("2","1")
<=> $true )
& ( ssSkP1153("2","2")
<=> $true )
& ( ssSkP1153("2","3")
<=> $true )
& ( ssSkP1153("3","1")
<=> $true )
& ( ssSkP1153("3","2")
<=> $true )
& ( ssSkP1153("3","3")
<=> $true ) ) ).
fof(ssSkP1154,fi_predicates,
( ( ssSkP1154("1")
<=> $false )
& ( ssSkP1154("2")
<=> $true )
& ( ssSkP1154("3")
<=> $false ) ) ).
fof(ssSkP1155,fi_predicates,
( ( ssSkP1155("1")
<=> $false )
& ( ssSkP1155("2")
<=> $true )
& ( ssSkP1155("3")
<=> $false ) ) ).
fof(ssSkP1156,fi_predicates,
( ( ssSkP1156("1")
<=> $false )
& ( ssSkP1156("2")
<=> $true )
& ( ssSkP1156("3")
<=> $false ) ) ).
fof(ssSkP1157,fi_predicates,
( ( ssSkP1157("1")
<=> $false )
& ( ssSkP1157("2")
<=> $true )
& ( ssSkP1157("3")
<=> $false ) ) ).
fof(ssSkP1158,fi_predicates,
( ( ssSkP1158("1")
<=> $false )
& ( ssSkP1158("2")
<=> $true )
& ( ssSkP1158("3")
<=> $false ) ) ).
fof(ssSkP1159,fi_predicates,
( ( ssSkP1159("1")
<=> $true )
& ( ssSkP1159("2")
<=> $true )
& ( ssSkP1159("3")
<=> $false ) ) ).
fof(ssSkP116,fi_predicates,
( ( ssSkP116("1")
<=> $false )
& ( ssSkP116("2")
<=> $true )
& ( ssSkP116("3")
<=> $true ) ) ).
fof(ssSkP1160,fi_predicates,
( ( ssSkP1160("1")
<=> $false )
& ( ssSkP1160("2")
<=> $true )
& ( ssSkP1160("3")
<=> $false ) ) ).
fof(ssSkP1161,fi_predicates,
( ( ssSkP1161("1")
<=> $false )
& ( ssSkP1161("2")
<=> $true )
& ( ssSkP1161("3")
<=> $false ) ) ).
fof(ssSkP1162,fi_predicates,
( ( ssSkP1162("1")
<=> $false )
& ( ssSkP1162("2")
<=> $true )
& ( ssSkP1162("3")
<=> $false ) ) ).
fof(ssSkP1163,fi_predicates,
( ( ssSkP1163("1")
<=> $true )
& ( ssSkP1163("2")
<=> $true )
& ( ssSkP1163("3")
<=> $false ) ) ).
fof(ssSkP1164,fi_predicates,
( ( ssSkP1164("1")
<=> $false )
& ( ssSkP1164("2")
<=> $true )
& ( ssSkP1164("3")
<=> $false ) ) ).
fof(ssSkP1165,fi_predicates,
( ( ssSkP1165("1")
<=> $false )
& ( ssSkP1165("2")
<=> $true )
& ( ssSkP1165("3")
<=> $false ) ) ).
fof(ssSkP1166,fi_predicates,
( ( ssSkP1166("1","1")
<=> $true )
& ( ssSkP1166("1","2")
<=> $false )
& ( ssSkP1166("1","3")
<=> $false )
& ( ssSkP1166("2","1")
<=> $true )
& ( ssSkP1166("2","2")
<=> $true )
& ( ssSkP1166("2","3")
<=> $true )
& ( ssSkP1166("3","1")
<=> $true )
& ( ssSkP1166("3","2")
<=> $true )
& ( ssSkP1166("3","3")
<=> $true ) ) ).
fof(ssSkP1167,fi_predicates,
( ( ssSkP1167("1")
<=> $false )
& ( ssSkP1167("2")
<=> $true )
& ( ssSkP1167("3")
<=> $true ) ) ).
fof(ssSkP1168,fi_predicates,
( ( ssSkP1168("1")
<=> $false )
& ( ssSkP1168("2")
<=> $true )
& ( ssSkP1168("3")
<=> $true ) ) ).
fof(ssSkP1169,fi_predicates,
( ( ssSkP1169("1")
<=> $false )
& ( ssSkP1169("2")
<=> $true )
& ( ssSkP1169("3")
<=> $true ) ) ).
fof(ssSkP117,fi_predicates,
( ( ssSkP117("1")
<=> $false )
& ( ssSkP117("2")
<=> $true )
& ( ssSkP117("3")
<=> $true ) ) ).
fof(ssSkP1170,fi_predicates,
( ( ssSkP1170("1")
<=> $false )
& ( ssSkP1170("2")
<=> $true )
& ( ssSkP1170("3")
<=> $false ) ) ).
fof(ssSkP1171,fi_predicates,
( ( ssSkP1171("1")
<=> $false )
& ( ssSkP1171("2")
<=> $true )
& ( ssSkP1171("3")
<=> $true ) ) ).
fof(ssSkP1172,fi_predicates,
( ( ssSkP1172("1")
<=> $false )
& ( ssSkP1172("2")
<=> $true )
& ( ssSkP1172("3")
<=> $true ) ) ).
fof(ssSkP1173,fi_predicates,
( ( ssSkP1173("1")
<=> $false )
& ( ssSkP1173("2")
<=> $true )
& ( ssSkP1173("3")
<=> $true ) ) ).
fof(ssSkP1174,fi_predicates,
( ( ssSkP1174("1")
<=> $true )
& ( ssSkP1174("2")
<=> $true )
& ( ssSkP1174("3")
<=> $true ) ) ).
fof(ssSkP1175,fi_predicates,
( ( ssSkP1175("1")
<=> $true )
& ( ssSkP1175("2")
<=> $true )
& ( ssSkP1175("3")
<=> $false ) ) ).
fof(ssSkP1176,fi_predicates,
( ( ssSkP1176("1")
<=> $false )
& ( ssSkP1176("2")
<=> $true )
& ( ssSkP1176("3")
<=> $true ) ) ).
fof(ssSkP1177,fi_predicates,
( ( ssSkP1177("1")
<=> $false )
& ( ssSkP1177("2")
<=> $true )
& ( ssSkP1177("3")
<=> $true ) ) ).
fof(ssSkP1178,fi_predicates,
( ( ssSkP1178("1")
<=> $false )
& ( ssSkP1178("2")
<=> $true )
& ( ssSkP1178("3")
<=> $true ) ) ).
fof(ssSkP1179,fi_predicates,
( ( ssSkP1179("1")
<=> $false )
& ( ssSkP1179("2")
<=> $true )
& ( ssSkP1179("3")
<=> $false ) ) ).
fof(ssSkP118,fi_predicates,
( ( ssSkP118("1")
<=> $false )
& ( ssSkP118("2")
<=> $true )
& ( ssSkP118("3")
<=> $true ) ) ).
fof(ssSkP1180,fi_predicates,
( ( ssSkP1180("1")
<=> $false )
& ( ssSkP1180("2")
<=> $true )
& ( ssSkP1180("3")
<=> $false ) ) ).
fof(ssSkP1181,fi_predicates,
( ( ssSkP1181("1")
<=> $false )
& ( ssSkP1181("2")
<=> $true )
& ( ssSkP1181("3")
<=> $false ) ) ).
fof(ssSkP1182,fi_predicates,
( ( ssSkP1182("1")
<=> $false )
& ( ssSkP1182("2")
<=> $true )
& ( ssSkP1182("3")
<=> $false ) ) ).
fof(ssSkP1183,fi_predicates,
( ( ssSkP1183("1")
<=> $false )
& ( ssSkP1183("2")
<=> $true )
& ( ssSkP1183("3")
<=> $false ) ) ).
fof(ssSkP1184,fi_predicates,
( ( ssSkP1184("1")
<=> $false )
& ( ssSkP1184("2")
<=> $true )
& ( ssSkP1184("3")
<=> $false ) ) ).
fof(ssSkP1185,fi_predicates,
( ( ssSkP1185("1")
<=> $false )
& ( ssSkP1185("2")
<=> $true )
& ( ssSkP1185("3")
<=> $false ) ) ).
fof(ssSkP1186,fi_predicates,
( ( ssSkP1186("1")
<=> $false )
& ( ssSkP1186("2")
<=> $true )
& ( ssSkP1186("3")
<=> $false ) ) ).
fof(ssSkP1187,fi_predicates,
( ( ssSkP1187("1")
<=> $false )
& ( ssSkP1187("2")
<=> $true )
& ( ssSkP1187("3")
<=> $false ) ) ).
fof(ssSkP1188,fi_predicates,
( ( ssSkP1188("1")
<=> $true )
& ( ssSkP1188("2")
<=> $true )
& ( ssSkP1188("3")
<=> $true ) ) ).
fof(ssSkP1189,fi_predicates,
( ( ssSkP1189("1")
<=> $false )
& ( ssSkP1189("2")
<=> $true )
& ( ssSkP1189("3")
<=> $false ) ) ).
fof(ssSkP119,fi_predicates,
( ( ssSkP119("1")
<=> $false )
& ( ssSkP119("2")
<=> $true )
& ( ssSkP119("3")
<=> $true ) ) ).
fof(ssSkP1190,fi_predicates,
( ( ssSkP1190("1")
<=> $false )
& ( ssSkP1190("2")
<=> $true )
& ( ssSkP1190("3")
<=> $false ) ) ).
fof(ssSkP1191,fi_predicates,
( ( ssSkP1191("1")
<=> $false )
& ( ssSkP1191("2")
<=> $true )
& ( ssSkP1191("3")
<=> $false ) ) ).
fof(ssSkP1192,fi_predicates,
( ( ssSkP1192("1")
<=> $true )
& ( ssSkP1192("2")
<=> $true )
& ( ssSkP1192("3")
<=> $true ) ) ).
fof(ssSkP1193,fi_predicates,
( ( ssSkP1193("1")
<=> $false )
& ( ssSkP1193("2")
<=> $true )
& ( ssSkP1193("3")
<=> $true ) ) ).
fof(ssSkP1194,fi_predicates,
( ( ssSkP1194("1")
<=> $false )
& ( ssSkP1194("2")
<=> $true )
& ( ssSkP1194("3")
<=> $true ) ) ).
fof(ssSkP1195,fi_predicates,
( ( ssSkP1195("1")
<=> $false )
& ( ssSkP1195("2")
<=> $true )
& ( ssSkP1195("3")
<=> $true ) ) ).
fof(ssSkP1196,fi_predicates,
( ( ssSkP1196("1")
<=> $false )
& ( ssSkP1196("2")
<=> $true )
& ( ssSkP1196("3")
<=> $true ) ) ).
fof(ssSkP1197,fi_predicates,
( ( ssSkP1197("1")
<=> $false )
& ( ssSkP1197("2")
<=> $true )
& ( ssSkP1197("3")
<=> $true ) ) ).
fof(ssSkP1198,fi_predicates,
( ( ssSkP1198("1")
<=> $false )
& ( ssSkP1198("2")
<=> $true )
& ( ssSkP1198("3")
<=> $true ) ) ).
fof(ssSkP1199,fi_predicates,
( ( ssSkP1199("1")
<=> $false )
& ( ssSkP1199("2")
<=> $true )
& ( ssSkP1199("3")
<=> $true ) ) ).
fof(ssSkP12,fi_predicates,
( ( ssSkP12("1")
<=> $true )
& ( ssSkP12("2")
<=> $false )
& ( ssSkP12("3")
<=> $false ) ) ).
fof(ssSkP120,fi_predicates,
( ( ssSkP120("1")
<=> $false )
& ( ssSkP120("2")
<=> $true )
& ( ssSkP120("3")
<=> $true ) ) ).
fof(ssSkP1200,fi_predicates,
( ( ssSkP1200("1")
<=> $false )
& ( ssSkP1200("2")
<=> $true )
& ( ssSkP1200("3")
<=> $true ) ) ).
fof(ssSkP1201,fi_predicates,
( ( ssSkP1201("1")
<=> $false )
& ( ssSkP1201("2")
<=> $true )
& ( ssSkP1201("3")
<=> $true ) ) ).
fof(ssSkP1202,fi_predicates,
( ( ssSkP1202("1")
<=> $false )
& ( ssSkP1202("2")
<=> $true )
& ( ssSkP1202("3")
<=> $true ) ) ).
fof(ssSkP1203,fi_predicates,
( ( ssSkP1203("1")
<=> $false )
& ( ssSkP1203("2")
<=> $true )
& ( ssSkP1203("3")
<=> $true ) ) ).
fof(ssSkP1204,fi_predicates,
( ( ssSkP1204("1")
<=> $false )
& ( ssSkP1204("2")
<=> $true )
& ( ssSkP1204("3")
<=> $true ) ) ).
fof(ssSkP1205,fi_predicates,
( ( ssSkP1205("1")
<=> $true )
& ( ssSkP1205("2")
<=> $true )
& ( ssSkP1205("3")
<=> $true ) ) ).
fof(ssSkP1206,fi_predicates,
( ( ssSkP1206("1")
<=> $true )
& ( ssSkP1206("2")
<=> $true )
& ( ssSkP1206("3")
<=> $true ) ) ).
fof(ssSkP1207,fi_predicates,
( ( ssSkP1207("1")
<=> $true )
& ( ssSkP1207("2")
<=> $true )
& ( ssSkP1207("3")
<=> $true ) ) ).
fof(ssSkP1208,fi_predicates,
( ( ssSkP1208("1")
<=> $true )
& ( ssSkP1208("2")
<=> $true )
& ( ssSkP1208("3")
<=> $true ) ) ).
fof(ssSkP1209,fi_predicates,
( ( ssSkP1209("1")
<=> $true )
& ( ssSkP1209("2")
<=> $true )
& ( ssSkP1209("3")
<=> $true ) ) ).
fof(ssSkP121,fi_predicates,
( ( ssSkP121("1")
<=> $false )
& ( ssSkP121("2")
<=> $true )
& ( ssSkP121("3")
<=> $true ) ) ).
fof(ssSkP1210,fi_predicates,
( ( ssSkP1210("1")
<=> $false )
& ( ssSkP1210("2")
<=> $true )
& ( ssSkP1210("3")
<=> $true ) ) ).
fof(ssSkP1211,fi_predicates,
( ( ssSkP1211("1")
<=> $false )
& ( ssSkP1211("2")
<=> $true )
& ( ssSkP1211("3")
<=> $true ) ) ).
fof(ssSkP1212,fi_predicates,
( ( ssSkP1212("1")
<=> $false )
& ( ssSkP1212("2")
<=> $true )
& ( ssSkP1212("3")
<=> $true ) ) ).
fof(ssSkP1213,fi_predicates,
( ( ssSkP1213("1")
<=> $false )
& ( ssSkP1213("2")
<=> $true )
& ( ssSkP1213("3")
<=> $true ) ) ).
fof(ssSkP1214,fi_predicates,
( ( ssSkP1214("1")
<=> $false )
& ( ssSkP1214("2")
<=> $true )
& ( ssSkP1214("3")
<=> $true ) ) ).
fof(ssSkP1215,fi_predicates,
( ( ssSkP1215("1")
<=> $false )
& ( ssSkP1215("2")
<=> $true )
& ( ssSkP1215("3")
<=> $true ) ) ).
fof(ssSkP1216,fi_predicates,
( ( ssSkP1216("1")
<=> $false )
& ( ssSkP1216("2")
<=> $true )
& ( ssSkP1216("3")
<=> $true ) ) ).
fof(ssSkP1217,fi_predicates,
( ( ssSkP1217("1")
<=> $false )
& ( ssSkP1217("2")
<=> $true )
& ( ssSkP1217("3")
<=> $true ) ) ).
fof(ssSkP1218,fi_predicates,
( ( ssSkP1218("1")
<=> $false )
& ( ssSkP1218("2")
<=> $true )
& ( ssSkP1218("3")
<=> $true ) ) ).
fof(ssSkP1219,fi_predicates,
( ( ssSkP1219("1")
<=> $false )
& ( ssSkP1219("2")
<=> $true )
& ( ssSkP1219("3")
<=> $true ) ) ).
fof(ssSkP122,fi_predicates,
( ( ssSkP122("1")
<=> $false )
& ( ssSkP122("2")
<=> $true )
& ( ssSkP122("3")
<=> $true ) ) ).
fof(ssSkP1220,fi_predicates,
( ( ssSkP1220("1")
<=> $false )
& ( ssSkP1220("2")
<=> $true )
& ( ssSkP1220("3")
<=> $true ) ) ).
fof(ssSkP1221,fi_predicates,
( ( ssSkP1221("1")
<=> $false )
& ( ssSkP1221("2")
<=> $true )
& ( ssSkP1221("3")
<=> $true ) ) ).
fof(ssSkP1222,fi_predicates,
( ( ssSkP1222("1")
<=> $false )
& ( ssSkP1222("2")
<=> $true )
& ( ssSkP1222("3")
<=> $true ) ) ).
fof(ssSkP1223,fi_predicates,
( ( ssSkP1223("1")
<=> $false )
& ( ssSkP1223("2")
<=> $true )
& ( ssSkP1223("3")
<=> $true ) ) ).
fof(ssSkP1224,fi_predicates,
( ( ssSkP1224("1")
<=> $false )
& ( ssSkP1224("2")
<=> $true )
& ( ssSkP1224("3")
<=> $true ) ) ).
fof(ssSkP1225,fi_predicates,
( ( ssSkP1225("1")
<=> $false )
& ( ssSkP1225("2")
<=> $true )
& ( ssSkP1225("3")
<=> $true ) ) ).
fof(ssSkP1226,fi_predicates,
( ( ssSkP1226("1")
<=> $false )
& ( ssSkP1226("2")
<=> $true )
& ( ssSkP1226("3")
<=> $true ) ) ).
fof(ssSkP1227,fi_predicates,
( ( ssSkP1227("1")
<=> $false )
& ( ssSkP1227("2")
<=> $true )
& ( ssSkP1227("3")
<=> $true ) ) ).
fof(ssSkP1228,fi_predicates,
( ( ssSkP1228("1")
<=> $false )
& ( ssSkP1228("2")
<=> $true )
& ( ssSkP1228("3")
<=> $true ) ) ).
fof(ssSkP1229,fi_predicates,
( ( ssSkP1229("1")
<=> $false )
& ( ssSkP1229("2")
<=> $true )
& ( ssSkP1229("3")
<=> $true ) ) ).
fof(ssSkP123,fi_predicates,
( ( ssSkP123("1")
<=> $false )
& ( ssSkP123("2")
<=> $true )
& ( ssSkP123("3")
<=> $true ) ) ).
fof(ssSkP1230,fi_predicates,
( ( ssSkP1230("1")
<=> $false )
& ( ssSkP1230("2")
<=> $true )
& ( ssSkP1230("3")
<=> $true ) ) ).
fof(ssSkP1231,fi_predicates,
( ( ssSkP1231("1")
<=> $false )
& ( ssSkP1231("2")
<=> $true )
& ( ssSkP1231("3")
<=> $true ) ) ).
fof(ssSkP1232,fi_predicates,
( ( ssSkP1232("1")
<=> $false )
& ( ssSkP1232("2")
<=> $true )
& ( ssSkP1232("3")
<=> $true ) ) ).
fof(ssSkP1233,fi_predicates,
( ( ssSkP1233("1")
<=> $false )
& ( ssSkP1233("2")
<=> $true )
& ( ssSkP1233("3")
<=> $true ) ) ).
fof(ssSkP1234,fi_predicates,
( ( ssSkP1234("1")
<=> $false )
& ( ssSkP1234("2")
<=> $true )
& ( ssSkP1234("3")
<=> $true ) ) ).
fof(ssSkP1235,fi_predicates,
( ( ssSkP1235("1")
<=> $false )
& ( ssSkP1235("2")
<=> $true )
& ( ssSkP1235("3")
<=> $true ) ) ).
fof(ssSkP1236,fi_predicates,
( ( ssSkP1236("1")
<=> $false )
& ( ssSkP1236("2")
<=> $true )
& ( ssSkP1236("3")
<=> $true ) ) ).
fof(ssSkP1237,fi_predicates,
( ( ssSkP1237("1")
<=> $false )
& ( ssSkP1237("2")
<=> $true )
& ( ssSkP1237("3")
<=> $true ) ) ).
fof(ssSkP1238,fi_predicates,
( ( ssSkP1238("1")
<=> $false )
& ( ssSkP1238("2")
<=> $true )
& ( ssSkP1238("3")
<=> $true ) ) ).
fof(ssSkP1239,fi_predicates,
( ( ssSkP1239("1")
<=> $false )
& ( ssSkP1239("2")
<=> $true )
& ( ssSkP1239("3")
<=> $true ) ) ).
fof(ssSkP124,fi_predicates,
( ( ssSkP124("1")
<=> $false )
& ( ssSkP124("2")
<=> $true )
& ( ssSkP124("3")
<=> $true ) ) ).
fof(ssSkP1240,fi_predicates,
( ( ssSkP1240("1")
<=> $false )
& ( ssSkP1240("2")
<=> $true )
& ( ssSkP1240("3")
<=> $true ) ) ).
fof(ssSkP1241,fi_predicates,
( ( ssSkP1241("1")
<=> $false )
& ( ssSkP1241("2")
<=> $true )
& ( ssSkP1241("3")
<=> $true ) ) ).
fof(ssSkP1242,fi_predicates,
( ( ssSkP1242("1")
<=> $false )
& ( ssSkP1242("2")
<=> $true )
& ( ssSkP1242("3")
<=> $true ) ) ).
fof(ssSkP1243,fi_predicates,
( ( ssSkP1243("1")
<=> $false )
& ( ssSkP1243("2")
<=> $true )
& ( ssSkP1243("3")
<=> $true ) ) ).
fof(ssSkP1244,fi_predicates,
( ( ssSkP1244("1")
<=> $false )
& ( ssSkP1244("2")
<=> $true )
& ( ssSkP1244("3")
<=> $true ) ) ).
fof(ssSkP1245,fi_predicates,
( ( ssSkP1245("1")
<=> $false )
& ( ssSkP1245("2")
<=> $true )
& ( ssSkP1245("3")
<=> $true ) ) ).
fof(ssSkP1246,fi_predicates,
( ( ssSkP1246("1")
<=> $false )
& ( ssSkP1246("2")
<=> $true )
& ( ssSkP1246("3")
<=> $true ) ) ).
fof(ssSkP1247,fi_predicates,
( ( ssSkP1247("1")
<=> $false )
& ( ssSkP1247("2")
<=> $true )
& ( ssSkP1247("3")
<=> $true ) ) ).
fof(ssSkP1248,fi_predicates,
( ( ssSkP1248("1")
<=> $false )
& ( ssSkP1248("2")
<=> $true )
& ( ssSkP1248("3")
<=> $true ) ) ).
fof(ssSkP1249,fi_predicates,
( ( ssSkP1249("1")
<=> $false )
& ( ssSkP1249("2")
<=> $true )
& ( ssSkP1249("3")
<=> $true ) ) ).
fof(ssSkP125,fi_predicates,
( ( ssSkP125("1")
<=> $false )
& ( ssSkP125("2")
<=> $false )
& ( ssSkP125("3")
<=> $true ) ) ).
fof(ssSkP1250,fi_predicates,
( ( ssSkP1250("1")
<=> $false )
& ( ssSkP1250("2")
<=> $true )
& ( ssSkP1250("3")
<=> $true ) ) ).
fof(ssSkP1251,fi_predicates,
( ( ssSkP1251("1")
<=> $false )
& ( ssSkP1251("2")
<=> $true )
& ( ssSkP1251("3")
<=> $true ) ) ).
fof(ssSkP1252,fi_predicates,
( ( ssSkP1252("1")
<=> $false )
& ( ssSkP1252("2")
<=> $true )
& ( ssSkP1252("3")
<=> $true ) ) ).
fof(ssSkP1253,fi_predicates,
( ( ssSkP1253("1")
<=> $false )
& ( ssSkP1253("2")
<=> $true )
& ( ssSkP1253("3")
<=> $true ) ) ).
fof(ssSkP1254,fi_predicates,
( ( ssSkP1254("1")
<=> $false )
& ( ssSkP1254("2")
<=> $true )
& ( ssSkP1254("3")
<=> $true ) ) ).
fof(ssSkP1255,fi_predicates,
( ( ssSkP1255("1")
<=> $false )
& ( ssSkP1255("2")
<=> $true )
& ( ssSkP1255("3")
<=> $false ) ) ).
fof(ssSkP1256,fi_predicates,
( ( ssSkP1256("1")
<=> $false )
& ( ssSkP1256("2")
<=> $true )
& ( ssSkP1256("3")
<=> $false ) ) ).
fof(ssSkP126,fi_predicates,
( ( ssSkP126("1")
<=> $true )
& ( ssSkP126("2")
<=> $true )
& ( ssSkP126("3")
<=> $true ) ) ).
fof(ssSkP127,fi_predicates,
( ( ssSkP127("1")
<=> $true )
& ( ssSkP127("2")
<=> $true )
& ( ssSkP127("3")
<=> $true ) ) ).
fof(ssSkP128,fi_predicates,
( ( ssSkP128("1")
<=> $true )
& ( ssSkP128("2")
<=> $true )
& ( ssSkP128("3")
<=> $true ) ) ).
fof(ssSkP129,fi_predicates,
( ( ssSkP129("1")
<=> $true )
& ( ssSkP129("2")
<=> $true )
& ( ssSkP129("3")
<=> $true ) ) ).
fof(ssSkP13,fi_predicates,
( ( ssSkP13("1")
<=> $true )
& ( ssSkP13("2")
<=> $false )
& ( ssSkP13("3")
<=> $false ) ) ).
fof(ssSkP130,fi_predicates,
( ( ssSkP130("1")
<=> $true )
& ( ssSkP130("2")
<=> $true )
& ( ssSkP130("3")
<=> $false ) ) ).
fof(ssSkP131,fi_predicates,
( ( ssSkP131("1")
<=> $true )
& ( ssSkP131("2")
<=> $true )
& ( ssSkP131("3")
<=> $true ) ) ).
fof(ssSkP132,fi_predicates,
( ( ssSkP132("1")
<=> $false )
& ( ssSkP132("2")
<=> $false )
& ( ssSkP132("3")
<=> $true ) ) ).
fof(ssSkP133,fi_predicates,
( ( ssSkP133("1","1")
<=> $true )
& ( ssSkP133("1","2")
<=> $true )
& ( ssSkP133("1","3")
<=> $true )
& ( ssSkP133("2","1")
<=> $true )
& ( ssSkP133("2","2")
<=> $true )
& ( ssSkP133("2","3")
<=> $true )
& ( ssSkP133("3","1")
<=> $true )
& ( ssSkP133("3","2")
<=> $true )
& ( ssSkP133("3","3")
<=> $true ) ) ).
fof(ssSkP134,fi_predicates,
( ( ssSkP134("1","1")
<=> $true )
& ( ssSkP134("1","2")
<=> $true )
& ( ssSkP134("1","3")
<=> $true )
& ( ssSkP134("2","1")
<=> $true )
& ( ssSkP134("2","2")
<=> $true )
& ( ssSkP134("2","3")
<=> $true )
& ( ssSkP134("3","1")
<=> $true )
& ( ssSkP134("3","2")
<=> $true )
& ( ssSkP134("3","3")
<=> $true ) ) ).
fof(ssSkP135,fi_predicates,
( ( ssSkP135("1")
<=> $false )
& ( ssSkP135("2")
<=> $true )
& ( ssSkP135("3")
<=> $true ) ) ).
fof(ssSkP136,fi_predicates,
( ( ssSkP136("1")
<=> $false )
& ( ssSkP136("2")
<=> $true )
& ( ssSkP136("3")
<=> $true ) ) ).
fof(ssSkP137,fi_predicates,
( ( ssSkP137("1")
<=> $false )
& ( ssSkP137("2")
<=> $false )
& ( ssSkP137("3")
<=> $true ) ) ).
fof(ssSkP138,fi_predicates,
( ( ssSkP138("1")
<=> $false )
& ( ssSkP138("2")
<=> $true )
& ( ssSkP138("3")
<=> $true ) ) ).
fof(ssSkP139,fi_predicates,
( ( ssSkP139("1")
<=> $false )
& ( ssSkP139("2")
<=> $false )
& ( ssSkP139("3")
<=> $true ) ) ).
fof(ssSkP14,fi_predicates,
( ( ssSkP14("1")
<=> $true )
& ( ssSkP14("2")
<=> $false )
& ( ssSkP14("3")
<=> $false ) ) ).
fof(ssSkP140,fi_predicates,
( ( ssSkP140("1")
<=> $false )
& ( ssSkP140("2")
<=> $true )
& ( ssSkP140("3")
<=> $true ) ) ).
fof(ssSkP141,fi_predicates,
( ( ssSkP141("1")
<=> $false )
& ( ssSkP141("2")
<=> $true )
& ( ssSkP141("3")
<=> $true ) ) ).
fof(ssSkP142,fi_predicates,
( ( ssSkP142("1")
<=> $false )
& ( ssSkP142("2")
<=> $true )
& ( ssSkP142("3")
<=> $true ) ) ).
fof(ssSkP143,fi_predicates,
( ( ssSkP143("1")
<=> $false )
& ( ssSkP143("2")
<=> $false )
& ( ssSkP143("3")
<=> $false ) ) ).
fof(ssSkP144,fi_predicates,
( ( ssSkP144("1")
<=> $false )
& ( ssSkP144("2")
<=> $false )
& ( ssSkP144("3")
<=> $false ) ) ).
fof(ssSkP145,fi_predicates,
( ( ssSkP145("1")
<=> $false )
& ( ssSkP145("2")
<=> $false )
& ( ssSkP145("3")
<=> $false ) ) ).
fof(ssSkP146,fi_predicates,
( ( ssSkP146("1")
<=> $false )
& ( ssSkP146("2")
<=> $false )
& ( ssSkP146("3")
<=> $false ) ) ).
fof(ssSkP147,fi_predicates,
( ( ssSkP147("1")
<=> $false )
& ( ssSkP147("2")
<=> $false )
& ( ssSkP147("3")
<=> $false ) ) ).
fof(ssSkP148,fi_predicates,
( ( ssSkP148("1")
<=> $false )
& ( ssSkP148("2")
<=> $false )
& ( ssSkP148("3")
<=> $false ) ) ).
fof(ssSkP149,fi_predicates,
( ( ssSkP149("1")
<=> $false )
& ( ssSkP149("2")
<=> $false )
& ( ssSkP149("3")
<=> $false ) ) ).
fof(ssSkP15,fi_predicates,
( ( ssSkP15("1")
<=> $true )
& ( ssSkP15("2")
<=> $false )
& ( ssSkP15("3")
<=> $false ) ) ).
fof(ssSkP150,fi_predicates,
( ( ssSkP150("1")
<=> $false )
& ( ssSkP150("2")
<=> $false )
& ( ssSkP150("3")
<=> $false ) ) ).
fof(ssSkP151,fi_predicates,
( ( ssSkP151("1")
<=> $false )
& ( ssSkP151("2")
<=> $false )
& ( ssSkP151("3")
<=> $false ) ) ).
fof(ssSkP152,fi_predicates,
( ( ssSkP152("1")
<=> $false )
& ( ssSkP152("2")
<=> $false )
& ( ssSkP152("3")
<=> $false ) ) ).
fof(ssSkP153,fi_predicates,
( ( ssSkP153("1")
<=> $false )
& ( ssSkP153("2")
<=> $false )
& ( ssSkP153("3")
<=> $false ) ) ).
fof(ssSkP154,fi_predicates,
( ( ssSkP154("1")
<=> $true )
& ( ssSkP154("2")
<=> $true )
& ( ssSkP154("3")
<=> $true ) ) ).
fof(ssSkP155,fi_predicates,
( ( ssSkP155("1")
<=> $true )
& ( ssSkP155("2")
<=> $false )
& ( ssSkP155("3")
<=> $false ) ) ).
fof(ssSkP156,fi_predicates,
( ( ssSkP156("1","1")
<=> $true )
& ( ssSkP156("1","2")
<=> $true )
& ( ssSkP156("1","3")
<=> $true )
& ( ssSkP156("2","1")
<=> $false )
& ( ssSkP156("2","2")
<=> $true )
& ( ssSkP156("2","3")
<=> $true )
& ( ssSkP156("3","1")
<=> $false )
& ( ssSkP156("3","2")
<=> $true )
& ( ssSkP156("3","3")
<=> $true ) ) ).
fof(ssSkP157,fi_predicates,
( ( ssSkP157("1","1")
<=> $true )
& ( ssSkP157("1","2")
<=> $true )
& ( ssSkP157("1","3")
<=> $true )
& ( ssSkP157("2","1")
<=> $false )
& ( ssSkP157("2","2")
<=> $true )
& ( ssSkP157("2","3")
<=> $true )
& ( ssSkP157("3","1")
<=> $false )
& ( ssSkP157("3","2")
<=> $true )
& ( ssSkP157("3","3")
<=> $true ) ) ).
fof(ssSkP158,fi_predicates,
( ( ssSkP158("1")
<=> $true )
& ( ssSkP158("2")
<=> $false )
& ( ssSkP158("3")
<=> $false ) ) ).
fof(ssSkP159,fi_predicates,
( ( ssSkP159("1")
<=> $true )
& ( ssSkP159("2")
<=> $false )
& ( ssSkP159("3")
<=> $false ) ) ).
fof(ssSkP16,fi_predicates,
( ( ssSkP16("1")
<=> $true )
& ( ssSkP16("2")
<=> $false )
& ( ssSkP16("3")
<=> $false ) ) ).
fof(ssSkP160,fi_predicates,
( ( ssSkP160("1")
<=> $true )
& ( ssSkP160("2")
<=> $false )
& ( ssSkP160("3")
<=> $false ) ) ).
fof(ssSkP161,fi_predicates,
( ( ssSkP161("1")
<=> $true )
& ( ssSkP161("2")
<=> $false )
& ( ssSkP161("3")
<=> $false ) ) ).
fof(ssSkP162,fi_predicates,
( ( ssSkP162("1")
<=> $true )
& ( ssSkP162("2")
<=> $false )
& ( ssSkP162("3")
<=> $false ) ) ).
fof(ssSkP163,fi_predicates,
( ( ssSkP163("1")
<=> $true )
& ( ssSkP163("2")
<=> $false )
& ( ssSkP163("3")
<=> $false ) ) ).
fof(ssSkP164,fi_predicates,
( ( ssSkP164("1")
<=> $true )
& ( ssSkP164("2")
<=> $false )
& ( ssSkP164("3")
<=> $false ) ) ).
fof(ssSkP165,fi_predicates,
( ( ssSkP165("1")
<=> $true )
& ( ssSkP165("2")
<=> $false )
& ( ssSkP165("3")
<=> $false ) ) ).
fof(ssSkP166,fi_predicates,
( ( ssSkP166("1")
<=> $true )
& ( ssSkP166("2")
<=> $false )
& ( ssSkP166("3")
<=> $false ) ) ).
fof(ssSkP167,fi_predicates,
( ( ssSkP167("1")
<=> $true )
& ( ssSkP167("2")
<=> $false )
& ( ssSkP167("3")
<=> $false ) ) ).
fof(ssSkP168,fi_predicates,
( ( ssSkP168("1")
<=> $true )
& ( ssSkP168("2")
<=> $false )
& ( ssSkP168("3")
<=> $false ) ) ).
fof(ssSkP169,fi_predicates,
( ( ssSkP169("1")
<=> $true )
& ( ssSkP169("2")
<=> $false )
& ( ssSkP169("3")
<=> $false ) ) ).
fof(ssSkP17,fi_predicates,
( ( ssSkP17("1")
<=> $true )
& ( ssSkP17("2")
<=> $false )
& ( ssSkP17("3")
<=> $false ) ) ).
fof(ssSkP170,fi_predicates,
( ( ssSkP170("1")
<=> $true )
& ( ssSkP170("2")
<=> $false )
& ( ssSkP170("3")
<=> $false ) ) ).
fof(ssSkP171,fi_predicates,
( ( ssSkP171("1")
<=> $true )
& ( ssSkP171("2")
<=> $false )
& ( ssSkP171("3")
<=> $true ) ) ).
fof(ssSkP172,fi_predicates,
( ( ssSkP172("1")
<=> $true )
& ( ssSkP172("2")
<=> $false )
& ( ssSkP172("3")
<=> $false ) ) ).
fof(ssSkP173,fi_predicates,
( ( ssSkP173("1")
<=> $true )
& ( ssSkP173("2")
<=> $false )
& ( ssSkP173("3")
<=> $false ) ) ).
fof(ssSkP174,fi_predicates,
( ( ssSkP174("1")
<=> $true )
& ( ssSkP174("2")
<=> $false )
& ( ssSkP174("3")
<=> $false ) ) ).
fof(ssSkP175,fi_predicates,
( ( ssSkP175("1")
<=> $true )
& ( ssSkP175("2")
<=> $false )
& ( ssSkP175("3")
<=> $false ) ) ).
fof(ssSkP176,fi_predicates,
( ( ssSkP176("1")
<=> $true )
& ( ssSkP176("2")
<=> $false )
& ( ssSkP176("3")
<=> $false ) ) ).
fof(ssSkP177,fi_predicates,
( ( ssSkP177("1")
<=> $true )
& ( ssSkP177("2")
<=> $false )
& ( ssSkP177("3")
<=> $false ) ) ).
fof(ssSkP178,fi_predicates,
( ( ssSkP178("1")
<=> $true )
& ( ssSkP178("2")
<=> $false )
& ( ssSkP178("3")
<=> $false ) ) ).
fof(ssSkP179,fi_predicates,
( ( ssSkP179("1")
<=> $true )
& ( ssSkP179("2")
<=> $false )
& ( ssSkP179("3")
<=> $false ) ) ).
fof(ssSkP18,fi_predicates,
( ( ssSkP18("1")
<=> $true )
& ( ssSkP18("2")
<=> $false )
& ( ssSkP18("3")
<=> $false ) ) ).
fof(ssSkP180,fi_predicates,
( ( ssSkP180("1")
<=> $true )
& ( ssSkP180("2")
<=> $false )
& ( ssSkP180("3")
<=> $false ) ) ).
fof(ssSkP181,fi_predicates,
( ( ssSkP181("1")
<=> $true )
& ( ssSkP181("2")
<=> $false )
& ( ssSkP181("3")
<=> $false ) ) ).
fof(ssSkP182,fi_predicates,
( ( ssSkP182("1")
<=> $true )
& ( ssSkP182("2")
<=> $false )
& ( ssSkP182("3")
<=> $false ) ) ).
fof(ssSkP183,fi_predicates,
( ( ssSkP183("1")
<=> $true )
& ( ssSkP183("2")
<=> $false )
& ( ssSkP183("3")
<=> $false ) ) ).
fof(ssSkP184,fi_predicates,
( ( ssSkP184("1")
<=> $true )
& ( ssSkP184("2")
<=> $false )
& ( ssSkP184("3")
<=> $false ) ) ).
fof(ssSkP185,fi_predicates,
( ( ssSkP185("1")
<=> $true )
& ( ssSkP185("2")
<=> $true )
& ( ssSkP185("3")
<=> $true ) ) ).
fof(ssSkP186,fi_predicates,
( ( ssSkP186("1")
<=> $false )
& ( ssSkP186("2")
<=> $false )
& ( ssSkP186("3")
<=> $true ) ) ).
fof(ssSkP187,fi_predicates,
( ( ssSkP187("1","1")
<=> $true )
& ( ssSkP187("1","2")
<=> $true )
& ( ssSkP187("1","3")
<=> $true )
& ( ssSkP187("2","1")
<=> $true )
& ( ssSkP187("2","2")
<=> $true )
& ( ssSkP187("2","3")
<=> $true )
& ( ssSkP187("3","1")
<=> $true )
& ( ssSkP187("3","2")
<=> $true )
& ( ssSkP187("3","3")
<=> $true ) ) ).
fof(ssSkP188,fi_predicates,
( ( ssSkP188("1","1")
<=> $true )
& ( ssSkP188("1","2")
<=> $true )
& ( ssSkP188("1","3")
<=> $true )
& ( ssSkP188("2","1")
<=> $true )
& ( ssSkP188("2","2")
<=> $true )
& ( ssSkP188("2","3")
<=> $true )
& ( ssSkP188("3","1")
<=> $true )
& ( ssSkP188("3","2")
<=> $true )
& ( ssSkP188("3","3")
<=> $true ) ) ).
fof(ssSkP189,fi_predicates,
( ( ssSkP189("1")
<=> $false )
& ( ssSkP189("2")
<=> $false )
& ( ssSkP189("3")
<=> $false ) ) ).
fof(ssSkP19,fi_predicates,
( ( ssSkP19("1")
<=> $false )
& ( ssSkP19("2")
<=> $false )
& ( ssSkP19("3")
<=> $false ) ) ).
fof(ssSkP190,fi_predicates,
( ( ssSkP190("1")
<=> $false )
& ( ssSkP190("2")
<=> $false )
& ( ssSkP190("3")
<=> $false ) ) ).
fof(ssSkP191,fi_predicates,
( ( ssSkP191("1")
<=> $false )
& ( ssSkP191("2")
<=> $false )
& ( ssSkP191("3")
<=> $false ) ) ).
fof(ssSkP192,fi_predicates,
( ( ssSkP192("1")
<=> $false )
& ( ssSkP192("2")
<=> $false )
& ( ssSkP192("3")
<=> $false ) ) ).
fof(ssSkP193,fi_predicates,
( ( ssSkP193("1")
<=> $false )
& ( ssSkP193("2")
<=> $false )
& ( ssSkP193("3")
<=> $false ) ) ).
fof(ssSkP194,fi_predicates,
( ( ssSkP194("1")
<=> $false )
& ( ssSkP194("2")
<=> $false )
& ( ssSkP194("3")
<=> $false ) ) ).
fof(ssSkP195,fi_predicates,
( ( ssSkP195("1")
<=> $false )
& ( ssSkP195("2")
<=> $false )
& ( ssSkP195("3")
<=> $false ) ) ).
fof(ssSkP196,fi_predicates,
( ( ssSkP196("1")
<=> $false )
& ( ssSkP196("2")
<=> $false )
& ( ssSkP196("3")
<=> $false ) ) ).
fof(ssSkP197,fi_predicates,
( ( ssSkP197("1")
<=> $false )
& ( ssSkP197("2")
<=> $false )
& ( ssSkP197("3")
<=> $false ) ) ).
fof(ssSkP198,fi_predicates,
( ( ssSkP198("1")
<=> $false )
& ( ssSkP198("2")
<=> $false )
& ( ssSkP198("3")
<=> $false ) ) ).
fof(ssSkP199,fi_predicates,
( ( ssSkP199("1")
<=> $true )
& ( ssSkP199("2")
<=> $true )
& ( ssSkP199("3")
<=> $false ) ) ).
fof(ssSkP2,fi_predicates,
( ( ssSkP2("1")
<=> $true )
& ( ssSkP2("2")
<=> $false )
& ( ssSkP2("3")
<=> $false ) ) ).
fof(ssSkP20,fi_predicates,
( ( ssSkP20("1")
<=> $true )
& ( ssSkP20("2")
<=> $true )
& ( ssSkP20("3")
<=> $false ) ) ).
fof(ssSkP200,fi_predicates,
( ( ssSkP200("1")
<=> $true )
& ( ssSkP200("2")
<=> $false )
& ( ssSkP200("3")
<=> $false ) ) ).
fof(ssSkP201,fi_predicates,
( ( ssSkP201("1")
<=> $false )
& ( ssSkP201("2")
<=> $false )
& ( ssSkP201("3")
<=> $false ) ) ).
fof(ssSkP202,fi_predicates,
( ( ssSkP202("1")
<=> $false )
& ( ssSkP202("2")
<=> $false )
& ( ssSkP202("3")
<=> $false ) ) ).
fof(ssSkP203,fi_predicates,
( ( ssSkP203("1")
<=> $false )
& ( ssSkP203("2")
<=> $false )
& ( ssSkP203("3")
<=> $false ) ) ).
fof(ssSkP204,fi_predicates,
( ( ssSkP204("1")
<=> $false )
& ( ssSkP204("2")
<=> $false )
& ( ssSkP204("3")
<=> $false ) ) ).
fof(ssSkP205,fi_predicates,
( ( ssSkP205("1")
<=> $false )
& ( ssSkP205("2")
<=> $false )
& ( ssSkP205("3")
<=> $false ) ) ).
fof(ssSkP206,fi_predicates,
( ( ssSkP206("1")
<=> $false )
& ( ssSkP206("2")
<=> $false )
& ( ssSkP206("3")
<=> $false ) ) ).
fof(ssSkP207,fi_predicates,
( ( ssSkP207("1")
<=> $false )
& ( ssSkP207("2")
<=> $false )
& ( ssSkP207("3")
<=> $false ) ) ).
fof(ssSkP208,fi_predicates,
( ( ssSkP208("1")
<=> $false )
& ( ssSkP208("2")
<=> $false )
& ( ssSkP208("3")
<=> $false ) ) ).
fof(ssSkP209,fi_predicates,
( ( ssSkP209("1")
<=> $false )
& ( ssSkP209("2")
<=> $false )
& ( ssSkP209("3")
<=> $false ) ) ).
fof(ssSkP21,fi_predicates,
( ( ssSkP21("1")
<=> $true )
& ( ssSkP21("2")
<=> $false )
& ( ssSkP21("3")
<=> $false ) ) ).
fof(ssSkP210,fi_predicates,
( ( ssSkP210("1")
<=> $true )
& ( ssSkP210("2")
<=> $true )
& ( ssSkP210("3")
<=> $true ) ) ).
fof(ssSkP211,fi_predicates,
( ( ssSkP211("1")
<=> $true )
& ( ssSkP211("2")
<=> $true )
& ( ssSkP211("3")
<=> $true ) ) ).
fof(ssSkP212,fi_predicates,
( ( ssSkP212("1")
<=> $true )
& ( ssSkP212("2")
<=> $true )
& ( ssSkP212("3")
<=> $true ) ) ).
fof(ssSkP213,fi_predicates,
( ( ssSkP213("1")
<=> $true )
& ( ssSkP213("2")
<=> $true )
& ( ssSkP213("3")
<=> $true ) ) ).
fof(ssSkP214,fi_predicates,
( ( ssSkP214("1")
<=> $false )
& ( ssSkP214("2")
<=> $false )
& ( ssSkP214("3")
<=> $true ) ) ).
fof(ssSkP215,fi_predicates,
( ( ssSkP215("1","1")
<=> $true )
& ( ssSkP215("1","2")
<=> $true )
& ( ssSkP215("1","3")
<=> $true )
& ( ssSkP215("2","1")
<=> $true )
& ( ssSkP215("2","2")
<=> $true )
& ( ssSkP215("2","3")
<=> $true )
& ( ssSkP215("3","1")
<=> $true )
& ( ssSkP215("3","2")
<=> $true )
& ( ssSkP215("3","3")
<=> $true ) ) ).
fof(ssSkP216,fi_predicates,
( ( ssSkP216("1","1")
<=> $true )
& ( ssSkP216("1","2")
<=> $true )
& ( ssSkP216("1","3")
<=> $true )
& ( ssSkP216("2","1")
<=> $true )
& ( ssSkP216("2","2")
<=> $true )
& ( ssSkP216("2","3")
<=> $true )
& ( ssSkP216("3","1")
<=> $true )
& ( ssSkP216("3","2")
<=> $true )
& ( ssSkP216("3","3")
<=> $true ) ) ).
fof(ssSkP217,fi_predicates,
( ( ssSkP217("1")
<=> $true )
& ( ssSkP217("2")
<=> $false )
& ( ssSkP217("3")
<=> $true ) ) ).
fof(ssSkP218,fi_predicates,
( ( ssSkP218("1")
<=> $true )
& ( ssSkP218("2")
<=> $false )
& ( ssSkP218("3")
<=> $true ) ) ).
fof(ssSkP219,fi_predicates,
( ( ssSkP219("1")
<=> $false )
& ( ssSkP219("2")
<=> $false )
& ( ssSkP219("3")
<=> $false ) ) ).
fof(ssSkP22,fi_predicates,
( ( ssSkP22("1")
<=> $true )
& ( ssSkP22("2")
<=> $false )
& ( ssSkP22("3")
<=> $false ) ) ).
fof(ssSkP220,fi_predicates,
( ( ssSkP220("1")
<=> $false )
& ( ssSkP220("2")
<=> $false )
& ( ssSkP220("3")
<=> $false ) ) ).
fof(ssSkP221,fi_predicates,
( ( ssSkP221("1")
<=> $false )
& ( ssSkP221("2")
<=> $false )
& ( ssSkP221("3")
<=> $false ) ) ).
fof(ssSkP222,fi_predicates,
( ( ssSkP222("1")
<=> $false )
& ( ssSkP222("2")
<=> $false )
& ( ssSkP222("3")
<=> $false ) ) ).
fof(ssSkP223,fi_predicates,
( ( ssSkP223("1")
<=> $false )
& ( ssSkP223("2")
<=> $false )
& ( ssSkP223("3")
<=> $false ) ) ).
fof(ssSkP224,fi_predicates,
( ( ssSkP224("1")
<=> $false )
& ( ssSkP224("2")
<=> $false )
& ( ssSkP224("3")
<=> $false ) ) ).
fof(ssSkP225,fi_predicates,
( ( ssSkP225("1")
<=> $false )
& ( ssSkP225("2")
<=> $false )
& ( ssSkP225("3")
<=> $false ) ) ).
fof(ssSkP226,fi_predicates,
( ( ssSkP226("1")
<=> $false )
& ( ssSkP226("2")
<=> $false )
& ( ssSkP226("3")
<=> $false ) ) ).
fof(ssSkP227,fi_predicates,
( ( ssSkP227("1")
<=> $false )
& ( ssSkP227("2")
<=> $false )
& ( ssSkP227("3")
<=> $false ) ) ).
fof(ssSkP228,fi_predicates,
( ( ssSkP228("1")
<=> $false )
& ( ssSkP228("2")
<=> $false )
& ( ssSkP228("3")
<=> $false ) ) ).
fof(ssSkP229,fi_predicates,
( ( ssSkP229("1")
<=> $false )
& ( ssSkP229("2")
<=> $false )
& ( ssSkP229("3")
<=> $false ) ) ).
fof(ssSkP23,fi_predicates,
( ( ssSkP23("1")
<=> $true )
& ( ssSkP23("2")
<=> $false )
& ( ssSkP23("3")
<=> $false ) ) ).
fof(ssSkP230,fi_predicates,
( ( ssSkP230("1")
<=> $false )
& ( ssSkP230("2")
<=> $false )
& ( ssSkP230("3")
<=> $false ) ) ).
fof(ssSkP231,fi_predicates,
( ( ssSkP231("1")
<=> $false )
& ( ssSkP231("2")
<=> $false )
& ( ssSkP231("3")
<=> $false ) ) ).
fof(ssSkP232,fi_predicates,
( ( ssSkP232("1")
<=> $false )
& ( ssSkP232("2")
<=> $false )
& ( ssSkP232("3")
<=> $false ) ) ).
fof(ssSkP233,fi_predicates,
( ( ssSkP233("1")
<=> $false )
& ( ssSkP233("2")
<=> $false )
& ( ssSkP233("3")
<=> $false ) ) ).
fof(ssSkP234,fi_predicates,
( ( ssSkP234("1")
<=> $false )
& ( ssSkP234("2")
<=> $false )
& ( ssSkP234("3")
<=> $false ) ) ).
fof(ssSkP235,fi_predicates,
( ( ssSkP235("1")
<=> $false )
& ( ssSkP235("2")
<=> $false )
& ( ssSkP235("3")
<=> $false ) ) ).
fof(ssSkP236,fi_predicates,
( ( ssSkP236("1")
<=> $false )
& ( ssSkP236("2")
<=> $false )
& ( ssSkP236("3")
<=> $false ) ) ).
fof(ssSkP237,fi_predicates,
( ( ssSkP237("1")
<=> $false )
& ( ssSkP237("2")
<=> $false )
& ( ssSkP237("3")
<=> $true ) ) ).
fof(ssSkP238,fi_predicates,
( ( ssSkP238("1")
<=> $false )
& ( ssSkP238("2")
<=> $false )
& ( ssSkP238("3")
<=> $false ) ) ).
fof(ssSkP239,fi_predicates,
( ( ssSkP239("1")
<=> $false )
& ( ssSkP239("2")
<=> $false )
& ( ssSkP239("3")
<=> $false ) ) ).
fof(ssSkP24,fi_predicates,
( ( ssSkP24("1")
<=> $true )
& ( ssSkP24("2")
<=> $false )
& ( ssSkP24("3")
<=> $false ) ) ).
fof(ssSkP240,fi_predicates,
( ( ssSkP240("1")
<=> $false )
& ( ssSkP240("2")
<=> $false )
& ( ssSkP240("3")
<=> $false ) ) ).
fof(ssSkP241,fi_predicates,
( ( ssSkP241("1")
<=> $false )
& ( ssSkP241("2")
<=> $false )
& ( ssSkP241("3")
<=> $false ) ) ).
fof(ssSkP242,fi_predicates,
( ( ssSkP242("1")
<=> $true )
& ( ssSkP242("2")
<=> $true )
& ( ssSkP242("3")
<=> $true ) ) ).
fof(ssSkP243,fi_predicates,
( ( ssSkP243("1")
<=> $true )
& ( ssSkP243("2")
<=> $true )
& ( ssSkP243("3")
<=> $true ) ) ).
fof(ssSkP244,fi_predicates,
( ( ssSkP244("1")
<=> $false )
& ( ssSkP244("2")
<=> $false )
& ( ssSkP244("3")
<=> $true ) ) ).
fof(ssSkP245,fi_predicates,
( ( ssSkP245("1","1")
<=> $true )
& ( ssSkP245("1","2")
<=> $true )
& ( ssSkP245("1","3")
<=> $true )
& ( ssSkP245("2","1")
<=> $true )
& ( ssSkP245("2","2")
<=> $true )
& ( ssSkP245("2","3")
<=> $true )
& ( ssSkP245("3","1")
<=> $true )
& ( ssSkP245("3","2")
<=> $true )
& ( ssSkP245("3","3")
<=> $true ) ) ).
fof(ssSkP246,fi_predicates,
( ( ssSkP246("1","1")
<=> $true )
& ( ssSkP246("1","2")
<=> $true )
& ( ssSkP246("1","3")
<=> $true )
& ( ssSkP246("2","1")
<=> $true )
& ( ssSkP246("2","2")
<=> $true )
& ( ssSkP246("2","3")
<=> $true )
& ( ssSkP246("3","1")
<=> $true )
& ( ssSkP246("3","2")
<=> $true )
& ( ssSkP246("3","3")
<=> $true ) ) ).
fof(ssSkP247,fi_predicates,
( ( ssSkP247("1")
<=> $false )
& ( ssSkP247("2")
<=> $false )
& ( ssSkP247("3")
<=> $false ) ) ).
fof(ssSkP248,fi_predicates,
( ( ssSkP248("1")
<=> $false )
& ( ssSkP248("2")
<=> $false )
& ( ssSkP248("3")
<=> $false ) ) ).
fof(ssSkP249,fi_predicates,
( ( ssSkP249("1")
<=> $false )
& ( ssSkP249("2")
<=> $false )
& ( ssSkP249("3")
<=> $false ) ) ).
fof(ssSkP25,fi_predicates,
( ( ssSkP25("1")
<=> $true )
& ( ssSkP25("2")
<=> $false )
& ( ssSkP25("3")
<=> $false ) ) ).
fof(ssSkP250,fi_predicates,
( ( ssSkP250("1")
<=> $false )
& ( ssSkP250("2")
<=> $false )
& ( ssSkP250("3")
<=> $false ) ) ).
fof(ssSkP251,fi_predicates,
( ( ssSkP251("1")
<=> $false )
& ( ssSkP251("2")
<=> $false )
& ( ssSkP251("3")
<=> $false ) ) ).
fof(ssSkP252,fi_predicates,
( ( ssSkP252("1")
<=> $false )
& ( ssSkP252("2")
<=> $false )
& ( ssSkP252("3")
<=> $false ) ) ).
fof(ssSkP253,fi_predicates,
( ( ssSkP253("1")
<=> $false )
& ( ssSkP253("2")
<=> $false )
& ( ssSkP253("3")
<=> $false ) ) ).
fof(ssSkP254,fi_predicates,
( ( ssSkP254("1")
<=> $false )
& ( ssSkP254("2")
<=> $false )
& ( ssSkP254("3")
<=> $false ) ) ).
fof(ssSkP255,fi_predicates,
( ( ssSkP255("1")
<=> $false )
& ( ssSkP255("2")
<=> $false )
& ( ssSkP255("3")
<=> $false ) ) ).
fof(ssSkP256,fi_predicates,
( ( ssSkP256("1")
<=> $false )
& ( ssSkP256("2")
<=> $false )
& ( ssSkP256("3")
<=> $false ) ) ).
fof(ssSkP257,fi_predicates,
( ( ssSkP257("1")
<=> $true )
& ( ssSkP257("2")
<=> $true )
& ( ssSkP257("3")
<=> $false ) ) ).
fof(ssSkP258,fi_predicates,
( ( ssSkP258("1")
<=> $false )
& ( ssSkP258("2")
<=> $false )
& ( ssSkP258("3")
<=> $false ) ) ).
fof(ssSkP259,fi_predicates,
( ( ssSkP259("1")
<=> $false )
& ( ssSkP259("2")
<=> $false )
& ( ssSkP259("3")
<=> $false ) ) ).
fof(ssSkP26,fi_predicates,
( ( ssSkP26("1")
<=> $true )
& ( ssSkP26("2")
<=> $false )
& ( ssSkP26("3")
<=> $false ) ) ).
fof(ssSkP260,fi_predicates,
( ( ssSkP260("1")
<=> $false )
& ( ssSkP260("2")
<=> $false )
& ( ssSkP260("3")
<=> $false ) ) ).
fof(ssSkP261,fi_predicates,
( ( ssSkP261("1")
<=> $false )
& ( ssSkP261("2")
<=> $false )
& ( ssSkP261("3")
<=> $false ) ) ).
fof(ssSkP262,fi_predicates,
( ( ssSkP262("1")
<=> $false )
& ( ssSkP262("2")
<=> $false )
& ( ssSkP262("3")
<=> $false ) ) ).
fof(ssSkP263,fi_predicates,
( ( ssSkP263("1")
<=> $false )
& ( ssSkP263("2")
<=> $false )
& ( ssSkP263("3")
<=> $false ) ) ).
fof(ssSkP264,fi_predicates,
( ( ssSkP264("1")
<=> $false )
& ( ssSkP264("2")
<=> $false )
& ( ssSkP264("3")
<=> $false ) ) ).
fof(ssSkP265,fi_predicates,
( ( ssSkP265("1")
<=> $true )
& ( ssSkP265("2")
<=> $true )
& ( ssSkP265("3")
<=> $false ) ) ).
fof(ssSkP266,fi_predicates,
( ( ssSkP266("1")
<=> $true )
& ( ssSkP266("2")
<=> $false )
& ( ssSkP266("3")
<=> $false ) ) ).
fof(ssSkP267,fi_predicates,
( ( ssSkP267("1")
<=> $true )
& ( ssSkP267("2")
<=> $false )
& ( ssSkP267("3")
<=> $false ) ) ).
fof(ssSkP268,fi_predicates,
( ( ssSkP268("1")
<=> $true )
& ( ssSkP268("2")
<=> $false )
& ( ssSkP268("3")
<=> $false ) ) ).
fof(ssSkP269,fi_predicates,
( ( ssSkP269("1")
<=> $true )
& ( ssSkP269("2")
<=> $false )
& ( ssSkP269("3")
<=> $false ) ) ).
fof(ssSkP27,fi_predicates,
! [X1,X2] :
( ssSkP27(X1,X2)
<=> $true ) ).
fof(ssSkP270,fi_predicates,
( ( ssSkP270("1")
<=> $true )
& ( ssSkP270("2")
<=> $false )
& ( ssSkP270("3")
<=> $false ) ) ).
fof(ssSkP271,fi_predicates,
( ( ssSkP271("1")
<=> $true )
& ( ssSkP271("2")
<=> $false )
& ( ssSkP271("3")
<=> $false ) ) ).
fof(ssSkP272,fi_predicates,
( ( ssSkP272("1")
<=> $true )
& ( ssSkP272("2")
<=> $true )
& ( ssSkP272("3")
<=> $true ) ) ).
fof(ssSkP273,fi_predicates,
( ( ssSkP273("1")
<=> $true )
& ( ssSkP273("2")
<=> $true )
& ( ssSkP273("3")
<=> $true ) ) ).
fof(ssSkP274,fi_predicates,
( ( ssSkP274("1")
<=> $true )
& ( ssSkP274("2")
<=> $false )
& ( ssSkP274("3")
<=> $false ) ) ).
fof(ssSkP275,fi_predicates,
( ( ssSkP275("1","1")
<=> $true )
& ( ssSkP275("1","2")
<=> $true )
& ( ssSkP275("1","3")
<=> $true )
& ( ssSkP275("2","1")
<=> $true )
& ( ssSkP275("2","2")
<=> $true )
& ( ssSkP275("2","3")
<=> $true )
& ( ssSkP275("3","1")
<=> $true )
& ( ssSkP275("3","2")
<=> $true )
& ( ssSkP275("3","3")
<=> $true ) ) ).
fof(ssSkP276,fi_predicates,
( ( ssSkP276("1","1")
<=> $true )
& ( ssSkP276("1","2")
<=> $true )
& ( ssSkP276("1","3")
<=> $true )
& ( ssSkP276("2","1")
<=> $true )
& ( ssSkP276("2","2")
<=> $true )
& ( ssSkP276("2","3")
<=> $true )
& ( ssSkP276("3","1")
<=> $true )
& ( ssSkP276("3","2")
<=> $true )
& ( ssSkP276("3","3")
<=> $true ) ) ).
fof(ssSkP277,fi_predicates,
( ( ssSkP277("1")
<=> $true )
& ( ssSkP277("2")
<=> $false )
& ( ssSkP277("3")
<=> $false ) ) ).
fof(ssSkP278,fi_predicates,
( ( ssSkP278("1")
<=> $true )
& ( ssSkP278("2")
<=> $false )
& ( ssSkP278("3")
<=> $false ) ) ).
fof(ssSkP279,fi_predicates,
( ( ssSkP279("1")
<=> $true )
& ( ssSkP279("2")
<=> $false )
& ( ssSkP279("3")
<=> $false ) ) ).
fof(ssSkP28,fi_predicates,
! [X1,X2] :
( ssSkP28(X1,X2)
<=> $true ) ).
fof(ssSkP280,fi_predicates,
( ( ssSkP280("1")
<=> $true )
& ( ssSkP280("2")
<=> $false )
& ( ssSkP280("3")
<=> $false ) ) ).
fof(ssSkP281,fi_predicates,
( ( ssSkP281("1")
<=> $true )
& ( ssSkP281("2")
<=> $false )
& ( ssSkP281("3")
<=> $true ) ) ).
fof(ssSkP282,fi_predicates,
( ( ssSkP282("1")
<=> $true )
& ( ssSkP282("2")
<=> $false )
& ( ssSkP282("3")
<=> $false ) ) ).
fof(ssSkP283,fi_predicates,
( ( ssSkP283("1")
<=> $true )
& ( ssSkP283("2")
<=> $false )
& ( ssSkP283("3")
<=> $false ) ) ).
fof(ssSkP284,fi_predicates,
( ( ssSkP284("1")
<=> $true )
& ( ssSkP284("2")
<=> $false )
& ( ssSkP284("3")
<=> $false ) ) ).
fof(ssSkP285,fi_predicates,
( ( ssSkP285("1")
<=> $true )
& ( ssSkP285("2")
<=> $false )
& ( ssSkP285("3")
<=> $false ) ) ).
fof(ssSkP286,fi_predicates,
( ( ssSkP286("1")
<=> $true )
& ( ssSkP286("2")
<=> $false )
& ( ssSkP286("3")
<=> $false ) ) ).
fof(ssSkP287,fi_predicates,
( ( ssSkP287("1")
<=> $true )
& ( ssSkP287("2")
<=> $false )
& ( ssSkP287("3")
<=> $false ) ) ).
fof(ssSkP288,fi_predicates,
( ( ssSkP288("1")
<=> $true )
& ( ssSkP288("2")
<=> $false )
& ( ssSkP288("3")
<=> $false ) ) ).
fof(ssSkP289,fi_predicates,
( ( ssSkP289("1")
<=> $true )
& ( ssSkP289("2")
<=> $false )
& ( ssSkP289("3")
<=> $false ) ) ).
fof(ssSkP29,fi_predicates,
! [X1] :
( ssSkP29(X1)
<=> $false ) ).
fof(ssSkP290,fi_predicates,
( ( ssSkP290("1")
<=> $true )
& ( ssSkP290("2")
<=> $false )
& ( ssSkP290("3")
<=> $false ) ) ).
fof(ssSkP291,fi_predicates,
( ( ssSkP291("1")
<=> $true )
& ( ssSkP291("2")
<=> $true )
& ( ssSkP291("3")
<=> $false ) ) ).
fof(ssSkP292,fi_predicates,
( ( ssSkP292("1")
<=> $true )
& ( ssSkP292("2")
<=> $false )
& ( ssSkP292("3")
<=> $false ) ) ).
fof(ssSkP293,fi_predicates,
( ( ssSkP293("1")
<=> $true )
& ( ssSkP293("2")
<=> $false )
& ( ssSkP293("3")
<=> $false ) ) ).
fof(ssSkP294,fi_predicates,
( ( ssSkP294("1")
<=> $true )
& ( ssSkP294("2")
<=> $false )
& ( ssSkP294("3")
<=> $false ) ) ).
fof(ssSkP295,fi_predicates,
( ( ssSkP295("1")
<=> $true )
& ( ssSkP295("2")
<=> $false )
& ( ssSkP295("3")
<=> $false ) ) ).
fof(ssSkP296,fi_predicates,
( ( ssSkP296("1")
<=> $true )
& ( ssSkP296("2")
<=> $false )
& ( ssSkP296("3")
<=> $false ) ) ).
fof(ssSkP297,fi_predicates,
( ( ssSkP297("1")
<=> $true )
& ( ssSkP297("2")
<=> $false )
& ( ssSkP297("3")
<=> $false ) ) ).
fof(ssSkP298,fi_predicates,
( ( ssSkP298("1")
<=> $true )
& ( ssSkP298("2")
<=> $false )
& ( ssSkP298("3")
<=> $false ) ) ).
fof(ssSkP299,fi_predicates,
( ( ssSkP299("1")
<=> $true )
& ( ssSkP299("2")
<=> $false )
& ( ssSkP299("3")
<=> $false ) ) ).
fof(ssSkP3,fi_predicates,
( ( ssSkP3("1")
<=> $true )
& ( ssSkP3("2")
<=> $false )
& ( ssSkP3("3")
<=> $false ) ) ).
fof(ssSkP30,fi_predicates,
! [X1] :
( ssSkP30(X1)
<=> $false ) ).
fof(ssSkP300,fi_predicates,
( ( ssSkP300("1")
<=> $true )
& ( ssSkP300("2")
<=> $false )
& ( ssSkP300("3")
<=> $false ) ) ).
fof(ssSkP301,fi_predicates,
( ( ssSkP301("1")
<=> $true )
& ( ssSkP301("2")
<=> $false )
& ( ssSkP301("3")
<=> $false ) ) ).
fof(ssSkP302,fi_predicates,
( ( ssSkP302("1")
<=> $true )
& ( ssSkP302("2")
<=> $false )
& ( ssSkP302("3")
<=> $false ) ) ).
fof(ssSkP303,fi_predicates,
( ( ssSkP303("1")
<=> $true )
& ( ssSkP303("2")
<=> $true )
& ( ssSkP303("3")
<=> $true ) ) ).
fof(ssSkP304,fi_predicates,
( ( ssSkP304("1")
<=> $true )
& ( ssSkP304("2")
<=> $true )
& ( ssSkP304("3")
<=> $true ) ) ).
fof(ssSkP305,fi_predicates,
( ( ssSkP305("1")
<=> $false )
& ( ssSkP305("2")
<=> $false )
& ( ssSkP305("3")
<=> $true ) ) ).
fof(ssSkP306,fi_predicates,
( ( ssSkP306("1","1")
<=> $true )
& ( ssSkP306("1","2")
<=> $true )
& ( ssSkP306("1","3")
<=> $true )
& ( ssSkP306("2","1")
<=> $true )
& ( ssSkP306("2","2")
<=> $true )
& ( ssSkP306("2","3")
<=> $true )
& ( ssSkP306("3","1")
<=> $false )
& ( ssSkP306("3","2")
<=> $true )
& ( ssSkP306("3","3")
<=> $true ) ) ).
fof(ssSkP307,fi_predicates,
( ( ssSkP307("1","1")
<=> $true )
& ( ssSkP307("1","2")
<=> $true )
& ( ssSkP307("1","3")
<=> $true )
& ( ssSkP307("2","1")
<=> $true )
& ( ssSkP307("2","2")
<=> $true )
& ( ssSkP307("2","3")
<=> $true )
& ( ssSkP307("3","1")
<=> $false )
& ( ssSkP307("3","2")
<=> $true )
& ( ssSkP307("3","3")
<=> $true ) ) ).
fof(ssSkP308,fi_predicates,
( ( ssSkP308("1")
<=> $false )
& ( ssSkP308("2")
<=> $false )
& ( ssSkP308("3")
<=> $false ) ) ).
fof(ssSkP309,fi_predicates,
( ( ssSkP309("1")
<=> $false )
& ( ssSkP309("2")
<=> $false )
& ( ssSkP309("3")
<=> $false ) ) ).
fof(ssSkP31,fi_predicates,
! [X1] :
( ssSkP31(X1)
<=> $true ) ).
fof(ssSkP310,fi_predicates,
( ( ssSkP310("1")
<=> $false )
& ( ssSkP310("2")
<=> $false )
& ( ssSkP310("3")
<=> $false ) ) ).
fof(ssSkP311,fi_predicates,
( ( ssSkP311("1")
<=> $false )
& ( ssSkP311("2")
<=> $false )
& ( ssSkP311("3")
<=> $false ) ) ).
fof(ssSkP312,fi_predicates,
( ( ssSkP312("1")
<=> $false )
& ( ssSkP312("2")
<=> $false )
& ( ssSkP312("3")
<=> $false ) ) ).
fof(ssSkP313,fi_predicates,
( ( ssSkP313("1")
<=> $false )
& ( ssSkP313("2")
<=> $false )
& ( ssSkP313("3")
<=> $false ) ) ).
fof(ssSkP314,fi_predicates,
( ( ssSkP314("1")
<=> $false )
& ( ssSkP314("2")
<=> $false )
& ( ssSkP314("3")
<=> $false ) ) ).
fof(ssSkP315,fi_predicates,
( ( ssSkP315("1")
<=> $false )
& ( ssSkP315("2")
<=> $false )
& ( ssSkP315("3")
<=> $false ) ) ).
fof(ssSkP316,fi_predicates,
( ( ssSkP316("1")
<=> $false )
& ( ssSkP316("2")
<=> $false )
& ( ssSkP316("3")
<=> $false ) ) ).
fof(ssSkP317,fi_predicates,
( ( ssSkP317("1")
<=> $false )
& ( ssSkP317("2")
<=> $false )
& ( ssSkP317("3")
<=> $false ) ) ).
fof(ssSkP318,fi_predicates,
( ( ssSkP318("1")
<=> $false )
& ( ssSkP318("2")
<=> $false )
& ( ssSkP318("3")
<=> $false ) ) ).
fof(ssSkP319,fi_predicates,
( ( ssSkP319("1")
<=> $true )
& ( ssSkP319("2")
<=> $true )
& ( ssSkP319("3")
<=> $false ) ) ).
fof(ssSkP32,fi_predicates,
! [X1] :
( ssSkP32(X1)
<=> $true ) ).
fof(ssSkP320,fi_predicates,
( ( ssSkP320("1")
<=> $true )
& ( ssSkP320("2")
<=> $false )
& ( ssSkP320("3")
<=> $false ) ) ).
fof(ssSkP321,fi_predicates,
( ( ssSkP321("1")
<=> $true )
& ( ssSkP321("2")
<=> $false )
& ( ssSkP321("3")
<=> $false ) ) ).
fof(ssSkP322,fi_predicates,
( ( ssSkP322("1")
<=> $true )
& ( ssSkP322("2")
<=> $false )
& ( ssSkP322("3")
<=> $false ) ) ).
fof(ssSkP323,fi_predicates,
( ( ssSkP323("1")
<=> $true )
& ( ssSkP323("2")
<=> $true )
& ( ssSkP323("3")
<=> $true ) ) ).
fof(ssSkP324,fi_predicates,
( ( ssSkP324("1")
<=> $true )
& ( ssSkP324("2")
<=> $true )
& ( ssSkP324("3")
<=> $true ) ) ).
fof(ssSkP325,fi_predicates,
( ( ssSkP325("1")
<=> $true )
& ( ssSkP325("2")
<=> $true )
& ( ssSkP325("3")
<=> $false ) ) ).
fof(ssSkP326,fi_predicates,
( ( ssSkP326("1")
<=> $true )
& ( ssSkP326("2")
<=> $false )
& ( ssSkP326("3")
<=> $false ) ) ).
fof(ssSkP327,fi_predicates,
( ( ssSkP327("1","1")
<=> $true )
& ( ssSkP327("1","2")
<=> $true )
& ( ssSkP327("1","3")
<=> $true )
& ( ssSkP327("2","1")
<=> $false )
& ( ssSkP327("2","2")
<=> $true )
& ( ssSkP327("2","3")
<=> $true )
& ( ssSkP327("3","1")
<=> $false )
& ( ssSkP327("3","2")
<=> $true )
& ( ssSkP327("3","3")
<=> $true ) ) ).
fof(ssSkP328,fi_predicates,
( ( ssSkP328("1","1")
<=> $true )
& ( ssSkP328("1","2")
<=> $true )
& ( ssSkP328("1","3")
<=> $true )
& ( ssSkP328("2","1")
<=> $false )
& ( ssSkP328("2","2")
<=> $true )
& ( ssSkP328("2","3")
<=> $true )
& ( ssSkP328("3","1")
<=> $false )
& ( ssSkP328("3","2")
<=> $true )
& ( ssSkP328("3","3")
<=> $true ) ) ).
fof(ssSkP329,fi_predicates,
( ( ssSkP329("1")
<=> $false )
& ( ssSkP329("2")
<=> $false )
& ( ssSkP329("3")
<=> $false ) ) ).
fof(ssSkP33,fi_predicates,
! [X1] :
( ssSkP33(X1)
<=> $true ) ).
fof(ssSkP330,fi_predicates,
( ( ssSkP330("1")
<=> $false )
& ( ssSkP330("2")
<=> $false )
& ( ssSkP330("3")
<=> $false ) ) ).
fof(ssSkP331,fi_predicates,
( ( ssSkP331("1")
<=> $false )
& ( ssSkP331("2")
<=> $false )
& ( ssSkP331("3")
<=> $false ) ) ).
fof(ssSkP332,fi_predicates,
( ( ssSkP332("1")
<=> $false )
& ( ssSkP332("2")
<=> $false )
& ( ssSkP332("3")
<=> $false ) ) ).
fof(ssSkP333,fi_predicates,
( ( ssSkP333("1")
<=> $false )
& ( ssSkP333("2")
<=> $false )
& ( ssSkP333("3")
<=> $false ) ) ).
fof(ssSkP334,fi_predicates,
( ( ssSkP334("1")
<=> $false )
& ( ssSkP334("2")
<=> $false )
& ( ssSkP334("3")
<=> $false ) ) ).
fof(ssSkP335,fi_predicates,
( ( ssSkP335("1")
<=> $false )
& ( ssSkP335("2")
<=> $false )
& ( ssSkP335("3")
<=> $false ) ) ).
fof(ssSkP336,fi_predicates,
( ( ssSkP336("1")
<=> $false )
& ( ssSkP336("2")
<=> $false )
& ( ssSkP336("3")
<=> $false ) ) ).
fof(ssSkP337,fi_predicates,
( ( ssSkP337("1")
<=> $false )
& ( ssSkP337("2")
<=> $false )
& ( ssSkP337("3")
<=> $false ) ) ).
fof(ssSkP338,fi_predicates,
( ( ssSkP338("1")
<=> $false )
& ( ssSkP338("2")
<=> $false )
& ( ssSkP338("3")
<=> $false ) ) ).
fof(ssSkP339,fi_predicates,
( ( ssSkP339("1")
<=> $false )
& ( ssSkP339("2")
<=> $false )
& ( ssSkP339("3")
<=> $false ) ) ).
fof(ssSkP34,fi_predicates,
! [X1] :
( ssSkP34(X1)
<=> $true ) ).
fof(ssSkP340,fi_predicates,
( ( ssSkP340("1")
<=> $true )
& ( ssSkP340("2")
<=> $false )
& ( ssSkP340("3")
<=> $false ) ) ).
fof(ssSkP341,fi_predicates,
( ( ssSkP341("1")
<=> $true )
& ( ssSkP341("2")
<=> $false )
& ( ssSkP341("3")
<=> $false ) ) ).
fof(ssSkP342,fi_predicates,
( ( ssSkP342("1")
<=> $true )
& ( ssSkP342("2")
<=> $false )
& ( ssSkP342("3")
<=> $false ) ) ).
fof(ssSkP343,fi_predicates,
( ( ssSkP343("1")
<=> $true )
& ( ssSkP343("2")
<=> $false )
& ( ssSkP343("3")
<=> $false ) ) ).
fof(ssSkP344,fi_predicates,
( ( ssSkP344("1")
<=> $true )
& ( ssSkP344("2")
<=> $false )
& ( ssSkP344("3")
<=> $false ) ) ).
fof(ssSkP345,fi_predicates,
( ( ssSkP345("1")
<=> $true )
& ( ssSkP345("2")
<=> $false )
& ( ssSkP345("3")
<=> $false ) ) ).
fof(ssSkP346,fi_predicates,
( ( ssSkP346("1","1")
<=> $true )
& ( ssSkP346("1","2")
<=> $true )
& ( ssSkP346("1","3")
<=> $true )
& ( ssSkP346("2","1")
<=> $false )
& ( ssSkP346("2","2")
<=> $true )
& ( ssSkP346("2","3")
<=> $true )
& ( ssSkP346("3","1")
<=> $false )
& ( ssSkP346("3","2")
<=> $true )
& ( ssSkP346("3","3")
<=> $true ) ) ).
fof(ssSkP347,fi_predicates,
( ( ssSkP347("1","1")
<=> $true )
& ( ssSkP347("1","2")
<=> $true )
& ( ssSkP347("1","3")
<=> $true )
& ( ssSkP347("2","1")
<=> $false )
& ( ssSkP347("2","2")
<=> $true )
& ( ssSkP347("2","3")
<=> $true )
& ( ssSkP347("3","1")
<=> $false )
& ( ssSkP347("3","2")
<=> $true )
& ( ssSkP347("3","3")
<=> $true ) ) ).
fof(ssSkP348,fi_predicates,
( ( ssSkP348("1")
<=> $false )
& ( ssSkP348("2")
<=> $false )
& ( ssSkP348("3")
<=> $false ) ) ).
fof(ssSkP349,fi_predicates,
( ( ssSkP349("1")
<=> $false )
& ( ssSkP349("2")
<=> $false )
& ( ssSkP349("3")
<=> $false ) ) ).
fof(ssSkP35,fi_predicates,
! [X1] :
( ssSkP35(X1)
<=> $true ) ).
fof(ssSkP350,fi_predicates,
( ( ssSkP350("1")
<=> $false )
& ( ssSkP350("2")
<=> $false )
& ( ssSkP350("3")
<=> $false ) ) ).
fof(ssSkP351,fi_predicates,
( ( ssSkP351("1")
<=> $false )
& ( ssSkP351("2")
<=> $false )
& ( ssSkP351("3")
<=> $false ) ) ).
fof(ssSkP352,fi_predicates,
( ( ssSkP352("1")
<=> $false )
& ( ssSkP352("2")
<=> $false )
& ( ssSkP352("3")
<=> $false ) ) ).
fof(ssSkP353,fi_predicates,
( ( ssSkP353("1")
<=> $false )
& ( ssSkP353("2")
<=> $false )
& ( ssSkP353("3")
<=> $false ) ) ).
fof(ssSkP354,fi_predicates,
( ( ssSkP354("1")
<=> $false )
& ( ssSkP354("2")
<=> $false )
& ( ssSkP354("3")
<=> $false ) ) ).
fof(ssSkP355,fi_predicates,
( ( ssSkP355("1")
<=> $false )
& ( ssSkP355("2")
<=> $false )
& ( ssSkP355("3")
<=> $false ) ) ).
fof(ssSkP356,fi_predicates,
( ( ssSkP356("1")
<=> $false )
& ( ssSkP356("2")
<=> $false )
& ( ssSkP356("3")
<=> $false ) ) ).
fof(ssSkP357,fi_predicates,
( ( ssSkP357("1")
<=> $false )
& ( ssSkP357("2")
<=> $false )
& ( ssSkP357("3")
<=> $false ) ) ).
fof(ssSkP358,fi_predicates,
( ( ssSkP358("1")
<=> $false )
& ( ssSkP358("2")
<=> $false )
& ( ssSkP358("3")
<=> $false ) ) ).
fof(ssSkP359,fi_predicates,
( ( ssSkP359("1")
<=> $false )
& ( ssSkP359("2")
<=> $false )
& ( ssSkP359("3")
<=> $false ) ) ).
fof(ssSkP36,fi_predicates,
! [X1] :
( ssSkP36(X1)
<=> $true ) ).
fof(ssSkP360,fi_predicates,
( ( ssSkP360("1")
<=> $false )
& ( ssSkP360("2")
<=> $false )
& ( ssSkP360("3")
<=> $false ) ) ).
fof(ssSkP361,fi_predicates,
( ( ssSkP361("1")
<=> $false )
& ( ssSkP361("2")
<=> $false )
& ( ssSkP361("3")
<=> $false ) ) ).
fof(ssSkP362,fi_predicates,
( ( ssSkP362("1")
<=> $false )
& ( ssSkP362("2")
<=> $false )
& ( ssSkP362("3")
<=> $false ) ) ).
fof(ssSkP363,fi_predicates,
( ( ssSkP363("1")
<=> $false )
& ( ssSkP363("2")
<=> $false )
& ( ssSkP363("3")
<=> $false ) ) ).
fof(ssSkP364,fi_predicates,
( ( ssSkP364("1")
<=> $true )
& ( ssSkP364("2")
<=> $true )
& ( ssSkP364("3")
<=> $false ) ) ).
fof(ssSkP365,fi_predicates,
( ( ssSkP365("1")
<=> $true )
& ( ssSkP365("2")
<=> $false )
& ( ssSkP365("3")
<=> $false ) ) ).
fof(ssSkP366,fi_predicates,
( ( ssSkP366("1")
<=> $true )
& ( ssSkP366("2")
<=> $false )
& ( ssSkP366("3")
<=> $false ) ) ).
fof(ssSkP367,fi_predicates,
( ( ssSkP367("1")
<=> $true )
& ( ssSkP367("2")
<=> $false )
& ( ssSkP367("3")
<=> $false ) ) ).
fof(ssSkP368,fi_predicates,
( ( ssSkP368("1")
<=> $true )
& ( ssSkP368("2")
<=> $false )
& ( ssSkP368("3")
<=> $false ) ) ).
fof(ssSkP369,fi_predicates,
( ( ssSkP369("1")
<=> $true )
& ( ssSkP369("2")
<=> $false )
& ( ssSkP369("3")
<=> $false ) ) ).
fof(ssSkP37,fi_predicates,
! [X1] :
( ssSkP37(X1)
<=> $true ) ).
fof(ssSkP370,fi_predicates,
( ( ssSkP370("1")
<=> $true )
& ( ssSkP370("2")
<=> $false )
& ( ssSkP370("3")
<=> $false ) ) ).
fof(ssSkP371,fi_predicates,
( ( ssSkP371("1")
<=> $true )
& ( ssSkP371("2")
<=> $false )
& ( ssSkP371("3")
<=> $false ) ) ).
fof(ssSkP372,fi_predicates,
( ( ssSkP372("1")
<=> $true )
& ( ssSkP372("2")
<=> $false )
& ( ssSkP372("3")
<=> $false ) ) ).
fof(ssSkP373,fi_predicates,
( ( ssSkP373("1","1")
<=> $true )
& ( ssSkP373("1","2")
<=> $true )
& ( ssSkP373("1","3")
<=> $true )
& ( ssSkP373("2","1")
<=> $true )
& ( ssSkP373("2","2")
<=> $true )
& ( ssSkP373("2","3")
<=> $true )
& ( ssSkP373("3","1")
<=> $true )
& ( ssSkP373("3","2")
<=> $true )
& ( ssSkP373("3","3")
<=> $true ) ) ).
fof(ssSkP374,fi_predicates,
( ( ssSkP374("1","1")
<=> $true )
& ( ssSkP374("1","2")
<=> $true )
& ( ssSkP374("1","3")
<=> $true )
& ( ssSkP374("2","1")
<=> $true )
& ( ssSkP374("2","2")
<=> $true )
& ( ssSkP374("2","3")
<=> $true )
& ( ssSkP374("3","1")
<=> $true )
& ( ssSkP374("3","2")
<=> $true )
& ( ssSkP374("3","3")
<=> $true ) ) ).
fof(ssSkP375,fi_predicates,
( ( ssSkP375("1")
<=> $false )
& ( ssSkP375("2")
<=> $false )
& ( ssSkP375("3")
<=> $false ) ) ).
fof(ssSkP376,fi_predicates,
( ( ssSkP376("1")
<=> $false )
& ( ssSkP376("2")
<=> $false )
& ( ssSkP376("3")
<=> $false ) ) ).
fof(ssSkP377,fi_predicates,
( ( ssSkP377("1")
<=> $false )
& ( ssSkP377("2")
<=> $false )
& ( ssSkP377("3")
<=> $false ) ) ).
fof(ssSkP378,fi_predicates,
( ( ssSkP378("1")
<=> $false )
& ( ssSkP378("2")
<=> $false )
& ( ssSkP378("3")
<=> $false ) ) ).
fof(ssSkP379,fi_predicates,
( ( ssSkP379("1")
<=> $false )
& ( ssSkP379("2")
<=> $false )
& ( ssSkP379("3")
<=> $false ) ) ).
fof(ssSkP38,fi_predicates,
! [X1] :
( ssSkP38(X1)
<=> $true ) ).
fof(ssSkP380,fi_predicates,
( ( ssSkP380("1")
<=> $false )
& ( ssSkP380("2")
<=> $false )
& ( ssSkP380("3")
<=> $false ) ) ).
fof(ssSkP381,fi_predicates,
( ( ssSkP381("1")
<=> $false )
& ( ssSkP381("2")
<=> $false )
& ( ssSkP381("3")
<=> $false ) ) ).
fof(ssSkP382,fi_predicates,
( ( ssSkP382("1")
<=> $false )
& ( ssSkP382("2")
<=> $false )
& ( ssSkP382("3")
<=> $false ) ) ).
fof(ssSkP383,fi_predicates,
( ( ssSkP383("1")
<=> $false )
& ( ssSkP383("2")
<=> $false )
& ( ssSkP383("3")
<=> $true ) ) ).
fof(ssSkP384,fi_predicates,
( ( ssSkP384("1")
<=> $false )
& ( ssSkP384("2")
<=> $false )
& ( ssSkP384("3")
<=> $false ) ) ).
fof(ssSkP385,fi_predicates,
( ( ssSkP385("1")
<=> $false )
& ( ssSkP385("2")
<=> $false )
& ( ssSkP385("3")
<=> $false ) ) ).
fof(ssSkP386,fi_predicates,
( ( ssSkP386("1")
<=> $false )
& ( ssSkP386("2")
<=> $false )
& ( ssSkP386("3")
<=> $false ) ) ).
fof(ssSkP387,fi_predicates,
( ( ssSkP387("1")
<=> $false )
& ( ssSkP387("2")
<=> $false )
& ( ssSkP387("3")
<=> $false ) ) ).
fof(ssSkP388,fi_predicates,
( ( ssSkP388("1")
<=> $true )
& ( ssSkP388("2")
<=> $true )
& ( ssSkP388("3")
<=> $true ) ) ).
fof(ssSkP389,fi_predicates,
( ( ssSkP389("1")
<=> $true )
& ( ssSkP389("2")
<=> $true )
& ( ssSkP389("3")
<=> $true ) ) ).
fof(ssSkP39,fi_predicates,
! [X1] :
( ssSkP39(X1)
<=> $true ) ).
fof(ssSkP390,fi_predicates,
( ( ssSkP390("1")
<=> $true )
& ( ssSkP390("2")
<=> $true )
& ( ssSkP390("3")
<=> $true ) ) ).
fof(ssSkP391,fi_predicates,
( ( ssSkP391("1")
<=> $true )
& ( ssSkP391("2")
<=> $true )
& ( ssSkP391("3")
<=> $true ) ) ).
fof(ssSkP392,fi_predicates,
( ( ssSkP392("1")
<=> $true )
& ( ssSkP392("2")
<=> $true )
& ( ssSkP392("3")
<=> $true ) ) ).
fof(ssSkP393,fi_predicates,
( ( ssSkP393("1")
<=> $true )
& ( ssSkP393("2")
<=> $true )
& ( ssSkP393("3")
<=> $true ) ) ).
fof(ssSkP394,fi_predicates,
( ( ssSkP394("1")
<=> $true )
& ( ssSkP394("2")
<=> $true )
& ( ssSkP394("3")
<=> $true ) ) ).
fof(ssSkP395,fi_predicates,
( ( ssSkP395("1")
<=> $true )
& ( ssSkP395("2")
<=> $true )
& ( ssSkP395("3")
<=> $true ) ) ).
fof(ssSkP396,fi_predicates,
( ( ssSkP396("1")
<=> $true )
& ( ssSkP396("2")
<=> $true )
& ( ssSkP396("3")
<=> $true ) ) ).
fof(ssSkP397,fi_predicates,
( ( ssSkP397("1")
<=> $true )
& ( ssSkP397("2")
<=> $true )
& ( ssSkP397("3")
<=> $true ) ) ).
fof(ssSkP398,fi_predicates,
( ( ssSkP398("1")
<=> $true )
& ( ssSkP398("2")
<=> $true )
& ( ssSkP398("3")
<=> $true ) ) ).
fof(ssSkP399,fi_predicates,
( ( ssSkP399("1")
<=> $false )
& ( ssSkP399("2")
<=> $false )
& ( ssSkP399("3")
<=> $true ) ) ).
fof(ssSkP4,fi_predicates,
( ( ssSkP4("1")
<=> $true )
& ( ssSkP4("2")
<=> $false )
& ( ssSkP4("3")
<=> $false ) ) ).
fof(ssSkP40,fi_predicates,
! [X1] :
( ssSkP40(X1)
<=> $true ) ).
fof(ssSkP400,fi_predicates,
( ( ssSkP400("1","1")
<=> $true )
& ( ssSkP400("1","2")
<=> $true )
& ( ssSkP400("1","3")
<=> $true )
& ( ssSkP400("2","1")
<=> $false )
& ( ssSkP400("2","2")
<=> $true )
& ( ssSkP400("2","3")
<=> $true )
& ( ssSkP400("3","1")
<=> $false )
& ( ssSkP400("3","2")
<=> $true )
& ( ssSkP400("3","3")
<=> $true ) ) ).
fof(ssSkP401,fi_predicates,
( ( ssSkP401("1","1")
<=> $true )
& ( ssSkP401("1","2")
<=> $true )
& ( ssSkP401("1","3")
<=> $true )
& ( ssSkP401("2","1")
<=> $false )
& ( ssSkP401("2","2")
<=> $true )
& ( ssSkP401("2","3")
<=> $true )
& ( ssSkP401("3","1")
<=> $false )
& ( ssSkP401("3","2")
<=> $true )
& ( ssSkP401("3","3")
<=> $true ) ) ).
fof(ssSkP402,fi_predicates,
( ( ssSkP402("1")
<=> $false )
& ( ssSkP402("2")
<=> $false )
& ( ssSkP402("3")
<=> $false ) ) ).
fof(ssSkP403,fi_predicates,
( ( ssSkP403("1")
<=> $false )
& ( ssSkP403("2")
<=> $false )
& ( ssSkP403("3")
<=> $false ) ) ).
fof(ssSkP404,fi_predicates,
( ( ssSkP404("1")
<=> $false )
& ( ssSkP404("2")
<=> $false )
& ( ssSkP404("3")
<=> $false ) ) ).
fof(ssSkP405,fi_predicates,
( ( ssSkP405("1")
<=> $false )
& ( ssSkP405("2")
<=> $false )
& ( ssSkP405("3")
<=> $false ) ) ).
fof(ssSkP406,fi_predicates,
( ( ssSkP406("1")
<=> $false )
& ( ssSkP406("2")
<=> $false )
& ( ssSkP406("3")
<=> $false ) ) ).
fof(ssSkP407,fi_predicates,
( ( ssSkP407("1")
<=> $false )
& ( ssSkP407("2")
<=> $false )
& ( ssSkP407("3")
<=> $false ) ) ).
fof(ssSkP408,fi_predicates,
( ( ssSkP408("1")
<=> $false )
& ( ssSkP408("2")
<=> $false )
& ( ssSkP408("3")
<=> $false ) ) ).
fof(ssSkP409,fi_predicates,
( ( ssSkP409("1")
<=> $false )
& ( ssSkP409("2")
<=> $false )
& ( ssSkP409("3")
<=> $false ) ) ).
fof(ssSkP41,fi_predicates,
! [X1] :
( ssSkP41(X1)
<=> $true ) ).
fof(ssSkP410,fi_predicates,
( ( ssSkP410("1")
<=> $false )
& ( ssSkP410("2")
<=> $false )
& ( ssSkP410("3")
<=> $false ) ) ).
fof(ssSkP411,fi_predicates,
( ( ssSkP411("1")
<=> $false )
& ( ssSkP411("2")
<=> $false )
& ( ssSkP411("3")
<=> $false ) ) ).
fof(ssSkP412,fi_predicates,
( ( ssSkP412("1")
<=> $false )
& ( ssSkP412("2")
<=> $false )
& ( ssSkP412("3")
<=> $false ) ) ).
fof(ssSkP413,fi_predicates,
( ( ssSkP413("1")
<=> $false )
& ( ssSkP413("2")
<=> $false )
& ( ssSkP413("3")
<=> $false ) ) ).
fof(ssSkP414,fi_predicates,
( ( ssSkP414("1")
<=> $false )
& ( ssSkP414("2")
<=> $false )
& ( ssSkP414("3")
<=> $false ) ) ).
fof(ssSkP415,fi_predicates,
( ( ssSkP415("1")
<=> $false )
& ( ssSkP415("2")
<=> $false )
& ( ssSkP415("3")
<=> $false ) ) ).
fof(ssSkP416,fi_predicates,
( ( ssSkP416("1")
<=> $false )
& ( ssSkP416("2")
<=> $false )
& ( ssSkP416("3")
<=> $false ) ) ).
fof(ssSkP417,fi_predicates,
( ( ssSkP417("1")
<=> $false )
& ( ssSkP417("2")
<=> $false )
& ( ssSkP417("3")
<=> $false ) ) ).
fof(ssSkP418,fi_predicates,
( ( ssSkP418("1")
<=> $false )
& ( ssSkP418("2")
<=> $false )
& ( ssSkP418("3")
<=> $false ) ) ).
fof(ssSkP419,fi_predicates,
( ( ssSkP419("1")
<=> $false )
& ( ssSkP419("2")
<=> $false )
& ( ssSkP419("3")
<=> $false ) ) ).
fof(ssSkP42,fi_predicates,
! [X1] :
( ssSkP42(X1)
<=> $true ) ).
fof(ssSkP420,fi_predicates,
( ( ssSkP420("1")
<=> $false )
& ( ssSkP420("2")
<=> $false )
& ( ssSkP420("3")
<=> $false ) ) ).
fof(ssSkP421,fi_predicates,
( ( ssSkP421("1")
<=> $false )
& ( ssSkP421("2")
<=> $false )
& ( ssSkP421("3")
<=> $false ) ) ).
fof(ssSkP422,fi_predicates,
( ( ssSkP422("1")
<=> $false )
& ( ssSkP422("2")
<=> $false )
& ( ssSkP422("3")
<=> $false ) ) ).
fof(ssSkP423,fi_predicates,
( ( ssSkP423("1")
<=> $true )
& ( ssSkP423("2")
<=> $false )
& ( ssSkP423("3")
<=> $false ) ) ).
fof(ssSkP424,fi_predicates,
( ( ssSkP424("1")
<=> $true )
& ( ssSkP424("2")
<=> $false )
& ( ssSkP424("3")
<=> $false ) ) ).
fof(ssSkP425,fi_predicates,
( ( ssSkP425("1")
<=> $true )
& ( ssSkP425("2")
<=> $false )
& ( ssSkP425("3")
<=> $false ) ) ).
fof(ssSkP426,fi_predicates,
( ( ssSkP426("1")
<=> $true )
& ( ssSkP426("2")
<=> $false )
& ( ssSkP426("3")
<=> $false ) ) ).
fof(ssSkP427,fi_predicates,
( ( ssSkP427("1")
<=> $true )
& ( ssSkP427("2")
<=> $false )
& ( ssSkP427("3")
<=> $false ) ) ).
fof(ssSkP428,fi_predicates,
( ( ssSkP428("1","1")
<=> $true )
& ( ssSkP428("1","2")
<=> $true )
& ( ssSkP428("1","3")
<=> $true )
& ( ssSkP428("2","1")
<=> $false )
& ( ssSkP428("2","2")
<=> $true )
& ( ssSkP428("2","3")
<=> $true )
& ( ssSkP428("3","1")
<=> $false )
& ( ssSkP428("3","2")
<=> $true )
& ( ssSkP428("3","3")
<=> $true ) ) ).
fof(ssSkP429,fi_predicates,
( ( ssSkP429("1","1")
<=> $true )
& ( ssSkP429("1","2")
<=> $true )
& ( ssSkP429("1","3")
<=> $true )
& ( ssSkP429("2","1")
<=> $false )
& ( ssSkP429("2","2")
<=> $true )
& ( ssSkP429("2","3")
<=> $true )
& ( ssSkP429("3","1")
<=> $false )
& ( ssSkP429("3","2")
<=> $true )
& ( ssSkP429("3","3")
<=> $true ) ) ).
fof(ssSkP43,fi_predicates,
! [X1] :
( ssSkP43(X1)
<=> $true ) ).
fof(ssSkP430,fi_predicates,
( ( ssSkP430("1")
<=> $false )
& ( ssSkP430("2")
<=> $false )
& ( ssSkP430("3")
<=> $false ) ) ).
fof(ssSkP431,fi_predicates,
( ( ssSkP431("1")
<=> $false )
& ( ssSkP431("2")
<=> $false )
& ( ssSkP431("3")
<=> $false ) ) ).
fof(ssSkP432,fi_predicates,
( ( ssSkP432("1")
<=> $false )
& ( ssSkP432("2")
<=> $false )
& ( ssSkP432("3")
<=> $false ) ) ).
fof(ssSkP433,fi_predicates,
( ( ssSkP433("1")
<=> $false )
& ( ssSkP433("2")
<=> $false )
& ( ssSkP433("3")
<=> $false ) ) ).
fof(ssSkP434,fi_predicates,
( ( ssSkP434("1")
<=> $false )
& ( ssSkP434("2")
<=> $false )
& ( ssSkP434("3")
<=> $false ) ) ).
fof(ssSkP435,fi_predicates,
( ( ssSkP435("1")
<=> $false )
& ( ssSkP435("2")
<=> $false )
& ( ssSkP435("3")
<=> $false ) ) ).
fof(ssSkP436,fi_predicates,
( ( ssSkP436("1")
<=> $false )
& ( ssSkP436("2")
<=> $false )
& ( ssSkP436("3")
<=> $false ) ) ).
fof(ssSkP437,fi_predicates,
( ( ssSkP437("1")
<=> $false )
& ( ssSkP437("2")
<=> $false )
& ( ssSkP437("3")
<=> $false ) ) ).
fof(ssSkP438,fi_predicates,
( ( ssSkP438("1")
<=> $false )
& ( ssSkP438("2")
<=> $false )
& ( ssSkP438("3")
<=> $false ) ) ).
fof(ssSkP439,fi_predicates,
( ( ssSkP439("1")
<=> $false )
& ( ssSkP439("2")
<=> $false )
& ( ssSkP439("3")
<=> $false ) ) ).
fof(ssSkP44,fi_predicates,
! [X1] :
( ssSkP44(X1)
<=> $true ) ).
fof(ssSkP440,fi_predicates,
( ( ssSkP440("1")
<=> $false )
& ( ssSkP440("2")
<=> $false )
& ( ssSkP440("3")
<=> $false ) ) ).
fof(ssSkP441,fi_predicates,
( ( ssSkP441("1")
<=> $false )
& ( ssSkP441("2")
<=> $false )
& ( ssSkP441("3")
<=> $false ) ) ).
fof(ssSkP442,fi_predicates,
( ( ssSkP442("1")
<=> $false )
& ( ssSkP442("2")
<=> $false )
& ( ssSkP442("3")
<=> $false ) ) ).
fof(ssSkP443,fi_predicates,
( ( ssSkP443("1")
<=> $false )
& ( ssSkP443("2")
<=> $false )
& ( ssSkP443("3")
<=> $false ) ) ).
fof(ssSkP444,fi_predicates,
( ( ssSkP444("1")
<=> $false )
& ( ssSkP444("2")
<=> $false )
& ( ssSkP444("3")
<=> $false ) ) ).
fof(ssSkP445,fi_predicates,
( ( ssSkP445("1")
<=> $false )
& ( ssSkP445("2")
<=> $false )
& ( ssSkP445("3")
<=> $false ) ) ).
fof(ssSkP446,fi_predicates,
( ( ssSkP446("1")
<=> $false )
& ( ssSkP446("2")
<=> $false )
& ( ssSkP446("3")
<=> $false ) ) ).
fof(ssSkP447,fi_predicates,
( ( ssSkP447("1")
<=> $false )
& ( ssSkP447("2")
<=> $false )
& ( ssSkP447("3")
<=> $false ) ) ).
fof(ssSkP448,fi_predicates,
( ( ssSkP448("1")
<=> $false )
& ( ssSkP448("2")
<=> $false )
& ( ssSkP448("3")
<=> $false ) ) ).
fof(ssSkP449,fi_predicates,
( ( ssSkP449("1")
<=> $false )
& ( ssSkP449("2")
<=> $false )
& ( ssSkP449("3")
<=> $false ) ) ).
fof(ssSkP45,fi_predicates,
! [X1] :
( ssSkP45(X1)
<=> $true ) ).
fof(ssSkP450,fi_predicates,
( ( ssSkP450("1")
<=> $false )
& ( ssSkP450("2")
<=> $false )
& ( ssSkP450("3")
<=> $false ) ) ).
fof(ssSkP451,fi_predicates,
( ( ssSkP451("1")
<=> $false )
& ( ssSkP451("2")
<=> $false )
& ( ssSkP451("3")
<=> $false ) ) ).
fof(ssSkP452,fi_predicates,
( ( ssSkP452("1")
<=> $false )
& ( ssSkP452("2")
<=> $false )
& ( ssSkP452("3")
<=> $false ) ) ).
fof(ssSkP453,fi_predicates,
( ( ssSkP453("1")
<=> $false )
& ( ssSkP453("2")
<=> $false )
& ( ssSkP453("3")
<=> $false ) ) ).
fof(ssSkP454,fi_predicates,
( ( ssSkP454("1")
<=> $false )
& ( ssSkP454("2")
<=> $false )
& ( ssSkP454("3")
<=> $false ) ) ).
fof(ssSkP455,fi_predicates,
( ( ssSkP455("1")
<=> $false )
& ( ssSkP455("2")
<=> $false )
& ( ssSkP455("3")
<=> $false ) ) ).
fof(ssSkP456,fi_predicates,
( ( ssSkP456("1")
<=> $true )
& ( ssSkP456("2")
<=> $false )
& ( ssSkP456("3")
<=> $false ) ) ).
fof(ssSkP457,fi_predicates,
( ( ssSkP457("1")
<=> $true )
& ( ssSkP457("2")
<=> $false )
& ( ssSkP457("3")
<=> $false ) ) ).
fof(ssSkP458,fi_predicates,
( ( ssSkP458("1")
<=> $true )
& ( ssSkP458("2")
<=> $false )
& ( ssSkP458("3")
<=> $false ) ) ).
fof(ssSkP459,fi_predicates,
( ( ssSkP459("1")
<=> $true )
& ( ssSkP459("2")
<=> $false )
& ( ssSkP459("3")
<=> $false ) ) ).
fof(ssSkP46,fi_predicates,
! [X1] :
( ssSkP46(X1)
<=> $true ) ).
fof(ssSkP460,fi_predicates,
( ( ssSkP460("1")
<=> $true )
& ( ssSkP460("2")
<=> $false )
& ( ssSkP460("3")
<=> $false ) ) ).
fof(ssSkP461,fi_predicates,
( ( ssSkP461("1","1")
<=> $true )
& ( ssSkP461("1","2")
<=> $true )
& ( ssSkP461("1","3")
<=> $true )
& ( ssSkP461("2","1")
<=> $false )
& ( ssSkP461("2","2")
<=> $true )
& ( ssSkP461("2","3")
<=> $true )
& ( ssSkP461("3","1")
<=> $false )
& ( ssSkP461("3","2")
<=> $true )
& ( ssSkP461("3","3")
<=> $true ) ) ).
fof(ssSkP462,fi_predicates,
( ( ssSkP462("1","1")
<=> $true )
& ( ssSkP462("1","2")
<=> $true )
& ( ssSkP462("1","3")
<=> $true )
& ( ssSkP462("2","1")
<=> $false )
& ( ssSkP462("2","2")
<=> $true )
& ( ssSkP462("2","3")
<=> $true )
& ( ssSkP462("3","1")
<=> $false )
& ( ssSkP462("3","2")
<=> $true )
& ( ssSkP462("3","3")
<=> $true ) ) ).
fof(ssSkP463,fi_predicates,
( ( ssSkP463("1")
<=> $false )
& ( ssSkP463("2")
<=> $false )
& ( ssSkP463("3")
<=> $false ) ) ).
fof(ssSkP464,fi_predicates,
( ( ssSkP464("1")
<=> $false )
& ( ssSkP464("2")
<=> $false )
& ( ssSkP464("3")
<=> $false ) ) ).
fof(ssSkP465,fi_predicates,
( ( ssSkP465("1")
<=> $false )
& ( ssSkP465("2")
<=> $false )
& ( ssSkP465("3")
<=> $false ) ) ).
fof(ssSkP466,fi_predicates,
( ( ssSkP466("1")
<=> $false )
& ( ssSkP466("2")
<=> $false )
& ( ssSkP466("3")
<=> $false ) ) ).
fof(ssSkP467,fi_predicates,
( ( ssSkP467("1")
<=> $false )
& ( ssSkP467("2")
<=> $false )
& ( ssSkP467("3")
<=> $false ) ) ).
fof(ssSkP468,fi_predicates,
( ( ssSkP468("1")
<=> $false )
& ( ssSkP468("2")
<=> $false )
& ( ssSkP468("3")
<=> $false ) ) ).
fof(ssSkP469,fi_predicates,
( ( ssSkP469("1")
<=> $false )
& ( ssSkP469("2")
<=> $false )
& ( ssSkP469("3")
<=> $false ) ) ).
fof(ssSkP47,fi_predicates,
! [X1] :
( ssSkP47(X1)
<=> $true ) ).
fof(ssSkP470,fi_predicates,
( ( ssSkP470("1")
<=> $false )
& ( ssSkP470("2")
<=> $false )
& ( ssSkP470("3")
<=> $false ) ) ).
fof(ssSkP471,fi_predicates,
( ( ssSkP471("1")
<=> $false )
& ( ssSkP471("2")
<=> $false )
& ( ssSkP471("3")
<=> $false ) ) ).
fof(ssSkP472,fi_predicates,
( ( ssSkP472("1")
<=> $false )
& ( ssSkP472("2")
<=> $false )
& ( ssSkP472("3")
<=> $false ) ) ).
fof(ssSkP473,fi_predicates,
( ( ssSkP473("1")
<=> $false )
& ( ssSkP473("2")
<=> $false )
& ( ssSkP473("3")
<=> $false ) ) ).
fof(ssSkP474,fi_predicates,
( ( ssSkP474("1")
<=> $false )
& ( ssSkP474("2")
<=> $false )
& ( ssSkP474("3")
<=> $false ) ) ).
fof(ssSkP475,fi_predicates,
( ( ssSkP475("1")
<=> $false )
& ( ssSkP475("2")
<=> $false )
& ( ssSkP475("3")
<=> $false ) ) ).
fof(ssSkP476,fi_predicates,
( ( ssSkP476("1")
<=> $false )
& ( ssSkP476("2")
<=> $false )
& ( ssSkP476("3")
<=> $false ) ) ).
fof(ssSkP477,fi_predicates,
( ( ssSkP477("1")
<=> $false )
& ( ssSkP477("2")
<=> $false )
& ( ssSkP477("3")
<=> $false ) ) ).
fof(ssSkP478,fi_predicates,
( ( ssSkP478("1")
<=> $false )
& ( ssSkP478("2")
<=> $false )
& ( ssSkP478("3")
<=> $false ) ) ).
fof(ssSkP479,fi_predicates,
( ( ssSkP479("1")
<=> $false )
& ( ssSkP479("2")
<=> $false )
& ( ssSkP479("3")
<=> $false ) ) ).
fof(ssSkP48,fi_predicates,
! [X1] :
( ssSkP48(X1)
<=> $true ) ).
fof(ssSkP480,fi_predicates,
( ( ssSkP480("1")
<=> $false )
& ( ssSkP480("2")
<=> $false )
& ( ssSkP480("3")
<=> $false ) ) ).
fof(ssSkP481,fi_predicates,
( ( ssSkP481("1")
<=> $false )
& ( ssSkP481("2")
<=> $false )
& ( ssSkP481("3")
<=> $false ) ) ).
fof(ssSkP482,fi_predicates,
( ( ssSkP482("1")
<=> $false )
& ( ssSkP482("2")
<=> $false )
& ( ssSkP482("3")
<=> $false ) ) ).
fof(ssSkP483,fi_predicates,
( ( ssSkP483("1")
<=> $false )
& ( ssSkP483("2")
<=> $false )
& ( ssSkP483("3")
<=> $false ) ) ).
fof(ssSkP484,fi_predicates,
( ( ssSkP484("1")
<=> $false )
& ( ssSkP484("2")
<=> $false )
& ( ssSkP484("3")
<=> $false ) ) ).
fof(ssSkP485,fi_predicates,
( ( ssSkP485("1")
<=> $false )
& ( ssSkP485("2")
<=> $false )
& ( ssSkP485("3")
<=> $false ) ) ).
fof(ssSkP486,fi_predicates,
( ( ssSkP486("1")
<=> $false )
& ( ssSkP486("2")
<=> $false )
& ( ssSkP486("3")
<=> $false ) ) ).
fof(ssSkP487,fi_predicates,
( ( ssSkP487("1")
<=> $true )
& ( ssSkP487("2")
<=> $false )
& ( ssSkP487("3")
<=> $false ) ) ).
fof(ssSkP488,fi_predicates,
( ( ssSkP488("1")
<=> $true )
& ( ssSkP488("2")
<=> $false )
& ( ssSkP488("3")
<=> $false ) ) ).
fof(ssSkP489,fi_predicates,
( ( ssSkP489("1")
<=> $true )
& ( ssSkP489("2")
<=> $false )
& ( ssSkP489("3")
<=> $false ) ) ).
fof(ssSkP49,fi_predicates,
! [X1] :
( ssSkP49(X1)
<=> $true ) ).
fof(ssSkP490,fi_predicates,
( ( ssSkP490("1")
<=> $true )
& ( ssSkP490("2")
<=> $false )
& ( ssSkP490("3")
<=> $false ) ) ).
fof(ssSkP491,fi_predicates,
( ( ssSkP491("1")
<=> $true )
& ( ssSkP491("2")
<=> $false )
& ( ssSkP491("3")
<=> $false ) ) ).
fof(ssSkP492,fi_predicates,
( ( ssSkP492("1","1")
<=> $true )
& ( ssSkP492("1","2")
<=> $false )
& ( ssSkP492("1","3")
<=> $false )
& ( ssSkP492("2","1")
<=> $true )
& ( ssSkP492("2","2")
<=> $true )
& ( ssSkP492("2","3")
<=> $true )
& ( ssSkP492("3","1")
<=> $true )
& ( ssSkP492("3","2")
<=> $true )
& ( ssSkP492("3","3")
<=> $true ) ) ).
fof(ssSkP493,fi_predicates,
( ( ssSkP493("1","1")
<=> $true )
& ( ssSkP493("1","2")
<=> $false )
& ( ssSkP493("1","3")
<=> $false )
& ( ssSkP493("2","1")
<=> $true )
& ( ssSkP493("2","2")
<=> $true )
& ( ssSkP493("2","3")
<=> $true )
& ( ssSkP493("3","1")
<=> $true )
& ( ssSkP493("3","2")
<=> $true )
& ( ssSkP493("3","3")
<=> $true ) ) ).
fof(ssSkP494,fi_predicates,
( ( ssSkP494("1")
<=> $false )
& ( ssSkP494("2")
<=> $false )
& ( ssSkP494("3")
<=> $false ) ) ).
fof(ssSkP495,fi_predicates,
( ( ssSkP495("1")
<=> $false )
& ( ssSkP495("2")
<=> $false )
& ( ssSkP495("3")
<=> $false ) ) ).
fof(ssSkP496,fi_predicates,
( ( ssSkP496("1")
<=> $false )
& ( ssSkP496("2")
<=> $false )
& ( ssSkP496("3")
<=> $false ) ) ).
fof(ssSkP497,fi_predicates,
( ( ssSkP497("1")
<=> $false )
& ( ssSkP497("2")
<=> $false )
& ( ssSkP497("3")
<=> $false ) ) ).
fof(ssSkP498,fi_predicates,
( ( ssSkP498("1")
<=> $false )
& ( ssSkP498("2")
<=> $false )
& ( ssSkP498("3")
<=> $false ) ) ).
fof(ssSkP499,fi_predicates,
( ( ssSkP499("1")
<=> $false )
& ( ssSkP499("2")
<=> $false )
& ( ssSkP499("3")
<=> $false ) ) ).
fof(ssSkP5,fi_predicates,
( ( ssSkP5("1")
<=> $true )
& ( ssSkP5("2")
<=> $false )
& ( ssSkP5("3")
<=> $false ) ) ).
fof(ssSkP50,fi_predicates,
! [X1] :
( ssSkP50(X1)
<=> $true ) ).
fof(ssSkP500,fi_predicates,
( ( ssSkP500("1")
<=> $false )
& ( ssSkP500("2")
<=> $false )
& ( ssSkP500("3")
<=> $false ) ) ).
fof(ssSkP501,fi_predicates,
( ( ssSkP501("1")
<=> $false )
& ( ssSkP501("2")
<=> $false )
& ( ssSkP501("3")
<=> $false ) ) ).
fof(ssSkP502,fi_predicates,
( ( ssSkP502("1")
<=> $false )
& ( ssSkP502("2")
<=> $false )
& ( ssSkP502("3")
<=> $false ) ) ).
fof(ssSkP503,fi_predicates,
( ( ssSkP503("1")
<=> $false )
& ( ssSkP503("2")
<=> $false )
& ( ssSkP503("3")
<=> $false ) ) ).
fof(ssSkP504,fi_predicates,
( ( ssSkP504("1")
<=> $false )
& ( ssSkP504("2")
<=> $false )
& ( ssSkP504("3")
<=> $false ) ) ).
fof(ssSkP505,fi_predicates,
( ( ssSkP505("1")
<=> $false )
& ( ssSkP505("2")
<=> $false )
& ( ssSkP505("3")
<=> $false ) ) ).
fof(ssSkP506,fi_predicates,
( ( ssSkP506("1")
<=> $false )
& ( ssSkP506("2")
<=> $false )
& ( ssSkP506("3")
<=> $false ) ) ).
fof(ssSkP507,fi_predicates,
( ( ssSkP507("1")
<=> $false )
& ( ssSkP507("2")
<=> $false )
& ( ssSkP507("3")
<=> $false ) ) ).
fof(ssSkP508,fi_predicates,
( ( ssSkP508("1")
<=> $false )
& ( ssSkP508("2")
<=> $false )
& ( ssSkP508("3")
<=> $false ) ) ).
fof(ssSkP509,fi_predicates,
( ( ssSkP509("1")
<=> $false )
& ( ssSkP509("2")
<=> $false )
& ( ssSkP509("3")
<=> $false ) ) ).
fof(ssSkP51,fi_predicates,
! [X1] :
( ssSkP51(X1)
<=> $true ) ).
fof(ssSkP510,fi_predicates,
( ( ssSkP510("1")
<=> $false )
& ( ssSkP510("2")
<=> $false )
& ( ssSkP510("3")
<=> $false ) ) ).
fof(ssSkP511,fi_predicates,
( ( ssSkP511("1")
<=> $false )
& ( ssSkP511("2")
<=> $false )
& ( ssSkP511("3")
<=> $false ) ) ).
fof(ssSkP512,fi_predicates,
( ( ssSkP512("1")
<=> $false )
& ( ssSkP512("2")
<=> $false )
& ( ssSkP512("3")
<=> $false ) ) ).
fof(ssSkP513,fi_predicates,
( ( ssSkP513("1")
<=> $false )
& ( ssSkP513("2")
<=> $false )
& ( ssSkP513("3")
<=> $false ) ) ).
fof(ssSkP514,fi_predicates,
( ( ssSkP514("1")
<=> $false )
& ( ssSkP514("2")
<=> $false )
& ( ssSkP514("3")
<=> $false ) ) ).
fof(ssSkP515,fi_predicates,
( ( ssSkP515("1")
<=> $false )
& ( ssSkP515("2")
<=> $false )
& ( ssSkP515("3")
<=> $false ) ) ).
fof(ssSkP516,fi_predicates,
( ( ssSkP516("1")
<=> $false )
& ( ssSkP516("2")
<=> $false )
& ( ssSkP516("3")
<=> $false ) ) ).
fof(ssSkP517,fi_predicates,
( ( ssSkP517("1")
<=> $false )
& ( ssSkP517("2")
<=> $false )
& ( ssSkP517("3")
<=> $false ) ) ).
fof(ssSkP518,fi_predicates,
( ( ssSkP518("1")
<=> $false )
& ( ssSkP518("2")
<=> $false )
& ( ssSkP518("3")
<=> $false ) ) ).
fof(ssSkP519,fi_predicates,
( ( ssSkP519("1")
<=> $false )
& ( ssSkP519("2")
<=> $false )
& ( ssSkP519("3")
<=> $false ) ) ).
fof(ssSkP52,fi_predicates,
! [X1] :
( ssSkP52(X1)
<=> $true ) ).
fof(ssSkP520,fi_predicates,
( ( ssSkP520("1")
<=> $false )
& ( ssSkP520("2")
<=> $true )
& ( ssSkP520("3")
<=> $true ) ) ).
fof(ssSkP521,fi_predicates,
( ( ssSkP521("1")
<=> $false )
& ( ssSkP521("2")
<=> $true )
& ( ssSkP521("3")
<=> $true ) ) ).
fof(ssSkP522,fi_predicates,
( ( ssSkP522("1")
<=> $false )
& ( ssSkP522("2")
<=> $true )
& ( ssSkP522("3")
<=> $true ) ) ).
fof(ssSkP523,fi_predicates,
( ( ssSkP523("1")
<=> $false )
& ( ssSkP523("2")
<=> $true )
& ( ssSkP523("3")
<=> $true ) ) ).
fof(ssSkP524,fi_predicates,
( ( ssSkP524("1")
<=> $false )
& ( ssSkP524("2")
<=> $false )
& ( ssSkP524("3")
<=> $true ) ) ).
fof(ssSkP525,fi_predicates,
! [X1,X2] :
( ssSkP525(X1,X2)
<=> $true ) ).
fof(ssSkP526,fi_predicates,
! [X1,X2] :
( ssSkP526(X1,X2)
<=> $true ) ).
fof(ssSkP527,fi_predicates,
! [X1] :
( ssSkP527(X1)
<=> $true ) ).
fof(ssSkP528,fi_predicates,
! [X1] :
( ssSkP528(X1)
<=> $true ) ).
fof(ssSkP529,fi_predicates,
! [X1] :
( ssSkP529(X1)
<=> $true ) ).
fof(ssSkP53,fi_predicates,
( ( ssSkP53("1","1")
<=> $true )
& ( ssSkP53("1","2")
<=> $true )
& ( ssSkP53("1","3")
<=> $true )
& ( ssSkP53("2","1")
<=> $true )
& ( ssSkP53("2","2")
<=> $true )
& ( ssSkP53("2","3")
<=> $true )
& ( ssSkP53("3","1")
<=> $false )
& ( ssSkP53("3","2")
<=> $true )
& ( ssSkP53("3","3")
<=> $true ) ) ).
fof(ssSkP530,fi_predicates,
! [X1] :
( ssSkP530(X1)
<=> $true ) ).
fof(ssSkP531,fi_predicates,
! [X1] :
( ssSkP531(X1)
<=> $true ) ).
fof(ssSkP532,fi_predicates,
! [X1] :
( ssSkP532(X1)
<=> $true ) ).
fof(ssSkP533,fi_predicates,
! [X1] :
( ssSkP533(X1)
<=> $true ) ).
fof(ssSkP534,fi_predicates,
! [X1] :
( ssSkP534(X1)
<=> $true ) ).
fof(ssSkP535,fi_predicates,
! [X1] :
( ssSkP535(X1)
<=> $true ) ).
fof(ssSkP536,fi_predicates,
! [X1] :
( ssSkP536(X1)
<=> $true ) ).
fof(ssSkP537,fi_predicates,
! [X1] :
( ssSkP537(X1)
<=> $true ) ).
fof(ssSkP538,fi_predicates,
! [X1] :
( ssSkP538(X1)
<=> $true ) ).
fof(ssSkP539,fi_predicates,
! [X1] :
( ssSkP539(X1)
<=> $true ) ).
fof(ssSkP54,fi_predicates,
( ( ssSkP54("1","1")
<=> $true )
& ( ssSkP54("1","2")
<=> $true )
& ( ssSkP54("1","3")
<=> $true )
& ( ssSkP54("2","1")
<=> $true )
& ( ssSkP54("2","2")
<=> $true )
& ( ssSkP54("2","3")
<=> $true )
& ( ssSkP54("3","1")
<=> $false )
& ( ssSkP54("3","2")
<=> $true )
& ( ssSkP54("3","3")
<=> $true ) ) ).
fof(ssSkP540,fi_predicates,
! [X1] :
( ssSkP540(X1)
<=> $true ) ).
fof(ssSkP541,fi_predicates,
! [X1] :
( ssSkP541(X1)
<=> $true ) ).
fof(ssSkP542,fi_predicates,
! [X1] :
( ssSkP542(X1)
<=> $true ) ).
fof(ssSkP543,fi_predicates,
! [X1] :
( ssSkP543(X1)
<=> $true ) ).
fof(ssSkP544,fi_predicates,
! [X1] :
( ssSkP544(X1)
<=> $true ) ).
fof(ssSkP545,fi_predicates,
! [X1] :
( ssSkP545(X1)
<=> $true ) ).
fof(ssSkP546,fi_predicates,
! [X1] :
( ssSkP546(X1)
<=> $true ) ).
fof(ssSkP547,fi_predicates,
! [X1] :
( ssSkP547(X1)
<=> $true ) ).
fof(ssSkP548,fi_predicates,
! [X1] :
( ssSkP548(X1)
<=> $true ) ).
fof(ssSkP549,fi_predicates,
! [X1] :
( ssSkP549(X1)
<=> $true ) ).
fof(ssSkP55,fi_predicates,
( ( ssSkP55("1")
<=> $false )
& ( ssSkP55("2")
<=> $false )
& ( ssSkP55("3")
<=> $false ) ) ).
fof(ssSkP550,fi_predicates,
! [X1] :
( ssSkP550(X1)
<=> $true ) ).
fof(ssSkP551,fi_predicates,
! [X1] :
( ssSkP551(X1)
<=> $true ) ).
fof(ssSkP552,fi_predicates,
! [X1] :
( ssSkP552(X1)
<=> $true ) ).
fof(ssSkP553,fi_predicates,
! [X1] :
( ssSkP553(X1)
<=> $true ) ).
fof(ssSkP554,fi_predicates,
! [X1] :
( ssSkP554(X1)
<=> $true ) ).
fof(ssSkP555,fi_predicates,
! [X1] :
( ssSkP555(X1)
<=> $true ) ).
fof(ssSkP556,fi_predicates,
! [X1] :
( ssSkP556(X1)
<=> $true ) ).
fof(ssSkP557,fi_predicates,
( ( ssSkP557("1","1")
<=> $true )
& ( ssSkP557("1","2")
<=> $true )
& ( ssSkP557("1","3")
<=> $true )
& ( ssSkP557("2","1")
<=> $true )
& ( ssSkP557("2","2")
<=> $true )
& ( ssSkP557("2","3")
<=> $true )
& ( ssSkP557("3","1")
<=> $true )
& ( ssSkP557("3","2")
<=> $true )
& ( ssSkP557("3","3")
<=> $true ) ) ).
fof(ssSkP558,fi_predicates,
( ( ssSkP558("1","1")
<=> $true )
& ( ssSkP558("1","2")
<=> $true )
& ( ssSkP558("1","3")
<=> $true )
& ( ssSkP558("2","1")
<=> $true )
& ( ssSkP558("2","2")
<=> $true )
& ( ssSkP558("2","3")
<=> $true )
& ( ssSkP558("3","1")
<=> $true )
& ( ssSkP558("3","2")
<=> $true )
& ( ssSkP558("3","3")
<=> $true ) ) ).
fof(ssSkP559,fi_predicates,
( ( ssSkP559("1")
<=> $false )
& ( ssSkP559("2")
<=> $false )
& ( ssSkP559("3")
<=> $false ) ) ).
fof(ssSkP56,fi_predicates,
( ( ssSkP56("1")
<=> $false )
& ( ssSkP56("2")
<=> $false )
& ( ssSkP56("3")
<=> $false ) ) ).
fof(ssSkP560,fi_predicates,
( ( ssSkP560("1")
<=> $false )
& ( ssSkP560("2")
<=> $false )
& ( ssSkP560("3")
<=> $false ) ) ).
fof(ssSkP561,fi_predicates,
( ( ssSkP561("1")
<=> $false )
& ( ssSkP561("2")
<=> $false )
& ( ssSkP561("3")
<=> $false ) ) ).
fof(ssSkP562,fi_predicates,
( ( ssSkP562("1")
<=> $false )
& ( ssSkP562("2")
<=> $false )
& ( ssSkP562("3")
<=> $false ) ) ).
fof(ssSkP563,fi_predicates,
( ( ssSkP563("1")
<=> $false )
& ( ssSkP563("2")
<=> $false )
& ( ssSkP563("3")
<=> $false ) ) ).
fof(ssSkP564,fi_predicates,
( ( ssSkP564("1")
<=> $false )
& ( ssSkP564("2")
<=> $false )
& ( ssSkP564("3")
<=> $false ) ) ).
fof(ssSkP565,fi_predicates,
( ( ssSkP565("1")
<=> $false )
& ( ssSkP565("2")
<=> $false )
& ( ssSkP565("3")
<=> $false ) ) ).
fof(ssSkP566,fi_predicates,
( ( ssSkP566("1")
<=> $false )
& ( ssSkP566("2")
<=> $false )
& ( ssSkP566("3")
<=> $false ) ) ).
fof(ssSkP567,fi_predicates,
( ( ssSkP567("1")
<=> $false )
& ( ssSkP567("2")
<=> $false )
& ( ssSkP567("3")
<=> $false ) ) ).
fof(ssSkP568,fi_predicates,
( ( ssSkP568("1")
<=> $false )
& ( ssSkP568("2")
<=> $false )
& ( ssSkP568("3")
<=> $false ) ) ).
fof(ssSkP569,fi_predicates,
( ( ssSkP569("1")
<=> $false )
& ( ssSkP569("2")
<=> $false )
& ( ssSkP569("3")
<=> $false ) ) ).
fof(ssSkP57,fi_predicates,
( ( ssSkP57("1")
<=> $false )
& ( ssSkP57("2")
<=> $false )
& ( ssSkP57("3")
<=> $false ) ) ).
fof(ssSkP570,fi_predicates,
( ( ssSkP570("1")
<=> $false )
& ( ssSkP570("2")
<=> $false )
& ( ssSkP570("3")
<=> $false ) ) ).
fof(ssSkP571,fi_predicates,
( ( ssSkP571("1")
<=> $false )
& ( ssSkP571("2")
<=> $false )
& ( ssSkP571("3")
<=> $false ) ) ).
fof(ssSkP572,fi_predicates,
( ( ssSkP572("1")
<=> $false )
& ( ssSkP572("2")
<=> $false )
& ( ssSkP572("3")
<=> $false ) ) ).
fof(ssSkP573,fi_predicates,
( ( ssSkP573("1")
<=> $false )
& ( ssSkP573("2")
<=> $false )
& ( ssSkP573("3")
<=> $false ) ) ).
fof(ssSkP574,fi_predicates,
( ( ssSkP574("1")
<=> $false )
& ( ssSkP574("2")
<=> $true )
& ( ssSkP574("3")
<=> $true ) ) ).
fof(ssSkP575,fi_predicates,
( ( ssSkP575("1")
<=> $false )
& ( ssSkP575("2")
<=> $true )
& ( ssSkP575("3")
<=> $true ) ) ).
fof(ssSkP576,fi_predicates,
( ( ssSkP576("1")
<=> $false )
& ( ssSkP576("2")
<=> $true )
& ( ssSkP576("3")
<=> $true ) ) ).
fof(ssSkP577,fi_predicates,
( ( ssSkP577("1")
<=> $false )
& ( ssSkP577("2")
<=> $true )
& ( ssSkP577("3")
<=> $true ) ) ).
fof(ssSkP578,fi_predicates,
( ( ssSkP578("1")
<=> $false )
& ( ssSkP578("2")
<=> $true )
& ( ssSkP578("3")
<=> $true ) ) ).
fof(ssSkP579,fi_predicates,
( ( ssSkP579("1")
<=> $true )
& ( ssSkP579("2")
<=> $true )
& ( ssSkP579("3")
<=> $true ) ) ).
fof(ssSkP58,fi_predicates,
( ( ssSkP58("1")
<=> $false )
& ( ssSkP58("2")
<=> $false )
& ( ssSkP58("3")
<=> $false ) ) ).
fof(ssSkP580,fi_predicates,
( ( ssSkP580("1")
<=> $true )
& ( ssSkP580("2")
<=> $true )
& ( ssSkP580("3")
<=> $true ) ) ).
fof(ssSkP581,fi_predicates,
( ( ssSkP581("1")
<=> $true )
& ( ssSkP581("2")
<=> $true )
& ( ssSkP581("3")
<=> $true ) ) ).
fof(ssSkP582,fi_predicates,
( ( ssSkP582("1")
<=> $true )
& ( ssSkP582("2")
<=> $true )
& ( ssSkP582("3")
<=> $true ) ) ).
fof(ssSkP583,fi_predicates,
( ( ssSkP583("1")
<=> $true )
& ( ssSkP583("2")
<=> $true )
& ( ssSkP583("3")
<=> $true ) ) ).
fof(ssSkP584,fi_predicates,
( ( ssSkP584("1")
<=> $true )
& ( ssSkP584("2")
<=> $false )
& ( ssSkP584("3")
<=> $false ) ) ).
fof(ssSkP585,fi_predicates,
! [X1,X2] :
( ssSkP585(X1,X2)
<=> $true ) ).
fof(ssSkP586,fi_predicates,
! [X1,X2] :
( ssSkP586(X1,X2)
<=> $true ) ).
fof(ssSkP587,fi_predicates,
! [X1] :
( ssSkP587(X1)
<=> $false ) ).
fof(ssSkP588,fi_predicates,
! [X1] :
( ssSkP588(X1)
<=> $false ) ).
fof(ssSkP589,fi_predicates,
! [X1] :
( ssSkP589(X1)
<=> $false ) ).
fof(ssSkP59,fi_predicates,
( ( ssSkP59("1")
<=> $false )
& ( ssSkP59("2")
<=> $false )
& ( ssSkP59("3")
<=> $false ) ) ).
fof(ssSkP590,fi_predicates,
! [X1] :
( ssSkP590(X1)
<=> $false ) ).
fof(ssSkP591,fi_predicates,
! [X1] :
( ssSkP591(X1)
<=> $false ) ).
fof(ssSkP592,fi_predicates,
! [X1] :
( ssSkP592(X1)
<=> $false ) ).
fof(ssSkP593,fi_predicates,
! [X1] :
( ssSkP593(X1)
<=> $false ) ).
fof(ssSkP594,fi_predicates,
! [X1] :
( ssSkP594(X1)
<=> $false ) ).
fof(ssSkP595,fi_predicates,
! [X1] :
( ssSkP595(X1)
<=> $false ) ).
fof(ssSkP596,fi_predicates,
! [X1] :
( ssSkP596(X1)
<=> $false ) ).
fof(ssSkP597,fi_predicates,
! [X1] :
( ssSkP597(X1)
<=> $false ) ).
fof(ssSkP598,fi_predicates,
! [X1] :
( ssSkP598(X1)
<=> $true ) ).
fof(ssSkP599,fi_predicates,
! [X1] :
( ssSkP599(X1)
<=> $true ) ).
fof(ssSkP6,fi_predicates,
( ( ssSkP6("1")
<=> $true )
& ( ssSkP6("2")
<=> $false )
& ( ssSkP6("3")
<=> $false ) ) ).
fof(ssSkP60,fi_predicates,
( ( ssSkP60("1")
<=> $false )
& ( ssSkP60("2")
<=> $false )
& ( ssSkP60("3")
<=> $false ) ) ).
fof(ssSkP600,fi_predicates,
! [X1] :
( ssSkP600(X1)
<=> $true ) ).
fof(ssSkP601,fi_predicates,
! [X1] :
( ssSkP601(X1)
<=> $true ) ).
fof(ssSkP602,fi_predicates,
! [X1] :
( ssSkP602(X1)
<=> $true ) ).
fof(ssSkP603,fi_predicates,
! [X1] :
( ssSkP603(X1)
<=> $true ) ).
fof(ssSkP604,fi_predicates,
! [X1] :
( ssSkP604(X1)
<=> $true ) ).
fof(ssSkP605,fi_predicates,
! [X1] :
( ssSkP605(X1)
<=> $true ) ).
fof(ssSkP606,fi_predicates,
! [X1] :
( ssSkP606(X1)
<=> $true ) ).
fof(ssSkP607,fi_predicates,
! [X1] :
( ssSkP607(X1)
<=> $true ) ).
fof(ssSkP608,fi_predicates,
! [X1] :
( ssSkP608(X1)
<=> $true ) ).
fof(ssSkP609,fi_predicates,
! [X1] :
( ssSkP609(X1)
<=> $true ) ).
fof(ssSkP61,fi_predicates,
( ( ssSkP61("1")
<=> $false )
& ( ssSkP61("2")
<=> $false )
& ( ssSkP61("3")
<=> $false ) ) ).
fof(ssSkP610,fi_predicates,
! [X1] :
( ssSkP610(X1)
<=> $true ) ).
fof(ssSkP611,fi_predicates,
! [X1] :
( ssSkP611(X1)
<=> $true ) ).
fof(ssSkP612,fi_predicates,
! [X1] :
( ssSkP612(X1)
<=> $true ) ).
fof(ssSkP613,fi_predicates,
( ( ssSkP613("1","1")
<=> $true )
& ( ssSkP613("1","2")
<=> $true )
& ( ssSkP613("1","3")
<=> $true )
& ( ssSkP613("2","1")
<=> $true )
& ( ssSkP613("2","2")
<=> $true )
& ( ssSkP613("2","3")
<=> $true )
& ( ssSkP613("3","1")
<=> $true )
& ( ssSkP613("3","2")
<=> $true )
& ( ssSkP613("3","3")
<=> $true ) ) ).
fof(ssSkP614,fi_predicates,
( ( ssSkP614("1","1")
<=> $true )
& ( ssSkP614("1","2")
<=> $true )
& ( ssSkP614("1","3")
<=> $true )
& ( ssSkP614("2","1")
<=> $true )
& ( ssSkP614("2","2")
<=> $true )
& ( ssSkP614("2","3")
<=> $true )
& ( ssSkP614("3","1")
<=> $true )
& ( ssSkP614("3","2")
<=> $true )
& ( ssSkP614("3","3")
<=> $true ) ) ).
fof(ssSkP615,fi_predicates,
( ( ssSkP615("1")
<=> $false )
& ( ssSkP615("2")
<=> $false )
& ( ssSkP615("3")
<=> $false ) ) ).
fof(ssSkP616,fi_predicates,
( ( ssSkP616("1")
<=> $false )
& ( ssSkP616("2")
<=> $true )
& ( ssSkP616("3")
<=> $true ) ) ).
fof(ssSkP617,fi_predicates,
( ( ssSkP617("1")
<=> $false )
& ( ssSkP617("2")
<=> $true )
& ( ssSkP617("3")
<=> $true ) ) ).
fof(ssSkP618,fi_predicates,
( ( ssSkP618("1")
<=> $false )
& ( ssSkP618("2")
<=> $true )
& ( ssSkP618("3")
<=> $true ) ) ).
fof(ssSkP619,fi_predicates,
( ( ssSkP619("1")
<=> $false )
& ( ssSkP619("2")
<=> $true )
& ( ssSkP619("3")
<=> $true ) ) ).
fof(ssSkP62,fi_predicates,
( ( ssSkP62("1")
<=> $true )
& ( ssSkP62("2")
<=> $true )
& ( ssSkP62("3")
<=> $false ) ) ).
fof(ssSkP620,fi_predicates,
( ( ssSkP620("1")
<=> $false )
& ( ssSkP620("2")
<=> $true )
& ( ssSkP620("3")
<=> $true ) ) ).
fof(ssSkP621,fi_predicates,
( ( ssSkP621("1")
<=> $false )
& ( ssSkP621("2")
<=> $true )
& ( ssSkP621("3")
<=> $true ) ) ).
fof(ssSkP622,fi_predicates,
( ( ssSkP622("1")
<=> $false )
& ( ssSkP622("2")
<=> $true )
& ( ssSkP622("3")
<=> $true ) ) ).
fof(ssSkP623,fi_predicates,
( ( ssSkP623("1")
<=> $false )
& ( ssSkP623("2")
<=> $true )
& ( ssSkP623("3")
<=> $true ) ) ).
fof(ssSkP624,fi_predicates,
( ( ssSkP624("1")
<=> $false )
& ( ssSkP624("2")
<=> $true )
& ( ssSkP624("3")
<=> $true ) ) ).
fof(ssSkP625,fi_predicates,
( ( ssSkP625("1")
<=> $false )
& ( ssSkP625("2")
<=> $true )
& ( ssSkP625("3")
<=> $true ) ) ).
fof(ssSkP626,fi_predicates,
( ( ssSkP626("1")
<=> $true )
& ( ssSkP626("2")
<=> $true )
& ( ssSkP626("3")
<=> $true ) ) ).
fof(ssSkP627,fi_predicates,
( ( ssSkP627("1")
<=> $true )
& ( ssSkP627("2")
<=> $true )
& ( ssSkP627("3")
<=> $true ) ) ).
fof(ssSkP628,fi_predicates,
( ( ssSkP628("1")
<=> $true )
& ( ssSkP628("2")
<=> $true )
& ( ssSkP628("3")
<=> $true ) ) ).
fof(ssSkP629,fi_predicates,
( ( ssSkP629("1")
<=> $true )
& ( ssSkP629("2")
<=> $true )
& ( ssSkP629("3")
<=> $true ) ) ).
fof(ssSkP63,fi_predicates,
( ( ssSkP63("1")
<=> $true )
& ( ssSkP63("2")
<=> $false )
& ( ssSkP63("3")
<=> $false ) ) ).
fof(ssSkP630,fi_predicates,
( ( ssSkP630("1")
<=> $true )
& ( ssSkP630("2")
<=> $true )
& ( ssSkP630("3")
<=> $true ) ) ).
fof(ssSkP631,fi_predicates,
( ( ssSkP631("1")
<=> $true )
& ( ssSkP631("2")
<=> $true )
& ( ssSkP631("3")
<=> $true ) ) ).
fof(ssSkP632,fi_predicates,
( ( ssSkP632("1")
<=> $true )
& ( ssSkP632("2")
<=> $true )
& ( ssSkP632("3")
<=> $true ) ) ).
fof(ssSkP633,fi_predicates,
( ( ssSkP633("1")
<=> $true )
& ( ssSkP633("2")
<=> $true )
& ( ssSkP633("3")
<=> $true ) ) ).
fof(ssSkP634,fi_predicates,
( ( ssSkP634("1")
<=> $true )
& ( ssSkP634("2")
<=> $true )
& ( ssSkP634("3")
<=> $true ) ) ).
fof(ssSkP635,fi_predicates,
( ( ssSkP635("1")
<=> $true )
& ( ssSkP635("2")
<=> $true )
& ( ssSkP635("3")
<=> $true ) ) ).
fof(ssSkP636,fi_predicates,
( ( ssSkP636("1")
<=> $true )
& ( ssSkP636("2")
<=> $true )
& ( ssSkP636("3")
<=> $true ) ) ).
fof(ssSkP637,fi_predicates,
( ( ssSkP637("1")
<=> $true )
& ( ssSkP637("2")
<=> $true )
& ( ssSkP637("3")
<=> $true ) ) ).
fof(ssSkP638,fi_predicates,
( ( ssSkP638("1")
<=> $true )
& ( ssSkP638("2")
<=> $true )
& ( ssSkP638("3")
<=> $true ) ) ).
fof(ssSkP639,fi_predicates,
( ( ssSkP639("1")
<=> $true )
& ( ssSkP639("2")
<=> $true )
& ( ssSkP639("3")
<=> $true ) ) ).
fof(ssSkP64,fi_predicates,
( ( ssSkP64("1")
<=> $true )
& ( ssSkP64("2")
<=> $false )
& ( ssSkP64("3")
<=> $false ) ) ).
fof(ssSkP640,fi_predicates,
( ( ssSkP640("1")
<=> $true )
& ( ssSkP640("2")
<=> $true )
& ( ssSkP640("3")
<=> $true ) ) ).
fof(ssSkP641,fi_predicates,
( ( ssSkP641("1")
<=> $true )
& ( ssSkP641("2")
<=> $true )
& ( ssSkP641("3")
<=> $true ) ) ).
fof(ssSkP642,fi_predicates,
( ( ssSkP642("1")
<=> $true )
& ( ssSkP642("2")
<=> $true )
& ( ssSkP642("3")
<=> $true ) ) ).
fof(ssSkP643,fi_predicates,
( ( ssSkP643("1")
<=> $true )
& ( ssSkP643("2")
<=> $false )
& ( ssSkP643("3")
<=> $false ) ) ).
fof(ssSkP644,fi_predicates,
! [X1,X2] :
( ssSkP644(X1,X2)
<=> $true ) ).
fof(ssSkP645,fi_predicates,
! [X1,X2] :
( ssSkP645(X1,X2)
<=> $true ) ).
fof(ssSkP646,fi_predicates,
! [X1] :
( ssSkP646(X1)
<=> $true ) ).
fof(ssSkP647,fi_predicates,
! [X1] :
( ssSkP647(X1)
<=> $true ) ).
fof(ssSkP648,fi_predicates,
! [X1] :
( ssSkP648(X1)
<=> $true ) ).
fof(ssSkP649,fi_predicates,
! [X1] :
( ssSkP649(X1)
<=> $true ) ).
fof(ssSkP65,fi_predicates,
( ( ssSkP65("1")
<=> $true )
& ( ssSkP65("2")
<=> $false )
& ( ssSkP65("3")
<=> $false ) ) ).
fof(ssSkP650,fi_predicates,
! [X1] :
( ssSkP650(X1)
<=> $true ) ).
fof(ssSkP651,fi_predicates,
! [X1] :
( ssSkP651(X1)
<=> $true ) ).
fof(ssSkP652,fi_predicates,
! [X1] :
( ssSkP652(X1)
<=> $true ) ).
fof(ssSkP653,fi_predicates,
! [X1] :
( ssSkP653(X1)
<=> $true ) ).
fof(ssSkP654,fi_predicates,
! [X1] :
( ssSkP654(X1)
<=> $true ) ).
fof(ssSkP655,fi_predicates,
! [X1] :
( ssSkP655(X1)
<=> $true ) ).
fof(ssSkP656,fi_predicates,
! [X1] :
( ssSkP656(X1)
<=> $true ) ).
fof(ssSkP657,fi_predicates,
! [X1] :
( ssSkP657(X1)
<=> $true ) ).
fof(ssSkP658,fi_predicates,
! [X1] :
( ssSkP658(X1)
<=> $true ) ).
fof(ssSkP659,fi_predicates,
! [X1] :
( ssSkP659(X1)
<=> $true ) ).
fof(ssSkP66,fi_predicates,
( ( ssSkP66("1")
<=> $true )
& ( ssSkP66("2")
<=> $false )
& ( ssSkP66("3")
<=> $false ) ) ).
fof(ssSkP660,fi_predicates,
! [X1] :
( ssSkP660(X1)
<=> $true ) ).
fof(ssSkP661,fi_predicates,
! [X1] :
( ssSkP661(X1)
<=> $true ) ).
fof(ssSkP662,fi_predicates,
! [X1] :
( ssSkP662(X1)
<=> $true ) ).
fof(ssSkP663,fi_predicates,
! [X1] :
( ssSkP663(X1)
<=> $true ) ).
fof(ssSkP664,fi_predicates,
! [X1] :
( ssSkP664(X1)
<=> $true ) ).
fof(ssSkP665,fi_predicates,
! [X1] :
( ssSkP665(X1)
<=> $true ) ).
fof(ssSkP666,fi_predicates,
! [X1] :
( ssSkP666(X1)
<=> $true ) ).
fof(ssSkP667,fi_predicates,
! [X1] :
( ssSkP667(X1)
<=> $true ) ).
fof(ssSkP668,fi_predicates,
! [X1] :
( ssSkP668(X1)
<=> $true ) ).
fof(ssSkP669,fi_predicates,
! [X1] :
( ssSkP669(X1)
<=> $true ) ).
fof(ssSkP67,fi_predicates,
( ( ssSkP67("1")
<=> $true )
& ( ssSkP67("2")
<=> $false )
& ( ssSkP67("3")
<=> $false ) ) ).
fof(ssSkP670,fi_predicates,
! [X1] :
( ssSkP670(X1)
<=> $true ) ).
fof(ssSkP671,fi_predicates,
! [X1] :
( ssSkP671(X1)
<=> $true ) ).
fof(ssSkP672,fi_predicates,
! [X1] :
( ssSkP672(X1)
<=> $true ) ).
fof(ssSkP673,fi_predicates,
! [X1] :
( ssSkP673(X1)
<=> $true ) ).
fof(ssSkP674,fi_predicates,
! [X1] :
( ssSkP674(X1)
<=> $true ) ).
fof(ssSkP675,fi_predicates,
! [X1] :
( ssSkP675(X1)
<=> $true ) ).
fof(ssSkP676,fi_predicates,
! [X1,X2] :
( ssSkP676(X1,X2)
<=> $true ) ).
fof(ssSkP677,fi_predicates,
! [X1,X2] :
( ssSkP677(X1,X2)
<=> $true ) ).
fof(ssSkP678,fi_predicates,
! [X1] :
( ssSkP678(X1)
<=> $false ) ).
fof(ssSkP679,fi_predicates,
! [X1] :
( ssSkP679(X1)
<=> $false ) ).
fof(ssSkP68,fi_predicates,
( ( ssSkP68("1")
<=> $true )
& ( ssSkP68("2")
<=> $true )
& ( ssSkP68("3")
<=> $true ) ) ).
fof(ssSkP680,fi_predicates,
! [X1] :
( ssSkP680(X1)
<=> $false ) ).
fof(ssSkP681,fi_predicates,
! [X1] :
( ssSkP681(X1)
<=> $false ) ).
fof(ssSkP682,fi_predicates,
! [X1] :
( ssSkP682(X1)
<=> $false ) ).
fof(ssSkP683,fi_predicates,
! [X1] :
( ssSkP683(X1)
<=> $false ) ).
fof(ssSkP684,fi_predicates,
! [X1] :
( ssSkP684(X1)
<=> $false ) ).
fof(ssSkP685,fi_predicates,
! [X1] :
( ssSkP685(X1)
<=> $false ) ).
fof(ssSkP686,fi_predicates,
! [X1] :
( ssSkP686(X1)
<=> $false ) ).
fof(ssSkP687,fi_predicates,
! [X1] :
( ssSkP687(X1)
<=> $false ) ).
fof(ssSkP688,fi_predicates,
! [X1] :
( ssSkP688(X1)
<=> $false ) ).
fof(ssSkP689,fi_predicates,
! [X1] :
( ssSkP689(X1)
<=> $true ) ).
fof(ssSkP69,fi_predicates,
( ( ssSkP69("1")
<=> $true )
& ( ssSkP69("2")
<=> $true )
& ( ssSkP69("3")
<=> $true ) ) ).
fof(ssSkP690,fi_predicates,
! [X1] :
( ssSkP690(X1)
<=> $true ) ).
fof(ssSkP691,fi_predicates,
! [X1] :
( ssSkP691(X1)
<=> $true ) ).
fof(ssSkP692,fi_predicates,
! [X1] :
( ssSkP692(X1)
<=> $true ) ).
fof(ssSkP693,fi_predicates,
! [X1] :
( ssSkP693(X1)
<=> $true ) ).
fof(ssSkP694,fi_predicates,
! [X1] :
( ssSkP694(X1)
<=> $true ) ).
fof(ssSkP695,fi_predicates,
! [X1] :
( ssSkP695(X1)
<=> $true ) ).
fof(ssSkP696,fi_predicates,
! [X1] :
( ssSkP696(X1)
<=> $true ) ).
fof(ssSkP697,fi_predicates,
! [X1] :
( ssSkP697(X1)
<=> $true ) ).
fof(ssSkP698,fi_predicates,
! [X1] :
( ssSkP698(X1)
<=> $true ) ).
fof(ssSkP699,fi_predicates,
! [X1] :
( ssSkP699(X1)
<=> $true ) ).
fof(ssSkP7,fi_predicates,
( ( ssSkP7("1")
<=> $true )
& ( ssSkP7("2")
<=> $false )
& ( ssSkP7("3")
<=> $false ) ) ).
fof(ssSkP70,fi_predicates,
( ( ssSkP70("1")
<=> $true )
& ( ssSkP70("2")
<=> $true )
& ( ssSkP70("3")
<=> $false ) ) ).
fof(ssSkP700,fi_predicates,
! [X1] :
( ssSkP700(X1)
<=> $true ) ).
fof(ssSkP701,fi_predicates,
! [X1] :
( ssSkP701(X1)
<=> $true ) ).
fof(ssSkP702,fi_predicates,
! [X1,X2] :
( ssSkP702(X1,X2)
<=> $true ) ).
fof(ssSkP703,fi_predicates,
! [X1,X2] :
( ssSkP703(X1,X2)
<=> $true ) ).
fof(ssSkP704,fi_predicates,
! [X1] :
( ssSkP704(X1)
<=> $false ) ).
fof(ssSkP705,fi_predicates,
! [X1] :
( ssSkP705(X1)
<=> $false ) ).
fof(ssSkP706,fi_predicates,
! [X1] :
( ssSkP706(X1)
<=> $false ) ).
fof(ssSkP707,fi_predicates,
! [X1] :
( ssSkP707(X1)
<=> $false ) ).
fof(ssSkP708,fi_predicates,
! [X1] :
( ssSkP708(X1)
<=> $false ) ).
fof(ssSkP709,fi_predicates,
! [X1] :
( ssSkP709(X1)
<=> $false ) ).
fof(ssSkP71,fi_predicates,
( ( ssSkP71("1")
<=> $true )
& ( ssSkP71("2")
<=> $true )
& ( ssSkP71("3")
<=> $false ) ) ).
fof(ssSkP710,fi_predicates,
! [X1] :
( ssSkP710(X1)
<=> $false ) ).
fof(ssSkP711,fi_predicates,
! [X1] :
( ssSkP711(X1)
<=> $false ) ).
fof(ssSkP712,fi_predicates,
! [X1] :
( ssSkP712(X1)
<=> $false ) ).
fof(ssSkP713,fi_predicates,
! [X1] :
( ssSkP713(X1)
<=> $false ) ).
fof(ssSkP714,fi_predicates,
! [X1] :
( ssSkP714(X1)
<=> $false ) ).
fof(ssSkP715,fi_predicates,
! [X1] :
( ssSkP715(X1)
<=> $false ) ).
fof(ssSkP716,fi_predicates,
! [X1] :
( ssSkP716(X1)
<=> $false ) ).
fof(ssSkP717,fi_predicates,
! [X1] :
( ssSkP717(X1)
<=> $false ) ).
fof(ssSkP718,fi_predicates,
! [X1] :
( ssSkP718(X1)
<=> $false ) ).
fof(ssSkP719,fi_predicates,
! [X1] :
( ssSkP719(X1)
<=> $false ) ).
fof(ssSkP72,fi_predicates,
( ( ssSkP72("1")
<=> $true )
& ( ssSkP72("2")
<=> $false )
& ( ssSkP72("3")
<=> $false ) ) ).
fof(ssSkP720,fi_predicates,
! [X1] :
( ssSkP720(X1)
<=> $false ) ).
fof(ssSkP721,fi_predicates,
! [X1] :
( ssSkP721(X1)
<=> $true ) ).
fof(ssSkP722,fi_predicates,
! [X1] :
( ssSkP722(X1)
<=> $true ) ).
fof(ssSkP723,fi_predicates,
! [X1] :
( ssSkP723(X1)
<=> $true ) ).
fof(ssSkP724,fi_predicates,
! [X1] :
( ssSkP724(X1)
<=> $true ) ).
fof(ssSkP725,fi_predicates,
! [X1] :
( ssSkP725(X1)
<=> $true ) ).
fof(ssSkP726,fi_predicates,
! [X1] :
( ssSkP726(X1)
<=> $true ) ).
fof(ssSkP727,fi_predicates,
! [X1] :
( ssSkP727(X1)
<=> $true ) ).
fof(ssSkP728,fi_predicates,
! [X1] :
( ssSkP728(X1)
<=> $true ) ).
fof(ssSkP729,fi_predicates,
! [X1] :
( ssSkP729(X1)
<=> $true ) ).
fof(ssSkP73,fi_predicates,
( ( ssSkP73("1","1")
<=> $true )
& ( ssSkP73("1","2")
<=> $true )
& ( ssSkP73("1","3")
<=> $true )
& ( ssSkP73("2","1")
<=> $true )
& ( ssSkP73("2","2")
<=> $true )
& ( ssSkP73("2","3")
<=> $true )
& ( ssSkP73("3","1")
<=> $true )
& ( ssSkP73("3","2")
<=> $true )
& ( ssSkP73("3","3")
<=> $true ) ) ).
fof(ssSkP730,fi_predicates,
! [X1] :
( ssSkP730(X1)
<=> $true ) ).
fof(ssSkP731,fi_predicates,
! [X1] :
( ssSkP731(X1)
<=> $true ) ).
fof(ssSkP732,fi_predicates,
! [X1] :
( ssSkP732(X1)
<=> $true ) ).
fof(ssSkP733,fi_predicates,
! [X1] :
( ssSkP733(X1)
<=> $true ) ).
fof(ssSkP734,fi_predicates,
! [X1] :
( ssSkP734(X1)
<=> $true ) ).
fof(ssSkP735,fi_predicates,
( ( ssSkP735("1","1")
<=> $true )
& ( ssSkP735("1","2")
<=> $true )
& ( ssSkP735("1","3")
<=> $true )
& ( ssSkP735("2","1")
<=> $false )
& ( ssSkP735("2","2")
<=> $true )
& ( ssSkP735("2","3")
<=> $true )
& ( ssSkP735("3","1")
<=> $false )
& ( ssSkP735("3","2")
<=> $true )
& ( ssSkP735("3","3")
<=> $true ) ) ).
fof(ssSkP736,fi_predicates,
( ( ssSkP736("1","1")
<=> $true )
& ( ssSkP736("1","2")
<=> $true )
& ( ssSkP736("1","3")
<=> $true )
& ( ssSkP736("2","1")
<=> $false )
& ( ssSkP736("2","2")
<=> $true )
& ( ssSkP736("2","3")
<=> $true )
& ( ssSkP736("3","1")
<=> $false )
& ( ssSkP736("3","2")
<=> $true )
& ( ssSkP736("3","3")
<=> $true ) ) ).
fof(ssSkP737,fi_predicates,
( ( ssSkP737("1")
<=> $true )
& ( ssSkP737("2")
<=> $false )
& ( ssSkP737("3")
<=> $false ) ) ).
fof(ssSkP738,fi_predicates,
( ( ssSkP738("1")
<=> $true )
& ( ssSkP738("2")
<=> $false )
& ( ssSkP738("3")
<=> $false ) ) ).
fof(ssSkP739,fi_predicates,
( ( ssSkP739("1")
<=> $true )
& ( ssSkP739("2")
<=> $false )
& ( ssSkP739("3")
<=> $false ) ) ).
fof(ssSkP74,fi_predicates,
( ( ssSkP74("1","1")
<=> $true )
& ( ssSkP74("1","2")
<=> $true )
& ( ssSkP74("1","3")
<=> $true )
& ( ssSkP74("2","1")
<=> $true )
& ( ssSkP74("2","2")
<=> $true )
& ( ssSkP74("2","3")
<=> $true )
& ( ssSkP74("3","1")
<=> $true )
& ( ssSkP74("3","2")
<=> $true )
& ( ssSkP74("3","3")
<=> $true ) ) ).
fof(ssSkP740,fi_predicates,
( ( ssSkP740("1")
<=> $true )
& ( ssSkP740("2")
<=> $false )
& ( ssSkP740("3")
<=> $false ) ) ).
fof(ssSkP741,fi_predicates,
( ( ssSkP741("1")
<=> $true )
& ( ssSkP741("2")
<=> $false )
& ( ssSkP741("3")
<=> $false ) ) ).
fof(ssSkP742,fi_predicates,
( ( ssSkP742("1")
<=> $true )
& ( ssSkP742("2")
<=> $false )
& ( ssSkP742("3")
<=> $false ) ) ).
fof(ssSkP743,fi_predicates,
( ( ssSkP743("1")
<=> $true )
& ( ssSkP743("2")
<=> $false )
& ( ssSkP743("3")
<=> $false ) ) ).
fof(ssSkP744,fi_predicates,
( ( ssSkP744("1")
<=> $true )
& ( ssSkP744("2")
<=> $false )
& ( ssSkP744("3")
<=> $false ) ) ).
fof(ssSkP745,fi_predicates,
( ( ssSkP745("1")
<=> $true )
& ( ssSkP745("2")
<=> $false )
& ( ssSkP745("3")
<=> $false ) ) ).
fof(ssSkP746,fi_predicates,
( ( ssSkP746("1")
<=> $true )
& ( ssSkP746("2")
<=> $false )
& ( ssSkP746("3")
<=> $false ) ) ).
fof(ssSkP747,fi_predicates,
( ( ssSkP747("1")
<=> $true )
& ( ssSkP747("2")
<=> $false )
& ( ssSkP747("3")
<=> $false ) ) ).
fof(ssSkP748,fi_predicates,
( ( ssSkP748("1")
<=> $true )
& ( ssSkP748("2")
<=> $false )
& ( ssSkP748("3")
<=> $false ) ) ).
fof(ssSkP749,fi_predicates,
( ( ssSkP749("1")
<=> $true )
& ( ssSkP749("2")
<=> $false )
& ( ssSkP749("3")
<=> $false ) ) ).
fof(ssSkP75,fi_predicates,
( ( ssSkP75("1")
<=> $false )
& ( ssSkP75("2")
<=> $false )
& ( ssSkP75("3")
<=> $false ) ) ).
fof(ssSkP750,fi_predicates,
( ( ssSkP750("1")
<=> $true )
& ( ssSkP750("2")
<=> $false )
& ( ssSkP750("3")
<=> $false ) ) ).
fof(ssSkP751,fi_predicates,
( ( ssSkP751("1")
<=> $true )
& ( ssSkP751("2")
<=> $false )
& ( ssSkP751("3")
<=> $false ) ) ).
fof(ssSkP752,fi_predicates,
( ( ssSkP752("1")
<=> $true )
& ( ssSkP752("2")
<=> $false )
& ( ssSkP752("3")
<=> $false ) ) ).
fof(ssSkP753,fi_predicates,
( ( ssSkP753("1")
<=> $true )
& ( ssSkP753("2")
<=> $false )
& ( ssSkP753("3")
<=> $true ) ) ).
fof(ssSkP754,fi_predicates,
( ( ssSkP754("1")
<=> $true )
& ( ssSkP754("2")
<=> $false )
& ( ssSkP754("3")
<=> $false ) ) ).
fof(ssSkP755,fi_predicates,
( ( ssSkP755("1")
<=> $true )
& ( ssSkP755("2")
<=> $false )
& ( ssSkP755("3")
<=> $false ) ) ).
fof(ssSkP756,fi_predicates,
( ( ssSkP756("1")
<=> $true )
& ( ssSkP756("2")
<=> $false )
& ( ssSkP756("3")
<=> $false ) ) ).
fof(ssSkP757,fi_predicates,
( ( ssSkP757("1")
<=> $true )
& ( ssSkP757("2")
<=> $false )
& ( ssSkP757("3")
<=> $false ) ) ).
fof(ssSkP758,fi_predicates,
( ( ssSkP758("1")
<=> $true )
& ( ssSkP758("2")
<=> $false )
& ( ssSkP758("3")
<=> $false ) ) ).
fof(ssSkP759,fi_predicates,
( ( ssSkP759("1")
<=> $true )
& ( ssSkP759("2")
<=> $false )
& ( ssSkP759("3")
<=> $false ) ) ).
fof(ssSkP76,fi_predicates,
( ( ssSkP76("1")
<=> $false )
& ( ssSkP76("2")
<=> $false )
& ( ssSkP76("3")
<=> $false ) ) ).
fof(ssSkP760,fi_predicates,
( ( ssSkP760("1")
<=> $true )
& ( ssSkP760("2")
<=> $false )
& ( ssSkP760("3")
<=> $true ) ) ).
fof(ssSkP761,fi_predicates,
( ( ssSkP761("1")
<=> $true )
& ( ssSkP761("2")
<=> $false )
& ( ssSkP761("3")
<=> $false ) ) ).
fof(ssSkP762,fi_predicates,
( ( ssSkP762("1")
<=> $true )
& ( ssSkP762("2")
<=> $false )
& ( ssSkP762("3")
<=> $false ) ) ).
fof(ssSkP763,fi_predicates,
( ( ssSkP763("1")
<=> $true )
& ( ssSkP763("2")
<=> $false )
& ( ssSkP763("3")
<=> $false ) ) ).
fof(ssSkP764,fi_predicates,
( ( ssSkP764("1")
<=> $true )
& ( ssSkP764("2")
<=> $false )
& ( ssSkP764("3")
<=> $false ) ) ).
fof(ssSkP765,fi_predicates,
( ( ssSkP765("1")
<=> $true )
& ( ssSkP765("2")
<=> $false )
& ( ssSkP765("3")
<=> $false ) ) ).
fof(ssSkP766,fi_predicates,
( ( ssSkP766("1")
<=> $true )
& ( ssSkP766("2")
<=> $false )
& ( ssSkP766("3")
<=> $false ) ) ).
fof(ssSkP767,fi_predicates,
( ( ssSkP767("1")
<=> $true )
& ( ssSkP767("2")
<=> $false )
& ( ssSkP767("3")
<=> $false ) ) ).
fof(ssSkP768,fi_predicates,
( ( ssSkP768("1","1")
<=> $true )
& ( ssSkP768("1","2")
<=> $true )
& ( ssSkP768("1","3")
<=> $true )
& ( ssSkP768("2","1")
<=> $false )
& ( ssSkP768("2","2")
<=> $true )
& ( ssSkP768("2","3")
<=> $true )
& ( ssSkP768("3","1")
<=> $false )
& ( ssSkP768("3","2")
<=> $true )
& ( ssSkP768("3","3")
<=> $true ) ) ).
fof(ssSkP769,fi_predicates,
( ( ssSkP769("1","1")
<=> $true )
& ( ssSkP769("1","2")
<=> $true )
& ( ssSkP769("1","3")
<=> $true )
& ( ssSkP769("2","1")
<=> $false )
& ( ssSkP769("2","2")
<=> $true )
& ( ssSkP769("2","3")
<=> $true )
& ( ssSkP769("3","1")
<=> $false )
& ( ssSkP769("3","2")
<=> $true )
& ( ssSkP769("3","3")
<=> $true ) ) ).
fof(ssSkP77,fi_predicates,
( ( ssSkP77("1")
<=> $false )
& ( ssSkP77("2")
<=> $false )
& ( ssSkP77("3")
<=> $false ) ) ).
fof(ssSkP770,fi_predicates,
( ( ssSkP770("1")
<=> $false )
& ( ssSkP770("2")
<=> $false )
& ( ssSkP770("3")
<=> $false ) ) ).
fof(ssSkP771,fi_predicates,
( ( ssSkP771("1")
<=> $false )
& ( ssSkP771("2")
<=> $false )
& ( ssSkP771("3")
<=> $false ) ) ).
fof(ssSkP772,fi_predicates,
( ( ssSkP772("1")
<=> $false )
& ( ssSkP772("2")
<=> $false )
& ( ssSkP772("3")
<=> $false ) ) ).
fof(ssSkP773,fi_predicates,
( ( ssSkP773("1")
<=> $false )
& ( ssSkP773("2")
<=> $false )
& ( ssSkP773("3")
<=> $false ) ) ).
fof(ssSkP774,fi_predicates,
( ( ssSkP774("1")
<=> $false )
& ( ssSkP774("2")
<=> $false )
& ( ssSkP774("3")
<=> $false ) ) ).
fof(ssSkP775,fi_predicates,
( ( ssSkP775("1")
<=> $false )
& ( ssSkP775("2")
<=> $false )
& ( ssSkP775("3")
<=> $false ) ) ).
fof(ssSkP776,fi_predicates,
( ( ssSkP776("1")
<=> $false )
& ( ssSkP776("2")
<=> $false )
& ( ssSkP776("3")
<=> $false ) ) ).
fof(ssSkP777,fi_predicates,
( ( ssSkP777("1")
<=> $false )
& ( ssSkP777("2")
<=> $false )
& ( ssSkP777("3")
<=> $false ) ) ).
fof(ssSkP778,fi_predicates,
( ( ssSkP778("1")
<=> $false )
& ( ssSkP778("2")
<=> $false )
& ( ssSkP778("3")
<=> $false ) ) ).
fof(ssSkP779,fi_predicates,
( ( ssSkP779("1")
<=> $false )
& ( ssSkP779("2")
<=> $false )
& ( ssSkP779("3")
<=> $false ) ) ).
fof(ssSkP78,fi_predicates,
( ( ssSkP78("1")
<=> $false )
& ( ssSkP78("2")
<=> $false )
& ( ssSkP78("3")
<=> $false ) ) ).
fof(ssSkP780,fi_predicates,
( ( ssSkP780("1")
<=> $false )
& ( ssSkP780("2")
<=> $false )
& ( ssSkP780("3")
<=> $false ) ) ).
fof(ssSkP781,fi_predicates,
( ( ssSkP781("1")
<=> $false )
& ( ssSkP781("2")
<=> $false )
& ( ssSkP781("3")
<=> $false ) ) ).
fof(ssSkP782,fi_predicates,
( ( ssSkP782("1")
<=> $false )
& ( ssSkP782("2")
<=> $false )
& ( ssSkP782("3")
<=> $false ) ) ).
fof(ssSkP783,fi_predicates,
( ( ssSkP783("1")
<=> $false )
& ( ssSkP783("2")
<=> $false )
& ( ssSkP783("3")
<=> $false ) ) ).
fof(ssSkP784,fi_predicates,
( ( ssSkP784("1")
<=> $false )
& ( ssSkP784("2")
<=> $false )
& ( ssSkP784("3")
<=> $false ) ) ).
fof(ssSkP785,fi_predicates,
( ( ssSkP785("1")
<=> $false )
& ( ssSkP785("2")
<=> $false )
& ( ssSkP785("3")
<=> $false ) ) ).
fof(ssSkP786,fi_predicates,
( ( ssSkP786("1")
<=> $true )
& ( ssSkP786("2")
<=> $true )
& ( ssSkP786("3")
<=> $false ) ) ).
fof(ssSkP787,fi_predicates,
( ( ssSkP787("1")
<=> $true )
& ( ssSkP787("2")
<=> $false )
& ( ssSkP787("3")
<=> $false ) ) ).
fof(ssSkP788,fi_predicates,
( ( ssSkP788("1")
<=> $true )
& ( ssSkP788("2")
<=> $false )
& ( ssSkP788("3")
<=> $false ) ) ).
fof(ssSkP789,fi_predicates,
( ( ssSkP789("1")
<=> $true )
& ( ssSkP789("2")
<=> $false )
& ( ssSkP789("3")
<=> $false ) ) ).
fof(ssSkP79,fi_predicates,
( ( ssSkP79("1")
<=> $false )
& ( ssSkP79("2")
<=> $false )
& ( ssSkP79("3")
<=> $false ) ) ).
fof(ssSkP790,fi_predicates,
( ( ssSkP790("1")
<=> $true )
& ( ssSkP790("2")
<=> $false )
& ( ssSkP790("3")
<=> $false ) ) ).
fof(ssSkP791,fi_predicates,
( ( ssSkP791("1")
<=> $true )
& ( ssSkP791("2")
<=> $false )
& ( ssSkP791("3")
<=> $false ) ) ).
fof(ssSkP792,fi_predicates,
( ( ssSkP792("1")
<=> $true )
& ( ssSkP792("2")
<=> $false )
& ( ssSkP792("3")
<=> $false ) ) ).
fof(ssSkP793,fi_predicates,
( ( ssSkP793("1")
<=> $true )
& ( ssSkP793("2")
<=> $false )
& ( ssSkP793("3")
<=> $false ) ) ).
fof(ssSkP794,fi_predicates,
( ( ssSkP794("1")
<=> $true )
& ( ssSkP794("2")
<=> $false )
& ( ssSkP794("3")
<=> $false ) ) ).
fof(ssSkP795,fi_predicates,
! [X1,X2] :
( ssSkP795(X1,X2)
<=> $true ) ).
fof(ssSkP796,fi_predicates,
! [X1,X2] :
( ssSkP796(X1,X2)
<=> $true ) ).
fof(ssSkP797,fi_predicates,
! [X1] :
( ssSkP797(X1)
<=> $false ) ).
fof(ssSkP798,fi_predicates,
! [X1] :
( ssSkP798(X1)
<=> $false ) ).
fof(ssSkP799,fi_predicates,
! [X1] :
( ssSkP799(X1)
<=> $false ) ).
fof(ssSkP8,fi_predicates,
( ( ssSkP8("1")
<=> $true )
& ( ssSkP8("2")
<=> $false )
& ( ssSkP8("3")
<=> $false ) ) ).
fof(ssSkP80,fi_predicates,
( ( ssSkP80("1")
<=> $false )
& ( ssSkP80("2")
<=> $false )
& ( ssSkP80("3")
<=> $false ) ) ).
fof(ssSkP800,fi_predicates,
! [X1] :
( ssSkP800(X1)
<=> $false ) ).
fof(ssSkP801,fi_predicates,
! [X1] :
( ssSkP801(X1)
<=> $false ) ).
fof(ssSkP802,fi_predicates,
! [X1] :
( ssSkP802(X1)
<=> $false ) ).
fof(ssSkP803,fi_predicates,
! [X1] :
( ssSkP803(X1)
<=> $false ) ).
fof(ssSkP804,fi_predicates,
! [X1] :
( ssSkP804(X1)
<=> $false ) ).
fof(ssSkP805,fi_predicates,
! [X1] :
( ssSkP805(X1)
<=> $false ) ).
fof(ssSkP806,fi_predicates,
! [X1] :
( ssSkP806(X1)
<=> $false ) ).
fof(ssSkP807,fi_predicates,
! [X1] :
( ssSkP807(X1)
<=> $true ) ).
fof(ssSkP808,fi_predicates,
! [X1] :
( ssSkP808(X1)
<=> $true ) ).
fof(ssSkP809,fi_predicates,
! [X1] :
( ssSkP809(X1)
<=> $true ) ).
fof(ssSkP81,fi_predicates,
( ( ssSkP81("1")
<=> $false )
& ( ssSkP81("2")
<=> $false )
& ( ssSkP81("3")
<=> $false ) ) ).
fof(ssSkP810,fi_predicates,
! [X1] :
( ssSkP810(X1)
<=> $true ) ).
fof(ssSkP811,fi_predicates,
! [X1] :
( ssSkP811(X1)
<=> $true ) ).
fof(ssSkP812,fi_predicates,
! [X1] :
( ssSkP812(X1)
<=> $true ) ).
fof(ssSkP813,fi_predicates,
! [X1] :
( ssSkP813(X1)
<=> $true ) ).
fof(ssSkP814,fi_predicates,
! [X1] :
( ssSkP814(X1)
<=> $true ) ).
fof(ssSkP815,fi_predicates,
! [X1] :
( ssSkP815(X1)
<=> $true ) ).
fof(ssSkP816,fi_predicates,
! [X1] :
( ssSkP816(X1)
<=> $true ) ).
fof(ssSkP817,fi_predicates,
! [X1] :
( ssSkP817(X1)
<=> $true ) ).
fof(ssSkP818,fi_predicates,
! [X1] :
( ssSkP818(X1)
<=> $true ) ).
fof(ssSkP819,fi_predicates,
! [X1] :
( ssSkP819(X1)
<=> $true ) ).
fof(ssSkP82,fi_predicates,
( ( ssSkP82("1")
<=> $false )
& ( ssSkP82("2")
<=> $false )
& ( ssSkP82("3")
<=> $false ) ) ).
fof(ssSkP820,fi_predicates,
! [X1] :
( ssSkP820(X1)
<=> $true ) ).
fof(ssSkP821,fi_predicates,
! [X1,X2] :
( ssSkP821(X1,X2)
<=> $true ) ).
fof(ssSkP822,fi_predicates,
! [X1,X2] :
( ssSkP822(X1,X2)
<=> $true ) ).
fof(ssSkP823,fi_predicates,
! [X1] :
( ssSkP823(X1)
<=> $true ) ).
fof(ssSkP824,fi_predicates,
! [X1] :
( ssSkP824(X1)
<=> $true ) ).
fof(ssSkP825,fi_predicates,
! [X1] :
( ssSkP825(X1)
<=> $true ) ).
fof(ssSkP826,fi_predicates,
! [X1] :
( ssSkP826(X1)
<=> $true ) ).
fof(ssSkP827,fi_predicates,
! [X1] :
( ssSkP827(X1)
<=> $true ) ).
fof(ssSkP828,fi_predicates,
! [X1] :
( ssSkP828(X1)
<=> $true ) ).
fof(ssSkP829,fi_predicates,
! [X1] :
( ssSkP829(X1)
<=> $true ) ).
fof(ssSkP83,fi_predicates,
( ( ssSkP83("1")
<=> $false )
& ( ssSkP83("2")
<=> $false )
& ( ssSkP83("3")
<=> $false ) ) ).
fof(ssSkP830,fi_predicates,
! [X1] :
( ssSkP830(X1)
<=> $true ) ).
fof(ssSkP831,fi_predicates,
! [X1] :
( ssSkP831(X1)
<=> $true ) ).
fof(ssSkP832,fi_predicates,
! [X1] :
( ssSkP832(X1)
<=> $true ) ).
fof(ssSkP833,fi_predicates,
! [X1] :
( ssSkP833(X1)
<=> $true ) ).
fof(ssSkP834,fi_predicates,
! [X1] :
( ssSkP834(X1)
<=> $true ) ).
fof(ssSkP835,fi_predicates,
! [X1] :
( ssSkP835(X1)
<=> $true ) ).
fof(ssSkP836,fi_predicates,
! [X1] :
( ssSkP836(X1)
<=> $true ) ).
fof(ssSkP837,fi_predicates,
! [X1] :
( ssSkP837(X1)
<=> $true ) ).
fof(ssSkP838,fi_predicates,
! [X1] :
( ssSkP838(X1)
<=> $true ) ).
fof(ssSkP839,fi_predicates,
! [X1] :
( ssSkP839(X1)
<=> $true ) ).
fof(ssSkP84,fi_predicates,
( ( ssSkP84("1")
<=> $false )
& ( ssSkP84("2")
<=> $false )
& ( ssSkP84("3")
<=> $false ) ) ).
fof(ssSkP840,fi_predicates,
! [X1] :
( ssSkP840(X1)
<=> $true ) ).
fof(ssSkP841,fi_predicates,
! [X1] :
( ssSkP841(X1)
<=> $true ) ).
fof(ssSkP842,fi_predicates,
! [X1] :
( ssSkP842(X1)
<=> $true ) ).
fof(ssSkP843,fi_predicates,
! [X1] :
( ssSkP843(X1)
<=> $true ) ).
fof(ssSkP844,fi_predicates,
! [X1] :
( ssSkP844(X1)
<=> $true ) ).
fof(ssSkP845,fi_predicates,
! [X1] :
( ssSkP845(X1)
<=> $true ) ).
fof(ssSkP846,fi_predicates,
! [X1] :
( ssSkP846(X1)
<=> $true ) ).
fof(ssSkP847,fi_predicates,
! [X1] :
( ssSkP847(X1)
<=> $true ) ).
fof(ssSkP848,fi_predicates,
! [X1] :
( ssSkP848(X1)
<=> $true ) ).
fof(ssSkP849,fi_predicates,
! [X1] :
( ssSkP849(X1)
<=> $true ) ).
fof(ssSkP85,fi_predicates,
( ( ssSkP85("1")
<=> $false )
& ( ssSkP85("2")
<=> $false )
& ( ssSkP85("3")
<=> $false ) ) ).
fof(ssSkP850,fi_predicates,
! [X1] :
( ssSkP850(X1)
<=> $true ) ).
fof(ssSkP851,fi_predicates,
! [X1] :
( ssSkP851(X1)
<=> $true ) ).
fof(ssSkP852,fi_predicates,
! [X1] :
( ssSkP852(X1)
<=> $true ) ).
fof(ssSkP853,fi_predicates,
! [X1,X2] :
( ssSkP853(X1,X2)
<=> $true ) ).
fof(ssSkP854,fi_predicates,
! [X1,X2] :
( ssSkP854(X1,X2)
<=> $true ) ).
fof(ssSkP855,fi_predicates,
! [X1] :
( ssSkP855(X1)
<=> $true ) ).
fof(ssSkP856,fi_predicates,
! [X1] :
( ssSkP856(X1)
<=> $true ) ).
fof(ssSkP857,fi_predicates,
! [X1] :
( ssSkP857(X1)
<=> $true ) ).
fof(ssSkP858,fi_predicates,
! [X1] :
( ssSkP858(X1)
<=> $true ) ).
fof(ssSkP859,fi_predicates,
! [X1] :
( ssSkP859(X1)
<=> $true ) ).
fof(ssSkP86,fi_predicates,
( ( ssSkP86("1")
<=> $false )
& ( ssSkP86("2")
<=> $false )
& ( ssSkP86("3")
<=> $true ) ) ).
fof(ssSkP860,fi_predicates,
! [X1] :
( ssSkP860(X1)
<=> $true ) ).
fof(ssSkP861,fi_predicates,
! [X1] :
( ssSkP861(X1)
<=> $true ) ).
fof(ssSkP862,fi_predicates,
! [X1] :
( ssSkP862(X1)
<=> $true ) ).
fof(ssSkP863,fi_predicates,
! [X1] :
( ssSkP863(X1)
<=> $true ) ).
fof(ssSkP864,fi_predicates,
! [X1] :
( ssSkP864(X1)
<=> $true ) ).
fof(ssSkP865,fi_predicates,
! [X1] :
( ssSkP865(X1)
<=> $true ) ).
fof(ssSkP866,fi_predicates,
! [X1] :
( ssSkP866(X1)
<=> $true ) ).
fof(ssSkP867,fi_predicates,
! [X1] :
( ssSkP867(X1)
<=> $true ) ).
fof(ssSkP868,fi_predicates,
! [X1] :
( ssSkP868(X1)
<=> $true ) ).
fof(ssSkP869,fi_predicates,
! [X1] :
( ssSkP869(X1)
<=> $true ) ).
fof(ssSkP87,fi_predicates,
( ( ssSkP87("1")
<=> $false )
& ( ssSkP87("2")
<=> $false )
& ( ssSkP87("3")
<=> $false ) ) ).
fof(ssSkP870,fi_predicates,
! [X1] :
( ssSkP870(X1)
<=> $true ) ).
fof(ssSkP871,fi_predicates,
! [X1] :
( ssSkP871(X1)
<=> $true ) ).
fof(ssSkP872,fi_predicates,
! [X1] :
( ssSkP872(X1)
<=> $true ) ).
fof(ssSkP873,fi_predicates,
! [X1] :
( ssSkP873(X1)
<=> $true ) ).
fof(ssSkP874,fi_predicates,
! [X1] :
( ssSkP874(X1)
<=> $true ) ).
fof(ssSkP875,fi_predicates,
! [X1] :
( ssSkP875(X1)
<=> $true ) ).
fof(ssSkP876,fi_predicates,
! [X1] :
( ssSkP876(X1)
<=> $true ) ).
fof(ssSkP877,fi_predicates,
! [X1] :
( ssSkP877(X1)
<=> $true ) ).
fof(ssSkP878,fi_predicates,
! [X1] :
( ssSkP878(X1)
<=> $true ) ).
fof(ssSkP879,fi_predicates,
! [X1] :
( ssSkP879(X1)
<=> $true ) ).
fof(ssSkP88,fi_predicates,
( ( ssSkP88("1")
<=> $false )
& ( ssSkP88("2")
<=> $false )
& ( ssSkP88("3")
<=> $false ) ) ).
fof(ssSkP880,fi_predicates,
! [X1] :
( ssSkP880(X1)
<=> $true ) ).
fof(ssSkP881,fi_predicates,
! [X1] :
( ssSkP881(X1)
<=> $true ) ).
fof(ssSkP882,fi_predicates,
! [X1] :
( ssSkP882(X1)
<=> $true ) ).
fof(ssSkP883,fi_predicates,
! [X1] :
( ssSkP883(X1)
<=> $true ) ).
fof(ssSkP884,fi_predicates,
! [X1] :
( ssSkP884(X1)
<=> $true ) ).
fof(ssSkP885,fi_predicates,
( ( ssSkP885("1","1")
<=> $true )
& ( ssSkP885("1","2")
<=> $true )
& ( ssSkP885("1","3")
<=> $true )
& ( ssSkP885("2","1")
<=> $false )
& ( ssSkP885("2","2")
<=> $true )
& ( ssSkP885("2","3")
<=> $true )
& ( ssSkP885("3","1")
<=> $false )
& ( ssSkP885("3","2")
<=> $true )
& ( ssSkP885("3","3")
<=> $true ) ) ).
fof(ssSkP886,fi_predicates,
( ( ssSkP886("1","1")
<=> $true )
& ( ssSkP886("1","2")
<=> $true )
& ( ssSkP886("1","3")
<=> $true )
& ( ssSkP886("2","1")
<=> $false )
& ( ssSkP886("2","2")
<=> $true )
& ( ssSkP886("2","3")
<=> $true )
& ( ssSkP886("3","1")
<=> $false )
& ( ssSkP886("3","2")
<=> $true )
& ( ssSkP886("3","3")
<=> $true ) ) ).
fof(ssSkP887,fi_predicates,
( ( ssSkP887("1")
<=> $false )
& ( ssSkP887("2")
<=> $false )
& ( ssSkP887("3")
<=> $false ) ) ).
fof(ssSkP888,fi_predicates,
( ( ssSkP888("1")
<=> $false )
& ( ssSkP888("2")
<=> $false )
& ( ssSkP888("3")
<=> $false ) ) ).
fof(ssSkP889,fi_predicates,
( ( ssSkP889("1")
<=> $false )
& ( ssSkP889("2")
<=> $false )
& ( ssSkP889("3")
<=> $false ) ) ).
fof(ssSkP89,fi_predicates,
( ( ssSkP89("1")
<=> $false )
& ( ssSkP89("2")
<=> $false )
& ( ssSkP89("3")
<=> $false ) ) ).
fof(ssSkP890,fi_predicates,
( ( ssSkP890("1")
<=> $false )
& ( ssSkP890("2")
<=> $false )
& ( ssSkP890("3")
<=> $false ) ) ).
fof(ssSkP891,fi_predicates,
( ( ssSkP891("1")
<=> $false )
& ( ssSkP891("2")
<=> $false )
& ( ssSkP891("3")
<=> $false ) ) ).
fof(ssSkP892,fi_predicates,
( ( ssSkP892("1")
<=> $false )
& ( ssSkP892("2")
<=> $false )
& ( ssSkP892("3")
<=> $false ) ) ).
fof(ssSkP893,fi_predicates,
( ( ssSkP893("1")
<=> $false )
& ( ssSkP893("2")
<=> $false )
& ( ssSkP893("3")
<=> $false ) ) ).
fof(ssSkP894,fi_predicates,
( ( ssSkP894("1")
<=> $false )
& ( ssSkP894("2")
<=> $false )
& ( ssSkP894("3")
<=> $false ) ) ).
fof(ssSkP895,fi_predicates,
( ( ssSkP895("1")
<=> $false )
& ( ssSkP895("2")
<=> $false )
& ( ssSkP895("3")
<=> $false ) ) ).
fof(ssSkP896,fi_predicates,
( ( ssSkP896("1")
<=> $false )
& ( ssSkP896("2")
<=> $false )
& ( ssSkP896("3")
<=> $false ) ) ).
fof(ssSkP897,fi_predicates,
( ( ssSkP897("1")
<=> $false )
& ( ssSkP897("2")
<=> $false )
& ( ssSkP897("3")
<=> $false ) ) ).
fof(ssSkP898,fi_predicates,
( ( ssSkP898("1")
<=> $false )
& ( ssSkP898("2")
<=> $false )
& ( ssSkP898("3")
<=> $false ) ) ).
fof(ssSkP899,fi_predicates,
( ( ssSkP899("1")
<=> $false )
& ( ssSkP899("2")
<=> $false )
& ( ssSkP899("3")
<=> $false ) ) ).
fof(ssSkP9,fi_predicates,
( ( ssSkP9("1")
<=> $true )
& ( ssSkP9("2")
<=> $false )
& ( ssSkP9("3")
<=> $false ) ) ).
fof(ssSkP90,fi_predicates,
( ( ssSkP90("1")
<=> $false )
& ( ssSkP90("2")
<=> $false )
& ( ssSkP90("3")
<=> $false ) ) ).
fof(ssSkP900,fi_predicates,
( ( ssSkP900("1")
<=> $false )
& ( ssSkP900("2")
<=> $false )
& ( ssSkP900("3")
<=> $false ) ) ).
fof(ssSkP901,fi_predicates,
( ( ssSkP901("1")
<=> $false )
& ( ssSkP901("2")
<=> $false )
& ( ssSkP901("3")
<=> $false ) ) ).
fof(ssSkP902,fi_predicates,
( ( ssSkP902("1")
<=> $false )
& ( ssSkP902("2")
<=> $false )
& ( ssSkP902("3")
<=> $false ) ) ).
fof(ssSkP903,fi_predicates,
( ( ssSkP903("1")
<=> $false )
& ( ssSkP903("2")
<=> $false )
& ( ssSkP903("3")
<=> $false ) ) ).
fof(ssSkP904,fi_predicates,
( ( ssSkP904("1")
<=> $true )
& ( ssSkP904("2")
<=> $false )
& ( ssSkP904("3")
<=> $false ) ) ).
fof(ssSkP905,fi_predicates,
( ( ssSkP905("1")
<=> $true )
& ( ssSkP905("2")
<=> $false )
& ( ssSkP905("3")
<=> $false ) ) ).
fof(ssSkP906,fi_predicates,
( ( ssSkP906("1")
<=> $true )
& ( ssSkP906("2")
<=> $false )
& ( ssSkP906("3")
<=> $false ) ) ).
fof(ssSkP907,fi_predicates,
( ( ssSkP907("1")
<=> $true )
& ( ssSkP907("2")
<=> $false )
& ( ssSkP907("3")
<=> $false ) ) ).
fof(ssSkP908,fi_predicates,
( ( ssSkP908("1")
<=> $true )
& ( ssSkP908("2")
<=> $false )
& ( ssSkP908("3")
<=> $false ) ) ).
fof(ssSkP909,fi_predicates,
( ( ssSkP909("1")
<=> $true )
& ( ssSkP909("2")
<=> $false )
& ( ssSkP909("3")
<=> $false ) ) ).
fof(ssSkP91,fi_predicates,
( ( ssSkP91("1")
<=> $false )
& ( ssSkP91("2")
<=> $false )
& ( ssSkP91("3")
<=> $false ) ) ).
fof(ssSkP910,fi_predicates,
( ( ssSkP910("1")
<=> $true )
& ( ssSkP910("2")
<=> $false )
& ( ssSkP910("3")
<=> $false ) ) ).
fof(ssSkP911,fi_predicates,
( ( ssSkP911("1")
<=> $true )
& ( ssSkP911("2")
<=> $false )
& ( ssSkP911("3")
<=> $false ) ) ).
fof(ssSkP912,fi_predicates,
( ( ssSkP912("1")
<=> $true )
& ( ssSkP912("2")
<=> $false )
& ( ssSkP912("3")
<=> $false ) ) ).
fof(ssSkP913,fi_predicates,
( ( ssSkP913("1")
<=> $true )
& ( ssSkP913("2")
<=> $false )
& ( ssSkP913("3")
<=> $false ) ) ).
fof(ssSkP914,fi_predicates,
! [X1,X2] :
( ssSkP914(X1,X2)
<=> $true ) ).
fof(ssSkP915,fi_predicates,
! [X1,X2] :
( ssSkP915(X1,X2)
<=> $true ) ).
fof(ssSkP916,fi_predicates,
! [X1] :
( ssSkP916(X1)
<=> $false ) ).
fof(ssSkP917,fi_predicates,
! [X1] :
( ssSkP917(X1)
<=> $false ) ).
fof(ssSkP918,fi_predicates,
! [X1] :
( ssSkP918(X1)
<=> $false ) ).
fof(ssSkP919,fi_predicates,
! [X1] :
( ssSkP919(X1)
<=> $false ) ).
fof(ssSkP92,fi_predicates,
( ( ssSkP92("1")
<=> $false )
& ( ssSkP92("2")
<=> $false )
& ( ssSkP92("3")
<=> $false ) ) ).
fof(ssSkP920,fi_predicates,
! [X1] :
( ssSkP920(X1)
<=> $false ) ).
fof(ssSkP921,fi_predicates,
! [X1] :
( ssSkP921(X1)
<=> $false ) ).
fof(ssSkP922,fi_predicates,
! [X1] :
( ssSkP922(X1)
<=> $false ) ).
fof(ssSkP923,fi_predicates,
! [X1] :
( ssSkP923(X1)
<=> $false ) ).
fof(ssSkP924,fi_predicates,
! [X1] :
( ssSkP924(X1)
<=> $false ) ).
fof(ssSkP925,fi_predicates,
! [X1] :
( ssSkP925(X1)
<=> $false ) ).
fof(ssSkP926,fi_predicates,
! [X1] :
( ssSkP926(X1)
<=> $false ) ).
fof(ssSkP927,fi_predicates,
! [X1] :
( ssSkP927(X1)
<=> $false ) ).
fof(ssSkP928,fi_predicates,
! [X1] :
( ssSkP928(X1)
<=> $false ) ).
fof(ssSkP929,fi_predicates,
! [X1] :
( ssSkP929(X1)
<=> $false ) ).
fof(ssSkP93,fi_predicates,
( ( ssSkP93("1")
<=> $false )
& ( ssSkP93("2")
<=> $false )
& ( ssSkP93("3")
<=> $false ) ) ).
fof(ssSkP930,fi_predicates,
! [X1] :
( ssSkP930(X1)
<=> $false ) ).
fof(ssSkP931,fi_predicates,
! [X1] :
( ssSkP931(X1)
<=> $false ) ).
fof(ssSkP932,fi_predicates,
! [X1] :
( ssSkP932(X1)
<=> $false ) ).
fof(ssSkP933,fi_predicates,
! [X1] :
( ssSkP933(X1)
<=> $true ) ).
fof(ssSkP934,fi_predicates,
! [X1] :
( ssSkP934(X1)
<=> $true ) ).
fof(ssSkP935,fi_predicates,
! [X1] :
( ssSkP935(X1)
<=> $true ) ).
fof(ssSkP936,fi_predicates,
! [X1] :
( ssSkP936(X1)
<=> $true ) ).
fof(ssSkP937,fi_predicates,
! [X1] :
( ssSkP937(X1)
<=> $true ) ).
fof(ssSkP938,fi_predicates,
! [X1] :
( ssSkP938(X1)
<=> $true ) ).
fof(ssSkP939,fi_predicates,
! [X1] :
( ssSkP939(X1)
<=> $true ) ).
fof(ssSkP94,fi_predicates,
( ( ssSkP94("1")
<=> $false )
& ( ssSkP94("2")
<=> $false )
& ( ssSkP94("3")
<=> $false ) ) ).
fof(ssSkP940,fi_predicates,
! [X1] :
( ssSkP940(X1)
<=> $true ) ).
fof(ssSkP941,fi_predicates,
! [X1] :
( ssSkP941(X1)
<=> $true ) ).
fof(ssSkP942,fi_predicates,
! [X1] :
( ssSkP942(X1)
<=> $true ) ).
fof(ssSkP943,fi_predicates,
! [X1] :
( ssSkP943(X1)
<=> $true ) ).
fof(ssSkP944,fi_predicates,
! [X1] :
( ssSkP944(X1)
<=> $true ) ).
fof(ssSkP945,fi_predicates,
! [X1] :
( ssSkP945(X1)
<=> $true ) ).
fof(ssSkP946,fi_predicates,
( ( ssSkP946("1","1")
<=> $true )
& ( ssSkP946("1","2")
<=> $true )
& ( ssSkP946("1","3")
<=> $true )
& ( ssSkP946("2","1")
<=> $true )
& ( ssSkP946("2","2")
<=> $true )
& ( ssSkP946("2","3")
<=> $true )
& ( ssSkP946("3","1")
<=> $true )
& ( ssSkP946("3","2")
<=> $true )
& ( ssSkP946("3","3")
<=> $true ) ) ).
fof(ssSkP947,fi_predicates,
( ( ssSkP947("1","1")
<=> $true )
& ( ssSkP947("1","2")
<=> $true )
& ( ssSkP947("1","3")
<=> $true )
& ( ssSkP947("2","1")
<=> $true )
& ( ssSkP947("2","2")
<=> $true )
& ( ssSkP947("2","3")
<=> $true )
& ( ssSkP947("3","1")
<=> $true )
& ( ssSkP947("3","2")
<=> $true )
& ( ssSkP947("3","3")
<=> $true ) ) ).
fof(ssSkP948,fi_predicates,
( ( ssSkP948("1")
<=> $false )
& ( ssSkP948("2")
<=> $false )
& ( ssSkP948("3")
<=> $false ) ) ).
fof(ssSkP949,fi_predicates,
( ( ssSkP949("1")
<=> $true )
& ( ssSkP949("2")
<=> $true )
& ( ssSkP949("3")
<=> $true ) ) ).
fof(ssSkP95,fi_predicates,
( ( ssSkP95("1")
<=> $false )
& ( ssSkP95("2")
<=> $false )
& ( ssSkP95("3")
<=> $false ) ) ).
fof(ssSkP950,fi_predicates,
( ( ssSkP950("1")
<=> $true )
& ( ssSkP950("2")
<=> $true )
& ( ssSkP950("3")
<=> $true ) ) ).
fof(ssSkP951,fi_predicates,
( ( ssSkP951("1")
<=> $true )
& ( ssSkP951("2")
<=> $true )
& ( ssSkP951("3")
<=> $true ) ) ).
fof(ssSkP952,fi_predicates,
( ( ssSkP952("1")
<=> $true )
& ( ssSkP952("2")
<=> $true )
& ( ssSkP952("3")
<=> $true ) ) ).
fof(ssSkP953,fi_predicates,
( ( ssSkP953("1")
<=> $true )
& ( ssSkP953("2")
<=> $true )
& ( ssSkP953("3")
<=> $true ) ) ).
fof(ssSkP954,fi_predicates,
( ( ssSkP954("1")
<=> $true )
& ( ssSkP954("2")
<=> $true )
& ( ssSkP954("3")
<=> $false ) ) ).
fof(ssSkP955,fi_predicates,
( ( ssSkP955("1")
<=> $true )
& ( ssSkP955("2")
<=> $true )
& ( ssSkP955("3")
<=> $true ) ) ).
fof(ssSkP956,fi_predicates,
( ( ssSkP956("1")
<=> $true )
& ( ssSkP956("2")
<=> $true )
& ( ssSkP956("3")
<=> $true ) ) ).
fof(ssSkP957,fi_predicates,
( ( ssSkP957("1")
<=> $true )
& ( ssSkP957("2")
<=> $true )
& ( ssSkP957("3")
<=> $true ) ) ).
fof(ssSkP958,fi_predicates,
( ( ssSkP958("1")
<=> $true )
& ( ssSkP958("2")
<=> $true )
& ( ssSkP958("3")
<=> $true ) ) ).
fof(ssSkP959,fi_predicates,
( ( ssSkP959("1")
<=> $true )
& ( ssSkP959("2")
<=> $true )
& ( ssSkP959("3")
<=> $true ) ) ).
fof(ssSkP96,fi_predicates,
( ( ssSkP96("1")
<=> $false )
& ( ssSkP96("2")
<=> $false )
& ( ssSkP96("3")
<=> $false ) ) ).
fof(ssSkP960,fi_predicates,
( ( ssSkP960("1")
<=> $true )
& ( ssSkP960("2")
<=> $true )
& ( ssSkP960("3")
<=> $true ) ) ).
fof(ssSkP961,fi_predicates,
( ( ssSkP961("1")
<=> $true )
& ( ssSkP961("2")
<=> $true )
& ( ssSkP961("3")
<=> $true ) ) ).
fof(ssSkP962,fi_predicates,
( ( ssSkP962("1")
<=> $true )
& ( ssSkP962("2")
<=> $true )
& ( ssSkP962("3")
<=> $true ) ) ).
fof(ssSkP963,fi_predicates,
( ( ssSkP963("1")
<=> $true )
& ( ssSkP963("2")
<=> $true )
& ( ssSkP963("3")
<=> $true ) ) ).
fof(ssSkP964,fi_predicates,
( ( ssSkP964("1")
<=> $true )
& ( ssSkP964("2")
<=> $true )
& ( ssSkP964("3")
<=> $true ) ) ).
fof(ssSkP965,fi_predicates,
( ( ssSkP965("1")
<=> $true )
& ( ssSkP965("2")
<=> $true )
& ( ssSkP965("3")
<=> $true ) ) ).
fof(ssSkP966,fi_predicates,
( ( ssSkP966("1")
<=> $true )
& ( ssSkP966("2")
<=> $true )
& ( ssSkP966("3")
<=> $true ) ) ).
fof(ssSkP967,fi_predicates,
( ( ssSkP967("1")
<=> $true )
& ( ssSkP967("2")
<=> $true )
& ( ssSkP967("3")
<=> $true ) ) ).
fof(ssSkP968,fi_predicates,
( ( ssSkP968("1")
<=> $true )
& ( ssSkP968("2")
<=> $false )
& ( ssSkP968("3")
<=> $false ) ) ).
fof(ssSkP969,fi_predicates,
( ( ssSkP969("1","1")
<=> $true )
& ( ssSkP969("1","2")
<=> $true )
& ( ssSkP969("1","3")
<=> $true )
& ( ssSkP969("2","1")
<=> $true )
& ( ssSkP969("2","2")
<=> $true )
& ( ssSkP969("2","3")
<=> $true )
& ( ssSkP969("3","1")
<=> $true )
& ( ssSkP969("3","2")
<=> $true )
& ( ssSkP969("3","3")
<=> $true ) ) ).
fof(ssSkP97,fi_predicates,
( ( ssSkP97("1")
<=> $false )
& ( ssSkP97("2")
<=> $false )
& ( ssSkP97("3")
<=> $false ) ) ).
fof(ssSkP970,fi_predicates,
( ( ssSkP970("1","1")
<=> $true )
& ( ssSkP970("1","2")
<=> $true )
& ( ssSkP970("1","3")
<=> $true )
& ( ssSkP970("2","1")
<=> $true )
& ( ssSkP970("2","2")
<=> $true )
& ( ssSkP970("2","3")
<=> $true )
& ( ssSkP970("3","1")
<=> $true )
& ( ssSkP970("3","2")
<=> $true )
& ( ssSkP970("3","3")
<=> $true ) ) ).
fof(ssSkP971,fi_predicates,
( ( ssSkP971("1")
<=> $true )
& ( ssSkP971("2")
<=> $false )
& ( ssSkP971("3")
<=> $false ) ) ).
fof(ssSkP972,fi_predicates,
( ( ssSkP972("1")
<=> $true )
& ( ssSkP972("2")
<=> $true )
& ( ssSkP972("3")
<=> $true ) ) ).
fof(ssSkP973,fi_predicates,
( ( ssSkP973("1")
<=> $true )
& ( ssSkP973("2")
<=> $true )
& ( ssSkP973("3")
<=> $true ) ) ).
fof(ssSkP974,fi_predicates,
( ( ssSkP974("1")
<=> $true )
& ( ssSkP974("2")
<=> $true )
& ( ssSkP974("3")
<=> $true ) ) ).
fof(ssSkP975,fi_predicates,
( ( ssSkP975("1")
<=> $true )
& ( ssSkP975("2")
<=> $true )
& ( ssSkP975("3")
<=> $true ) ) ).
fof(ssSkP976,fi_predicates,
( ( ssSkP976("1")
<=> $true )
& ( ssSkP976("2")
<=> $true )
& ( ssSkP976("3")
<=> $true ) ) ).
fof(ssSkP977,fi_predicates,
( ( ssSkP977("1")
<=> $true )
& ( ssSkP977("2")
<=> $true )
& ( ssSkP977("3")
<=> $true ) ) ).
fof(ssSkP978,fi_predicates,
( ( ssSkP978("1")
<=> $true )
& ( ssSkP978("2")
<=> $true )
& ( ssSkP978("3")
<=> $true ) ) ).
fof(ssSkP979,fi_predicates,
( ( ssSkP979("1")
<=> $true )
& ( ssSkP979("2")
<=> $true )
& ( ssSkP979("3")
<=> $true ) ) ).
fof(ssSkP98,fi_predicates,
( ( ssSkP98("1")
<=> $false )
& ( ssSkP98("2")
<=> $false )
& ( ssSkP98("3")
<=> $false ) ) ).
fof(ssSkP980,fi_predicates,
( ( ssSkP980("1")
<=> $true )
& ( ssSkP980("2")
<=> $true )
& ( ssSkP980("3")
<=> $false ) ) ).
fof(ssSkP981,fi_predicates,
( ( ssSkP981("1")
<=> $true )
& ( ssSkP981("2")
<=> $true )
& ( ssSkP981("3")
<=> $true ) ) ).
fof(ssSkP982,fi_predicates,
( ( ssSkP982("1")
<=> $true )
& ( ssSkP982("2")
<=> $true )
& ( ssSkP982("3")
<=> $true ) ) ).
fof(ssSkP983,fi_predicates,
( ( ssSkP983("1")
<=> $true )
& ( ssSkP983("2")
<=> $true )
& ( ssSkP983("3")
<=> $true ) ) ).
fof(ssSkP984,fi_predicates,
( ( ssSkP984("1")
<=> $true )
& ( ssSkP984("2")
<=> $true )
& ( ssSkP984("3")
<=> $true ) ) ).
fof(ssSkP985,fi_predicates,
( ( ssSkP985("1")
<=> $true )
& ( ssSkP985("2")
<=> $true )
& ( ssSkP985("3")
<=> $true ) ) ).
fof(ssSkP986,fi_predicates,
( ( ssSkP986("1")
<=> $true )
& ( ssSkP986("2")
<=> $true )
& ( ssSkP986("3")
<=> $true ) ) ).
fof(ssSkP987,fi_predicates,
( ( ssSkP987("1")
<=> $true )
& ( ssSkP987("2")
<=> $true )
& ( ssSkP987("3")
<=> $true ) ) ).
fof(ssSkP988,fi_predicates,
( ( ssSkP988("1")
<=> $true )
& ( ssSkP988("2")
<=> $true )
& ( ssSkP988("3")
<=> $true ) ) ).
fof(ssSkP989,fi_predicates,
( ( ssSkP989("1")
<=> $true )
& ( ssSkP989("2")
<=> $true )
& ( ssSkP989("3")
<=> $true ) ) ).
fof(ssSkP99,fi_predicates,
( ( ssSkP99("1")
<=> $false )
& ( ssSkP99("2")
<=> $false )
& ( ssSkP99("3")
<=> $false ) ) ).
fof(ssSkP990,fi_predicates,
( ( ssSkP990("1")
<=> $true )
& ( ssSkP990("2")
<=> $true )
& ( ssSkP990("3")
<=> $true ) ) ).
fof(ssSkP991,fi_predicates,
( ( ssSkP991("1")
<=> $true )
& ( ssSkP991("2")
<=> $true )
& ( ssSkP991("3")
<=> $true ) ) ).
fof(ssSkP992,fi_predicates,
( ( ssSkP992("1")
<=> $true )
& ( ssSkP992("2")
<=> $true )
& ( ssSkP992("3")
<=> $true ) ) ).
fof(ssSkP993,fi_predicates,
( ( ssSkP993("1")
<=> $true )
& ( ssSkP993("2")
<=> $true )
& ( ssSkP993("3")
<=> $true ) ) ).
fof(ssSkP994,fi_predicates,
( ( ssSkP994("1")
<=> $true )
& ( ssSkP994("2")
<=> $false )
& ( ssSkP994("3")
<=> $false ) ) ).
fof(ssSkP995,fi_predicates,
( ( ssSkP995("1","1")
<=> $true )
& ( ssSkP995("1","2")
<=> $true )
& ( ssSkP995("1","3")
<=> $true )
& ( ssSkP995("2","1")
<=> $false )
& ( ssSkP995("2","2")
<=> $true )
& ( ssSkP995("2","3")
<=> $true )
& ( ssSkP995("3","1")
<=> $false )
& ( ssSkP995("3","2")
<=> $true )
& ( ssSkP995("3","3")
<=> $true ) ) ).
fof(ssSkP996,fi_predicates,
( ( ssSkP996("1","1")
<=> $true )
& ( ssSkP996("1","2")
<=> $true )
& ( ssSkP996("1","3")
<=> $true )
& ( ssSkP996("2","1")
<=> $false )
& ( ssSkP996("2","2")
<=> $true )
& ( ssSkP996("2","3")
<=> $true )
& ( ssSkP996("3","1")
<=> $false )
& ( ssSkP996("3","2")
<=> $true )
& ( ssSkP996("3","3")
<=> $true ) ) ).
fof(ssSkP997,fi_predicates,
( ( ssSkP997("1")
<=> $false )
& ( ssSkP997("2")
<=> $false )
& ( ssSkP997("3")
<=> $false ) ) ).
fof(ssSkP998,fi_predicates,
( ( ssSkP998("1")
<=> $false )
& ( ssSkP998("2")
<=> $false )
& ( ssSkP998("3")
<=> $false ) ) ).
fof(ssSkP999,fi_predicates,
( ( ssSkP999("1")
<=> $false )
& ( ssSkP999("2")
<=> $false )
& ( ssSkP999("3")
<=> $false ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN911-1 : TPTP v8.1.0. Released v2.5.0.
% 0.07/0.13 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jul 11 15:38:53 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 Paradox, version 4.0, 2010-06-29.
% 0.13/0.34 +++ PROBLEM: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 Reading '/export/starexec/sandbox2/benchmark/theBenchmark.p' ... OK
% 0.38/0.60 +++ SOLVING: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.30/1.48 +++ BEGIN MODEL
% 1.30/1.48 SZS output start FiniteModel for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 1.30/1.51 +++ END MODEL
% 1.30/1.51 +++ RESULT: Satisfiable
% 1.30/1.51 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------