%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN742-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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 : 300s
% DateTime : Thu May 9 17:48:47 EDT 2024
% Result : Satisfiable 4.11s 4.35s
% Output : Saturation 4.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(X2,skf1(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X412,X414)
| ~ ssPv4(X414)
| ~ ssRr(X410,X412)
| ~ ssRr(X411,X409)
| ~ ssPv3(X409)
| ~ ssRr(X410,X411)
| ~ ssRr(X413,X415)
| ~ ssPv1(X415)
| ~ ssRr(X410,X413)
| ssPv2(X410) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c218,plain,
( ~ ssRr(X1538,X1539)
| ~ ssPv4(X1539)
| ~ ssRr(X1537,X1538)
| ~ ssRr(X1536,X1535)
| ~ ssPv3(X1535)
| ~ ssRr(X1537,X1536)
| ~ ssRr(X1536,X1540)
| ~ ssPv1(X1540)
| ssPv2(X1537) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c727,plain,
( ~ ssRr(X2993,X2990)
| ~ ssPv4(X2990)
| ~ ssRr(X2992,X2993)
| ~ ssRr(X2989,X2991)
| ~ ssPv3(X2991)
| ~ ssRr(X2992,X2989)
| ~ ssPv1(X2991)
| ssPv2(X2992) ),
inference(factor,[status(thm)],[c218]) ).
cnf(c1223,plain,
( ~ ssRr(X3007,X3006)
| ~ ssPv4(X3006)
| ~ ssRr(X3009,X3007)
| ~ ssRr(skf1(X3009),X3008)
| ~ ssPv3(X3008)
| ~ ssPv1(X3008)
| ssPv2(X3009) ),
inference(resolution,[status(thm)],[c727,clause1]) ).
cnf(c1225,plain,
( ~ ssRr(X3289,X3288)
| ~ ssPv4(X3288)
| ~ ssRr(X3290,X3289)
| ~ ssPv3(skf1(skf1(X3290)))
| ~ ssPv1(skf1(skf1(X3290)))
| ssPv2(X3290) ),
inference(resolution,[status(thm)],[c1223,clause1]) ).
cnf(c216,plain,
( ~ ssRr(X1507,X1510)
| ~ ssPv4(X1510)
| ~ ssRr(X1508,X1507)
| ~ ssRr(X1509,X1506)
| ~ ssPv3(X1506)
| ~ ssRr(X1508,X1509)
| ~ ssRr(X1507,X1511)
| ~ ssPv1(X1511)
| ssPv2(X1508) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c711,plain,
( ~ ssRr(X2924,X2921)
| ~ ssPv4(X2921)
| ~ ssRr(X2924,X2924)
| ~ ssRr(X2923,X2922)
| ~ ssPv3(X2922)
| ~ ssRr(X2924,X2923)
| ~ ssPv1(X2923)
| ssPv2(X2924) ),
inference(factor,[status(thm)],[c216]) ).
cnf(c1209,plain,
( ~ ssRr(X3285,X3284)
| ~ ssPv4(X3284)
| ~ ssRr(X3285,X3285)
| ~ ssRr(skf1(X3285),X3283)
| ~ ssPv3(X3283)
| ~ ssPv1(skf1(X3285))
| ssPv2(X3285) ),
inference(resolution,[status(thm)],[c711,clause1]) ).
cnf(c1305,plain,
( ~ ssRr(X3286,X3287)
| ~ ssPv4(X3287)
| ~ ssRr(X3286,X3286)
| ~ ssPv3(skf1(skf1(X3286)))
| ~ ssPv1(skf1(X3286))
| ssPv2(X3286) ),
inference(resolution,[status(thm)],[c1209,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X395,X397)
| ~ ssPv4(X397)
| ~ ssRr(X393,X395)
| ~ ssRr(X394,X392)
| ~ ssRr(X393,X394)
| ~ ssRr(X396,X398)
| ~ ssRr(X393,X396)
| ~ ssPv2(X393)
| ssPv3(X392)
| ssPv2(X398) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c211,plain,
( ~ ssRr(X1442,X1445)
| ~ ssPv4(X1445)
| ~ ssRr(X1441,X1442)
| ~ ssRr(X1446,X1443)
| ~ ssRr(X1441,X1446)
| ~ ssRr(X1446,X1444)
| ~ ssPv2(X1441)
| ssPv3(X1443)
| ssPv2(X1444) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c682,plain,
( ~ ssRr(X2784,X2788)
| ~ ssPv4(X2788)
| ~ ssRr(X2786,X2784)
| ~ ssRr(X2785,X2787)
| ~ ssRr(X2786,X2785)
| ~ ssPv2(X2786)
| ssPv3(X2787)
| ssPv2(X2787) ),
inference(factor,[status(thm)],[c211]) ).
cnf(c1159,plain,
( ~ ssRr(X2889,X2888)
| ~ ssPv4(X2888)
| ~ ssRr(X2890,X2889)
| ~ ssRr(skf1(X2890),X2887)
| ~ ssPv2(X2890)
| ssPv3(X2887)
| ssPv2(X2887) ),
inference(resolution,[status(thm)],[c682,clause1]) ).
cnf(c1192,plain,
( ~ ssRr(X3279,X3278)
| ~ ssPv4(X3278)
| ~ ssRr(X3277,X3279)
| ~ ssPv2(X3277)
| ssPv3(skf1(skf1(X3277)))
| ssPv2(skf1(skf1(X3277))) ),
inference(resolution,[status(thm)],[c1159,clause1]) ).
cnf(c1303,plain,
( ~ ssRr(X3280,X3280)
| ~ ssPv4(X3280)
| ~ ssPv2(X3280)
| ssPv3(skf1(skf1(X3280)))
| ssPv2(skf1(skf1(X3280))) ),
inference(factor,[status(thm)],[c1192]) ).
cnf(c213,plain,
( ~ ssRr(X1475,X1478)
| ~ ssPv4(X1478)
| ~ ssRr(X1480,X1475)
| ~ ssRr(X1479,X1476)
| ~ ssRr(X1480,X1479)
| ~ ssRr(skf1(X1480),X1477)
| ~ ssPv2(X1480)
| ssPv3(X1476)
| ssPv2(X1477) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c694,plain,
( ~ ssRr(X2863,X2862)
| ~ ssPv4(X2862)
| ~ ssRr(X2860,X2863)
| ~ ssRr(X2861,X2859)
| ~ ssRr(X2860,X2861)
| ~ ssPv2(X2860)
| ssPv3(X2859)
| ssPv2(skf1(skf1(X2860))) ),
inference(resolution,[status(thm)],[c213,clause1]) ).
cnf(c1181,plain,
( ~ ssRr(X3248,X3249)
| ~ ssPv4(X3249)
| ~ ssRr(X3251,X3248)
| ~ ssRr(X3248,X3250)
| ~ ssPv2(X3251)
| ssPv3(X3250)
| ssPv2(skf1(skf1(X3251))) ),
inference(factor,[status(thm)],[c694]) ).
cnf(c1295,plain,
( ~ ssRr(X3273,X3271)
| ~ ssPv4(X3271)
| ~ ssRr(X3272,X3273)
| ~ ssPv2(X3272)
| ssPv3(skf1(X3273))
| ssPv2(skf1(skf1(X3272))) ),
inference(resolution,[status(thm)],[c1181,clause1]) ).
cnf(c1294,plain,
( ~ ssRr(X3263,X3262)
| ~ ssPv4(X3262)
| ~ ssRr(X3263,X3263)
| ~ ssPv2(X3263)
| ssPv3(X3263)
| ssPv2(skf1(skf1(X3263))) ),
inference(factor,[status(thm)],[c1181]) ).
cnf(c1293,plain,
( ~ ssRr(X3256,X3257)
| ~ ssPv4(X3257)
| ~ ssRr(X3258,X3256)
| ~ ssPv2(X3258)
| ssPv3(X3257)
| ssPv2(skf1(skf1(X3258))) ),
inference(factor,[status(thm)],[c1181]) ).
cnf(c1182,plain,
( ~ ssRr(X3252,X3253)
| ~ ssPv4(X3253)
| ~ ssRr(X3254,X3252)
| ~ ssRr(X3254,X3254)
| ~ ssPv2(X3254)
| ssPv3(X3254)
| ssPv2(skf1(skf1(X3254))) ),
inference(factor,[status(thm)],[c694]) ).
cnf(c1180,plain,
( ~ ssRr(X3238,X3236)
| ~ ssPv4(X3236)
| ~ ssRr(X3238,X3238)
| ~ ssRr(X3236,X3237)
| ~ ssPv2(X3238)
| ssPv3(X3237)
| ssPv2(skf1(skf1(X3238))) ),
inference(factor,[status(thm)],[c694]) ).
cnf(c1289,plain,
( ~ ssRr(X3245,X3246)
| ~ ssPv4(X3246)
| ~ ssRr(X3245,X3245)
| ~ ssPv2(X3245)
| ssPv3(skf1(X3246))
| ssPv2(skf1(skf1(X3245))) ),
inference(resolution,[status(thm)],[c1180,clause1]) ).
cnf(c1287,plain,
( ~ ssRr(X3243,X3243)
| ~ ssPv4(X3243)
| ~ ssPv2(X3243)
| ssPv3(X3243)
| ssPv2(skf1(skf1(X3243))) ),
inference(factor,[status(thm)],[c1180]) ).
cnf(c684,plain,
( ~ ssRr(X2818,X2822)
| ~ ssPv4(X2822)
| ~ ssRr(X2820,X2818)
| ~ ssRr(X2821,X2819)
| ~ ssRr(X2820,X2821)
| ~ ssPv2(X2820)
| ssPv3(X2819)
| ssPv2(skf1(X2821)) ),
inference(resolution,[status(thm)],[c211,clause1]) ).
cnf(c1168,plain,
( ~ ssRr(X3241,X3240)
| ~ ssPv4(X3240)
| ~ ssRr(X3242,X3241)
| ~ ssRr(skf1(X3242),X3239)
| ~ ssPv2(X3242)
| ssPv3(X3239)
| ssPv2(skf1(skf1(X3242))) ),
inference(resolution,[status(thm)],[c684,clause1]) ).
cnf(c209,plain,
( ~ ssRr(X1411,X1409)
| ~ ssPv4(X1409)
| ~ ssRr(X1406,X1411)
| ~ ssRr(X1410,X1407)
| ~ ssRr(X1406,X1410)
| ~ ssRr(X1411,X1408)
| ~ ssPv2(X1406)
| ssPv3(X1407)
| ssPv2(X1408) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c665,plain,
( ~ ssRr(X2741,X2740)
| ~ ssPv4(X2740)
| ~ ssRr(X2742,X2741)
| ~ ssRr(X2739,X2738)
| ~ ssRr(X2742,X2739)
| ~ ssPv2(X2742)
| ssPv3(X2738)
| ssPv2(skf1(X2741)) ),
inference(resolution,[status(thm)],[c209,clause1]) ).
cnf(c1140,plain,
( ~ ssRr(X3226,X3225)
| ~ ssPv4(X3225)
| ~ ssRr(X3228,X3226)
| ~ ssRr(skf1(X3228),X3227)
| ~ ssPv2(X3228)
| ssPv3(X3227)
| ssPv2(skf1(X3226)) ),
inference(resolution,[status(thm)],[c665,clause1]) ).
cnf(c1284,plain,
( ~ ssRr(X3231,X3230)
| ~ ssPv4(X3230)
| ~ ssRr(X3232,X3231)
| ~ ssPv2(X3232)
| ssPv3(skf1(skf1(X3232)))
| ssPv2(skf1(X3231)) ),
inference(resolution,[status(thm)],[c1140,clause1]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X379,X381)
| ~ ssPv4(X381)
| ~ ssRr(X377,X379)
| ~ ssRr(X378,X376)
| ~ ssPv3(X376)
| ~ ssRr(X377,X378)
| ~ ssRr(X380,X382)
| ~ ssRr(X377,X380)
| ssPv4(X382)
| ssPv3(X377) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(c202,plain,
( ~ ssRr(X1342,X1343)
| ~ ssPv4(X1343)
| ~ ssRr(X1340,X1342)
| ~ ssRr(X1339,X1338)
| ~ ssPv3(X1338)
| ~ ssRr(X1340,X1339)
| ~ ssRr(X1339,X1341)
| ssPv4(X1341)
| ssPv3(X1340) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c637,plain,
( ~ ssRr(X2585,X2583)
| ~ ssPv4(X2583)
| ~ ssRr(X2582,X2585)
| ~ ssRr(X2584,X2581)
| ~ ssPv3(X2581)
| ~ ssRr(X2582,X2584)
| ssPv4(X2581)
| ssPv3(X2582) ),
inference(factor,[status(thm)],[c202]) ).
cnf(c1087,plain,
( ~ ssRr(X2718,X2719)
| ~ ssPv4(X2719)
| ~ ssRr(X2720,X2718)
| ~ ssRr(skf1(X2720),X2717)
| ~ ssPv3(X2717)
| ssPv4(X2717)
| ssPv3(X2720) ),
inference(resolution,[status(thm)],[c637,clause1]) ).
cnf(c1132,plain,
( ~ ssRr(X3218,X3217)
| ~ ssPv4(X3217)
| ~ ssRr(X3219,X3218)
| ~ ssPv3(skf1(skf1(X3219)))
| ssPv4(skf1(skf1(X3219)))
| ssPv3(X3219) ),
inference(resolution,[status(thm)],[c1087,clause1]) ).
cnf(c208,plain,
( ~ ssRr(X1388,X1392)
| ~ ssPv4(X1392)
| ~ ssRr(X1388,X1388)
| ~ ssRr(X1391,X1389)
| ~ ssRr(X1388,X1391)
| ~ ssRr(X1392,X1390)
| ~ ssPv2(X1388)
| ssPv3(X1389)
| ssPv2(X1390) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c657,plain,
( ~ ssRr(X2679,X2678)
| ~ ssPv4(X2678)
| ~ ssRr(X2679,X2679)
| ~ ssRr(X2677,X2676)
| ~ ssRr(X2679,X2677)
| ~ ssPv2(X2679)
| ssPv3(X2676)
| ssPv2(skf1(X2678)) ),
inference(resolution,[status(thm)],[c208,clause1]) ).
cnf(c1119,plain,
( ~ ssRr(X3209,X3207)
| ~ ssPv4(X3207)
| ~ ssRr(X3209,X3209)
| ~ ssRr(skf1(X3209),X3208)
| ~ ssPv2(X3209)
| ssPv3(X3208)
| ssPv2(skf1(X3207)) ),
inference(resolution,[status(thm)],[c657,clause1]) ).
cnf(c1279,plain,
( ~ ssRr(X3214,X3215)
| ~ ssPv4(X3215)
| ~ ssRr(X3214,X3214)
| ~ ssPv2(X3214)
| ssPv3(skf1(skf1(X3214)))
| ssPv2(skf1(X3215)) ),
inference(resolution,[status(thm)],[c1119,clause1]) ).
cnf(c204,plain,
( ~ ssRr(X1373,X1374)
| ~ ssPv4(X1374)
| ~ ssRr(X1375,X1373)
| ~ ssRr(X1371,X1370)
| ~ ssPv3(X1370)
| ~ ssRr(X1375,X1371)
| ~ ssRr(skf1(X1375),X1372)
| ssPv4(X1372)
| ssPv3(X1375) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(c650,plain,
( ~ ssRr(X2663,X2664)
| ~ ssPv4(X2664)
| ~ ssRr(X2665,X2663)
| ~ ssRr(X2661,X2662)
| ~ ssPv3(X2662)
| ~ ssRr(X2665,X2661)
| ssPv4(skf1(skf1(X2665)))
| ssPv3(X2665) ),
inference(resolution,[status(thm)],[c204,clause1]) ).
cnf(c1109,plain,
( ~ ssRr(X3192,X3190)
| ~ ssPv4(X3190)
| ~ ssRr(X3191,X3192)
| ~ ssRr(X3192,X3189)
| ~ ssPv3(X3189)
| ssPv4(skf1(skf1(X3191)))
| ssPv3(X3191) ),
inference(factor,[status(thm)],[c650]) ).
cnf(c1276,plain,
( ~ ssRr(X3206,X3205)
| ~ ssPv4(X3205)
| ~ ssRr(X3204,X3206)
| ~ ssPv3(skf1(X3206))
| ssPv4(skf1(skf1(X3204)))
| ssPv3(X3204) ),
inference(resolution,[status(thm)],[c1109,clause1]) ).
cnf(c1274,plain,
( ~ ssRr(X3195,X3194)
| ~ ssPv4(X3194)
| ~ ssRr(X3193,X3195)
| ~ ssPv3(X3194)
| ssPv4(skf1(skf1(X3193)))
| ssPv3(X3193) ),
inference(factor,[status(thm)],[c1109]) ).
cnf(c1108,plain,
( ~ ssRr(X3179,X3180)
| ~ ssPv4(X3180)
| ~ ssRr(X3179,X3179)
| ~ ssRr(X3180,X3178)
| ~ ssPv3(X3178)
| ssPv4(skf1(skf1(X3179)))
| ssPv3(X3179) ),
inference(factor,[status(thm)],[c650]) ).
cnf(c1271,plain,
( ~ ssRr(X3187,X3188)
| ~ ssPv4(X3188)
| ~ ssRr(X3187,X3187)
| ~ ssPv3(skf1(X3188))
| ssPv4(skf1(skf1(X3187)))
| ssPv3(X3187) ),
inference(resolution,[status(thm)],[c1108,clause1]) ).
cnf(c639,plain,
( ~ ssRr(X2620,X2617)
| ~ ssPv4(X2617)
| ~ ssRr(X2616,X2620)
| ~ ssRr(X2619,X2618)
| ~ ssPv3(X2618)
| ~ ssRr(X2616,X2619)
| ssPv4(skf1(X2619))
| ssPv3(X2616) ),
inference(resolution,[status(thm)],[c202,clause1]) ).
cnf(c1094,plain,
( ~ ssRr(X3183,X3182)
| ~ ssPv4(X3182)
| ~ ssRr(X3184,X3183)
| ~ ssRr(skf1(X3184),X3181)
| ~ ssPv3(X3181)
| ssPv4(skf1(skf1(X3184)))
| ssPv3(X3184) ),
inference(resolution,[status(thm)],[c639,clause1]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X361,X363)
| ~ ssPv3(X363)
| ~ ssRr(X359,X361)
| ~ ssRr(X360,X358)
| ~ ssRr(X359,X360)
| ~ ssRr(X362,X364)
| ~ ssRr(X359,X362)
| ssPv4(X358)
| ssPv2(X364)
| ssPv3(X359) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c190,plain,
( ~ ssRr(X1241,X1243)
| ~ ssPv3(X1243)
| ~ ssRr(X1240,X1241)
| ~ ssRr(X1242,X1244)
| ~ ssRr(X1240,X1242)
| ~ ssRr(X1242,X1245)
| ssPv4(X1244)
| ssPv2(X1245)
| ssPv3(X1240) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c589,plain,
( ~ ssRr(X2345,X2346)
| ~ ssPv3(X2346)
| ~ ssRr(X2348,X2345)
| ~ ssRr(X2344,X2347)
| ~ ssRr(X2348,X2344)
| ssPv4(X2347)
| ssPv2(X2347)
| ssPv3(X2348) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c1008,plain,
( ~ ssRr(X2561,X2560)
| ~ ssPv3(X2560)
| ~ ssRr(X2563,X2561)
| ~ ssRr(skf1(X2563),X2562)
| ssPv4(X2562)
| ssPv2(X2562)
| ssPv3(X2563) ),
inference(resolution,[status(thm)],[c589,clause1]) ).
cnf(c1080,plain,
( ~ ssRr(X3172,X3173)
| ~ ssPv3(X3173)
| ~ ssRr(X3174,X3172)
| ssPv4(skf1(skf1(X3174)))
| ssPv2(skf1(skf1(X3174)))
| ssPv3(X3174) ),
inference(resolution,[status(thm)],[c1008,clause1]) ).
cnf(c200,plain,
( ~ ssRr(X1304,X1307)
| ~ ssPv4(X1307)
| ~ ssRr(X1305,X1304)
| ~ ssRr(X1303,X1302)
| ~ ssPv3(X1302)
| ~ ssRr(X1305,X1303)
| ~ ssRr(X1304,X1306)
| ssPv4(X1306)
| ssPv3(X1305) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c624,plain,
( ~ ssRr(X2537,X2536)
| ~ ssPv4(X2536)
| ~ ssRr(X2534,X2537)
| ~ ssRr(X2535,X2538)
| ~ ssPv3(X2538)
| ~ ssRr(X2534,X2535)
| ssPv4(skf1(X2537))
| ssPv3(X2534) ),
inference(resolution,[status(thm)],[c200,clause1]) ).
cnf(c1068,plain,
( ~ ssRr(X3165,X3167)
| ~ ssPv4(X3167)
| ~ ssRr(X3168,X3165)
| ~ ssRr(skf1(X3168),X3166)
| ~ ssPv3(X3166)
| ssPv4(skf1(X3165))
| ssPv3(X3168) ),
inference(resolution,[status(thm)],[c624,clause1]) ).
cnf(c1266,plain,
( ~ ssRr(X3169,X3170)
| ~ ssPv4(X3170)
| ~ ssRr(X3171,X3169)
| ~ ssPv3(skf1(skf1(X3171)))
| ssPv4(skf1(X3169))
| ssPv3(X3171) ),
inference(resolution,[status(thm)],[c1068,clause1]) ).
cnf(c199,plain,
( ~ ssRr(X1290,X1289)
| ~ ssPv4(X1289)
| ~ ssRr(X1290,X1290)
| ~ ssRr(X1288,X1287)
| ~ ssPv3(X1287)
| ~ ssRr(X1290,X1288)
| ~ ssRr(X1289,X1291)
| ssPv4(X1291)
| ssPv3(X1290) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c616,plain,
( ~ ssRr(X2478,X2479)
| ~ ssPv4(X2479)
| ~ ssRr(X2478,X2478)
| ~ ssRr(X2476,X2477)
| ~ ssPv3(X2477)
| ~ ssRr(X2478,X2476)
| ssPv4(skf1(X2479))
| ssPv3(X2478) ),
inference(resolution,[status(thm)],[c199,clause1]) ).
cnf(c1047,plain,
( ~ ssRr(X3157,X3156)
| ~ ssPv4(X3156)
| ~ ssRr(X3157,X3157)
| ~ ssRr(skf1(X3157),X3155)
| ~ ssPv3(X3155)
| ssPv4(skf1(X3156))
| ssPv3(X3157) ),
inference(resolution,[status(thm)],[c616,clause1]) ).
cnf(c1263,plain,
( ~ ssRr(X3158,X3159)
| ~ ssPv4(X3159)
| ~ ssRr(X3158,X3158)
| ~ ssPv3(skf1(skf1(X3158)))
| ssPv4(skf1(X3159))
| ssPv3(X3158) ),
inference(resolution,[status(thm)],[c1047,clause1]) ).
cnf(c192,plain,
( ~ ssRr(X1270,X1271)
| ~ ssPv3(X1271)
| ~ ssRr(X1274,X1270)
| ~ ssRr(X1272,X1273)
| ~ ssRr(X1274,X1272)
| ~ ssRr(skf1(X1274),X1275)
| ssPv4(X1273)
| ssPv2(X1275)
| ssPv3(X1274) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(c605,plain,
( ~ ssRr(X2462,X2464)
| ~ ssPv3(X2464)
| ~ ssRr(X2465,X2462)
| ~ ssRr(X2463,X2466)
| ~ ssRr(X2465,X2463)
| ssPv4(X2466)
| ssPv2(skf1(skf1(X2465)))
| ssPv3(X2465) ),
inference(resolution,[status(thm)],[c192,clause1]) ).
cnf(c1039,plain,
( ~ ssRr(X3127,X3128)
| ~ ssPv3(X3128)
| ~ ssRr(X3129,X3127)
| ~ ssRr(X3127,X3126)
| ssPv4(X3126)
| ssPv2(skf1(skf1(X3129)))
| ssPv3(X3129) ),
inference(factor,[status(thm)],[c605]) ).
cnf(c1255,plain,
( ~ ssRr(X3147,X3145)
| ~ ssPv3(X3145)
| ~ ssRr(X3146,X3147)
| ssPv4(skf1(X3147))
| ssPv2(skf1(skf1(X3146)))
| ssPv3(X3146) ),
inference(resolution,[status(thm)],[c1039,clause1]) ).
cnf(c1040,plain,
( ~ ssRr(X3140,X3138)
| ~ ssPv3(X3138)
| ~ ssRr(X3139,X3140)
| ~ ssRr(X3139,X3139)
| ssPv4(X3139)
| ssPv2(skf1(skf1(X3139)))
| ssPv3(X3139) ),
inference(factor,[status(thm)],[c605]) ).
cnf(c1254,plain,
( ~ ssRr(X3137,X3136)
| ~ ssPv3(X3136)
| ~ ssRr(X3137,X3137)
| ssPv4(X3137)
| ssPv2(skf1(skf1(X3137)))
| ssPv3(X3137) ),
inference(factor,[status(thm)],[c1039]) ).
cnf(c1253,plain,
( ~ ssRr(X3131,X3132)
| ~ ssPv3(X3132)
| ~ ssRr(X3130,X3131)
| ssPv4(X3132)
| ssPv2(skf1(skf1(X3130)))
| ssPv3(X3130) ),
inference(factor,[status(thm)],[c1039]) ).
cnf(c591,plain,
( ~ ssRr(X2379,X2380)
| ~ ssPv3(X2380)
| ~ ssRr(X2383,X2379)
| ~ ssRr(X2382,X2381)
| ~ ssRr(X2383,X2382)
| ssPv4(X2381)
| ssPv2(skf1(X2382))
| ssPv3(X2383) ),
inference(resolution,[status(thm)],[c190,clause1]) ).
cnf(c1017,plain,
( ~ ssRr(X3123,X3125)
| ~ ssPv3(X3125)
| ~ ssRr(X3124,X3123)
| ~ ssRr(skf1(X3124),X3122)
| ssPv4(X3122)
| ssPv2(skf1(skf1(X3124)))
| ssPv3(X3124) ),
inference(resolution,[status(thm)],[c591,clause1]) ).
cnf(c1038,plain,
( ~ ssRr(X3116,X3115)
| ~ ssPv3(X3115)
| ~ ssRr(X3116,X3116)
| ~ ssRr(X3115,X3114)
| ssPv4(X3114)
| ssPv2(skf1(skf1(X3116)))
| ssPv3(X3116) ),
inference(factor,[status(thm)],[c605]) ).
cnf(c1249,plain,
( ~ ssRr(X3119,X3120)
| ~ ssPv3(X3120)
| ~ ssRr(X3119,X3119)
| ssPv4(skf1(X3120))
| ssPv2(skf1(skf1(X3119)))
| ssPv3(X3119) ),
inference(resolution,[status(thm)],[c1038,clause1]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X344,X346)
| ~ ssPv4(X346)
| ~ ssRr(X342,X344)
| ~ ssRr(X343,X341)
| ~ ssRr(X342,X343)
| ~ ssRr(X345,X347)
| ~ ssRr(X342,X345)
| ssPv4(X341)
| ssPv1(X347)
| ssPv4(X342) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c179,plain,
( ~ ssRr(X1147,X1145)
| ~ ssPv4(X1145)
| ~ ssRr(X1148,X1147)
| ~ ssRr(X1144,X1143)
| ~ ssRr(X1148,X1144)
| ~ ssRr(X1144,X1146)
| ssPv4(X1143)
| ssPv1(X1146)
| ssPv4(X1148) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c546,plain,
( ~ ssRr(X2152,X2151)
| ~ ssPv4(X2151)
| ~ ssRr(X2153,X2152)
| ~ ssRr(X2155,X2154)
| ~ ssRr(X2153,X2155)
| ssPv4(X2154)
| ssPv1(X2154)
| ssPv4(X2153) ),
inference(factor,[status(thm)],[c179]) ).
cnf(c941,plain,
( ~ ssRr(X2412,X2411)
| ~ ssPv4(X2411)
| ~ ssRr(X2413,X2412)
| ~ ssRr(skf1(X2413),X2410)
| ssPv4(X2410)
| ssPv1(X2410)
| ssPv4(X2413) ),
inference(resolution,[status(thm)],[c546,clause1]) ).
cnf(c1025,plain,
( ~ ssRr(X3106,X3105)
| ~ ssPv4(X3105)
| ~ ssRr(X3104,X3106)
| ssPv4(skf1(skf1(X3104)))
| ssPv1(skf1(skf1(X3104)))
| ssPv4(X3104) ),
inference(resolution,[status(thm)],[c941,clause1]) ).
cnf(c548,plain,
( ~ ssRr(X2185,X2183)
| ~ ssPv4(X2183)
| ~ ssRr(X2186,X2185)
| ~ ssRr(X2187,X2184)
| ~ ssRr(X2186,X2187)
| ssPv4(X2184)
| ssPv1(skf1(X2187))
| ssPv4(X2186) ),
inference(resolution,[status(thm)],[c179,clause1]) ).
cnf(c948,plain,
( ~ ssRr(X3098,X3099)
| ~ ssPv4(X3099)
| ~ ssRr(X3100,X3098)
| ~ ssRr(skf1(X3100),X3097)
| ssPv4(X3097)
| ssPv1(skf1(skf1(X3100)))
| ssPv4(X3100) ),
inference(resolution,[status(thm)],[c548,clause1]) ).
cnf(c188,plain,
( ~ ssRr(X1207,X1208)
| ~ ssPv3(X1208)
| ~ ssRr(X1206,X1207)
| ~ ssRr(X1209,X1210)
| ~ ssRr(X1206,X1209)
| ~ ssRr(X1207,X1211)
| ssPv4(X1210)
| ssPv2(X1211)
| ssPv3(X1206) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c577,plain,
( ~ ssRr(X2299,X2296)
| ~ ssPv3(X2296)
| ~ ssRr(X2298,X2299)
| ~ ssRr(X2297,X2300)
| ~ ssRr(X2298,X2297)
| ssPv4(X2300)
| ssPv2(skf1(X2299))
| ssPv3(X2298) ),
inference(resolution,[status(thm)],[c188,clause1]) ).
cnf(c991,plain,
( ~ ssRr(X3091,X3092)
| ~ ssPv3(X3092)
| ~ ssRr(X3093,X3091)
| ~ ssRr(skf1(X3093),X3090)
| ssPv4(X3090)
| ssPv2(skf1(X3091))
| ssPv3(X3093) ),
inference(resolution,[status(thm)],[c577,clause1]) ).
cnf(c1240,plain,
( ~ ssRr(X3095,X3096)
| ~ ssPv3(X3096)
| ~ ssRr(X3094,X3095)
| ssPv4(skf1(skf1(X3094)))
| ssPv2(skf1(X3095))
| ssPv3(X3094) ),
inference(resolution,[status(thm)],[c991,clause1]) ).
cnf(c220,plain,
( ~ ssRr(X1574,X1575)
| ~ ssPv4(X1575)
| ~ ssRr(X1576,X1574)
| ~ ssRr(X1573,X1572)
| ~ ssPv3(X1572)
| ~ ssRr(X1576,X1573)
| ~ ssRr(skf1(X1576),X1577)
| ~ ssPv1(X1577)
| ssPv2(X1576) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c742,plain,
( ~ ssRr(X3083,X3082)
| ~ ssPv4(X3082)
| ~ ssRr(X3079,X3083)
| ~ ssRr(X3080,X3081)
| ~ ssPv3(X3081)
| ~ ssRr(X3079,X3080)
| ~ ssPv1(skf1(skf1(X3079)))
| ssPv2(X3079) ),
inference(resolution,[status(thm)],[c220,clause1]) ).
cnf(c187,plain,
( ~ ssRr(X1190,X1191)
| ~ ssPv3(X1191)
| ~ ssRr(X1190,X1190)
| ~ ssRr(X1192,X1193)
| ~ ssRr(X1190,X1192)
| ~ ssRr(X1191,X1194)
| ssPv4(X1193)
| ssPv2(X1194)
| ssPv3(X1190) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c567,plain,
( ~ ssRr(X2241,X2244)
| ~ ssPv3(X2244)
| ~ ssRr(X2241,X2241)
| ~ ssRr(X2243,X2242)
| ~ ssRr(X2241,X2243)
| ssPv4(X2242)
| ssPv2(skf1(X2244))
| ssPv3(X2241) ),
inference(resolution,[status(thm)],[c187,clause1]) ).
cnf(c963,plain,
( ~ ssRr(X3075,X3073)
| ~ ssPv3(X3073)
| ~ ssRr(X3075,X3075)
| ~ ssRr(skf1(X3075),X3074)
| ssPv4(X3074)
| ssPv2(skf1(X3073))
| ssPv3(X3075) ),
inference(resolution,[status(thm)],[c567,clause1]) ).
cnf(c1235,plain,
( ~ ssRr(X3077,X3076)
| ~ ssPv3(X3076)
| ~ ssRr(X3077,X3077)
| ssPv4(skf1(skf1(X3077)))
| ssPv2(skf1(X3076))
| ssPv3(X3077) ),
inference(resolution,[status(thm)],[c963,clause1]) ).
cnf(c181,plain,
( ~ ssRr(X1179,X1176)
| ~ ssPv4(X1176)
| ~ ssRr(X1178,X1179)
| ~ ssRr(X1180,X1175)
| ~ ssRr(X1178,X1180)
| ~ ssRr(skf1(X1178),X1177)
| ssPv4(X1175)
| ssPv1(X1177)
| ssPv4(X1178) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c559,plain,
( ~ ssRr(X2230,X2226)
| ~ ssPv4(X2226)
| ~ ssRr(X2227,X2230)
| ~ ssRr(X2229,X2228)
| ~ ssRr(X2227,X2229)
| ssPv4(X2228)
| ssPv1(skf1(skf1(X2227)))
| ssPv4(X2227) ),
inference(resolution,[status(thm)],[c181,clause1]) ).
cnf(c953,plain,
( ~ ssRr(X3056,X3057)
| ~ ssPv4(X3057)
| ~ ssRr(X3054,X3056)
| ~ ssRr(X3056,X3055)
| ssPv4(X3055)
| ssPv1(skf1(skf1(X3054)))
| ssPv4(X3054) ),
inference(factor,[status(thm)],[c559]) ).
cnf(c1232,plain,
( ~ ssRr(X3065,X3064)
| ~ ssPv4(X3064)
| ~ ssRr(X3063,X3065)
| ssPv4(skf1(X3065))
| ssPv1(skf1(skf1(X3063)))
| ssPv4(X3063) ),
inference(resolution,[status(thm)],[c953,clause1]) ).
cnf(c177,plain,
( ~ ssRr(X1116,X1117)
| ~ ssPv4(X1117)
| ~ ssRr(X1119,X1116)
| ~ ssRr(X1120,X1115)
| ~ ssRr(X1119,X1120)
| ~ ssRr(X1116,X1118)
| ssPv4(X1115)
| ssPv1(X1118)
| ssPv4(X1119) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c531,plain,
( ~ ssRr(X2112,X2113)
| ~ ssPv4(X2113)
| ~ ssRr(X2114,X2112)
| ~ ssRr(X2111,X2110)
| ~ ssRr(X2114,X2111)
| ssPv4(X2110)
| ssPv1(skf1(X2112))
| ssPv4(X2114) ),
inference(resolution,[status(thm)],[c177,clause1]) ).
cnf(c926,plain,
( ~ ssRr(X3040,X3038)
| ~ ssPv4(X3038)
| ~ ssRr(X3039,X3040)
| ~ ssRr(skf1(X3039),X3037)
| ssPv4(X3037)
| ssPv1(skf1(X3040))
| ssPv4(X3039) ),
inference(resolution,[status(thm)],[c531,clause1]) ).
cnf(c1227,plain,
( ~ ssRr(X3041,X3043)
| ~ ssPv4(X3043)
| ~ ssRr(X3042,X3041)
| ssPv4(skf1(skf1(X3042)))
| ssPv1(skf1(X3041))
| ssPv4(X3042) ),
inference(resolution,[status(thm)],[c926,clause1]) ).
cnf(c729,plain,
( ~ ssRr(X3032,X3029)
| ~ ssPv4(X3029)
| ~ ssRr(X3031,X3032)
| ~ ssRr(X3033,X3030)
| ~ ssPv3(X3030)
| ~ ssRr(X3031,X3033)
| ~ ssPv1(skf1(X3033))
| ssPv2(X3031) ),
inference(resolution,[status(thm)],[c218,clause1]) ).
cnf(c709,plain,
( ~ ssRr(X2908,X2906)
| ~ ssPv4(X2906)
| ~ ssRr(X2908,X2908)
| ~ ssRr(X2907,X2905)
| ~ ssPv3(X2905)
| ~ ssRr(X2908,X2907)
| ~ ssPv1(X2908)
| ssPv2(X2908) ),
inference(factor,[status(thm)],[c216]) ).
cnf(c1203,plain,
( ~ ssRr(X2987,X2986)
| ~ ssPv4(X2986)
| ~ ssRr(X2987,X2987)
| ~ ssRr(skf1(X2987),X2988)
| ~ ssPv3(X2988)
| ~ ssPv1(X2987)
| ssPv2(X2987) ),
inference(resolution,[status(thm)],[c709,clause1]) ).
cnf(c1219,plain,
( ~ ssRr(X2995,X2994)
| ~ ssPv4(X2994)
| ~ ssRr(X2995,X2995)
| ~ ssPv3(skf1(skf1(X2995)))
| ~ ssPv1(X2995)
| ssPv2(X2995) ),
inference(resolution,[status(thm)],[c1203,clause1]) ).
cnf(c708,plain,
( ~ ssRr(X2892,X2893)
| ~ ssPv4(X2893)
| ~ ssRr(X2895,X2892)
| ~ ssRr(X2891,X2894)
| ~ ssPv3(X2894)
| ~ ssRr(X2895,X2891)
| ~ ssPv1(X2893)
| ssPv2(X2895) ),
inference(factor,[status(thm)],[c216]) ).
cnf(c1196,plain,
( ~ ssRr(X2966,X2965)
| ~ ssPv4(X2965)
| ~ ssRr(X2968,X2966)
| ~ ssRr(skf1(X2968),X2967)
| ~ ssPv3(X2967)
| ~ ssPv1(X2965)
| ssPv2(X2968) ),
inference(resolution,[status(thm)],[c708,clause1]) ).
cnf(c1215,plain,
( ~ ssRr(X2979,X2978)
| ~ ssPv4(X2978)
| ~ ssRr(X2977,X2979)
| ~ ssPv3(skf1(skf1(X2977)))
| ~ ssPv1(X2978)
| ssPv2(X2977) ),
inference(resolution,[status(thm)],[c1196,clause1]) ).
cnf(c726,plain,
( ~ ssRr(X2974,X2972)
| ~ ssPv4(X2972)
| ~ ssRr(X2971,X2974)
| ~ ssRr(X2971,X2973)
| ~ ssPv3(X2973)
| ~ ssRr(X2971,X2971)
| ~ ssPv1(X2974)
| ssPv2(X2971) ),
inference(factor,[status(thm)],[c218]) ).
cnf(c217,plain,
( ~ ssRr(X1522,X1523)
| ~ ssPv4(X1523)
| ~ ssRr(X1521,X1522)
| ~ ssRr(X1521,X1520)
| ~ ssPv3(X1520)
| ~ ssRr(X1521,X1521)
| ~ ssRr(X1520,X1524)
| ~ ssPv1(X1524)
| ssPv2(X1521) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c720,plain,
( ~ ssRr(X2957,X2955)
| ~ ssPv4(X2955)
| ~ ssRr(X2956,X2957)
| ~ ssRr(X2956,X2958)
| ~ ssPv3(X2958)
| ~ ssRr(X2956,X2956)
| ~ ssPv1(skf1(X2958))
| ssPv2(X2956) ),
inference(resolution,[status(thm)],[c217,clause1]) ).
cnf(c712,plain,
( ~ ssRr(X2936,X2935)
| ~ ssPv4(X2935)
| ~ ssRr(X2938,X2936)
| ~ ssRr(X2934,X2937)
| ~ ssPv3(X2937)
| ~ ssRr(X2938,X2934)
| ~ ssPv1(skf1(X2936))
| ssPv2(X2938) ),
inference(resolution,[status(thm)],[c216,clause1]) ).
cnf(c1200,plain,
( ~ ssRr(X2927,X2928)
| ~ ssPv4(X2928)
| ~ ssRr(X2927,X2927)
| ~ ssRr(X2928,X2929)
| ~ ssPv3(X2929)
| ~ ssPv1(X2927)
| ssPv2(X2927) ),
inference(factor,[status(thm)],[c709]) ).
cnf(c1212,plain,
( ~ ssRr(X2932,X2933)
| ~ ssPv4(X2933)
| ~ ssRr(X2932,X2932)
| ~ ssPv3(skf1(X2933))
| ~ ssPv1(X2932)
| ssPv2(X2932) ),
inference(resolution,[status(thm)],[c1200,clause1]) ).
cnf(c1195,plain,
( ~ ssRr(X2916,X2915)
| ~ ssPv4(X2915)
| ~ ssRr(X2917,X2916)
| ~ ssRr(X2917,X2917)
| ~ ssPv3(X2917)
| ~ ssPv1(X2915)
| ssPv2(X2917) ),
inference(factor,[status(thm)],[c708]) ).
cnf(c1193,plain,
( ~ ssRr(X2899,X2900)
| ~ ssPv4(X2900)
| ~ ssRr(X2899,X2899)
| ~ ssRr(X2900,X2898)
| ~ ssPv3(X2898)
| ~ ssPv1(X2900)
| ssPv2(X2899) ),
inference(factor,[status(thm)],[c708]) ).
cnf(c1199,plain,
( ~ ssRr(X2903,X2904)
| ~ ssPv4(X2904)
| ~ ssRr(X2903,X2903)
| ~ ssPv3(skf1(X2904))
| ~ ssPv1(X2904)
| ssPv2(X2903) ),
inference(resolution,[status(thm)],[c1193,clause1]) ).
cnf(c210,plain,
( ~ ssRr(X1426,X1428)
| ~ ssPv4(X1428)
| ~ ssRr(X1425,X1426)
| ~ ssRr(X1425,X1429)
| ~ ssRr(X1425,X1425)
| ~ ssRr(X1429,X1427)
| ~ ssPv2(X1425)
| ssPv3(X1429)
| ssPv2(X1427) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c673,plain,
( ~ ssRr(X2758,X2756)
| ~ ssPv4(X2756)
| ~ ssRr(X2757,X2758)
| ~ ssRr(X2757,X2759)
| ~ ssRr(X2757,X2757)
| ~ ssPv2(X2757)
| ssPv3(X2759)
| ssPv2(skf1(X2759)) ),
inference(resolution,[status(thm)],[c210,clause1]) ).
cnf(c1146,plain,
( ~ ssRr(X2882,X2881)
| ~ ssPv4(X2881)
| ~ ssRr(X2883,X2882)
| ~ ssRr(X2883,X2883)
| ~ ssPv2(X2883)
| ssPv3(X2883)
| ssPv2(skf1(X2883)) ),
inference(factor,[status(thm)],[c673]) ).
cnf(c215,plain,
( ~ ssRr(X1491,X1490)
| ~ ssPv4(X1490)
| ~ ssRr(X1491,X1491)
| ~ ssRr(X1492,X1489)
| ~ ssPv3(X1489)
| ~ ssRr(X1491,X1492)
| ~ ssRr(X1490,X1493)
| ~ ssPv1(X1493)
| ssPv2(X1491) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c700,plain,
( ~ ssRr(X2875,X2878)
| ~ ssPv4(X2878)
| ~ ssRr(X2875,X2875)
| ~ ssRr(X2877,X2876)
| ~ ssPv3(X2876)
| ~ ssRr(X2875,X2877)
| ~ ssPv1(skf1(X2878))
| ssPv2(X2875) ),
inference(resolution,[status(thm)],[c215,clause1]) ).
cnf(c1145,plain,
( ~ ssRr(X2872,X2870)
| ~ ssPv4(X2870)
| ~ ssRr(X2872,X2872)
| ~ ssRr(X2872,X2871)
| ~ ssPv2(X2872)
| ssPv3(X2871)
| ssPv2(skf1(X2871)) ),
inference(factor,[status(thm)],[c673]) ).
cnf(c1139,plain,
( ~ ssRr(X2866,X2864)
| ~ ssPv4(X2864)
| ~ ssRr(X2865,X2866)
| ~ ssRr(X2865,X2865)
| ~ ssPv2(X2865)
| ssPv3(X2865)
| ssPv2(skf1(X2866)) ),
inference(factor,[status(thm)],[c665]) ).
cnf(c1138,plain,
( ~ ssRr(X2840,X2838)
| ~ ssPv4(X2838)
| ~ ssRr(X2839,X2840)
| ~ ssRr(X2840,X2841)
| ~ ssPv2(X2839)
| ssPv3(X2841)
| ssPv2(skf1(X2840)) ),
inference(factor,[status(thm)],[c665]) ).
cnf(c1173,plain,
( ~ ssRr(X2843,X2842)
| ~ ssPv4(X2842)
| ~ ssRr(X2844,X2843)
| ~ ssPv2(X2844)
| ssPv3(X2842)
| ssPv2(skf1(X2843)) ),
inference(factor,[status(thm)],[c1138]) ).
cnf(c1177,plain,
( ~ ssRr(skf1(X2854),X2853)
| ~ ssPv4(X2853)
| ~ ssPv2(X2854)
| ssPv3(X2853)
| ssPv2(skf1(skf1(X2854))) ),
inference(resolution,[status(thm)],[c1173,clause1]) ).
cnf(c1174,plain,
( ~ ssRr(X2850,X2851)
| ~ ssPv4(X2851)
| ~ ssRr(X2850,X2850)
| ~ ssPv2(X2850)
| ssPv3(X2850)
| ssPv2(skf1(X2850)) ),
inference(factor,[status(thm)],[c1138]) ).
cnf(c1137,plain,
( ~ ssRr(X2826,X2827)
| ~ ssPv4(X2827)
| ~ ssRr(X2826,X2826)
| ~ ssRr(X2827,X2828)
| ~ ssPv2(X2826)
| ssPv3(X2828)
| ssPv2(skf1(X2826)) ),
inference(factor,[status(thm)],[c665]) ).
cnf(c1171,plain,
( ~ ssRr(X2835,X2836)
| ~ ssPv4(X2836)
| ~ ssRr(X2835,X2835)
| ~ ssPv2(X2835)
| ssPv3(skf1(X2836))
| ssPv2(skf1(X2835)) ),
inference(resolution,[status(thm)],[c1137,clause1]) ).
cnf(c661,plain,
( ~ ssRr(X2693,X2692)
| ~ ssPv4(X2692)
| ~ ssRr(X2694,X2693)
| ~ ssRr(X2691,X2690)
| ~ ssRr(X2694,X2691)
| ~ ssPv2(X2694)
| ssPv3(X2690)
| ssPv2(X2692) ),
inference(factor,[status(thm)],[c209]) ).
cnf(c1124,plain,
( ~ ssRr(X2812,X2809)
| ~ ssPv4(X2809)
| ~ ssRr(X2811,X2812)
| ~ ssRr(skf1(X2811),X2810)
| ~ ssPv2(X2811)
| ssPv3(X2810)
| ssPv2(X2809) ),
inference(resolution,[status(thm)],[c661,clause1]) ).
cnf(c1162,plain,
( ~ ssRr(X2815,X2817)
| ~ ssPv4(X2817)
| ~ ssRr(X2816,X2815)
| ~ ssPv2(X2816)
| ssPv3(skf1(skf1(X2816)))
| ssPv2(X2817) ),
inference(resolution,[status(thm)],[c1124,clause1]) ).
cnf(c1117,plain,
( ~ ssRr(X2780,X2779)
| ~ ssPv4(X2779)
| ~ ssRr(X2780,X2780)
| ~ ssRr(X2780,X2781)
| ~ ssPv2(X2780)
| ssPv3(X2781)
| ssPv2(skf1(X2779)) ),
inference(factor,[status(thm)],[c657]) ).
cnf(c1154,plain,
( ~ ssRr(X2793,X2792)
| ~ ssPv4(X2792)
| ~ ssRr(X2793,X2793)
| ~ ssPv2(X2793)
| ssPv3(skf1(X2793))
| ssPv2(skf1(X2792)) ),
inference(resolution,[status(thm)],[c1117,clause1]) ).
cnf(c1152,plain,
( ~ ssRr(X2782,X2783)
| ~ ssPv4(X2783)
| ~ ssRr(X2782,X2782)
| ~ ssPv2(X2782)
| ssPv3(X2783)
| ssPv2(skf1(X2783)) ),
inference(factor,[status(thm)],[c1117]) ).
cnf(c681,plain,
( ~ ssRr(X2768,X2769)
| ~ ssPv4(X2769)
| ~ ssRr(X2770,X2768)
| ~ ssRr(X2770,X2767)
| ~ ssRr(X2770,X2770)
| ~ ssPv2(X2770)
| ssPv3(X2767)
| ssPv2(X2768) ),
inference(factor,[status(thm)],[c211]) ).
cnf(c1144,plain,
( ~ ssRr(X2762,X2762)
| ~ ssPv4(X2762)
| ~ ssRr(X2762,X2761)
| ~ ssPv2(X2762)
| ssPv3(X2761)
| ssPv2(skf1(X2761)) ),
inference(factor,[status(thm)],[c673]) ).
cnf(c1148,plain,
( ~ ssRr(X2764,X2764)
| ~ ssPv4(X2764)
| ~ ssPv2(X2764)
| ssPv3(skf1(X2764))
| ssPv2(skf1(skf1(X2764))) ),
inference(resolution,[status(thm)],[c1144,clause1]) ).
cnf(c1116,plain,
( ~ ssRr(X2754,X2752)
| ~ ssPv4(X2752)
| ~ ssRr(X2754,X2754)
| ~ ssRr(X2752,X2753)
| ~ ssPv2(X2754)
| ssPv3(X2753)
| ssPv2(skf1(X2752)) ),
inference(factor,[status(thm)],[c657]) ).
cnf(c664,plain,
( ~ ssRr(X2724,X2721)
| ~ ssPv4(X2721)
| ~ ssRr(X2724,X2724)
| ~ ssRr(X2722,X2723)
| ~ ssRr(X2724,X2722)
| ~ ssPv2(X2724)
| ssPv3(X2723)
| ssPv2(X2722) ),
inference(factor,[status(thm)],[c209]) ).
cnf(c1123,plain,
( ~ ssRr(X2713,X2711)
| ~ ssPv4(X2711)
| ~ ssRr(X2712,X2713)
| ~ ssRr(X2712,X2712)
| ~ ssPv2(X2712)
| ssPv3(X2712)
| ssPv2(X2711) ),
inference(factor,[status(thm)],[c661]) ).
cnf(c1121,plain,
( ~ ssRr(X2697,X2695)
| ~ ssPv4(X2695)
| ~ ssRr(X2697,X2697)
| ~ ssRr(X2695,X2696)
| ~ ssPv2(X2697)
| ssPv3(X2696)
| ssPv2(X2695) ),
inference(factor,[status(thm)],[c661]) ).
cnf(c1127,plain,
( ~ ssRr(X2700,X2701)
| ~ ssPv4(X2701)
| ~ ssRr(X2700,X2700)
| ~ ssPv2(X2700)
| ssPv3(skf1(X2701))
| ssPv2(X2701) ),
inference(resolution,[status(thm)],[c1121,clause1]) ).
cnf(c1118,plain,
( ~ ssRr(X2685,X2684)
| ~ ssPv4(X2684)
| ~ ssRr(X2685,X2685)
| ~ ssPv2(X2685)
| ssPv3(X2685)
| ssPv2(skf1(X2684)) ),
inference(factor,[status(thm)],[c657]) ).
cnf(c1120,plain,
( ~ ssRr(X2686,X2686)
| ~ ssPv4(X2686)
| ~ ssPv2(X2686)
| ssPv3(X2686)
| ssPv2(skf1(X2686)) ),
inference(factor,[status(thm)],[c1118]) ).
cnf(c201,plain,
( ~ ssRr(X1323,X1324)
| ~ ssPv4(X1324)
| ~ ssRr(X1321,X1323)
| ~ ssRr(X1321,X1320)
| ~ ssPv3(X1320)
| ~ ssRr(X1321,X1321)
| ~ ssRr(X1320,X1322)
| ssPv4(X1322)
| ssPv3(X1321) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c634,plain,
( ~ ssRr(X2550,X2552)
| ~ ssPv4(X2552)
| ~ ssRr(X2551,X2550)
| ~ ssRr(X2551,X2553)
| ~ ssPv3(X2553)
| ~ ssRr(X2551,X2551)
| ssPv4(skf1(X2553))
| ssPv3(X2551) ),
inference(resolution,[status(thm)],[c201,clause1]) ).
cnf(c1075,plain,
( ~ ssRr(X2673,X2674)
| ~ ssPv4(X2674)
| ~ ssRr(X2673,X2673)
| ~ ssRr(X2673,X2675)
| ~ ssPv3(X2675)
| ssPv4(skf1(X2675))
| ssPv3(X2673) ),
inference(factor,[status(thm)],[c634]) ).
cnf(c1066,plain,
( ~ ssRr(X2645,X2644)
| ~ ssPv4(X2644)
| ~ ssRr(X2642,X2645)
| ~ ssRr(X2645,X2643)
| ~ ssPv3(X2643)
| ssPv4(skf1(X2645))
| ssPv3(X2642) ),
inference(factor,[status(thm)],[c624]) ).
cnf(c1102,plain,
( ~ ssRr(X2652,X2651)
| ~ ssPv4(X2651)
| ~ ssRr(X2650,X2652)
| ~ ssPv3(X2651)
| ssPv4(skf1(X2652))
| ssPv3(X2650) ),
inference(factor,[status(thm)],[c1066]) ).
cnf(c1106,plain,
( ~ ssRr(skf1(X2657),X2656)
| ~ ssPv4(X2656)
| ~ ssPv3(X2656)
| ssPv4(skf1(skf1(X2657)))
| ssPv3(X2657) ),
inference(resolution,[status(thm)],[c1102,clause1]) ).
cnf(c1065,plain,
( ~ ssRr(X2635,X2637)
| ~ ssPv4(X2637)
| ~ ssRr(X2635,X2635)
| ~ ssRr(X2637,X2636)
| ~ ssPv3(X2636)
| ssPv4(skf1(X2635))
| ssPv3(X2635) ),
inference(factor,[status(thm)],[c624]) ).
cnf(c1101,plain,
( ~ ssRr(X2640,X2641)
| ~ ssPv4(X2641)
| ~ ssRr(X2640,X2640)
| ~ ssPv3(skf1(X2641))
| ssPv4(skf1(X2640))
| ssPv3(X2640) ),
inference(resolution,[status(thm)],[c1065,clause1]) ).
cnf(c1045,plain,
( ~ ssRr(X2623,X2622)
| ~ ssPv4(X2622)
| ~ ssRr(X2623,X2623)
| ~ ssRr(X2623,X2621)
| ~ ssPv3(X2621)
| ssPv4(skf1(X2622))
| ssPv3(X2623) ),
inference(factor,[status(thm)],[c616]) ).
cnf(c1097,plain,
( ~ ssRr(X2630,X2629)
| ~ ssPv4(X2629)
| ~ ssRr(X2630,X2630)
| ~ ssPv3(skf1(X2630))
| ssPv4(skf1(X2629))
| ssPv3(X2630) ),
inference(resolution,[status(thm)],[c1045,clause1]) ).
cnf(c1095,plain,
( ~ ssRr(X2624,X2625)
| ~ ssPv4(X2625)
| ~ ssRr(X2624,X2624)
| ~ ssPv3(X2625)
| ssPv4(skf1(X2625))
| ssPv3(X2624) ),
inference(factor,[status(thm)],[c1045]) ).
cnf(c1044,plain,
( ~ ssRr(X2609,X2611)
| ~ ssPv4(X2611)
| ~ ssRr(X2609,X2609)
| ~ ssRr(X2611,X2610)
| ~ ssPv3(X2610)
| ssPv4(skf1(X2611))
| ssPv3(X2609) ),
inference(factor,[status(thm)],[c616]) ).
cnf(c636,plain,
( ~ ssRr(X2564,X2566)
| ~ ssPv4(X2566)
| ~ ssRr(X2565,X2564)
| ~ ssRr(X2565,X2567)
| ~ ssPv3(X2567)
| ~ ssRr(X2565,X2565)
| ssPv4(X2564)
| ssPv3(X2565) ),
inference(factor,[status(thm)],[c202]) ).
cnf(c1074,plain,
( ~ ssRr(X2556,X2556)
| ~ ssPv4(X2556)
| ~ ssRr(X2556,X2557)
| ~ ssPv3(X2557)
| ssPv4(skf1(X2557))
| ssPv3(X2556) ),
inference(factor,[status(thm)],[c634]) ).
cnf(c1078,plain,
( ~ ssRr(X2559,X2559)
| ~ ssPv4(X2559)
| ~ ssPv3(skf1(X2559))
| ssPv4(skf1(skf1(X2559)))
| ssPv3(X2559) ),
inference(resolution,[status(thm)],[c1074,clause1]) ).
cnf(c189,plain,
( ~ ssRr(X1224,X1226)
| ~ ssPv3(X1226)
| ~ ssRr(X1223,X1224)
| ~ ssRr(X1223,X1225)
| ~ ssRr(X1223,X1223)
| ~ ssRr(X1225,X1227)
| ssPv4(X1225)
| ssPv2(X1227)
| ssPv3(X1223) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c583,plain,
( ~ ssRr(X2310,X2311)
| ~ ssPv3(X2311)
| ~ ssRr(X2312,X2310)
| ~ ssRr(X2312,X2313)
| ~ ssRr(X2312,X2312)
| ssPv4(X2313)
| ssPv2(skf1(X2313))
| ssPv3(X2312) ),
inference(resolution,[status(thm)],[c189,clause1]) ).
cnf(c998,plain,
( ~ ssRr(X2547,X2546)
| ~ ssPv3(X2546)
| ~ ssRr(X2548,X2547)
| ~ ssRr(X2548,X2548)
| ssPv4(X2548)
| ssPv2(skf1(X2548))
| ssPv3(X2548) ),
inference(factor,[status(thm)],[c583]) ).
cnf(c997,plain,
( ~ ssRr(X2539,X2540)
| ~ ssPv3(X2540)
| ~ ssRr(X2539,X2539)
| ~ ssRr(X2539,X2541)
| ssPv4(X2541)
| ssPv2(skf1(X2541))
| ssPv3(X2539) ),
inference(factor,[status(thm)],[c583]) ).
cnf(c623,plain,
( ~ ssRr(X2521,X2522)
| ~ ssPv4(X2522)
| ~ ssRr(X2521,X2521)
| ~ ssRr(X2519,X2520)
| ~ ssPv3(X2520)
| ~ ssRr(X2521,X2519)
| ssPv4(X2519)
| ssPv3(X2521) ),
inference(factor,[status(thm)],[c200]) ).
cnf(c990,plain,
( ~ ssRr(X2517,X2518)
| ~ ssPv3(X2518)
| ~ ssRr(X2516,X2517)
| ~ ssRr(X2516,X2516)
| ssPv4(X2516)
| ssPv2(skf1(X2517))
| ssPv3(X2516) ),
inference(factor,[status(thm)],[c577]) ).
cnf(c989,plain,
( ~ ssRr(X2495,X2497)
| ~ ssPv3(X2497)
| ~ ssRr(X2496,X2495)
| ~ ssRr(X2495,X2498)
| ssPv4(X2498)
| ssPv2(skf1(X2495))
| ssPv3(X2496) ),
inference(factor,[status(thm)],[c577]) ).
cnf(c1052,plain,
( ~ ssRr(X2500,X2499)
| ~ ssPv3(X2499)
| ~ ssRr(X2501,X2500)
| ssPv4(X2499)
| ssPv2(skf1(X2500))
| ssPv3(X2501) ),
inference(factor,[status(thm)],[c989]) ).
cnf(c1056,plain,
( ~ ssRr(skf1(X2511),X2510)
| ~ ssPv3(X2510)
| ssPv4(X2510)
| ssPv2(skf1(skf1(X2511)))
| ssPv3(X2511) ),
inference(resolution,[status(thm)],[c1052,clause1]) ).
cnf(c1053,plain,
( ~ ssRr(X2503,X2504)
| ~ ssPv3(X2504)
| ~ ssRr(X2503,X2503)
| ssPv4(X2503)
| ssPv2(skf1(X2503))
| ssPv3(X2503) ),
inference(factor,[status(thm)],[c989]) ).
cnf(c988,plain,
( ~ ssRr(X2483,X2482)
| ~ ssPv3(X2482)
| ~ ssRr(X2483,X2483)
| ~ ssRr(X2482,X2484)
| ssPv4(X2484)
| ssPv2(skf1(X2483))
| ssPv3(X2483) ),
inference(factor,[status(thm)],[c577]) ).
cnf(c1050,plain,
( ~ ssRr(X2487,X2488)
| ~ ssPv3(X2488)
| ~ ssRr(X2487,X2487)
| ssPv4(skf1(X2488))
| ssPv2(skf1(X2487))
| ssPv3(X2487) ),
inference(resolution,[status(thm)],[c988,clause1]) ).
cnf(c574,plain,
( ~ ssRr(X2269,X2267)
| ~ ssPv3(X2267)
| ~ ssRr(X2269,X2269)
| ~ ssRr(X2268,X2270)
| ~ ssRr(X2269,X2268)
| ssPv4(X2270)
| ssPv2(X2269)
| ssPv3(X2269) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c977,plain,
( ~ ssRr(X2472,X2471)
| ~ ssPv3(X2471)
| ~ ssRr(X2472,X2472)
| ~ ssRr(skf1(X2472),X2470)
| ssPv4(X2470)
| ssPv2(X2472)
| ssPv3(X2472) ),
inference(resolution,[status(thm)],[c574,clause1]) ).
cnf(c1042,plain,
( ~ ssRr(X2474,X2473)
| ~ ssPv3(X2473)
| ~ ssRr(X2474,X2474)
| ssPv4(skf1(skf1(X2474)))
| ssPv2(X2474)
| ssPv3(X2474) ),
inference(resolution,[status(thm)],[c977,clause1]) ).
cnf(c573,plain,
( ~ ssRr(X2256,X2255)
| ~ ssPv3(X2255)
| ~ ssRr(X2257,X2256)
| ~ ssRr(X2254,X2258)
| ~ ssRr(X2257,X2254)
| ssPv4(X2258)
| ssPv2(X2255)
| ssPv3(X2257) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c969,plain,
( ~ ssRr(X2453,X2456)
| ~ ssPv3(X2456)
| ~ ssRr(X2455,X2453)
| ~ ssRr(skf1(X2455),X2454)
| ssPv4(X2454)
| ssPv2(X2456)
| ssPv3(X2455) ),
inference(resolution,[status(thm)],[c573,clause1]) ).
cnf(c1035,plain,
( ~ ssRr(X2460,X2459)
| ~ ssPv3(X2459)
| ~ ssRr(X2461,X2460)
| ssPv4(skf1(skf1(X2461)))
| ssPv2(X2459)
| ssPv3(X2461) ),
inference(resolution,[status(thm)],[c969,clause1]) ).
cnf(c961,plain,
( ~ ssRr(X2440,X2438)
| ~ ssPv3(X2438)
| ~ ssRr(X2440,X2440)
| ~ ssRr(X2440,X2439)
| ssPv4(X2439)
| ssPv2(skf1(X2438))
| ssPv3(X2440) ),
inference(factor,[status(thm)],[c567]) ).
cnf(c1031,plain,
( ~ ssRr(X2451,X2450)
| ~ ssPv3(X2450)
| ~ ssRr(X2451,X2451)
| ssPv4(skf1(X2451))
| ssPv2(skf1(X2450))
| ssPv3(X2451) ),
inference(resolution,[status(thm)],[c961,clause1]) ).
cnf(c1029,plain,
( ~ ssRr(X2442,X2441)
| ~ ssPv3(X2441)
| ~ ssRr(X2442,X2442)
| ssPv4(X2441)
| ssPv2(skf1(X2441))
| ssPv3(X2442) ),
inference(factor,[status(thm)],[c961]) ).
cnf(c960,plain,
( ~ ssRr(X2428,X2429)
| ~ ssPv3(X2429)
| ~ ssRr(X2428,X2428)
| ~ ssRr(X2429,X2427)
| ssPv4(X2427)
| ssPv2(skf1(X2429))
| ssPv3(X2428) ),
inference(factor,[status(thm)],[c567]) ).
cnf(c178,plain,
( ~ ssRr(X1133,X1131)
| ~ ssPv4(X1131)
| ~ ssRr(X1134,X1133)
| ~ ssRr(X1134,X1130)
| ~ ssRr(X1134,X1134)
| ~ ssRr(X1130,X1132)
| ssPv4(X1130)
| ssPv1(X1132)
| ssPv4(X1134) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c540,plain,
( ~ ssRr(X2123,X2125)
| ~ ssPv4(X2125)
| ~ ssRr(X2124,X2123)
| ~ ssRr(X2124,X2126)
| ~ ssRr(X2124,X2124)
| ssPv4(X2126)
| ssPv1(skf1(X2126))
| ssPv4(X2124) ),
inference(resolution,[status(thm)],[c178,clause1]) ).
cnf(c931,plain,
( ~ ssRr(X2405,X2403)
| ~ ssPv4(X2403)
| ~ ssRr(X2405,X2405)
| ~ ssRr(X2405,X2404)
| ssPv4(X2404)
| ssPv1(skf1(X2404))
| ssPv4(X2405) ),
inference(factor,[status(thm)],[c540]) ).
cnf(c924,plain,
( ~ ssRr(X2390,X2388)
| ~ ssPv4(X2388)
| ~ ssRr(X2389,X2390)
| ~ ssRr(X2390,X2387)
| ssPv4(X2387)
| ssPv1(skf1(X2390))
| ssPv4(X2389) ),
inference(factor,[status(thm)],[c531]) ).
cnf(c590,plain,
( ~ ssRr(X2363,X2361)
| ~ ssPv3(X2361)
| ~ ssRr(X2362,X2363)
| ~ ssRr(X2362,X2360)
| ~ ssRr(X2362,X2362)
| ssPv4(X2360)
| ssPv2(X2362)
| ssPv3(X2362) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c527,plain,
( ~ ssRr(X2063,X2062)
| ~ ssPv4(X2062)
| ~ ssRr(X2066,X2063)
| ~ ssRr(X2065,X2064)
| ~ ssRr(X2066,X2065)
| ssPv4(X2064)
| ssPv1(X2062)
| ssPv4(X2066) ),
inference(factor,[status(thm)],[c177]) ).
cnf(c913,plain,
( ~ ssRr(X2341,X2342)
| ~ ssPv4(X2342)
| ~ ssRr(X2343,X2341)
| ~ ssRr(skf1(X2343),X2340)
| ssPv4(X2340)
| ssPv1(X2342)
| ssPv4(X2343) ),
inference(resolution,[status(thm)],[c527,clause1]) ).
cnf(c1004,plain,
( ~ ssRr(X2352,X2351)
| ~ ssPv4(X2351)
| ~ ssRr(X2353,X2352)
| ssPv4(skf1(skf1(X2353)))
| ssPv1(X2351)
| ssPv4(X2353) ),
inference(resolution,[status(thm)],[c913,clause1]) ).
cnf(c588,plain,
( ~ ssRr(X2327,X2325)
| ~ ssPv3(X2325)
| ~ ssRr(X2326,X2327)
| ~ ssRr(X2326,X2328)
| ~ ssRr(X2326,X2326)
| ssPv4(X2328)
| ssPv2(X2327)
| ssPv3(X2326) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c975,plain,
( ~ ssRr(X2303,X2304)
| ~ ssPv3(X2304)
| ~ ssRr(X2303,X2303)
| ~ ssRr(X2303,X2302)
| ssPv4(X2302)
| ssPv2(X2303)
| ssPv3(X2303) ),
inference(factor,[status(thm)],[c574]) ).
cnf(c994,plain,
( ~ ssRr(X2315,X2314)
| ~ ssPv3(X2314)
| ~ ssRr(X2315,X2315)
| ssPv4(skf1(X2315))
| ssPv2(X2315)
| ssPv3(X2315) ),
inference(resolution,[status(thm)],[c975,clause1]) ).
cnf(c992,plain,
( ~ ssRr(X2306,X2305)
| ~ ssPv3(X2305)
| ~ ssRr(X2306,X2306)
| ssPv4(X2305)
| ssPv2(X2306)
| ssPv3(X2306) ),
inference(factor,[status(thm)],[c975]) ).
cnf(c974,plain,
( ~ ssRr(X2289,X2291)
| ~ ssPv3(X2291)
| ~ ssRr(X2289,X2289)
| ~ ssRr(X2291,X2290)
| ssPv4(X2290)
| ssPv2(X2289)
| ssPv3(X2289) ),
inference(factor,[status(thm)],[c574]) ).
cnf(c986,plain,
( ~ ssRr(X2294,X2295)
| ~ ssPv3(X2295)
| ~ ssRr(X2294,X2294)
| ssPv4(skf1(X2295))
| ssPv2(X2294)
| ssPv3(X2294) ),
inference(resolution,[status(thm)],[c974,clause1]) ).
cnf(c576,plain,
( ~ ssRr(X2283,X2284)
| ~ ssPv3(X2284)
| ~ ssRr(X2283,X2283)
| ~ ssRr(X2285,X2286)
| ~ ssRr(X2283,X2285)
| ssPv4(X2286)
| ssPv2(X2285)
| ssPv3(X2283) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c968,plain,
( ~ ssRr(X2277,X2279)
| ~ ssPv3(X2279)
| ~ ssRr(X2278,X2277)
| ~ ssRr(X2278,X2278)
| ssPv4(X2278)
| ssPv2(X2279)
| ssPv3(X2278) ),
inference(factor,[status(thm)],[c573]) ).
cnf(c966,plain,
( ~ ssRr(X2261,X2259)
| ~ ssPv3(X2259)
| ~ ssRr(X2261,X2261)
| ~ ssRr(X2259,X2260)
| ssPv4(X2260)
| ssPv2(X2259)
| ssPv3(X2261) ),
inference(factor,[status(thm)],[c573]) ).
cnf(c972,plain,
( ~ ssRr(X2264,X2265)
| ~ ssPv3(X2265)
| ~ ssRr(X2264,X2264)
| ssPv4(skf1(X2265))
| ssPv2(X2265)
| ssPv3(X2264) ),
inference(resolution,[status(thm)],[c966,clause1]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X330,X332)
| ~ ssPv3(X332)
| ~ ssRr(X328,X330)
| ~ ssRr(X329,X327)
| ~ ssRr(X328,X329)
| ~ ssRr(X328,X331)
| ~ ssPv3(X331)
| ~ ssPv1(X328)
| ssPv2(X327) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c171,plain,
( ~ ssRr(X1068,X1067)
| ~ ssPv3(X1067)
| ~ ssRr(X1069,X1068)
| ~ ssRr(X1071,X1070)
| ~ ssRr(X1069,X1071)
| ~ ssPv3(X1071)
| ~ ssPv1(X1069)
| ssPv2(X1070) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c511,plain,
( ~ ssRr(X2026,X2023)
| ~ ssPv3(X2023)
| ~ ssRr(X2025,X2026)
| ~ ssRr(skf1(X2025),X2024)
| ~ ssPv3(skf1(X2025))
| ~ ssPv1(X2025)
| ssPv2(X2024) ),
inference(resolution,[status(thm)],[c171,clause1]) ).
cnf(c893,plain,
( ~ ssRr(X2239,X2240)
| ~ ssPv3(X2240)
| ~ ssRr(X2238,X2239)
| ~ ssPv3(skf1(X2238))
| ~ ssPv1(X2238)
| ssPv2(skf1(skf1(X2238))) ),
inference(resolution,[status(thm)],[c511,clause1]) ).
cnf(c959,plain,
( ~ ssRr(X2249,skf1(X2248))
| ~ ssPv3(skf1(X2248))
| ~ ssRr(X2248,X2249)
| ~ ssPv1(X2248)
| ssPv2(skf1(skf1(X2248))) ),
inference(factor,[status(thm)],[c893]) ).
cnf(c962,plain,
( ~ ssRr(X2246,X2245)
| ~ ssPv3(X2245)
| ~ ssRr(X2246,X2246)
| ssPv4(X2246)
| ssPv2(skf1(X2245))
| ssPv3(X2246) ),
inference(factor,[status(thm)],[c567]) ).
cnf(c954,plain,
( ~ ssRr(X2232,X2233)
| ~ ssPv4(X2233)
| ~ ssRr(X2231,X2232)
| ~ ssRr(X2231,X2231)
| ssPv4(X2231)
| ssPv1(skf1(skf1(X2231))) ),
inference(factor,[status(thm)],[c559]) ).
cnf(c957,plain,
( ~ ssRr(X2236,X2235)
| ~ ssPv4(X2235)
| ~ ssRr(X2236,X2236)
| ssPv4(X2236)
| ssPv1(skf1(skf1(X2236))) ),
inference(factor,[status(thm)],[c954]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X315,X317)
| ~ ssPv3(X317)
| ~ ssRr(X313,X315)
| ~ ssRr(X314,X312)
| ~ ssPv2(X312)
| ~ ssRr(X313,X314)
| ~ ssRr(X313,X316)
| ~ ssPv1(X316)
| ssPv3(X313) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c162,plain,
( ~ ssRr(X1001,X1000)
| ~ ssPv3(X1000)
| ~ ssRr(X999,X1001)
| ~ ssRr(X997,X998)
| ~ ssPv2(X998)
| ~ ssRr(X999,X997)
| ~ ssPv1(X997)
| ssPv3(X999) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c479,plain,
( ~ ssRr(X1998,X1997)
| ~ ssPv3(X1997)
| ~ ssRr(X1999,X1998)
| ~ ssRr(skf1(X1999),X1996)
| ~ ssPv2(X1996)
| ~ ssPv1(skf1(X1999))
| ssPv3(X1999) ),
inference(resolution,[status(thm)],[c162,clause1]) ).
cnf(c884,plain,
( ~ ssRr(X2219,X2220)
| ~ ssPv3(X2220)
| ~ ssRr(X2221,X2219)
| ~ ssPv2(skf1(skf1(X2221)))
| ~ ssPv1(skf1(X2221))
| ssPv3(X2221) ),
inference(resolution,[status(thm)],[c479,clause1]) ).
cnf(c663,plain,
( ~ ssRr(X1686,X1684)
| ~ ssPv4(X1684)
| ~ ssRr(X1687,X1686)
| ~ ssRr(X1686,X1685)
| ~ ssPv2(X1687)
| ssPv3(X1685)
| ssPv2(X1685) ),
inference(factor,[status(thm)],[c209]) ).
cnf(c778,plain,
( ~ ssRr(X1922,X1920)
| ~ ssPv4(X1920)
| ~ ssRr(X1921,X1922)
| ~ ssPv2(X1921)
| ssPv3(skf1(X1922))
| ssPv2(skf1(X1922)) ),
inference(resolution,[status(thm)],[c663,clause1]) ).
cnf(c858,plain,
( ~ ssRr(skf1(X2209),X2208)
| ~ ssPv4(X2208)
| ~ ssPv2(X2209)
| ssPv3(skf1(skf1(X2209)))
| ssPv2(skf1(skf1(X2209))) ),
inference(resolution,[status(thm)],[c778,clause1]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X300,X302)
| ~ ssPv4(X302)
| ~ ssRr(X298,X300)
| ~ ssRr(X299,X297)
| ~ ssRr(X298,X299)
| ~ ssRr(X298,X301)
| ~ ssPv1(X298)
| ssPv3(X297)
| ssPv2(X301) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c153,plain,
( ~ ssRr(X923,X926)
| ~ ssPv4(X926)
| ~ ssRr(X925,X923)
| ~ ssRr(X924,X927)
| ~ ssRr(X925,X924)
| ~ ssPv1(X925)
| ssPv3(X927)
| ssPv2(X924) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c444,plain,
( ~ ssRr(X1914,X1913)
| ~ ssPv4(X1913)
| ~ ssRr(X1915,X1914)
| ~ ssRr(skf1(X1915),X1912)
| ~ ssPv1(X1915)
| ssPv3(X1912)
| ssPv2(skf1(X1915)) ),
inference(resolution,[status(thm)],[c153,clause1]) ).
cnf(c855,plain,
( ~ ssRr(X2204,X2202)
| ~ ssPv4(X2202)
| ~ ssRr(X2203,X2204)
| ~ ssPv1(X2203)
| ssPv3(skf1(skf1(X2203)))
| ssPv2(skf1(X2203)) ),
inference(resolution,[status(thm)],[c444,clause1]) ).
cnf(c949,plain,
( ~ ssRr(X2205,X2205)
| ~ ssPv4(X2205)
| ~ ssPv1(X2205)
| ssPv3(skf1(skf1(X2205)))
| ssPv2(skf1(X2205)) ),
inference(factor,[status(thm)],[c855]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X284,X286)
| ~ ssPv4(X286)
| ~ ssRr(X282,X284)
| ~ ssRr(X283,X281)
| ~ ssRr(X282,X283)
| ~ ssRr(X282,X285)
| ~ ssPv2(X282)
| ssPv4(X281)
| ssPv1(X285) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c142,plain,
( ~ ssRr(X844,X843)
| ~ ssPv4(X843)
| ~ ssRr(X845,X844)
| ~ ssRr(X846,X847)
| ~ ssRr(X845,X846)
| ~ ssPv2(X845)
| ssPv4(X847)
| ssPv1(X846) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c408,plain,
( ~ ssRr(X1815,X1814)
| ~ ssPv4(X1814)
| ~ ssRr(X1816,X1815)
| ~ ssRr(skf1(X1816),X1817)
| ~ ssPv2(X1816)
| ssPv4(X1817)
| ssPv1(skf1(X1816)) ),
inference(resolution,[status(thm)],[c142,clause1]) ).
cnf(c827,plain,
( ~ ssRr(X2180,X2181)
| ~ ssPv4(X2181)
| ~ ssRr(X2182,X2180)
| ~ ssPv2(X2182)
| ssPv4(skf1(skf1(X2182)))
| ssPv1(skf1(X2182)) ),
inference(resolution,[status(thm)],[c408,clause1]) ).
cnf(c943,plain,
( ~ ssRr(X2188,X2188)
| ~ ssPv4(X2188)
| ~ ssPv2(X2188)
| ssPv4(skf1(skf1(X2188)))
| ssPv1(skf1(X2188)) ),
inference(factor,[status(thm)],[c827]) ).
cnf(c575,plain,
( ~ ssRr(X1494,X1496)
| ~ ssPv3(X1496)
| ~ ssRr(X1495,X1494)
| ~ ssRr(X1494,X1497)
| ssPv4(X1497)
| ssPv2(X1497)
| ssPv3(X1495) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c703,plain,
( ~ ssRr(X1799,X1797)
| ~ ssPv3(X1797)
| ~ ssRr(X1798,X1799)
| ssPv4(skf1(X1799))
| ssPv2(skf1(X1799))
| ssPv3(X1798) ),
inference(resolution,[status(thm)],[c575,clause1]) ).
cnf(c818,plain,
( ~ ssRr(skf1(X2174),X2173)
| ~ ssPv3(X2173)
| ssPv4(skf1(skf1(X2174)))
| ssPv2(skf1(skf1(X2174)))
| ssPv3(X2174) ),
inference(resolution,[status(thm)],[c703,clause1]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X269,X271)
| ~ ssPv1(X271)
| ~ ssRr(X267,X269)
| ~ ssRr(X268,X266)
| ~ ssRr(X267,X268)
| ~ ssRr(X267,X270)
| ssPv2(X266)
| ssPv3(X270)
| ssPv3(X267) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c134,plain,
( ~ ssRr(X779,X778)
| ~ ssPv1(X778)
| ~ ssRr(X777,X779)
| ~ ssRr(X776,X780)
| ~ ssRr(X777,X776)
| ssPv2(X780)
| ssPv3(X776)
| ssPv3(X777) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c369,plain,
( ~ ssRr(X1719,X1717)
| ~ ssPv1(X1717)
| ~ ssRr(X1720,X1719)
| ~ ssRr(skf1(X1720),X1718)
| ssPv2(X1718)
| ssPv3(skf1(X1720))
| ssPv3(X1720) ),
inference(resolution,[status(thm)],[c134,clause1]) ).
cnf(c793,plain,
( ~ ssRr(X2148,X2150)
| ~ ssPv1(X2150)
| ~ ssRr(X2149,X2148)
| ssPv2(skf1(skf1(X2149)))
| ssPv3(skf1(X2149))
| ssPv3(X2149) ),
inference(resolution,[status(thm)],[c369,clause1]) ).
cnf(c529,plain,
( ~ ssRr(X1417,X1419)
| ~ ssPv4(X1419)
| ~ ssRr(X1418,X1417)
| ~ ssRr(X1417,X1416)
| ssPv4(X1416)
| ssPv1(X1416)
| ssPv4(X1418) ),
inference(factor,[status(thm)],[c177]) ).
cnf(c668,plain,
( ~ ssRr(X1700,X1699)
| ~ ssPv4(X1699)
| ~ ssRr(X1701,X1700)
| ssPv4(skf1(X1700))
| ssPv1(skf1(X1700))
| ssPv4(X1701) ),
inference(resolution,[status(thm)],[c529,clause1]) ).
cnf(c784,plain,
( ~ ssRr(skf1(X2142),X2141)
| ~ ssPv4(X2141)
| ssPv4(skf1(skf1(X2142)))
| ssPv1(skf1(skf1(X2142)))
| ssPv4(X2142) ),
inference(resolution,[status(thm)],[c668,clause1]) ).
cnf(c932,plain,
( ~ ssRr(X2129,X2130)
| ~ ssPv4(X2130)
| ~ ssRr(X2131,X2129)
| ~ ssRr(X2131,X2131)
| ssPv4(X2131)
| ssPv1(skf1(X2131)) ),
inference(factor,[status(thm)],[c540]) ).
cnf(c925,plain,
( ~ ssRr(X2118,X2116)
| ~ ssPv4(X2116)
| ~ ssRr(X2117,X2118)
| ~ ssRr(X2117,X2117)
| ssPv4(X2117)
| ssPv1(skf1(X2118)) ),
inference(factor,[status(thm)],[c531]) ).
cnf(c928,plain,
( ~ ssRr(X2121,X2120)
| ~ ssPv4(X2120)
| ~ ssRr(X2121,X2121)
| ssPv4(X2121)
| ssPv1(skf1(X2121)) ),
inference(factor,[status(thm)],[c925]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X247,X249)
| ~ ssRr(X245,X247)
| ~ ssRr(X246,X244)
| ~ ssRr(X245,X246)
| ~ ssRr(X245,X248)
| ~ ssPv4(X245)
| ssPv4(X249)
| ssPv1(X244)
| ssPv2(X248) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c123,plain,
( ~ ssRr(X705,X702)
| ~ ssRr(X706,X705)
| ~ ssRr(X703,X704)
| ~ ssRr(X706,X703)
| ~ ssPv4(X706)
| ssPv4(X702)
| ssPv1(X704)
| ssPv2(X703) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c340,plain,
( ~ ssRr(X1622,X1624)
| ~ ssRr(X1625,X1622)
| ~ ssRr(skf1(X1625),X1623)
| ~ ssPv4(X1625)
| ssPv4(X1624)
| ssPv1(X1623)
| ssPv2(skf1(X1625)) ),
inference(resolution,[status(thm)],[c123,clause1]) ).
cnf(c756,plain,
( ~ ssRr(X2107,X2108)
| ~ ssRr(X2109,X2107)
| ~ ssPv4(X2109)
| ssPv4(X2108)
| ssPv1(skf1(skf1(X2109)))
| ssPv2(skf1(X2109)) ),
inference(resolution,[status(thm)],[c340,clause1]) ).
cnf(c530,plain,
( ~ ssRr(X2094,X2096)
| ~ ssPv4(X2096)
| ~ ssRr(X2094,X2094)
| ~ ssRr(X2093,X2095)
| ~ ssRr(X2094,X2093)
| ssPv4(X2095)
| ssPv1(X2093)
| ssPv4(X2094) ),
inference(factor,[status(thm)],[c177]) ).
cnf(c912,plain,
( ~ ssRr(X2071,X2072)
| ~ ssPv4(X2072)
| ~ ssRr(X2070,X2071)
| ~ ssRr(X2070,X2070)
| ssPv4(X2070)
| ssPv1(X2072) ),
inference(factor,[status(thm)],[c527]) ).
cnf(c172,plain,
( ~ ssRr(X1088,X1086)
| ~ ssPv3(X1086)
| ~ ssRr(X1090,X1088)
| ~ ssRr(X1087,X1089)
| ~ ssRr(X1090,X1087)
| ~ ssPv3(skf1(X1090))
| ~ ssPv1(X1090)
| ssPv2(X1089) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(c512,plain,
( ~ ssRr(X2039,skf1(X2042))
| ~ ssPv3(skf1(X2042))
| ~ ssRr(X2042,X2039)
| ~ ssRr(X2040,X2041)
| ~ ssRr(X2042,X2040)
| ~ ssPv1(X2042)
| ssPv2(X2041) ),
inference(factor,[status(thm)],[c172]) ).
cnf(c898,plain,
( ~ ssPv3(skf1(X2049))
| ~ ssRr(X2049,X2049)
| ~ ssRr(X2047,X2048)
| ~ ssRr(X2049,X2047)
| ~ ssPv1(X2049)
| ssPv2(X2048) ),
inference(resolution,[status(thm)],[c512,clause1]) ).
cnf(c902,plain,
( ~ ssPv3(skf1(X2067))
| ~ ssRr(X2067,X2067)
| ~ ssRr(skf1(X2067),X2068)
| ~ ssPv1(X2067)
| ssPv2(X2068) ),
inference(resolution,[status(thm)],[c898,clause1]) ).
cnf(c914,plain,
( ~ ssPv3(skf1(X2069))
| ~ ssRr(X2069,X2069)
| ~ ssPv1(X2069)
| ssPv2(skf1(skf1(X2069))) ),
inference(resolution,[status(thm)],[c902,clause1]) ).
cnf(c176,plain,
( ~ ssRr(X1104,X1102)
| ~ ssPv4(X1102)
| ~ ssRr(X1104,X1104)
| ~ ssRr(X1105,X1101)
| ~ ssRr(X1104,X1105)
| ~ ssRr(X1102,X1103)
| ssPv4(X1101)
| ssPv1(X1103)
| ssPv4(X1104) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c521,plain,
( ~ ssRr(X2052,X2054)
| ~ ssPv4(X2054)
| ~ ssRr(X2052,X2052)
| ~ ssRr(X2053,X2051)
| ~ ssRr(X2052,X2053)
| ssPv4(X2051)
| ssPv1(skf1(X2054))
| ssPv4(X2052) ),
inference(resolution,[status(thm)],[c176,clause1]) ).
cnf(c905,plain,
( ~ ssRr(X2059,X2060)
| ~ ssPv4(X2060)
| ~ ssRr(X2059,X2059)
| ssPv4(X2059)
| ssPv1(skf1(X2060)) ),
inference(factor,[status(thm)],[c521]) ).
cnf(c900,plain,
( ~ ssPv3(skf1(X2055))
| ~ ssRr(X2055,X2055)
| ~ ssRr(X2055,X2056)
| ~ ssPv1(X2055)
| ssPv2(X2056) ),
inference(factor,[status(thm)],[c898]) ).
cnf(c901,plain,
( ~ ssPv3(skf1(X2050))
| ~ ssRr(X2050,X2050)
| ~ ssPv1(X2050)
| ssPv2(X2050) ),
inference(factor,[status(thm)],[c898]) ).
cnf(c896,plain,
( ~ ssRr(X2044,skf1(X2045))
| ~ ssPv3(skf1(X2045))
| ~ ssRr(X2045,X2044)
| ~ ssPv1(X2045)
| ssPv2(skf1(X2045)) ),
inference(factor,[status(thm)],[c512]) ).
cnf(c899,plain,
( ~ ssPv3(skf1(X2046))
| ~ ssRr(X2046,X2046)
| ~ ssPv1(X2046)
| ssPv2(skf1(X2046)) ),
inference(resolution,[status(thm)],[c896,clause1]) ).
cnf(c169,plain,
( ~ ssRr(X1043,X1039)
| ~ ssPv3(X1039)
| ~ ssRr(X1041,X1043)
| ~ ssRr(X1040,X1042)
| ~ ssRr(X1041,X1040)
| ~ ssPv3(X1043)
| ~ ssPv1(X1041)
| ssPv2(X1042) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c499,plain,
( ~ ssRr(X2010,X2011)
| ~ ssPv3(X2011)
| ~ ssRr(X2012,X2010)
| ~ ssRr(skf1(X2012),X2009)
| ~ ssPv3(X2010)
| ~ ssPv1(X2012)
| ssPv2(X2009) ),
inference(resolution,[status(thm)],[c169,clause1]) ).
cnf(c889,plain,
( ~ ssRr(X2036,X2038)
| ~ ssPv3(X2038)
| ~ ssRr(X2037,X2036)
| ~ ssPv3(X2036)
| ~ ssPv1(X2037)
| ssPv2(skf1(skf1(X2037))) ),
inference(resolution,[status(thm)],[c499,clause1]) ).
cnf(c160,plain,
( ~ ssRr(X968,X971)
| ~ ssPv3(X971)
| ~ ssRr(X970,X968)
| ~ ssRr(X972,X969)
| ~ ssPv2(X969)
| ~ ssRr(X970,X972)
| ~ ssPv1(X968)
| ssPv3(X970) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c465,plain,
( ~ ssRr(X1984,X1983)
| ~ ssPv3(X1983)
| ~ ssRr(X1985,X1984)
| ~ ssRr(skf1(X1985),X1986)
| ~ ssPv2(X1986)
| ~ ssPv1(X1984)
| ssPv3(X1985) ),
inference(resolution,[status(thm)],[c160,clause1]) ).
cnf(c879,plain,
( ~ ssRr(X2030,X2031)
| ~ ssPv3(X2031)
| ~ ssRr(X2029,X2030)
| ~ ssPv2(skf1(skf1(X2029)))
| ~ ssPv1(X2030)
| ssPv3(X2029) ),
inference(resolution,[status(thm)],[c465,clause1]) ).
cnf(c159,plain,
( ~ ssRr(X955,X956)
| ~ ssPv3(X956)
| ~ ssRr(X955,X955)
| ~ ssRr(X958,X957)
| ~ ssPv2(X957)
| ~ ssRr(X955,X958)
| ~ ssPv1(X956)
| ssPv3(X955) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c459,plain,
( ~ ssRr(X1973,X1972)
| ~ ssPv3(X1972)
| ~ ssRr(X1973,X1973)
| ~ ssRr(skf1(X1973),X1974)
| ~ ssPv2(X1974)
| ~ ssPv1(X1972)
| ssPv3(X1973) ),
inference(resolution,[status(thm)],[c159,clause1]) ).
cnf(c876,plain,
( ~ ssRr(X2028,X2027)
| ~ ssPv3(X2027)
| ~ ssRr(X2028,X2028)
| ~ ssPv2(skf1(skf1(X2028)))
| ~ ssPv1(X2027)
| ssPv3(X2028) ),
inference(resolution,[status(thm)],[c459,clause1]) ).
cnf(c154,plain,
( ~ ssRr(X943,X945)
| ~ ssPv4(X945)
| ~ ssRr(X944,X943)
| ~ ssRr(X942,X946)
| ~ ssRr(X944,X942)
| ~ ssPv1(X944)
| ssPv3(X946)
| ssPv2(skf1(X944)) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c449,plain,
( ~ ssRr(X1935,X1934)
| ~ ssPv4(X1934)
| ~ ssRr(X1936,X1935)
| ~ ssRr(X1935,X1933)
| ~ ssPv1(X1936)
| ssPv3(X1933)
| ssPv2(skf1(X1936)) ),
inference(factor,[status(thm)],[c154]) ).
cnf(c865,plain,
( ~ ssRr(X2015,X2013)
| ~ ssPv4(X2013)
| ~ ssRr(X2014,X2015)
| ~ ssPv1(X2014)
| ssPv3(skf1(X2015))
| ssPv2(skf1(X2014)) ),
inference(resolution,[status(thm)],[c449,clause1]) ).
cnf(c448,plain,
( ~ ssRr(X1926,X1925)
| ~ ssPv4(X1925)
| ~ ssRr(X1926,X1926)
| ~ ssRr(X1925,X1924)
| ~ ssPv1(X1926)
| ssPv3(X1924)
| ssPv2(skf1(X1926)) ),
inference(factor,[status(thm)],[c154]) ).
cnf(c861,plain,
( ~ ssRr(X2006,X2007)
| ~ ssPv4(X2007)
| ~ ssRr(X2006,X2006)
| ~ ssPv1(X2006)
| ssPv3(skf1(X2007))
| ssPv2(skf1(X2006)) ),
inference(resolution,[status(thm)],[c448,clause1]) ).
cnf(c151,plain,
( ~ ssRr(X895,X897)
| ~ ssPv4(X897)
| ~ ssRr(X896,X895)
| ~ ssRr(X894,X898)
| ~ ssRr(X896,X894)
| ~ ssPv1(X896)
| ssPv3(X898)
| ssPv2(X895) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c427,plain,
( ~ ssRr(X1900,X1901)
| ~ ssPv4(X1901)
| ~ ssRr(X1902,X1900)
| ~ ssRr(skf1(X1902),X1899)
| ~ ssPv1(X1902)
| ssPv3(X1899)
| ssPv2(X1900) ),
inference(resolution,[status(thm)],[c151,clause1]) ).
cnf(c849,plain,
( ~ ssRr(X2000,X2001)
| ~ ssPv4(X2001)
| ~ ssRr(X2002,X2000)
| ~ ssPv1(X2002)
| ssPv3(skf1(skf1(X2002)))
| ssPv2(X2000) ),
inference(resolution,[status(thm)],[c427,clause1]) ).
cnf(c150,plain,
( ~ ssRr(X884,X883)
| ~ ssPv4(X883)
| ~ ssRr(X884,X884)
| ~ ssRr(X881,X882)
| ~ ssRr(X884,X881)
| ~ ssPv1(X884)
| ssPv3(X882)
| ssPv2(X883) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c422,plain,
( ~ ssRr(X1887,X1886)
| ~ ssPv4(X1886)
| ~ ssRr(X1887,X1887)
| ~ ssRr(skf1(X1887),X1888)
| ~ ssPv1(X1887)
| ssPv3(X1888)
| ssPv2(X1886) ),
inference(resolution,[status(thm)],[c150,clause1]) ).
cnf(c844,plain,
( ~ ssRr(X1992,X1991)
| ~ ssPv4(X1991)
| ~ ssRr(X1992,X1992)
| ~ ssPv1(X1992)
| ssPv3(skf1(skf1(X1992)))
| ssPv2(X1991) ),
inference(resolution,[status(thm)],[c422,clause1]) ).
cnf(c882,plain,
( ~ ssRr(X1993,X1993)
| ~ ssPv4(X1993)
| ~ ssPv1(X1993)
| ssPv3(skf1(skf1(X1993)))
| ssPv2(X1993) ),
inference(factor,[status(thm)],[c844]) ).
cnf(c143,plain,
( ~ ssRr(X861,X860)
| ~ ssPv4(X860)
| ~ ssRr(X862,X861)
| ~ ssRr(X864,X863)
| ~ ssRr(X862,X864)
| ~ ssPv2(X862)
| ssPv4(X863)
| ssPv1(skf1(X862)) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(c413,plain,
( ~ ssRr(X1841,X1840)
| ~ ssPv4(X1840)
| ~ ssRr(X1838,X1841)
| ~ ssRr(X1841,X1839)
| ~ ssPv2(X1838)
| ssPv4(X1839)
| ssPv1(skf1(X1838)) ),
inference(factor,[status(thm)],[c143]) ).
cnf(c839,plain,
( ~ ssRr(X1989,X1988)
| ~ ssPv4(X1988)
| ~ ssRr(X1987,X1989)
| ~ ssPv2(X1987)
| ssPv4(skf1(X1989))
| ssPv1(skf1(X1987)) ),
inference(resolution,[status(thm)],[c413,clause1]) ).
cnf(c412,plain,
( ~ ssRr(X1828,X1830)
| ~ ssPv4(X1830)
| ~ ssRr(X1828,X1828)
| ~ ssRr(X1830,X1829)
| ~ ssPv2(X1828)
| ssPv4(X1829)
| ssPv1(skf1(X1828)) ),
inference(factor,[status(thm)],[c143]) ).
cnf(c834,plain,
( ~ ssRr(X1980,X1981)
| ~ ssPv4(X1981)
| ~ ssRr(X1980,X1980)
| ~ ssPv2(X1980)
| ssPv4(skf1(X1981))
| ssPv1(skf1(X1980)) ),
inference(resolution,[status(thm)],[c412,clause1]) ).
cnf(c710,plain,
( ~ ssRr(X1809,X1806)
| ~ ssPv4(X1806)
| ~ ssRr(X1808,X1809)
| ~ ssRr(X1809,X1807)
| ~ ssPv3(X1807)
| ~ ssPv1(X1807)
| ssPv2(X1808) ),
inference(factor,[status(thm)],[c216]) ).
cnf(c821,plain,
( ~ ssRr(X1810,X1812)
| ~ ssPv4(X1812)
| ~ ssRr(X1811,X1810)
| ~ ssPv3(X1812)
| ~ ssPv1(X1812)
| ssPv2(X1811) ),
inference(factor,[status(thm)],[c710]) ).
cnf(c825,plain,
( ~ ssRr(skf1(X1819),X1818)
| ~ ssPv4(X1818)
| ~ ssPv3(X1818)
| ~ ssPv1(X1818)
| ssPv2(X1819) ),
inference(resolution,[status(thm)],[c821,clause1]) ).
cnf(c828,plain,
( ~ ssPv4(skf1(skf1(X1979)))
| ~ ssPv3(skf1(skf1(X1979)))
| ~ ssPv1(skf1(skf1(X1979)))
| ssPv2(X1979) ),
inference(resolution,[status(thm)],[c825,clause1]) ).
cnf(c823,plain,
( ~ ssRr(X1977,X1978)
| ~ ssPv4(X1978)
| ~ ssRr(X1976,X1977)
| ~ ssPv3(skf1(X1977))
| ~ ssPv1(skf1(X1977))
| ssPv2(X1976) ),
inference(resolution,[status(thm)],[c710,clause1]) ).
cnf(c140,plain,
( ~ ssRr(X819,X817)
| ~ ssPv4(X817)
| ~ ssRr(X818,X819)
| ~ ssRr(X821,X820)
| ~ ssRr(X818,X821)
| ~ ssPv2(X818)
| ssPv4(X820)
| ssPv1(X819) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c394,plain,
( ~ ssRr(X1803,X1800)
| ~ ssPv4(X1800)
| ~ ssRr(X1802,X1803)
| ~ ssRr(skf1(X1802),X1801)
| ~ ssPv2(X1802)
| ssPv4(X1801)
| ssPv1(X1803) ),
inference(resolution,[status(thm)],[c140,clause1]) ).
cnf(c820,plain,
( ~ ssRr(X1971,X1969)
| ~ ssPv4(X1969)
| ~ ssRr(X1970,X1971)
| ~ ssPv2(X1970)
| ssPv4(skf1(skf1(X1970)))
| ssPv1(X1971) ),
inference(resolution,[status(thm)],[c394,clause1]) ).
cnf(c699,plain,
( ~ ssRr(X1792,X1792)
| ~ ssPv4(X1792)
| ~ ssRr(X1793,X1791)
| ~ ssPv3(X1791)
| ~ ssRr(X1792,X1793)
| ~ ssPv1(X1793)
| ssPv2(X1792) ),
inference(factor,[status(thm)],[c215]) ).
cnf(c816,plain,
( ~ ssRr(X1966,X1966)
| ~ ssPv4(X1966)
| ~ ssRr(skf1(X1966),X1967)
| ~ ssPv3(X1967)
| ~ ssPv1(skf1(X1966))
| ssPv2(X1966) ),
inference(resolution,[status(thm)],[c699,clause1]) ).
cnf(c873,plain,
( ~ ssRr(X1968,X1968)
| ~ ssPv4(X1968)
| ~ ssPv3(skf1(skf1(X1968)))
| ~ ssPv1(skf1(X1968))
| ssPv2(X1968) ),
inference(resolution,[status(thm)],[c816,clause1]) ).
cnf(c139,plain,
( ~ ssRr(X803,X805)
| ~ ssPv4(X805)
| ~ ssRr(X803,X803)
| ~ ssRr(X804,X802)
| ~ ssRr(X803,X804)
| ~ ssPv2(X803)
| ssPv4(X802)
| ssPv1(X805) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c384,plain,
( ~ ssRr(X1788,X1789)
| ~ ssPv4(X1789)
| ~ ssRr(X1788,X1788)
| ~ ssRr(skf1(X1788),X1787)
| ~ ssPv2(X1788)
| ssPv4(X1787)
| ssPv1(X1789) ),
inference(resolution,[status(thm)],[c139,clause1]) ).
cnf(c813,plain,
( ~ ssRr(X1963,X1964)
| ~ ssPv4(X1964)
| ~ ssRr(X1963,X1963)
| ~ ssPv2(X1963)
| ssPv4(skf1(skf1(X1963)))
| ssPv1(X1964) ),
inference(resolution,[status(thm)],[c384,clause1]) ).
cnf(c872,plain,
( ~ ssRr(X1965,X1965)
| ~ ssPv4(X1965)
| ~ ssPv2(X1965)
| ssPv4(skf1(skf1(X1965)))
| ssPv1(X1965) ),
inference(factor,[status(thm)],[c813]) ).
cnf(c698,plain,
( ~ ssRr(X1783,X1784)
| ~ ssPv4(X1784)
| ~ ssRr(X1783,X1783)
| ~ ssRr(X1784,X1785)
| ~ ssPv3(X1785)
| ~ ssPv1(X1785)
| ssPv2(X1783) ),
inference(factor,[status(thm)],[c215]) ).
cnf(c812,plain,
( ~ ssRr(X1957,X1958)
| ~ ssPv4(X1958)
| ~ ssRr(X1957,X1957)
| ~ ssPv3(skf1(X1958))
| ~ ssPv1(skf1(X1958))
| ssPv2(X1957) ),
inference(resolution,[status(thm)],[c698,clause1]) ).
cnf(c135,plain,
( ~ ssRr(X791,X790)
| ~ ssPv1(X790)
| ~ ssRr(X792,X791)
| ~ ssRr(X789,X793)
| ~ ssRr(X792,X789)
| ssPv2(X793)
| ssPv3(skf1(X792))
| ssPv3(X792) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c374,plain,
( ~ ssRr(X1750,X1749)
| ~ ssPv1(X1749)
| ~ ssRr(X1751,X1750)
| ~ ssRr(X1750,X1748)
| ssPv2(X1748)
| ssPv3(skf1(X1751))
| ssPv3(X1751) ),
inference(factor,[status(thm)],[c135]) ).
cnf(c802,plain,
( ~ ssRr(X1955,X1953)
| ~ ssPv1(X1953)
| ~ ssRr(X1954,X1955)
| ssPv2(skf1(X1955))
| ssPv3(skf1(X1954))
| ssPv3(X1954) ),
inference(resolution,[status(thm)],[c374,clause1]) ).
cnf(c132,plain,
( ~ ssRr(X750,X752)
| ~ ssPv1(X752)
| ~ ssRr(X751,X750)
| ~ ssRr(X749,X753)
| ~ ssRr(X751,X749)
| ssPv2(X753)
| ssPv3(X750)
| ssPv3(X751) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c356,plain,
( ~ ssRr(X1703,X1705)
| ~ ssPv1(X1705)
| ~ ssRr(X1706,X1703)
| ~ ssRr(skf1(X1706),X1704)
| ssPv2(X1704)
| ssPv3(X1703)
| ssPv3(X1706) ),
inference(resolution,[status(thm)],[c132,clause1]) ).
cnf(c786,plain,
( ~ ssRr(X1945,X1946)
| ~ ssPv1(X1946)
| ~ ssRr(X1947,X1945)
| ssPv2(skf1(skf1(X1947)))
| ssPv3(X1945)
| ssPv3(X1947) ),
inference(resolution,[status(thm)],[c356,clause1]) ).
cnf(c863,plain,
( ~ ssRr(X1938,X1937)
| ~ ssPv4(X1937)
| ~ ssRr(X1939,X1938)
| ~ ssPv1(X1939)
| ssPv3(X1937)
| ssPv2(skf1(X1939)) ),
inference(factor,[status(thm)],[c449]) ).
cnf(c776,plain,
( ~ ssRr(X1690,X1689)
| ~ ssPv4(X1689)
| ~ ssRr(X1688,X1690)
| ~ ssPv2(X1688)
| ssPv3(X1689)
| ssPv2(X1689) ),
inference(factor,[status(thm)],[c663]) ).
cnf(c780,plain,
( ~ ssRr(skf1(X1696),X1695)
| ~ ssPv4(X1695)
| ~ ssPv2(X1696)
| ssPv3(X1695)
| ssPv2(X1695) ),
inference(resolution,[status(thm)],[c776,clause1]) ).
cnf(c782,plain,
( ~ ssPv4(skf1(skf1(X1932)))
| ~ ssPv2(X1932)
| ssPv3(skf1(skf1(X1932)))
| ssPv2(skf1(skf1(X1932))) ),
inference(resolution,[status(thm)],[c780,clause1]) ).
cnf(c131,plain,
( ~ ssRr(X739,X738)
| ~ ssPv1(X738)
| ~ ssRr(X739,X739)
| ~ ssRr(X741,X740)
| ~ ssRr(X739,X741)
| ssPv2(X740)
| ssPv3(X738)
| ssPv3(X739) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c351,plain,
( ~ ssRr(X1693,X1691)
| ~ ssPv1(X1691)
| ~ ssRr(X1693,X1693)
| ~ ssRr(skf1(X1693),X1692)
| ssPv2(X1692)
| ssPv3(X1691)
| ssPv3(X1693) ),
inference(resolution,[status(thm)],[c131,clause1]) ).
cnf(c781,plain,
( ~ ssRr(X1929,X1930)
| ~ ssPv1(X1930)
| ~ ssRr(X1929,X1929)
| ssPv2(skf1(skf1(X1929)))
| ssPv3(X1930)
| ssPv3(X1929) ),
inference(resolution,[status(thm)],[c351,clause1]) ).
cnf(c862,plain,
( ~ ssRr(X1931,X1931)
| ~ ssPv1(X1931)
| ssPv2(skf1(skf1(X1931)))
| ssPv3(X1931) ),
inference(factor,[status(thm)],[c781]) ).
cnf(c656,plain,
( ~ ssRr(X1671,X1671)
| ~ ssPv4(X1671)
| ~ ssRr(X1673,X1672)
| ~ ssRr(X1671,X1673)
| ~ ssPv2(X1671)
| ssPv3(X1672)
| ssPv2(X1673) ),
inference(factor,[status(thm)],[c208]) ).
cnf(c774,plain,
( ~ ssRr(X1918,X1918)
| ~ ssPv4(X1918)
| ~ ssRr(skf1(X1918),X1917)
| ~ ssPv2(X1918)
| ssPv3(X1917)
| ssPv2(skf1(X1918)) ),
inference(resolution,[status(thm)],[c656,clause1]) ).
cnf(c856,plain,
( ~ ssRr(X1919,X1919)
| ~ ssPv4(X1919)
| ~ ssPv2(X1919)
| ssPv3(skf1(skf1(X1919)))
| ssPv2(skf1(X1919)) ),
inference(resolution,[status(thm)],[c774,clause1]) ).
cnf(c124,plain,
( ~ ssRr(X722,X718)
| ~ ssRr(X721,X722)
| ~ ssRr(X720,X719)
| ~ ssRr(X721,X720)
| ~ ssPv4(X721)
| ssPv4(X718)
| ssPv1(X719)
| ssPv2(skf1(X721)) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c342,plain,
( ~ ssRr(X1654,X1652)
| ~ ssRr(X1653,X1654)
| ~ ssRr(X1654,X1651)
| ~ ssPv4(X1653)
| ssPv4(X1652)
| ssPv1(X1651)
| ssPv2(skf1(X1653)) ),
inference(factor,[status(thm)],[c124]) ).
cnf(c766,plain,
( ~ ssRr(X1911,X1910)
| ~ ssRr(X1909,X1911)
| ~ ssPv4(X1909)
| ssPv4(X1910)
| ssPv1(skf1(X1911))
| ssPv2(skf1(X1909)) ),
inference(resolution,[status(thm)],[c342,clause1]) ).
cnf(c655,plain,
( ~ ssRr(X1649,X1647)
| ~ ssPv4(X1647)
| ~ ssRr(X1649,X1649)
| ~ ssRr(X1647,X1648)
| ~ ssPv2(X1649)
| ssPv3(X1648)
| ssPv2(X1648) ),
inference(factor,[status(thm)],[c208]) ).
cnf(c763,plain,
( ~ ssRr(X1907,X1906)
| ~ ssPv4(X1906)
| ~ ssRr(X1907,X1907)
| ~ ssPv2(X1907)
| ssPv3(skf1(X1906))
| ssPv2(skf1(X1906)) ),
inference(resolution,[status(thm)],[c655,clause1]) ).
cnf(c851,plain,
( ~ ssRr(X1908,X1908)
| ~ ssPv4(X1908)
| ~ ssPv2(X1908)
| ssPv3(skf1(X1908))
| ssPv2(skf1(X1908)) ),
inference(factor,[status(thm)],[c763]) ).
cnf(c341,plain,
( ~ ssRr(X1640,X1641)
| ~ ssRr(X1640,X1640)
| ~ ssRr(X1641,X1639)
| ~ ssPv4(X1640)
| ssPv4(X1641)
| ssPv1(X1639)
| ssPv2(skf1(X1640)) ),
inference(factor,[status(thm)],[c124]) ).
cnf(c760,plain,
( ~ ssRr(X1904,X1903)
| ~ ssRr(X1904,X1904)
| ~ ssPv4(X1904)
| ssPv4(X1903)
| ssPv1(skf1(X1903))
| ssPv2(skf1(X1904)) ),
inference(resolution,[status(thm)],[c341,clause1]) ).
cnf(c121,plain,
( ~ ssRr(X673,X672)
| ~ ssRr(X676,X673)
| ~ ssRr(X675,X674)
| ~ ssRr(X676,X675)
| ~ ssPv4(X676)
| ssPv4(X672)
| ssPv1(X674)
| ssPv2(X673) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c327,plain,
( ~ ssRr(X1606,X1608)
| ~ ssRr(X1607,X1606)
| ~ ssRr(skf1(X1607),X1605)
| ~ ssPv4(X1607)
| ssPv4(X1608)
| ssPv1(X1605)
| ssPv2(X1606) ),
inference(resolution,[status(thm)],[c121,clause1]) ).
cnf(c754,plain,
( ~ ssRr(X1896,X1897)
| ~ ssRr(X1895,X1896)
| ~ ssPv4(X1895)
| ssPv4(X1897)
| ssPv1(skf1(skf1(X1895)))
| ssPv2(X1896) ),
inference(resolution,[status(thm)],[c327,clause1]) ).
cnf(c622,plain,
( ~ ssRr(X1599,X1600)
| ~ ssPv4(X1600)
| ~ ssRr(X1601,X1599)
| ~ ssRr(X1599,X1598)
| ~ ssPv3(X1598)
| ssPv4(X1598)
| ssPv3(X1601) ),
inference(factor,[status(thm)],[c200]) ).
cnf(c752,plain,
( ~ ssRr(X1894,X1892)
| ~ ssPv4(X1892)
| ~ ssRr(X1893,X1894)
| ~ ssPv3(skf1(X1894))
| ssPv4(skf1(X1894))
| ssPv3(X1893) ),
inference(resolution,[status(thm)],[c622,clause1]) ).
cnf(c615,plain,
( ~ ssRr(X1594,X1594)
| ~ ssPv4(X1594)
| ~ ssRr(X1593,X1592)
| ~ ssPv3(X1592)
| ~ ssRr(X1594,X1593)
| ssPv4(X1593)
| ssPv3(X1594) ),
inference(factor,[status(thm)],[c199]) ).
cnf(c749,plain,
( ~ ssRr(X1890,X1890)
| ~ ssPv4(X1890)
| ~ ssRr(skf1(X1890),X1889)
| ~ ssPv3(X1889)
| ssPv4(skf1(X1890))
| ssPv3(X1890) ),
inference(resolution,[status(thm)],[c615,clause1]) ).
cnf(c845,plain,
( ~ ssRr(X1891,X1891)
| ~ ssPv4(X1891)
| ~ ssPv3(skf1(skf1(X1891)))
| ssPv4(skf1(X1891))
| ssPv3(X1891) ),
inference(resolution,[status(thm)],[c749,clause1]) ).
cnf(c120,plain,
( ~ ssRr(X660,X661)
| ~ ssRr(X660,X660)
| ~ ssRr(X662,X659)
| ~ ssRr(X660,X662)
| ~ ssPv4(X660)
| ssPv4(X661)
| ssPv1(X659)
| ssPv2(X661) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c320,plain,
( ~ ssRr(X1591,X1590)
| ~ ssRr(X1591,X1591)
| ~ ssRr(skf1(X1591),X1589)
| ~ ssPv4(X1591)
| ssPv4(X1590)
| ssPv1(X1589)
| ssPv2(X1590) ),
inference(resolution,[status(thm)],[c120,clause1]) ).
cnf(c746,plain,
( ~ ssRr(X1884,X1883)
| ~ ssRr(X1884,X1884)
| ~ ssPv4(X1884)
| ssPv4(X1883)
| ssPv1(skf1(skf1(X1884)))
| ssPv2(X1883) ),
inference(resolution,[status(thm)],[c320,clause1]) ).
cnf(c614,plain,
( ~ ssRr(X1586,X1584)
| ~ ssPv4(X1584)
| ~ ssRr(X1586,X1586)
| ~ ssRr(X1584,X1585)
| ~ ssPv3(X1585)
| ssPv4(X1585)
| ssPv3(X1586) ),
inference(factor,[status(thm)],[c199]) ).
cnf(c745,plain,
( ~ ssRr(X1882,X1881)
| ~ ssPv4(X1881)
| ~ ssRr(X1882,X1882)
| ~ ssPv3(skf1(X1881))
| ssPv4(skf1(X1881))
| ssPv3(X1882) ),
inference(resolution,[status(thm)],[c614,clause1]) ).
cnf(c725,plain,
( ~ ssRr(X1859,X1861)
| ~ ssPv4(X1861)
| ~ ssRr(X1860,X1859)
| ~ ssRr(X1859,X1858)
| ~ ssPv3(X1858)
| ~ ssPv1(X1861)
| ssPv2(X1860) ),
inference(factor,[status(thm)],[c218]) ).
cnf(c842,plain,
( ~ ssRr(X1869,X1868)
| ~ ssPv4(X1868)
| ~ ssRr(X1867,X1869)
| ~ ssPv3(skf1(X1869))
| ~ ssPv1(X1868)
| ssPv2(X1867) ),
inference(resolution,[status(thm)],[c725,clause1]) ).
cnf(c717,plain,
( ~ ssRr(X1836,X1834)
| ~ ssPv4(X1834)
| ~ ssRr(X1835,X1836)
| ~ ssRr(X1835,X1835)
| ~ ssPv3(X1835)
| ~ ssPv1(X1836)
| ssPv2(X1835) ),
inference(factor,[status(thm)],[c217]) ).
cnf(c716,plain,
( ~ ssRr(X1823,X1824)
| ~ ssPv4(X1824)
| ~ ssRr(X1822,X1823)
| ~ ssPv3(X1823)
| ~ ssRr(X1822,X1822)
| ~ ssPv1(X1824)
| ssPv2(X1822) ),
inference(factor,[status(thm)],[c217]) ).
cnf(c830,plain,
( ~ ssRr(X1826,X1827)
| ~ ssPv4(X1827)
| ~ ssRr(X1826,X1826)
| ~ ssPv3(X1826)
| ~ ssPv1(X1827)
| ssPv2(X1826) ),
inference(factor,[status(thm)],[c716]) ).
cnf(c701,plain,
( ~ ssRr(X1499,X1500)
| ~ ssPv3(X1500)
| ~ ssRr(X1498,X1499)
| ssPv4(X1500)
| ssPv2(X1500)
| ssPv3(X1498) ),
inference(factor,[status(thm)],[c575]) ).
cnf(c705,plain,
( ~ ssRr(skf1(X1503),X1502)
| ~ ssPv3(X1502)
| ssPv4(X1502)
| ssPv2(X1502)
| ssPv3(X1503) ),
inference(resolution,[status(thm)],[c701,clause1]) ).
cnf(c706,plain,
( ~ ssPv3(skf1(skf1(X1805)))
| ssPv4(skf1(skf1(X1805)))
| ssPv2(skf1(skf1(X1805)))
| ssPv3(X1805) ),
inference(resolution,[status(thm)],[c705,clause1]) ).
cnf(c696,plain,
( ~ ssRr(X1769,X1769)
| ~ ssPv4(X1769)
| ~ ssRr(X1768,X1767)
| ~ ssPv3(X1767)
| ~ ssRr(X1769,X1768)
| ~ ssPv1(X1769)
| ssPv2(X1769) ),
inference(factor,[status(thm)],[c215]) ).
cnf(c808,plain,
( ~ ssRr(X1778,X1778)
| ~ ssPv4(X1778)
| ~ ssRr(skf1(X1778),X1777)
| ~ ssPv3(X1777)
| ~ ssPv1(X1778)
| ssPv2(X1778) ),
inference(resolution,[status(thm)],[c696,clause1]) ).
cnf(c809,plain,
( ~ ssRr(X1779,X1779)
| ~ ssPv4(X1779)
| ~ ssPv3(skf1(skf1(X1779)))
| ~ ssPv1(X1779)
| ssPv2(X1779) ),
inference(resolution,[status(thm)],[c808,clause1]) ).
cnf(c565,plain,
( ~ ssRr(X1473,X1474)
| ~ ssPv3(X1474)
| ~ ssRr(X1473,X1473)
| ~ ssRr(X1474,X1472)
| ssPv4(X1472)
| ssPv2(X1472)
| ssPv3(X1473) ),
inference(factor,[status(thm)],[c187]) ).
cnf(c691,plain,
( ~ ssRr(X1764,X1765)
| ~ ssPv3(X1765)
| ~ ssRr(X1764,X1764)
| ssPv4(skf1(X1765))
| ssPv2(skf1(X1765))
| ssPv3(X1764) ),
inference(resolution,[status(thm)],[c565,clause1]) ).
cnf(c800,plain,
( ~ ssRr(X1754,X1752)
| ~ ssPv1(X1752)
| ~ ssRr(X1753,X1754)
| ssPv2(X1752)
| ssPv3(skf1(X1753))
| ssPv3(X1753) ),
inference(factor,[status(thm)],[c374]) ).
cnf(c680,plain,
( ~ ssRr(X1733,X1732)
| ~ ssPv4(X1732)
| ~ ssRr(X1730,X1733)
| ~ ssRr(X1733,X1731)
| ~ ssPv2(X1730)
| ssPv3(X1731)
| ssPv2(X1732) ),
inference(factor,[status(thm)],[c211]) ).
cnf(c796,plain,
( ~ ssRr(X1743,X1742)
| ~ ssPv4(X1742)
| ~ ssRr(X1744,X1743)
| ~ ssPv2(X1744)
| ssPv3(skf1(X1743))
| ssPv2(X1742) ),
inference(resolution,[status(thm)],[c680,clause1]) ).
cnf(c798,plain,
( ~ ssRr(skf1(X1746),X1747)
| ~ ssPv4(X1747)
| ~ ssPv2(X1746)
| ssPv3(skf1(skf1(X1746)))
| ssPv2(X1747) ),
inference(resolution,[status(thm)],[c796,clause1]) ).
cnf(c670,plain,
( ~ ssRr(X1715,X1714)
| ~ ssPv4(X1714)
| ~ ssRr(X1716,X1715)
| ~ ssRr(X1716,X1716)
| ~ ssPv2(X1716)
| ssPv3(X1716)
| ssPv2(X1715) ),
inference(factor,[status(thm)],[c210]) ).
cnf(c669,plain,
( ~ ssRr(X1708,X1707)
| ~ ssPv4(X1707)
| ~ ssRr(X1709,X1708)
| ~ ssRr(X1709,X1709)
| ~ ssPv2(X1709)
| ssPv3(X1708)
| ssPv2(X1707) ),
inference(factor,[status(thm)],[c210]) ).
cnf(c788,plain,
( ~ ssRr(X1711,X1712)
| ~ ssPv4(X1712)
| ~ ssRr(X1711,X1711)
| ~ ssPv2(X1711)
| ssPv3(X1711)
| ssPv2(X1712) ),
inference(factor,[status(thm)],[c669]) ).
cnf(c343,plain,
( ~ ssRr(X1666,X1664)
| ~ ssRr(X1665,X1666)
| ~ ssRr(X1665,X1665)
| ~ ssPv4(X1665)
| ssPv4(X1664)
| ssPv1(X1665)
| ssPv2(skf1(X1665)) ),
inference(factor,[status(thm)],[c124]) ).
cnf(c765,plain,
( ~ ssRr(X1662,X1663)
| ~ ssRr(X1662,X1662)
| ~ ssPv4(X1662)
| ssPv4(X1663)
| ssPv1(X1662)
| ssPv2(skf1(X1662)) ),
inference(factor,[status(thm)],[c342]) ).
cnf(c764,plain,
( ~ ssRr(X1658,X1656)
| ~ ssRr(X1657,X1658)
| ~ ssPv4(X1657)
| ssPv4(X1656)
| ssPv1(X1656)
| ssPv2(skf1(X1657)) ),
inference(factor,[status(thm)],[c342]) ).
cnf(c497,plain,
( ~ ssRr(X1360,X1361)
| ~ ssPv3(X1361)
| ~ ssRr(X1359,X1360)
| ~ ssRr(X1360,X1358)
| ~ ssPv3(X1360)
| ~ ssPv1(X1359)
| ssPv2(X1358) ),
inference(factor,[status(thm)],[c169]) ).
cnf(c644,plain,
( ~ ssRr(X1377,X1378)
| ~ ssPv3(X1378)
| ~ ssRr(X1376,X1377)
| ~ ssPv3(X1377)
| ~ ssPv1(X1376)
| ssPv2(skf1(X1377)) ),
inference(resolution,[status(thm)],[c497,clause1]) ).
cnf(c652,plain,
( ~ ssRr(skf1(X1634),X1633)
| ~ ssPv3(X1633)
| ~ ssPv3(skf1(X1634))
| ~ ssPv1(X1634)
| ssPv2(skf1(skf1(X1634))) ),
inference(resolution,[status(thm)],[c644,clause1]) ).
cnf(c161,plain,
( ~ ssRr(X983,X981)
| ~ ssPv3(X981)
| ~ ssRr(X982,X983)
| ~ ssRr(X982,X984)
| ~ ssPv2(X984)
| ~ ssRr(X982,X982)
| ~ ssPv1(X984)
| ssPv3(X982) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c471,plain,
( ~ ssRr(X1311,X1310)
| ~ ssPv3(X1310)
| ~ ssRr(X1311,X1311)
| ~ ssRr(X1311,X1312)
| ~ ssPv2(X1312)
| ~ ssPv1(X1312)
| ssPv3(X1311) ),
inference(factor,[status(thm)],[c161]) ).
cnf(c627,plain,
( ~ ssRr(X1612,X1611)
| ~ ssPv3(X1611)
| ~ ssRr(X1612,X1612)
| ~ ssPv2(skf1(X1612))
| ~ ssPv1(skf1(X1612))
| ssPv3(X1612) ),
inference(resolution,[status(thm)],[c471,clause1]) ).
cnf(c587,plain,
( ~ ssRr(X1546,X1547)
| ~ ssPv3(X1547)
| ~ ssRr(X1548,X1546)
| ~ ssRr(X1546,X1549)
| ssPv4(X1549)
| ssPv2(X1547)
| ssPv3(X1548) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c732,plain,
( ~ ssRr(X1562,X1561)
| ~ ssPv3(X1561)
| ~ ssRr(X1560,X1562)
| ssPv4(skf1(X1562))
| ssPv2(X1561)
| ssPv3(X1560) ),
inference(resolution,[status(thm)],[c587,clause1]) ).
cnf(c738,plain,
( ~ ssRr(skf1(X1565),X1564)
| ~ ssPv3(X1564)
| ssPv4(skf1(skf1(X1565)))
| ssPv2(X1564)
| ssPv3(X1565) ),
inference(resolution,[status(thm)],[c732,clause1]) ).
cnf(c219,plain,
( ~ ssRr(X1558,X1559)
| ~ ssPv4(X1559)
| ~ ssRr(X1556,X1558)
| ~ ssRr(X1557,X1555)
| ~ ssPv3(X1555)
| ~ ssRr(X1556,X1557)
| ~ ssRr(X1556,X1556)
| ~ ssPv1(X1556)
| ssPv2(X1556) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c581,plain,
( ~ ssRr(X1531,X1533)
| ~ ssPv3(X1533)
| ~ ssRr(X1532,X1531)
| ~ ssRr(X1532,X1532)
| ssPv4(X1532)
| ssPv2(X1532)
| ssPv3(X1532) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c580,plain,
( ~ ssRr(X1526,X1527)
| ~ ssPv3(X1527)
| ~ ssRr(X1525,X1526)
| ~ ssRr(X1525,X1525)
| ssPv4(X1525)
| ssPv2(X1526)
| ssPv3(X1525) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c579,plain,
( ~ ssRr(X1513,X1514)
| ~ ssPv3(X1514)
| ~ ssRr(X1515,X1513)
| ~ ssRr(X1515,X1515)
| ssPv4(X1513)
| ssPv2(X1514)
| ssPv3(X1515) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c714,plain,
( ~ ssRr(X1518,X1517)
| ~ ssPv3(X1517)
| ~ ssRr(X1518,X1518)
| ssPv4(X1518)
| ssPv2(X1517)
| ssPv3(X1518) ),
inference(factor,[status(thm)],[c579]) ).
cnf(c702,plain,
( ~ ssRr(X1504,X1505)
| ~ ssPv3(X1505)
| ~ ssRr(X1504,X1504)
| ssPv4(X1504)
| ssPv2(X1504)
| ssPv3(X1504) ),
inference(factor,[status(thm)],[c575]) ).
cnf(c425,plain,
( ~ ssRr(X1167,X1170)
| ~ ssPv4(X1170)
| ~ ssRr(X1168,X1167)
| ~ ssRr(X1167,X1169)
| ~ ssPv1(X1168)
| ssPv3(X1169)
| ssPv2(X1167) ),
inference(factor,[status(thm)],[c151]) ).
cnf(c554,plain,
( ~ ssRr(X1186,X1185)
| ~ ssPv4(X1185)
| ~ ssRr(X1187,X1186)
| ~ ssPv1(X1187)
| ssPv3(skf1(X1186))
| ssPv2(X1186) ),
inference(resolution,[status(thm)],[c425,clause1]) ).
cnf(c562,plain,
( ~ ssRr(skf1(X1464),X1463)
| ~ ssPv4(X1463)
| ~ ssPv1(X1464)
| ssPv3(skf1(skf1(X1464)))
| ssPv2(skf1(X1464)) ),
inference(resolution,[status(thm)],[c554,clause1]) ).
cnf(c544,plain,
( ~ ssRr(X1440,X1437)
| ~ ssPv4(X1437)
| ~ ssRr(X1438,X1440)
| ~ ssRr(X1440,X1439)
| ssPv4(X1439)
| ssPv1(X1437)
| ssPv4(X1438) ),
inference(factor,[status(thm)],[c179]) ).
cnf(c679,plain,
( ~ ssRr(X1454,X1453)
| ~ ssPv4(X1453)
| ~ ssRr(X1452,X1454)
| ssPv4(skf1(X1454))
| ssPv1(X1453)
| ssPv4(X1452) ),
inference(resolution,[status(thm)],[c544,clause1]) ).
cnf(c686,plain,
( ~ ssRr(skf1(X1457),X1456)
| ~ ssPv4(X1456)
| ssPv4(skf1(skf1(X1457)))
| ssPv1(X1456)
| ssPv4(X1457) ),
inference(resolution,[status(thm)],[c679,clause1]) ).
cnf(c536,plain,
( ~ ssRr(X1431,X1432)
| ~ ssPv4(X1432)
| ~ ssRr(X1430,X1431)
| ~ ssRr(X1430,X1430)
| ssPv4(X1431)
| ssPv1(X1432)
| ssPv4(X1430) ),
inference(factor,[status(thm)],[c178]) ).
cnf(c675,plain,
( ~ ssRr(X1435,X1434)
| ~ ssPv4(X1434)
| ~ ssRr(X1435,X1435)
| ssPv4(X1435)
| ssPv1(X1434) ),
inference(factor,[status(thm)],[c536]) ).
cnf(c519,plain,
( ~ ssRr(X1402,X1403)
| ~ ssPv4(X1403)
| ~ ssRr(X1402,X1402)
| ~ ssRr(X1403,X1404)
| ssPv4(X1404)
| ssPv1(X1404)
| ssPv4(X1402) ),
inference(factor,[status(thm)],[c176]) ).
cnf(c642,plain,
( ~ ssRr(X1362,X1363)
| ~ ssPv3(X1363)
| ~ ssRr(X1364,X1362)
| ~ ssPv3(X1362)
| ~ ssPv1(X1364)
| ssPv2(X1363) ),
inference(factor,[status(thm)],[c497]) ).
cnf(c646,plain,
( ~ ssRr(skf1(X1368),X1369)
| ~ ssPv3(X1369)
| ~ ssPv3(skf1(X1368))
| ~ ssPv1(X1368)
| ssPv2(X1369) ),
inference(resolution,[status(thm)],[c642,clause1]) ).
cnf(c647,plain,
( ~ ssPv3(skf1(skf1(X1380)))
| ~ ssPv3(skf1(X1380))
| ~ ssPv1(X1380)
| ssPv2(skf1(skf1(X1380))) ),
inference(resolution,[status(thm)],[c646,clause1]) ).
cnf(c392,plain,
( ~ ssRr(X990,X988)
| ~ ssPv4(X988)
| ~ ssRr(X991,X990)
| ~ ssRr(X990,X989)
| ~ ssPv2(X991)
| ssPv4(X989)
| ssPv1(X990) ),
inference(factor,[status(thm)],[c140]) ).
cnf(c475,plain,
( ~ ssRr(X1003,X1002)
| ~ ssPv4(X1002)
| ~ ssRr(X1004,X1003)
| ~ ssPv2(X1004)
| ssPv4(skf1(X1003))
| ssPv1(X1003) ),
inference(resolution,[status(thm)],[c392,clause1]) ).
cnf(c481,plain,
( ~ ssRr(skf1(X1344),X1345)
| ~ ssPv4(X1345)
| ~ ssPv2(X1344)
| ssPv4(skf1(skf1(X1344)))
| ssPv1(skf1(X1344)) ),
inference(resolution,[status(thm)],[c475,clause1]) ).
cnf(c472,plain,
( ~ ssRr(X1319,X1317)
| ~ ssPv3(X1317)
| ~ ssRr(X1318,X1319)
| ~ ssRr(X1318,X1318)
| ~ ssPv2(X1318)
| ~ ssPv1(X1318)
| ssPv3(X1318) ),
inference(factor,[status(thm)],[c161]) ).
cnf(c464,plain,
( ~ ssRr(X1299,X1298)
| ~ ssPv3(X1298)
| ~ ssRr(X1300,X1299)
| ~ ssRr(X1300,X1300)
| ~ ssPv2(X1300)
| ~ ssPv1(X1299)
| ssPv3(X1300) ),
inference(factor,[status(thm)],[c160]) ).
cnf(c463,plain,
( ~ ssRr(X1277,X1276)
| ~ ssPv3(X1276)
| ~ ssRr(X1278,X1277)
| ~ ssRr(X1277,X1279)
| ~ ssPv2(X1279)
| ~ ssPv1(X1277)
| ssPv3(X1278) ),
inference(factor,[status(thm)],[c160]) ).
cnf(c606,plain,
( ~ ssRr(X1281,X1280)
| ~ ssPv3(X1280)
| ~ ssRr(X1282,X1281)
| ~ ssPv2(X1280)
| ~ ssPv1(X1281)
| ssPv3(X1282) ),
inference(factor,[status(thm)],[c463]) ).
cnf(c610,plain,
( ~ ssRr(skf1(X1293),X1292)
| ~ ssPv3(X1292)
| ~ ssPv2(X1292)
| ~ ssPv1(skf1(X1293))
| ssPv3(X1293) ),
inference(resolution,[status(thm)],[c606,clause1]) ).
cnf(c617,plain,
( ~ ssPv3(skf1(skf1(X1297)))
| ~ ssPv2(skf1(skf1(X1297)))
| ~ ssPv1(skf1(X1297))
| ssPv3(X1297) ),
inference(resolution,[status(thm)],[c610,clause1]) ).
cnf(c608,plain,
( ~ ssRr(X1296,X1294)
| ~ ssPv3(X1294)
| ~ ssRr(X1295,X1296)
| ~ ssPv2(skf1(X1296))
| ~ ssPv1(X1296)
| ssPv3(X1295) ),
inference(resolution,[status(thm)],[c463,clause1]) ).
cnf(c607,plain,
( ~ ssRr(X1284,X1285)
| ~ ssPv3(X1285)
| ~ ssRr(X1284,X1284)
| ~ ssPv2(X1284)
| ~ ssPv1(X1284)
| ssPv3(X1284) ),
inference(factor,[status(thm)],[c463]) ).
cnf(c462,plain,
( ~ ssRr(X1264,X1263)
| ~ ssPv3(X1263)
| ~ ssRr(X1264,X1264)
| ~ ssRr(X1263,X1265)
| ~ ssPv2(X1265)
| ~ ssPv1(X1264)
| ssPv3(X1264) ),
inference(factor,[status(thm)],[c160]) ).
cnf(c602,plain,
( ~ ssRr(X1268,X1269)
| ~ ssPv3(X1269)
| ~ ssRr(X1268,X1268)
| ~ ssPv2(skf1(X1269))
| ~ ssPv1(X1268)
| ssPv3(X1268) ),
inference(resolution,[status(thm)],[c462,clause1]) ).
cnf(c457,plain,
( ~ ssRr(X1248,X1249)
| ~ ssPv3(X1249)
| ~ ssRr(X1248,X1248)
| ~ ssRr(X1248,X1250)
| ~ ssPv2(X1250)
| ~ ssPv1(X1249)
| ssPv3(X1248) ),
inference(factor,[status(thm)],[c159]) ).
cnf(c594,plain,
( ~ ssRr(X1262,X1261)
| ~ ssPv3(X1261)
| ~ ssRr(X1262,X1262)
| ~ ssPv2(skf1(X1262))
| ~ ssPv1(X1261)
| ssPv3(X1262) ),
inference(resolution,[status(thm)],[c457,clause1]) ).
cnf(c191,plain,
( ~ ssRr(X1257,X1258)
| ~ ssPv3(X1258)
| ~ ssRr(X1256,X1257)
| ~ ssRr(X1259,X1260)
| ~ ssRr(X1256,X1259)
| ~ ssRr(X1256,X1256)
| ssPv4(X1260)
| ssPv2(X1256)
| ssPv3(X1256) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c592,plain,
( ~ ssRr(X1251,X1252)
| ~ ssPv3(X1252)
| ~ ssRr(X1251,X1251)
| ~ ssPv2(X1252)
| ~ ssPv1(X1252)
| ssPv3(X1251) ),
inference(factor,[status(thm)],[c457]) ).
cnf(c456,plain,
( ~ ssRr(X1236,X1235)
| ~ ssPv3(X1235)
| ~ ssRr(X1236,X1236)
| ~ ssRr(X1235,X1237)
| ~ ssPv2(X1237)
| ~ ssPv1(X1235)
| ssPv3(X1236) ),
inference(factor,[status(thm)],[c159]) ).
cnf(c586,plain,
( ~ ssRr(X1246,X1247)
| ~ ssPv3(X1247)
| ~ ssRr(X1246,X1246)
| ~ ssPv2(skf1(X1247))
| ~ ssPv1(X1247)
| ssPv3(X1246) ),
inference(resolution,[status(thm)],[c456,clause1]) ).
cnf(c354,plain,
( ~ ssRr(X900,X901)
| ~ ssPv1(X901)
| ~ ssRr(X899,X900)
| ~ ssRr(X900,X902)
| ssPv2(X902)
| ssPv3(X900)
| ssPv3(X899) ),
inference(factor,[status(thm)],[c132]) ).
cnf(c430,plain,
( ~ ssRr(X921,X920)
| ~ ssPv1(X920)
| ~ ssRr(X919,X921)
| ssPv2(skf1(X921))
| ssPv3(X921)
| ssPv3(X919) ),
inference(resolution,[status(thm)],[c354,clause1]) ).
cnf(c440,plain,
( ~ ssRr(skf1(X1217),X1218)
| ~ ssPv1(X1218)
| ssPv2(skf1(skf1(X1217)))
| ssPv3(skf1(X1217))
| ssPv3(X1217) ),
inference(resolution,[status(thm)],[c430,clause1]) ).
cnf(c152,plain,
( ~ ssRr(X912,X911)
| ~ ssPv4(X911)
| ~ ssRr(X914,X912)
| ~ ssRr(X914,X913)
| ~ ssRr(X914,X914)
| ~ ssPv1(X914)
| ssPv3(X913)
| ssPv2(X913) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c435,plain,
( ~ ssRr(X1201,X1203)
| ~ ssPv4(X1203)
| ~ ssRr(X1201,X1201)
| ~ ssRr(X1201,X1202)
| ~ ssPv1(X1201)
| ssPv3(X1202)
| ssPv2(X1202) ),
inference(factor,[status(thm)],[c152]) ).
cnf(c426,plain,
( ~ ssRr(X1196,X1197)
| ~ ssPv4(X1197)
| ~ ssRr(X1195,X1196)
| ~ ssRr(X1195,X1195)
| ~ ssPv1(X1195)
| ssPv3(X1195)
| ssPv2(X1196) ),
inference(factor,[status(thm)],[c151]) ).
cnf(c552,plain,
( ~ ssRr(X1171,X1173)
| ~ ssPv4(X1173)
| ~ ssRr(X1172,X1171)
| ~ ssPv1(X1172)
| ssPv3(X1173)
| ssPv2(X1171) ),
inference(factor,[status(thm)],[c425]) ).
cnf(c556,plain,
( ~ ssRr(skf1(X1184),X1183)
| ~ ssPv4(X1183)
| ~ ssPv1(X1184)
| ssPv3(X1183)
| ssPv2(skf1(X1184)) ),
inference(resolution,[status(thm)],[c552,clause1]) ).
cnf(c560,plain,
( ~ ssPv4(skf1(skf1(X1189)))
| ~ ssPv1(X1189)
| ssPv3(skf1(skf1(X1189)))
| ssPv2(skf1(X1189)) ),
inference(resolution,[status(thm)],[c556,clause1]) ).
cnf(c424,plain,
( ~ ssRr(X1128,X1127)
| ~ ssPv4(X1127)
| ~ ssRr(X1128,X1128)
| ~ ssRr(X1127,X1129)
| ~ ssPv1(X1128)
| ssPv3(X1129)
| ssPv2(X1128) ),
inference(factor,[status(thm)],[c151]) ).
cnf(c535,plain,
( ~ ssRr(X1164,X1165)
| ~ ssPv4(X1165)
| ~ ssRr(X1164,X1164)
| ~ ssPv1(X1164)
| ssPv3(skf1(X1165))
| ssPv2(X1164) ),
inference(resolution,[status(thm)],[c424,clause1]) ).
cnf(c538,plain,
( ~ ssRr(X1150,X1151)
| ~ ssPv4(X1151)
| ~ ssRr(X1152,X1150)
| ~ ssRr(X1152,X1152)
| ssPv4(X1152)
| ssPv1(X1152) ),
inference(factor,[status(thm)],[c178]) ).
cnf(c537,plain,
( ~ ssRr(X1139,X1138)
| ~ ssPv4(X1138)
| ~ ssRr(X1137,X1139)
| ~ ssRr(X1137,X1137)
| ssPv4(X1137)
| ssPv1(X1139) ),
inference(factor,[status(thm)],[c178]) ).
cnf(c542,plain,
( ~ ssRr(X1142,X1141)
| ~ ssPv4(X1141)
| ~ ssRr(X1142,X1142)
| ssPv4(X1142)
| ssPv1(X1142) ),
inference(factor,[status(thm)],[c537]) ).
cnf(c420,plain,
( ~ ssRr(X1111,X1110)
| ~ ssPv4(X1110)
| ~ ssRr(X1111,X1111)
| ~ ssRr(X1111,X1112)
| ~ ssPv1(X1111)
| ssPv3(X1112)
| ssPv2(X1110) ),
inference(factor,[status(thm)],[c150]) ).
cnf(c525,plain,
( ~ ssRr(X1125,X1124)
| ~ ssPv4(X1124)
| ~ ssRr(X1125,X1125)
| ~ ssPv1(X1125)
| ssPv3(skf1(X1125))
| ssPv2(X1124) ),
inference(resolution,[status(thm)],[c420,clause1]) ).
cnf(c523,plain,
( ~ ssRr(X1113,X1114)
| ~ ssPv4(X1114)
| ~ ssRr(X1113,X1113)
| ~ ssPv1(X1113)
| ssPv3(X1114)
| ssPv2(X1114) ),
inference(factor,[status(thm)],[c420]) ).
cnf(c419,plain,
( ~ ssRr(X1098,X1099)
| ~ ssPv4(X1099)
| ~ ssRr(X1098,X1098)
| ~ ssRr(X1099,X1097)
| ~ ssPv1(X1098)
| ssPv3(X1097)
| ssPv2(X1099) ),
inference(factor,[status(thm)],[c150]) ).
cnf(c516,plain,
( ~ ssRr(X1108,X1107)
| ~ ssPv4(X1107)
| ~ ssRr(X1108,X1108)
| ~ ssPv1(X1108)
| ssPv3(skf1(X1107))
| ssPv2(X1107) ),
inference(resolution,[status(thm)],[c419,clause1]) ).
cnf(c522,plain,
( ~ ssRr(X1109,X1109)
| ~ ssPv4(X1109)
| ~ ssPv1(X1109)
| ssPv3(skf1(X1109))
| ssPv2(X1109) ),
inference(factor,[status(thm)],[c516]) ).
cnf(c168,plain,
( ~ ssRr(X1027,X1030)
| ~ ssPv3(X1030)
| ~ ssRr(X1027,X1027)
| ~ ssRr(X1028,X1029)
| ~ ssRr(X1027,X1028)
| ~ ssPv1(X1027)
| ssPv2(X1029) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c491,plain,
( ~ ssRr(X1064,X1063)
| ~ ssPv3(X1063)
| ~ ssRr(X1064,X1064)
| ~ ssRr(skf1(X1064),X1062)
| ~ ssPv1(X1064)
| ssPv2(X1062) ),
inference(resolution,[status(thm)],[c168,clause1]) ).
cnf(c506,plain,
( ~ ssRr(X1066,X1065)
| ~ ssPv3(X1065)
| ~ ssRr(X1066,X1066)
| ~ ssPv1(X1066)
| ssPv2(skf1(skf1(X1066))) ),
inference(resolution,[status(thm)],[c491,clause1]) ).
cnf(c507,plain,
( ~ ssRr(X1072,X1072)
| ~ ssPv3(X1072)
| ~ ssPv1(X1072)
| ssPv2(skf1(skf1(X1072))) ),
inference(factor,[status(thm)],[c506]) ).
cnf(c489,plain,
( ~ ssRr(X1049,X1048)
| ~ ssPv3(X1048)
| ~ ssRr(X1049,X1049)
| ~ ssRr(X1049,X1047)
| ~ ssPv1(X1049)
| ssPv2(X1047) ),
inference(factor,[status(thm)],[c168]) ).
cnf(c503,plain,
( ~ ssRr(X1060,X1059)
| ~ ssPv3(X1059)
| ~ ssRr(X1060,X1060)
| ~ ssPv1(X1060)
| ssPv2(skf1(X1060)) ),
inference(resolution,[status(thm)],[c489,clause1]) ).
cnf(c501,plain,
( ~ ssRr(X1050,X1051)
| ~ ssPv3(X1051)
| ~ ssRr(X1050,X1050)
| ~ ssPv1(X1050)
| ssPv2(X1051) ),
inference(factor,[status(thm)],[c489]) ).
cnf(c488,plain,
( ~ ssRr(X1035,X1036)
| ~ ssPv3(X1036)
| ~ ssRr(X1035,X1035)
| ~ ssRr(X1036,X1034)
| ~ ssPv1(X1035)
| ssPv2(X1034) ),
inference(factor,[status(thm)],[c168]) ).
cnf(c495,plain,
( ~ ssRr(X1044,X1045)
| ~ ssPv3(X1045)
| ~ ssRr(X1044,X1044)
| ~ ssPv1(X1044)
| ssPv2(skf1(X1045)) ),
inference(resolution,[status(thm)],[c488,clause1]) ).
cnf(c500,plain,
( ~ ssRr(X1046,X1046)
| ~ ssPv3(X1046)
| ~ ssPv1(X1046)
| ssPv2(skf1(X1046)) ),
inference(factor,[status(thm)],[c495]) ).
cnf(c490,plain,
( ~ ssRr(X1031,X1032)
| ~ ssPv3(X1032)
| ~ ssRr(X1031,X1031)
| ~ ssPv1(X1031)
| ssPv2(X1031) ),
inference(factor,[status(thm)],[c168]) ).
cnf(c492,plain,
( ~ ssRr(X1033,X1033)
| ~ ssPv3(X1033)
| ~ ssPv1(X1033)
| ssPv2(X1033) ),
inference(factor,[status(thm)],[c490]) ).
cnf(c141,plain,
( ~ ssRr(X833,X831)
| ~ ssPv4(X831)
| ~ ssRr(X834,X833)
| ~ ssRr(X834,X832)
| ~ ssRr(X834,X834)
| ~ ssPv2(X834)
| ssPv4(X832)
| ssPv1(X832) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c399,plain,
( ~ ssRr(X1021,X1020)
| ~ ssPv4(X1020)
| ~ ssRr(X1021,X1021)
| ~ ssRr(X1021,X1022)
| ~ ssPv2(X1021)
| ssPv4(X1022)
| ssPv1(X1022) ),
inference(factor,[status(thm)],[c141]) ).
cnf(c325,plain,
( ~ ssRr(X812,X810)
| ~ ssRr(X811,X812)
| ~ ssRr(X812,X809)
| ~ ssPv4(X811)
| ssPv4(X810)
| ssPv1(X809)
| ssPv2(X812) ),
inference(factor,[status(thm)],[c121]) ).
cnf(c388,plain,
( ~ ssRr(X828,X826)
| ~ ssRr(X827,X828)
| ~ ssPv4(X827)
| ssPv4(X826)
| ssPv1(skf1(X828))
| ssPv2(X828) ),
inference(resolution,[status(thm)],[c325,clause1]) ).
cnf(c397,plain,
( ~ ssRr(skf1(X1018),X1017)
| ~ ssPv4(X1018)
| ssPv4(X1017)
| ssPv1(skf1(skf1(X1018)))
| ssPv2(skf1(X1018)) ),
inference(resolution,[status(thm)],[c388,clause1]) ).
cnf(c163,plain,
( ~ ssRr(X1014,X1013)
| ~ ssPv3(X1013)
| ~ ssRr(X1015,X1014)
| ~ ssRr(X1016,X1012)
| ~ ssPv2(X1012)
| ~ ssRr(X1015,X1016)
| ~ ssPv1(skf1(X1015))
| ssPv3(X1015) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c391,plain,
( ~ ssRr(X976,X975)
| ~ ssPv4(X975)
| ~ ssRr(X976,X976)
| ~ ssRr(X975,X974)
| ~ ssPv2(X976)
| ssPv4(X974)
| ssPv1(X976) ),
inference(factor,[status(thm)],[c140]) ).
cnf(c468,plain,
( ~ ssRr(X979,X980)
| ~ ssPv4(X980)
| ~ ssRr(X979,X979)
| ~ ssPv2(X979)
| ssPv4(skf1(X980))
| ssPv1(X979) ),
inference(resolution,[status(thm)],[c391,clause1]) ).
cnf(c382,plain,
( ~ ssRr(X952,X953)
| ~ ssPv4(X953)
| ~ ssRr(X952,X952)
| ~ ssRr(X952,X954)
| ~ ssPv2(X952)
| ssPv4(X954)
| ssPv1(X953) ),
inference(factor,[status(thm)],[c139]) ).
cnf(c455,plain,
( ~ ssRr(X967,X966)
| ~ ssPv4(X966)
| ~ ssRr(X967,X967)
| ~ ssPv2(X967)
| ssPv4(skf1(X967))
| ssPv1(X966) ),
inference(resolution,[status(thm)],[c382,clause1]) ).
cnf(c458,plain,
( ~ ssRr(X964,X963)
| ~ ssPv3(X963)
| ~ ssRr(X964,X964)
| ~ ssPv2(X964)
| ~ ssPv1(X963)
| ssPv3(X964) ),
inference(factor,[status(thm)],[c159]) ).
cnf(c381,plain,
( ~ ssRr(X939,X940)
| ~ ssPv4(X940)
| ~ ssRr(X939,X939)
| ~ ssRr(X940,X941)
| ~ ssPv2(X939)
| ssPv4(X941)
| ssPv1(X940) ),
inference(factor,[status(thm)],[c139]) ).
cnf(c447,plain,
( ~ ssRr(X949,X950)
| ~ ssPv4(X950)
| ~ ssRr(X949,X949)
| ~ ssPv2(X949)
| ssPv4(skf1(X950))
| ssPv1(X950) ),
inference(resolution,[status(thm)],[c381,clause1]) ).
cnf(c452,plain,
( ~ ssRr(X951,X951)
| ~ ssPv4(X951)
| ~ ssPv2(X951)
| ssPv4(skf1(X951))
| ssPv1(X951) ),
inference(factor,[status(thm)],[c447]) ).
cnf(c428,plain,
( ~ ssRr(X907,X906)
| ~ ssPv1(X906)
| ~ ssRr(X905,X907)
| ssPv2(X906)
| ssPv3(X907)
| ssPv3(X905) ),
inference(factor,[status(thm)],[c354]) ).
cnf(c432,plain,
( ~ ssRr(skf1(X910),X909)
| ~ ssPv1(X909)
| ssPv2(X909)
| ssPv3(skf1(X910))
| ssPv3(X910) ),
inference(resolution,[status(thm)],[c428,clause1]) ).
cnf(c433,plain,
( ~ ssPv1(skf1(skf1(X928)))
| ssPv2(skf1(skf1(X928)))
| ssPv3(skf1(X928))
| ssPv3(X928) ),
inference(resolution,[status(thm)],[c432,clause1]) ).
cnf(c434,plain,
( ~ ssRr(X915,X915)
| ~ ssPv4(X915)
| ~ ssRr(X915,X916)
| ~ ssPv1(X915)
| ssPv3(X916)
| ssPv2(X916) ),
inference(factor,[status(thm)],[c152]) ).
cnf(c438,plain,
( ~ ssRr(X918,X918)
| ~ ssPv4(X918)
| ~ ssPv1(X918)
| ssPv3(skf1(X918))
| ssPv2(skf1(X918)) ),
inference(resolution,[status(thm)],[c434,clause1]) ).
cnf(c421,plain,
( ~ ssRr(X890,X889)
| ~ ssPv4(X889)
| ~ ssRr(X890,X890)
| ~ ssPv1(X890)
| ssPv3(X890)
| ssPv2(X889) ),
inference(factor,[status(thm)],[c150]) ).
cnf(c349,plain,
( ~ ssRr(X879,X878)
| ~ ssPv1(X878)
| ~ ssRr(X879,X879)
| ~ ssRr(X879,X880)
| ssPv2(X880)
| ssPv3(X878)
| ssPv3(X879) ),
inference(factor,[status(thm)],[c131]) ).
cnf(c122,plain,
( ~ ssRr(X689,X688)
| ~ ssRr(X690,X689)
| ~ ssRr(X690,X691)
| ~ ssRr(X690,X690)
| ~ ssPv4(X690)
| ssPv4(X688)
| ssPv1(X691)
| ssPv2(X691) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c333,plain,
( ~ ssRr(X851,X850)
| ~ ssRr(X851,X851)
| ~ ssRr(X851,X852)
| ~ ssPv4(X851)
| ssPv4(X850)
| ssPv1(X852)
| ssPv2(X852) ),
inference(factor,[status(thm)],[c122]) ).
cnf(c326,plain,
( ~ ssRr(X839,X841)
| ~ ssRr(X840,X839)
| ~ ssRr(X840,X840)
| ~ ssPv4(X840)
| ssPv4(X841)
| ssPv1(X840)
| ssPv2(X839) ),
inference(factor,[status(thm)],[c121]) ).
cnf(c398,plain,
( ~ ssRr(X836,X836)
| ~ ssPv4(X836)
| ~ ssRr(X836,X835)
| ~ ssPv2(X836)
| ssPv4(X835)
| ssPv1(X835) ),
inference(factor,[status(thm)],[c141]) ).
cnf(c402,plain,
( ~ ssRr(X838,X838)
| ~ ssPv4(X838)
| ~ ssPv2(X838)
| ssPv4(skf1(X838))
| ssPv1(skf1(X838)) ),
inference(resolution,[status(thm)],[c398,clause1]) ).
cnf(c386,plain,
( ~ ssRr(X813,X814)
| ~ ssRr(X815,X813)
| ~ ssPv4(X815)
| ssPv4(X814)
| ssPv1(X814)
| ssPv2(X813) ),
inference(factor,[status(thm)],[c325]) ).
cnf(c390,plain,
( ~ ssRr(skf1(X825),X824)
| ~ ssPv4(X825)
| ssPv4(X824)
| ssPv1(X824)
| ssPv2(skf1(X825)) ),
inference(resolution,[status(thm)],[c386,clause1]) ).
cnf(c395,plain,
( ~ ssPv4(X830)
| ssPv4(skf1(skf1(X830)))
| ssPv1(skf1(skf1(X830)))
| ssPv2(skf1(X830)) ),
inference(resolution,[status(thm)],[c390,clause1]) ).
cnf(c324,plain,
( ~ ssRr(X796,X795)
| ~ ssRr(X796,X796)
| ~ ssRr(X795,X794)
| ~ ssPv4(X796)
| ssPv4(X795)
| ssPv1(X794)
| ssPv2(X796) ),
inference(factor,[status(thm)],[c121]) ).
cnf(c379,plain,
( ~ ssRr(X799,X800)
| ~ ssRr(X799,X799)
| ~ ssPv4(X799)
| ssPv4(X800)
| ssPv1(skf1(X800))
| ssPv2(X799) ),
inference(resolution,[status(thm)],[c324,clause1]) ).
cnf(c368,plain,
( ~ ssRr(X783,X782)
| ~ ssPv1(X782)
| ~ ssRr(X784,X783)
| ~ ssRr(X784,X784)
| ssPv2(X784)
| ssPv3(X784) ),
inference(factor,[status(thm)],[c134]) ).
cnf(c371,plain,
( ~ ssRr(X787,X786)
| ~ ssPv1(X786)
| ~ ssRr(X787,X787)
| ssPv2(X787)
| ssPv3(X787) ),
inference(factor,[status(thm)],[c368]) ).
cnf(c318,plain,
( ~ ssRr(X768,X767)
| ~ ssRr(X768,X768)
| ~ ssRr(X768,X766)
| ~ ssPv4(X768)
| ssPv4(X767)
| ssPv1(X766)
| ssPv2(X767) ),
inference(factor,[status(thm)],[c120]) ).
cnf(c363,plain,
( ~ ssRr(X774,X775)
| ~ ssRr(X774,X774)
| ~ ssPv4(X774)
| ssPv4(X775)
| ssPv1(skf1(X774))
| ssPv2(X775) ),
inference(resolution,[status(thm)],[c318,clause1]) ).
cnf(c361,plain,
( ~ ssRr(X770,X769)
| ~ ssRr(X770,X770)
| ~ ssPv4(X770)
| ssPv4(X769)
| ssPv1(X769)
| ssPv2(X769) ),
inference(factor,[status(thm)],[c318]) ).
cnf(c353,plain,
( ~ ssRr(X754,X755)
| ~ ssPv1(X755)
| ~ ssRr(X754,X754)
| ~ ssRr(X755,X756)
| ssPv2(X756)
| ssPv3(X754) ),
inference(factor,[status(thm)],[c132]) ).
cnf(c359,plain,
( ~ ssRr(X759,X760)
| ~ ssPv1(X760)
| ~ ssRr(X759,X759)
| ssPv2(skf1(X760))
| ssPv3(X759) ),
inference(resolution,[status(thm)],[c353,clause1]) ).
cnf(c317,plain,
( ~ ssRr(X737,X735)
| ~ ssRr(X737,X737)
| ~ ssRr(X735,X736)
| ~ ssPv4(X737)
| ssPv4(X735)
| ssPv1(X736)
| ssPv2(X735) ),
inference(factor,[status(thm)],[c120]) ).
cnf(c347,plain,
( ~ ssRr(X746,X747)
| ~ ssRr(X746,X746)
| ~ ssPv4(X746)
| ssPv4(X747)
| ssPv1(skf1(X747))
| ssPv2(X747) ),
inference(resolution,[status(thm)],[c317,clause1]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X233,X234)
| ~ ssRr(X231,X233)
| ~ ssRr(X231,X232)
| ~ ssPv4(X232)
| ~ ssRr(X231,X230)
| ~ ssPv3(X230)
| ~ ssPv3(X231)
| ssPv1(X234) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c115,plain,
( ~ ssRr(X629,X631)
| ~ ssRr(X630,X629)
| ~ ssRr(X630,X632)
| ~ ssPv4(X632)
| ~ ssPv3(X632)
| ~ ssPv3(X630)
| ssPv1(X631) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c313,plain,
( ~ ssRr(X732,X733)
| ~ ssRr(X734,X732)
| ~ ssPv4(skf1(X734))
| ~ ssPv3(skf1(X734))
| ~ ssPv3(X734)
| ssPv1(X733) ),
inference(resolution,[status(thm)],[c115,clause1]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X217,X218)
| ~ ssPv3(X218)
| ~ ssRr(X215,X217)
| ~ ssRr(X215,X216)
| ~ ssPv2(X216)
| ~ ssRr(X215,X214)
| ~ ssPv1(X214)
| ssPv2(X215) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c105,plain,
( ~ ssRr(X588,X589)
| ~ ssPv3(X589)
| ~ ssRr(X591,X588)
| ~ ssRr(X591,X590)
| ~ ssPv2(X590)
| ~ ssPv1(X590)
| ssPv2(X591) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c298,plain,
( ~ ssRr(X729,X730)
| ~ ssPv3(X730)
| ~ ssRr(X731,X729)
| ~ ssPv2(skf1(X731))
| ~ ssPv1(skf1(X731))
| ssPv2(X731) ),
inference(resolution,[status(thm)],[c105,clause1]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X202,X203)
| ~ ssPv1(X203)
| ~ ssRr(X200,X202)
| ~ ssRr(X200,X201)
| ~ ssPv2(X201)
| ~ ssRr(X200,X199)
| ssPv4(X199)
| ssPv1(X200) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c97,plain,
( ~ ssRr(X536,X539)
| ~ ssPv1(X539)
| ~ ssRr(X537,X536)
| ~ ssRr(X537,X538)
| ~ ssPv2(X538)
| ssPv4(X538)
| ssPv1(X537) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c278,plain,
( ~ ssRr(X725,X723)
| ~ ssPv1(X723)
| ~ ssRr(X724,X725)
| ~ ssPv2(skf1(X724))
| ssPv4(skf1(X724))
| ssPv1(X724) ),
inference(resolution,[status(thm)],[c97,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X182,X183)
| ~ ssPv3(X183)
| ~ ssRr(X180,X182)
| ~ ssRr(X181,X179)
| ~ ssPv1(X179)
| ~ ssRr(X180,X181)
| ssPv2(X180)
| ssPv4(X180) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(c94,plain,
( ~ ssRr(X510,X512)
| ~ ssPv3(X512)
| ~ ssRr(X513,X510)
| ~ ssRr(skf1(X513),X511)
| ~ ssPv1(X511)
| ssPv2(X513)
| ssPv4(X513) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(c264,plain,
( ~ ssRr(X715,X717)
| ~ ssPv3(X717)
| ~ ssRr(X716,X715)
| ~ ssPv1(skf1(skf1(X716)))
| ssPv2(X716)
| ssPv4(X716) ),
inference(resolution,[status(thm)],[c94,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X153,X154)
| ~ ssRr(X151,X153)
| ~ ssRr(X152,X150)
| ~ ssRr(X151,X152)
| ~ ssPv2(X151)
| ssPv4(X154)
| ssPv1(X150)
| ssPv4(X151) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c80,plain,
( ~ ssRr(X472,X470)
| ~ ssRr(X473,X472)
| ~ ssRr(skf1(X473),X471)
| ~ ssPv2(X473)
| ssPv4(X470)
| ssPv1(X471)
| ssPv4(X473) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(c247,plain,
( ~ ssRr(X701,X700)
| ~ ssRr(X699,X701)
| ~ ssPv2(X699)
| ssPv4(X700)
| ssPv1(skf1(skf1(X699)))
| ssPv4(X699) ),
inference(resolution,[status(thm)],[c80,clause1]) ).
cnf(c335,plain,
( ~ ssRr(X707,X707)
| ~ ssPv2(X707)
| ssPv4(X707)
| ssPv1(skf1(skf1(X707))) ),
inference(factor,[status(thm)],[c247]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X168,X169)
| ~ ssPv1(X169)
| ~ ssRr(X166,X168)
| ~ ssRr(X166,X167)
| ~ ssRr(X166,X165)
| ~ ssPv2(X166)
| ssPv2(X167)
| ssPv1(X165) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c87,plain,
( ~ ssRr(X458,X459)
| ~ ssPv1(X459)
| ~ ssRr(X457,X458)
| ~ ssRr(X457,X460)
| ~ ssPv2(X457)
| ssPv2(X460)
| ssPv1(X460) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c242,plain,
( ~ ssRr(X685,X686)
| ~ ssPv1(X686)
| ~ ssRr(X687,X685)
| ~ ssPv2(X687)
| ssPv2(skf1(X687))
| ssPv1(skf1(X687)) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(c330,plain,
( ~ ssRr(X692,X692)
| ~ ssPv1(X692)
| ~ ssPv2(X692)
| ssPv2(skf1(X692))
| ssPv1(skf1(X692)) ),
inference(factor,[status(thm)],[c242]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X139,X140)
| ~ ssPv4(X140)
| ~ ssRr(X137,X139)
| ~ ssRr(X138,X136)
| ~ ssRr(X137,X138)
| ssPv2(X136)
| ssPv1(X137)
| ssPv3(X137) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c72,plain,
( ~ ssRr(X453,X454)
| ~ ssPv4(X454)
| ~ ssRr(X456,X453)
| ~ ssRr(skf1(X456),X455)
| ssPv2(X455)
| ssPv1(X456)
| ssPv3(X456) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(c239,plain,
( ~ ssRr(X680,X681)
| ~ ssPv4(X681)
| ~ ssRr(X679,X680)
| ssPv2(skf1(skf1(X679)))
| ssPv1(X679)
| ssPv3(X679) ),
inference(resolution,[status(thm)],[c72,clause1]) ).
cnf(c328,plain,
( ~ ssRr(X682,X682)
| ~ ssPv4(X682)
| ssPv2(skf1(skf1(X682)))
| ssPv1(X682)
| ssPv3(X682) ),
inference(factor,[status(thm)],[c239]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X126,X127)
| ~ ssPv4(X127)
| ~ ssRr(X124,X126)
| ~ ssRr(X125,X123)
| ~ ssRr(X124,X125)
| ssPv3(X123)
| ssPv3(X124)
| ssPv4(X124) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c65,plain,
( ~ ssRr(X442,X440)
| ~ ssPv4(X440)
| ~ ssRr(X443,X442)
| ~ ssRr(skf1(X443),X441)
| ssPv3(X441)
| ssPv3(X443)
| ssPv4(X443) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(c235,plain,
( ~ ssRr(X667,X668)
| ~ ssPv4(X668)
| ~ ssRr(X666,X667)
| ssPv3(skf1(skf1(X666)))
| ssPv3(X666)
| ssPv4(X666) ),
inference(resolution,[status(thm)],[c65,clause1]) ).
cnf(c319,plain,
( ~ ssRr(X664,X663)
| ~ ssRr(X664,X664)
| ~ ssPv4(X664)
| ssPv4(X663)
| ssPv1(X664)
| ssPv2(X663) ),
inference(factor,[status(thm)],[c120]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X112,X113)
| ~ ssPv1(X113)
| ~ ssRr(X110,X112)
| ~ ssRr(X110,X111)
| ~ ssRr(X110,X109)
| ssPv3(X111)
| ssPv2(X109)
| ssPv3(X110) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c56,plain,
( ~ ssRr(X253,X252)
| ~ ssPv1(X252)
| ~ ssRr(X250,X253)
| ~ ssRr(X250,X251)
| ssPv3(X251)
| ssPv2(X251)
| ssPv3(X250) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c127,plain,
( ~ ssRr(X649,X648)
| ~ ssPv1(X648)
| ~ ssRr(X650,X649)
| ssPv3(skf1(X650))
| ssPv2(skf1(X650))
| ssPv3(X650) ),
inference(resolution,[status(thm)],[c56,clause1]) ).
cnf(c116,plain,
( ~ ssRr(X644,X645)
| ~ ssRr(X646,X644)
| ~ ssRr(X646,X647)
| ~ ssPv4(X647)
| ~ ssPv3(skf1(X646))
| ~ ssPv3(X646)
| ssPv1(X645) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c114,plain,
( ~ ssRr(X616,X618)
| ~ ssRr(X617,X616)
| ~ ssRr(X617,X619)
| ~ ssPv4(X619)
| ~ ssPv3(X616)
| ~ ssPv3(X617)
| ssPv1(X618) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c306,plain,
( ~ ssRr(X625,X624)
| ~ ssRr(X623,X625)
| ~ ssPv4(X625)
| ~ ssPv3(X625)
| ~ ssPv3(X623)
| ssPv1(X624) ),
inference(factor,[status(thm)],[c114]) ).
cnf(c310,plain,
( ~ ssRr(skf1(X642),X641)
| ~ ssPv4(skf1(X642))
| ~ ssPv3(skf1(X642))
| ~ ssPv3(X642)
| ssPv1(X641) ),
inference(resolution,[status(thm)],[c306,clause1]) ).
cnf(c314,plain,
( ~ ssPv4(skf1(X643))
| ~ ssPv3(skf1(X643))
| ~ ssPv3(X643)
| ssPv1(skf1(skf1(X643))) ),
inference(resolution,[status(thm)],[c310,clause1]) ).
cnf(c307,plain,
( ~ ssRr(X638,X639)
| ~ ssRr(X640,X638)
| ~ ssPv4(skf1(X640))
| ~ ssPv3(X638)
| ~ ssPv3(X640)
| ssPv1(X639) ),
inference(resolution,[status(thm)],[c114,clause1]) ).
cnf(c113,plain,
( ~ ssRr(X608,X607)
| ~ ssRr(X608,X608)
| ~ ssRr(X608,X609)
| ~ ssPv4(X609)
| ~ ssPv3(X607)
| ~ ssPv3(X608)
| ssPv1(X607) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c302,plain,
( ~ ssRr(X628,X627)
| ~ ssRr(X628,X628)
| ~ ssPv4(skf1(X628))
| ~ ssPv3(X627)
| ~ ssPv3(X628)
| ssPv1(X627) ),
inference(resolution,[status(thm)],[c113,clause1]) ).
cnf(c305,plain,
( ~ ssRr(X620,X621)
| ~ ssRr(X620,X620)
| ~ ssPv4(X621)
| ~ ssPv3(X620)
| ssPv1(X621) ),
inference(factor,[status(thm)],[c114]) ).
cnf(c301,plain,
( ~ ssRr(X614,X613)
| ~ ssRr(X614,X614)
| ~ ssPv4(X614)
| ~ ssPv3(X613)
| ~ ssPv3(X614)
| ssPv1(X613) ),
inference(factor,[status(thm)],[c113]) ).
cnf(c106,plain,
( ~ ssRr(X603,X604)
| ~ ssPv3(X604)
| ~ ssRr(X606,X603)
| ~ ssRr(X606,X605)
| ~ ssPv2(X605)
| ~ ssPv1(skf1(X606))
| ssPv2(X606) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c104,plain,
( ~ ssRr(X577,X576)
| ~ ssPv3(X576)
| ~ ssRr(X578,X577)
| ~ ssRr(X578,X575)
| ~ ssPv2(X575)
| ~ ssPv1(X577)
| ssPv2(X578) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c291,plain,
( ~ ssRr(X584,X582)
| ~ ssPv3(X582)
| ~ ssRr(X583,X584)
| ~ ssPv2(X584)
| ~ ssPv1(X584)
| ssPv2(X583) ),
inference(factor,[status(thm)],[c104]) ).
cnf(c295,plain,
( ~ ssRr(skf1(X601),X600)
| ~ ssPv3(X600)
| ~ ssPv2(skf1(X601))
| ~ ssPv1(skf1(X601))
| ssPv2(X601) ),
inference(resolution,[status(thm)],[c291,clause1]) ).
cnf(c299,plain,
( ~ ssPv3(skf1(skf1(X602)))
| ~ ssPv2(skf1(X602))
| ~ ssPv1(skf1(X602))
| ssPv2(X602) ),
inference(resolution,[status(thm)],[c295,clause1]) ).
cnf(c292,plain,
( ~ ssRr(X597,X598)
| ~ ssPv3(X598)
| ~ ssRr(X599,X597)
| ~ ssPv2(skf1(X599))
| ~ ssPv1(X597)
| ssPv2(X599) ),
inference(resolution,[status(thm)],[c104,clause1]) ).
cnf(c103,plain,
( ~ ssRr(X566,X565)
| ~ ssPv3(X565)
| ~ ssRr(X566,X566)
| ~ ssRr(X566,X564)
| ~ ssPv2(X564)
| ~ ssPv1(X565)
| ssPv2(X566) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c288,plain,
( ~ ssRr(X587,X586)
| ~ ssPv3(X586)
| ~ ssRr(X587,X587)
| ~ ssPv2(skf1(X587))
| ~ ssPv1(X586)
| ssPv2(X587) ),
inference(resolution,[status(thm)],[c103,clause1]) ).
cnf(c286,plain,
( ~ ssRr(X569,X568)
| ~ ssPv3(X568)
| ~ ssRr(X569,X569)
| ~ ssPv2(X568)
| ~ ssPv1(X568)
| ssPv2(X569) ),
inference(factor,[status(thm)],[c103]) ).
cnf(c98,plain,
( ~ ssRr(X551,X553)
| ~ ssPv1(X553)
| ~ ssRr(X554,X551)
| ~ ssRr(X554,X552)
| ~ ssPv2(X552)
| ssPv4(skf1(X554))
| ssPv1(X554) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c280,plain,
( ~ ssRr(X562,X563)
| ~ ssPv1(X563)
| ~ ssRr(X561,X562)
| ~ ssPv2(X562)
| ssPv4(skf1(X561))
| ssPv1(X561) ),
inference(factor,[status(thm)],[c98]) ).
cnf(c279,plain,
( ~ ssRr(X558,X559)
| ~ ssPv1(X559)
| ~ ssRr(X558,X558)
| ~ ssPv2(X559)
| ssPv4(skf1(X558))
| ssPv1(X558) ),
inference(factor,[status(thm)],[c98]) ).
cnf(c96,plain,
( ~ ssRr(X526,X523)
| ~ ssPv1(X523)
| ~ ssRr(X524,X526)
| ~ ssRr(X524,X525)
| ~ ssPv2(X525)
| ssPv4(X526)
| ssPv1(X524) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c270,plain,
( ~ ssRr(X534,X535)
| ~ ssPv1(X535)
| ~ ssRr(X533,X534)
| ~ ssPv2(X534)
| ssPv4(X534)
| ssPv1(X533) ),
inference(factor,[status(thm)],[c96]) ).
cnf(c275,plain,
( ~ ssRr(skf1(X556),X555)
| ~ ssPv1(X555)
| ~ ssPv2(skf1(X556))
| ssPv4(skf1(X556))
| ssPv1(X556) ),
inference(resolution,[status(thm)],[c270,clause1]) ).
cnf(c282,plain,
( ~ ssPv1(skf1(skf1(X557)))
| ~ ssPv2(skf1(X557))
| ssPv4(skf1(X557))
| ssPv1(X557) ),
inference(resolution,[status(thm)],[c275,clause1]) ).
cnf(c271,plain,
( ~ ssRr(X548,X549)
| ~ ssPv1(X549)
| ~ ssRr(X550,X548)
| ~ ssPv2(skf1(X550))
| ssPv4(X548)
| ssPv1(X550) ),
inference(resolution,[status(thm)],[c96,clause1]) ).
cnf(c95,plain,
( ~ ssRr(X517,X519)
| ~ ssPv1(X519)
| ~ ssRr(X517,X517)
| ~ ssRr(X517,X518)
| ~ ssPv2(X518)
| ssPv4(X519)
| ssPv1(X517) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c267,plain,
( ~ ssRr(X547,X546)
| ~ ssPv1(X546)
| ~ ssRr(X547,X547)
| ~ ssPv2(skf1(X547))
| ssPv4(X546)
| ssPv1(X547) ),
inference(resolution,[status(thm)],[c95,clause1]) ).
cnf(c269,plain,
( ~ ssRr(X531,X530)
| ~ ssPv1(X530)
| ~ ssRr(X531,X531)
| ~ ssPv2(X530)
| ssPv4(X531)
| ssPv1(X531) ),
inference(factor,[status(thm)],[c96]) ).
cnf(c266,plain,
( ~ ssRr(X528,X527)
| ~ ssPv1(X527)
| ~ ssRr(X528,X528)
| ~ ssPv2(X528)
| ssPv4(X527)
| ssPv1(X528) ),
inference(factor,[status(thm)],[c95]) ).
cnf(c265,plain,
( ~ ssRr(X520,X521)
| ~ ssPv1(X521)
| ~ ssRr(X520,X520)
| ~ ssPv2(X521)
| ssPv4(X521)
| ssPv1(X520) ),
inference(factor,[status(thm)],[c95]) ).
cnf(c88,plain,
( ~ ssRr(X486,X487)
| ~ ssPv1(X487)
| ~ ssRr(X488,X486)
| ~ ssRr(X488,X485)
| ~ ssPv2(X488)
| ssPv2(X485)
| ssPv1(skf1(X488)) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(c254,plain,
( ~ ssRr(X507,X509)
| ~ ssPv1(X509)
| ~ ssRr(X508,X507)
| ~ ssPv2(X508)
| ssPv2(X507)
| ssPv1(skf1(X508)) ),
inference(factor,[status(thm)],[c88]) ).
cnf(c253,plain,
( ~ ssRr(X505,X504)
| ~ ssPv1(X504)
| ~ ssRr(X505,X505)
| ~ ssPv2(X505)
| ssPv2(X504)
| ssPv1(skf1(X505)) ),
inference(factor,[status(thm)],[c88]) ).
cnf(c93,plain,
( ~ ssRr(X498,X499)
| ~ ssPv3(X499)
| ~ ssRr(X500,X498)
| ~ ssRr(X500,X500)
| ~ ssPv1(X500)
| ssPv2(X500)
| ssPv4(X500) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c92,plain,
( ~ ssRr(X480,X479)
| ~ ssPv3(X479)
| ~ ssRr(X477,X480)
| ~ ssRr(X480,X478)
| ~ ssPv1(X478)
| ssPv2(X477)
| ssPv4(X477) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c250,plain,
( ~ ssRr(X497,X495)
| ~ ssPv3(X495)
| ~ ssRr(X496,X497)
| ~ ssPv1(skf1(X497))
| ssPv2(X496)
| ssPv4(X496) ),
inference(resolution,[status(thm)],[c92,clause1]) ).
cnf(c248,plain,
( ~ ssRr(X483,X482)
| ~ ssPv3(X482)
| ~ ssRr(X481,X483)
| ~ ssPv1(X482)
| ssPv2(X481)
| ssPv4(X481) ),
inference(factor,[status(thm)],[c92]) ).
cnf(c252,plain,
( ~ ssRr(skf1(X489),X490)
| ~ ssPv3(X490)
| ~ ssPv1(X490)
| ssPv2(X489)
| ssPv4(X489) ),
inference(resolution,[status(thm)],[c248,clause1]) ).
cnf(c256,plain,
( ~ ssPv3(skf1(skf1(X494)))
| ~ ssPv1(skf1(skf1(X494)))
| ssPv2(X494)
| ssPv4(X494) ),
inference(resolution,[status(thm)],[c252,clause1]) ).
cnf(c91,plain,
( ~ ssRr(X468,X466)
| ~ ssPv3(X466)
| ~ ssRr(X468,X468)
| ~ ssRr(X466,X467)
| ~ ssPv1(X467)
| ssPv2(X468)
| ssPv4(X468) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c245,plain,
( ~ ssRr(X475,X476)
| ~ ssPv3(X476)
| ~ ssRr(X475,X475)
| ~ ssPv1(skf1(X476))
| ssPv2(X475)
| ssPv4(X475) ),
inference(resolution,[status(thm)],[c91,clause1]) ).
cnf(c57,plain,
( ~ ssRr(X430,X429)
| ~ ssPv1(X429)
| ~ ssRr(X427,X430)
| ~ ssRr(X427,X428)
| ssPv3(X428)
| ssPv2(skf1(X427))
| ssPv3(X427) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c228,plain,
( ~ ssRr(X447,X446)
| ~ ssPv1(X446)
| ~ ssRr(X445,X447)
| ssPv3(X447)
| ssPv2(skf1(X445))
| ssPv3(X445) ),
inference(factor,[status(thm)],[c57]) ).
cnf(c227,plain,
( ~ ssRr(X438,X439)
| ~ ssPv1(X439)
| ~ ssRr(X438,X438)
| ssPv3(X439)
| ssPv2(skf1(X438))
| ssPv3(X438) ),
inference(factor,[status(thm)],[c57]) ).
cnf(c233,plain,
( ~ ssRr(X444,X444)
| ~ ssPv1(X444)
| ssPv3(X444)
| ssPv2(skf1(X444)) ),
inference(factor,[status(thm)],[c227]) ).
cnf(c86,plain,
( ~ ssRr(X419,X418)
| ~ ssPv1(X418)
| ~ ssRr(X416,X419)
| ~ ssRr(X416,X417)
| ~ ssPv2(X416)
| ssPv2(X417)
| ssPv1(X419) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c222,plain,
( ~ ssRr(X424,X425)
| ~ ssPv1(X425)
| ~ ssRr(X423,X424)
| ~ ssPv2(X423)
| ssPv2(X424)
| ssPv1(X424) ),
inference(factor,[status(thm)],[c86]) ).
cnf(c226,plain,
( ~ ssRr(skf1(X435),X436)
| ~ ssPv1(X436)
| ~ ssPv2(X435)
| ssPv2(skf1(X435))
| ssPv1(skf1(X435)) ),
inference(resolution,[status(thm)],[c222,clause1]) ).
cnf(c232,plain,
( ~ ssPv1(skf1(skf1(X437)))
| ~ ssPv2(X437)
| ssPv2(skf1(X437))
| ssPv1(skf1(X437)) ),
inference(resolution,[status(thm)],[c226,clause1]) ).
cnf(c223,plain,
( ~ ssRr(X431,X433)
| ~ ssPv1(X433)
| ~ ssRr(X432,X431)
| ~ ssPv2(X432)
| ssPv2(skf1(X432))
| ssPv1(X431) ),
inference(resolution,[status(thm)],[c86,clause1]) ).
cnf(c221,plain,
( ~ ssRr(X420,X421)
| ~ ssPv1(X421)
| ~ ssRr(X420,X420)
| ~ ssPv2(X420)
| ssPv2(X421)
| ssPv1(X420) ),
inference(factor,[status(thm)],[c86]) ).
cnf(c78,plain,
( ~ ssRr(X372,X370)
| ~ ssRr(X369,X372)
| ~ ssRr(X372,X371)
| ~ ssPv2(X369)
| ssPv4(X370)
| ssPv1(X371)
| ssPv4(X369) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c196,plain,
( ~ ssRr(X391,X390)
| ~ ssRr(X389,X391)
| ~ ssPv2(X389)
| ssPv4(X390)
| ssPv1(skf1(X391))
| ssPv4(X389) ),
inference(resolution,[status(thm)],[c78,clause1]) ).
cnf(c207,plain,
( ~ ssRr(skf1(X401),X400)
| ~ ssPv2(X401)
| ssPv4(X400)
| ssPv1(skf1(skf1(X401)))
| ssPv4(X401) ),
inference(resolution,[status(thm)],[c196,clause1]) ).
cnf(c194,plain,
( ~ ssRr(X374,X373)
| ~ ssRr(X375,X374)
| ~ ssPv2(X375)
| ssPv4(X373)
| ssPv1(X373)
| ssPv4(X375) ),
inference(factor,[status(thm)],[c78]) ).
cnf(c198,plain,
( ~ ssRr(skf1(X385),X384)
| ~ ssPv2(X385)
| ssPv4(X384)
| ssPv1(X384)
| ssPv4(X385) ),
inference(resolution,[status(thm)],[c194,clause1]) ).
cnf(c205,plain,
( ~ ssPv2(X388)
| ssPv4(skf1(skf1(X388)))
| ssPv1(skf1(skf1(X388)))
| ssPv4(X388) ),
inference(resolution,[status(thm)],[c198,clause1]) ).
cnf(c77,plain,
( ~ ssRr(X354,X356)
| ~ ssRr(X354,X354)
| ~ ssRr(X356,X355)
| ~ ssPv2(X354)
| ssPv4(X356)
| ssPv1(X355)
| ssPv4(X354) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c186,plain,
( ~ ssRr(X366,X367)
| ~ ssRr(X366,X366)
| ~ ssPv2(X366)
| ssPv4(X367)
| ssPv1(skf1(X367))
| ssPv4(X366) ),
inference(resolution,[status(thm)],[c77,clause1]) ).
cnf(c193,plain,
( ~ ssRr(X368,X368)
| ~ ssPv2(X368)
| ssPv4(X368)
| ssPv1(skf1(X368)) ),
inference(factor,[status(thm)],[c186]) ).
cnf(c184,plain,
( ~ ssRr(X357,X357)
| ~ ssPv2(X357)
| ssPv4(X357)
| ssPv1(X357) ),
inference(factor,[status(thm)],[c77]) ).
cnf(c71,plain,
( ~ ssRr(X348,X349)
| ~ ssPv4(X349)
| ~ ssRr(X350,X348)
| ~ ssRr(X350,X350)
| ssPv2(X350)
| ssPv1(X350)
| ssPv3(X350) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c70,plain,
( ~ ssRr(X311,X309)
| ~ ssPv4(X309)
| ~ ssRr(X310,X311)
| ~ ssRr(X311,X308)
| ssPv2(X308)
| ssPv1(X310)
| ssPv3(X310) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c158,plain,
( ~ ssRr(X335,X336)
| ~ ssPv4(X336)
| ~ ssRr(X334,X335)
| ssPv2(skf1(X335))
| ssPv1(X334)
| ssPv3(X334) ),
inference(resolution,[status(thm)],[c70,clause1]) ).
cnf(c174,plain,
( ~ ssRr(skf1(X339),X338)
| ~ ssPv4(X338)
| ssPv2(skf1(skf1(X339)))
| ssPv1(X339)
| ssPv3(X339) ),
inference(resolution,[status(thm)],[c158,clause1]) ).
cnf(c156,plain,
( ~ ssRr(X319,X318)
| ~ ssPv4(X318)
| ~ ssRr(X320,X319)
| ssPv2(X318)
| ssPv1(X320)
| ssPv3(X320) ),
inference(factor,[status(thm)],[c70]) ).
cnf(c165,plain,
( ~ ssRr(skf1(X323),X322)
| ~ ssPv4(X322)
| ssPv2(X322)
| ssPv1(X323)
| ssPv3(X323) ),
inference(resolution,[status(thm)],[c156,clause1]) ).
cnf(c166,plain,
( ~ ssPv4(skf1(skf1(X333)))
| ssPv2(skf1(skf1(X333)))
| ssPv1(X333)
| ssPv3(X333) ),
inference(resolution,[status(thm)],[c165,clause1]) ).
cnf(c157,plain,
( ~ ssRr(X324,X325)
| ~ ssPv4(X325)
| ~ ssRr(X324,X324)
| ssPv2(X324)
| ssPv1(X324)
| ssPv3(X324) ),
inference(factor,[status(thm)],[c70]) ).
cnf(c69,plain,
( ~ ssRr(X295,X296)
| ~ ssPv4(X296)
| ~ ssRr(X295,X295)
| ~ ssRr(X296,X294)
| ssPv2(X294)
| ssPv1(X295)
| ssPv3(X295) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c149,plain,
( ~ ssRr(X305,X306)
| ~ ssPv4(X306)
| ~ ssRr(X305,X305)
| ssPv2(skf1(X306))
| ssPv1(X305)
| ssPv3(X305) ),
inference(resolution,[status(thm)],[c69,clause1]) ).
cnf(c155,plain,
( ~ ssRr(X307,X307)
| ~ ssPv4(X307)
| ssPv2(skf1(X307))
| ssPv1(X307)
| ssPv3(X307) ),
inference(factor,[status(thm)],[c149]) ).
cnf(c63,plain,
( ~ ssRr(X265,X263)
| ~ ssPv4(X263)
| ~ ssRr(X262,X265)
| ~ ssRr(X265,X264)
| ssPv3(X264)
| ssPv3(X262)
| ssPv4(X262) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c130,plain,
( ~ ssRr(X289,X288)
| ~ ssPv4(X288)
| ~ ssRr(X287,X289)
| ssPv3(skf1(X289))
| ssPv3(X287)
| ssPv4(X287) ),
inference(resolution,[status(thm)],[c63,clause1]) ).
cnf(c145,plain,
( ~ ssRr(skf1(X292),X291)
| ~ ssPv4(X291)
| ssPv3(skf1(skf1(X292)))
| ssPv3(X292)
| ssPv4(X292) ),
inference(resolution,[status(thm)],[c130,clause1]) ).
cnf(c128,plain,
( ~ ssRr(X275,X274)
| ~ ssPv4(X274)
| ~ ssRr(X276,X275)
| ssPv3(X274)
| ssPv3(X276)
| ssPv4(X276) ),
inference(factor,[status(thm)],[c63]) ).
cnf(c137,plain,
( ~ ssRr(skf1(X278),X279)
| ~ ssPv4(X279)
| ssPv3(X279)
| ssPv3(X278)
| ssPv4(X278) ),
inference(resolution,[status(thm)],[c128,clause1]) ).
cnf(c138,plain,
( ~ ssPv4(skf1(skf1(X280)))
| ssPv3(skf1(skf1(X280)))
| ssPv3(X280)
| ssPv4(X280) ),
inference(resolution,[status(thm)],[c137,clause1]) ).
cnf(c55,plain,
( ~ ssRr(X220,X222)
| ~ ssPv1(X222)
| ~ ssRr(X219,X220)
| ~ ssRr(X219,X221)
| ssPv3(X221)
| ssPv2(X220)
| ssPv3(X219) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c108,plain,
( ~ ssRr(X226,X227)
| ~ ssPv1(X227)
| ~ ssRr(X228,X226)
| ssPv3(X226)
| ssPv2(X226)
| ssPv3(X228) ),
inference(factor,[status(thm)],[c55]) ).
cnf(c112,plain,
( ~ ssRr(skf1(X240),X239)
| ~ ssPv1(X239)
| ssPv3(skf1(X240))
| ssPv2(skf1(X240))
| ssPv3(X240) ),
inference(resolution,[status(thm)],[c108,clause1]) ).
cnf(c119,plain,
( ~ ssPv1(skf1(skf1(X241)))
| ssPv3(skf1(X241))
| ssPv2(skf1(X241))
| ssPv3(X241) ),
inference(resolution,[status(thm)],[c112,clause1]) ).
cnf(c109,plain,
( ~ ssRr(X236,X235)
| ~ ssPv1(X235)
| ~ ssRr(X237,X236)
| ssPv3(skf1(X237))
| ssPv2(X236)
| ssPv3(X237) ),
inference(resolution,[status(thm)],[c55,clause1]) ).
cnf(c54,plain,
( ~ ssRr(X204,X205)
| ~ ssPv1(X205)
| ~ ssRr(X204,X204)
| ~ ssRr(X204,X206)
| ssPv3(X206)
| ssPv2(X205)
| ssPv3(X204) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c100,plain,
( ~ ssRr(X207,X208)
| ~ ssPv1(X208)
| ~ ssRr(X207,X207)
| ssPv3(X207)
| ssPv2(X208) ),
inference(factor,[status(thm)],[c54]) ).
cnf(c102,plain,
( ~ ssRr(X209,X209)
| ~ ssPv1(X209)
| ssPv3(X209)
| ssPv2(X209) ),
inference(factor,[status(thm)],[c100]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X100,X101)
| ~ ssPv1(X101)
| ~ ssRr(X99,X100)
| ~ ssRr(X99,X98)
| ~ ssPv4(X98)
| ~ ssPv2(X99)
| ~ ssPv3(X99) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c51,plain,
( ~ ssRr(X197,X196)
| ~ ssPv1(X196)
| ~ ssRr(X198,X197)
| ~ ssPv4(skf1(X198))
| ~ ssPv2(X198)
| ~ ssPv3(X198) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X87,X88)
| ~ ssPv3(X88)
| ~ ssRr(X86,X87)
| ~ ssRr(X86,X85)
| ~ ssPv1(X85)
| ~ ssPv1(X86)
| ssPv3(X86) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c44,plain,
( ~ ssRr(X193,X194)
| ~ ssPv3(X194)
| ~ ssRr(X195,X193)
| ~ ssPv1(skf1(X195))
| ~ ssPv1(X195)
| ssPv3(X195) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X75,X76)
| ~ ssPv1(X76)
| ~ ssRr(X74,X75)
| ~ ssRr(X74,X73)
| ~ ssPv4(X73)
| ~ ssPv2(X74)
| ssPv3(X74) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c38,plain,
( ~ ssRr(X190,X192)
| ~ ssPv1(X192)
| ~ ssRr(X191,X190)
| ~ ssPv4(skf1(X191))
| ~ ssPv2(X191)
| ssPv3(X191) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X62,X63)
| ~ ssRr(X61,X62)
| ~ ssRr(X61,X60)
| ~ ssPv4(X60)
| ~ ssPv3(X61)
| ~ ssPv4(X61)
| ssPv3(X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c31,plain,
( ~ ssRr(X187,X188)
| ~ ssRr(X189,X187)
| ~ ssPv4(skf1(X189))
| ~ ssPv3(X189)
| ~ ssPv4(X189)
| ssPv3(X188) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X50,X51)
| ~ ssPv2(X51)
| ~ ssRr(X49,X50)
| ~ ssRr(X49,X48)
| ~ ssPv3(X48)
| ~ ssPv4(X49)
| ssPv2(X49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c25,plain,
( ~ ssRr(X185,X184)
| ~ ssPv2(X184)
| ~ ssRr(X186,X185)
| ~ ssPv3(skf1(X186))
| ~ ssPv4(X186)
| ssPv2(X186) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X37,X38)
| ~ ssPv3(X38)
| ~ ssRr(X36,X37)
| ~ ssRr(X36,X35)
| ~ ssPv4(X36)
| ssPv1(X35)
| ssPv2(X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c18,plain,
( ~ ssRr(X174,X173)
| ~ ssPv3(X173)
| ~ ssRr(X175,X174)
| ~ ssPv4(X175)
| ssPv1(skf1(X175))
| ssPv2(X175) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(c89,plain,
( ~ ssRr(X176,X176)
| ~ ssPv3(X176)
| ~ ssPv4(X176)
| ssPv1(skf1(X176))
| ssPv2(X176) ),
inference(factor,[status(thm)],[c18]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X25,X26)
| ~ ssPv4(X26)
| ~ ssRr(X24,X25)
| ~ ssRr(X24,X23)
| ssPv2(X23)
| ssPv1(X24)
| ssPv2(X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c12,plain,
( ~ ssRr(X163,X162)
| ~ ssPv4(X162)
| ~ ssRr(X164,X163)
| ssPv2(skf1(X164))
| ssPv1(X164)
| ssPv2(X164) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X19,X20)
| ~ ssRr(X18,X19)
| ~ ssRr(X18,X17)
| ~ ssPv3(X18)
| ssPv4(X20)
| ssPv3(X17)
| ssPv1(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c8,plain,
( ~ ssRr(X156,X157)
| ~ ssRr(X158,X156)
| ~ ssPv3(X158)
| ssPv4(X157)
| ssPv3(skf1(X158))
| ssPv1(X158) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(c81,plain,
( ~ ssRr(X159,X159)
| ~ ssPv3(X159)
| ssPv4(X159)
| ssPv3(skf1(X159))
| ssPv1(X159) ),
inference(factor,[status(thm)],[c8]) ).
cnf(c64,plain,
( ~ ssRr(X146,X145)
| ~ ssPv4(X145)
| ~ ssRr(X144,X146)
| ~ ssRr(X144,X144)
| ssPv3(X144)
| ssPv4(X144) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c75,plain,
( ~ ssRr(X148,X149)
| ~ ssPv4(X149)
| ~ ssRr(X148,X148)
| ssPv3(X148)
| ssPv4(X148) ),
inference(factor,[status(thm)],[c64]) ).
cnf(c50,plain,
( ~ ssRr(X129,X130)
| ~ ssPv1(X130)
| ~ ssRr(X131,X129)
| ~ ssPv4(X129)
| ~ ssPv2(X131)
| ~ ssPv3(X131) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c67,plain,
( ~ ssRr(skf1(X142),X141)
| ~ ssPv1(X141)
| ~ ssPv4(skf1(X142))
| ~ ssPv2(X142)
| ~ ssPv3(X142) ),
inference(resolution,[status(thm)],[c50,clause1]) ).
cnf(c73,plain,
( ~ ssPv1(skf1(skf1(X143)))
| ~ ssPv4(skf1(X143))
| ~ ssPv2(X143)
| ~ ssPv3(X143) ),
inference(resolution,[status(thm)],[c67,clause1]) ).
cnf(c43,plain,
( ~ ssRr(X114,X115)
| ~ ssPv3(X115)
| ~ ssRr(X116,X114)
| ~ ssPv1(X114)
| ~ ssPv1(X116)
| ssPv3(X116) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c59,plain,
( ~ ssRr(skf1(X134),X133)
| ~ ssPv3(X133)
| ~ ssPv1(skf1(X134))
| ~ ssPv1(X134)
| ssPv3(X134) ),
inference(resolution,[status(thm)],[c43,clause1]) ).
cnf(c68,plain,
( ~ ssPv3(skf1(skf1(X135)))
| ~ ssPv1(skf1(X135))
| ~ ssPv1(X135)
| ssPv3(X135) ),
inference(resolution,[status(thm)],[c59,clause1]) ).
cnf(c49,plain,
( ~ ssRr(X122,X121)
| ~ ssPv1(X121)
| ~ ssRr(X122,X122)
| ~ ssPv4(X121)
| ~ ssPv2(X122)
| ~ ssPv3(X122) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c61,plain,
( ~ ssRr(X128,X128)
| ~ ssPv1(X128)
| ~ ssPv4(X128)
| ~ ssPv2(X128)
| ~ ssPv3(X128) ),
inference(factor,[status(thm)],[c49]) ).
cnf(c37,plain,
( ~ ssRr(X95,X97)
| ~ ssPv1(X97)
| ~ ssRr(X96,X95)
| ~ ssPv4(X95)
| ~ ssPv2(X96)
| ssPv3(X96) ),
inference(factor,[status(thm)],[clause9]) ).
cnf(c48,plain,
( ~ ssRr(skf1(X119),X118)
| ~ ssPv1(X118)
| ~ ssPv4(skf1(X119))
| ~ ssPv2(X119)
| ssPv3(X119) ),
inference(resolution,[status(thm)],[c37,clause1]) ).
cnf(c60,plain,
( ~ ssPv1(skf1(skf1(X120)))
| ~ ssPv4(skf1(X120))
| ~ ssPv2(X120)
| ssPv3(X120) ),
inference(resolution,[status(thm)],[c48,clause1]) ).
cnf(c42,plain,
( ~ ssRr(X107,X106)
| ~ ssPv3(X106)
| ~ ssRr(X107,X107)
| ~ ssPv1(X106)
| ~ ssPv1(X107)
| ssPv3(X107) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c30,plain,
( ~ ssRr(X81,X82)
| ~ ssRr(X83,X81)
| ~ ssPv4(X81)
| ~ ssPv3(X83)
| ~ ssPv4(X83)
| ssPv3(X82) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(c41,plain,
( ~ ssRr(skf1(X104),X103)
| ~ ssPv4(skf1(X104))
| ~ ssPv3(X104)
| ~ ssPv4(X104)
| ssPv3(X103) ),
inference(resolution,[status(thm)],[c30,clause1]) ).
cnf(c52,plain,
( ~ ssPv4(skf1(X105))
| ~ ssPv3(X105)
| ~ ssPv4(X105)
| ssPv3(skf1(skf1(X105))) ),
inference(resolution,[status(thm)],[c41,clause1]) ).
cnf(c36,plain,
( ~ ssRr(X93,X92)
| ~ ssPv1(X92)
| ~ ssRr(X93,X93)
| ~ ssPv4(X92)
| ~ ssPv2(X93)
| ssPv3(X93) ),
inference(factor,[status(thm)],[clause9]) ).
cnf(c24,plain,
( ~ ssRr(X69,X67)
| ~ ssPv2(X67)
| ~ ssRr(X68,X69)
| ~ ssPv3(X69)
| ~ ssPv4(X68)
| ssPv2(X68) ),
inference(factor,[status(thm)],[clause7]) ).
cnf(c34,plain,
( ~ ssRr(skf1(X90),X89)
| ~ ssPv2(X89)
| ~ ssPv3(skf1(X90))
| ~ ssPv4(X90)
| ssPv2(X90) ),
inference(resolution,[status(thm)],[c24,clause1]) ).
cnf(c45,plain,
( ~ ssPv2(skf1(skf1(X91)))
| ~ ssPv3(skf1(X91))
| ~ ssPv4(X91)
| ssPv2(X91) ),
inference(resolution,[status(thm)],[c34,clause1]) ).
cnf(c29,plain,
( ~ ssRr(X79,X78)
| ~ ssRr(X79,X79)
| ~ ssPv4(X78)
| ~ ssPv3(X79)
| ~ ssPv4(X79)
| ssPv3(X78) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(c17,plain,
( ~ ssRr(X54,X53)
| ~ ssPv3(X53)
| ~ ssRr(X55,X54)
| ~ ssPv4(X55)
| ssPv1(X54)
| ssPv2(X55) ),
inference(factor,[status(thm)],[clause6]) ).
cnf(c27,plain,
( ~ ssRr(skf1(X72),X71)
| ~ ssPv3(X71)
| ~ ssPv4(X72)
| ssPv1(skf1(X72))
| ssPv2(X72) ),
inference(resolution,[status(thm)],[c17,clause1]) ).
cnf(c35,plain,
( ~ ssPv3(skf1(skf1(X77)))
| ~ ssPv4(X77)
| ssPv1(skf1(X77))
| ssPv2(X77) ),
inference(resolution,[status(thm)],[c27,clause1]) ).
cnf(c23,plain,
( ~ ssRr(X64,X65)
| ~ ssPv2(X65)
| ~ ssRr(X64,X64)
| ~ ssPv3(X65)
| ~ ssPv4(X64)
| ssPv2(X64) ),
inference(factor,[status(thm)],[clause7]) ).
cnf(c11,plain,
( ~ ssRr(X39,X41)
| ~ ssPv4(X41)
| ~ ssRr(X40,X39)
| ssPv2(X39)
| ssPv1(X40)
| ssPv2(X40) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(c20,plain,
( ~ ssRr(skf1(X58),X57)
| ~ ssPv4(X57)
| ssPv2(skf1(X58))
| ssPv1(X58)
| ssPv2(X58) ),
inference(resolution,[status(thm)],[c11,clause1]) ).
cnf(c28,plain,
( ~ ssPv4(skf1(skf1(X59)))
| ssPv2(skf1(X59))
| ssPv1(X59)
| ssPv2(X59) ),
inference(resolution,[status(thm)],[c20,clause1]) ).
cnf(c16,plain,
( ~ ssRr(X47,X46)
| ~ ssPv3(X46)
| ~ ssRr(X47,X47)
| ~ ssPv4(X47)
| ssPv1(X46)
| ssPv2(X47) ),
inference(factor,[status(thm)],[clause6]) ).
cnf(c7,plain,
( ~ ssRr(X30,X29)
| ~ ssRr(X28,X30)
| ~ ssPv3(X28)
| ssPv4(X29)
| ssPv3(X30)
| ssPv1(X28) ),
inference(factor,[status(thm)],[clause4]) ).
cnf(c14,plain,
( ~ ssRr(skf1(X44),X43)
| ~ ssPv3(X44)
| ssPv4(X43)
| ssPv3(skf1(X44))
| ssPv1(X44) ),
inference(resolution,[status(thm)],[c7,clause1]) ).
cnf(c21,plain,
( ~ ssPv3(X45)
| ssPv4(skf1(skf1(X45)))
| ssPv3(skf1(X45))
| ssPv1(X45) ),
inference(resolution,[status(thm)],[c14,clause1]) ).
cnf(c10,plain,
( ~ ssRr(X33,X32)
| ~ ssPv4(X32)
| ~ ssRr(X33,X33)
| ssPv2(X32)
| ssPv1(X33)
| ssPv2(X33) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(c15,plain,
( ~ ssRr(X34,X34)
| ~ ssPv4(X34)
| ssPv2(X34)
| ssPv1(X34) ),
inference(factor,[status(thm)],[c10]) ).
cnf(c6,plain,
( ~ ssRr(X21,X22)
| ~ ssRr(X21,X21)
| ~ ssPv3(X21)
| ssPv4(X22)
| ssPv3(X22)
| ssPv1(X21) ),
inference(factor,[status(thm)],[clause4]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X11,X12)
| ~ ssPv4(X12)
| ~ ssRr(X10,X11)
| ~ ssPv3(X10)
| ~ ssPv4(X10)
| ssPv1(X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c4,plain,
( ~ ssRr(skf1(X15),X14)
| ~ ssPv4(X14)
| ~ ssPv3(X15)
| ~ ssPv4(X15)
| ssPv1(X15) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(c5,plain,
( ~ ssPv4(skf1(skf1(X16)))
| ~ ssPv3(X16)
| ~ ssPv4(X16)
| ssPv1(X16) ),
inference(resolution,[status(thm)],[c4,clause1]) ).
cnf(c3,plain,
( ~ ssRr(X13,X13)
| ~ ssPv4(X13)
| ~ ssPv3(X13)
| ssPv1(X13) ),
inference(factor,[status(thm)],[clause3]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X4,X5)
| ~ ssRr(X3,X4)
| ~ ssPv1(X3)
| ~ ssPv4(X3)
| ssPv3(X5)
| ssPv3(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c1,plain,
( ~ ssRr(skf1(X8),X7)
| ~ ssPv1(X8)
| ~ ssPv4(X8)
| ssPv3(X7)
| ssPv3(X8) ),
inference(resolution,[status(thm)],[clause2,clause1]) ).
cnf(c2,plain,
( ~ ssPv1(X9)
| ~ ssPv4(X9)
| ssPv3(skf1(skf1(X9)))
| ssPv3(X9) ),
inference(resolution,[status(thm)],[c1,clause1]) ).
cnf(c0,plain,
( ~ ssRr(X6,X6)
| ~ ssPv1(X6)
| ~ ssPv4(X6)
| ssPv3(X6) ),
inference(factor,[status(thm)],[clause2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SYN742-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.32 % Computer : n032.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed May 8 20:10:22 EDT 2024
% 0.11/0.32 % CPUTime :
% 4.11/4.35 % Version: 1.5
% 4.11/4.35 % SZS status Satisfiable
% 4.11/4.35 % SZS output start Saturation
% See solution above
% 4.21/4.37
% 4.21/4.37 % Initial clauses : 31
% 4.21/4.37 % Processed clauses : 678
% 4.21/4.37 % Factors computed : 900
% 4.21/4.37 % Resolvents computed: 406
% 4.21/4.37 % Tautologies deleted: 239
% 4.21/4.37 % Forward subsumed : 420
% 4.21/4.37 % Backward subsumed : 23
% 4.21/4.37 % -------- CPU Time ---------
% 4.21/4.37 % User time : 4.038 s
% 4.21/4.37 % System time : 0.011 s
% 4.21/4.37 % Total time : 4.049 s
%------------------------------------------------------------------------------