%------------------------------------------------------------------------------
% File : Paradox---4.0
% Problem : SYN912-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:short
% Command : paradox --no-progress --time %d --tstp --model %s
% Computer : n013.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:47 EDT 2022
% Result : Satisfiable 1.72s 1.91s
% Output : FiniteModel 1.72s
% Verified :
% SZS Type : FiniteModel
% Domain size : 2
% Comments :
%------------------------------------------------------------------------------
% domain size is 2
fof(domain,fi_domain,
! [X] :
( X = "1"
| X = "2" ) ).
fof(skc81,fi_functors,
skc81 = "1" ).
fof(skf100,fi_functors,
( skf100("1") = "1"
& skf100("2") = "1" ) ).
fof(skf101,fi_functors,
( skf101("1") = "1"
& skf101("2") = "1" ) ).
fof(skf102,fi_functors,
( skf102("1") = "1"
& skf102("2") = "1" ) ).
fof(skf103,fi_functors,
( skf103("1") = "2"
& skf103("2") = "2" ) ).
fof(skf104,fi_functors,
( skf104("1") = "1"
& skf104("2") = "1" ) ).
fof(skf105,fi_functors,
( skf105("1") = "1"
& skf105("2") = "1" ) ).
fof(skf106,fi_functors,
( skf106("1") = "1"
& skf106("2") = "1" ) ).
fof(skf107,fi_functors,
( skf107("1") = "1"
& skf107("2") = "1" ) ).
fof(skf108,fi_functors,
( skf108("1") = "1"
& skf108("2") = "1" ) ).
fof(skf109,fi_functors,
( skf109("1") = "1"
& skf109("2") = "1" ) ).
fof(skf110,fi_functors,
( skf110("1") = "1"
& skf110("2") = "1" ) ).
fof(skf111,fi_functors,
( skf111("1") = "1"
& skf111("2") = "1" ) ).
fof(skf112,fi_functors,
( skf112("1") = "2"
& skf112("2") = "2" ) ).
fof(skf113,fi_functors,
( skf113("1") = "1"
& skf113("2") = "1" ) ).
fof(skf114,fi_functors,
( skf114("1") = "2"
& skf114("2") = "2" ) ).
fof(skf115,fi_functors,
( skf115("1") = "2"
& skf115("2") = "2" ) ).
fof(skf116,fi_functors,
( skf116("1") = "1"
& skf116("2") = "1" ) ).
fof(skf117,fi_functors,
( skf117("1") = "2"
& skf117("2") = "2" ) ).
fof(skf118,fi_functors,
( skf118("1") = "2"
& skf118("2") = "2" ) ).
fof(skf119,fi_functors,
( skf119("1") = "1"
& skf119("2") = "1" ) ).
fof(skf120,fi_functors,
( skf120("1") = "1"
& skf120("2") = "1" ) ).
fof(skf121,fi_functors,
( skf121("1") = "1"
& skf121("2") = "1" ) ).
fof(skf122,fi_functors,
( skf122("1") = "1"
& skf122("2") = "1" ) ).
fof(skf123,fi_functors,
( skf123("1") = "1"
& skf123("2") = "1" ) ).
fof(skf124,fi_functors,
( skf124("1") = "1"
& skf124("2") = "1" ) ).
fof(skf125,fi_functors,
( skf125("1") = "1"
& skf125("2") = "1" ) ).
fof(skf126,fi_functors,
( skf126("1") = "1"
& skf126("2") = "1" ) ).
fof(skf127,fi_functors,
( skf127("1") = "1"
& skf127("2") = "1" ) ).
fof(skf128,fi_functors,
( skf128("1") = "1"
& skf128("2") = "1" ) ).
fof(skf129,fi_functors,
( skf129("1") = "1"
& skf129("2") = "1" ) ).
fof(skf130,fi_functors,
( skf130("1") = "1"
& skf130("2") = "1" ) ).
fof(skf131,fi_functors,
( skf131("1") = "1"
& skf131("2") = "1" ) ).
fof(skf132,fi_functors,
( skf132("1") = "1"
& skf132("2") = "1" ) ).
fof(skf133,fi_functors,
( skf133("1") = "1"
& skf133("2") = "1" ) ).
fof(skf134,fi_functors,
( skf134("1") = "1"
& skf134("2") = "1" ) ).
fof(skf135,fi_functors,
( skf135("1") = "1"
& skf135("2") = "1" ) ).
fof(skf136,fi_functors,
( skf136("1") = "1"
& skf136("2") = "1" ) ).
fof(skf137,fi_functors,
( skf137("1") = "1"
& skf137("2") = "1" ) ).
fof(skf138,fi_functors,
( skf138("1") = "1"
& skf138("2") = "1" ) ).
fof(skf139,fi_functors,
( skf139("1") = "1"
& skf139("2") = "1" ) ).
fof(skf70,fi_functors,
( skf70("1") = "1"
& skf70("2") = "1" ) ).
fof(skf71,fi_functors,
( skf71("1") = "1"
& skf71("2") = "1" ) ).
fof(skf72,fi_functors,
( skf72("1") = "2"
& skf72("2") = "1" ) ).
fof(skf73,fi_functors,
( skf73("1") = "2"
& skf73("2") = "1" ) ).
fof(skf74,fi_functors,
( skf74("1") = "1"
& skf74("2") = "1" ) ).
fof(skf75,fi_functors,
( skf75("1") = "2"
& skf75("2") = "1" ) ).
fof(skf76,fi_functors,
( skf76("1") = "1"
& skf76("2") = "1" ) ).
fof(skf77,fi_functors,
( skf77("1") = "2"
& skf77("2") = "1" ) ).
fof(skf78,fi_functors,
( skf78("1") = "2"
& skf78("2") = "1" ) ).
fof(skf79,fi_functors,
( skf79("1") = "2"
& skf79("2") = "1" ) ).
fof(skf80,fi_functors,
( skf80("1") = "2"
& skf80("2") = "1" ) ).
fof(skf81,fi_functors,
( skf81("1") = "2"
& skf81("2") = "1" ) ).
fof(skf82,fi_functors,
( skf82("1") = "2"
& skf82("2") = "1" ) ).
fof(skf83,fi_functors,
( skf83("1") = "2"
& skf83("2") = "1" ) ).
fof(skf84,fi_functors,
( skf84("1") = "1"
& skf84("2") = "1" ) ).
fof(skf85,fi_functors,
( skf85("1") = "1"
& skf85("2") = "1" ) ).
fof(skf86,fi_functors,
( skf86("1") = "1"
& skf86("2") = "1" ) ).
fof(skf87,fi_functors,
( skf87("1") = "1"
& skf87("2") = "1" ) ).
fof(skf88,fi_functors,
( skf88("1") = "1"
& skf88("2") = "1" ) ).
fof(skf89,fi_functors,
( skf89("1") = "1"
& skf89("2") = "1" ) ).
fof(skf90,fi_functors,
( skf90("1") = "1"
& skf90("2") = "1" ) ).
fof(skf91,fi_functors,
( skf91("1") = "1"
& skf91("2") = "1" ) ).
fof(skf92,fi_functors,
( skf92("1") = "1"
& skf92("2") = "1" ) ).
fof(skf93,fi_functors,
( skf93("1") = "1"
& skf93("2") = "1" ) ).
fof(skf94,fi_functors,
( skf94("1") = "1"
& skf94("2") = "1" ) ).
fof(skf95,fi_functors,
( skf95("1") = "1"
& skf95("2") = "1" ) ).
fof(skf96,fi_functors,
( skf96("1") = "1"
& skf96("2") = "1" ) ).
fof(skf97,fi_functors,
( skf97("1") = "1"
& skf97("2") = "1" ) ).
fof(skf98,fi_functors,
( skf98("1") = "1"
& skf98("2") = "1" ) ).
fof(skf99,fi_functors,
( skf99("1") = "1"
& skf99("2") = "1" ) ).
fof(ssPv10,fi_predicates,
( ( ssPv10("1")
<=> $false )
& ( ssPv10("2")
<=> $true ) ) ).
fof(ssPv11,fi_predicates,
( ( ssPv11("1")
<=> $true )
& ( ssPv11("2")
<=> $false ) ) ).
fof(ssPv12,fi_predicates,
( ( ssPv12("1")
<=> $false )
& ( ssPv12("2")
<=> $true ) ) ).
fof(ssPv13,fi_predicates,
( ( ssPv13("1")
<=> $false )
& ( ssPv13("2")
<=> $true ) ) ).
fof(ssPv14,fi_predicates,
( ( ssPv14("1")
<=> $true )
& ( ssPv14("2")
<=> $false ) ) ).
fof(ssPv15,fi_predicates,
( ( ssPv15("1")
<=> $false )
& ( ssPv15("2")
<=> $true ) ) ).
fof(ssPv16,fi_predicates,
( ( ssPv16("1")
<=> $true )
& ( ssPv16("2")
<=> $false ) ) ).
fof(ssPv17,fi_predicates,
! [X1] :
( ssPv17(X1)
<=> $true ) ).
fof(ssPv18,fi_predicates,
! [X1] :
( ssPv18(X1)
<=> $false ) ).
fof(ssPv19,fi_predicates,
! [X1] :
( ssPv19(X1)
<=> $false ) ).
fof(ssPv2,fi_predicates,
! [X1] :
( ssPv2(X1)
<=> $false ) ).
fof(ssPv20,fi_predicates,
! [X1] :
( ssPv20(X1)
<=> $false ) ).
fof(ssPv21,fi_predicates,
! [X1] :
( ssPv21(X1)
<=> $true ) ).
fof(ssPv22,fi_predicates,
! [X1] :
( ssPv22(X1)
<=> $true ) ).
fof(ssPv23,fi_predicates,
! [X1] :
( ssPv23(X1)
<=> $false ) ).
fof(ssPv24,fi_predicates,
! [X1] :
( ssPv24(X1)
<=> $false ) ).
fof(ssPv25,fi_predicates,
( ( ssPv25("1")
<=> $true )
& ( ssPv25("2")
<=> $false ) ) ).
fof(ssPv26,fi_predicates,
( ( ssPv26("1")
<=> $true )
& ( ssPv26("2")
<=> $false ) ) ).
fof(ssPv27,fi_predicates,
( ( ssPv27("1")
<=> $true )
& ( ssPv27("2")
<=> $false ) ) ).
fof(ssPv28,fi_predicates,
( ( ssPv28("1")
<=> $true )
& ( ssPv28("2")
<=> $false ) ) ).
fof(ssPv29,fi_predicates,
( ( ssPv29("1")
<=> $true )
& ( ssPv29("2")
<=> $false ) ) ).
fof(ssPv3,fi_predicates,
! [X1] :
( ssPv3(X1)
<=> $false ) ).
fof(ssPv30,fi_predicates,
( ( ssPv30("1")
<=> $true )
& ( ssPv30("2")
<=> $false ) ) ).
fof(ssPv31,fi_predicates,
( ( ssPv31("1")
<=> $true )
& ( ssPv31("2")
<=> $false ) ) ).
fof(ssPv32,fi_predicates,
( ( ssPv32("1")
<=> $false )
& ( ssPv32("2")
<=> $true ) ) ).
fof(ssPv33,fi_predicates,
! [X1] :
( ssPv33(X1)
<=> $true ) ).
fof(ssPv34,fi_predicates,
! [X1] :
( ssPv34(X1)
<=> $false ) ).
fof(ssPv36,fi_predicates,
! [X1] :
( ssPv36(X1)
<=> $true ) ).
fof(ssPv37,fi_predicates,
! [X1] :
( ssPv37(X1)
<=> $false ) ).
fof(ssPv38,fi_predicates,
! [X1] :
( ssPv38(X1)
<=> $true ) ).
fof(ssPv39,fi_predicates,
! [X1] :
( ssPv39(X1)
<=> $true ) ).
fof(ssPv4,fi_predicates,
! [X1] :
( ssPv4(X1)
<=> $true ) ).
fof(ssPv40,fi_predicates,
! [X1] :
( ssPv40(X1)
<=> $false ) ).
fof(ssPv5,fi_predicates,
! [X1] :
( ssPv5(X1)
<=> $true ) ).
fof(ssPv6,fi_predicates,
! [X1] :
( ssPv6(X1)
<=> $true ) ).
fof(ssPv7,fi_predicates,
! [X1] :
( ssPv7(X1)
<=> $true ) ).
fof(ssPv8,fi_predicates,
! [X1] :
( ssPv8(X1)
<=> $false ) ).
fof(ssPv9,fi_predicates,
( ( ssPv9("1")
<=> $false )
& ( ssPv9("2")
<=> $true ) ) ).
fof(ssRr,fi_predicates,
( ( ssRr("1","1")
<=> $true )
& ( ssRr("1","2")
<=> $true )
& ( ssRr("2","1")
<=> $true )
& ( ssRr("2","2")
<=> $true ) ) ).
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,
! [X1,X2] :
( ssSkP0(X1,X2)
<=> $true ) ).
fof(ssSkP1,fi_predicates,
! [X1,X2] :
( ssSkP1(X1,X2)
<=> $true ) ).
fof(ssSkP10,fi_predicates,
! [X1] :
( ssSkP10(X1)
<=> $false ) ).
fof(ssSkP100,fi_predicates,
! [X1] :
( ssSkP100(X1)
<=> $false ) ).
fof(ssSkP1000,fi_predicates,
! [X1] :
( ssSkP1000(X1)
<=> $true ) ).
fof(ssSkP1001,fi_predicates,
! [X1] :
( ssSkP1001(X1)
<=> $true ) ).
fof(ssSkP1002,fi_predicates,
! [X1] :
( ssSkP1002(X1)
<=> $true ) ).
fof(ssSkP1003,fi_predicates,
! [X1] :
( ssSkP1003(X1)
<=> $true ) ).
fof(ssSkP1004,fi_predicates,
! [X1] :
( ssSkP1004(X1)
<=> $true ) ).
fof(ssSkP1005,fi_predicates,
! [X1] :
( ssSkP1005(X1)
<=> $true ) ).
fof(ssSkP1006,fi_predicates,
! [X1] :
( ssSkP1006(X1)
<=> $true ) ).
fof(ssSkP1007,fi_predicates,
! [X1] :
( ssSkP1007(X1)
<=> $true ) ).
fof(ssSkP1008,fi_predicates,
! [X1] :
( ssSkP1008(X1)
<=> $true ) ).
fof(ssSkP1009,fi_predicates,
! [X1] :
( ssSkP1009(X1)
<=> $true ) ).
fof(ssSkP101,fi_predicates,
! [X1] :
( ssSkP101(X1)
<=> $false ) ).
fof(ssSkP1010,fi_predicates,
! [X1] :
( ssSkP1010(X1)
<=> $true ) ).
fof(ssSkP1011,fi_predicates,
! [X1] :
( ssSkP1011(X1)
<=> $true ) ).
fof(ssSkP1012,fi_predicates,
! [X1] :
( ssSkP1012(X1)
<=> $true ) ).
fof(ssSkP1013,fi_predicates,
! [X1] :
( ssSkP1013(X1)
<=> $true ) ).
fof(ssSkP1014,fi_predicates,
! [X1] :
( ssSkP1014(X1)
<=> $true ) ).
fof(ssSkP1015,fi_predicates,
! [X1] :
( ssSkP1015(X1)
<=> $true ) ).
fof(ssSkP1016,fi_predicates,
! [X1,X2] :
( ssSkP1016(X1,X2)
<=> $true ) ).
fof(ssSkP1017,fi_predicates,
! [X1,X2] :
( ssSkP1017(X1,X2)
<=> $true ) ).
fof(ssSkP1018,fi_predicates,
! [X1] :
( ssSkP1018(X1)
<=> $false ) ).
fof(ssSkP1019,fi_predicates,
! [X1] :
( ssSkP1019(X1)
<=> $false ) ).
fof(ssSkP102,fi_predicates,
! [X1] :
( ssSkP102(X1)
<=> $false ) ).
fof(ssSkP1020,fi_predicates,
! [X1] :
( ssSkP1020(X1)
<=> $false ) ).
fof(ssSkP1021,fi_predicates,
! [X1] :
( ssSkP1021(X1)
<=> $true ) ).
fof(ssSkP1022,fi_predicates,
! [X1] :
( ssSkP1022(X1)
<=> $true ) ).
fof(ssSkP1023,fi_predicates,
! [X1] :
( ssSkP1023(X1)
<=> $true ) ).
fof(ssSkP1024,fi_predicates,
! [X1] :
( ssSkP1024(X1)
<=> $true ) ).
fof(ssSkP1025,fi_predicates,
! [X1] :
( ssSkP1025(X1)
<=> $true ) ).
fof(ssSkP1026,fi_predicates,
! [X1] :
( ssSkP1026(X1)
<=> $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,
! [X1] :
( ssSkP103(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP104(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP105(X1)
<=> $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,
! [X1] :
( ssSkP1057(X1)
<=> $true ) ).
fof(ssSkP1058,fi_predicates,
! [X1,X2] :
( ssSkP1058(X1,X2)
<=> $true ) ).
fof(ssSkP1059,fi_predicates,
! [X1,X2] :
( ssSkP1059(X1,X2)
<=> $true ) ).
fof(ssSkP106,fi_predicates,
! [X1] :
( ssSkP106(X1)
<=> $false ) ).
fof(ssSkP1060,fi_predicates,
! [X1] :
( ssSkP1060(X1)
<=> $false ) ).
fof(ssSkP1061,fi_predicates,
! [X1] :
( ssSkP1061(X1)
<=> $false ) ).
fof(ssSkP1062,fi_predicates,
! [X1] :
( ssSkP1062(X1)
<=> $false ) ).
fof(ssSkP1063,fi_predicates,
! [X1] :
( ssSkP1063(X1)
<=> $false ) ).
fof(ssSkP1064,fi_predicates,
! [X1] :
( ssSkP1064(X1)
<=> $false ) ).
fof(ssSkP1065,fi_predicates,
! [X1] :
( ssSkP1065(X1)
<=> $false ) ).
fof(ssSkP1066,fi_predicates,
! [X1] :
( ssSkP1066(X1)
<=> $false ) ).
fof(ssSkP1067,fi_predicates,
! [X1] :
( ssSkP1067(X1)
<=> $false ) ).
fof(ssSkP1068,fi_predicates,
! [X1] :
( ssSkP1068(X1)
<=> $false ) ).
fof(ssSkP1069,fi_predicates,
! [X1] :
( ssSkP1069(X1)
<=> $false ) ).
fof(ssSkP107,fi_predicates,
! [X1] :
( ssSkP107(X1)
<=> $false ) ).
fof(ssSkP1070,fi_predicates,
! [X1] :
( ssSkP1070(X1)
<=> $false ) ).
fof(ssSkP1071,fi_predicates,
! [X1] :
( ssSkP1071(X1)
<=> $false ) ).
fof(ssSkP1072,fi_predicates,
! [X1] :
( ssSkP1072(X1)
<=> $false ) ).
fof(ssSkP1073,fi_predicates,
! [X1] :
( ssSkP1073(X1)
<=> $false ) ).
fof(ssSkP1074,fi_predicates,
! [X1] :
( ssSkP1074(X1)
<=> $false ) ).
fof(ssSkP1075,fi_predicates,
! [X1] :
( ssSkP1075(X1)
<=> $true ) ).
fof(ssSkP1076,fi_predicates,
! [X1] :
( ssSkP1076(X1)
<=> $true ) ).
fof(ssSkP1077,fi_predicates,
! [X1] :
( ssSkP1077(X1)
<=> $true ) ).
fof(ssSkP1078,fi_predicates,
! [X1] :
( ssSkP1078(X1)
<=> $true ) ).
fof(ssSkP1079,fi_predicates,
! [X1] :
( ssSkP1079(X1)
<=> $true ) ).
fof(ssSkP108,fi_predicates,
! [X1] :
( ssSkP108(X1)
<=> $false ) ).
fof(ssSkP1080,fi_predicates,
! [X1] :
( ssSkP1080(X1)
<=> $true ) ).
fof(ssSkP1081,fi_predicates,
! [X1] :
( ssSkP1081(X1)
<=> $true ) ).
fof(ssSkP1082,fi_predicates,
! [X1] :
( ssSkP1082(X1)
<=> $true ) ).
fof(ssSkP1083,fi_predicates,
! [X1] :
( ssSkP1083(X1)
<=> $true ) ).
fof(ssSkP1084,fi_predicates,
! [X1] :
( ssSkP1084(X1)
<=> $true ) ).
fof(ssSkP1085,fi_predicates,
! [X1] :
( ssSkP1085(X1)
<=> $true ) ).
fof(ssSkP1086,fi_predicates,
! [X1] :
( ssSkP1086(X1)
<=> $true ) ).
fof(ssSkP1087,fi_predicates,
! [X1] :
( ssSkP1087(X1)
<=> $true ) ).
fof(ssSkP1088,fi_predicates,
! [X1] :
( ssSkP1088(X1)
<=> $true ) ).
fof(ssSkP1089,fi_predicates,
! [X1] :
( ssSkP1089(X1)
<=> $true ) ).
fof(ssSkP109,fi_predicates,
! [X1] :
( ssSkP109(X1)
<=> $false ) ).
fof(ssSkP1090,fi_predicates,
! [X1] :
( ssSkP1090(X1)
<=> $true ) ).
fof(ssSkP1091,fi_predicates,
! [X1] :
( ssSkP1091(X1)
<=> $true ) ).
fof(ssSkP1092,fi_predicates,
! [X1] :
( ssSkP1092(X1)
<=> $true ) ).
fof(ssSkP1093,fi_predicates,
! [X1] :
( ssSkP1093(X1)
<=> $true ) ).
fof(ssSkP1094,fi_predicates,
! [X1] :
( ssSkP1094(X1)
<=> $true ) ).
fof(ssSkP1095,fi_predicates,
! [X1] :
( ssSkP1095(X1)
<=> $true ) ).
fof(ssSkP1096,fi_predicates,
! [X1] :
( ssSkP1096(X1)
<=> $true ) ).
fof(ssSkP1097,fi_predicates,
! [X1] :
( ssSkP1097(X1)
<=> $true ) ).
fof(ssSkP1098,fi_predicates,
! [X1] :
( ssSkP1098(X1)
<=> $true ) ).
fof(ssSkP1099,fi_predicates,
! [X1] :
( ssSkP1099(X1)
<=> $true ) ).
fof(ssSkP11,fi_predicates,
! [X1] :
( ssSkP11(X1)
<=> $false ) ).
fof(ssSkP110,fi_predicates,
! [X1] :
( ssSkP110(X1)
<=> $false ) ).
fof(ssSkP1100,fi_predicates,
! [X1] :
( ssSkP1100(X1)
<=> $true ) ).
fof(ssSkP1101,fi_predicates,
! [X1,X2] :
( ssSkP1101(X1,X2)
<=> $true ) ).
fof(ssSkP1102,fi_predicates,
! [X1,X2] :
( ssSkP1102(X1,X2)
<=> $true ) ).
fof(ssSkP1103,fi_predicates,
! [X1] :
( ssSkP1103(X1)
<=> $true ) ).
fof(ssSkP1104,fi_predicates,
! [X1] :
( ssSkP1104(X1)
<=> $true ) ).
fof(ssSkP1105,fi_predicates,
! [X1] :
( ssSkP1105(X1)
<=> $true ) ).
fof(ssSkP1106,fi_predicates,
! [X1] :
( ssSkP1106(X1)
<=> $true ) ).
fof(ssSkP1107,fi_predicates,
! [X1] :
( ssSkP1107(X1)
<=> $true ) ).
fof(ssSkP1108,fi_predicates,
! [X1] :
( ssSkP1108(X1)
<=> $true ) ).
fof(ssSkP1109,fi_predicates,
! [X1] :
( ssSkP1109(X1)
<=> $true ) ).
fof(ssSkP111,fi_predicates,
! [X1] :
( ssSkP111(X1)
<=> $false ) ).
fof(ssSkP1110,fi_predicates,
! [X1] :
( ssSkP1110(X1)
<=> $true ) ).
fof(ssSkP1111,fi_predicates,
! [X1] :
( ssSkP1111(X1)
<=> $true ) ).
fof(ssSkP1112,fi_predicates,
! [X1] :
( ssSkP1112(X1)
<=> $true ) ).
fof(ssSkP1113,fi_predicates,
! [X1] :
( ssSkP1113(X1)
<=> $true ) ).
fof(ssSkP1114,fi_predicates,
! [X1] :
( ssSkP1114(X1)
<=> $true ) ).
fof(ssSkP1115,fi_predicates,
! [X1] :
( ssSkP1115(X1)
<=> $true ) ).
fof(ssSkP1116,fi_predicates,
! [X1] :
( ssSkP1116(X1)
<=> $true ) ).
fof(ssSkP1117,fi_predicates,
! [X1] :
( ssSkP1117(X1)
<=> $true ) ).
fof(ssSkP1118,fi_predicates,
! [X1] :
( ssSkP1118(X1)
<=> $true ) ).
fof(ssSkP1119,fi_predicates,
! [X1] :
( ssSkP1119(X1)
<=> $true ) ).
fof(ssSkP112,fi_predicates,
! [X1] :
( ssSkP112(X1)
<=> $false ) ).
fof(ssSkP1120,fi_predicates,
! [X1] :
( ssSkP1120(X1)
<=> $true ) ).
fof(ssSkP1121,fi_predicates,
! [X1] :
( ssSkP1121(X1)
<=> $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,
! [X1] :
( ssSkP113(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP114(X1)
<=> $false ) ).
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,X2] :
( ssSkP1145(X1,X2)
<=> $true ) ).
fof(ssSkP1146,fi_predicates,
! [X1,X2] :
( ssSkP1146(X1,X2)
<=> $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,
! [X1] :
( ssSkP115(X1)
<=> $false ) ).
fof(ssSkP1150,fi_predicates,
! [X1] :
( ssSkP1150(X1)
<=> $true ) ).
fof(ssSkP1151,fi_predicates,
! [X1] :
( ssSkP1151(X1)
<=> $true ) ).
fof(ssSkP1152,fi_predicates,
! [X1] :
( ssSkP1152(X1)
<=> $true ) ).
fof(ssSkP1153,fi_predicates,
! [X1] :
( ssSkP1153(X1)
<=> $true ) ).
fof(ssSkP1154,fi_predicates,
! [X1] :
( ssSkP1154(X1)
<=> $true ) ).
fof(ssSkP1155,fi_predicates,
! [X1] :
( ssSkP1155(X1)
<=> $true ) ).
fof(ssSkP1156,fi_predicates,
! [X1] :
( ssSkP1156(X1)
<=> $true ) ).
fof(ssSkP1157,fi_predicates,
! [X1] :
( ssSkP1157(X1)
<=> $true ) ).
fof(ssSkP1158,fi_predicates,
! [X1] :
( ssSkP1158(X1)
<=> $true ) ).
fof(ssSkP1159,fi_predicates,
! [X1] :
( ssSkP1159(X1)
<=> $true ) ).
fof(ssSkP116,fi_predicates,
! [X1] :
( ssSkP116(X1)
<=> $false ) ).
fof(ssSkP1160,fi_predicates,
! [X1] :
( ssSkP1160(X1)
<=> $true ) ).
fof(ssSkP1161,fi_predicates,
! [X1] :
( ssSkP1161(X1)
<=> $true ) ).
fof(ssSkP1162,fi_predicates,
! [X1] :
( ssSkP1162(X1)
<=> $true ) ).
fof(ssSkP1163,fi_predicates,
! [X1] :
( ssSkP1163(X1)
<=> $true ) ).
fof(ssSkP1164,fi_predicates,
! [X1] :
( ssSkP1164(X1)
<=> $true ) ).
fof(ssSkP1165,fi_predicates,
! [X1] :
( ssSkP1165(X1)
<=> $true ) ).
fof(ssSkP1166,fi_predicates,
! [X1] :
( ssSkP1166(X1)
<=> $true ) ).
fof(ssSkP1167,fi_predicates,
! [X1] :
( ssSkP1167(X1)
<=> $true ) ).
fof(ssSkP1168,fi_predicates,
! [X1] :
( ssSkP1168(X1)
<=> $true ) ).
fof(ssSkP1169,fi_predicates,
! [X1] :
( ssSkP1169(X1)
<=> $true ) ).
fof(ssSkP117,fi_predicates,
! [X1] :
( ssSkP117(X1)
<=> $false ) ).
fof(ssSkP1170,fi_predicates,
! [X1] :
( ssSkP1170(X1)
<=> $true ) ).
fof(ssSkP1171,fi_predicates,
! [X1] :
( ssSkP1171(X1)
<=> $true ) ).
fof(ssSkP1172,fi_predicates,
! [X1] :
( ssSkP1172(X1)
<=> $true ) ).
fof(ssSkP1173,fi_predicates,
! [X1] :
( ssSkP1173(X1)
<=> $true ) ).
fof(ssSkP1174,fi_predicates,
! [X1] :
( ssSkP1174(X1)
<=> $true ) ).
fof(ssSkP1175,fi_predicates,
! [X1] :
( ssSkP1175(X1)
<=> $true ) ).
fof(ssSkP1176,fi_predicates,
! [X1] :
( ssSkP1176(X1)
<=> $true ) ).
fof(ssSkP1177,fi_predicates,
! [X1] :
( ssSkP1177(X1)
<=> $true ) ).
fof(ssSkP1178,fi_predicates,
! [X1] :
( ssSkP1178(X1)
<=> $true ) ).
fof(ssSkP1179,fi_predicates,
! [X1] :
( ssSkP1179(X1)
<=> $true ) ).
fof(ssSkP118,fi_predicates,
! [X1] :
( ssSkP118(X1)
<=> $false ) ).
fof(ssSkP1180,fi_predicates,
! [X1] :
( ssSkP1180(X1)
<=> $true ) ).
fof(ssSkP1181,fi_predicates,
! [X1] :
( ssSkP1181(X1)
<=> $true ) ).
fof(ssSkP1182,fi_predicates,
! [X1] :
( ssSkP1182(X1)
<=> $true ) ).
fof(ssSkP1183,fi_predicates,
! [X1] :
( ssSkP1183(X1)
<=> $true ) ).
fof(ssSkP1184,fi_predicates,
! [X1] :
( ssSkP1184(X1)
<=> $true ) ).
fof(ssSkP1185,fi_predicates,
! [X1] :
( ssSkP1185(X1)
<=> $true ) ).
fof(ssSkP1186,fi_predicates,
! [X1] :
( ssSkP1186(X1)
<=> $true ) ).
fof(ssSkP1187,fi_predicates,
! [X1] :
( ssSkP1187(X1)
<=> $true ) ).
fof(ssSkP1188,fi_predicates,
! [X1,X2] :
( ssSkP1188(X1,X2)
<=> $true ) ).
fof(ssSkP1189,fi_predicates,
! [X1,X2] :
( ssSkP1189(X1,X2)
<=> $true ) ).
fof(ssSkP119,fi_predicates,
! [X1] :
( ssSkP119(X1)
<=> $false ) ).
fof(ssSkP1190,fi_predicates,
! [X1] :
( ssSkP1190(X1)
<=> $false ) ).
fof(ssSkP1191,fi_predicates,
! [X1] :
( ssSkP1191(X1)
<=> $false ) ).
fof(ssSkP1192,fi_predicates,
! [X1] :
( ssSkP1192(X1)
<=> $false ) ).
fof(ssSkP1193,fi_predicates,
! [X1] :
( ssSkP1193(X1)
<=> $false ) ).
fof(ssSkP1194,fi_predicates,
! [X1] :
( ssSkP1194(X1)
<=> $false ) ).
fof(ssSkP1195,fi_predicates,
! [X1] :
( ssSkP1195(X1)
<=> $false ) ).
fof(ssSkP1196,fi_predicates,
! [X1] :
( ssSkP1196(X1)
<=> $false ) ).
fof(ssSkP1197,fi_predicates,
! [X1] :
( ssSkP1197(X1)
<=> $false ) ).
fof(ssSkP1198,fi_predicates,
! [X1] :
( ssSkP1198(X1)
<=> $false ) ).
fof(ssSkP1199,fi_predicates,
! [X1] :
( ssSkP1199(X1)
<=> $false ) ).
fof(ssSkP12,fi_predicates,
! [X1] :
( ssSkP12(X1)
<=> $false ) ).
fof(ssSkP120,fi_predicates,
! [X1] :
( ssSkP120(X1)
<=> $true ) ).
fof(ssSkP1200,fi_predicates,
! [X1] :
( ssSkP1200(X1)
<=> $false ) ).
fof(ssSkP1201,fi_predicates,
! [X1] :
( ssSkP1201(X1)
<=> $false ) ).
fof(ssSkP1202,fi_predicates,
! [X1] :
( ssSkP1202(X1)
<=> $false ) ).
fof(ssSkP1203,fi_predicates,
! [X1] :
( ssSkP1203(X1)
<=> $false ) ).
fof(ssSkP1204,fi_predicates,
! [X1] :
( ssSkP1204(X1)
<=> $false ) ).
fof(ssSkP1205,fi_predicates,
! [X1] :
( ssSkP1205(X1)
<=> $true ) ).
fof(ssSkP1206,fi_predicates,
! [X1] :
( ssSkP1206(X1)
<=> $true ) ).
fof(ssSkP1207,fi_predicates,
! [X1] :
( ssSkP1207(X1)
<=> $true ) ).
fof(ssSkP1208,fi_predicates,
! [X1] :
( ssSkP1208(X1)
<=> $true ) ).
fof(ssSkP1209,fi_predicates,
! [X1] :
( ssSkP1209(X1)
<=> $true ) ).
fof(ssSkP121,fi_predicates,
! [X1] :
( ssSkP121(X1)
<=> $true ) ).
fof(ssSkP1210,fi_predicates,
! [X1] :
( ssSkP1210(X1)
<=> $true ) ).
fof(ssSkP1211,fi_predicates,
! [X1] :
( ssSkP1211(X1)
<=> $true ) ).
fof(ssSkP1212,fi_predicates,
! [X1] :
( ssSkP1212(X1)
<=> $true ) ).
fof(ssSkP1213,fi_predicates,
! [X1] :
( ssSkP1213(X1)
<=> $true ) ).
fof(ssSkP1214,fi_predicates,
! [X1] :
( ssSkP1214(X1)
<=> $true ) ).
fof(ssSkP1215,fi_predicates,
! [X1] :
( ssSkP1215(X1)
<=> $true ) ).
fof(ssSkP1216,fi_predicates,
! [X1] :
( ssSkP1216(X1)
<=> $true ) ).
fof(ssSkP1217,fi_predicates,
! [X1] :
( ssSkP1217(X1)
<=> $true ) ).
fof(ssSkP1218,fi_predicates,
! [X1] :
( ssSkP1218(X1)
<=> $true ) ).
fof(ssSkP1219,fi_predicates,
! [X1] :
( ssSkP1219(X1)
<=> $true ) ).
fof(ssSkP122,fi_predicates,
! [X1,X2] :
( ssSkP122(X1,X2)
<=> $true ) ).
fof(ssSkP1220,fi_predicates,
! [X1] :
( ssSkP1220(X1)
<=> $true ) ).
fof(ssSkP1221,fi_predicates,
! [X1] :
( ssSkP1221(X1)
<=> $true ) ).
fof(ssSkP1222,fi_predicates,
! [X1] :
( ssSkP1222(X1)
<=> $true ) ).
fof(ssSkP1223,fi_predicates,
! [X1] :
( ssSkP1223(X1)
<=> $true ) ).
fof(ssSkP1224,fi_predicates,
! [X1] :
( ssSkP1224(X1)
<=> $true ) ).
fof(ssSkP1225,fi_predicates,
! [X1] :
( ssSkP1225(X1)
<=> $true ) ).
fof(ssSkP1226,fi_predicates,
! [X1] :
( ssSkP1226(X1)
<=> $true ) ).
fof(ssSkP1227,fi_predicates,
! [X1] :
( ssSkP1227(X1)
<=> $true ) ).
fof(ssSkP1228,fi_predicates,
! [X1] :
( ssSkP1228(X1)
<=> $true ) ).
fof(ssSkP1229,fi_predicates,
! [X1] :
( ssSkP1229(X1)
<=> $true ) ).
fof(ssSkP123,fi_predicates,
! [X1,X2] :
( ssSkP123(X1,X2)
<=> $true ) ).
fof(ssSkP1230,fi_predicates,
! [X1] :
( ssSkP1230(X1)
<=> $true ) ).
fof(ssSkP1231,fi_predicates,
! [X1] :
( ssSkP1231(X1)
<=> $true ) ).
fof(ssSkP1232,fi_predicates,
! [X1,X2] :
( ssSkP1232(X1,X2)
<=> $true ) ).
fof(ssSkP1233,fi_predicates,
! [X1,X2] :
( ssSkP1233(X1,X2)
<=> $true ) ).
fof(ssSkP1234,fi_predicates,
! [X1] :
( ssSkP1234(X1)
<=> $false ) ).
fof(ssSkP1235,fi_predicates,
! [X1] :
( ssSkP1235(X1)
<=> $false ) ).
fof(ssSkP1236,fi_predicates,
! [X1] :
( ssSkP1236(X1)
<=> $false ) ).
fof(ssSkP1237,fi_predicates,
! [X1] :
( ssSkP1237(X1)
<=> $false ) ).
fof(ssSkP1238,fi_predicates,
! [X1] :
( ssSkP1238(X1)
<=> $false ) ).
fof(ssSkP1239,fi_predicates,
! [X1] :
( ssSkP1239(X1)
<=> $false ) ).
fof(ssSkP124,fi_predicates,
! [X1] :
( ssSkP124(X1)
<=> $false ) ).
fof(ssSkP1240,fi_predicates,
! [X1] :
( ssSkP1240(X1)
<=> $true ) ).
fof(ssSkP1241,fi_predicates,
! [X1] :
( ssSkP1241(X1)
<=> $true ) ).
fof(ssSkP1242,fi_predicates,
! [X1] :
( ssSkP1242(X1)
<=> $true ) ).
fof(ssSkP1243,fi_predicates,
! [X1] :
( ssSkP1243(X1)
<=> $true ) ).
fof(ssSkP1244,fi_predicates,
! [X1] :
( ssSkP1244(X1)
<=> $true ) ).
fof(ssSkP1245,fi_predicates,
! [X1] :
( ssSkP1245(X1)
<=> $true ) ).
fof(ssSkP1246,fi_predicates,
! [X1] :
( ssSkP1246(X1)
<=> $true ) ).
fof(ssSkP1247,fi_predicates,
! [X1] :
( ssSkP1247(X1)
<=> $true ) ).
fof(ssSkP1248,fi_predicates,
! [X1] :
( ssSkP1248(X1)
<=> $true ) ).
fof(ssSkP1249,fi_predicates,
! [X1] :
( ssSkP1249(X1)
<=> $true ) ).
fof(ssSkP125,fi_predicates,
! [X1] :
( ssSkP125(X1)
<=> $false ) ).
fof(ssSkP1250,fi_predicates,
! [X1] :
( ssSkP1250(X1)
<=> $true ) ).
fof(ssSkP1251,fi_predicates,
! [X1] :
( ssSkP1251(X1)
<=> $true ) ).
fof(ssSkP1252,fi_predicates,
! [X1] :
( ssSkP1252(X1)
<=> $true ) ).
fof(ssSkP1253,fi_predicates,
! [X1] :
( ssSkP1253(X1)
<=> $true ) ).
fof(ssSkP1254,fi_predicates,
! [X1] :
( ssSkP1254(X1)
<=> $true ) ).
fof(ssSkP1255,fi_predicates,
! [X1] :
( ssSkP1255(X1)
<=> $true ) ).
fof(ssSkP1256,fi_predicates,
! [X1] :
( ssSkP1256(X1)
<=> $true ) ).
fof(ssSkP1257,fi_predicates,
! [X1] :
( ssSkP1257(X1)
<=> $true ) ).
fof(ssSkP1258,fi_predicates,
! [X1] :
( ssSkP1258(X1)
<=> $true ) ).
fof(ssSkP1259,fi_predicates,
! [X1] :
( ssSkP1259(X1)
<=> $true ) ).
fof(ssSkP126,fi_predicates,
! [X1] :
( ssSkP126(X1)
<=> $false ) ).
fof(ssSkP1260,fi_predicates,
! [X1] :
( ssSkP1260(X1)
<=> $true ) ).
fof(ssSkP1261,fi_predicates,
! [X1] :
( ssSkP1261(X1)
<=> $true ) ).
fof(ssSkP1262,fi_predicates,
! [X1] :
( ssSkP1262(X1)
<=> $true ) ).
fof(ssSkP1263,fi_predicates,
! [X1] :
( ssSkP1263(X1)
<=> $true ) ).
fof(ssSkP1264,fi_predicates,
! [X1,X2] :
( ssSkP1264(X1,X2)
<=> $true ) ).
fof(ssSkP1265,fi_predicates,
! [X1,X2] :
( ssSkP1265(X1,X2)
<=> $true ) ).
fof(ssSkP1266,fi_predicates,
! [X1] :
( ssSkP1266(X1)
<=> $false ) ).
fof(ssSkP1267,fi_predicates,
! [X1] :
( ssSkP1267(X1)
<=> $false ) ).
fof(ssSkP1268,fi_predicates,
! [X1] :
( ssSkP1268(X1)
<=> $false ) ).
fof(ssSkP1269,fi_predicates,
! [X1] :
( ssSkP1269(X1)
<=> $false ) ).
fof(ssSkP127,fi_predicates,
! [X1] :
( ssSkP127(X1)
<=> $false ) ).
fof(ssSkP1270,fi_predicates,
! [X1] :
( ssSkP1270(X1)
<=> $false ) ).
fof(ssSkP1271,fi_predicates,
! [X1] :
( ssSkP1271(X1)
<=> $false ) ).
fof(ssSkP1272,fi_predicates,
! [X1] :
( ssSkP1272(X1)
<=> $true ) ).
fof(ssSkP1273,fi_predicates,
! [X1] :
( ssSkP1273(X1)
<=> $true ) ).
fof(ssSkP1274,fi_predicates,
! [X1] :
( ssSkP1274(X1)
<=> $true ) ).
fof(ssSkP1275,fi_predicates,
! [X1] :
( ssSkP1275(X1)
<=> $true ) ).
fof(ssSkP1276,fi_predicates,
! [X1] :
( ssSkP1276(X1)
<=> $true ) ).
fof(ssSkP1277,fi_predicates,
! [X1] :
( ssSkP1277(X1)
<=> $true ) ).
fof(ssSkP1278,fi_predicates,
! [X1] :
( ssSkP1278(X1)
<=> $true ) ).
fof(ssSkP1279,fi_predicates,
! [X1] :
( ssSkP1279(X1)
<=> $true ) ).
fof(ssSkP128,fi_predicates,
! [X1] :
( ssSkP128(X1)
<=> $false ) ).
fof(ssSkP1280,fi_predicates,
! [X1] :
( ssSkP1280(X1)
<=> $true ) ).
fof(ssSkP1281,fi_predicates,
! [X1] :
( ssSkP1281(X1)
<=> $true ) ).
fof(ssSkP1282,fi_predicates,
! [X1] :
( ssSkP1282(X1)
<=> $true ) ).
fof(ssSkP1283,fi_predicates,
! [X1] :
( ssSkP1283(X1)
<=> $true ) ).
fof(ssSkP1284,fi_predicates,
! [X1] :
( ssSkP1284(X1)
<=> $true ) ).
fof(ssSkP1285,fi_predicates,
! [X1] :
( ssSkP1285(X1)
<=> $true ) ).
fof(ssSkP1286,fi_predicates,
! [X1] :
( ssSkP1286(X1)
<=> $true ) ).
fof(ssSkP1287,fi_predicates,
! [X1] :
( ssSkP1287(X1)
<=> $true ) ).
fof(ssSkP1288,fi_predicates,
! [X1] :
( ssSkP1288(X1)
<=> $true ) ).
fof(ssSkP1289,fi_predicates,
! [X1] :
( ssSkP1289(X1)
<=> $true ) ).
fof(ssSkP129,fi_predicates,
! [X1] :
( ssSkP129(X1)
<=> $false ) ).
fof(ssSkP1290,fi_predicates,
! [X1] :
( ssSkP1290(X1)
<=> $true ) ).
fof(ssSkP1291,fi_predicates,
! [X1] :
( ssSkP1291(X1)
<=> $true ) ).
fof(ssSkP1292,fi_predicates,
! [X1] :
( ssSkP1292(X1)
<=> $true ) ).
fof(ssSkP1293,fi_predicates,
! [X1] :
( ssSkP1293(X1)
<=> $true ) ).
fof(ssSkP1294,fi_predicates,
! [X1] :
( ssSkP1294(X1)
<=> $true ) ).
fof(ssSkP1295,fi_predicates,
! [X1] :
( ssSkP1295(X1)
<=> $true ) ).
fof(ssSkP1296,fi_predicates,
! [X1] :
( ssSkP1296(X1)
<=> $true ) ).
fof(ssSkP1297,fi_predicates,
! [X1] :
( ssSkP1297(X1)
<=> $true ) ).
fof(ssSkP1298,fi_predicates,
! [X1,X2] :
( ssSkP1298(X1,X2)
<=> $true ) ).
fof(ssSkP1299,fi_predicates,
! [X1,X2] :
( ssSkP1299(X1,X2)
<=> $true ) ).
fof(ssSkP13,fi_predicates,
! [X1] :
( ssSkP13(X1)
<=> $false ) ).
fof(ssSkP130,fi_predicates,
! [X1] :
( ssSkP130(X1)
<=> $false ) ).
fof(ssSkP1300,fi_predicates,
! [X1] :
( ssSkP1300(X1)
<=> $false ) ).
fof(ssSkP1301,fi_predicates,
! [X1] :
( ssSkP1301(X1)
<=> $false ) ).
fof(ssSkP1302,fi_predicates,
! [X1] :
( ssSkP1302(X1)
<=> $false ) ).
fof(ssSkP1303,fi_predicates,
! [X1] :
( ssSkP1303(X1)
<=> $false ) ).
fof(ssSkP1304,fi_predicates,
! [X1] :
( ssSkP1304(X1)
<=> $false ) ).
fof(ssSkP1305,fi_predicates,
! [X1] :
( ssSkP1305(X1)
<=> $false ) ).
fof(ssSkP1306,fi_predicates,
! [X1] :
( ssSkP1306(X1)
<=> $false ) ).
fof(ssSkP1307,fi_predicates,
! [X1] :
( ssSkP1307(X1)
<=> $false ) ).
fof(ssSkP1308,fi_predicates,
! [X1] :
( ssSkP1308(X1)
<=> $false ) ).
fof(ssSkP1309,fi_predicates,
! [X1] :
( ssSkP1309(X1)
<=> $false ) ).
fof(ssSkP131,fi_predicates,
! [X1] :
( ssSkP131(X1)
<=> $false ) ).
fof(ssSkP1310,fi_predicates,
! [X1] :
( ssSkP1310(X1)
<=> $false ) ).
fof(ssSkP1311,fi_predicates,
! [X1] :
( ssSkP1311(X1)
<=> $false ) ).
fof(ssSkP1312,fi_predicates,
! [X1] :
( ssSkP1312(X1)
<=> $false ) ).
fof(ssSkP1313,fi_predicates,
! [X1] :
( ssSkP1313(X1)
<=> $false ) ).
fof(ssSkP1314,fi_predicates,
! [X1] :
( ssSkP1314(X1)
<=> $true ) ).
fof(ssSkP1315,fi_predicates,
! [X1] :
( ssSkP1315(X1)
<=> $true ) ).
fof(ssSkP1316,fi_predicates,
! [X1] :
( ssSkP1316(X1)
<=> $true ) ).
fof(ssSkP1317,fi_predicates,
! [X1] :
( ssSkP1317(X1)
<=> $true ) ).
fof(ssSkP1318,fi_predicates,
! [X1] :
( ssSkP1318(X1)
<=> $true ) ).
fof(ssSkP1319,fi_predicates,
! [X1] :
( ssSkP1319(X1)
<=> $true ) ).
fof(ssSkP132,fi_predicates,
! [X1] :
( ssSkP132(X1)
<=> $false ) ).
fof(ssSkP1320,fi_predicates,
! [X1] :
( ssSkP1320(X1)
<=> $true ) ).
fof(ssSkP1321,fi_predicates,
! [X1] :
( ssSkP1321(X1)
<=> $true ) ).
fof(ssSkP1322,fi_predicates,
! [X1] :
( ssSkP1322(X1)
<=> $true ) ).
fof(ssSkP1323,fi_predicates,
! [X1] :
( ssSkP1323(X1)
<=> $true ) ).
fof(ssSkP1324,fi_predicates,
! [X1] :
( ssSkP1324(X1)
<=> $true ) ).
fof(ssSkP1325,fi_predicates,
! [X1] :
( ssSkP1325(X1)
<=> $true ) ).
fof(ssSkP1326,fi_predicates,
! [X1] :
( ssSkP1326(X1)
<=> $true ) ).
fof(ssSkP1327,fi_predicates,
! [X1] :
( ssSkP1327(X1)
<=> $true ) ).
fof(ssSkP1328,fi_predicates,
! [X1] :
( ssSkP1328(X1)
<=> $true ) ).
fof(ssSkP1329,fi_predicates,
! [X1] :
( ssSkP1329(X1)
<=> $true ) ).
fof(ssSkP133,fi_predicates,
! [X1] :
( ssSkP133(X1)
<=> $false ) ).
fof(ssSkP1330,fi_predicates,
! [X1] :
( ssSkP1330(X1)
<=> $true ) ).
fof(ssSkP1331,fi_predicates,
! [X1] :
( ssSkP1331(X1)
<=> $true ) ).
fof(ssSkP1332,fi_predicates,
! [X1] :
( ssSkP1332(X1)
<=> $true ) ).
fof(ssSkP1333,fi_predicates,
! [X1] :
( ssSkP1333(X1)
<=> $true ) ).
fof(ssSkP1334,fi_predicates,
! [X1] :
( ssSkP1334(X1)
<=> $true ) ).
fof(ssSkP1335,fi_predicates,
! [X1] :
( ssSkP1335(X1)
<=> $true ) ).
fof(ssSkP1336,fi_predicates,
! [X1,X2] :
( ssSkP1336(X1,X2)
<=> $true ) ).
fof(ssSkP1337,fi_predicates,
! [X1,X2] :
( ssSkP1337(X1,X2)
<=> $true ) ).
fof(ssSkP1338,fi_predicates,
! [X1] :
( ssSkP1338(X1)
<=> $true ) ).
fof(ssSkP1339,fi_predicates,
! [X1] :
( ssSkP1339(X1)
<=> $true ) ).
fof(ssSkP134,fi_predicates,
! [X1] :
( ssSkP134(X1)
<=> $false ) ).
fof(ssSkP1340,fi_predicates,
! [X1] :
( ssSkP1340(X1)
<=> $true ) ).
fof(ssSkP1341,fi_predicates,
! [X1] :
( ssSkP1341(X1)
<=> $true ) ).
fof(ssSkP1342,fi_predicates,
! [X1] :
( ssSkP1342(X1)
<=> $true ) ).
fof(ssSkP1343,fi_predicates,
! [X1] :
( ssSkP1343(X1)
<=> $true ) ).
fof(ssSkP1344,fi_predicates,
! [X1] :
( ssSkP1344(X1)
<=> $true ) ).
fof(ssSkP1345,fi_predicates,
! [X1] :
( ssSkP1345(X1)
<=> $true ) ).
fof(ssSkP1346,fi_predicates,
! [X1] :
( ssSkP1346(X1)
<=> $true ) ).
fof(ssSkP1347,fi_predicates,
! [X1] :
( ssSkP1347(X1)
<=> $true ) ).
fof(ssSkP1348,fi_predicates,
! [X1] :
( ssSkP1348(X1)
<=> $true ) ).
fof(ssSkP1349,fi_predicates,
! [X1] :
( ssSkP1349(X1)
<=> $true ) ).
fof(ssSkP135,fi_predicates,
! [X1] :
( ssSkP135(X1)
<=> $false ) ).
fof(ssSkP1350,fi_predicates,
! [X1] :
( ssSkP1350(X1)
<=> $true ) ).
fof(ssSkP1351,fi_predicates,
! [X1] :
( ssSkP1351(X1)
<=> $true ) ).
fof(ssSkP1352,fi_predicates,
! [X1] :
( ssSkP1352(X1)
<=> $true ) ).
fof(ssSkP1353,fi_predicates,
! [X1] :
( ssSkP1353(X1)
<=> $true ) ).
fof(ssSkP1354,fi_predicates,
! [X1] :
( ssSkP1354(X1)
<=> $true ) ).
fof(ssSkP1355,fi_predicates,
! [X1] :
( ssSkP1355(X1)
<=> $true ) ).
fof(ssSkP1356,fi_predicates,
! [X1] :
( ssSkP1356(X1)
<=> $true ) ).
fof(ssSkP1357,fi_predicates,
! [X1] :
( ssSkP1357(X1)
<=> $true ) ).
fof(ssSkP1358,fi_predicates,
! [X1] :
( ssSkP1358(X1)
<=> $true ) ).
fof(ssSkP1359,fi_predicates,
! [X1] :
( ssSkP1359(X1)
<=> $true ) ).
fof(ssSkP136,fi_predicates,
! [X1] :
( ssSkP136(X1)
<=> $false ) ).
fof(ssSkP1360,fi_predicates,
! [X1] :
( ssSkP1360(X1)
<=> $true ) ).
fof(ssSkP1361,fi_predicates,
! [X1] :
( ssSkP1361(X1)
<=> $true ) ).
fof(ssSkP1362,fi_predicates,
! [X1] :
( ssSkP1362(X1)
<=> $true ) ).
fof(ssSkP1363,fi_predicates,
! [X1] :
( ssSkP1363(X1)
<=> $true ) ).
fof(ssSkP1364,fi_predicates,
! [X1] :
( ssSkP1364(X1)
<=> $true ) ).
fof(ssSkP1365,fi_predicates,
! [X1] :
( ssSkP1365(X1)
<=> $true ) ).
fof(ssSkP1366,fi_predicates,
! [X1] :
( ssSkP1366(X1)
<=> $true ) ).
fof(ssSkP1367,fi_predicates,
! [X1] :
( ssSkP1367(X1)
<=> $true ) ).
fof(ssSkP1368,fi_predicates,
! [X1] :
( ssSkP1368(X1)
<=> $true ) ).
fof(ssSkP1369,fi_predicates,
! [X1] :
( ssSkP1369(X1)
<=> $true ) ).
fof(ssSkP137,fi_predicates,
! [X1] :
( ssSkP137(X1)
<=> $false ) ).
fof(ssSkP1370,fi_predicates,
! [X1] :
( ssSkP1370(X1)
<=> $true ) ).
fof(ssSkP1371,fi_predicates,
! [X1] :
( ssSkP1371(X1)
<=> $true ) ).
fof(ssSkP1372,fi_predicates,
! [X1] :
( ssSkP1372(X1)
<=> $true ) ).
fof(ssSkP1373,fi_predicates,
! [X1] :
( ssSkP1373(X1)
<=> $true ) ).
fof(ssSkP1374,fi_predicates,
! [X1] :
( ssSkP1374(X1)
<=> $true ) ).
fof(ssSkP1375,fi_predicates,
! [X1] :
( ssSkP1375(X1)
<=> $true ) ).
fof(ssSkP1376,fi_predicates,
! [X1] :
( ssSkP1376(X1)
<=> $true ) ).
fof(ssSkP1377,fi_predicates,
! [X1] :
( ssSkP1377(X1)
<=> $true ) ).
fof(ssSkP1378,fi_predicates,
! [X1] :
( ssSkP1378(X1)
<=> $true ) ).
fof(ssSkP1379,fi_predicates,
! [X1] :
( ssSkP1379(X1)
<=> $true ) ).
fof(ssSkP138,fi_predicates,
! [X1] :
( ssSkP138(X1)
<=> $false ) ).
fof(ssSkP1380,fi_predicates,
! [X1,X2] :
( ssSkP1380(X1,X2)
<=> $true ) ).
fof(ssSkP1381,fi_predicates,
! [X1,X2] :
( ssSkP1381(X1,X2)
<=> $true ) ).
fof(ssSkP1382,fi_predicates,
! [X1] :
( ssSkP1382(X1)
<=> $false ) ).
fof(ssSkP1383,fi_predicates,
! [X1] :
( ssSkP1383(X1)
<=> $false ) ).
fof(ssSkP1384,fi_predicates,
! [X1] :
( ssSkP1384(X1)
<=> $false ) ).
fof(ssSkP1385,fi_predicates,
! [X1] :
( ssSkP1385(X1)
<=> $false ) ).
fof(ssSkP1386,fi_predicates,
! [X1] :
( ssSkP1386(X1)
<=> $false ) ).
fof(ssSkP1387,fi_predicates,
! [X1] :
( ssSkP1387(X1)
<=> $false ) ).
fof(ssSkP1388,fi_predicates,
! [X1] :
( ssSkP1388(X1)
<=> $false ) ).
fof(ssSkP1389,fi_predicates,
! [X1] :
( ssSkP1389(X1)
<=> $false ) ).
fof(ssSkP139,fi_predicates,
! [X1] :
( ssSkP139(X1)
<=> $false ) ).
fof(ssSkP1390,fi_predicates,
! [X1] :
( ssSkP1390(X1)
<=> $false ) ).
fof(ssSkP1391,fi_predicates,
! [X1] :
( ssSkP1391(X1)
<=> $false ) ).
fof(ssSkP1392,fi_predicates,
! [X1] :
( ssSkP1392(X1)
<=> $false ) ).
fof(ssSkP1393,fi_predicates,
! [X1] :
( ssSkP1393(X1)
<=> $false ) ).
fof(ssSkP1394,fi_predicates,
! [X1] :
( ssSkP1394(X1)
<=> $false ) ).
fof(ssSkP1395,fi_predicates,
! [X1] :
( ssSkP1395(X1)
<=> $false ) ).
fof(ssSkP1396,fi_predicates,
! [X1] :
( ssSkP1396(X1)
<=> $false ) ).
fof(ssSkP1397,fi_predicates,
! [X1] :
( ssSkP1397(X1)
<=> $false ) ).
fof(ssSkP1398,fi_predicates,
! [X1] :
( ssSkP1398(X1)
<=> $false ) ).
fof(ssSkP1399,fi_predicates,
! [X1] :
( ssSkP1399(X1)
<=> $false ) ).
fof(ssSkP14,fi_predicates,
! [X1] :
( ssSkP14(X1)
<=> $false ) ).
fof(ssSkP140,fi_predicates,
! [X1] :
( ssSkP140(X1)
<=> $false ) ).
fof(ssSkP1400,fi_predicates,
! [X1] :
( ssSkP1400(X1)
<=> $false ) ).
fof(ssSkP1401,fi_predicates,
! [X1] :
( ssSkP1401(X1)
<=> $true ) ).
fof(ssSkP1402,fi_predicates,
! [X1] :
( ssSkP1402(X1)
<=> $true ) ).
fof(ssSkP1403,fi_predicates,
! [X1] :
( ssSkP1403(X1)
<=> $true ) ).
fof(ssSkP1404,fi_predicates,
! [X1] :
( ssSkP1404(X1)
<=> $true ) ).
fof(ssSkP1405,fi_predicates,
! [X1] :
( ssSkP1405(X1)
<=> $true ) ).
fof(ssSkP1406,fi_predicates,
! [X1] :
( ssSkP1406(X1)
<=> $true ) ).
fof(ssSkP1407,fi_predicates,
! [X1] :
( ssSkP1407(X1)
<=> $true ) ).
fof(ssSkP1408,fi_predicates,
! [X1] :
( ssSkP1408(X1)
<=> $true ) ).
fof(ssSkP1409,fi_predicates,
! [X1] :
( ssSkP1409(X1)
<=> $true ) ).
fof(ssSkP141,fi_predicates,
! [X1] :
( ssSkP141(X1)
<=> $false ) ).
fof(ssSkP1410,fi_predicates,
! [X1] :
( ssSkP1410(X1)
<=> $true ) ).
fof(ssSkP1411,fi_predicates,
! [X1] :
( ssSkP1411(X1)
<=> $true ) ).
fof(ssSkP1412,fi_predicates,
! [X1] :
( ssSkP1412(X1)
<=> $true ) ).
fof(ssSkP1413,fi_predicates,
! [X1] :
( ssSkP1413(X1)
<=> $true ) ).
fof(ssSkP1414,fi_predicates,
! [X1] :
( ssSkP1414(X1)
<=> $true ) ).
fof(ssSkP1415,fi_predicates,
! [X1] :
( ssSkP1415(X1)
<=> $true ) ).
fof(ssSkP1416,fi_predicates,
! [X1] :
( ssSkP1416(X1)
<=> $true ) ).
fof(ssSkP1417,fi_predicates,
! [X1] :
( ssSkP1417(X1)
<=> $true ) ).
fof(ssSkP1418,fi_predicates,
! [X1] :
( ssSkP1418(X1)
<=> $true ) ).
fof(ssSkP1419,fi_predicates,
! [X1,X2] :
( ssSkP1419(X1,X2)
<=> $true ) ).
fof(ssSkP142,fi_predicates,
! [X1] :
( ssSkP142(X1)
<=> $false ) ).
fof(ssSkP1420,fi_predicates,
! [X1,X2] :
( ssSkP1420(X1,X2)
<=> $true ) ).
fof(ssSkP1421,fi_predicates,
! [X1] :
( ssSkP1421(X1)
<=> $false ) ).
fof(ssSkP1422,fi_predicates,
! [X1] :
( ssSkP1422(X1)
<=> $false ) ).
fof(ssSkP1423,fi_predicates,
! [X1] :
( ssSkP1423(X1)
<=> $false ) ).
fof(ssSkP1424,fi_predicates,
! [X1] :
( ssSkP1424(X1)
<=> $false ) ).
fof(ssSkP1425,fi_predicates,
! [X1] :
( ssSkP1425(X1)
<=> $false ) ).
fof(ssSkP1426,fi_predicates,
! [X1] :
( ssSkP1426(X1)
<=> $false ) ).
fof(ssSkP1427,fi_predicates,
! [X1] :
( ssSkP1427(X1)
<=> $false ) ).
fof(ssSkP1428,fi_predicates,
! [X1] :
( ssSkP1428(X1)
<=> $false ) ).
fof(ssSkP1429,fi_predicates,
! [X1] :
( ssSkP1429(X1)
<=> $false ) ).
fof(ssSkP143,fi_predicates,
! [X1] :
( ssSkP143(X1)
<=> $false ) ).
fof(ssSkP1430,fi_predicates,
! [X1] :
( ssSkP1430(X1)
<=> $false ) ).
fof(ssSkP1431,fi_predicates,
! [X1] :
( ssSkP1431(X1)
<=> $true ) ).
fof(ssSkP1432,fi_predicates,
! [X1] :
( ssSkP1432(X1)
<=> $true ) ).
fof(ssSkP1433,fi_predicates,
! [X1] :
( ssSkP1433(X1)
<=> $true ) ).
fof(ssSkP1434,fi_predicates,
! [X1] :
( ssSkP1434(X1)
<=> $true ) ).
fof(ssSkP1435,fi_predicates,
! [X1] :
( ssSkP1435(X1)
<=> $true ) ).
fof(ssSkP1436,fi_predicates,
! [X1] :
( ssSkP1436(X1)
<=> $true ) ).
fof(ssSkP1437,fi_predicates,
! [X1] :
( ssSkP1437(X1)
<=> $true ) ).
fof(ssSkP1438,fi_predicates,
! [X1] :
( ssSkP1438(X1)
<=> $true ) ).
fof(ssSkP1439,fi_predicates,
! [X1] :
( ssSkP1439(X1)
<=> $true ) ).
fof(ssSkP144,fi_predicates,
! [X1] :
( ssSkP144(X1)
<=> $false ) ).
fof(ssSkP1440,fi_predicates,
! [X1] :
( ssSkP1440(X1)
<=> $true ) ).
fof(ssSkP1441,fi_predicates,
! [X1] :
( ssSkP1441(X1)
<=> $true ) ).
fof(ssSkP1442,fi_predicates,
! [X1] :
( ssSkP1442(X1)
<=> $true ) ).
fof(ssSkP1443,fi_predicates,
! [X1] :
( ssSkP1443(X1)
<=> $true ) ).
fof(ssSkP1444,fi_predicates,
! [X1] :
( ssSkP1444(X1)
<=> $true ) ).
fof(ssSkP1445,fi_predicates,
! [X1] :
( ssSkP1445(X1)
<=> $true ) ).
fof(ssSkP1446,fi_predicates,
! [X1] :
( ssSkP1446(X1)
<=> $true ) ).
fof(ssSkP1447,fi_predicates,
! [X1] :
( ssSkP1447(X1)
<=> $true ) ).
fof(ssSkP1448,fi_predicates,
! [X1] :
( ssSkP1448(X1)
<=> $true ) ).
fof(ssSkP1449,fi_predicates,
! [X1] :
( ssSkP1449(X1)
<=> $true ) ).
fof(ssSkP145,fi_predicates,
! [X1] :
( ssSkP145(X1)
<=> $false ) ).
fof(ssSkP1450,fi_predicates,
! [X1] :
( ssSkP1450(X1)
<=> $true ) ).
fof(ssSkP1451,fi_predicates,
! [X1] :
( ssSkP1451(X1)
<=> $true ) ).
fof(ssSkP1452,fi_predicates,
! [X1] :
( ssSkP1452(X1)
<=> $true ) ).
fof(ssSkP1453,fi_predicates,
( ( ssSkP1453("1")
<=> $true )
& ( ssSkP1453("2")
<=> $true ) ) ).
fof(ssSkP1454,fi_predicates,
( ( ssSkP1454("1","1")
<=> $true )
& ( ssSkP1454("1","2")
<=> $true )
& ( ssSkP1454("2","1")
<=> $true )
& ( ssSkP1454("2","2")
<=> $true ) ) ).
fof(ssSkP1455,fi_predicates,
( ( ssSkP1455("1")
<=> $true )
& ( ssSkP1455("2")
<=> $false ) ) ).
fof(ssSkP1456,fi_predicates,
( ( ssSkP1456("1")
<=> $true )
& ( ssSkP1456("2")
<=> $false ) ) ).
fof(ssSkP1457,fi_predicates,
( ( ssSkP1457("1")
<=> $true )
& ( ssSkP1457("2")
<=> $false ) ) ).
fof(ssSkP1458,fi_predicates,
( ( ssSkP1458("1")
<=> $true )
& ( ssSkP1458("2")
<=> $false ) ) ).
fof(ssSkP1459,fi_predicates,
( ( ssSkP1459("1")
<=> $true )
& ( ssSkP1459("2")
<=> $false ) ) ).
fof(ssSkP146,fi_predicates,
! [X1] :
( ssSkP146(X1)
<=> $false ) ).
fof(ssSkP1460,fi_predicates,
( ( ssSkP1460("1")
<=> $true )
& ( ssSkP1460("2")
<=> $false ) ) ).
fof(ssSkP1461,fi_predicates,
( ( ssSkP1461("1")
<=> $true )
& ( ssSkP1461("2")
<=> $false ) ) ).
fof(ssSkP1462,fi_predicates,
( ( ssSkP1462("1")
<=> $true )
& ( ssSkP1462("2")
<=> $false ) ) ).
fof(ssSkP1463,fi_predicates,
( ( ssSkP1463("1")
<=> $true )
& ( ssSkP1463("2")
<=> $false ) ) ).
fof(ssSkP1464,fi_predicates,
( ( ssSkP1464("1")
<=> $true )
& ( ssSkP1464("2")
<=> $false ) ) ).
fof(ssSkP1465,fi_predicates,
( ( ssSkP1465("1")
<=> $true )
& ( ssSkP1465("2")
<=> $false ) ) ).
fof(ssSkP1466,fi_predicates,
( ( ssSkP1466("1")
<=> $true )
& ( ssSkP1466("2")
<=> $false ) ) ).
fof(ssSkP1467,fi_predicates,
( ( ssSkP1467("1")
<=> $true )
& ( ssSkP1467("2")
<=> $false ) ) ).
fof(ssSkP1468,fi_predicates,
( ( ssSkP1468("1")
<=> $true )
& ( ssSkP1468("2")
<=> $false ) ) ).
fof(ssSkP1469,fi_predicates,
( ( ssSkP1469("1")
<=> $true )
& ( ssSkP1469("2")
<=> $false ) ) ).
fof(ssSkP147,fi_predicates,
! [X1] :
( ssSkP147(X1)
<=> $false ) ).
fof(ssSkP1470,fi_predicates,
( ( ssSkP1470("1")
<=> $true )
& ( ssSkP1470("2")
<=> $false ) ) ).
fof(ssSkP1471,fi_predicates,
( ( ssSkP1471("1","1")
<=> $true )
& ( ssSkP1471("1","2")
<=> $true )
& ( ssSkP1471("2","1")
<=> $true )
& ( ssSkP1471("2","2")
<=> $true ) ) ).
fof(ssSkP1472,fi_predicates,
( ( ssSkP1472("1")
<=> $true )
& ( ssSkP1472("2")
<=> $true ) ) ).
fof(ssSkP1473,fi_predicates,
( ( ssSkP1473("1")
<=> $true )
& ( ssSkP1473("2")
<=> $true ) ) ).
fof(ssSkP1474,fi_predicates,
( ( ssSkP1474("1")
<=> $true )
& ( ssSkP1474("2")
<=> $true ) ) ).
fof(ssSkP1475,fi_predicates,
( ( ssSkP1475("1")
<=> $true )
& ( ssSkP1475("2")
<=> $false ) ) ).
fof(ssSkP1476,fi_predicates,
( ( ssSkP1476("1")
<=> $true )
& ( ssSkP1476("2")
<=> $false ) ) ).
fof(ssSkP1477,fi_predicates,
( ( ssSkP1477("1")
<=> $true )
& ( ssSkP1477("2")
<=> $true ) ) ).
fof(ssSkP1478,fi_predicates,
( ( ssSkP1478("1")
<=> $true )
& ( ssSkP1478("2")
<=> $false ) ) ).
fof(ssSkP1479,fi_predicates,
( ( ssSkP1479("1")
<=> $true )
& ( ssSkP1479("2")
<=> $false ) ) ).
fof(ssSkP148,fi_predicates,
! [X1] :
( ssSkP148(X1)
<=> $false ) ).
fof(ssSkP1480,fi_predicates,
( ( ssSkP1480("1")
<=> $true )
& ( ssSkP1480("2")
<=> $false ) ) ).
fof(ssSkP1481,fi_predicates,
( ( ssSkP1481("1")
<=> $true )
& ( ssSkP1481("2")
<=> $false ) ) ).
fof(ssSkP1482,fi_predicates,
( ( ssSkP1482("1")
<=> $true )
& ( ssSkP1482("2")
<=> $false ) ) ).
fof(ssSkP1483,fi_predicates,
( ( ssSkP1483("1")
<=> $true )
& ( ssSkP1483("2")
<=> $true ) ) ).
fof(ssSkP1484,fi_predicates,
( ( ssSkP1484("1")
<=> $true )
& ( ssSkP1484("2")
<=> $false ) ) ).
fof(ssSkP1485,fi_predicates,
( ( ssSkP1485("1")
<=> $true )
& ( ssSkP1485("2")
<=> $false ) ) ).
fof(ssSkP1486,fi_predicates,
( ( ssSkP1486("1")
<=> $true )
& ( ssSkP1486("2")
<=> $true ) ) ).
fof(ssSkP1487,fi_predicates,
( ( ssSkP1487("1")
<=> $true )
& ( ssSkP1487("2")
<=> $false ) ) ).
fof(ssSkP1488,fi_predicates,
( ( ssSkP1488("1")
<=> $false )
& ( ssSkP1488("2")
<=> $true ) ) ).
fof(ssSkP1489,fi_predicates,
( ( ssSkP1489("1")
<=> $true )
& ( ssSkP1489("2")
<=> $true ) ) ).
fof(ssSkP149,fi_predicates,
! [X1] :
( ssSkP149(X1)
<=> $false ) ).
fof(ssSkP1490,fi_predicates,
( ( ssSkP1490("1")
<=> $true )
& ( ssSkP1490("2")
<=> $false ) ) ).
fof(ssSkP1491,fi_predicates,
( ( ssSkP1491("1")
<=> $false )
& ( ssSkP1491("2")
<=> $true ) ) ).
fof(ssSkP1492,fi_predicates,
( ( ssSkP1492("1")
<=> $true )
& ( ssSkP1492("2")
<=> $false ) ) ).
fof(ssSkP1493,fi_predicates,
( ( ssSkP1493("1")
<=> $true )
& ( ssSkP1493("2")
<=> $false ) ) ).
fof(ssSkP1494,fi_predicates,
( ( ssSkP1494("1")
<=> $true )
& ( ssSkP1494("2")
<=> $false ) ) ).
fof(ssSkP1495,fi_predicates,
( ( ssSkP1495("1")
<=> $true )
& ( ssSkP1495("2")
<=> $false ) ) ).
fof(ssSkP1496,fi_predicates,
( ( ssSkP1496("1")
<=> $true )
& ( ssSkP1496("2")
<=> $false ) ) ).
fof(ssSkP1497,fi_predicates,
( ( ssSkP1497("1")
<=> $false )
& ( ssSkP1497("2")
<=> $true ) ) ).
fof(ssSkP1498,fi_predicates,
( ( ssSkP1498("1")
<=> $true )
& ( ssSkP1498("2")
<=> $false ) ) ).
fof(ssSkP1499,fi_predicates,
( ( ssSkP1499("1")
<=> $false )
& ( ssSkP1499("2")
<=> $true ) ) ).
fof(ssSkP15,fi_predicates,
! [X1] :
( ssSkP15(X1)
<=> $false ) ).
fof(ssSkP150,fi_predicates,
! [X1] :
( ssSkP150(X1)
<=> $false ) ).
fof(ssSkP1500,fi_predicates,
( ( ssSkP1500("1")
<=> $true )
& ( ssSkP1500("2")
<=> $false ) ) ).
fof(ssSkP1501,fi_predicates,
( ( ssSkP1501("1")
<=> $false )
& ( ssSkP1501("2")
<=> $true ) ) ).
fof(ssSkP1502,fi_predicates,
( ( ssSkP1502("1")
<=> $true )
& ( ssSkP1502("2")
<=> $false ) ) ).
fof(ssSkP1503,fi_predicates,
( ( ssSkP1503("1")
<=> $false )
& ( ssSkP1503("2")
<=> $true ) ) ).
fof(ssSkP1504,fi_predicates,
( ( ssSkP1504("1")
<=> $true )
& ( ssSkP1504("2")
<=> $false ) ) ).
fof(ssSkP1505,fi_predicates,
( ( ssSkP1505("1")
<=> $true )
& ( ssSkP1505("2")
<=> $true ) ) ).
fof(ssSkP1506,fi_predicates,
( ( ssSkP1506("1")
<=> $true )
& ( ssSkP1506("2")
<=> $true ) ) ).
fof(ssSkP1507,fi_predicates,
( ( ssSkP1507("1")
<=> $true )
& ( ssSkP1507("2")
<=> $true ) ) ).
fof(ssSkP1508,fi_predicates,
( ( ssSkP1508("1")
<=> $true )
& ( ssSkP1508("2")
<=> $true ) ) ).
fof(ssSkP1509,fi_predicates,
( ( ssSkP1509("1")
<=> $true )
& ( ssSkP1509("2")
<=> $true ) ) ).
fof(ssSkP151,fi_predicates,
! [X1] :
( ssSkP151(X1)
<=> $false ) ).
fof(ssSkP1510,fi_predicates,
( ( ssSkP1510("1")
<=> $true )
& ( ssSkP1510("2")
<=> $true ) ) ).
fof(ssSkP1511,fi_predicates,
( ( ssSkP1511("1")
<=> $true )
& ( ssSkP1511("2")
<=> $true ) ) ).
fof(ssSkP1512,fi_predicates,
( ( ssSkP1512("1")
<=> $true )
& ( ssSkP1512("2")
<=> $true ) ) ).
fof(ssSkP1513,fi_predicates,
( ( ssSkP1513("1")
<=> $true )
& ( ssSkP1513("2")
<=> $true ) ) ).
fof(ssSkP1514,fi_predicates,
( ( ssSkP1514("1")
<=> $true )
& ( ssSkP1514("2")
<=> $true ) ) ).
fof(ssSkP1515,fi_predicates,
( ( ssSkP1515("1")
<=> $true )
& ( ssSkP1515("2")
<=> $true ) ) ).
fof(ssSkP1516,fi_predicates,
( ( ssSkP1516("1")
<=> $true )
& ( ssSkP1516("2")
<=> $true ) ) ).
fof(ssSkP1517,fi_predicates,
( ( ssSkP1517("1")
<=> $true )
& ( ssSkP1517("2")
<=> $true ) ) ).
fof(ssSkP1518,fi_predicates,
( ( ssSkP1518("1")
<=> $true )
& ( ssSkP1518("2")
<=> $true ) ) ).
fof(ssSkP1519,fi_predicates,
( ( ssSkP1519("1")
<=> $true )
& ( ssSkP1519("2")
<=> $true ) ) ).
fof(ssSkP152,fi_predicates,
! [X1] :
( ssSkP152(X1)
<=> $false ) ).
fof(ssSkP1520,fi_predicates,
( ( ssSkP1520("1")
<=> $true )
& ( ssSkP1520("2")
<=> $true ) ) ).
fof(ssSkP1521,fi_predicates,
( ( ssSkP1521("1")
<=> $true )
& ( ssSkP1521("2")
<=> $true ) ) ).
fof(ssSkP1522,fi_predicates,
( ( ssSkP1522("1")
<=> $true )
& ( ssSkP1522("2")
<=> $true ) ) ).
fof(ssSkP1523,fi_predicates,
( ( ssSkP1523("1")
<=> $true )
& ( ssSkP1523("2")
<=> $true ) ) ).
fof(ssSkP1524,fi_predicates,
( ( ssSkP1524("1")
<=> $true )
& ( ssSkP1524("2")
<=> $true ) ) ).
fof(ssSkP1525,fi_predicates,
( ( ssSkP1525("1")
<=> $true )
& ( ssSkP1525("2")
<=> $true ) ) ).
fof(ssSkP1526,fi_predicates,
( ( ssSkP1526("1")
<=> $true )
& ( ssSkP1526("2")
<=> $true ) ) ).
fof(ssSkP1527,fi_predicates,
( ( ssSkP1527("1")
<=> $true )
& ( ssSkP1527("2")
<=> $true ) ) ).
fof(ssSkP1528,fi_predicates,
( ( ssSkP1528("1")
<=> $true )
& ( ssSkP1528("2")
<=> $true ) ) ).
fof(ssSkP1529,fi_predicates,
( ( ssSkP1529("1")
<=> $true )
& ( ssSkP1529("2")
<=> $true ) ) ).
fof(ssSkP153,fi_predicates,
! [X1] :
( ssSkP153(X1)
<=> $false ) ).
fof(ssSkP1530,fi_predicates,
( ( ssSkP1530("1")
<=> $true )
& ( ssSkP1530("2")
<=> $true ) ) ).
fof(ssSkP1531,fi_predicates,
( ( ssSkP1531("1")
<=> $true )
& ( ssSkP1531("2")
<=> $true ) ) ).
fof(ssSkP1532,fi_predicates,
( ( ssSkP1532("1")
<=> $true )
& ( ssSkP1532("2")
<=> $true ) ) ).
fof(ssSkP1533,fi_predicates,
( ( ssSkP1533("1")
<=> $true )
& ( ssSkP1533("2")
<=> $true ) ) ).
fof(ssSkP1534,fi_predicates,
( ( ssSkP1534("1")
<=> $true )
& ( ssSkP1534("2")
<=> $true ) ) ).
fof(ssSkP1535,fi_predicates,
( ( ssSkP1535("1")
<=> $true )
& ( ssSkP1535("2")
<=> $true ) ) ).
fof(ssSkP1536,fi_predicates,
( ( ssSkP1536("1")
<=> $true )
& ( ssSkP1536("2")
<=> $true ) ) ).
fof(ssSkP1537,fi_predicates,
( ( ssSkP1537("1")
<=> $true )
& ( ssSkP1537("2")
<=> $true ) ) ).
fof(ssSkP1538,fi_predicates,
( ( ssSkP1538("1")
<=> $true )
& ( ssSkP1538("2")
<=> $true ) ) ).
fof(ssSkP1539,fi_predicates,
( ( ssSkP1539("1")
<=> $true )
& ( ssSkP1539("2")
<=> $true ) ) ).
fof(ssSkP154,fi_predicates,
! [X1] :
( ssSkP154(X1)
<=> $true ) ).
fof(ssSkP1540,fi_predicates,
( ( ssSkP1540("1")
<=> $true )
& ( ssSkP1540("2")
<=> $true ) ) ).
fof(ssSkP1541,fi_predicates,
( ( ssSkP1541("1")
<=> $true )
& ( ssSkP1541("2")
<=> $true ) ) ).
fof(ssSkP1542,fi_predicates,
( ( ssSkP1542("1")
<=> $true )
& ( ssSkP1542("2")
<=> $true ) ) ).
fof(ssSkP1543,fi_predicates,
( ( ssSkP1543("1")
<=> $true )
& ( ssSkP1543("2")
<=> $true ) ) ).
fof(ssSkP1544,fi_predicates,
( ( ssSkP1544("1")
<=> $true )
& ( ssSkP1544("2")
<=> $true ) ) ).
fof(ssSkP1545,fi_predicates,
( ( ssSkP1545("1")
<=> $true )
& ( ssSkP1545("2")
<=> $true ) ) ).
fof(ssSkP1546,fi_predicates,
( ( ssSkP1546("1")
<=> $true )
& ( ssSkP1546("2")
<=> $true ) ) ).
fof(ssSkP1547,fi_predicates,
( ( ssSkP1547("1")
<=> $true )
& ( ssSkP1547("2")
<=> $true ) ) ).
fof(ssSkP1548,fi_predicates,
( ( ssSkP1548("1")
<=> $true )
& ( ssSkP1548("2")
<=> $true ) ) ).
fof(ssSkP1549,fi_predicates,
( ( ssSkP1549("1")
<=> $true )
& ( ssSkP1549("2")
<=> $true ) ) ).
fof(ssSkP155,fi_predicates,
! [X1] :
( ssSkP155(X1)
<=> $true ) ).
fof(ssSkP1550,fi_predicates,
( ( ssSkP1550("1")
<=> $true )
& ( ssSkP1550("2")
<=> $true ) ) ).
fof(ssSkP1551,fi_predicates,
( ( ssSkP1551("1")
<=> $true )
& ( ssSkP1551("2")
<=> $true ) ) ).
fof(ssSkP1552,fi_predicates,
( ( ssSkP1552("1")
<=> $true )
& ( ssSkP1552("2")
<=> $true ) ) ).
fof(ssSkP1553,fi_predicates,
( ( ssSkP1553("1")
<=> $true )
& ( ssSkP1553("2")
<=> $true ) ) ).
fof(ssSkP1554,fi_predicates,
( ( ssSkP1554("1")
<=> $true )
& ( ssSkP1554("2")
<=> $true ) ) ).
fof(ssSkP1555,fi_predicates,
( ( ssSkP1555("1")
<=> $true )
& ( ssSkP1555("2")
<=> $true ) ) ).
fof(ssSkP1556,fi_predicates,
( ( ssSkP1556("1")
<=> $true )
& ( ssSkP1556("2")
<=> $true ) ) ).
fof(ssSkP1557,fi_predicates,
( ( ssSkP1557("1")
<=> $true )
& ( ssSkP1557("2")
<=> $true ) ) ).
fof(ssSkP1558,fi_predicates,
( ( ssSkP1558("1")
<=> $true )
& ( ssSkP1558("2")
<=> $true ) ) ).
fof(ssSkP1559,fi_predicates,
( ( ssSkP1559("1")
<=> $true )
& ( ssSkP1559("2")
<=> $true ) ) ).
fof(ssSkP156,fi_predicates,
! [X1,X2] :
( ssSkP156(X1,X2)
<=> $true ) ).
fof(ssSkP1560,fi_predicates,
( ( ssSkP1560("1")
<=> $true )
& ( ssSkP1560("2")
<=> $true ) ) ).
fof(ssSkP1561,fi_predicates,
( ( ssSkP1561("1")
<=> $true )
& ( ssSkP1561("2")
<=> $true ) ) ).
fof(ssSkP1562,fi_predicates,
( ( ssSkP1562("1")
<=> $true )
& ( ssSkP1562("2")
<=> $true ) ) ).
fof(ssSkP1563,fi_predicates,
( ( ssSkP1563("1")
<=> $true )
& ( ssSkP1563("2")
<=> $true ) ) ).
fof(ssSkP1564,fi_predicates,
( ( ssSkP1564("1")
<=> $true )
& ( ssSkP1564("2")
<=> $true ) ) ).
fof(ssSkP1565,fi_predicates,
( ( ssSkP1565("1")
<=> $true )
& ( ssSkP1565("2")
<=> $true ) ) ).
fof(ssSkP1566,fi_predicates,
( ( ssSkP1566("1")
<=> $true )
& ( ssSkP1566("2")
<=> $true ) ) ).
fof(ssSkP1567,fi_predicates,
( ( ssSkP1567("1")
<=> $true )
& ( ssSkP1567("2")
<=> $true ) ) ).
fof(ssSkP1568,fi_predicates,
( ( ssSkP1568("1")
<=> $true )
& ( ssSkP1568("2")
<=> $true ) ) ).
fof(ssSkP1569,fi_predicates,
( ( ssSkP1569("1")
<=> $true )
& ( ssSkP1569("2")
<=> $true ) ) ).
fof(ssSkP157,fi_predicates,
! [X1,X2] :
( ssSkP157(X1,X2)
<=> $true ) ).
fof(ssSkP1570,fi_predicates,
( ( ssSkP1570("1")
<=> $true )
& ( ssSkP1570("2")
<=> $true ) ) ).
fof(ssSkP1571,fi_predicates,
( ( ssSkP1571("1")
<=> $true )
& ( ssSkP1571("2")
<=> $true ) ) ).
fof(ssSkP1572,fi_predicates,
( ( ssSkP1572("1")
<=> $true )
& ( ssSkP1572("2")
<=> $true ) ) ).
fof(ssSkP1573,fi_predicates,
( ( ssSkP1573("1")
<=> $true )
& ( ssSkP1573("2")
<=> $true ) ) ).
fof(ssSkP1574,fi_predicates,
( ( ssSkP1574("1")
<=> $true )
& ( ssSkP1574("2")
<=> $true ) ) ).
fof(ssSkP1575,fi_predicates,
( ( ssSkP1575("1")
<=> $true )
& ( ssSkP1575("2")
<=> $true ) ) ).
fof(ssSkP1576,fi_predicates,
( ( ssSkP1576("1")
<=> $true )
& ( ssSkP1576("2")
<=> $true ) ) ).
fof(ssSkP1577,fi_predicates,
( ( ssSkP1577("1")
<=> $true )
& ( ssSkP1577("2")
<=> $true ) ) ).
fof(ssSkP1578,fi_predicates,
( ( ssSkP1578("1")
<=> $true )
& ( ssSkP1578("2")
<=> $true ) ) ).
fof(ssSkP1579,fi_predicates,
( ( ssSkP1579("1")
<=> $true )
& ( ssSkP1579("2")
<=> $true ) ) ).
fof(ssSkP158,fi_predicates,
! [X1] :
( ssSkP158(X1)
<=> $false ) ).
fof(ssSkP1580,fi_predicates,
( ( ssSkP1580("1")
<=> $true )
& ( ssSkP1580("2")
<=> $true ) ) ).
fof(ssSkP1581,fi_predicates,
( ( ssSkP1581("1")
<=> $true )
& ( ssSkP1581("2")
<=> $true ) ) ).
fof(ssSkP1582,fi_predicates,
( ( ssSkP1582("1")
<=> $true )
& ( ssSkP1582("2")
<=> $true ) ) ).
fof(ssSkP1583,fi_predicates,
( ( ssSkP1583("1")
<=> $true )
& ( ssSkP1583("2")
<=> $true ) ) ).
fof(ssSkP1584,fi_predicates,
( ( ssSkP1584("1")
<=> $true )
& ( ssSkP1584("2")
<=> $true ) ) ).
fof(ssSkP1585,fi_predicates,
( ( ssSkP1585("1")
<=> $true )
& ( ssSkP1585("2")
<=> $true ) ) ).
fof(ssSkP1586,fi_predicates,
( ( ssSkP1586("1")
<=> $true )
& ( ssSkP1586("2")
<=> $true ) ) ).
fof(ssSkP1587,fi_predicates,
( ( ssSkP1587("1")
<=> $true )
& ( ssSkP1587("2")
<=> $true ) ) ).
fof(ssSkP1588,fi_predicates,
( ( ssSkP1588("1")
<=> $true )
& ( ssSkP1588("2")
<=> $true ) ) ).
fof(ssSkP1589,fi_predicates,
( ( ssSkP1589("1")
<=> $true )
& ( ssSkP1589("2")
<=> $true ) ) ).
fof(ssSkP159,fi_predicates,
! [X1] :
( ssSkP159(X1)
<=> $false ) ).
fof(ssSkP1590,fi_predicates,
( ( ssSkP1590("1")
<=> $true )
& ( ssSkP1590("2")
<=> $true ) ) ).
fof(ssSkP1591,fi_predicates,
( ( ssSkP1591("1")
<=> $true )
& ( ssSkP1591("2")
<=> $true ) ) ).
fof(ssSkP1592,fi_predicates,
( ( ssSkP1592("1")
<=> $true )
& ( ssSkP1592("2")
<=> $true ) ) ).
fof(ssSkP1593,fi_predicates,
( ( ssSkP1593("1")
<=> $true )
& ( ssSkP1593("2")
<=> $true ) ) ).
fof(ssSkP1594,fi_predicates,
( ( ssSkP1594("1")
<=> $true )
& ( ssSkP1594("2")
<=> $false ) ) ).
fof(ssSkP1595,fi_predicates,
( ( ssSkP1595("1")
<=> $true )
& ( ssSkP1595("2")
<=> $false ) ) ).
fof(ssSkP16,fi_predicates,
! [X1] :
( ssSkP16(X1)
<=> $true ) ).
fof(ssSkP160,fi_predicates,
! [X1] :
( ssSkP160(X1)
<=> $false ) ).
fof(ssSkP161,fi_predicates,
! [X1] :
( ssSkP161(X1)
<=> $false ) ).
fof(ssSkP162,fi_predicates,
! [X1] :
( ssSkP162(X1)
<=> $false ) ).
fof(ssSkP163,fi_predicates,
! [X1] :
( ssSkP163(X1)
<=> $false ) ).
fof(ssSkP164,fi_predicates,
! [X1] :
( ssSkP164(X1)
<=> $false ) ).
fof(ssSkP165,fi_predicates,
! [X1] :
( ssSkP165(X1)
<=> $false ) ).
fof(ssSkP166,fi_predicates,
! [X1] :
( ssSkP166(X1)
<=> $false ) ).
fof(ssSkP167,fi_predicates,
! [X1] :
( ssSkP167(X1)
<=> $false ) ).
fof(ssSkP168,fi_predicates,
! [X1] :
( ssSkP168(X1)
<=> $false ) ).
fof(ssSkP169,fi_predicates,
! [X1] :
( ssSkP169(X1)
<=> $false ) ).
fof(ssSkP17,fi_predicates,
! [X1] :
( ssSkP17(X1)
<=> $true ) ).
fof(ssSkP170,fi_predicates,
! [X1] :
( ssSkP170(X1)
<=> $false ) ).
fof(ssSkP171,fi_predicates,
! [X1] :
( ssSkP171(X1)
<=> $false ) ).
fof(ssSkP172,fi_predicates,
! [X1] :
( ssSkP172(X1)
<=> $false ) ).
fof(ssSkP173,fi_predicates,
! [X1] :
( ssSkP173(X1)
<=> $false ) ).
fof(ssSkP174,fi_predicates,
! [X1] :
( ssSkP174(X1)
<=> $false ) ).
fof(ssSkP175,fi_predicates,
! [X1] :
( ssSkP175(X1)
<=> $false ) ).
fof(ssSkP176,fi_predicates,
! [X1] :
( ssSkP176(X1)
<=> $false ) ).
fof(ssSkP177,fi_predicates,
! [X1] :
( ssSkP177(X1)
<=> $false ) ).
fof(ssSkP178,fi_predicates,
! [X1] :
( ssSkP178(X1)
<=> $false ) ).
fof(ssSkP179,fi_predicates,
! [X1] :
( ssSkP179(X1)
<=> $false ) ).
fof(ssSkP18,fi_predicates,
! [X1] :
( ssSkP18(X1)
<=> $true ) ).
fof(ssSkP180,fi_predicates,
! [X1] :
( ssSkP180(X1)
<=> $false ) ).
fof(ssSkP181,fi_predicates,
! [X1] :
( ssSkP181(X1)
<=> $false ) ).
fof(ssSkP182,fi_predicates,
! [X1] :
( ssSkP182(X1)
<=> $false ) ).
fof(ssSkP183,fi_predicates,
! [X1] :
( ssSkP183(X1)
<=> $false ) ).
fof(ssSkP184,fi_predicates,
! [X1] :
( ssSkP184(X1)
<=> $false ) ).
fof(ssSkP185,fi_predicates,
! [X1] :
( ssSkP185(X1)
<=> $false ) ).
fof(ssSkP186,fi_predicates,
! [X1] :
( ssSkP186(X1)
<=> $true ) ).
fof(ssSkP187,fi_predicates,
! [X1] :
( ssSkP187(X1)
<=> $true ) ).
fof(ssSkP188,fi_predicates,
! [X1] :
( ssSkP188(X1)
<=> $true ) ).
fof(ssSkP189,fi_predicates,
! [X1,X2] :
( ssSkP189(X1,X2)
<=> $true ) ).
fof(ssSkP19,fi_predicates,
! [X1] :
( ssSkP19(X1)
<=> $true ) ).
fof(ssSkP190,fi_predicates,
! [X1,X2] :
( ssSkP190(X1,X2)
<=> $true ) ).
fof(ssSkP191,fi_predicates,
! [X1] :
( ssSkP191(X1)
<=> $true ) ).
fof(ssSkP192,fi_predicates,
! [X1] :
( ssSkP192(X1)
<=> $true ) ).
fof(ssSkP193,fi_predicates,
! [X1] :
( ssSkP193(X1)
<=> $true ) ).
fof(ssSkP194,fi_predicates,
! [X1] :
( ssSkP194(X1)
<=> $true ) ).
fof(ssSkP195,fi_predicates,
! [X1] :
( ssSkP195(X1)
<=> $true ) ).
fof(ssSkP196,fi_predicates,
! [X1] :
( ssSkP196(X1)
<=> $true ) ).
fof(ssSkP197,fi_predicates,
! [X1] :
( ssSkP197(X1)
<=> $true ) ).
fof(ssSkP198,fi_predicates,
! [X1] :
( ssSkP198(X1)
<=> $true ) ).
fof(ssSkP199,fi_predicates,
! [X1] :
( ssSkP199(X1)
<=> $true ) ).
fof(ssSkP2,fi_predicates,
! [X1] :
( ssSkP2(X1)
<=> $false ) ).
fof(ssSkP20,fi_predicates,
! [X1,X2] :
( ssSkP20(X1,X2)
<=> $true ) ).
fof(ssSkP200,fi_predicates,
! [X1] :
( ssSkP200(X1)
<=> $true ) ).
fof(ssSkP201,fi_predicates,
! [X1] :
( ssSkP201(X1)
<=> $true ) ).
fof(ssSkP202,fi_predicates,
! [X1] :
( ssSkP202(X1)
<=> $true ) ).
fof(ssSkP203,fi_predicates,
! [X1] :
( ssSkP203(X1)
<=> $true ) ).
fof(ssSkP204,fi_predicates,
! [X1] :
( ssSkP204(X1)
<=> $true ) ).
fof(ssSkP205,fi_predicates,
! [X1] :
( ssSkP205(X1)
<=> $true ) ).
fof(ssSkP206,fi_predicates,
! [X1] :
( ssSkP206(X1)
<=> $true ) ).
fof(ssSkP207,fi_predicates,
! [X1] :
( ssSkP207(X1)
<=> $true ) ).
fof(ssSkP208,fi_predicates,
! [X1] :
( ssSkP208(X1)
<=> $true ) ).
fof(ssSkP209,fi_predicates,
! [X1] :
( ssSkP209(X1)
<=> $true ) ).
fof(ssSkP21,fi_predicates,
! [X1,X2] :
( ssSkP21(X1,X2)
<=> $true ) ).
fof(ssSkP210,fi_predicates,
! [X1] :
( ssSkP210(X1)
<=> $true ) ).
fof(ssSkP211,fi_predicates,
! [X1] :
( ssSkP211(X1)
<=> $true ) ).
fof(ssSkP212,fi_predicates,
! [X1] :
( ssSkP212(X1)
<=> $true ) ).
fof(ssSkP213,fi_predicates,
! [X1] :
( ssSkP213(X1)
<=> $true ) ).
fof(ssSkP214,fi_predicates,
! [X1] :
( ssSkP214(X1)
<=> $true ) ).
fof(ssSkP215,fi_predicates,
! [X1] :
( ssSkP215(X1)
<=> $true ) ).
fof(ssSkP216,fi_predicates,
! [X1] :
( ssSkP216(X1)
<=> $true ) ).
fof(ssSkP217,fi_predicates,
! [X1] :
( ssSkP217(X1)
<=> $true ) ).
fof(ssSkP218,fi_predicates,
! [X1] :
( ssSkP218(X1)
<=> $true ) ).
fof(ssSkP219,fi_predicates,
! [X1] :
( ssSkP219(X1)
<=> $true ) ).
fof(ssSkP22,fi_predicates,
! [X1] :
( ssSkP22(X1)
<=> $false ) ).
fof(ssSkP220,fi_predicates,
! [X1] :
( ssSkP220(X1)
<=> $true ) ).
fof(ssSkP221,fi_predicates,
! [X1] :
( ssSkP221(X1)
<=> $true ) ).
fof(ssSkP222,fi_predicates,
! [X1] :
( ssSkP222(X1)
<=> $true ) ).
fof(ssSkP223,fi_predicates,
! [X1] :
( ssSkP223(X1)
<=> $true ) ).
fof(ssSkP224,fi_predicates,
! [X1] :
( ssSkP224(X1)
<=> $true ) ).
fof(ssSkP225,fi_predicates,
! [X1] :
( ssSkP225(X1)
<=> $true ) ).
fof(ssSkP226,fi_predicates,
! [X1] :
( ssSkP226(X1)
<=> $true ) ).
fof(ssSkP227,fi_predicates,
! [X1] :
( ssSkP227(X1)
<=> $true ) ).
fof(ssSkP228,fi_predicates,
! [X1] :
( ssSkP228(X1)
<=> $true ) ).
fof(ssSkP229,fi_predicates,
! [X1,X2] :
( ssSkP229(X1,X2)
<=> $true ) ).
fof(ssSkP23,fi_predicates,
! [X1] :
( ssSkP23(X1)
<=> $false ) ).
fof(ssSkP230,fi_predicates,
! [X1,X2] :
( ssSkP230(X1,X2)
<=> $true ) ).
fof(ssSkP231,fi_predicates,
! [X1] :
( ssSkP231(X1)
<=> $false ) ).
fof(ssSkP232,fi_predicates,
! [X1] :
( ssSkP232(X1)
<=> $false ) ).
fof(ssSkP233,fi_predicates,
! [X1] :
( ssSkP233(X1)
<=> $false ) ).
fof(ssSkP234,fi_predicates,
! [X1] :
( ssSkP234(X1)
<=> $false ) ).
fof(ssSkP235,fi_predicates,
! [X1] :
( ssSkP235(X1)
<=> $false ) ).
fof(ssSkP236,fi_predicates,
! [X1] :
( ssSkP236(X1)
<=> $false ) ).
fof(ssSkP237,fi_predicates,
! [X1] :
( ssSkP237(X1)
<=> $false ) ).
fof(ssSkP238,fi_predicates,
! [X1] :
( ssSkP238(X1)
<=> $false ) ).
fof(ssSkP239,fi_predicates,
! [X1] :
( ssSkP239(X1)
<=> $false ) ).
fof(ssSkP24,fi_predicates,
! [X1] :
( ssSkP24(X1)
<=> $false ) ).
fof(ssSkP240,fi_predicates,
! [X1] :
( ssSkP240(X1)
<=> $false ) ).
fof(ssSkP241,fi_predicates,
! [X1] :
( ssSkP241(X1)
<=> $false ) ).
fof(ssSkP242,fi_predicates,
! [X1] :
( ssSkP242(X1)
<=> $false ) ).
fof(ssSkP243,fi_predicates,
! [X1] :
( ssSkP243(X1)
<=> $false ) ).
fof(ssSkP244,fi_predicates,
! [X1] :
( ssSkP244(X1)
<=> $false ) ).
fof(ssSkP245,fi_predicates,
! [X1] :
( ssSkP245(X1)
<=> $false ) ).
fof(ssSkP246,fi_predicates,
! [X1] :
( ssSkP246(X1)
<=> $false ) ).
fof(ssSkP247,fi_predicates,
! [X1] :
( ssSkP247(X1)
<=> $false ) ).
fof(ssSkP248,fi_predicates,
! [X1] :
( ssSkP248(X1)
<=> $false ) ).
fof(ssSkP249,fi_predicates,
! [X1] :
( ssSkP249(X1)
<=> $false ) ).
fof(ssSkP25,fi_predicates,
! [X1] :
( ssSkP25(X1)
<=> $false ) ).
fof(ssSkP250,fi_predicates,
! [X1] :
( ssSkP250(X1)
<=> $false ) ).
fof(ssSkP251,fi_predicates,
! [X1] :
( ssSkP251(X1)
<=> $false ) ).
fof(ssSkP252,fi_predicates,
! [X1] :
( ssSkP252(X1)
<=> $false ) ).
fof(ssSkP253,fi_predicates,
! [X1] :
( ssSkP253(X1)
<=> $false ) ).
fof(ssSkP254,fi_predicates,
! [X1] :
( ssSkP254(X1)
<=> $false ) ).
fof(ssSkP255,fi_predicates,
! [X1] :
( ssSkP255(X1)
<=> $false ) ).
fof(ssSkP256,fi_predicates,
! [X1] :
( ssSkP256(X1)
<=> $false ) ).
fof(ssSkP257,fi_predicates,
! [X1] :
( ssSkP257(X1)
<=> $false ) ).
fof(ssSkP258,fi_predicates,
! [X1] :
( ssSkP258(X1)
<=> $false ) ).
fof(ssSkP259,fi_predicates,
! [X1] :
( ssSkP259(X1)
<=> $false ) ).
fof(ssSkP26,fi_predicates,
! [X1] :
( ssSkP26(X1)
<=> $false ) ).
fof(ssSkP260,fi_predicates,
! [X1] :
( ssSkP260(X1)
<=> $true ) ).
fof(ssSkP261,fi_predicates,
! [X1] :
( ssSkP261(X1)
<=> $true ) ).
fof(ssSkP262,fi_predicates,
! [X1] :
( ssSkP262(X1)
<=> $true ) ).
fof(ssSkP263,fi_predicates,
! [X1] :
( ssSkP263(X1)
<=> $true ) ).
fof(ssSkP264,fi_predicates,
! [X1,X2] :
( ssSkP264(X1,X2)
<=> $true ) ).
fof(ssSkP265,fi_predicates,
! [X1,X2] :
( ssSkP265(X1,X2)
<=> $true ) ).
fof(ssSkP266,fi_predicates,
! [X1] :
( ssSkP266(X1)
<=> $false ) ).
fof(ssSkP267,fi_predicates,
! [X1] :
( ssSkP267(X1)
<=> $false ) ).
fof(ssSkP268,fi_predicates,
! [X1] :
( ssSkP268(X1)
<=> $false ) ).
fof(ssSkP269,fi_predicates,
! [X1] :
( ssSkP269(X1)
<=> $false ) ).
fof(ssSkP27,fi_predicates,
! [X1] :
( ssSkP27(X1)
<=> $false ) ).
fof(ssSkP270,fi_predicates,
! [X1] :
( ssSkP270(X1)
<=> $false ) ).
fof(ssSkP271,fi_predicates,
! [X1] :
( ssSkP271(X1)
<=> $false ) ).
fof(ssSkP272,fi_predicates,
! [X1] :
( ssSkP272(X1)
<=> $false ) ).
fof(ssSkP273,fi_predicates,
! [X1] :
( ssSkP273(X1)
<=> $false ) ).
fof(ssSkP274,fi_predicates,
! [X1] :
( ssSkP274(X1)
<=> $false ) ).
fof(ssSkP275,fi_predicates,
! [X1] :
( ssSkP275(X1)
<=> $false ) ).
fof(ssSkP276,fi_predicates,
! [X1] :
( ssSkP276(X1)
<=> $false ) ).
fof(ssSkP277,fi_predicates,
! [X1] :
( ssSkP277(X1)
<=> $false ) ).
fof(ssSkP278,fi_predicates,
! [X1] :
( ssSkP278(X1)
<=> $false ) ).
fof(ssSkP279,fi_predicates,
! [X1] :
( ssSkP279(X1)
<=> $false ) ).
fof(ssSkP28,fi_predicates,
! [X1] :
( ssSkP28(X1)
<=> $false ) ).
fof(ssSkP280,fi_predicates,
! [X1] :
( ssSkP280(X1)
<=> $false ) ).
fof(ssSkP281,fi_predicates,
! [X1] :
( ssSkP281(X1)
<=> $false ) ).
fof(ssSkP282,fi_predicates,
! [X1] :
( ssSkP282(X1)
<=> $false ) ).
fof(ssSkP283,fi_predicates,
! [X1] :
( ssSkP283(X1)
<=> $true ) ).
fof(ssSkP284,fi_predicates,
! [X1] :
( ssSkP284(X1)
<=> $true ) ).
fof(ssSkP285,fi_predicates,
! [X1] :
( ssSkP285(X1)
<=> $true ) ).
fof(ssSkP286,fi_predicates,
! [X1] :
( ssSkP286(X1)
<=> $true ) ).
fof(ssSkP287,fi_predicates,
! [X1,X2] :
( ssSkP287(X1,X2)
<=> $true ) ).
fof(ssSkP288,fi_predicates,
! [X1,X2] :
( ssSkP288(X1,X2)
<=> $true ) ).
fof(ssSkP289,fi_predicates,
! [X1] :
( ssSkP289(X1)
<=> $true ) ).
fof(ssSkP29,fi_predicates,
! [X1] :
( ssSkP29(X1)
<=> $false ) ).
fof(ssSkP290,fi_predicates,
! [X1] :
( ssSkP290(X1)
<=> $true ) ).
fof(ssSkP291,fi_predicates,
! [X1] :
( ssSkP291(X1)
<=> $true ) ).
fof(ssSkP292,fi_predicates,
! [X1] :
( ssSkP292(X1)
<=> $true ) ).
fof(ssSkP293,fi_predicates,
! [X1] :
( ssSkP293(X1)
<=> $true ) ).
fof(ssSkP294,fi_predicates,
! [X1] :
( ssSkP294(X1)
<=> $true ) ).
fof(ssSkP295,fi_predicates,
! [X1] :
( ssSkP295(X1)
<=> $true ) ).
fof(ssSkP296,fi_predicates,
! [X1] :
( ssSkP296(X1)
<=> $true ) ).
fof(ssSkP297,fi_predicates,
! [X1] :
( ssSkP297(X1)
<=> $true ) ).
fof(ssSkP298,fi_predicates,
! [X1] :
( ssSkP298(X1)
<=> $true ) ).
fof(ssSkP299,fi_predicates,
! [X1] :
( ssSkP299(X1)
<=> $true ) ).
fof(ssSkP3,fi_predicates,
! [X1] :
( ssSkP3(X1)
<=> $false ) ).
fof(ssSkP30,fi_predicates,
! [X1] :
( ssSkP30(X1)
<=> $false ) ).
fof(ssSkP300,fi_predicates,
! [X1] :
( ssSkP300(X1)
<=> $true ) ).
fof(ssSkP301,fi_predicates,
! [X1] :
( ssSkP301(X1)
<=> $true ) ).
fof(ssSkP302,fi_predicates,
! [X1] :
( ssSkP302(X1)
<=> $true ) ).
fof(ssSkP303,fi_predicates,
! [X1] :
( ssSkP303(X1)
<=> $true ) ).
fof(ssSkP304,fi_predicates,
! [X1] :
( ssSkP304(X1)
<=> $true ) ).
fof(ssSkP305,fi_predicates,
! [X1] :
( ssSkP305(X1)
<=> $true ) ).
fof(ssSkP306,fi_predicates,
! [X1] :
( ssSkP306(X1)
<=> $true ) ).
fof(ssSkP307,fi_predicates,
! [X1] :
( ssSkP307(X1)
<=> $true ) ).
fof(ssSkP308,fi_predicates,
! [X1] :
( ssSkP308(X1)
<=> $true ) ).
fof(ssSkP309,fi_predicates,
! [X1] :
( ssSkP309(X1)
<=> $true ) ).
fof(ssSkP31,fi_predicates,
! [X1] :
( ssSkP31(X1)
<=> $false ) ).
fof(ssSkP310,fi_predicates,
! [X1] :
( ssSkP310(X1)
<=> $true ) ).
fof(ssSkP311,fi_predicates,
! [X1] :
( ssSkP311(X1)
<=> $true ) ).
fof(ssSkP312,fi_predicates,
! [X1] :
( ssSkP312(X1)
<=> $true ) ).
fof(ssSkP313,fi_predicates,
! [X1] :
( ssSkP313(X1)
<=> $true ) ).
fof(ssSkP314,fi_predicates,
! [X1] :
( ssSkP314(X1)
<=> $true ) ).
fof(ssSkP315,fi_predicates,
! [X1] :
( ssSkP315(X1)
<=> $true ) ).
fof(ssSkP316,fi_predicates,
! [X1] :
( ssSkP316(X1)
<=> $true ) ).
fof(ssSkP317,fi_predicates,
! [X1] :
( ssSkP317(X1)
<=> $true ) ).
fof(ssSkP318,fi_predicates,
! [X1] :
( ssSkP318(X1)
<=> $true ) ).
fof(ssSkP319,fi_predicates,
! [X1] :
( ssSkP319(X1)
<=> $true ) ).
fof(ssSkP32,fi_predicates,
! [X1] :
( ssSkP32(X1)
<=> $false ) ).
fof(ssSkP320,fi_predicates,
! [X1] :
( ssSkP320(X1)
<=> $true ) ).
fof(ssSkP321,fi_predicates,
! [X1] :
( ssSkP321(X1)
<=> $true ) ).
fof(ssSkP322,fi_predicates,
! [X1] :
( ssSkP322(X1)
<=> $true ) ).
fof(ssSkP323,fi_predicates,
! [X1] :
( ssSkP323(X1)
<=> $true ) ).
fof(ssSkP324,fi_predicates,
! [X1] :
( ssSkP324(X1)
<=> $true ) ).
fof(ssSkP325,fi_predicates,
! [X1,X2] :
( ssSkP325(X1,X2)
<=> $true ) ).
fof(ssSkP326,fi_predicates,
! [X1,X2] :
( ssSkP326(X1,X2)
<=> $true ) ).
fof(ssSkP327,fi_predicates,
! [X1] :
( ssSkP327(X1)
<=> $true ) ).
fof(ssSkP328,fi_predicates,
! [X1] :
( ssSkP328(X1)
<=> $true ) ).
fof(ssSkP329,fi_predicates,
! [X1] :
( ssSkP329(X1)
<=> $true ) ).
fof(ssSkP33,fi_predicates,
! [X1] :
( ssSkP33(X1)
<=> $false ) ).
fof(ssSkP330,fi_predicates,
! [X1] :
( ssSkP330(X1)
<=> $true ) ).
fof(ssSkP331,fi_predicates,
! [X1] :
( ssSkP331(X1)
<=> $true ) ).
fof(ssSkP332,fi_predicates,
! [X1] :
( ssSkP332(X1)
<=> $true ) ).
fof(ssSkP333,fi_predicates,
! [X1] :
( ssSkP333(X1)
<=> $true ) ).
fof(ssSkP334,fi_predicates,
! [X1] :
( ssSkP334(X1)
<=> $true ) ).
fof(ssSkP335,fi_predicates,
! [X1] :
( ssSkP335(X1)
<=> $true ) ).
fof(ssSkP336,fi_predicates,
! [X1] :
( ssSkP336(X1)
<=> $true ) ).
fof(ssSkP337,fi_predicates,
! [X1] :
( ssSkP337(X1)
<=> $true ) ).
fof(ssSkP338,fi_predicates,
! [X1] :
( ssSkP338(X1)
<=> $true ) ).
fof(ssSkP339,fi_predicates,
! [X1] :
( ssSkP339(X1)
<=> $true ) ).
fof(ssSkP34,fi_predicates,
! [X1] :
( ssSkP34(X1)
<=> $false ) ).
fof(ssSkP340,fi_predicates,
! [X1] :
( ssSkP340(X1)
<=> $true ) ).
fof(ssSkP341,fi_predicates,
! [X1] :
( ssSkP341(X1)
<=> $true ) ).
fof(ssSkP342,fi_predicates,
! [X1] :
( ssSkP342(X1)
<=> $true ) ).
fof(ssSkP343,fi_predicates,
! [X1] :
( ssSkP343(X1)
<=> $true ) ).
fof(ssSkP344,fi_predicates,
! [X1] :
( ssSkP344(X1)
<=> $true ) ).
fof(ssSkP345,fi_predicates,
! [X1] :
( ssSkP345(X1)
<=> $true ) ).
fof(ssSkP346,fi_predicates,
! [X1] :
( ssSkP346(X1)
<=> $true ) ).
fof(ssSkP347,fi_predicates,
! [X1] :
( ssSkP347(X1)
<=> $true ) ).
fof(ssSkP348,fi_predicates,
! [X1] :
( ssSkP348(X1)
<=> $true ) ).
fof(ssSkP349,fi_predicates,
! [X1] :
( ssSkP349(X1)
<=> $true ) ).
fof(ssSkP35,fi_predicates,
! [X1] :
( ssSkP35(X1)
<=> $false ) ).
fof(ssSkP350,fi_predicates,
! [X1] :
( ssSkP350(X1)
<=> $true ) ).
fof(ssSkP351,fi_predicates,
! [X1] :
( ssSkP351(X1)
<=> $true ) ).
fof(ssSkP352,fi_predicates,
! [X1] :
( ssSkP352(X1)
<=> $true ) ).
fof(ssSkP353,fi_predicates,
! [X1] :
( ssSkP353(X1)
<=> $true ) ).
fof(ssSkP354,fi_predicates,
! [X1] :
( ssSkP354(X1)
<=> $true ) ).
fof(ssSkP355,fi_predicates,
! [X1] :
( ssSkP355(X1)
<=> $true ) ).
fof(ssSkP356,fi_predicates,
! [X1] :
( ssSkP356(X1)
<=> $true ) ).
fof(ssSkP357,fi_predicates,
! [X1] :
( ssSkP357(X1)
<=> $true ) ).
fof(ssSkP358,fi_predicates,
! [X1] :
( ssSkP358(X1)
<=> $true ) ).
fof(ssSkP359,fi_predicates,
! [X1] :
( ssSkP359(X1)
<=> $true ) ).
fof(ssSkP36,fi_predicates,
! [X1] :
( ssSkP36(X1)
<=> $false ) ).
fof(ssSkP360,fi_predicates,
! [X1] :
( ssSkP360(X1)
<=> $true ) ).
fof(ssSkP361,fi_predicates,
! [X1] :
( ssSkP361(X1)
<=> $true ) ).
fof(ssSkP362,fi_predicates,
! [X1] :
( ssSkP362(X1)
<=> $true ) ).
fof(ssSkP363,fi_predicates,
! [X1] :
( ssSkP363(X1)
<=> $true ) ).
fof(ssSkP364,fi_predicates,
! [X1] :
( ssSkP364(X1)
<=> $true ) ).
fof(ssSkP365,fi_predicates,
! [X1,X2] :
( ssSkP365(X1,X2)
<=> $true ) ).
fof(ssSkP366,fi_predicates,
! [X1,X2] :
( ssSkP366(X1,X2)
<=> $true ) ).
fof(ssSkP367,fi_predicates,
! [X1] :
( ssSkP367(X1)
<=> $false ) ).
fof(ssSkP368,fi_predicates,
! [X1] :
( ssSkP368(X1)
<=> $false ) ).
fof(ssSkP369,fi_predicates,
! [X1] :
( ssSkP369(X1)
<=> $false ) ).
fof(ssSkP37,fi_predicates,
! [X1] :
( ssSkP37(X1)
<=> $false ) ).
fof(ssSkP370,fi_predicates,
! [X1] :
( ssSkP370(X1)
<=> $false ) ).
fof(ssSkP371,fi_predicates,
! [X1] :
( ssSkP371(X1)
<=> $false ) ).
fof(ssSkP372,fi_predicates,
! [X1] :
( ssSkP372(X1)
<=> $false ) ).
fof(ssSkP373,fi_predicates,
! [X1] :
( ssSkP373(X1)
<=> $false ) ).
fof(ssSkP374,fi_predicates,
! [X1] :
( ssSkP374(X1)
<=> $false ) ).
fof(ssSkP375,fi_predicates,
! [X1] :
( ssSkP375(X1)
<=> $false ) ).
fof(ssSkP376,fi_predicates,
! [X1] :
( ssSkP376(X1)
<=> $false ) ).
fof(ssSkP377,fi_predicates,
! [X1] :
( ssSkP377(X1)
<=> $false ) ).
fof(ssSkP378,fi_predicates,
! [X1] :
( ssSkP378(X1)
<=> $false ) ).
fof(ssSkP379,fi_predicates,
! [X1] :
( ssSkP379(X1)
<=> $true ) ).
fof(ssSkP38,fi_predicates,
! [X1] :
( ssSkP38(X1)
<=> $false ) ).
fof(ssSkP380,fi_predicates,
! [X1] :
( ssSkP380(X1)
<=> $true ) ).
fof(ssSkP381,fi_predicates,
! [X1] :
( ssSkP381(X1)
<=> $true ) ).
fof(ssSkP382,fi_predicates,
! [X1] :
( ssSkP382(X1)
<=> $true ) ).
fof(ssSkP383,fi_predicates,
! [X1] :
( ssSkP383(X1)
<=> $true ) ).
fof(ssSkP384,fi_predicates,
! [X1] :
( ssSkP384(X1)
<=> $true ) ).
fof(ssSkP385,fi_predicates,
! [X1] :
( ssSkP385(X1)
<=> $true ) ).
fof(ssSkP386,fi_predicates,
! [X1,X2] :
( ssSkP386(X1,X2)
<=> $true ) ).
fof(ssSkP387,fi_predicates,
! [X1,X2] :
( ssSkP387(X1,X2)
<=> $true ) ).
fof(ssSkP388,fi_predicates,
! [X1] :
( ssSkP388(X1)
<=> $false ) ).
fof(ssSkP389,fi_predicates,
! [X1] :
( ssSkP389(X1)
<=> $false ) ).
fof(ssSkP39,fi_predicates,
! [X1] :
( ssSkP39(X1)
<=> $false ) ).
fof(ssSkP390,fi_predicates,
! [X1] :
( ssSkP390(X1)
<=> $false ) ).
fof(ssSkP391,fi_predicates,
! [X1] :
( ssSkP391(X1)
<=> $false ) ).
fof(ssSkP392,fi_predicates,
! [X1] :
( ssSkP392(X1)
<=> $false ) ).
fof(ssSkP393,fi_predicates,
! [X1] :
( ssSkP393(X1)
<=> $false ) ).
fof(ssSkP394,fi_predicates,
! [X1] :
( ssSkP394(X1)
<=> $false ) ).
fof(ssSkP395,fi_predicates,
! [X1] :
( ssSkP395(X1)
<=> $false ) ).
fof(ssSkP396,fi_predicates,
! [X1] :
( ssSkP396(X1)
<=> $false ) ).
fof(ssSkP397,fi_predicates,
! [X1] :
( ssSkP397(X1)
<=> $false ) ).
fof(ssSkP398,fi_predicates,
! [X1] :
( ssSkP398(X1)
<=> $false ) ).
fof(ssSkP399,fi_predicates,
! [X1] :
( ssSkP399(X1)
<=> $false ) ).
fof(ssSkP4,fi_predicates,
! [X1] :
( ssSkP4(X1)
<=> $false ) ).
fof(ssSkP40,fi_predicates,
! [X1] :
( ssSkP40(X1)
<=> $false ) ).
fof(ssSkP400,fi_predicates,
! [X1] :
( ssSkP400(X1)
<=> $false ) ).
fof(ssSkP401,fi_predicates,
! [X1] :
( ssSkP401(X1)
<=> $false ) ).
fof(ssSkP402,fi_predicates,
! [X1] :
( ssSkP402(X1)
<=> $false ) ).
fof(ssSkP403,fi_predicates,
! [X1] :
( ssSkP403(X1)
<=> $false ) ).
fof(ssSkP404,fi_predicates,
! [X1] :
( ssSkP404(X1)
<=> $false ) ).
fof(ssSkP405,fi_predicates,
! [X1] :
( ssSkP405(X1)
<=> $false ) ).
fof(ssSkP406,fi_predicates,
! [X1] :
( ssSkP406(X1)
<=> $false ) ).
fof(ssSkP407,fi_predicates,
! [X1] :
( ssSkP407(X1)
<=> $false ) ).
fof(ssSkP408,fi_predicates,
! [X1] :
( ssSkP408(X1)
<=> $false ) ).
fof(ssSkP409,fi_predicates,
! [X1] :
( ssSkP409(X1)
<=> $false ) ).
fof(ssSkP41,fi_predicates,
! [X1] :
( ssSkP41(X1)
<=> $false ) ).
fof(ssSkP410,fi_predicates,
! [X1] :
( ssSkP410(X1)
<=> $false ) ).
fof(ssSkP411,fi_predicates,
! [X1] :
( ssSkP411(X1)
<=> $false ) ).
fof(ssSkP412,fi_predicates,
! [X1] :
( ssSkP412(X1)
<=> $false ) ).
fof(ssSkP413,fi_predicates,
! [X1] :
( ssSkP413(X1)
<=> $true ) ).
fof(ssSkP414,fi_predicates,
! [X1] :
( ssSkP414(X1)
<=> $true ) ).
fof(ssSkP415,fi_predicates,
! [X1] :
( ssSkP415(X1)
<=> $true ) ).
fof(ssSkP416,fi_predicates,
! [X1] :
( ssSkP416(X1)
<=> $true ) ).
fof(ssSkP417,fi_predicates,
! [X1] :
( ssSkP417(X1)
<=> $true ) ).
fof(ssSkP418,fi_predicates,
! [X1,X2] :
( ssSkP418(X1,X2)
<=> $true ) ).
fof(ssSkP419,fi_predicates,
! [X1,X2] :
( ssSkP419(X1,X2)
<=> $true ) ).
fof(ssSkP42,fi_predicates,
! [X1] :
( ssSkP42(X1)
<=> $false ) ).
fof(ssSkP420,fi_predicates,
! [X1] :
( ssSkP420(X1)
<=> $false ) ).
fof(ssSkP421,fi_predicates,
! [X1] :
( ssSkP421(X1)
<=> $false ) ).
fof(ssSkP422,fi_predicates,
! [X1] :
( ssSkP422(X1)
<=> $false ) ).
fof(ssSkP423,fi_predicates,
! [X1] :
( ssSkP423(X1)
<=> $false ) ).
fof(ssSkP424,fi_predicates,
! [X1] :
( ssSkP424(X1)
<=> $false ) ).
fof(ssSkP425,fi_predicates,
! [X1] :
( ssSkP425(X1)
<=> $false ) ).
fof(ssSkP426,fi_predicates,
! [X1] :
( ssSkP426(X1)
<=> $false ) ).
fof(ssSkP427,fi_predicates,
! [X1] :
( ssSkP427(X1)
<=> $false ) ).
fof(ssSkP428,fi_predicates,
! [X1] :
( ssSkP428(X1)
<=> $false ) ).
fof(ssSkP429,fi_predicates,
! [X1] :
( ssSkP429(X1)
<=> $false ) ).
fof(ssSkP43,fi_predicates,
! [X1] :
( ssSkP43(X1)
<=> $false ) ).
fof(ssSkP430,fi_predicates,
! [X1] :
( ssSkP430(X1)
<=> $false ) ).
fof(ssSkP431,fi_predicates,
! [X1] :
( ssSkP431(X1)
<=> $false ) ).
fof(ssSkP432,fi_predicates,
! [X1] :
( ssSkP432(X1)
<=> $false ) ).
fof(ssSkP433,fi_predicates,
! [X1] :
( ssSkP433(X1)
<=> $false ) ).
fof(ssSkP434,fi_predicates,
! [X1] :
( ssSkP434(X1)
<=> $false ) ).
fof(ssSkP435,fi_predicates,
! [X1] :
( ssSkP435(X1)
<=> $false ) ).
fof(ssSkP436,fi_predicates,
! [X1] :
( ssSkP436(X1)
<=> $false ) ).
fof(ssSkP437,fi_predicates,
! [X1] :
( ssSkP437(X1)
<=> $false ) ).
fof(ssSkP438,fi_predicates,
! [X1] :
( ssSkP438(X1)
<=> $false ) ).
fof(ssSkP439,fi_predicates,
! [X1] :
( ssSkP439(X1)
<=> $false ) ).
fof(ssSkP44,fi_predicates,
! [X1] :
( ssSkP44(X1)
<=> $false ) ).
fof(ssSkP440,fi_predicates,
! [X1] :
( ssSkP440(X1)
<=> $false ) ).
fof(ssSkP441,fi_predicates,
! [X1] :
( ssSkP441(X1)
<=> $false ) ).
fof(ssSkP442,fi_predicates,
! [X1] :
( ssSkP442(X1)
<=> $false ) ).
fof(ssSkP443,fi_predicates,
! [X1] :
( ssSkP443(X1)
<=> $false ) ).
fof(ssSkP444,fi_predicates,
! [X1] :
( ssSkP444(X1)
<=> $false ) ).
fof(ssSkP445,fi_predicates,
! [X1] :
( ssSkP445(X1)
<=> $false ) ).
fof(ssSkP446,fi_predicates,
! [X1] :
( ssSkP446(X1)
<=> $false ) ).
fof(ssSkP447,fi_predicates,
! [X1] :
( ssSkP447(X1)
<=> $false ) ).
fof(ssSkP448,fi_predicates,
! [X1] :
( ssSkP448(X1)
<=> $false ) ).
fof(ssSkP449,fi_predicates,
! [X1] :
( ssSkP449(X1)
<=> $false ) ).
fof(ssSkP45,fi_predicates,
! [X1] :
( ssSkP45(X1)
<=> $false ) ).
fof(ssSkP450,fi_predicates,
! [X1] :
( ssSkP450(X1)
<=> $false ) ).
fof(ssSkP451,fi_predicates,
! [X1] :
( ssSkP451(X1)
<=> $false ) ).
fof(ssSkP452,fi_predicates,
! [X1] :
( ssSkP452(X1)
<=> $true ) ).
fof(ssSkP453,fi_predicates,
! [X1] :
( ssSkP453(X1)
<=> $true ) ).
fof(ssSkP454,fi_predicates,
! [X1] :
( ssSkP454(X1)
<=> $true ) ).
fof(ssSkP455,fi_predicates,
! [X1] :
( ssSkP455(X1)
<=> $true ) ).
fof(ssSkP456,fi_predicates,
! [X1] :
( ssSkP456(X1)
<=> $true ) ).
fof(ssSkP457,fi_predicates,
! [X1,X2] :
( ssSkP457(X1,X2)
<=> $true ) ).
fof(ssSkP458,fi_predicates,
! [X1,X2] :
( ssSkP458(X1,X2)
<=> $true ) ).
fof(ssSkP459,fi_predicates,
! [X1] :
( ssSkP459(X1)
<=> $false ) ).
fof(ssSkP46,fi_predicates,
! [X1] :
( ssSkP46(X1)
<=> $false ) ).
fof(ssSkP460,fi_predicates,
! [X1] :
( ssSkP460(X1)
<=> $false ) ).
fof(ssSkP461,fi_predicates,
! [X1] :
( ssSkP461(X1)
<=> $false ) ).
fof(ssSkP462,fi_predicates,
! [X1] :
( ssSkP462(X1)
<=> $false ) ).
fof(ssSkP463,fi_predicates,
! [X1] :
( ssSkP463(X1)
<=> $false ) ).
fof(ssSkP464,fi_predicates,
! [X1] :
( ssSkP464(X1)
<=> $false ) ).
fof(ssSkP465,fi_predicates,
! [X1] :
( ssSkP465(X1)
<=> $false ) ).
fof(ssSkP466,fi_predicates,
! [X1] :
( ssSkP466(X1)
<=> $false ) ).
fof(ssSkP467,fi_predicates,
! [X1] :
( ssSkP467(X1)
<=> $false ) ).
fof(ssSkP468,fi_predicates,
! [X1] :
( ssSkP468(X1)
<=> $false ) ).
fof(ssSkP469,fi_predicates,
! [X1] :
( ssSkP469(X1)
<=> $false ) ).
fof(ssSkP47,fi_predicates,
! [X1] :
( ssSkP47(X1)
<=> $false ) ).
fof(ssSkP470,fi_predicates,
! [X1] :
( ssSkP470(X1)
<=> $false ) ).
fof(ssSkP471,fi_predicates,
! [X1] :
( ssSkP471(X1)
<=> $false ) ).
fof(ssSkP472,fi_predicates,
! [X1] :
( ssSkP472(X1)
<=> $false ) ).
fof(ssSkP473,fi_predicates,
! [X1] :
( ssSkP473(X1)
<=> $false ) ).
fof(ssSkP474,fi_predicates,
! [X1] :
( ssSkP474(X1)
<=> $false ) ).
fof(ssSkP475,fi_predicates,
! [X1] :
( ssSkP475(X1)
<=> $false ) ).
fof(ssSkP476,fi_predicates,
! [X1] :
( ssSkP476(X1)
<=> $false ) ).
fof(ssSkP477,fi_predicates,
! [X1] :
( ssSkP477(X1)
<=> $false ) ).
fof(ssSkP478,fi_predicates,
! [X1] :
( ssSkP478(X1)
<=> $false ) ).
fof(ssSkP479,fi_predicates,
! [X1] :
( ssSkP479(X1)
<=> $false ) ).
fof(ssSkP48,fi_predicates,
! [X1] :
( ssSkP48(X1)
<=> $false ) ).
fof(ssSkP480,fi_predicates,
! [X1] :
( ssSkP480(X1)
<=> $false ) ).
fof(ssSkP481,fi_predicates,
! [X1] :
( ssSkP481(X1)
<=> $false ) ).
fof(ssSkP482,fi_predicates,
! [X1] :
( ssSkP482(X1)
<=> $false ) ).
fof(ssSkP483,fi_predicates,
! [X1] :
( ssSkP483(X1)
<=> $false ) ).
fof(ssSkP484,fi_predicates,
! [X1] :
( ssSkP484(X1)
<=> $false ) ).
fof(ssSkP485,fi_predicates,
! [X1] :
( ssSkP485(X1)
<=> $false ) ).
fof(ssSkP486,fi_predicates,
! [X1] :
( ssSkP486(X1)
<=> $false ) ).
fof(ssSkP487,fi_predicates,
! [X1] :
( ssSkP487(X1)
<=> $false ) ).
fof(ssSkP488,fi_predicates,
! [X1] :
( ssSkP488(X1)
<=> $false ) ).
fof(ssSkP489,fi_predicates,
! [X1] :
( ssSkP489(X1)
<=> $true ) ).
fof(ssSkP49,fi_predicates,
! [X1] :
( ssSkP49(X1)
<=> $false ) ).
fof(ssSkP490,fi_predicates,
! [X1] :
( ssSkP490(X1)
<=> $true ) ).
fof(ssSkP491,fi_predicates,
! [X1] :
( ssSkP491(X1)
<=> $true ) ).
fof(ssSkP492,fi_predicates,
! [X1] :
( ssSkP492(X1)
<=> $true ) ).
fof(ssSkP493,fi_predicates,
! [X1] :
( ssSkP493(X1)
<=> $true ) ).
fof(ssSkP494,fi_predicates,
! [X1] :
( ssSkP494(X1)
<=> $true ) ).
fof(ssSkP495,fi_predicates,
! [X1,X2] :
( ssSkP495(X1,X2)
<=> $true ) ).
fof(ssSkP496,fi_predicates,
! [X1,X2] :
( ssSkP496(X1,X2)
<=> $true ) ).
fof(ssSkP497,fi_predicates,
! [X1] :
( ssSkP497(X1)
<=> $false ) ).
fof(ssSkP498,fi_predicates,
! [X1] :
( ssSkP498(X1)
<=> $false ) ).
fof(ssSkP499,fi_predicates,
! [X1] :
( ssSkP499(X1)
<=> $false ) ).
fof(ssSkP5,fi_predicates,
! [X1] :
( ssSkP5(X1)
<=> $false ) ).
fof(ssSkP50,fi_predicates,
! [X1] :
( ssSkP50(X1)
<=> $false ) ).
fof(ssSkP500,fi_predicates,
! [X1] :
( ssSkP500(X1)
<=> $false ) ).
fof(ssSkP501,fi_predicates,
! [X1] :
( ssSkP501(X1)
<=> $false ) ).
fof(ssSkP502,fi_predicates,
! [X1] :
( ssSkP502(X1)
<=> $false ) ).
fof(ssSkP503,fi_predicates,
! [X1] :
( ssSkP503(X1)
<=> $false ) ).
fof(ssSkP504,fi_predicates,
! [X1] :
( ssSkP504(X1)
<=> $false ) ).
fof(ssSkP505,fi_predicates,
! [X1] :
( ssSkP505(X1)
<=> $false ) ).
fof(ssSkP506,fi_predicates,
! [X1] :
( ssSkP506(X1)
<=> $false ) ).
fof(ssSkP507,fi_predicates,
! [X1] :
( ssSkP507(X1)
<=> $false ) ).
fof(ssSkP508,fi_predicates,
! [X1] :
( ssSkP508(X1)
<=> $false ) ).
fof(ssSkP509,fi_predicates,
! [X1] :
( ssSkP509(X1)
<=> $false ) ).
fof(ssSkP51,fi_predicates,
! [X1] :
( ssSkP51(X1)
<=> $false ) ).
fof(ssSkP510,fi_predicates,
! [X1] :
( ssSkP510(X1)
<=> $false ) ).
fof(ssSkP511,fi_predicates,
! [X1] :
( ssSkP511(X1)
<=> $false ) ).
fof(ssSkP512,fi_predicates,
! [X1] :
( ssSkP512(X1)
<=> $false ) ).
fof(ssSkP513,fi_predicates,
! [X1] :
( ssSkP513(X1)
<=> $false ) ).
fof(ssSkP514,fi_predicates,
! [X1] :
( ssSkP514(X1)
<=> $false ) ).
fof(ssSkP515,fi_predicates,
! [X1] :
( ssSkP515(X1)
<=> $false ) ).
fof(ssSkP516,fi_predicates,
! [X1] :
( ssSkP516(X1)
<=> $false ) ).
fof(ssSkP517,fi_predicates,
! [X1] :
( ssSkP517(X1)
<=> $false ) ).
fof(ssSkP518,fi_predicates,
! [X1] :
( ssSkP518(X1)
<=> $false ) ).
fof(ssSkP519,fi_predicates,
! [X1] :
( ssSkP519(X1)
<=> $false ) ).
fof(ssSkP52,fi_predicates,
! [X1] :
( ssSkP52(X1)
<=> $true ) ).
fof(ssSkP520,fi_predicates,
! [X1] :
( ssSkP520(X1)
<=> $false ) ).
fof(ssSkP521,fi_predicates,
! [X1] :
( ssSkP521(X1)
<=> $false ) ).
fof(ssSkP522,fi_predicates,
! [X1] :
( ssSkP522(X1)
<=> $false ) ).
fof(ssSkP523,fi_predicates,
! [X1] :
( ssSkP523(X1)
<=> $false ) ).
fof(ssSkP524,fi_predicates,
! [X1] :
( ssSkP524(X1)
<=> $true ) ).
fof(ssSkP525,fi_predicates,
! [X1] :
( ssSkP525(X1)
<=> $true ) ).
fof(ssSkP526,fi_predicates,
! [X1] :
( ssSkP526(X1)
<=> $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,
! [X1] :
( ssSkP53(X1)
<=> $true ) ).
fof(ssSkP530,fi_predicates,
! [X1,X2] :
( ssSkP530(X1,X2)
<=> $true ) ).
fof(ssSkP531,fi_predicates,
! [X1,X2] :
( ssSkP531(X1,X2)
<=> $true ) ).
fof(ssSkP532,fi_predicates,
! [X1] :
( ssSkP532(X1)
<=> $false ) ).
fof(ssSkP533,fi_predicates,
! [X1] :
( ssSkP533(X1)
<=> $false ) ).
fof(ssSkP534,fi_predicates,
! [X1] :
( ssSkP534(X1)
<=> $false ) ).
fof(ssSkP535,fi_predicates,
! [X1] :
( ssSkP535(X1)
<=> $false ) ).
fof(ssSkP536,fi_predicates,
! [X1] :
( ssSkP536(X1)
<=> $false ) ).
fof(ssSkP537,fi_predicates,
! [X1] :
( ssSkP537(X1)
<=> $false ) ).
fof(ssSkP538,fi_predicates,
! [X1] :
( ssSkP538(X1)
<=> $false ) ).
fof(ssSkP539,fi_predicates,
! [X1] :
( ssSkP539(X1)
<=> $false ) ).
fof(ssSkP54,fi_predicates,
! [X1] :
( ssSkP54(X1)
<=> $true ) ).
fof(ssSkP540,fi_predicates,
! [X1] :
( ssSkP540(X1)
<=> $false ) ).
fof(ssSkP541,fi_predicates,
! [X1] :
( ssSkP541(X1)
<=> $false ) ).
fof(ssSkP542,fi_predicates,
! [X1] :
( ssSkP542(X1)
<=> $false ) ).
fof(ssSkP543,fi_predicates,
! [X1] :
( ssSkP543(X1)
<=> $false ) ).
fof(ssSkP544,fi_predicates,
! [X1] :
( ssSkP544(X1)
<=> $false ) ).
fof(ssSkP545,fi_predicates,
! [X1] :
( ssSkP545(X1)
<=> $false ) ).
fof(ssSkP546,fi_predicates,
! [X1] :
( ssSkP546(X1)
<=> $false ) ).
fof(ssSkP547,fi_predicates,
! [X1] :
( ssSkP547(X1)
<=> $false ) ).
fof(ssSkP548,fi_predicates,
! [X1] :
( ssSkP548(X1)
<=> $false ) ).
fof(ssSkP549,fi_predicates,
! [X1] :
( ssSkP549(X1)
<=> $false ) ).
fof(ssSkP55,fi_predicates,
! [X1] :
( ssSkP55(X1)
<=> $true ) ).
fof(ssSkP550,fi_predicates,
! [X1] :
( ssSkP550(X1)
<=> $false ) ).
fof(ssSkP551,fi_predicates,
! [X1] :
( ssSkP551(X1)
<=> $false ) ).
fof(ssSkP552,fi_predicates,
! [X1] :
( ssSkP552(X1)
<=> $false ) ).
fof(ssSkP553,fi_predicates,
! [X1] :
( ssSkP553(X1)
<=> $false ) ).
fof(ssSkP554,fi_predicates,
! [X1] :
( ssSkP554(X1)
<=> $false ) ).
fof(ssSkP555,fi_predicates,
! [X1] :
( ssSkP555(X1)
<=> $false ) ).
fof(ssSkP556,fi_predicates,
! [X1] :
( ssSkP556(X1)
<=> $false ) ).
fof(ssSkP557,fi_predicates,
! [X1] :
( ssSkP557(X1)
<=> $false ) ).
fof(ssSkP558,fi_predicates,
! [X1] :
( ssSkP558(X1)
<=> $false ) ).
fof(ssSkP559,fi_predicates,
! [X1] :
( ssSkP559(X1)
<=> $false ) ).
fof(ssSkP56,fi_predicates,
! [X1,X2] :
( ssSkP56(X1,X2)
<=> $true ) ).
fof(ssSkP560,fi_predicates,
! [X1] :
( ssSkP560(X1)
<=> $false ) ).
fof(ssSkP561,fi_predicates,
! [X1] :
( ssSkP561(X1)
<=> $false ) ).
fof(ssSkP562,fi_predicates,
! [X1] :
( ssSkP562(X1)
<=> $false ) ).
fof(ssSkP563,fi_predicates,
! [X1] :
( ssSkP563(X1)
<=> $false ) ).
fof(ssSkP564,fi_predicates,
! [X1] :
( ssSkP564(X1)
<=> $false ) ).
fof(ssSkP565,fi_predicates,
! [X1] :
( ssSkP565(X1)
<=> $false ) ).
fof(ssSkP566,fi_predicates,
! [X1] :
( ssSkP566(X1)
<=> $true ) ).
fof(ssSkP567,fi_predicates,
! [X1] :
( ssSkP567(X1)
<=> $true ) ).
fof(ssSkP568,fi_predicates,
! [X1] :
( ssSkP568(X1)
<=> $true ) ).
fof(ssSkP569,fi_predicates,
! [X1] :
( ssSkP569(X1)
<=> $true ) ).
fof(ssSkP57,fi_predicates,
! [X1,X2] :
( ssSkP57(X1,X2)
<=> $true ) ).
fof(ssSkP570,fi_predicates,
! [X1] :
( ssSkP570(X1)
<=> $true ) ).
fof(ssSkP571,fi_predicates,
! [X1] :
( ssSkP571(X1)
<=> $true ) ).
fof(ssSkP572,fi_predicates,
! [X1,X2] :
( ssSkP572(X1,X2)
<=> $true ) ).
fof(ssSkP573,fi_predicates,
! [X1,X2] :
( ssSkP573(X1,X2)
<=> $true ) ).
fof(ssSkP574,fi_predicates,
! [X1] :
( ssSkP574(X1)
<=> $false ) ).
fof(ssSkP575,fi_predicates,
! [X1] :
( ssSkP575(X1)
<=> $false ) ).
fof(ssSkP576,fi_predicates,
! [X1] :
( ssSkP576(X1)
<=> $false ) ).
fof(ssSkP577,fi_predicates,
! [X1] :
( ssSkP577(X1)
<=> $false ) ).
fof(ssSkP578,fi_predicates,
! [X1] :
( ssSkP578(X1)
<=> $false ) ).
fof(ssSkP579,fi_predicates,
! [X1] :
( ssSkP579(X1)
<=> $false ) ).
fof(ssSkP58,fi_predicates,
! [X1] :
( ssSkP58(X1)
<=> $false ) ).
fof(ssSkP580,fi_predicates,
! [X1] :
( ssSkP580(X1)
<=> $false ) ).
fof(ssSkP581,fi_predicates,
! [X1] :
( ssSkP581(X1)
<=> $false ) ).
fof(ssSkP582,fi_predicates,
! [X1] :
( ssSkP582(X1)
<=> $false ) ).
fof(ssSkP583,fi_predicates,
! [X1] :
( ssSkP583(X1)
<=> $false ) ).
fof(ssSkP584,fi_predicates,
! [X1] :
( ssSkP584(X1)
<=> $false ) ).
fof(ssSkP585,fi_predicates,
! [X1] :
( ssSkP585(X1)
<=> $false ) ).
fof(ssSkP586,fi_predicates,
! [X1] :
( ssSkP586(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP59(X1)
<=> $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)
<=> $false ) ).
fof(ssSkP599,fi_predicates,
! [X1] :
( ssSkP599(X1)
<=> $false ) ).
fof(ssSkP6,fi_predicates,
! [X1] :
( ssSkP6(X1)
<=> $false ) ).
fof(ssSkP60,fi_predicates,
! [X1] :
( ssSkP60(X1)
<=> $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,X2] :
( ssSkP606(X1,X2)
<=> $true ) ).
fof(ssSkP607,fi_predicates,
! [X1,X2] :
( ssSkP607(X1,X2)
<=> $true ) ).
fof(ssSkP608,fi_predicates,
! [X1] :
( ssSkP608(X1)
<=> $false ) ).
fof(ssSkP609,fi_predicates,
! [X1] :
( ssSkP609(X1)
<=> $false ) ).
fof(ssSkP61,fi_predicates,
! [X1] :
( ssSkP61(X1)
<=> $false ) ).
fof(ssSkP610,fi_predicates,
! [X1] :
( ssSkP610(X1)
<=> $false ) ).
fof(ssSkP611,fi_predicates,
! [X1] :
( ssSkP611(X1)
<=> $false ) ).
fof(ssSkP612,fi_predicates,
! [X1] :
( ssSkP612(X1)
<=> $false ) ).
fof(ssSkP613,fi_predicates,
! [X1] :
( ssSkP613(X1)
<=> $false ) ).
fof(ssSkP614,fi_predicates,
! [X1] :
( ssSkP614(X1)
<=> $false ) ).
fof(ssSkP615,fi_predicates,
! [X1] :
( ssSkP615(X1)
<=> $false ) ).
fof(ssSkP616,fi_predicates,
! [X1] :
( ssSkP616(X1)
<=> $false ) ).
fof(ssSkP617,fi_predicates,
! [X1] :
( ssSkP617(X1)
<=> $false ) ).
fof(ssSkP618,fi_predicates,
! [X1] :
( ssSkP618(X1)
<=> $false ) ).
fof(ssSkP619,fi_predicates,
! [X1] :
( ssSkP619(X1)
<=> $false ) ).
fof(ssSkP62,fi_predicates,
! [X1] :
( ssSkP62(X1)
<=> $false ) ).
fof(ssSkP620,fi_predicates,
! [X1] :
( ssSkP620(X1)
<=> $false ) ).
fof(ssSkP621,fi_predicates,
! [X1] :
( ssSkP621(X1)
<=> $false ) ).
fof(ssSkP622,fi_predicates,
! [X1] :
( ssSkP622(X1)
<=> $false ) ).
fof(ssSkP623,fi_predicates,
! [X1] :
( ssSkP623(X1)
<=> $false ) ).
fof(ssSkP624,fi_predicates,
! [X1] :
( ssSkP624(X1)
<=> $false ) ).
fof(ssSkP625,fi_predicates,
! [X1] :
( ssSkP625(X1)
<=> $false ) ).
fof(ssSkP626,fi_predicates,
! [X1] :
( ssSkP626(X1)
<=> $false ) ).
fof(ssSkP627,fi_predicates,
! [X1] :
( ssSkP627(X1)
<=> $false ) ).
fof(ssSkP628,fi_predicates,
! [X1] :
( ssSkP628(X1)
<=> $false ) ).
fof(ssSkP629,fi_predicates,
! [X1] :
( ssSkP629(X1)
<=> $false ) ).
fof(ssSkP63,fi_predicates,
! [X1] :
( ssSkP63(X1)
<=> $false ) ).
fof(ssSkP630,fi_predicates,
! [X1] :
( ssSkP630(X1)
<=> $false ) ).
fof(ssSkP631,fi_predicates,
! [X1] :
( ssSkP631(X1)
<=> $false ) ).
fof(ssSkP632,fi_predicates,
! [X1] :
( ssSkP632(X1)
<=> $false ) ).
fof(ssSkP633,fi_predicates,
! [X1] :
( ssSkP633(X1)
<=> $false ) ).
fof(ssSkP634,fi_predicates,
! [X1] :
( ssSkP634(X1)
<=> $false ) ).
fof(ssSkP635,fi_predicates,
! [X1] :
( ssSkP635(X1)
<=> $false ) ).
fof(ssSkP636,fi_predicates,
! [X1] :
( ssSkP636(X1)
<=> $false ) ).
fof(ssSkP637,fi_predicates,
! [X1] :
( ssSkP637(X1)
<=> $true ) ).
fof(ssSkP638,fi_predicates,
! [X1] :
( ssSkP638(X1)
<=> $true ) ).
fof(ssSkP639,fi_predicates,
! [X1] :
( ssSkP639(X1)
<=> $true ) ).
fof(ssSkP64,fi_predicates,
! [X1] :
( ssSkP64(X1)
<=> $false ) ).
fof(ssSkP640,fi_predicates,
! [X1] :
( ssSkP640(X1)
<=> $true ) ).
fof(ssSkP641,fi_predicates,
! [X1] :
( ssSkP641(X1)
<=> $true ) ).
fof(ssSkP642,fi_predicates,
! [X1] :
( ssSkP642(X1)
<=> $true ) ).
fof(ssSkP643,fi_predicates,
! [X1] :
( ssSkP643(X1)
<=> $true ) ).
fof(ssSkP644,fi_predicates,
! [X1] :
( ssSkP644(X1)
<=> $true ) ).
fof(ssSkP645,fi_predicates,
! [X1,X2] :
( ssSkP645(X1,X2)
<=> $true ) ).
fof(ssSkP646,fi_predicates,
! [X1,X2] :
( ssSkP646(X1,X2)
<=> $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,
! [X1] :
( ssSkP65(X1)
<=> $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,
! [X1] :
( ssSkP66(X1)
<=> $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,X2] :
( ssSkP667(X1,X2)
<=> $true ) ).
fof(ssSkP668,fi_predicates,
! [X1,X2] :
( ssSkP668(X1,X2)
<=> $true ) ).
fof(ssSkP669,fi_predicates,
! [X1] :
( ssSkP669(X1)
<=> $false ) ).
fof(ssSkP67,fi_predicates,
! [X1] :
( ssSkP67(X1)
<=> $false ) ).
fof(ssSkP670,fi_predicates,
! [X1] :
( ssSkP670(X1)
<=> $false ) ).
fof(ssSkP671,fi_predicates,
! [X1] :
( ssSkP671(X1)
<=> $false ) ).
fof(ssSkP672,fi_predicates,
! [X1] :
( ssSkP672(X1)
<=> $false ) ).
fof(ssSkP673,fi_predicates,
! [X1] :
( ssSkP673(X1)
<=> $false ) ).
fof(ssSkP674,fi_predicates,
! [X1] :
( ssSkP674(X1)
<=> $false ) ).
fof(ssSkP675,fi_predicates,
! [X1] :
( ssSkP675(X1)
<=> $false ) ).
fof(ssSkP676,fi_predicates,
! [X1] :
( ssSkP676(X1)
<=> $false ) ).
fof(ssSkP677,fi_predicates,
! [X1] :
( ssSkP677(X1)
<=> $false ) ).
fof(ssSkP678,fi_predicates,
! [X1] :
( ssSkP678(X1)
<=> $false ) ).
fof(ssSkP679,fi_predicates,
! [X1] :
( ssSkP679(X1)
<=> $false ) ).
fof(ssSkP68,fi_predicates,
! [X1] :
( ssSkP68(X1)
<=> $false ) ).
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)
<=> $false ) ).
fof(ssSkP69,fi_predicates,
! [X1] :
( ssSkP69(X1)
<=> $false ) ).
fof(ssSkP690,fi_predicates,
! [X1] :
( ssSkP690(X1)
<=> $false ) ).
fof(ssSkP691,fi_predicates,
! [X1] :
( ssSkP691(X1)
<=> $false ) ).
fof(ssSkP692,fi_predicates,
! [X1] :
( ssSkP692(X1)
<=> $false ) ).
fof(ssSkP693,fi_predicates,
! [X1] :
( ssSkP693(X1)
<=> $false ) ).
fof(ssSkP694,fi_predicates,
! [X1] :
( ssSkP694(X1)
<=> $false ) ).
fof(ssSkP695,fi_predicates,
! [X1] :
( ssSkP695(X1)
<=> $false ) ).
fof(ssSkP696,fi_predicates,
! [X1] :
( ssSkP696(X1)
<=> $false ) ).
fof(ssSkP697,fi_predicates,
! [X1] :
( ssSkP697(X1)
<=> $false ) ).
fof(ssSkP698,fi_predicates,
! [X1] :
( ssSkP698(X1)
<=> $false ) ).
fof(ssSkP699,fi_predicates,
! [X1] :
( ssSkP699(X1)
<=> $false ) ).
fof(ssSkP7,fi_predicates,
! [X1] :
( ssSkP7(X1)
<=> $false ) ).
fof(ssSkP70,fi_predicates,
! [X1] :
( ssSkP70(X1)
<=> $false ) ).
fof(ssSkP700,fi_predicates,
! [X1] :
( ssSkP700(X1)
<=> $false ) ).
fof(ssSkP701,fi_predicates,
! [X1] :
( ssSkP701(X1)
<=> $false ) ).
fof(ssSkP702,fi_predicates,
! [X1] :
( ssSkP702(X1)
<=> $true ) ).
fof(ssSkP703,fi_predicates,
! [X1] :
( ssSkP703(X1)
<=> $true ) ).
fof(ssSkP704,fi_predicates,
! [X1] :
( ssSkP704(X1)
<=> $true ) ).
fof(ssSkP705,fi_predicates,
! [X1] :
( ssSkP705(X1)
<=> $true ) ).
fof(ssSkP706,fi_predicates,
! [X1] :
( ssSkP706(X1)
<=> $true ) ).
fof(ssSkP707,fi_predicates,
! [X1] :
( ssSkP707(X1)
<=> $true ) ).
fof(ssSkP708,fi_predicates,
! [X1] :
( ssSkP708(X1)
<=> $true ) ).
fof(ssSkP709,fi_predicates,
! [X1] :
( ssSkP709(X1)
<=> $true ) ).
fof(ssSkP71,fi_predicates,
! [X1] :
( ssSkP71(X1)
<=> $false ) ).
fof(ssSkP710,fi_predicates,
! [X1] :
( ssSkP710(X1)
<=> $true ) ).
fof(ssSkP711,fi_predicates,
! [X1,X2] :
( ssSkP711(X1,X2)
<=> $true ) ).
fof(ssSkP712,fi_predicates,
! [X1,X2] :
( ssSkP712(X1,X2)
<=> $true ) ).
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,
! [X1] :
( ssSkP72(X1)
<=> $false ) ).
fof(ssSkP720,fi_predicates,
! [X1] :
( ssSkP720(X1)
<=> $false ) ).
fof(ssSkP721,fi_predicates,
! [X1] :
( ssSkP721(X1)
<=> $false ) ).
fof(ssSkP722,fi_predicates,
! [X1] :
( ssSkP722(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP73(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP735(X1)
<=> $true ) ).
fof(ssSkP736,fi_predicates,
! [X1] :
( ssSkP736(X1)
<=> $true ) ).
fof(ssSkP737,fi_predicates,
! [X1] :
( ssSkP737(X1)
<=> $true ) ).
fof(ssSkP738,fi_predicates,
! [X1] :
( ssSkP738(X1)
<=> $true ) ).
fof(ssSkP739,fi_predicates,
! [X1] :
( ssSkP739(X1)
<=> $true ) ).
fof(ssSkP74,fi_predicates,
! [X1] :
( ssSkP74(X1)
<=> $false ) ).
fof(ssSkP740,fi_predicates,
! [X1] :
( ssSkP740(X1)
<=> $true ) ).
fof(ssSkP741,fi_predicates,
! [X1] :
( ssSkP741(X1)
<=> $true ) ).
fof(ssSkP742,fi_predicates,
! [X1] :
( ssSkP742(X1)
<=> $true ) ).
fof(ssSkP743,fi_predicates,
! [X1] :
( ssSkP743(X1)
<=> $true ) ).
fof(ssSkP744,fi_predicates,
! [X1] :
( ssSkP744(X1)
<=> $true ) ).
fof(ssSkP745,fi_predicates,
! [X1] :
( ssSkP745(X1)
<=> $true ) ).
fof(ssSkP746,fi_predicates,
! [X1] :
( ssSkP746(X1)
<=> $true ) ).
fof(ssSkP747,fi_predicates,
! [X1] :
( ssSkP747(X1)
<=> $true ) ).
fof(ssSkP748,fi_predicates,
! [X1,X2] :
( ssSkP748(X1,X2)
<=> $true ) ).
fof(ssSkP749,fi_predicates,
! [X1,X2] :
( ssSkP749(X1,X2)
<=> $true ) ).
fof(ssSkP75,fi_predicates,
! [X1] :
( ssSkP75(X1)
<=> $false ) ).
fof(ssSkP750,fi_predicates,
! [X1] :
( ssSkP750(X1)
<=> $false ) ).
fof(ssSkP751,fi_predicates,
! [X1] :
( ssSkP751(X1)
<=> $false ) ).
fof(ssSkP752,fi_predicates,
! [X1] :
( ssSkP752(X1)
<=> $false ) ).
fof(ssSkP753,fi_predicates,
! [X1] :
( ssSkP753(X1)
<=> $false ) ).
fof(ssSkP754,fi_predicates,
! [X1] :
( ssSkP754(X1)
<=> $false ) ).
fof(ssSkP755,fi_predicates,
! [X1] :
( ssSkP755(X1)
<=> $false ) ).
fof(ssSkP756,fi_predicates,
! [X1] :
( ssSkP756(X1)
<=> $false ) ).
fof(ssSkP757,fi_predicates,
! [X1] :
( ssSkP757(X1)
<=> $false ) ).
fof(ssSkP758,fi_predicates,
! [X1] :
( ssSkP758(X1)
<=> $false ) ).
fof(ssSkP759,fi_predicates,
! [X1] :
( ssSkP759(X1)
<=> $false ) ).
fof(ssSkP76,fi_predicates,
! [X1] :
( ssSkP76(X1)
<=> $false ) ).
fof(ssSkP760,fi_predicates,
! [X1] :
( ssSkP760(X1)
<=> $false ) ).
fof(ssSkP761,fi_predicates,
! [X1] :
( ssSkP761(X1)
<=> $false ) ).
fof(ssSkP762,fi_predicates,
! [X1] :
( ssSkP762(X1)
<=> $false ) ).
fof(ssSkP763,fi_predicates,
! [X1] :
( ssSkP763(X1)
<=> $false ) ).
fof(ssSkP764,fi_predicates,
! [X1] :
( ssSkP764(X1)
<=> $false ) ).
fof(ssSkP765,fi_predicates,
! [X1] :
( ssSkP765(X1)
<=> $false ) ).
fof(ssSkP766,fi_predicates,
! [X1] :
( ssSkP766(X1)
<=> $false ) ).
fof(ssSkP767,fi_predicates,
! [X1] :
( ssSkP767(X1)
<=> $false ) ).
fof(ssSkP768,fi_predicates,
! [X1] :
( ssSkP768(X1)
<=> $false ) ).
fof(ssSkP769,fi_predicates,
! [X1] :
( ssSkP769(X1)
<=> $false ) ).
fof(ssSkP77,fi_predicates,
! [X1] :
( ssSkP77(X1)
<=> $false ) ).
fof(ssSkP770,fi_predicates,
! [X1] :
( ssSkP770(X1)
<=> $false ) ).
fof(ssSkP771,fi_predicates,
! [X1] :
( ssSkP771(X1)
<=> $false ) ).
fof(ssSkP772,fi_predicates,
! [X1] :
( ssSkP772(X1)
<=> $true ) ).
fof(ssSkP773,fi_predicates,
! [X1] :
( ssSkP773(X1)
<=> $true ) ).
fof(ssSkP774,fi_predicates,
! [X1] :
( ssSkP774(X1)
<=> $true ) ).
fof(ssSkP775,fi_predicates,
! [X1] :
( ssSkP775(X1)
<=> $true ) ).
fof(ssSkP776,fi_predicates,
! [X1] :
( ssSkP776(X1)
<=> $true ) ).
fof(ssSkP777,fi_predicates,
! [X1] :
( ssSkP777(X1)
<=> $true ) ).
fof(ssSkP778,fi_predicates,
! [X1] :
( ssSkP778(X1)
<=> $true ) ).
fof(ssSkP779,fi_predicates,
! [X1] :
( ssSkP779(X1)
<=> $true ) ).
fof(ssSkP78,fi_predicates,
! [X1] :
( ssSkP78(X1)
<=> $false ) ).
fof(ssSkP780,fi_predicates,
! [X1] :
( ssSkP780(X1)
<=> $true ) ).
fof(ssSkP781,fi_predicates,
! [X1] :
( ssSkP781(X1)
<=> $true ) ).
fof(ssSkP782,fi_predicates,
! [X1] :
( ssSkP782(X1)
<=> $true ) ).
fof(ssSkP783,fi_predicates,
! [X1] :
( ssSkP783(X1)
<=> $true ) ).
fof(ssSkP784,fi_predicates,
! [X1] :
( ssSkP784(X1)
<=> $true ) ).
fof(ssSkP785,fi_predicates,
! [X1] :
( ssSkP785(X1)
<=> $true ) ).
fof(ssSkP786,fi_predicates,
! [X1] :
( ssSkP786(X1)
<=> $true ) ).
fof(ssSkP787,fi_predicates,
! [X1] :
( ssSkP787(X1)
<=> $true ) ).
fof(ssSkP788,fi_predicates,
! [X1] :
( ssSkP788(X1)
<=> $true ) ).
fof(ssSkP789,fi_predicates,
! [X1] :
( ssSkP789(X1)
<=> $true ) ).
fof(ssSkP79,fi_predicates,
! [X1] :
( ssSkP79(X1)
<=> $false ) ).
fof(ssSkP790,fi_predicates,
! [X1] :
( ssSkP790(X1)
<=> $true ) ).
fof(ssSkP791,fi_predicates,
! [X1] :
( ssSkP791(X1)
<=> $true ) ).
fof(ssSkP792,fi_predicates,
! [X1,X2] :
( ssSkP792(X1,X2)
<=> $true ) ).
fof(ssSkP793,fi_predicates,
! [X1,X2] :
( ssSkP793(X1,X2)
<=> $true ) ).
fof(ssSkP794,fi_predicates,
! [X1] :
( ssSkP794(X1)
<=> $true ) ).
fof(ssSkP795,fi_predicates,
! [X1] :
( ssSkP795(X1)
<=> $true ) ).
fof(ssSkP796,fi_predicates,
! [X1] :
( ssSkP796(X1)
<=> $true ) ).
fof(ssSkP797,fi_predicates,
! [X1] :
( ssSkP797(X1)
<=> $true ) ).
fof(ssSkP798,fi_predicates,
! [X1] :
( ssSkP798(X1)
<=> $true ) ).
fof(ssSkP799,fi_predicates,
! [X1] :
( ssSkP799(X1)
<=> $true ) ).
fof(ssSkP8,fi_predicates,
! [X1] :
( ssSkP8(X1)
<=> $false ) ).
fof(ssSkP80,fi_predicates,
! [X1] :
( ssSkP80(X1)
<=> $false ) ).
fof(ssSkP800,fi_predicates,
! [X1] :
( ssSkP800(X1)
<=> $true ) ).
fof(ssSkP801,fi_predicates,
! [X1] :
( ssSkP801(X1)
<=> $true ) ).
fof(ssSkP802,fi_predicates,
! [X1] :
( ssSkP802(X1)
<=> $true ) ).
fof(ssSkP803,fi_predicates,
! [X1] :
( ssSkP803(X1)
<=> $true ) ).
fof(ssSkP804,fi_predicates,
! [X1] :
( ssSkP804(X1)
<=> $true ) ).
fof(ssSkP805,fi_predicates,
! [X1] :
( ssSkP805(X1)
<=> $true ) ).
fof(ssSkP806,fi_predicates,
! [X1] :
( ssSkP806(X1)
<=> $true ) ).
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,
! [X1] :
( ssSkP81(X1)
<=> $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,
! [X1] :
( ssSkP82(X1)
<=> $false ) ).
fof(ssSkP820,fi_predicates,
! [X1] :
( ssSkP820(X1)
<=> $true ) ).
fof(ssSkP821,fi_predicates,
! [X1] :
( ssSkP821(X1)
<=> $true ) ).
fof(ssSkP822,fi_predicates,
! [X1] :
( ssSkP822(X1)
<=> $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,
! [X1] :
( ssSkP83(X1)
<=> $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,X2] :
( ssSkP833(X1,X2)
<=> $true ) ).
fof(ssSkP834,fi_predicates,
! [X1,X2] :
( ssSkP834(X1,X2)
<=> $true ) ).
fof(ssSkP835,fi_predicates,
! [X1] :
( ssSkP835(X1)
<=> $false ) ).
fof(ssSkP836,fi_predicates,
! [X1] :
( ssSkP836(X1)
<=> $false ) ).
fof(ssSkP837,fi_predicates,
! [X1] :
( ssSkP837(X1)
<=> $false ) ).
fof(ssSkP838,fi_predicates,
! [X1] :
( ssSkP838(X1)
<=> $false ) ).
fof(ssSkP839,fi_predicates,
! [X1] :
( ssSkP839(X1)
<=> $false ) ).
fof(ssSkP84,fi_predicates,
! [X1] :
( ssSkP84(X1)
<=> $false ) ).
fof(ssSkP840,fi_predicates,
! [X1] :
( ssSkP840(X1)
<=> $false ) ).
fof(ssSkP841,fi_predicates,
! [X1] :
( ssSkP841(X1)
<=> $false ) ).
fof(ssSkP842,fi_predicates,
! [X1] :
( ssSkP842(X1)
<=> $false ) ).
fof(ssSkP843,fi_predicates,
! [X1] :
( ssSkP843(X1)
<=> $false ) ).
fof(ssSkP844,fi_predicates,
! [X1] :
( ssSkP844(X1)
<=> $false ) ).
fof(ssSkP845,fi_predicates,
! [X1] :
( ssSkP845(X1)
<=> $false ) ).
fof(ssSkP846,fi_predicates,
! [X1] :
( ssSkP846(X1)
<=> $false ) ).
fof(ssSkP847,fi_predicates,
! [X1] :
( ssSkP847(X1)
<=> $false ) ).
fof(ssSkP848,fi_predicates,
! [X1] :
( ssSkP848(X1)
<=> $false ) ).
fof(ssSkP849,fi_predicates,
! [X1] :
( ssSkP849(X1)
<=> $false ) ).
fof(ssSkP85,fi_predicates,
! [X1] :
( ssSkP85(X1)
<=> $true ) ).
fof(ssSkP850,fi_predicates,
! [X1] :
( ssSkP850(X1)
<=> $false ) ).
fof(ssSkP851,fi_predicates,
! [X1] :
( ssSkP851(X1)
<=> $false ) ).
fof(ssSkP852,fi_predicates,
! [X1] :
( ssSkP852(X1)
<=> $true ) ).
fof(ssSkP853,fi_predicates,
! [X1] :
( ssSkP853(X1)
<=> $true ) ).
fof(ssSkP854,fi_predicates,
! [X1] :
( ssSkP854(X1)
<=> $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,
! [X1] :
( ssSkP86(X1)
<=> $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,
! [X1,X2] :
( ssSkP87(X1,X2)
<=> $true ) ).
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,X2] :
( ssSkP874(X1,X2)
<=> $true ) ).
fof(ssSkP875,fi_predicates,
! [X1,X2] :
( ssSkP875(X1,X2)
<=> $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,
! [X1,X2] :
( ssSkP88(X1,X2)
<=> $true ) ).
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,
! [X1] :
( ssSkP885(X1)
<=> $true ) ).
fof(ssSkP886,fi_predicates,
! [X1] :
( ssSkP886(X1)
<=> $true ) ).
fof(ssSkP887,fi_predicates,
! [X1] :
( ssSkP887(X1)
<=> $true ) ).
fof(ssSkP888,fi_predicates,
! [X1] :
( ssSkP888(X1)
<=> $true ) ).
fof(ssSkP889,fi_predicates,
! [X1] :
( ssSkP889(X1)
<=> $true ) ).
fof(ssSkP89,fi_predicates,
! [X1] :
( ssSkP89(X1)
<=> $false ) ).
fof(ssSkP890,fi_predicates,
! [X1] :
( ssSkP890(X1)
<=> $true ) ).
fof(ssSkP891,fi_predicates,
! [X1] :
( ssSkP891(X1)
<=> $true ) ).
fof(ssSkP892,fi_predicates,
! [X1] :
( ssSkP892(X1)
<=> $true ) ).
fof(ssSkP893,fi_predicates,
! [X1] :
( ssSkP893(X1)
<=> $true ) ).
fof(ssSkP894,fi_predicates,
! [X1] :
( ssSkP894(X1)
<=> $true ) ).
fof(ssSkP895,fi_predicates,
! [X1] :
( ssSkP895(X1)
<=> $true ) ).
fof(ssSkP896,fi_predicates,
! [X1] :
( ssSkP896(X1)
<=> $true ) ).
fof(ssSkP897,fi_predicates,
! [X1] :
( ssSkP897(X1)
<=> $true ) ).
fof(ssSkP898,fi_predicates,
! [X1] :
( ssSkP898(X1)
<=> $true ) ).
fof(ssSkP899,fi_predicates,
! [X1] :
( ssSkP899(X1)
<=> $true ) ).
fof(ssSkP9,fi_predicates,
! [X1] :
( ssSkP9(X1)
<=> $false ) ).
fof(ssSkP90,fi_predicates,
! [X1] :
( ssSkP90(X1)
<=> $false ) ).
fof(ssSkP900,fi_predicates,
! [X1] :
( ssSkP900(X1)
<=> $true ) ).
fof(ssSkP901,fi_predicates,
! [X1] :
( ssSkP901(X1)
<=> $true ) ).
fof(ssSkP902,fi_predicates,
! [X1] :
( ssSkP902(X1)
<=> $true ) ).
fof(ssSkP903,fi_predicates,
! [X1] :
( ssSkP903(X1)
<=> $true ) ).
fof(ssSkP904,fi_predicates,
! [X1] :
( ssSkP904(X1)
<=> $true ) ).
fof(ssSkP905,fi_predicates,
! [X1] :
( ssSkP905(X1)
<=> $true ) ).
fof(ssSkP906,fi_predicates,
! [X1] :
( ssSkP906(X1)
<=> $true ) ).
fof(ssSkP907,fi_predicates,
! [X1] :
( ssSkP907(X1)
<=> $true ) ).
fof(ssSkP908,fi_predicates,
! [X1] :
( ssSkP908(X1)
<=> $true ) ).
fof(ssSkP909,fi_predicates,
! [X1] :
( ssSkP909(X1)
<=> $true ) ).
fof(ssSkP91,fi_predicates,
! [X1] :
( ssSkP91(X1)
<=> $false ) ).
fof(ssSkP910,fi_predicates,
! [X1] :
( ssSkP910(X1)
<=> $true ) ).
fof(ssSkP911,fi_predicates,
! [X1] :
( ssSkP911(X1)
<=> $true ) ).
fof(ssSkP912,fi_predicates,
! [X1] :
( ssSkP912(X1)
<=> $true ) ).
fof(ssSkP913,fi_predicates,
! [X1] :
( ssSkP913(X1)
<=> $true ) ).
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,
! [X1] :
( ssSkP92(X1)
<=> $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,
! [X1] :
( ssSkP93(X1)
<=> $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)
<=> $false ) ).
fof(ssSkP934,fi_predicates,
! [X1] :
( ssSkP934(X1)
<=> $false ) ).
fof(ssSkP935,fi_predicates,
! [X1] :
( ssSkP935(X1)
<=> $false ) ).
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,
! [X1] :
( ssSkP94(X1)
<=> $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,
! [X1] :
( ssSkP946(X1)
<=> $true ) ).
fof(ssSkP947,fi_predicates,
! [X1] :
( ssSkP947(X1)
<=> $true ) ).
fof(ssSkP948,fi_predicates,
! [X1] :
( ssSkP948(X1)
<=> $true ) ).
fof(ssSkP949,fi_predicates,
! [X1] :
( ssSkP949(X1)
<=> $true ) ).
fof(ssSkP95,fi_predicates,
! [X1] :
( ssSkP95(X1)
<=> $false ) ).
fof(ssSkP950,fi_predicates,
! [X1] :
( ssSkP950(X1)
<=> $true ) ).
fof(ssSkP951,fi_predicates,
! [X1] :
( ssSkP951(X1)
<=> $true ) ).
fof(ssSkP952,fi_predicates,
! [X1] :
( ssSkP952(X1)
<=> $true ) ).
fof(ssSkP953,fi_predicates,
! [X1] :
( ssSkP953(X1)
<=> $true ) ).
fof(ssSkP954,fi_predicates,
! [X1] :
( ssSkP954(X1)
<=> $true ) ).
fof(ssSkP955,fi_predicates,
! [X1,X2] :
( ssSkP955(X1,X2)
<=> $true ) ).
fof(ssSkP956,fi_predicates,
! [X1,X2] :
( ssSkP956(X1,X2)
<=> $true ) ).
fof(ssSkP957,fi_predicates,
! [X1] :
( ssSkP957(X1)
<=> $false ) ).
fof(ssSkP958,fi_predicates,
! [X1] :
( ssSkP958(X1)
<=> $false ) ).
fof(ssSkP959,fi_predicates,
! [X1] :
( ssSkP959(X1)
<=> $false ) ).
fof(ssSkP96,fi_predicates,
! [X1] :
( ssSkP96(X1)
<=> $false ) ).
fof(ssSkP960,fi_predicates,
! [X1] :
( ssSkP960(X1)
<=> $false ) ).
fof(ssSkP961,fi_predicates,
! [X1] :
( ssSkP961(X1)
<=> $false ) ).
fof(ssSkP962,fi_predicates,
! [X1] :
( ssSkP962(X1)
<=> $false ) ).
fof(ssSkP963,fi_predicates,
! [X1] :
( ssSkP963(X1)
<=> $false ) ).
fof(ssSkP964,fi_predicates,
! [X1] :
( ssSkP964(X1)
<=> $false ) ).
fof(ssSkP965,fi_predicates,
! [X1] :
( ssSkP965(X1)
<=> $false ) ).
fof(ssSkP966,fi_predicates,
! [X1] :
( ssSkP966(X1)
<=> $false ) ).
fof(ssSkP967,fi_predicates,
! [X1] :
( ssSkP967(X1)
<=> $true ) ).
fof(ssSkP968,fi_predicates,
! [X1] :
( ssSkP968(X1)
<=> $true ) ).
fof(ssSkP969,fi_predicates,
! [X1] :
( ssSkP969(X1)
<=> $true ) ).
fof(ssSkP97,fi_predicates,
! [X1] :
( ssSkP97(X1)
<=> $false ) ).
fof(ssSkP970,fi_predicates,
! [X1] :
( ssSkP970(X1)
<=> $true ) ).
fof(ssSkP971,fi_predicates,
! [X1] :
( ssSkP971(X1)
<=> $true ) ).
fof(ssSkP972,fi_predicates,
! [X1] :
( ssSkP972(X1)
<=> $true ) ).
fof(ssSkP973,fi_predicates,
! [X1] :
( ssSkP973(X1)
<=> $true ) ).
fof(ssSkP974,fi_predicates,
! [X1] :
( ssSkP974(X1)
<=> $true ) ).
fof(ssSkP975,fi_predicates,
! [X1] :
( ssSkP975(X1)
<=> $true ) ).
fof(ssSkP976,fi_predicates,
! [X1] :
( ssSkP976(X1)
<=> $true ) ).
fof(ssSkP977,fi_predicates,
! [X1] :
( ssSkP977(X1)
<=> $true ) ).
fof(ssSkP978,fi_predicates,
! [X1] :
( ssSkP978(X1)
<=> $true ) ).
fof(ssSkP979,fi_predicates,
! [X1] :
( ssSkP979(X1)
<=> $true ) ).
fof(ssSkP98,fi_predicates,
! [X1] :
( ssSkP98(X1)
<=> $false ) ).
fof(ssSkP980,fi_predicates,
! [X1] :
( ssSkP980(X1)
<=> $true ) ).
fof(ssSkP981,fi_predicates,
! [X1] :
( ssSkP981(X1)
<=> $true ) ).
fof(ssSkP982,fi_predicates,
! [X1] :
( ssSkP982(X1)
<=> $true ) ).
fof(ssSkP983,fi_predicates,
! [X1] :
( ssSkP983(X1)
<=> $true ) ).
fof(ssSkP984,fi_predicates,
! [X1] :
( ssSkP984(X1)
<=> $true ) ).
fof(ssSkP985,fi_predicates,
! [X1] :
( ssSkP985(X1)
<=> $true ) ).
fof(ssSkP986,fi_predicates,
! [X1] :
( ssSkP986(X1)
<=> $true ) ).
fof(ssSkP987,fi_predicates,
! [X1,X2] :
( ssSkP987(X1,X2)
<=> $true ) ).
fof(ssSkP988,fi_predicates,
! [X1,X2] :
( ssSkP988(X1,X2)
<=> $true ) ).
fof(ssSkP989,fi_predicates,
! [X1] :
( ssSkP989(X1)
<=> $false ) ).
fof(ssSkP99,fi_predicates,
! [X1] :
( ssSkP99(X1)
<=> $false ) ).
fof(ssSkP990,fi_predicates,
! [X1] :
( ssSkP990(X1)
<=> $false ) ).
fof(ssSkP991,fi_predicates,
! [X1] :
( ssSkP991(X1)
<=> $false ) ).
fof(ssSkP992,fi_predicates,
! [X1] :
( ssSkP992(X1)
<=> $false ) ).
fof(ssSkP993,fi_predicates,
! [X1] :
( ssSkP993(X1)
<=> $false ) ).
fof(ssSkP994,fi_predicates,
! [X1] :
( ssSkP994(X1)
<=> $true ) ).
fof(ssSkP995,fi_predicates,
! [X1] :
( ssSkP995(X1)
<=> $true ) ).
fof(ssSkP996,fi_predicates,
! [X1] :
( ssSkP996(X1)
<=> $true ) ).
fof(ssSkP997,fi_predicates,
! [X1] :
( ssSkP997(X1)
<=> $true ) ).
fof(ssSkP998,fi_predicates,
! [X1] :
( ssSkP998(X1)
<=> $true ) ).
fof(ssSkP999,fi_predicates,
! [X1] :
( ssSkP999(X1)
<=> $true ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN912-1 : TPTP v8.1.0. Released v2.5.0.
% 0.06/0.12 % Command : paradox --no-progress --time %d --tstp --model %s
% 0.12/0.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jul 12 08:12:44 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.34 Paradox, version 4.0, 2010-06-29.
% 0.12/0.34 +++ PROBLEM: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 Reading '/export/starexec/sandbox/benchmark/theBenchmark.p' ... OK
% 0.46/0.67 +++ SOLVING: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.71/1.87 +++ BEGIN MODEL
% 1.71/1.87 SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 1.72/1.91 +++ END MODEL
% 1.72/1.91 +++ RESULT: Satisfiable
% 1.72/1.91 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------