%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN760-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:58 EDT 2024
% Result : Satisfiable 3.52s 3.75s
% Output : Saturation 3.61s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause1,negated_conjecture,
ssRr(X2,skf1(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause51,negated_conjecture,
( ~ ssRr(X710,X713)
| ~ ssPv4(X713)
| ~ ssRr(X714,X710)
| ~ ssRr(X709,X711)
| ~ ssPv3(X711)
| ~ ssRr(X714,X709)
| ~ ssRr(X712,X715)
| ~ ssRr(X714,X712)
| ssPv2(X715)
| ssPv2(X714) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c369,plain,
( ~ ssRr(X2438,X2436)
| ~ ssPv4(X2436)
| ~ ssRr(X2439,X2438)
| ~ ssRr(X2440,X2437)
| ~ ssPv3(X2437)
| ~ ssRr(X2439,X2440)
| ~ ssRr(skf1(X2439),X2435)
| ssPv2(X2435)
| ssPv2(X2439) ),
inference(resolution,[status(thm)],[clause51,clause1]) ).
cnf(c1101,plain,
( ~ ssRr(X3970,X3968)
| ~ ssPv4(X3968)
| ~ ssRr(X3969,X3970)
| ~ ssRr(X3967,X3971)
| ~ ssPv3(X3971)
| ~ ssRr(X3969,X3967)
| ssPv2(skf1(skf1(X3969)))
| ssPv2(X3969) ),
inference(resolution,[status(thm)],[c369,clause1]) ).
cnf(c1545,plain,
( ~ ssRr(X4058,X4057)
| ~ ssPv4(X4057)
| ~ ssRr(X4059,X4058)
| ~ ssRr(X4058,X4056)
| ~ ssPv3(X4056)
| ssPv2(skf1(skf1(X4059)))
| ssPv2(X4059) ),
inference(factor,[status(thm)],[c1101]) ).
cnf(c1571,plain,
( ~ ssRr(X4073,X4072)
| ~ ssPv4(X4072)
| ~ ssRr(X4074,X4073)
| ~ ssPv3(skf1(X4073))
| ssPv2(skf1(skf1(X4074)))
| ssPv2(X4074) ),
inference(resolution,[status(thm)],[c1545,clause1]) ).
cnf(c367,plain,
( ~ ssRr(X2408,X2406)
| ~ ssPv4(X2406)
| ~ ssRr(X2409,X2408)
| ~ ssRr(X2404,X2407)
| ~ ssPv3(X2407)
| ~ ssRr(X2409,X2404)
| ~ ssRr(X2404,X2405)
| ssPv2(X2405)
| ssPv2(X2409) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c1087,plain,
( ~ ssRr(X3916,X3917)
| ~ ssPv4(X3917)
| ~ ssRr(X3919,X3916)
| ~ ssRr(X3918,X3915)
| ~ ssPv3(X3915)
| ~ ssRr(X3919,X3918)
| ssPv2(skf1(X3918))
| ssPv2(X3919) ),
inference(resolution,[status(thm)],[c367,clause1]) ).
cnf(c1532,plain,
( ~ ssRr(X4067,X4065)
| ~ ssPv4(X4065)
| ~ ssRr(X4066,X4067)
| ~ ssRr(skf1(X4066),X4064)
| ~ ssPv3(X4064)
| ssPv2(skf1(skf1(X4066)))
| ssPv2(X4066) ),
inference(resolution,[status(thm)],[c1087,clause1]) ).
cnf(c1569,plain,
( ~ ssRr(X4060,X4061)
| ~ ssPv4(X4061)
| ~ ssRr(X4062,X4060)
| ~ ssPv3(X4061)
| ssPv2(skf1(skf1(X4062)))
| ssPv2(X4062) ),
inference(factor,[status(thm)],[c1545]) ).
cnf(c1085,plain,
( ~ ssRr(X3894,X3896)
| ~ ssPv4(X3896)
| ~ ssRr(X3897,X3894)
| ~ ssRr(X3898,X3895)
| ~ ssPv3(X3895)
| ~ ssRr(X3897,X3898)
| ssPv2(X3895)
| ssPv2(X3897) ),
inference(factor,[status(thm)],[c367]) ).
cnf(c1526,plain,
( ~ ssRr(X3909,X3910)
| ~ ssPv4(X3910)
| ~ ssRr(X3912,X3909)
| ~ ssRr(skf1(X3912),X3911)
| ~ ssPv3(X3911)
| ssPv2(X3911)
| ssPv2(X3912) ),
inference(resolution,[status(thm)],[c1085,clause1]) ).
cnf(c1528,plain,
( ~ ssRr(X4045,X4044)
| ~ ssPv4(X4044)
| ~ ssRr(X4046,X4045)
| ~ ssPv3(skf1(skf1(X4046)))
| ssPv2(skf1(skf1(X4046)))
| ssPv2(X4046) ),
inference(resolution,[status(thm)],[c1526,clause1]) ).
cnf(c365,plain,
( ~ ssRr(X2372,X2374)
| ~ ssPv4(X2374)
| ~ ssRr(X2377,X2372)
| ~ ssRr(X2376,X2375)
| ~ ssPv3(X2375)
| ~ ssRr(X2377,X2376)
| ~ ssRr(X2372,X2373)
| ssPv2(X2373)
| ssPv2(X2377) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c1071,plain,
( ~ ssRr(X3862,X3863)
| ~ ssPv4(X3863)
| ~ ssRr(X3860,X3862)
| ~ ssRr(X3859,X3861)
| ~ ssPv3(X3861)
| ~ ssRr(X3860,X3859)
| ssPv2(skf1(X3862))
| ssPv2(X3860) ),
inference(resolution,[status(thm)],[c365,clause1]) ).
cnf(c1516,plain,
( ~ ssRr(X4038,X4040)
| ~ ssPv4(X4040)
| ~ ssRr(X4039,X4038)
| ~ ssRr(skf1(X4039),X4037)
| ~ ssPv3(X4037)
| ssPv2(skf1(X4038))
| ssPv2(X4039) ),
inference(resolution,[status(thm)],[c1071,clause1]) ).
cnf(c1568,plain,
( ~ ssRr(X4041,X4043)
| ~ ssPv4(X4043)
| ~ ssRr(X4042,X4041)
| ~ ssPv3(skf1(skf1(X4042)))
| ssPv2(skf1(X4041))
| ssPv2(X4042) ),
inference(resolution,[status(thm)],[c1516,clause1]) ).
cnf(clause50,negated_conjecture,
( ~ ssRr(X692,X695)
| ~ ssPv2(X695)
| ~ ssRr(X696,X692)
| ~ ssRr(X691,X693)
| ~ ssRr(X696,X691)
| ~ ssRr(X694,X697)
| ~ ssRr(X696,X694)
| ssPv4(X693)
| ssPv3(X697)
| ssPv3(X696) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(c355,plain,
( ~ ssRr(X2313,X2309)
| ~ ssPv2(X2309)
| ~ ssRr(X2308,X2313)
| ~ ssRr(X2312,X2310)
| ~ ssRr(X2308,X2312)
| ~ ssRr(X2312,X2311)
| ssPv4(X2310)
| ssPv3(X2311)
| ssPv3(X2308) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c1041,plain,
( ~ ssRr(X3766,X3763)
| ~ ssPv2(X3763)
| ~ ssRr(X3764,X3766)
| ~ ssRr(X3765,X3762)
| ~ ssRr(X3764,X3765)
| ssPv4(X3762)
| ssPv3(skf1(X3765))
| ssPv3(X3764) ),
inference(resolution,[status(thm)],[c355,clause1]) ).
cnf(c1494,plain,
( ~ ssRr(X4029,X4030)
| ~ ssPv2(X4030)
| ~ ssRr(X4031,X4029)
| ~ ssRr(skf1(X4031),X4028)
| ssPv4(X4028)
| ssPv3(skf1(skf1(X4031)))
| ssPv3(X4031) ),
inference(resolution,[status(thm)],[c1041,clause1]) ).
cnf(c357,plain,
( ~ ssRr(X2348,X2343)
| ~ ssPv2(X2343)
| ~ ssRr(X2345,X2348)
| ~ ssRr(X2347,X2344)
| ~ ssRr(X2345,X2347)
| ~ ssRr(skf1(X2345),X2346)
| ssPv4(X2344)
| ssPv3(X2346)
| ssPv3(X2345) ),
inference(resolution,[status(thm)],[clause50,clause1]) ).
cnf(c1052,plain,
( ~ ssRr(X3818,X3817)
| ~ ssPv2(X3817)
| ~ ssRr(X3819,X3818)
| ~ ssRr(X3821,X3820)
| ~ ssRr(X3819,X3821)
| ssPv4(X3820)
| ssPv3(skf1(skf1(X3819)))
| ssPv3(X3819) ),
inference(resolution,[status(thm)],[c357,clause1]) ).
cnf(c1504,plain,
( ~ ssRr(X4008,X4010)
| ~ ssPv2(X4010)
| ~ ssRr(X4009,X4008)
| ~ ssRr(X4008,X4011)
| ssPv4(X4011)
| ssPv3(skf1(skf1(X4009)))
| ssPv3(X4009) ),
inference(factor,[status(thm)],[c1052]) ).
cnf(c1560,plain,
( ~ ssRr(X4026,X4024)
| ~ ssPv2(X4024)
| ~ ssRr(X4025,X4026)
| ssPv4(skf1(X4026))
| ssPv3(skf1(skf1(X4025)))
| ssPv3(X4025) ),
inference(resolution,[status(thm)],[c1504,clause1]) ).
cnf(c1558,plain,
( ~ ssRr(X4012,X4013)
| ~ ssPv2(X4013)
| ~ ssRr(X4014,X4012)
| ssPv4(X4013)
| ssPv3(skf1(skf1(X4014)))
| ssPv3(X4014) ),
inference(factor,[status(thm)],[c1504]) ).
cnf(clause49,negated_conjecture,
( ~ ssRr(X675,X678)
| ~ ssPv1(X678)
| ~ ssRr(X679,X675)
| ~ ssRr(X674,X676)
| ~ ssRr(X679,X674)
| ~ ssRr(X677,X680)
| ~ ssRr(X679,X677)
| ssPv4(X676)
| ssPv3(X680)
| ssPv3(X679) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(c345,plain,
( ~ ssRr(X2213,X2214)
| ~ ssPv1(X2214)
| ~ ssRr(X2218,X2213)
| ~ ssRr(X2216,X2215)
| ~ ssRr(X2218,X2216)
| ~ ssRr(X2216,X2217)
| ssPv4(X2215)
| ssPv3(X2217)
| ssPv3(X2218) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c993,plain,
( ~ ssRr(X3581,X3577)
| ~ ssPv1(X3577)
| ~ ssRr(X3579,X3581)
| ~ ssRr(X3580,X3578)
| ~ ssRr(X3579,X3580)
| ssPv4(X3578)
| ssPv3(skf1(X3580))
| ssPv3(X3579) ),
inference(resolution,[status(thm)],[c345,clause1]) ).
cnf(c1456,plain,
( ~ ssRr(X3999,X4000)
| ~ ssPv1(X4000)
| ~ ssRr(X4001,X3999)
| ~ ssRr(skf1(X4001),X3998)
| ssPv4(X3998)
| ssPv3(skf1(skf1(X4001)))
| ssPv3(X4001) ),
inference(resolution,[status(thm)],[c993,clause1]) ).
cnf(c1039,plain,
( ~ ssRr(X3749,X3747)
| ~ ssPv2(X3747)
| ~ ssRr(X3748,X3749)
| ~ ssRr(X3750,X3746)
| ~ ssRr(X3748,X3750)
| ssPv4(X3746)
| ssPv3(X3746)
| ssPv3(X3748) ),
inference(factor,[status(thm)],[c355]) ).
cnf(c1488,plain,
( ~ ssRr(X3806,X3805)
| ~ ssPv2(X3805)
| ~ ssRr(X3807,X3806)
| ~ ssRr(skf1(X3807),X3804)
| ssPv4(X3804)
| ssPv3(X3804)
| ssPv3(X3807) ),
inference(resolution,[status(thm)],[c1039,clause1]) ).
cnf(c1502,plain,
( ~ ssRr(X3996,X3995)
| ~ ssPv2(X3995)
| ~ ssRr(X3997,X3996)
| ssPv4(skf1(skf1(X3997)))
| ssPv3(skf1(skf1(X3997)))
| ssPv3(X3997) ),
inference(resolution,[status(thm)],[c1488,clause1]) ).
cnf(c991,plain,
( ~ ssRr(X3562,X3559)
| ~ ssPv1(X3559)
| ~ ssRr(X3560,X3562)
| ~ ssRr(X3561,X3558)
| ~ ssRr(X3560,X3561)
| ssPv4(X3558)
| ssPv3(X3558)
| ssPv3(X3560) ),
inference(factor,[status(thm)],[c345]) ).
cnf(c1450,plain,
( ~ ssRr(X3724,X3723)
| ~ ssPv1(X3723)
| ~ ssRr(X3725,X3724)
| ~ ssRr(skf1(X3725),X3722)
| ssPv4(X3722)
| ssPv3(X3722)
| ssPv3(X3725) ),
inference(resolution,[status(thm)],[c991,clause1]) ).
cnf(c1482,plain,
( ~ ssRr(X3991,X3989)
| ~ ssPv1(X3989)
| ~ ssRr(X3990,X3991)
| ssPv4(skf1(skf1(X3990)))
| ssPv3(skf1(skf1(X3990)))
| ssPv3(X3990) ),
inference(resolution,[status(thm)],[c1450,clause1]) ).
cnf(clause47,negated_conjecture,
( ~ ssRr(X644,X647)
| ~ ssPv4(X647)
| ~ ssRr(X648,X644)
| ~ ssRr(X643,X645)
| ~ ssPv1(X645)
| ~ ssRr(X648,X643)
| ~ ssRr(X648,X646)
| ~ ssPv1(X646)
| ssPv3(X648) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c327,plain,
( ~ ssRr(X2030,X2033)
| ~ ssPv4(X2033)
| ~ ssRr(X2029,X2030)
| ~ ssRr(X2031,X2032)
| ~ ssPv1(X2032)
| ~ ssRr(X2029,X2031)
| ~ ssPv1(X2030)
| ssPv3(X2029) ),
inference(factor,[status(thm)],[clause47]) ).
cnf(c914,plain,
( ~ ssRr(X3414,X3415)
| ~ ssPv4(X3415)
| ~ ssRr(X3412,X3414)
| ~ ssRr(skf1(X3412),X3413)
| ~ ssPv1(X3413)
| ~ ssPv1(X3414)
| ssPv3(X3412) ),
inference(resolution,[status(thm)],[c327,clause1]) ).
cnf(c1410,plain,
( ~ ssRr(X3416,X3418)
| ~ ssPv4(X3418)
| ~ ssRr(X3417,X3416)
| ~ ssPv1(skf1(skf1(X3417)))
| ~ ssPv1(X3416)
| ssPv3(X3417) ),
inference(resolution,[status(thm)],[c914,clause1]) ).
cnf(c1411,plain,
( ~ ssRr(skf1(skf1(X3985)),X3986)
| ~ ssPv4(X3986)
| ~ ssRr(X3985,skf1(skf1(X3985)))
| ~ ssPv1(skf1(skf1(X3985)))
| ssPv3(X3985) ),
inference(factor,[status(thm)],[c1410]) ).
cnf(c353,plain,
( ~ ssRr(X2280,X2281)
| ~ ssPv2(X2281)
| ~ ssRr(X2279,X2280)
| ~ ssRr(X2284,X2282)
| ~ ssRr(X2279,X2284)
| ~ ssRr(X2280,X2283)
| ssPv4(X2282)
| ssPv3(X2283)
| ssPv3(X2279) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c1027,plain,
( ~ ssRr(X3694,X3691)
| ~ ssPv2(X3691)
| ~ ssRr(X3692,X3694)
| ~ ssRr(X3693,X3695)
| ~ ssRr(X3692,X3693)
| ssPv4(X3695)
| ssPv3(skf1(X3694))
| ssPv3(X3692) ),
inference(resolution,[status(thm)],[c353,clause1]) ).
cnf(c1474,plain,
( ~ ssRr(X3980,X3979)
| ~ ssPv2(X3979)
| ~ ssRr(X3978,X3980)
| ~ ssRr(skf1(X3978),X3977)
| ssPv4(X3977)
| ssPv3(skf1(X3980))
| ssPv3(X3978) ),
inference(resolution,[status(thm)],[c1027,clause1]) ).
cnf(c1549,plain,
( ~ ssRr(X3981,X3982)
| ~ ssPv2(X3982)
| ~ ssRr(X3983,X3981)
| ssPv4(skf1(skf1(X3983)))
| ssPv3(skf1(X3981))
| ssPv3(X3983) ),
inference(resolution,[status(thm)],[c1474,clause1]) ).
cnf(c347,plain,
( ~ ssRr(X2247,X2248)
| ~ ssPv1(X2248)
| ~ ssRr(X2250,X2247)
| ~ ssRr(X2251,X2249)
| ~ ssRr(X2250,X2251)
| ~ ssRr(skf1(X2250),X2252)
| ssPv4(X2249)
| ssPv3(X2252)
| ssPv3(X2250) ),
inference(resolution,[status(thm)],[clause49,clause1]) ).
cnf(c1008,plain,
( ~ ssRr(X3626,X3623)
| ~ ssPv1(X3623)
| ~ ssRr(X3624,X3626)
| ~ ssRr(X3627,X3625)
| ~ ssRr(X3624,X3627)
| ssPv4(X3625)
| ssPv3(skf1(skf1(X3624)))
| ssPv3(X3624) ),
inference(resolution,[status(thm)],[c347,clause1]) ).
cnf(c1460,plain,
( ~ ssRr(X3949,X3948)
| ~ ssPv1(X3948)
| ~ ssRr(X3950,X3949)
| ~ ssRr(X3949,X3947)
| ssPv4(X3947)
| ssPv3(skf1(skf1(X3950)))
| ssPv3(X3950) ),
inference(factor,[status(thm)],[c1008]) ).
cnf(c1539,plain,
( ~ ssRr(X3965,X3963)
| ~ ssPv1(X3963)
| ~ ssRr(X3964,X3965)
| ssPv4(skf1(X3965))
| ssPv3(skf1(skf1(X3964)))
| ssPv3(X3964) ),
inference(resolution,[status(thm)],[c1460,clause1]) ).
cnf(c1537,plain,
( ~ ssRr(X3951,X3953)
| ~ ssPv1(X3953)
| ~ ssRr(X3952,X3951)
| ssPv4(X3953)
| ssPv3(skf1(skf1(X3952)))
| ssPv3(X3952) ),
inference(factor,[status(thm)],[c1460]) ).
cnf(c343,plain,
( ~ ssRr(X2182,X2180)
| ~ ssPv1(X2180)
| ~ ssRr(X2185,X2182)
| ~ ssRr(X2184,X2181)
| ~ ssRr(X2185,X2184)
| ~ ssRr(X2182,X2183)
| ssPv4(X2181)
| ssPv3(X2183)
| ssPv3(X2185) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c979,plain,
( ~ ssRr(X3519,X3520)
| ~ ssPv1(X3520)
| ~ ssRr(X3518,X3519)
| ~ ssRr(X3517,X3521)
| ~ ssRr(X3518,X3517)
| ssPv4(X3521)
| ssPv3(skf1(X3519))
| ssPv3(X3518) ),
inference(resolution,[status(thm)],[c343,clause1]) ).
cnf(c1440,plain,
( ~ ssRr(X3930,X3933)
| ~ ssPv1(X3933)
| ~ ssRr(X3932,X3930)
| ~ ssRr(skf1(X3932),X3931)
| ssPv4(X3931)
| ssPv3(skf1(X3930))
| ssPv3(X3932) ),
inference(resolution,[status(thm)],[c979,clause1]) ).
cnf(c1534,plain,
( ~ ssRr(X3936,X3934)
| ~ ssPv1(X3934)
| ~ ssRr(X3935,X3936)
| ssPv4(skf1(skf1(X3935)))
| ssPv3(skf1(X3936))
| ssPv3(X3935) ),
inference(resolution,[status(thm)],[c1440,clause1]) ).
cnf(c1514,plain,
( ~ ssRr(X3869,X3870)
| ~ ssPv4(X3870)
| ~ ssRr(X3867,X3869)
| ~ ssRr(X3869,X3868)
| ~ ssPv3(X3868)
| ssPv2(skf1(X3869))
| ssPv2(X3867) ),
inference(factor,[status(thm)],[c1071]) ).
cnf(c1517,plain,
( ~ ssRr(X3871,X3872)
| ~ ssPv4(X3872)
| ~ ssRr(X3873,X3871)
| ~ ssPv3(X3872)
| ssPv2(skf1(X3871))
| ssPv2(X3873) ),
inference(factor,[status(thm)],[c1514]) ).
cnf(c1521,plain,
( ~ ssRr(skf1(X3882),X3881)
| ~ ssPv4(X3881)
| ~ ssPv3(X3881)
| ssPv2(skf1(skf1(X3882)))
| ssPv2(X3882) ),
inference(resolution,[status(thm)],[c1517,clause1]) ).
cnf(c1067,plain,
( ~ ssRr(X3829,X3831)
| ~ ssPv4(X3831)
| ~ ssRr(X3828,X3829)
| ~ ssRr(X3827,X3830)
| ~ ssPv3(X3830)
| ~ ssRr(X3828,X3827)
| ssPv2(X3831)
| ssPv2(X3828) ),
inference(factor,[status(thm)],[c365]) ).
cnf(c1510,plain,
( ~ ssRr(X3846,X3847)
| ~ ssPv4(X3847)
| ~ ssRr(X3849,X3846)
| ~ ssRr(skf1(X3849),X3848)
| ~ ssPv3(X3848)
| ssPv2(X3847)
| ssPv2(X3849) ),
inference(resolution,[status(thm)],[c1067,clause1]) ).
cnf(c1512,plain,
( ~ ssRr(X3852,X3853)
| ~ ssPv4(X3853)
| ~ ssRr(X3854,X3852)
| ~ ssPv3(skf1(skf1(X3854)))
| ssPv2(X3853)
| ssPv2(X3854) ),
inference(resolution,[status(thm)],[c1510,clause1]) ).
cnf(c1472,plain,
( ~ ssRr(X3777,X3779)
| ~ ssPv2(X3779)
| ~ ssRr(X3778,X3777)
| ~ ssRr(X3777,X3780)
| ssPv4(X3780)
| ssPv3(skf1(X3777))
| ssPv3(X3778) ),
inference(factor,[status(thm)],[c1027]) ).
cnf(c1495,plain,
( ~ ssRr(X3783,X3782)
| ~ ssPv2(X3782)
| ~ ssRr(X3781,X3783)
| ssPv4(X3782)
| ssPv3(skf1(X3783))
| ssPv3(X3781) ),
inference(factor,[status(thm)],[c1472]) ).
cnf(c1499,plain,
( ~ ssRr(skf1(X3791),X3792)
| ~ ssPv2(X3792)
| ssPv4(X3792)
| ssPv3(skf1(skf1(X3791)))
| ssPv3(X3791) ),
inference(resolution,[status(thm)],[c1495,clause1]) ).
cnf(c1023,plain,
( ~ ssRr(X3658,X3655)
| ~ ssPv2(X3655)
| ~ ssRr(X3656,X3658)
| ~ ssRr(X3657,X3659)
| ~ ssRr(X3656,X3657)
| ssPv4(X3659)
| ssPv3(X3655)
| ssPv3(X3656) ),
inference(factor,[status(thm)],[c353]) ).
cnf(c1466,plain,
( ~ ssRr(X3745,X3744)
| ~ ssPv2(X3744)
| ~ ssRr(X3743,X3745)
| ~ ssRr(skf1(X3743),X3742)
| ssPv4(X3742)
| ssPv3(X3744)
| ssPv3(X3743) ),
inference(resolution,[status(thm)],[c1023,clause1]) ).
cnf(c1484,plain,
( ~ ssRr(X3756,X3758)
| ~ ssPv2(X3758)
| ~ ssRr(X3757,X3756)
| ssPv4(skf1(skf1(X3757)))
| ssPv3(X3758)
| ssPv3(X3757) ),
inference(resolution,[status(thm)],[c1466,clause1]) ).
cnf(c1438,plain,
( ~ ssRr(X3699,X3702)
| ~ ssPv1(X3702)
| ~ ssRr(X3700,X3699)
| ~ ssRr(X3699,X3701)
| ssPv4(X3701)
| ssPv3(skf1(X3699))
| ssPv3(X3700) ),
inference(factor,[status(thm)],[c979]) ).
cnf(c1475,plain,
( ~ ssRr(X3705,X3704)
| ~ ssPv1(X3704)
| ~ ssRr(X3703,X3705)
| ssPv4(X3704)
| ssPv3(skf1(X3705))
| ssPv3(X3703) ),
inference(factor,[status(thm)],[c1438]) ).
cnf(c1479,plain,
( ~ ssRr(skf1(X3714),X3713)
| ~ ssPv1(X3713)
| ssPv4(X3713)
| ssPv3(skf1(skf1(X3714)))
| ssPv3(X3714) ),
inference(resolution,[status(thm)],[c1475,clause1]) ).
cnf(c975,plain,
( ~ ssRr(X3485,X3486)
| ~ ssPv1(X3486)
| ~ ssRr(X3487,X3485)
| ~ ssRr(X3484,X3488)
| ~ ssRr(X3487,X3484)
| ssPv4(X3488)
| ssPv3(X3486)
| ssPv3(X3487) ),
inference(factor,[status(thm)],[c343]) ).
cnf(c1434,plain,
( ~ ssRr(X3680,X3681)
| ~ ssPv1(X3681)
| ~ ssRr(X3679,X3680)
| ~ ssRr(skf1(X3679),X3682)
| ssPv4(X3682)
| ssPv3(X3681)
| ssPv3(X3679) ),
inference(resolution,[status(thm)],[c975,clause1]) ).
cnf(c1468,plain,
( ~ ssRr(X3686,X3687)
| ~ ssPv1(X3687)
| ~ ssRr(X3685,X3686)
| ssPv4(skf1(skf1(X3685)))
| ssPv3(X3687)
| ssPv3(X3685) ),
inference(resolution,[status(thm)],[c1434,clause1]) ).
cnf(clause48,negated_conjecture,
( ~ ssRr(X659,X662)
| ~ ssPv4(X662)
| ~ ssRr(X663,X659)
| ~ ssRr(X658,X660)
| ~ ssPv1(X660)
| ~ ssRr(X663,X658)
| ~ ssRr(X663,X661)
| ~ ssPv2(X661)
| ~ ssPv4(X663) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(c337,plain,
( ~ ssRr(X2131,X2133)
| ~ ssPv4(X2133)
| ~ ssRr(X2134,X2131)
| ~ ssRr(X2132,X2135)
| ~ ssPv1(X2135)
| ~ ssRr(X2134,X2132)
| ~ ssPv2(X2132)
| ~ ssPv4(X2134) ),
inference(factor,[status(thm)],[clause48]) ).
cnf(c960,plain,
( ~ ssRr(X3457,X3458)
| ~ ssPv4(X3458)
| ~ ssRr(X3459,X3457)
| ~ ssRr(skf1(X3459),X3456)
| ~ ssPv1(X3456)
| ~ ssPv2(skf1(X3459))
| ~ ssPv4(X3459) ),
inference(resolution,[status(thm)],[c337,clause1]) ).
cnf(c1426,plain,
( ~ ssRr(X3674,X3672)
| ~ ssPv4(X3672)
| ~ ssRr(X3673,X3674)
| ~ ssPv1(skf1(skf1(X3673)))
| ~ ssPv2(skf1(X3673))
| ~ ssPv4(X3673) ),
inference(resolution,[status(thm)],[c960,clause1]) ).
cnf(c329,plain,
( ~ ssRr(X2060,X2064)
| ~ ssPv4(X2064)
| ~ ssRr(X2062,X2060)
| ~ ssRr(X2061,X2063)
| ~ ssPv1(X2063)
| ~ ssRr(X2062,X2061)
| ~ ssPv1(X2061)
| ssPv3(X2062) ),
inference(factor,[status(thm)],[clause47]) ).
cnf(c928,plain,
( ~ ssRr(X3429,X3431)
| ~ ssPv4(X3431)
| ~ ssRr(X3430,X3429)
| ~ ssRr(skf1(X3430),X3428)
| ~ ssPv1(X3428)
| ~ ssPv1(skf1(X3430))
| ssPv3(X3430) ),
inference(resolution,[status(thm)],[c329,clause1]) ).
cnf(c1416,plain,
( ~ ssRr(X3653,X3652)
| ~ ssPv4(X3652)
| ~ ssRr(X3654,X3653)
| ~ ssPv1(skf1(skf1(X3654)))
| ~ ssPv1(skf1(X3654))
| ssPv3(X3654) ),
inference(resolution,[status(thm)],[c928,clause1]) ).
cnf(clause46,negated_conjecture,
( ~ ssRr(X621,X624)
| ~ ssPv2(X624)
| ~ ssRr(X625,X621)
| ~ ssRr(X620,X622)
| ~ ssRr(X625,X620)
| ~ ssRr(X625,X623)
| ~ ssPv1(X623)
| ~ ssPv1(X625)
| ssPv3(X622) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(c321,plain,
( ~ ssRr(X1989,X1991)
| ~ ssPv2(X1991)
| ~ ssRr(X1990,X1989)
| ~ ssRr(X1993,X1992)
| ~ ssRr(X1990,X1993)
| ~ ssPv1(X1993)
| ~ ssPv1(X1990)
| ssPv3(X1992) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c899,plain,
( ~ ssRr(X3408,X3411)
| ~ ssPv2(X3411)
| ~ ssRr(X3410,X3408)
| ~ ssRr(skf1(X3410),X3409)
| ~ ssPv1(skf1(X3410))
| ~ ssPv1(X3410)
| ssPv3(X3409) ),
inference(resolution,[status(thm)],[c321,clause1]) ).
cnf(c1408,plain,
( ~ ssRr(X3645,X3643)
| ~ ssPv2(X3643)
| ~ ssRr(X3644,X3645)
| ~ ssPv1(skf1(X3644))
| ~ ssPv1(X3644)
| ssPv3(skf1(skf1(X3644))) ),
inference(resolution,[status(thm)],[c899,clause1]) ).
cnf(clause45,negated_conjecture,
( ~ ssRr(X604,X607)
| ~ ssPv4(X607)
| ~ ssRr(X608,X604)
| ~ ssRr(X603,X605)
| ~ ssRr(X608,X603)
| ~ ssRr(X608,X606)
| ~ ssPv2(X606)
| ~ ssPv4(X608)
| ssPv3(X605) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(c312,plain,
( ~ ssRr(X1922,X1924)
| ~ ssPv4(X1924)
| ~ ssRr(X1921,X1922)
| ~ ssRr(X1925,X1923)
| ~ ssRr(X1921,X1925)
| ~ ssPv2(X1925)
| ~ ssPv4(X1921)
| ssPv3(X1923) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c863,plain,
( ~ ssRr(X3380,X3381)
| ~ ssPv4(X3381)
| ~ ssRr(X3382,X3380)
| ~ ssRr(skf1(X3382),X3379)
| ~ ssPv2(skf1(X3382))
| ~ ssPv4(X3382)
| ssPv3(X3379) ),
inference(resolution,[status(thm)],[c312,clause1]) ).
cnf(c1398,plain,
( ~ ssRr(X3634,X3632)
| ~ ssPv4(X3632)
| ~ ssRr(X3633,X3634)
| ~ ssPv2(skf1(X3633))
| ~ ssPv4(X3633)
| ssPv3(skf1(skf1(X3633))) ),
inference(resolution,[status(thm)],[c863,clause1]) ).
cnf(clause44,negated_conjecture,
( ~ ssRr(X584,X587)
| ~ ssPv1(X587)
| ~ ssRr(X588,X584)
| ~ ssRr(X583,X585)
| ~ ssRr(X588,X583)
| ~ ssRr(X588,X586)
| ~ ssPv4(X586)
| ssPv2(X585)
| ssPv3(X588) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c301,plain,
( ~ ssRr(X1850,X1851)
| ~ ssPv1(X1851)
| ~ ssRr(X1849,X1850)
| ~ ssRr(X1847,X1848)
| ~ ssRr(X1849,X1847)
| ~ ssPv4(X1847)
| ssPv2(X1848)
| ssPv3(X1849) ),
inference(factor,[status(thm)],[clause44]) ).
cnf(c833,plain,
( ~ ssRr(X3343,X3345)
| ~ ssPv1(X3345)
| ~ ssRr(X3346,X3343)
| ~ ssRr(skf1(X3346),X3344)
| ~ ssPv4(skf1(X3346))
| ssPv2(X3344)
| ssPv3(X3346) ),
inference(resolution,[status(thm)],[c301,clause1]) ).
cnf(c1389,plain,
( ~ ssRr(X3621,X3620)
| ~ ssPv1(X3620)
| ~ ssRr(X3622,X3621)
| ~ ssPv4(skf1(X3622))
| ssPv2(skf1(skf1(X3622)))
| ssPv3(X3622) ),
inference(resolution,[status(thm)],[c833,clause1]) ).
cnf(clause43,negated_conjecture,
( ~ ssRr(X568,X571)
| ~ ssPv3(X571)
| ~ ssRr(X572,X568)
| ~ ssRr(X567,X569)
| ~ ssPv1(X569)
| ~ ssRr(X572,X567)
| ~ ssRr(X572,X570)
| ssPv4(X570)
| ssPv4(X572) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c293,plain,
( ~ ssRr(X1777,X1776)
| ~ ssPv3(X1776)
| ~ ssRr(X1775,X1777)
| ~ ssRr(X1779,X1778)
| ~ ssPv1(X1778)
| ~ ssRr(X1775,X1779)
| ssPv4(X1779)
| ssPv4(X1775) ),
inference(factor,[status(thm)],[clause43]) ).
cnf(c797,plain,
( ~ ssRr(X3239,X3240)
| ~ ssPv3(X3240)
| ~ ssRr(X3241,X3239)
| ~ ssRr(skf1(X3241),X3238)
| ~ ssPv1(X3238)
| ssPv4(skf1(X3241))
| ssPv4(X3241) ),
inference(resolution,[status(thm)],[c293,clause1]) ).
cnf(c1359,plain,
( ~ ssRr(X3614,X3613)
| ~ ssPv3(X3613)
| ~ ssRr(X3615,X3614)
| ~ ssPv1(skf1(skf1(X3615)))
| ssPv4(skf1(X3615))
| ssPv4(X3615) ),
inference(resolution,[status(thm)],[c797,clause1]) ).
cnf(clause42,negated_conjecture,
( ~ ssRr(X551,X554)
| ~ ssPv3(X554)
| ~ ssRr(X555,X551)
| ~ ssRr(X550,X552)
| ~ ssRr(X555,X550)
| ~ ssRr(X555,X553)
| ~ ssPv2(X553)
| ssPv1(X552)
| ssPv4(X555) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c284,plain,
( ~ ssRr(X1704,X1703)
| ~ ssPv3(X1703)
| ~ ssRr(X1701,X1704)
| ~ ssRr(X1702,X1700)
| ~ ssRr(X1701,X1702)
| ~ ssPv2(X1702)
| ssPv1(X1700)
| ssPv4(X1701) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c766,plain,
( ~ ssRr(X3191,X3188)
| ~ ssPv3(X3188)
| ~ ssRr(X3190,X3191)
| ~ ssRr(skf1(X3190),X3189)
| ~ ssPv2(skf1(X3190))
| ssPv1(X3189)
| ssPv4(X3190) ),
inference(resolution,[status(thm)],[c284,clause1]) ).
cnf(c1340,plain,
( ~ ssRr(X3603,X3604)
| ~ ssPv3(X3604)
| ~ ssRr(X3602,X3603)
| ~ ssPv2(skf1(X3602))
| ssPv1(skf1(skf1(X3602)))
| ssPv4(X3602) ),
inference(resolution,[status(thm)],[c766,clause1]) ).
cnf(clause41,negated_conjecture,
( ~ ssRr(X531,X534)
| ~ ssPv4(X534)
| ~ ssRr(X535,X531)
| ~ ssRr(X530,X532)
| ~ ssRr(X535,X530)
| ~ ssRr(X535,X533)
| ssPv3(X532)
| ssPv1(X533)
| ssPv2(X535) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c273,plain,
( ~ ssRr(X1625,X1622)
| ~ ssPv4(X1622)
| ~ ssRr(X1624,X1625)
| ~ ssRr(X1621,X1623)
| ~ ssRr(X1624,X1621)
| ssPv3(X1623)
| ssPv1(X1621)
| ssPv2(X1624) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c730,plain,
( ~ ssRr(X3101,X3103)
| ~ ssPv4(X3103)
| ~ ssRr(X3102,X3101)
| ~ ssRr(skf1(X3102),X3100)
| ssPv3(X3100)
| ssPv1(skf1(X3102))
| ssPv2(X3102) ),
inference(resolution,[status(thm)],[c273,clause1]) ).
cnf(c1303,plain,
( ~ ssRr(X3589,X3590)
| ~ ssPv4(X3590)
| ~ ssRr(X3588,X3589)
| ssPv3(skf1(skf1(X3588)))
| ssPv1(skf1(X3588))
| ssPv2(X3588) ),
inference(resolution,[status(thm)],[c730,clause1]) ).
cnf(c1457,plain,
( ~ ssRr(X3591,X3591)
| ~ ssPv4(X3591)
| ssPv3(skf1(skf1(X3591)))
| ssPv1(skf1(X3591))
| ssPv2(X3591) ),
inference(factor,[status(thm)],[c1303]) ).
cnf(clause40,negated_conjecture,
( ~ ssRr(X515,X518)
| ~ ssRr(X519,X515)
| ~ ssRr(X514,X516)
| ~ ssRr(X519,X514)
| ~ ssRr(X519,X517)
| ~ ssPv4(X519)
| ssPv4(X518)
| ssPv3(X516)
| ssPv4(X517) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c265,plain,
( ~ ssRr(X1542,X1546)
| ~ ssRr(X1543,X1542)
| ~ ssRr(X1545,X1544)
| ~ ssRr(X1543,X1545)
| ~ ssPv4(X1543)
| ssPv4(X1546)
| ssPv3(X1544)
| ssPv4(X1545) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c697,plain,
( ~ ssRr(X3010,X3009)
| ~ ssRr(X3011,X3010)
| ~ ssRr(skf1(X3011),X3008)
| ~ ssPv4(X3011)
| ssPv4(X3009)
| ssPv3(X3008)
| ssPv4(skf1(X3011)) ),
inference(resolution,[status(thm)],[c265,clause1]) ).
cnf(c1279,plain,
( ~ ssRr(X3573,X3574)
| ~ ssRr(X3575,X3573)
| ~ ssPv4(X3575)
| ssPv4(X3574)
| ssPv3(skf1(skf1(X3575)))
| ssPv4(skf1(X3575)) ),
inference(resolution,[status(thm)],[c697,clause1]) ).
cnf(c1025,plain,
( ~ ssRr(X2792,X2789)
| ~ ssPv2(X2789)
| ~ ssRr(X2790,X2792)
| ~ ssRr(X2792,X2791)
| ssPv4(X2791)
| ssPv3(X2791)
| ssPv3(X2790) ),
inference(factor,[status(thm)],[c353]) ).
cnf(c1203,plain,
( ~ ssRr(X2979,X2977)
| ~ ssPv2(X2977)
| ~ ssRr(X2978,X2979)
| ssPv4(skf1(X2979))
| ssPv3(skf1(X2979))
| ssPv3(X2978) ),
inference(resolution,[status(thm)],[c1025,clause1]) ).
cnf(c1270,plain,
( ~ ssRr(skf1(X3552),X3551)
| ~ ssPv2(X3551)
| ssPv4(skf1(skf1(X3552)))
| ssPv3(skf1(skf1(X3552)))
| ssPv3(X3552) ),
inference(resolution,[status(thm)],[c1203,clause1]) ).
cnf(c977,plain,
( ~ ssRr(X2719,X2718)
| ~ ssPv1(X2718)
| ~ ssRr(X2716,X2719)
| ~ ssRr(X2719,X2717)
| ssPv4(X2717)
| ssPv3(X2717)
| ssPv3(X2716) ),
inference(factor,[status(thm)],[c343]) ).
cnf(c1178,plain,
( ~ ssRr(X2951,X2949)
| ~ ssPv1(X2949)
| ~ ssRr(X2950,X2951)
| ssPv4(skf1(X2951))
| ssPv3(skf1(X2951))
| ssPv3(X2950) ),
inference(resolution,[status(thm)],[c977,clause1]) ).
cnf(c1260,plain,
( ~ ssRr(skf1(X3545),X3544)
| ~ ssPv1(X3544)
| ssPv4(skf1(skf1(X3545)))
| ssPv3(skf1(skf1(X3545)))
| ssPv3(X3545) ),
inference(resolution,[status(thm)],[c1178,clause1]) ).
cnf(clause39,negated_conjecture,
( ~ ssRr(X497,X500)
| ~ ssPv3(X500)
| ~ ssRr(X501,X497)
| ~ ssRr(X496,X498)
| ~ ssRr(X501,X496)
| ~ ssRr(X501,X499)
| ssPv2(X498)
| ssPv4(X499)
| ssPv4(X501) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c257,plain,
( ~ ssRr(X1470,X1471)
| ~ ssPv3(X1471)
| ~ ssRr(X1472,X1470)
| ~ ssRr(X1473,X1469)
| ~ ssRr(X1472,X1473)
| ssPv2(X1469)
| ssPv4(X1473)
| ssPv4(X1472) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c662,plain,
( ~ ssRr(X2936,X2935)
| ~ ssPv3(X2935)
| ~ ssRr(X2937,X2936)
| ~ ssRr(skf1(X2937),X2934)
| ssPv2(X2934)
| ssPv4(skf1(X2937))
| ssPv4(X2937) ),
inference(resolution,[status(thm)],[c257,clause1]) ).
cnf(c1255,plain,
( ~ ssRr(X3538,X3539)
| ~ ssPv3(X3539)
| ~ ssRr(X3540,X3538)
| ssPv2(skf1(skf1(X3540)))
| ssPv4(skf1(X3540))
| ssPv4(X3540) ),
inference(resolution,[status(thm)],[c662,clause1]) ).
cnf(clause38,negated_conjecture,
( ~ ssRr(X481,X484)
| ~ ssPv1(X484)
| ~ ssRr(X485,X481)
| ~ ssRr(X480,X482)
| ~ ssRr(X485,X480)
| ~ ssRr(X485,X483)
| ssPv1(X482)
| ssPv3(X483)
| ssPv3(X485) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c247,plain,
( ~ ssRr(X1399,X1400)
| ~ ssPv1(X1400)
| ~ ssRr(X1401,X1399)
| ~ ssRr(X1403,X1402)
| ~ ssRr(X1401,X1403)
| ssPv1(X1402)
| ssPv3(X1403)
| ssPv3(X1401) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c630,plain,
( ~ ssRr(X2834,X2832)
| ~ ssPv1(X2832)
| ~ ssRr(X2835,X2834)
| ~ ssRr(skf1(X2835),X2833)
| ssPv1(X2833)
| ssPv3(skf1(X2835))
| ssPv3(X2835) ),
inference(resolution,[status(thm)],[c247,clause1]) ).
cnf(c1219,plain,
( ~ ssRr(X3524,X3526)
| ~ ssPv1(X3526)
| ~ ssRr(X3525,X3524)
| ssPv1(skf1(skf1(X3525)))
| ssPv3(skf1(X3525))
| ssPv3(X3525) ),
inference(resolution,[status(thm)],[c630,clause1]) ).
cnf(clause37,negated_conjecture,
( ~ ssRr(X467,X470)
| ~ ssPv2(X470)
| ~ ssRr(X471,X467)
| ~ ssRr(X466,X468)
| ~ ssRr(X471,X466)
| ~ ssRr(X471,X469)
| ssPv1(X468)
| ssPv1(X469)
| ssPv4(X471) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c239,plain,
( ~ ssRr(X1330,X1332)
| ~ ssPv2(X1332)
| ~ ssRr(X1329,X1330)
| ~ ssRr(X1331,X1328)
| ~ ssRr(X1329,X1331)
| ssPv1(X1328)
| ssPv1(X1331)
| ssPv4(X1329) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c593,plain,
( ~ ssRr(X2728,X2731)
| ~ ssPv2(X2731)
| ~ ssRr(X2730,X2728)
| ~ ssRr(skf1(X2730),X2729)
| ssPv1(X2729)
| ssPv1(skf1(X2730))
| ssPv4(X2730) ),
inference(resolution,[status(thm)],[c239,clause1]) ).
cnf(c1183,plain,
( ~ ssRr(X3510,X3509)
| ~ ssPv2(X3509)
| ~ ssRr(X3511,X3510)
| ssPv1(skf1(skf1(X3511)))
| ssPv1(skf1(X3511))
| ssPv4(X3511) ),
inference(resolution,[status(thm)],[c593,clause1]) ).
cnf(clause36,negated_conjecture,
( ~ ssRr(X449,X452)
| ~ ssPv4(X452)
| ~ ssRr(X453,X449)
| ~ ssRr(X448,X450)
| ~ ssRr(X453,X448)
| ~ ssRr(X453,X451)
| ssPv1(X450)
| ssPv2(X451)
| ssPv1(X453) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c227,plain,
( ~ ssRr(X1254,X1253)
| ~ ssPv4(X1253)
| ~ ssRr(X1252,X1254)
| ~ ssRr(X1251,X1250)
| ~ ssRr(X1252,X1251)
| ssPv1(X1250)
| ssPv2(X1251)
| ssPv1(X1252) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c556,plain,
( ~ ssRr(X2638,X2639)
| ~ ssPv4(X2639)
| ~ ssRr(X2636,X2638)
| ~ ssRr(skf1(X2636),X2637)
| ssPv1(X2637)
| ssPv2(skf1(X2636))
| ssPv1(X2636) ),
inference(resolution,[status(thm)],[c227,clause1]) ).
cnf(c1157,plain,
( ~ ssRr(X3481,X3480)
| ~ ssPv4(X3480)
| ~ ssRr(X3482,X3481)
| ssPv1(skf1(skf1(X3482)))
| ssPv2(skf1(X3482))
| ssPv1(X3482) ),
inference(resolution,[status(thm)],[c556,clause1]) ).
cnf(clause35,negated_conjecture,
( ~ ssRr(X435,X438)
| ~ ssPv4(X438)
| ~ ssRr(X439,X435)
| ~ ssRr(X434,X436)
| ~ ssRr(X439,X434)
| ~ ssRr(X439,X437)
| ssPv1(X436)
| ssPv4(X437)
| ssPv1(X439) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c218,plain,
( ~ ssRr(X1170,X1172)
| ~ ssPv4(X1172)
| ~ ssRr(X1169,X1170)
| ~ ssRr(X1171,X1173)
| ~ ssRr(X1169,X1171)
| ssPv1(X1173)
| ssPv4(X1171)
| ssPv1(X1169) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c528,plain,
( ~ ssRr(X2562,X2563)
| ~ ssPv4(X2563)
| ~ ssRr(X2565,X2562)
| ~ ssRr(skf1(X2565),X2564)
| ssPv1(X2564)
| ssPv4(skf1(X2565))
| ssPv1(X2565) ),
inference(resolution,[status(thm)],[c218,clause1]) ).
cnf(c1133,plain,
( ~ ssRr(X3467,X3468)
| ~ ssPv4(X3468)
| ~ ssRr(X3466,X3467)
| ssPv1(skf1(skf1(X3466)))
| ssPv4(skf1(X3466))
| ssPv1(X3466) ),
inference(resolution,[status(thm)],[c528,clause1]) ).
cnf(c330,plain,
( ~ ssRr(X2074,X2078)
| ~ ssPv4(X2078)
| ~ ssRr(X2075,X2074)
| ~ ssRr(X2076,X2077)
| ~ ssPv1(X2077)
| ~ ssRr(X2075,X2076)
| ~ ssPv1(skf1(X2075))
| ssPv3(X2075) ),
inference(resolution,[status(thm)],[clause47,clause1]) ).
cnf(c932,plain,
( ~ ssRr(X3446,X3445)
| ~ ssPv4(X3445)
| ~ ssRr(X3443,X3446)
| ~ ssRr(X3444,skf1(X3443))
| ~ ssPv1(skf1(X3443))
| ~ ssRr(X3443,X3444)
| ssPv3(X3443) ),
inference(factor,[status(thm)],[c330]) ).
cnf(c1421,plain,
( ~ ssRr(X3451,X3450)
| ~ ssPv4(X3450)
| ~ ssRr(X3452,X3451)
| ~ ssPv1(skf1(X3452))
| ~ ssRr(X3452,X3452)
| ssPv3(X3452) ),
inference(resolution,[status(thm)],[c932,clause1]) ).
cnf(c1419,plain,
( ~ ssRr(X3447,skf1(X3448))
| ~ ssPv4(skf1(X3448))
| ~ ssRr(X3448,X3447)
| ~ ssPv1(skf1(X3448))
| ssPv3(X3448) ),
inference(factor,[status(thm)],[c932]) ).
cnf(c1422,plain,
( ~ ssPv4(skf1(X3449))
| ~ ssRr(X3449,X3449)
| ~ ssPv1(skf1(X3449))
| ssPv3(X3449) ),
inference(resolution,[status(thm)],[c1419,clause1]) ).
cnf(clause34,negated_conjecture,
( ~ ssRr(X420,X423)
| ~ ssPv4(X423)
| ~ ssRr(X424,X420)
| ~ ssRr(X419,X421)
| ~ ssRr(X424,X419)
| ~ ssRr(X424,X422)
| ssPv4(X421)
| ssPv4(X422)
| ssPv1(X424) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c210,plain,
( ~ ssRr(X1088,X1091)
| ~ ssPv4(X1091)
| ~ ssRr(X1089,X1088)
| ~ ssRr(X1090,X1087)
| ~ ssRr(X1089,X1090)
| ssPv4(X1087)
| ssPv4(X1090)
| ssPv1(X1089) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c508,plain,
( ~ ssRr(X2471,X2469)
| ~ ssPv4(X2469)
| ~ ssRr(X2470,X2471)
| ~ ssRr(skf1(X2470),X2468)
| ssPv4(X2468)
| ssPv4(skf1(X2470))
| ssPv1(X2470) ),
inference(resolution,[status(thm)],[c210,clause1]) ).
cnf(c1109,plain,
( ~ ssRr(X3441,X3439)
| ~ ssPv4(X3439)
| ~ ssRr(X3440,X3441)
| ssPv4(skf1(skf1(X3440)))
| ssPv4(skf1(X3440))
| ssPv1(X3440) ),
inference(resolution,[status(thm)],[c508,clause1]) ).
cnf(c335,plain,
( ~ ssRr(X2103,X2104)
| ~ ssPv4(X2104)
| ~ ssRr(X2106,X2103)
| ~ ssRr(X2105,X2107)
| ~ ssPv1(X2107)
| ~ ssRr(X2106,X2105)
| ~ ssPv2(X2103)
| ~ ssPv4(X2106) ),
inference(factor,[status(thm)],[clause48]) ).
cnf(c945,plain,
( ~ ssRr(X3427,X3424)
| ~ ssPv4(X3424)
| ~ ssRr(X3426,X3427)
| ~ ssRr(skf1(X3426),X3425)
| ~ ssPv1(X3425)
| ~ ssPv2(X3427)
| ~ ssPv4(X3426) ),
inference(resolution,[status(thm)],[c335,clause1]) ).
cnf(c1414,plain,
( ~ ssRr(X3432,X3433)
| ~ ssPv4(X3433)
| ~ ssRr(X3434,X3432)
| ~ ssPv1(skf1(skf1(X3434)))
| ~ ssPv2(X3432)
| ~ ssPv4(X3434) ),
inference(resolution,[status(thm)],[c945,clause1]) ).
cnf(c334,plain,
( ~ ssRr(X2091,X2094)
| ~ ssPv4(X2094)
| ~ ssRr(X2091,X2091)
| ~ ssRr(X2093,X2092)
| ~ ssPv1(X2092)
| ~ ssRr(X2091,X2093)
| ~ ssPv2(X2094)
| ~ ssPv4(X2091) ),
inference(factor,[status(thm)],[clause48]) ).
cnf(c939,plain,
( ~ ssRr(X3421,X3420)
| ~ ssPv4(X3420)
| ~ ssRr(X3421,X3421)
| ~ ssRr(skf1(X3421),X3419)
| ~ ssPv1(X3419)
| ~ ssPv2(X3420)
| ~ ssPv4(X3421) ),
inference(resolution,[status(thm)],[c334,clause1]) ).
cnf(c1412,plain,
( ~ ssRr(X3422,X3423)
| ~ ssPv4(X3423)
| ~ ssRr(X3422,X3422)
| ~ ssPv1(skf1(skf1(X3422)))
| ~ ssPv2(X3423)
| ~ ssPv4(X3422) ),
inference(resolution,[status(thm)],[c939,clause1]) ).
cnf(c319,plain,
( ~ ssRr(X1966,X1964)
| ~ ssPv2(X1964)
| ~ ssRr(X1963,X1966)
| ~ ssRr(X1962,X1965)
| ~ ssRr(X1963,X1962)
| ~ ssPv1(X1966)
| ~ ssPv1(X1963)
| ssPv3(X1965) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c883,plain,
( ~ ssRr(X3397,X3395)
| ~ ssPv2(X3395)
| ~ ssRr(X3396,X3397)
| ~ ssRr(skf1(X3396),X3394)
| ~ ssPv1(X3397)
| ~ ssPv1(X3396)
| ssPv3(X3394) ),
inference(resolution,[status(thm)],[c319,clause1]) ).
cnf(c1404,plain,
( ~ ssRr(X3399,X3401)
| ~ ssPv2(X3401)
| ~ ssRr(X3400,X3399)
| ~ ssPv1(X3399)
| ~ ssPv1(X3400)
| ssPv3(skf1(skf1(X3400))) ),
inference(resolution,[status(thm)],[c883,clause1]) ).
cnf(c318,plain,
( ~ ssRr(X1949,X1950)
| ~ ssPv2(X1950)
| ~ ssRr(X1949,X1949)
| ~ ssRr(X1948,X1951)
| ~ ssRr(X1949,X1948)
| ~ ssPv1(X1950)
| ~ ssPv1(X1949)
| ssPv3(X1951) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c874,plain,
( ~ ssRr(X3391,X3389)
| ~ ssPv2(X3389)
| ~ ssRr(X3391,X3391)
| ~ ssRr(skf1(X3391),X3390)
| ~ ssPv1(X3389)
| ~ ssPv1(X3391)
| ssPv3(X3390) ),
inference(resolution,[status(thm)],[c318,clause1]) ).
cnf(c1401,plain,
( ~ ssRr(X3393,X3392)
| ~ ssPv2(X3392)
| ~ ssRr(X3393,X3393)
| ~ ssPv1(X3392)
| ~ ssPv1(X3393)
| ssPv3(skf1(skf1(X3393))) ),
inference(resolution,[status(thm)],[c874,clause1]) ).
cnf(c1402,plain,
( ~ ssRr(X3398,X3398)
| ~ ssPv2(X3398)
| ~ ssPv1(X3398)
| ssPv3(skf1(skf1(X3398))) ),
inference(factor,[status(thm)],[c1401]) ).
cnf(c310,plain,
( ~ ssRr(X1893,X1892)
| ~ ssPv4(X1892)
| ~ ssRr(X1889,X1893)
| ~ ssRr(X1890,X1891)
| ~ ssRr(X1889,X1890)
| ~ ssPv2(X1893)
| ~ ssPv4(X1889)
| ssPv3(X1891) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c853,plain,
( ~ ssRr(X3376,X3375)
| ~ ssPv4(X3375)
| ~ ssRr(X3377,X3376)
| ~ ssRr(skf1(X3377),X3378)
| ~ ssPv2(X3376)
| ~ ssPv4(X3377)
| ssPv3(X3378) ),
inference(resolution,[status(thm)],[c310,clause1]) ).
cnf(c1396,plain,
( ~ ssRr(X3383,X3385)
| ~ ssPv4(X3385)
| ~ ssRr(X3384,X3383)
| ~ ssPv2(X3383)
| ~ ssPv4(X3384)
| ssPv3(skf1(skf1(X3384))) ),
inference(resolution,[status(thm)],[c853,clause1]) ).
cnf(c309,plain,
( ~ ssRr(X1876,X1879)
| ~ ssPv4(X1879)
| ~ ssRr(X1876,X1876)
| ~ ssRr(X1878,X1877)
| ~ ssRr(X1876,X1878)
| ~ ssPv2(X1879)
| ~ ssPv4(X1876)
| ssPv3(X1877) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c844,plain,
( ~ ssRr(X3363,X3362)
| ~ ssPv4(X3362)
| ~ ssRr(X3363,X3363)
| ~ ssRr(skf1(X3363),X3361)
| ~ ssPv2(X3362)
| ~ ssPv4(X3363)
| ssPv3(X3361) ),
inference(resolution,[status(thm)],[c309,clause1]) ).
cnf(c1393,plain,
( ~ ssRr(X3365,X3364)
| ~ ssPv4(X3364)
| ~ ssRr(X3365,X3365)
| ~ ssPv2(X3364)
| ~ ssPv4(X3365)
| ssPv3(skf1(skf1(X3365))) ),
inference(resolution,[status(thm)],[c844,clause1]) ).
cnf(c1394,plain,
( ~ ssRr(X3366,X3366)
| ~ ssPv4(X3366)
| ~ ssPv2(X3366)
| ssPv3(skf1(skf1(X3366))) ),
inference(factor,[status(thm)],[c1393]) ).
cnf(c1086,plain,
( ~ ssRr(X3351,X3349)
| ~ ssPv4(X3349)
| ~ ssRr(X3350,X3351)
| ~ ssRr(X3350,X3352)
| ~ ssPv3(X3352)
| ~ ssRr(X3350,X3350)
| ssPv2(X3350) ),
inference(factor,[status(thm)],[c367]) ).
cnf(c299,plain,
( ~ ssRr(X1819,X1823)
| ~ ssPv1(X1823)
| ~ ssRr(X1821,X1819)
| ~ ssRr(X1822,X1820)
| ~ ssRr(X1821,X1822)
| ~ ssPv4(X1819)
| ssPv2(X1820)
| ssPv3(X1821) ),
inference(factor,[status(thm)],[clause44]) ).
cnf(c819,plain,
( ~ ssRr(X3328,X3329)
| ~ ssPv1(X3329)
| ~ ssRr(X3330,X3328)
| ~ ssRr(skf1(X3330),X3331)
| ~ ssPv4(X3328)
| ssPv2(X3331)
| ssPv3(X3330) ),
inference(resolution,[status(thm)],[c299,clause1]) ).
cnf(c1384,plain,
( ~ ssRr(X3339,X3341)
| ~ ssPv1(X3341)
| ~ ssRr(X3340,X3339)
| ~ ssPv4(X3339)
| ssPv2(skf1(skf1(X3340)))
| ssPv3(X3340) ),
inference(resolution,[status(thm)],[c819,clause1]) ).
cnf(c1068,plain,
( ~ ssRr(X3305,X3307)
| ~ ssPv4(X3307)
| ~ ssRr(X3305,X3305)
| ~ ssRr(X3306,X3304)
| ~ ssPv3(X3304)
| ~ ssRr(X3305,X3306)
| ssPv2(X3305) ),
inference(factor,[status(thm)],[c365]) ).
cnf(c1375,plain,
( ~ ssRr(X3336,X3335)
| ~ ssPv4(X3335)
| ~ ssRr(X3336,X3336)
| ~ ssRr(skf1(X3336),X3334)
| ~ ssPv3(X3334)
| ssPv2(X3336) ),
inference(resolution,[status(thm)],[c1068,clause1]) ).
cnf(c1385,plain,
( ~ ssRr(X3338,X3337)
| ~ ssPv4(X3337)
| ~ ssRr(X3338,X3338)
| ~ ssPv3(skf1(skf1(X3338)))
| ssPv2(X3338) ),
inference(resolution,[status(thm)],[c1375,clause1]) ).
cnf(c1373,plain,
( ~ ssRr(X3322,X3321)
| ~ ssPv4(X3321)
| ~ ssRr(X3322,X3322)
| ~ ssRr(X3322,X3320)
| ~ ssPv3(X3320)
| ssPv2(X3322) ),
inference(factor,[status(thm)],[c1068]) ).
cnf(c1381,plain,
( ~ ssRr(X3333,X3332)
| ~ ssPv4(X3332)
| ~ ssRr(X3333,X3333)
| ~ ssPv3(skf1(X3333))
| ssPv2(X3333) ),
inference(resolution,[status(thm)],[c1373,clause1]) ).
cnf(c1379,plain,
( ~ ssRr(X3323,X3324)
| ~ ssPv4(X3324)
| ~ ssRr(X3323,X3323)
| ~ ssPv3(X3324)
| ssPv2(X3323) ),
inference(factor,[status(thm)],[c1373]) ).
cnf(c1372,plain,
( ~ ssRr(X3310,X3312)
| ~ ssPv4(X3312)
| ~ ssRr(X3310,X3310)
| ~ ssRr(X3312,X3311)
| ~ ssPv3(X3311)
| ssPv2(X3310) ),
inference(factor,[status(thm)],[c1068]) ).
cnf(c1378,plain,
( ~ ssRr(X3318,X3319)
| ~ ssPv4(X3319)
| ~ ssRr(X3318,X3318)
| ~ ssPv3(skf1(X3319))
| ssPv2(X3318) ),
inference(resolution,[status(thm)],[c1372,clause1]) ).
cnf(c294,plain,
( ~ ssRr(X1791,X1790)
| ~ ssPv3(X1790)
| ~ ssRr(X1793,X1791)
| ~ ssRr(X1789,X1792)
| ~ ssPv1(X1792)
| ~ ssRr(X1793,X1789)
| ssPv4(skf1(X1793))
| ssPv4(X1793) ),
inference(resolution,[status(thm)],[clause43,clause1]) ).
cnf(c801,plain,
( ~ ssRr(X3269,X3267)
| ~ ssPv3(X3267)
| ~ ssRr(X3268,X3269)
| ~ ssRr(X3269,X3266)
| ~ ssPv1(X3266)
| ssPv4(skf1(X3268))
| ssPv4(X3268) ),
inference(factor,[status(thm)],[c294]) ).
cnf(c1369,plain,
( ~ ssRr(X3291,X3290)
| ~ ssPv3(X3290)
| ~ ssRr(X3289,X3291)
| ~ ssPv1(skf1(X3291))
| ssPv4(skf1(X3289))
| ssPv4(X3289) ),
inference(resolution,[status(thm)],[c801,clause1]) ).
cnf(c1367,plain,
( ~ ssRr(X3278,X3279)
| ~ ssPv3(X3279)
| ~ ssRr(X3280,X3278)
| ~ ssPv1(X3279)
| ssPv4(skf1(X3280))
| ssPv4(X3280) ),
inference(factor,[status(thm)],[c801]) ).
cnf(c1040,plain,
( ~ ssRr(X3264,X3263)
| ~ ssPv2(X3263)
| ~ ssRr(X3265,X3264)
| ~ ssRr(X3265,X3262)
| ~ ssRr(X3265,X3265)
| ssPv4(X3262)
| ssPv3(X3265) ),
inference(factor,[status(thm)],[c355]) ).
cnf(c291,plain,
( ~ ssRr(X1752,X1750)
| ~ ssPv3(X1750)
| ~ ssRr(X1748,X1752)
| ~ ssRr(X1749,X1751)
| ~ ssPv1(X1751)
| ~ ssRr(X1748,X1749)
| ssPv4(X1752)
| ssPv4(X1748) ),
inference(factor,[status(thm)],[clause43]) ).
cnf(c783,plain,
( ~ ssRr(X3226,X3227)
| ~ ssPv3(X3227)
| ~ ssRr(X3229,X3226)
| ~ ssRr(skf1(X3229),X3228)
| ~ ssPv1(X3228)
| ssPv4(X3226)
| ssPv4(X3229) ),
inference(resolution,[status(thm)],[c291,clause1]) ).
cnf(c1353,plain,
( ~ ssRr(X3260,X3261)
| ~ ssPv3(X3261)
| ~ ssRr(X3259,X3260)
| ~ ssPv1(skf1(skf1(X3259)))
| ssPv4(X3260)
| ssPv4(X3259) ),
inference(resolution,[status(thm)],[c783,clause1]) ).
cnf(c1024,plain,
( ~ ssRr(X3219,X3217)
| ~ ssPv2(X3217)
| ~ ssRr(X3219,X3219)
| ~ ssRr(X3218,X3220)
| ~ ssRr(X3219,X3218)
| ssPv4(X3220)
| ssPv3(X3219) ),
inference(factor,[status(thm)],[c353]) ).
cnf(c1348,plain,
( ~ ssRr(X3255,X3253)
| ~ ssPv2(X3253)
| ~ ssRr(X3255,X3255)
| ~ ssRr(skf1(X3255),X3254)
| ssPv4(X3254)
| ssPv3(X3255) ),
inference(resolution,[status(thm)],[c1024,clause1]) ).
cnf(c1362,plain,
( ~ ssRr(X3257,X3256)
| ~ ssPv2(X3256)
| ~ ssRr(X3257,X3257)
| ssPv4(skf1(skf1(X3257)))
| ssPv3(X3257) ),
inference(resolution,[status(thm)],[c1348,clause1]) ).
cnf(c1346,plain,
( ~ ssRr(X3235,X3236)
| ~ ssPv2(X3236)
| ~ ssRr(X3235,X3235)
| ~ ssRr(X3235,X3237)
| ssPv4(X3237)
| ssPv3(X3235) ),
inference(factor,[status(thm)],[c1024]) ).
cnf(c1357,plain,
( ~ ssRr(X3248,X3247)
| ~ ssPv2(X3247)
| ~ ssRr(X3248,X3248)
| ssPv4(skf1(X3248))
| ssPv3(X3248) ),
inference(resolution,[status(thm)],[c1346,clause1]) ).
cnf(c1355,plain,
( ~ ssRr(X3242,X3243)
| ~ ssPv2(X3243)
| ~ ssRr(X3242,X3242)
| ssPv4(X3243)
| ssPv3(X3242) ),
inference(factor,[status(thm)],[c1346]) ).
cnf(c1345,plain,
( ~ ssRr(X3225,X3223)
| ~ ssPv2(X3223)
| ~ ssRr(X3225,X3225)
| ~ ssRr(X3223,X3224)
| ssPv4(X3224)
| ssPv3(X3225) ),
inference(factor,[status(thm)],[c1024]) ).
cnf(c1351,plain,
( ~ ssRr(X3232,X3233)
| ~ ssPv2(X3233)
| ~ ssRr(X3232,X3232)
| ssPv4(skf1(X3233))
| ssPv3(X3232) ),
inference(resolution,[status(thm)],[c1345,clause1]) ).
cnf(c290,plain,
( ~ ssRr(X1736,X1737)
| ~ ssPv3(X1737)
| ~ ssRr(X1736,X1736)
| ~ ssRr(X1739,X1738)
| ~ ssPv1(X1738)
| ~ ssRr(X1736,X1739)
| ssPv4(X1737)
| ssPv4(X1736) ),
inference(factor,[status(thm)],[clause43]) ).
cnf(c776,plain,
( ~ ssRr(X3210,X3208)
| ~ ssPv3(X3208)
| ~ ssRr(X3210,X3210)
| ~ ssRr(skf1(X3210),X3209)
| ~ ssPv1(X3209)
| ssPv4(X3208)
| ssPv4(X3210) ),
inference(resolution,[status(thm)],[c290,clause1]) ).
cnf(c1344,plain,
( ~ ssRr(X3211,X3212)
| ~ ssPv3(X3212)
| ~ ssRr(X3211,X3211)
| ~ ssPv1(skf1(skf1(X3211)))
| ssPv4(X3212)
| ssPv4(X3211) ),
inference(resolution,[status(thm)],[c776,clause1]) ).
cnf(c992,plain,
( ~ ssRr(X3193,X3194)
| ~ ssPv1(X3194)
| ~ ssRr(X3192,X3193)
| ~ ssRr(X3192,X3195)
| ~ ssRr(X3192,X3192)
| ssPv4(X3195)
| ssPv3(X3192) ),
inference(factor,[status(thm)],[c345]) ).
cnf(c282,plain,
( ~ ssRr(X1671,X1672)
| ~ ssPv3(X1672)
| ~ ssRr(X1670,X1671)
| ~ ssRr(X1669,X1668)
| ~ ssRr(X1670,X1669)
| ~ ssPv2(X1671)
| ssPv1(X1668)
| ssPv4(X1670) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c751,plain,
( ~ ssRr(X3175,X3178)
| ~ ssPv3(X3178)
| ~ ssRr(X3176,X3175)
| ~ ssRr(skf1(X3176),X3177)
| ~ ssPv2(X3175)
| ssPv1(X3177)
| ssPv4(X3176) ),
inference(resolution,[status(thm)],[c282,clause1]) ).
cnf(c1336,plain,
( ~ ssRr(X3184,X3182)
| ~ ssPv3(X3182)
| ~ ssRr(X3183,X3184)
| ~ ssPv2(X3184)
| ssPv1(skf1(skf1(X3183)))
| ssPv4(X3183) ),
inference(resolution,[status(thm)],[c751,clause1]) ).
cnf(c281,plain,
( ~ ssRr(X1659,X1656)
| ~ ssPv3(X1656)
| ~ ssRr(X1659,X1659)
| ~ ssRr(X1658,X1657)
| ~ ssRr(X1659,X1658)
| ~ ssPv2(X1656)
| ssPv1(X1657)
| ssPv4(X1659) ),
inference(factor,[status(thm)],[clause42]) ).
cnf(c746,plain,
( ~ ssRr(X3165,X3164)
| ~ ssPv3(X3164)
| ~ ssRr(X3165,X3165)
| ~ ssRr(skf1(X3165),X3163)
| ~ ssPv2(X3164)
| ssPv1(X3163)
| ssPv4(X3165) ),
inference(resolution,[status(thm)],[c281,clause1]) ).
cnf(c1330,plain,
( ~ ssRr(X3174,X3173)
| ~ ssPv3(X3173)
| ~ ssRr(X3174,X3174)
| ~ ssPv2(X3173)
| ssPv1(skf1(skf1(X3174)))
| ssPv4(X3174) ),
inference(resolution,[status(thm)],[c746,clause1]) ).
cnf(c1334,plain,
( ~ ssRr(X3179,X3179)
| ~ ssPv3(X3179)
| ~ ssPv2(X3179)
| ssPv1(skf1(skf1(X3179)))
| ssPv4(X3179) ),
inference(factor,[status(thm)],[c1330]) ).
cnf(c274,plain,
( ~ ssRr(X1643,X1640)
| ~ ssPv4(X1640)
| ~ ssRr(X1642,X1643)
| ~ ssRr(X1644,X1641)
| ~ ssRr(X1642,X1644)
| ssPv3(X1641)
| ssPv1(skf1(X1642))
| ssPv2(X1642) ),
inference(resolution,[status(thm)],[clause41,clause1]) ).
cnf(c735,plain,
( ~ ssRr(X3127,X3128)
| ~ ssPv4(X3128)
| ~ ssRr(X3129,X3127)
| ~ ssRr(X3127,X3126)
| ssPv3(X3126)
| ssPv1(skf1(X3129))
| ssPv2(X3129) ),
inference(factor,[status(thm)],[c274]) ).
cnf(c1320,plain,
( ~ ssRr(X3171,X3169)
| ~ ssPv4(X3169)
| ~ ssRr(X3170,X3171)
| ssPv3(skf1(X3171))
| ssPv1(skf1(X3170))
| ssPv2(X3170) ),
inference(resolution,[status(thm)],[c735,clause1]) ).
cnf(c734,plain,
( ~ ssRr(X3117,X3116)
| ~ ssPv4(X3116)
| ~ ssRr(X3117,X3117)
| ~ ssRr(X3116,X3115)
| ssPv3(X3115)
| ssPv1(skf1(X3117))
| ssPv2(X3117) ),
inference(factor,[status(thm)],[c274]) ).
cnf(c1313,plain,
( ~ ssRr(X3166,X3167)
| ~ ssPv4(X3167)
| ~ ssRr(X3166,X3166)
| ssPv3(skf1(X3167))
| ssPv1(skf1(X3166))
| ssPv2(X3166) ),
inference(resolution,[status(thm)],[c734,clause1]) ).
cnf(c976,plain,
( ~ ssRr(X3104,X3106)
| ~ ssPv1(X3106)
| ~ ssRr(X3104,X3104)
| ~ ssRr(X3105,X3107)
| ~ ssRr(X3104,X3105)
| ssPv4(X3107)
| ssPv3(X3104) ),
inference(factor,[status(thm)],[c343]) ).
cnf(c1307,plain,
( ~ ssRr(X3159,X3158)
| ~ ssPv1(X3158)
| ~ ssRr(X3159,X3159)
| ~ ssRr(skf1(X3159),X3157)
| ssPv4(X3157)
| ssPv3(X3159) ),
inference(resolution,[status(thm)],[c976,clause1]) ).
cnf(c1328,plain,
( ~ ssRr(X3160,X3161)
| ~ ssPv1(X3161)
| ~ ssRr(X3160,X3160)
| ssPv4(skf1(skf1(X3160)))
| ssPv3(X3160) ),
inference(resolution,[status(thm)],[c1307,clause1]) ).
cnf(c1319,plain,
( ~ ssRr(X3149,X3148)
| ~ ssPv4(X3148)
| ~ ssRr(X3149,X3149)
| ssPv3(X3149)
| ssPv1(skf1(X3149))
| ssPv2(X3149) ),
inference(factor,[status(thm)],[c735]) ).
cnf(c1318,plain,
( ~ ssRr(X3144,X3142)
| ~ ssPv4(X3142)
| ~ ssRr(X3143,X3144)
| ssPv3(X3142)
| ssPv1(skf1(X3143))
| ssPv2(X3143) ),
inference(factor,[status(thm)],[c735]) ).
cnf(c736,plain,
( ~ ssRr(X3138,X3139)
| ~ ssPv4(X3139)
| ~ ssRr(X3140,X3138)
| ~ ssRr(X3140,X3140)
| ssPv3(X3140)
| ssPv1(skf1(X3140))
| ssPv2(X3140) ),
inference(factor,[status(thm)],[c274]) ).
cnf(c1305,plain,
( ~ ssRr(X3123,X3125)
| ~ ssPv1(X3125)
| ~ ssRr(X3123,X3123)
| ~ ssRr(X3123,X3124)
| ssPv4(X3124)
| ssPv3(X3123) ),
inference(factor,[status(thm)],[c976]) ).
cnf(c1317,plain,
( ~ ssRr(X3136,X3135)
| ~ ssPv1(X3135)
| ~ ssRr(X3136,X3136)
| ssPv4(skf1(X3136))
| ssPv3(X3136) ),
inference(resolution,[status(thm)],[c1305,clause1]) ).
cnf(c1315,plain,
( ~ ssRr(X3130,X3131)
| ~ ssPv1(X3131)
| ~ ssRr(X3130,X3130)
| ssPv4(X3131)
| ssPv3(X3130) ),
inference(factor,[status(thm)],[c1305]) ).
cnf(c1304,plain,
( ~ ssRr(X3112,X3110)
| ~ ssPv1(X3110)
| ~ ssRr(X3112,X3112)
| ~ ssRr(X3110,X3111)
| ssPv4(X3111)
| ssPv3(X3112) ),
inference(factor,[status(thm)],[c976]) ).
cnf(c1310,plain,
( ~ ssRr(X3120,X3121)
| ~ ssPv1(X3121)
| ~ ssRr(X3120,X3120)
| ssPv4(skf1(X3121))
| ssPv3(X3120) ),
inference(resolution,[status(thm)],[c1304,clause1]) ).
cnf(c1311,plain,
( ~ ssRr(X3118,X3118)
| ~ ssPv4(X3118)
| ssPv3(X3118)
| ssPv1(skf1(X3118))
| ssPv2(X3118) ),
inference(factor,[status(thm)],[c734]) ).
cnf(c271,plain,
( ~ ssRr(X1591,X1592)
| ~ ssPv4(X1592)
| ~ ssRr(X1594,X1591)
| ~ ssRr(X1595,X1593)
| ~ ssRr(X1594,X1595)
| ssPv3(X1593)
| ssPv1(X1591)
| ssPv2(X1594) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c716,plain,
( ~ ssRr(X3088,X3087)
| ~ ssPv4(X3087)
| ~ ssRr(X3090,X3088)
| ~ ssRr(skf1(X3090),X3089)
| ssPv3(X3089)
| ssPv1(X3088)
| ssPv2(X3090) ),
inference(resolution,[status(thm)],[c271,clause1]) ).
cnf(c1299,plain,
( ~ ssRr(X3094,X3096)
| ~ ssPv4(X3096)
| ~ ssRr(X3095,X3094)
| ssPv3(skf1(skf1(X3095)))
| ssPv1(X3094)
| ssPv2(X3095) ),
inference(resolution,[status(thm)],[c716,clause1]) ).
cnf(c270,plain,
( ~ ssRr(X1579,X1578)
| ~ ssPv4(X1578)
| ~ ssRr(X1579,X1579)
| ~ ssRr(X1580,X1581)
| ~ ssRr(X1579,X1580)
| ssPv3(X1581)
| ssPv1(X1578)
| ssPv2(X1579) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c710,plain,
( ~ ssRr(X3076,X3074)
| ~ ssPv4(X3074)
| ~ ssRr(X3076,X3076)
| ~ ssRr(skf1(X3076),X3075)
| ssPv3(X3075)
| ssPv1(X3074)
| ssPv2(X3076) ),
inference(resolution,[status(thm)],[c270,clause1]) ).
cnf(c1294,plain,
( ~ ssRr(X3086,X3085)
| ~ ssPv4(X3085)
| ~ ssRr(X3086,X3086)
| ssPv3(skf1(skf1(X3086)))
| ssPv1(X3085)
| ssPv2(X3086) ),
inference(resolution,[status(thm)],[c710,clause1]) ).
cnf(c266,plain,
( ~ ssRr(X1557,X1561)
| ~ ssRr(X1560,X1557)
| ~ ssRr(X1558,X1559)
| ~ ssRr(X1560,X1558)
| ~ ssPv4(X1560)
| ssPv4(X1561)
| ssPv3(X1559)
| ssPv4(skf1(X1560)) ),
inference(resolution,[status(thm)],[clause40,clause1]) ).
cnf(c701,plain,
( ~ ssRr(X3036,X3037)
| ~ ssRr(X3034,X3036)
| ~ ssRr(X3036,X3035)
| ~ ssPv4(X3034)
| ssPv4(X3037)
| ssPv3(X3035)
| ssPv4(skf1(X3034)) ),
inference(factor,[status(thm)],[c266]) ).
cnf(c1285,plain,
( ~ ssRr(X3079,X3077)
| ~ ssRr(X3078,X3079)
| ~ ssPv4(X3078)
| ssPv4(X3077)
| ssPv3(skf1(X3079))
| ssPv4(skf1(X3078)) ),
inference(resolution,[status(thm)],[c701,clause1]) ).
cnf(c263,plain,
( ~ ssRr(X1518,X1519)
| ~ ssRr(X1515,X1518)
| ~ ssRr(X1516,X1517)
| ~ ssRr(X1515,X1516)
| ~ ssPv4(X1515)
| ssPv4(X1519)
| ssPv3(X1517)
| ssPv4(X1518) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c685,plain,
( ~ ssRr(X2997,X2996)
| ~ ssRr(X2995,X2997)
| ~ ssRr(skf1(X2995),X2994)
| ~ ssPv4(X2995)
| ssPv4(X2996)
| ssPv3(X2994)
| ssPv4(X2997) ),
inference(resolution,[status(thm)],[c263,clause1]) ).
cnf(c1275,plain,
( ~ ssRr(X3067,X3068)
| ~ ssRr(X3066,X3067)
| ~ ssPv4(X3066)
| ssPv4(X3068)
| ssPv3(skf1(skf1(X3066)))
| ssPv4(X3067) ),
inference(resolution,[status(thm)],[c685,clause1]) ).
cnf(c258,plain,
( ~ ssRr(X1488,X1490)
| ~ ssPv3(X1490)
| ~ ssRr(X1489,X1488)
| ~ ssRr(X1486,X1487)
| ~ ssRr(X1489,X1486)
| ssPv2(X1487)
| ssPv4(skf1(X1489))
| ssPv4(X1489) ),
inference(resolution,[status(thm)],[clause39,clause1]) ).
cnf(c665,plain,
( ~ ssRr(X2958,X2959)
| ~ ssPv3(X2959)
| ~ ssRr(X2960,X2958)
| ~ ssRr(X2958,X2961)
| ssPv2(X2961)
| ssPv4(skf1(X2960))
| ssPv4(X2960) ),
inference(factor,[status(thm)],[c258]) ).
cnf(c1265,plain,
( ~ ssRr(X3057,X3058)
| ~ ssPv3(X3058)
| ~ ssRr(X3056,X3057)
| ssPv2(skf1(X3057))
| ssPv4(skf1(X3056))
| ssPv4(X3056) ),
inference(resolution,[status(thm)],[c665,clause1]) ).
cnf(c702,plain,
( ~ ssRr(X3049,X3050)
| ~ ssRr(X3048,X3049)
| ~ ssRr(X3048,X3048)
| ~ ssPv4(X3048)
| ssPv4(X3050)
| ssPv3(X3048)
| ssPv4(skf1(X3048)) ),
inference(factor,[status(thm)],[c266]) ).
cnf(c1283,plain,
( ~ ssRr(X3039,X3040)
| ~ ssRr(X3038,X3039)
| ~ ssPv4(X3038)
| ssPv4(X3040)
| ssPv3(X3040)
| ssPv4(skf1(X3038)) ),
inference(factor,[status(thm)],[c701]) ).
cnf(c255,plain,
( ~ ssRr(X1448,X1446)
| ~ ssPv3(X1446)
| ~ ssRr(X1447,X1448)
| ~ ssRr(X1444,X1445)
| ~ ssRr(X1447,X1444)
| ssPv2(X1445)
| ssPv4(X1448)
| ssPv4(X1447) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c647,plain,
( ~ ssRr(X2921,X2920)
| ~ ssPv3(X2920)
| ~ ssRr(X2922,X2921)
| ~ ssRr(skf1(X2922),X2919)
| ssPv2(X2919)
| ssPv4(X2921)
| ssPv4(X2922) ),
inference(resolution,[status(thm)],[c255,clause1]) ).
cnf(c1247,plain,
( ~ ssRr(X3026,X3024)
| ~ ssPv3(X3024)
| ~ ssRr(X3025,X3026)
| ssPv2(skf1(skf1(X3025)))
| ssPv4(X3026)
| ssPv4(X3025) ),
inference(resolution,[status(thm)],[c647,clause1]) ).
cnf(c254,plain,
( ~ ssRr(X1432,X1434)
| ~ ssPv3(X1434)
| ~ ssRr(X1432,X1432)
| ~ ssRr(X1431,X1433)
| ~ ssRr(X1432,X1431)
| ssPv2(X1433)
| ssPv4(X1434)
| ssPv4(X1432) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c641,plain,
( ~ ssRr(X2909,X2907)
| ~ ssPv3(X2907)
| ~ ssRr(X2909,X2909)
| ~ ssRr(skf1(X2909),X2908)
| ssPv2(X2908)
| ssPv4(X2907)
| ssPv4(X2909) ),
inference(resolution,[status(thm)],[c254,clause1]) ).
cnf(c1242,plain,
( ~ ssRr(X3017,X3016)
| ~ ssPv3(X3016)
| ~ ssRr(X3017,X3017)
| ssPv2(skf1(skf1(X3017)))
| ssPv4(X3016)
| ssPv4(X3017) ),
inference(resolution,[status(thm)],[c641,clause1]) ).
cnf(c1280,plain,
( ~ ssRr(X3018,X3018)
| ~ ssPv3(X3018)
| ssPv2(skf1(skf1(X3018)))
| ssPv4(X3018) ),
inference(factor,[status(thm)],[c1242]) ).
cnf(c248,plain,
( ~ ssRr(X1414,X1415)
| ~ ssPv1(X1415)
| ~ ssRr(X1417,X1414)
| ~ ssRr(X1416,X1418)
| ~ ssRr(X1417,X1416)
| ssPv1(X1418)
| ssPv3(skf1(X1417))
| ssPv3(X1417) ),
inference(resolution,[status(thm)],[clause38,clause1]) ).
cnf(c635,plain,
( ~ ssRr(X2862,X2865)
| ~ ssPv1(X2865)
| ~ ssRr(X2864,X2862)
| ~ ssRr(X2862,X2863)
| ssPv1(X2863)
| ssPv3(skf1(X2864))
| ssPv3(X2864) ),
inference(factor,[status(thm)],[c248]) ).
cnf(c1233,plain,
( ~ ssRr(X3006,X3004)
| ~ ssPv1(X3004)
| ~ ssRr(X3005,X3006)
| ssPv1(skf1(X3006))
| ssPv3(skf1(X3005))
| ssPv3(X3005) ),
inference(resolution,[status(thm)],[c635,clause1]) ).
cnf(c1069,plain,
( ~ ssRr(X2845,X2847)
| ~ ssPv4(X2847)
| ~ ssRr(X2844,X2845)
| ~ ssRr(X2845,X2846)
| ~ ssPv3(X2846)
| ssPv2(X2846)
| ssPv2(X2844) ),
inference(factor,[status(thm)],[c365]) ).
cnf(c1223,plain,
( ~ ssRr(X2855,X2853)
| ~ ssPv4(X2853)
| ~ ssRr(X2854,X2855)
| ~ ssPv3(X2853)
| ssPv2(X2853)
| ssPv2(X2854) ),
inference(factor,[status(thm)],[c1069]) ).
cnf(c1227,plain,
( ~ ssRr(skf1(X2858),X2857)
| ~ ssPv4(X2857)
| ~ ssPv3(X2857)
| ssPv2(X2857)
| ssPv2(X2858) ),
inference(resolution,[status(thm)],[c1223,clause1]) ).
cnf(c1228,plain,
( ~ ssPv4(skf1(skf1(X3003)))
| ~ ssPv3(skf1(skf1(X3003)))
| ssPv2(skf1(skf1(X3003)))
| ssPv2(X3003) ),
inference(resolution,[status(thm)],[c1227,clause1]) ).
cnf(c1225,plain,
( ~ ssRr(X3002,X3000)
| ~ ssPv4(X3000)
| ~ ssRr(X3001,X3002)
| ~ ssPv3(skf1(X3002))
| ssPv2(skf1(X3002))
| ssPv2(X3001) ),
inference(resolution,[status(thm)],[c1069,clause1]) ).
cnf(c245,plain,
( ~ ssRr(X1377,X1373)
| ~ ssPv1(X1373)
| ~ ssRr(X1375,X1377)
| ~ ssRr(X1374,X1376)
| ~ ssRr(X1375,X1374)
| ssPv1(X1376)
| ssPv3(X1377)
| ssPv3(X1375) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c614,plain,
( ~ ssRr(X2820,X2819)
| ~ ssPv1(X2819)
| ~ ssRr(X2818,X2820)
| ~ ssRr(skf1(X2818),X2817)
| ssPv1(X2817)
| ssPv3(X2820)
| ssPv3(X2818) ),
inference(resolution,[status(thm)],[c245,clause1]) ).
cnf(c1214,plain,
( ~ ssRr(X2990,X2989)
| ~ ssPv1(X2989)
| ~ ssRr(X2991,X2990)
| ssPv1(skf1(skf1(X2991)))
| ssPv3(X2990)
| ssPv3(X2991) ),
inference(resolution,[status(thm)],[c614,clause1]) ).
cnf(c244,plain,
( ~ ssRr(X1358,X1360)
| ~ ssPv1(X1360)
| ~ ssRr(X1358,X1358)
| ~ ssRr(X1357,X1359)
| ~ ssRr(X1358,X1357)
| ssPv1(X1359)
| ssPv3(X1360)
| ssPv3(X1358) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c605,plain,
( ~ ssRr(X2802,X2803)
| ~ ssPv1(X2803)
| ~ ssRr(X2802,X2802)
| ~ ssRr(skf1(X2802),X2801)
| ssPv1(X2801)
| ssPv3(X2803)
| ssPv3(X2802) ),
inference(resolution,[status(thm)],[c244,clause1]) ).
cnf(c1207,plain,
( ~ ssRr(X2986,X2987)
| ~ ssPv1(X2987)
| ~ ssRr(X2986,X2986)
| ssPv1(skf1(skf1(X2986)))
| ssPv3(X2987)
| ssPv3(X2986) ),
inference(resolution,[status(thm)],[c605,clause1]) ).
cnf(c1271,plain,
( ~ ssRr(X2988,X2988)
| ~ ssPv1(X2988)
| ssPv1(skf1(skf1(X2988)))
| ssPv3(X2988) ),
inference(factor,[status(thm)],[c1207]) ).
cnf(c1201,plain,
( ~ ssRr(X2795,X2797)
| ~ ssPv2(X2797)
| ~ ssRr(X2796,X2795)
| ssPv4(X2797)
| ssPv3(X2797)
| ssPv3(X2796) ),
inference(factor,[status(thm)],[c1025]) ).
cnf(c1205,plain,
( ~ ssRr(skf1(X2800),X2799)
| ~ ssPv2(X2799)
| ssPv4(X2799)
| ssPv3(X2799)
| ssPv3(X2800) ),
inference(resolution,[status(thm)],[c1201,clause1]) ).
cnf(c1206,plain,
( ~ ssPv2(skf1(skf1(X2981)))
| ssPv4(skf1(skf1(X2981)))
| ssPv3(skf1(skf1(X2981)))
| ssPv3(X2981) ),
inference(resolution,[status(thm)],[c1205,clause1]) ).
cnf(c1263,plain,
( ~ ssRr(X2964,X2963)
| ~ ssPv3(X2963)
| ~ ssRr(X2965,X2964)
| ssPv2(X2963)
| ssPv4(skf1(X2965))
| ssPv4(X2965) ),
inference(factor,[status(thm)],[c665]) ).
cnf(c240,plain,
( ~ ssRr(X1341,X1342)
| ~ ssPv2(X1342)
| ~ ssRr(X1343,X1341)
| ~ ssRr(X1344,X1340)
| ~ ssRr(X1343,X1344)
| ssPv1(X1340)
| ssPv1(skf1(X1343))
| ssPv4(X1343) ),
inference(resolution,[status(thm)],[clause37,clause1]) ).
cnf(c597,plain,
( ~ ssRr(X2760,X2759)
| ~ ssPv2(X2759)
| ~ ssRr(X2761,X2760)
| ~ ssRr(X2760,X2762)
| ssPv1(X2762)
| ssPv1(skf1(X2761))
| ssPv4(X2761) ),
inference(factor,[status(thm)],[c240]) ).
cnf(c1194,plain,
( ~ ssRr(X2956,X2955)
| ~ ssPv2(X2955)
| ~ ssRr(X2957,X2956)
| ssPv1(skf1(X2956))
| ssPv1(skf1(X2957))
| ssPv4(X2957) ),
inference(resolution,[status(thm)],[c597,clause1]) ).
cnf(c1176,plain,
( ~ ssRr(X2722,X2724)
| ~ ssPv1(X2724)
| ~ ssRr(X2723,X2722)
| ssPv4(X2724)
| ssPv3(X2724)
| ssPv3(X2723) ),
inference(factor,[status(thm)],[c977]) ).
cnf(c1180,plain,
( ~ ssRr(skf1(X2726),X2727)
| ~ ssPv1(X2727)
| ssPv4(X2727)
| ssPv3(X2727)
| ssPv3(X2726) ),
inference(resolution,[status(thm)],[c1176,clause1]) ).
cnf(c1181,plain,
( ~ ssPv1(skf1(skf1(X2953)))
| ssPv4(skf1(skf1(X2953)))
| ssPv3(skf1(skf1(X2953)))
| ssPv3(X2953) ),
inference(resolution,[status(thm)],[c1180,clause1]) ).
cnf(c237,plain,
( ~ ssRr(X1300,X1301)
| ~ ssPv2(X1301)
| ~ ssRr(X1299,X1300)
| ~ ssRr(X1302,X1298)
| ~ ssRr(X1299,X1302)
| ssPv1(X1298)
| ssPv1(X1300)
| ssPv4(X1299) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c579,plain,
( ~ ssRr(X2712,X2715)
| ~ ssPv2(X2715)
| ~ ssRr(X2714,X2712)
| ~ ssRr(skf1(X2714),X2713)
| ssPv1(X2713)
| ssPv1(X2712)
| ssPv4(X2714) ),
inference(resolution,[status(thm)],[c237,clause1]) ).
cnf(c1175,plain,
( ~ ssRr(X2944,X2943)
| ~ ssPv2(X2943)
| ~ ssRr(X2942,X2944)
| ssPv1(skf1(skf1(X2942)))
| ssPv1(X2944)
| ssPv4(X2942) ),
inference(resolution,[status(thm)],[c579,clause1]) ).
cnf(c228,plain,
( ~ ssRr(X1274,X1272)
| ~ ssPv4(X1272)
| ~ ssRr(X1273,X1274)
| ~ ssRr(X1275,X1271)
| ~ ssRr(X1273,X1275)
| ssPv1(X1271)
| ssPv2(skf1(X1273))
| ssPv1(X1273) ),
inference(resolution,[status(thm)],[clause36,clause1]) ).
cnf(c561,plain,
( ~ ssRr(X2666,X2668)
| ~ ssPv4(X2668)
| ~ ssRr(X2665,X2666)
| ~ ssRr(X2666,X2667)
| ssPv1(X2667)
| ssPv2(skf1(X2665))
| ssPv1(X2665) ),
inference(factor,[status(thm)],[c228]) ).
cnf(c1168,plain,
( ~ ssRr(X2933,X2931)
| ~ ssPv4(X2931)
| ~ ssRr(X2932,X2933)
| ssPv1(skf1(X2933))
| ssPv2(skf1(X2932))
| ssPv1(X2932) ),
inference(resolution,[status(thm)],[c561,clause1]) ).
cnf(c225,plain,
( ~ ssRr(X1221,X1223)
| ~ ssPv4(X1223)
| ~ ssRr(X1222,X1221)
| ~ ssRr(X1224,X1220)
| ~ ssRr(X1222,X1224)
| ssPv1(X1220)
| ssPv2(X1221)
| ssPv1(X1222) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c545,plain,
( ~ ssRr(X2626,X2623)
| ~ ssPv4(X2623)
| ~ ssRr(X2624,X2626)
| ~ ssRr(skf1(X2624),X2625)
| ssPv1(X2625)
| ssPv2(X2626)
| ssPv1(X2624) ),
inference(resolution,[status(thm)],[c225,clause1]) ).
cnf(c1152,plain,
( ~ ssRr(X2928,X2927)
| ~ ssPv4(X2927)
| ~ ssRr(X2929,X2928)
| ssPv1(skf1(skf1(X2929)))
| ssPv2(X2928)
| ssPv1(X2929) ),
inference(resolution,[status(thm)],[c545,clause1]) ).
cnf(c219,plain,
( ~ ssRr(X1185,X1187)
| ~ ssPv4(X1187)
| ~ ssRr(X1189,X1185)
| ~ ssRr(X1186,X1188)
| ~ ssRr(X1189,X1186)
| ssPv1(X1188)
| ssPv4(skf1(X1189))
| ssPv1(X1189) ),
inference(resolution,[status(thm)],[clause35,clause1]) ).
cnf(c532,plain,
( ~ ssRr(X2597,X2596)
| ~ ssPv4(X2596)
| ~ ssRr(X2595,X2597)
| ~ ssRr(X2597,X2598)
| ssPv1(X2598)
| ssPv4(skf1(X2595))
| ssPv1(X2595) ),
inference(factor,[status(thm)],[c219]) ).
cnf(c1142,plain,
( ~ ssRr(X2924,X2923)
| ~ ssPv4(X2923)
| ~ ssRr(X2925,X2924)
| ssPv1(skf1(X2924))
| ssPv4(skf1(X2925))
| ssPv1(X2925) ),
inference(resolution,[status(thm)],[c532,clause1]) ).
cnf(c216,plain,
( ~ ssRr(X1137,X1138)
| ~ ssPv4(X1138)
| ~ ssRr(X1135,X1137)
| ~ ssRr(X1136,X1139)
| ~ ssRr(X1135,X1136)
| ssPv1(X1139)
| ssPv4(X1137)
| ssPv1(X1135) ),
inference(factor,[status(thm)],[clause35]) ).
cnf(c522,plain,
( ~ ssRr(X2547,X2548)
| ~ ssPv4(X2548)
| ~ ssRr(X2549,X2547)
| ~ ssRr(skf1(X2549),X2546)
| ssPv1(X2546)
| ssPv4(X2547)
| ssPv1(X2549) ),
inference(resolution,[status(thm)],[c216,clause1]) ).
cnf(c1130,plain,
( ~ ssRr(X2915,X2917)
| ~ ssPv4(X2917)
| ~ ssRr(X2916,X2915)
| ssPv1(skf1(skf1(X2916)))
| ssPv4(X2915)
| ssPv1(X2916) ),
inference(resolution,[status(thm)],[c522,clause1]) ).
cnf(c320,plain,
( ~ ssRr(X1978,X1979)
| ~ ssPv2(X1979)
| ~ ssRr(X1980,X1978)
| ~ ssRr(X1980,X1981)
| ~ ssRr(X1980,X1980)
| ~ ssPv1(X1981)
| ~ ssPv1(X1980)
| ssPv3(X1981) ),
inference(factor,[status(thm)],[clause46]) ).
cnf(c891,plain,
( ~ ssRr(X2532,X2534)
| ~ ssPv2(X2534)
| ~ ssRr(X2532,X2532)
| ~ ssRr(X2532,X2533)
| ~ ssPv1(X2533)
| ~ ssPv1(X2532)
| ssPv3(X2533) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c1128,plain,
( ~ ssRr(X2913,X2914)
| ~ ssPv2(X2914)
| ~ ssRr(X2913,X2913)
| ~ ssPv1(skf1(X2913))
| ~ ssPv1(X2913)
| ssPv3(skf1(X2913)) ),
inference(resolution,[status(thm)],[c891,clause1]) ).
cnf(c881,plain,
( ~ ssRr(X2497,X2498)
| ~ ssPv2(X2498)
| ~ ssRr(X2499,X2497)
| ~ ssRr(X2497,X2496)
| ~ ssPv1(X2497)
| ~ ssPv1(X2499)
| ssPv3(X2496) ),
inference(factor,[status(thm)],[c319]) ).
cnf(c1117,plain,
( ~ ssRr(X2513,X2512)
| ~ ssPv2(X2512)
| ~ ssRr(X2514,X2513)
| ~ ssPv1(X2513)
| ~ ssPv1(X2514)
| ssPv3(skf1(X2513)) ),
inference(resolution,[status(thm)],[c881,clause1]) ).
cnf(c1125,plain,
( ~ ssRr(skf1(X2911),X2910)
| ~ ssPv2(X2910)
| ~ ssPv1(skf1(X2911))
| ~ ssPv1(X2911)
| ssPv3(skf1(skf1(X2911))) ),
inference(resolution,[status(thm)],[c1117,clause1]) ).
cnf(c211,plain,
( ~ ssRr(X1106,X1107)
| ~ ssPv4(X1107)
| ~ ssRr(X1105,X1106)
| ~ ssRr(X1104,X1103)
| ~ ssRr(X1105,X1104)
| ssPv4(X1103)
| ssPv4(skf1(X1105))
| ssPv1(X1105) ),
inference(resolution,[status(thm)],[clause34,clause1]) ).
cnf(c512,plain,
( ~ ssRr(X2500,X2501)
| ~ ssPv4(X2501)
| ~ ssRr(X2502,X2500)
| ~ ssRr(X2500,X2503)
| ssPv4(X2503)
| ssPv4(skf1(X2502))
| ssPv1(X2502) ),
inference(factor,[status(thm)],[c211]) ).
cnf(c1120,plain,
( ~ ssRr(X2905,X2903)
| ~ ssPv4(X2903)
| ~ ssRr(X2904,X2905)
| ssPv4(skf1(X2905))
| ssPv4(skf1(X2904))
| ssPv1(X2904) ),
inference(resolution,[status(thm)],[c512,clause1]) ).
cnf(c208,plain,
( ~ ssRr(X1061,X1062)
| ~ ssPv4(X1062)
| ~ ssRr(X1060,X1061)
| ~ ssRr(X1059,X1058)
| ~ ssRr(X1060,X1059)
| ssPv4(X1058)
| ssPv4(X1061)
| ssPv1(X1060) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c497,plain,
( ~ ssRr(X2453,X2452)
| ~ ssPv4(X2452)
| ~ ssRr(X2455,X2453)
| ~ ssRr(skf1(X2455),X2454)
| ssPv4(X2454)
| ssPv4(X2453)
| ssPv1(X2455) ),
inference(resolution,[status(thm)],[c208,clause1]) ).
cnf(c1107,plain,
( ~ ssRr(X2901,X2899)
| ~ ssPv4(X2899)
| ~ ssRr(X2900,X2901)
| ssPv4(skf1(skf1(X2900)))
| ssPv4(X2901)
| ssPv1(X2900) ),
inference(resolution,[status(thm)],[c497,clause1]) ).
cnf(c851,plain,
( ~ ssRr(X2417,X2415)
| ~ ssPv4(X2415)
| ~ ssRr(X2416,X2417)
| ~ ssRr(X2417,X2418)
| ~ ssPv2(X2417)
| ~ ssPv4(X2416)
| ssPv3(X2418) ),
inference(factor,[status(thm)],[c310]) ).
cnf(c1091,plain,
( ~ ssRr(X2445,X2444)
| ~ ssPv4(X2444)
| ~ ssRr(X2446,X2445)
| ~ ssPv2(X2445)
| ~ ssPv4(X2446)
| ssPv3(skf1(X2445)) ),
inference(resolution,[status(thm)],[c851,clause1]) ).
cnf(c1103,plain,
( ~ ssRr(skf1(X2893),X2892)
| ~ ssPv4(X2892)
| ~ ssPv2(skf1(X2893))
| ~ ssPv4(X2893)
| ssPv3(skf1(skf1(X2893))) ),
inference(resolution,[status(thm)],[c1091,clause1]) ).
cnf(c1083,plain,
( ~ ssRr(X2881,X2880)
| ~ ssPv4(X2880)
| ~ ssRr(X2882,X2881)
| ~ ssRr(X2881,X2883)
| ~ ssPv3(X2883)
| ssPv2(X2880)
| ssPv2(X2882) ),
inference(factor,[status(thm)],[c367]) ).
cnf(c1236,plain,
( ~ ssRr(X2890,X2891)
| ~ ssPv4(X2891)
| ~ ssRr(X2889,X2890)
| ~ ssPv3(skf1(X2890))
| ssPv2(X2891)
| ssPv2(X2889) ),
inference(resolution,[status(thm)],[c1083,clause1]) ).
cnf(c366,plain,
( ~ ssRr(X2390,X2389)
| ~ ssPv4(X2389)
| ~ ssRr(X2391,X2390)
| ~ ssRr(X2391,X2387)
| ~ ssPv3(X2387)
| ~ ssRr(X2391,X2391)
| ~ ssRr(X2387,X2388)
| ssPv2(X2388)
| ssPv2(X2391) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c1074,plain,
( ~ ssRr(X2861,X2860)
| ~ ssPv4(X2860)
| ~ ssRr(X2859,X2861)
| ~ ssPv3(X2861)
| ~ ssRr(X2859,X2859)
| ssPv2(X2860)
| ssPv2(X2859) ),
inference(factor,[status(thm)],[c366]) ).
cnf(c1037,plain,
( ~ ssRr(X2815,X2816)
| ~ ssPv2(X2816)
| ~ ssRr(X2813,X2815)
| ~ ssRr(X2815,X2814)
| ssPv4(X2814)
| ssPv3(X2816)
| ssPv3(X2813) ),
inference(factor,[status(thm)],[c355]) ).
cnf(c1212,plain,
( ~ ssRr(X2828,X2826)
| ~ ssPv2(X2826)
| ~ ssRr(X2827,X2828)
| ssPv4(skf1(X2828))
| ssPv3(X2826)
| ssPv3(X2827) ),
inference(resolution,[status(thm)],[c1037,clause1]) ).
cnf(c1216,plain,
( ~ ssRr(skf1(X2831),X2830)
| ~ ssPv2(X2830)
| ssPv4(skf1(skf1(X2831)))
| ssPv3(X2830)
| ssPv3(X2831) ),
inference(resolution,[status(thm)],[c1212,clause1]) ).
cnf(c354,plain,
( ~ ssRr(X2297,X2294)
| ~ ssPv2(X2294)
| ~ ssRr(X2293,X2297)
| ~ ssRr(X2293,X2296)
| ~ ssRr(X2293,X2293)
| ~ ssRr(X2296,X2295)
| ssPv4(X2296)
| ssPv3(X2295)
| ssPv3(X2293) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c1029,plain,
( ~ ssRr(X2805,X2806)
| ~ ssPv2(X2806)
| ~ ssRr(X2804,X2805)
| ~ ssRr(X2804,X2804)
| ssPv4(X2805)
| ssPv3(X2806)
| ssPv3(X2804) ),
inference(factor,[status(thm)],[c354]) ).
cnf(c817,plain,
( ~ ssRr(X2220,X2219)
| ~ ssPv1(X2219)
| ~ ssRr(X2221,X2220)
| ~ ssRr(X2220,X2222)
| ~ ssPv4(X2220)
| ssPv2(X2222)
| ssPv3(X2221) ),
inference(factor,[status(thm)],[c299]) ).
cnf(c996,plain,
( ~ ssRr(X2244,X2242)
| ~ ssPv1(X2242)
| ~ ssRr(X2243,X2244)
| ~ ssPv4(X2244)
| ssPv2(skf1(X2244))
| ssPv3(X2243) ),
inference(resolution,[status(thm)],[c817,clause1]) ).
cnf(c1005,plain,
( ~ ssRr(skf1(X2771),X2772)
| ~ ssPv1(X2772)
| ~ ssPv4(skf1(X2771))
| ssPv2(skf1(skf1(X2771)))
| ssPv3(X2771) ),
inference(resolution,[status(thm)],[c996,clause1]) ).
cnf(c1192,plain,
( ~ ssRr(X2765,X2764)
| ~ ssPv2(X2764)
| ~ ssRr(X2763,X2765)
| ssPv1(X2764)
| ssPv1(skf1(X2763))
| ssPv4(X2763) ),
inference(factor,[status(thm)],[c597]) ).
cnf(c989,plain,
( ~ ssRr(X2743,X2742)
| ~ ssPv1(X2742)
| ~ ssRr(X2741,X2743)
| ~ ssRr(X2743,X2744)
| ssPv4(X2744)
| ssPv3(X2742)
| ssPv3(X2741) ),
inference(factor,[status(thm)],[c345]) ).
cnf(c1188,plain,
( ~ ssRr(X2755,X2753)
| ~ ssPv1(X2753)
| ~ ssRr(X2754,X2755)
| ssPv4(skf1(X2755))
| ssPv3(X2753)
| ssPv3(X2754) ),
inference(resolution,[status(thm)],[c989,clause1]) ).
cnf(c1190,plain,
( ~ ssRr(skf1(X2758),X2757)
| ~ ssPv1(X2757)
| ssPv4(skf1(skf1(X2758)))
| ssPv3(X2757)
| ssPv3(X2758) ),
inference(resolution,[status(thm)],[c1188,clause1]) ).
cnf(c344,plain,
( ~ ssRr(X2198,X2199)
| ~ ssPv1(X2199)
| ~ ssRr(X2202,X2198)
| ~ ssRr(X2202,X2200)
| ~ ssRr(X2202,X2202)
| ~ ssRr(X2200,X2201)
| ssPv4(X2200)
| ssPv3(X2201)
| ssPv3(X2202) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c981,plain,
( ~ ssRr(X2733,X2734)
| ~ ssPv1(X2734)
| ~ ssRr(X2732,X2733)
| ~ ssRr(X2732,X2732)
| ssPv4(X2733)
| ssPv3(X2734)
| ssPv3(X2732) ),
inference(factor,[status(thm)],[c344]) ).
cnf(c1166,plain,
( ~ ssRr(X2675,X2674)
| ~ ssPv4(X2674)
| ~ ssRr(X2673,X2675)
| ssPv1(X2674)
| ssPv2(skf1(X2673))
| ssPv1(X2673) ),
inference(factor,[status(thm)],[c561]) ).
cnf(c944,plain,
( ~ ssRr(X2663,X2661)
| ~ ssPv4(X2661)
| ~ ssRr(X2662,X2663)
| ~ ssRr(X2662,X2662)
| ~ ssPv1(X2662)
| ~ ssPv2(X2663)
| ~ ssPv4(X2662) ),
inference(factor,[status(thm)],[c335]) ).
cnf(c943,plain,
( ~ ssRr(X2642,X2644)
| ~ ssPv4(X2644)
| ~ ssRr(X2643,X2642)
| ~ ssRr(X2642,X2645)
| ~ ssPv1(X2645)
| ~ ssPv2(X2642)
| ~ ssPv4(X2643) ),
inference(factor,[status(thm)],[c335]) ).
cnf(c1158,plain,
( ~ ssRr(X2647,X2646)
| ~ ssPv4(X2646)
| ~ ssRr(X2648,X2647)
| ~ ssPv1(X2646)
| ~ ssPv2(X2647)
| ~ ssPv4(X2648) ),
inference(factor,[status(thm)],[c943]) ).
cnf(c1162,plain,
( ~ ssRr(skf1(X2655),X2656)
| ~ ssPv4(X2656)
| ~ ssPv1(X2656)
| ~ ssPv2(skf1(X2655))
| ~ ssPv4(X2655) ),
inference(resolution,[status(thm)],[c1158,clause1]) ).
cnf(c1163,plain,
( ~ ssPv4(skf1(skf1(X2660)))
| ~ ssPv1(skf1(skf1(X2660)))
| ~ ssPv2(skf1(X2660))
| ~ ssPv4(X2660) ),
inference(resolution,[status(thm)],[c1162,clause1]) ).
cnf(c1160,plain,
( ~ ssRr(X2658,X2657)
| ~ ssPv4(X2657)
| ~ ssRr(X2659,X2658)
| ~ ssPv1(skf1(X2658))
| ~ ssPv2(X2658)
| ~ ssPv4(X2659) ),
inference(resolution,[status(thm)],[c943,clause1]) ).
cnf(c942,plain,
( ~ ssRr(X2632,X2631)
| ~ ssPv4(X2631)
| ~ ssRr(X2632,X2632)
| ~ ssRr(X2631,X2633)
| ~ ssPv1(X2633)
| ~ ssPv2(X2632)
| ~ ssPv4(X2632) ),
inference(factor,[status(thm)],[c335]) ).
cnf(c1155,plain,
( ~ ssRr(X2640,X2641)
| ~ ssPv4(X2641)
| ~ ssRr(X2640,X2640)
| ~ ssPv1(skf1(X2641))
| ~ ssPv2(X2640)
| ~ ssPv4(X2640) ),
inference(resolution,[status(thm)],[c942,clause1]) ).
cnf(c937,plain,
( ~ ssRr(X2620,X2619)
| ~ ssPv4(X2619)
| ~ ssRr(X2620,X2620)
| ~ ssRr(X2620,X2618)
| ~ ssPv1(X2618)
| ~ ssPv2(X2619)
| ~ ssPv4(X2620) ),
inference(factor,[status(thm)],[c334]) ).
cnf(c1150,plain,
( ~ ssRr(X2630,X2629)
| ~ ssPv4(X2629)
| ~ ssRr(X2630,X2630)
| ~ ssPv1(skf1(X2630))
| ~ ssPv2(X2629)
| ~ ssPv4(X2630) ),
inference(resolution,[status(thm)],[c937,clause1]) ).
cnf(c936,plain,
( ~ ssRr(X2607,X2609)
| ~ ssPv4(X2609)
| ~ ssRr(X2607,X2607)
| ~ ssRr(X2609,X2608)
| ~ ssPv1(X2608)
| ~ ssPv2(X2609)
| ~ ssPv4(X2607) ),
inference(factor,[status(thm)],[c334]) ).
cnf(c1147,plain,
( ~ ssRr(X2617,X2616)
| ~ ssPv4(X2616)
| ~ ssRr(X2617,X2617)
| ~ ssPv1(skf1(X2616))
| ~ ssPv2(X2616)
| ~ ssPv4(X2617) ),
inference(resolution,[status(thm)],[c936,clause1]) ).
cnf(c1140,plain,
( ~ ssRr(X2602,X2601)
| ~ ssPv4(X2601)
| ~ ssRr(X2603,X2602)
| ssPv1(X2601)
| ssPv4(skf1(X2603))
| ssPv1(X2603) ),
inference(factor,[status(thm)],[c532]) ).
cnf(c912,plain,
( ~ ssRr(X2568,X2567)
| ~ ssPv4(X2567)
| ~ ssRr(X2569,X2568)
| ~ ssRr(X2568,X2566)
| ~ ssPv1(X2566)
| ~ ssPv1(X2568)
| ssPv3(X2569) ),
inference(factor,[status(thm)],[c327]) ).
cnf(c1134,plain,
( ~ ssRr(X2572,X2573)
| ~ ssPv4(X2573)
| ~ ssRr(X2574,X2572)
| ~ ssPv1(X2573)
| ~ ssPv1(X2572)
| ssPv3(X2574) ),
inference(factor,[status(thm)],[c912]) ).
cnf(c1138,plain,
( ~ ssRr(skf1(X2577),X2576)
| ~ ssPv4(X2576)
| ~ ssPv1(X2576)
| ~ ssPv1(skf1(X2577))
| ssPv3(X2577) ),
inference(resolution,[status(thm)],[c1134,clause1]) ).
cnf(c1139,plain,
( ~ ssPv4(skf1(skf1(X2584)))
| ~ ssPv1(skf1(skf1(X2584)))
| ~ ssPv1(skf1(X2584))
| ssPv3(X2584) ),
inference(resolution,[status(thm)],[c1138,clause1]) ).
cnf(c1136,plain,
( ~ ssRr(X2583,X2582)
| ~ ssPv4(X2582)
| ~ ssRr(X2581,X2583)
| ~ ssPv1(skf1(X2583))
| ~ ssPv1(X2583)
| ssPv3(X2581) ),
inference(resolution,[status(thm)],[c912,clause1]) ).
cnf(c749,plain,
( ~ ssRr(X1958,X1960)
| ~ ssPv3(X1960)
| ~ ssRr(X1959,X1958)
| ~ ssRr(X1958,X1961)
| ~ ssPv2(X1958)
| ssPv1(X1961)
| ssPv4(X1959) ),
inference(factor,[status(thm)],[c282]) ).
cnf(c879,plain,
( ~ ssRr(X2013,X2011)
| ~ ssPv3(X2011)
| ~ ssRr(X2012,X2013)
| ~ ssPv2(X2013)
| ssPv1(skf1(X2013))
| ssPv4(X2012) ),
inference(resolution,[status(thm)],[c749,clause1]) ).
cnf(c904,plain,
( ~ ssRr(skf1(X2551),X2550)
| ~ ssPv3(X2550)
| ~ ssPv2(skf1(X2551))
| ssPv1(skf1(skf1(X2551)))
| ssPv4(X2551) ),
inference(resolution,[status(thm)],[c879,clause1]) ).
cnf(c1115,plain,
( ~ ssRr(X2506,X2507)
| ~ ssPv2(X2507)
| ~ ssRr(X2508,X2506)
| ~ ssPv1(X2506)
| ~ ssPv1(X2508)
| ssPv3(X2507) ),
inference(factor,[status(thm)],[c881]) ).
cnf(c1122,plain,
( ~ ssRr(skf1(X2511),X2510)
| ~ ssPv2(X2510)
| ~ ssPv1(skf1(X2511))
| ~ ssPv1(X2511)
| ssPv3(X2510) ),
inference(resolution,[status(thm)],[c1115,clause1]) ).
cnf(c1123,plain,
( ~ ssPv2(skf1(skf1(X2524)))
| ~ ssPv1(skf1(X2524))
| ~ ssPv1(X2524)
| ssPv3(skf1(skf1(X2524))) ),
inference(resolution,[status(thm)],[c1122,clause1]) ).
cnf(c872,plain,
( ~ ssRr(X2483,X2484)
| ~ ssPv2(X2484)
| ~ ssRr(X2483,X2483)
| ~ ssRr(X2483,X2482)
| ~ ssPv1(X2484)
| ~ ssPv1(X2483)
| ssPv3(X2482) ),
inference(factor,[status(thm)],[c318]) ).
cnf(c1112,plain,
( ~ ssRr(X2494,X2493)
| ~ ssPv2(X2493)
| ~ ssRr(X2494,X2494)
| ~ ssPv1(X2493)
| ~ ssPv1(X2494)
| ssPv3(skf1(X2494)) ),
inference(resolution,[status(thm)],[c872,clause1]) ).
cnf(c1110,plain,
( ~ ssRr(X2485,X2486)
| ~ ssPv2(X2486)
| ~ ssRr(X2485,X2485)
| ~ ssPv1(X2486)
| ~ ssPv1(X2485)
| ssPv3(X2486) ),
inference(factor,[status(thm)],[c872]) ).
cnf(c852,plain,
( ~ ssRr(X2450,X2449)
| ~ ssPv4(X2449)
| ~ ssRr(X2451,X2450)
| ~ ssRr(X2451,X2451)
| ~ ssPv2(X2450)
| ~ ssPv4(X2451)
| ssPv3(X2451) ),
inference(factor,[status(thm)],[c310]) ).
cnf(c1089,plain,
( ~ ssRr(X2426,X2424)
| ~ ssPv4(X2424)
| ~ ssRr(X2425,X2426)
| ~ ssPv2(X2426)
| ~ ssPv4(X2425)
| ssPv3(X2424) ),
inference(factor,[status(thm)],[c851]) ).
cnf(c1097,plain,
( ~ ssRr(skf1(X2431),X2430)
| ~ ssPv4(X2430)
| ~ ssPv2(skf1(X2431))
| ~ ssPv4(X2431)
| ssPv3(X2430) ),
inference(resolution,[status(thm)],[c1089,clause1]) ).
cnf(c1098,plain,
( ~ ssPv4(skf1(skf1(X2448)))
| ~ ssPv2(skf1(X2448))
| ~ ssPv4(X2448)
| ssPv3(skf1(skf1(X2448))) ),
inference(resolution,[status(thm)],[c1097,clause1]) ).
cnf(c368,plain,
( ~ ssRr(X2421,X2419)
| ~ ssPv4(X2419)
| ~ ssRr(X2423,X2421)
| ~ ssRr(X2422,X2420)
| ~ ssPv3(X2420)
| ~ ssRr(X2423,X2422)
| ~ ssRr(X2423,X2423)
| ssPv2(X2423) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c850,plain,
( ~ ssRr(X2401,X2402)
| ~ ssPv4(X2402)
| ~ ssRr(X2401,X2401)
| ~ ssRr(X2402,X2403)
| ~ ssPv2(X2401)
| ~ ssPv4(X2401)
| ssPv3(X2403) ),
inference(factor,[status(thm)],[c310]) ).
cnf(c1082,plain,
( ~ ssRr(X2412,X2413)
| ~ ssPv4(X2413)
| ~ ssRr(X2412,X2412)
| ~ ssPv2(X2412)
| ~ ssPv4(X2412)
| ssPv3(skf1(X2413)) ),
inference(resolution,[status(thm)],[c850,clause1]) ).
cnf(c842,plain,
( ~ ssRr(X2352,X2353)
| ~ ssPv4(X2353)
| ~ ssRr(X2352,X2352)
| ~ ssRr(X2352,X2354)
| ~ ssPv2(X2353)
| ~ ssPv4(X2352)
| ssPv3(X2354) ),
inference(factor,[status(thm)],[c309]) ).
cnf(c1056,plain,
( ~ ssRr(X2385,X2384)
| ~ ssPv4(X2384)
| ~ ssRr(X2385,X2385)
| ~ ssPv2(X2384)
| ~ ssPv4(X2385)
| ssPv3(skf1(X2385)) ),
inference(resolution,[status(thm)],[c842,clause1]) ).
cnf(c364,plain,
( ~ ssRr(X2363,X2359)
| ~ ssPv4(X2359)
| ~ ssRr(X2363,X2363)
| ~ ssRr(X2362,X2361)
| ~ ssPv3(X2361)
| ~ ssRr(X2363,X2362)
| ~ ssRr(X2359,X2360)
| ssPv2(X2360)
| ssPv2(X2363) ),
inference(factor,[status(thm)],[clause51]) ).
cnf(c1057,plain,
( ~ ssRr(X2364,X2364)
| ~ ssPv4(X2364)
| ~ ssRr(X2365,X2366)
| ~ ssPv3(X2366)
| ~ ssRr(X2364,X2365)
| ssPv2(X2364) ),
inference(factor,[status(thm)],[c364]) ).
cnf(c1064,plain,
( ~ ssRr(X2379,X2379)
| ~ ssPv4(X2379)
| ~ ssRr(skf1(X2379),X2378)
| ~ ssPv3(X2378)
| ssPv2(X2379) ),
inference(resolution,[status(thm)],[c1057,clause1]) ).
cnf(c1072,plain,
( ~ ssRr(X2380,X2380)
| ~ ssPv4(X2380)
| ~ ssPv3(skf1(skf1(X2380)))
| ssPv2(X2380) ),
inference(resolution,[status(thm)],[c1064,clause1]) ).
cnf(c1062,plain,
( ~ ssRr(X2368,X2368)
| ~ ssPv4(X2368)
| ~ ssRr(X2368,X2369)
| ~ ssPv3(X2369)
| ssPv2(X2368) ),
inference(factor,[status(thm)],[c1057]) ).
cnf(c1066,plain,
( ~ ssRr(X2371,X2371)
| ~ ssPv4(X2371)
| ~ ssPv3(skf1(X2371))
| ssPv2(X2371) ),
inference(resolution,[status(thm)],[c1062,clause1]) ).
cnf(c841,plain,
( ~ ssRr(X2340,X2338)
| ~ ssPv4(X2338)
| ~ ssRr(X2340,X2340)
| ~ ssRr(X2338,X2339)
| ~ ssPv2(X2338)
| ~ ssPv4(X2340)
| ssPv3(X2339) ),
inference(factor,[status(thm)],[c309]) ).
cnf(c1049,plain,
( ~ ssRr(X2349,X2350)
| ~ ssPv4(X2350)
| ~ ssRr(X2349,X2349)
| ~ ssPv2(X2350)
| ~ ssPv4(X2349)
| ssPv3(skf1(X2350)) ),
inference(resolution,[status(thm)],[c841,clause1]) ).
cnf(c1053,plain,
( ~ ssRr(X2351,X2351)
| ~ ssPv4(X2351)
| ~ ssPv2(X2351)
| ssPv3(skf1(X2351)) ),
inference(factor,[status(thm)],[c1049]) ).
cnf(c356,plain,
( ~ ssRr(X2331,X2328)
| ~ ssPv2(X2328)
| ~ ssRr(X2327,X2331)
| ~ ssRr(X2330,X2329)
| ~ ssRr(X2327,X2330)
| ~ ssRr(X2327,X2327)
| ssPv4(X2329)
| ssPv3(X2327) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c714,plain,
( ~ ssRr(X1845,X1843)
| ~ ssPv4(X1843)
| ~ ssRr(X1846,X1845)
| ~ ssRr(X1845,X1844)
| ssPv3(X1844)
| ssPv1(X1845)
| ssPv2(X1846) ),
inference(factor,[status(thm)],[c271]) ).
cnf(c829,plain,
( ~ ssRr(X1861,X1860)
| ~ ssPv4(X1860)
| ~ ssRr(X1862,X1861)
| ssPv3(skf1(X1861))
| ssPv1(X1861)
| ssPv2(X1862) ),
inference(resolution,[status(thm)],[c714,clause1]) ).
cnf(c838,plain,
( ~ ssRr(skf1(X2325),X2324)
| ~ ssPv4(X2324)
| ssPv3(skf1(skf1(X2325)))
| ssPv1(skf1(X2325))
| ssPv2(X2325) ),
inference(resolution,[status(thm)],[c829,clause1]) ).
cnf(c1031,plain,
( ~ ssRr(X2298,X2299)
| ~ ssPv2(X2299)
| ~ ssRr(X2300,X2298)
| ~ ssRr(X2300,X2300)
| ssPv4(X2300)
| ssPv3(X2300) ),
inference(factor,[status(thm)],[c354]) ).
cnf(c1035,plain,
( ~ ssRr(X2302,X2303)
| ~ ssPv2(X2303)
| ~ ssRr(X2302,X2302)
| ssPv4(X2302)
| ssPv3(X2302) ),
inference(factor,[status(thm)],[c1031]) ).
cnf(c352,plain,
( ~ ssRr(X2265,X2266)
| ~ ssPv2(X2266)
| ~ ssRr(X2265,X2265)
| ~ ssRr(X2269,X2267)
| ~ ssRr(X2265,X2269)
| ~ ssRr(X2266,X2268)
| ssPv4(X2267)
| ssPv3(X2268)
| ssPv3(X2265) ),
inference(factor,[status(thm)],[clause50]) ).
cnf(c1013,plain,
( ~ ssRr(X2275,X2275)
| ~ ssPv2(X2275)
| ~ ssRr(X2273,X2274)
| ~ ssRr(X2275,X2273)
| ssPv4(X2274)
| ssPv3(X2275) ),
inference(factor,[status(thm)],[c352]) ).
cnf(c1020,plain,
( ~ ssRr(X2288,X2288)
| ~ ssPv2(X2288)
| ~ ssRr(skf1(X2288),X2287)
| ssPv4(X2287)
| ssPv3(X2288) ),
inference(resolution,[status(thm)],[c1013,clause1]) ).
cnf(c1028,plain,
( ~ ssRr(X2289,X2289)
| ~ ssPv2(X2289)
| ssPv4(skf1(skf1(X2289)))
| ssPv3(X2289) ),
inference(resolution,[status(thm)],[c1020,clause1]) ).
cnf(c1018,plain,
( ~ ssRr(X2278,X2278)
| ~ ssPv2(X2278)
| ~ ssRr(X2278,X2277)
| ssPv4(X2277)
| ssPv3(X2278) ),
inference(factor,[status(thm)],[c1013]) ).
cnf(c1022,plain,
( ~ ssRr(X2286,X2286)
| ~ ssPv2(X2286)
| ssPv4(skf1(X2286))
| ssPv3(X2286) ),
inference(resolution,[status(thm)],[c1018,clause1]) ).
cnf(c1019,plain,
( ~ ssRr(X2276,X2276)
| ~ ssPv2(X2276)
| ssPv4(X2276)
| ssPv3(X2276) ),
inference(factor,[status(thm)],[c1013]) ).
cnf(c300,plain,
( ~ ssRr(X1834,X1835)
| ~ ssPv1(X1835)
| ~ ssRr(X1833,X1834)
| ~ ssRr(X1833,X1832)
| ~ ssRr(X1833,X1833)
| ~ ssPv4(X1832)
| ssPv2(X1832)
| ssPv3(X1833) ),
inference(factor,[status(thm)],[clause44]) ).
cnf(c824,plain,
( ~ ssRr(X2262,X2264)
| ~ ssPv1(X2264)
| ~ ssRr(X2263,X2262)
| ~ ssRr(X2263,X2263)
| ~ ssPv4(X2263)
| ssPv2(X2263)
| ssPv3(X2263) ),
inference(factor,[status(thm)],[c300]) ).
cnf(c818,plain,
( ~ ssRr(X2254,X2255)
| ~ ssPv1(X2255)
| ~ ssRr(X2253,X2254)
| ~ ssRr(X2253,X2253)
| ~ ssPv4(X2254)
| ssPv2(X2253)
| ssPv3(X2253) ),
inference(factor,[status(thm)],[c299]) ).
cnf(c994,plain,
( ~ ssRr(X2223,X2224)
| ~ ssPv1(X2224)
| ~ ssRr(X2225,X2223)
| ~ ssPv4(X2223)
| ssPv2(X2224)
| ssPv3(X2225) ),
inference(factor,[status(thm)],[c817]) ).
cnf(c998,plain,
( ~ ssRr(skf1(X2230),X2229)
| ~ ssPv1(X2229)
| ~ ssPv4(skf1(X2230))
| ssPv2(X2229)
| ssPv3(X2230) ),
inference(resolution,[status(thm)],[c994,clause1]) ).
cnf(c999,plain,
( ~ ssPv1(skf1(skf1(X2246)))
| ~ ssPv4(skf1(X2246))
| ssPv2(skf1(skf1(X2246)))
| ssPv3(X2246) ),
inference(resolution,[status(thm)],[c998,clause1]) ).
cnf(c346,plain,
( ~ ssRr(X2231,X2232)
| ~ ssPv1(X2232)
| ~ ssRr(X2235,X2231)
| ~ ssRr(X2234,X2233)
| ~ ssRr(X2235,X2234)
| ~ ssRr(X2235,X2235)
| ssPv4(X2233)
| ssPv3(X2235) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c983,plain,
( ~ ssRr(X2204,X2203)
| ~ ssPv1(X2203)
| ~ ssRr(X2205,X2204)
| ~ ssRr(X2205,X2205)
| ssPv4(X2205)
| ssPv3(X2205) ),
inference(factor,[status(thm)],[c344]) ).
cnf(c987,plain,
( ~ ssRr(X2208,X2207)
| ~ ssPv1(X2207)
| ~ ssRr(X2208,X2208)
| ssPv4(X2208)
| ssPv3(X2208) ),
inference(factor,[status(thm)],[c983]) ).
cnf(c342,plain,
( ~ ssRr(X2171,X2168)
| ~ ssPv1(X2168)
| ~ ssRr(X2171,X2171)
| ~ ssRr(X2170,X2167)
| ~ ssRr(X2171,X2170)
| ~ ssRr(X2168,X2169)
| ssPv4(X2167)
| ssPv3(X2169)
| ssPv3(X2171) ),
inference(factor,[status(thm)],[clause49]) ).
cnf(c965,plain,
( ~ ssRr(X2172,X2172)
| ~ ssPv1(X2172)
| ~ ssRr(X2174,X2173)
| ~ ssRr(X2172,X2174)
| ssPv4(X2173)
| ssPv3(X2172) ),
inference(factor,[status(thm)],[c342]) ).
cnf(c972,plain,
( ~ ssRr(X2187,X2187)
| ~ ssPv1(X2187)
| ~ ssRr(skf1(X2187),X2186)
| ssPv4(X2186)
| ssPv3(X2187) ),
inference(resolution,[status(thm)],[c965,clause1]) ).
cnf(c980,plain,
( ~ ssRr(X2188,X2188)
| ~ ssPv1(X2188)
| ssPv4(skf1(skf1(X2188)))
| ssPv3(X2188) ),
inference(resolution,[status(thm)],[c972,clause1]) ).
cnf(c970,plain,
( ~ ssRr(X2177,X2177)
| ~ ssPv1(X2177)
| ~ ssRr(X2177,X2176)
| ssPv4(X2176)
| ssPv3(X2177) ),
inference(factor,[status(thm)],[c965]) ).
cnf(c974,plain,
( ~ ssRr(X2179,X2179)
| ~ ssPv1(X2179)
| ssPv4(skf1(X2179))
| ssPv3(X2179) ),
inference(resolution,[status(thm)],[c970,clause1]) ).
cnf(c971,plain,
( ~ ssRr(X2175,X2175)
| ~ ssPv1(X2175)
| ssPv4(X2175)
| ssPv3(X2175) ),
inference(factor,[status(thm)],[c965]) ).
cnf(c338,plain,
( ~ ssRr(X2148,X2149)
| ~ ssPv4(X2149)
| ~ ssRr(X2151,X2148)
| ~ ssRr(X2150,X2152)
| ~ ssPv1(X2152)
| ~ ssRr(X2151,X2150)
| ~ ssPv2(skf1(X2151))
| ~ ssPv4(X2151) ),
inference(resolution,[status(thm)],[clause48,clause1]) ).
cnf(c292,plain,
( ~ ssRr(X1766,X1764)
| ~ ssPv3(X1764)
| ~ ssRr(X1763,X1766)
| ~ ssRr(X1763,X1765)
| ~ ssPv1(X1765)
| ~ ssRr(X1763,X1763)
| ssPv4(X1765)
| ssPv4(X1763) ),
inference(factor,[status(thm)],[clause43]) ).
cnf(c788,plain,
( ~ ssRr(X2146,X2145)
| ~ ssPv3(X2145)
| ~ ssRr(X2146,X2146)
| ~ ssRr(X2146,X2147)
| ~ ssPv1(X2147)
| ssPv4(X2147)
| ssPv4(X2146) ),
inference(factor,[status(thm)],[c292]) ).
cnf(c781,plain,
( ~ ssRr(X2114,X2113)
| ~ ssPv3(X2113)
| ~ ssRr(X2115,X2114)
| ~ ssRr(X2114,X2116)
| ~ ssPv1(X2116)
| ssPv4(X2114)
| ssPv4(X2115) ),
inference(factor,[status(thm)],[c291]) ).
cnf(c947,plain,
( ~ ssRr(X2128,X2129)
| ~ ssPv3(X2129)
| ~ ssRr(X2127,X2128)
| ~ ssPv1(X2129)
| ssPv4(X2128)
| ssPv4(X2127) ),
inference(factor,[status(thm)],[c781]) ).
cnf(c956,plain,
( ~ ssRr(skf1(X2136),X2137)
| ~ ssPv3(X2137)
| ~ ssPv1(X2137)
| ssPv4(skf1(X2136))
| ssPv4(X2136) ),
inference(resolution,[status(thm)],[c947,clause1]) ).
cnf(c961,plain,
( ~ ssPv3(skf1(skf1(X2141)))
| ~ ssPv1(skf1(skf1(X2141)))
| ssPv4(skf1(X2141))
| ssPv4(X2141) ),
inference(resolution,[status(thm)],[c956,clause1]) ).
cnf(c949,plain,
( ~ ssRr(X2139,X2140)
| ~ ssPv3(X2140)
| ~ ssRr(X2138,X2139)
| ~ ssPv1(skf1(X2139))
| ssPv4(X2139)
| ssPv4(X2138) ),
inference(resolution,[status(thm)],[c781,clause1]) ).
cnf(c336,plain,
( ~ ssRr(X2121,X2120)
| ~ ssPv4(X2120)
| ~ ssRr(X2119,X2121)
| ~ ssRr(X2119,X2122)
| ~ ssPv1(X2122)
| ~ ssRr(X2119,X2119)
| ~ ssPv2(X2122)
| ~ ssPv4(X2119) ),
inference(factor,[status(thm)],[clause48]) ).
cnf(c950,plain,
( ~ ssRr(X2124,X2124)
| ~ ssPv4(X2124)
| ~ ssRr(X2124,X2123)
| ~ ssPv1(X2123)
| ~ ssPv2(X2123) ),
inference(factor,[status(thm)],[c336]) ).
cnf(c954,plain,
( ~ ssRr(X2126,X2126)
| ~ ssPv4(X2126)
| ~ ssPv1(skf1(X2126))
| ~ ssPv2(skf1(X2126)) ),
inference(resolution,[status(thm)],[c950,clause1]) ).
cnf(c683,plain,
( ~ ssRr(X1726,X1725)
| ~ ssRr(X1727,X1726)
| ~ ssRr(X1726,X1724)
| ~ ssPv4(X1727)
| ssPv4(X1725)
| ssPv3(X1724)
| ssPv4(X1726) ),
inference(factor,[status(thm)],[c263]) ).
cnf(c769,plain,
( ~ ssRr(X1744,X1745)
| ~ ssRr(X1743,X1744)
| ~ ssPv4(X1743)
| ssPv4(X1745)
| ssPv3(skf1(X1744))
| ssPv4(X1744) ),
inference(resolution,[status(thm)],[c683,clause1]) ).
cnf(c779,plain,
( ~ ssRr(skf1(X2111),X2110)
| ~ ssPv4(X2111)
| ssPv4(X2110)
| ssPv3(skf1(skf1(X2111)))
| ssPv4(skf1(X2111)) ),
inference(resolution,[status(thm)],[c769,clause1]) ).
cnf(c774,plain,
( ~ ssRr(X2088,X2089)
| ~ ssPv3(X2089)
| ~ ssRr(X2088,X2088)
| ~ ssRr(X2088,X2090)
| ~ ssPv1(X2090)
| ssPv4(X2089)
| ssPv4(X2088) ),
inference(factor,[status(thm)],[c290]) ).
cnf(c935,plain,
( ~ ssRr(X2109,X2108)
| ~ ssPv3(X2108)
| ~ ssRr(X2109,X2109)
| ~ ssPv1(skf1(X2109))
| ssPv4(X2108)
| ssPv4(X2109) ),
inference(resolution,[status(thm)],[c774,clause1]) ).
cnf(c938,plain,
( ~ ssRr(X2100,X2101)
| ~ ssPv4(X2101)
| ~ ssRr(X2100,X2100)
| ~ ssPv1(X2100)
| ~ ssPv2(X2101)
| ~ ssPv4(X2100) ),
inference(factor,[status(thm)],[c334]) ).
cnf(c941,plain,
( ~ ssRr(X2102,X2102)
| ~ ssPv4(X2102)
| ~ ssPv1(X2102)
| ~ ssPv2(X2102) ),
inference(factor,[status(thm)],[c938]) ).
cnf(c933,plain,
( ~ ssRr(X2096,X2095)
| ~ ssPv3(X2095)
| ~ ssRr(X2096,X2096)
| ~ ssPv1(X2095)
| ssPv4(X2095)
| ssPv4(X2096) ),
inference(factor,[status(thm)],[c774]) ).
cnf(c328,plain,
( ~ ssRr(X2048,X2049)
| ~ ssPv4(X2049)
| ~ ssRr(X2050,X2048)
| ~ ssRr(X2050,X2047)
| ~ ssPv1(X2047)
| ~ ssRr(X2050,X2050)
| ssPv3(X2050) ),
inference(factor,[status(thm)],[clause47]) ).
cnf(c918,plain,
( ~ ssRr(X2072,X2073)
| ~ ssPv4(X2073)
| ~ ssRr(X2071,X2072)
| ~ ssRr(X2071,X2071)
| ~ ssPv1(X2071)
| ssPv3(X2071) ),
inference(factor,[status(thm)],[c328]) ).
cnf(c917,plain,
( ~ ssRr(X2055,X2057)
| ~ ssPv4(X2057)
| ~ ssRr(X2055,X2055)
| ~ ssRr(X2055,X2056)
| ~ ssPv1(X2056)
| ssPv3(X2055) ),
inference(factor,[status(thm)],[c328]) ).
cnf(c923,plain,
( ~ ssRr(X2070,X2069)
| ~ ssPv4(X2069)
| ~ ssRr(X2070,X2070)
| ~ ssPv1(skf1(X2070))
| ssPv3(X2070) ),
inference(resolution,[status(thm)],[c917,clause1]) ).
cnf(c922,plain,
( ~ ssRr(X2066,X2067)
| ~ ssPv4(X2067)
| ~ ssRr(X2066,X2066)
| ~ ssPv1(X2066)
| ssPv3(X2066) ),
inference(factor,[status(thm)],[c917]) ).
cnf(c921,plain,
( ~ ssRr(X2058,X2059)
| ~ ssPv4(X2059)
| ~ ssRr(X2058,X2058)
| ~ ssPv1(X2059)
| ssPv3(X2058) ),
inference(factor,[status(thm)],[c917]) ).
cnf(c916,plain,
( ~ ssRr(X2051,X2051)
| ~ ssPv4(X2051)
| ~ ssRr(X2051,X2052)
| ~ ssPv1(X2052)
| ssPv3(X2051) ),
inference(factor,[status(thm)],[c328]) ).
cnf(c920,plain,
( ~ ssRr(X2054,X2054)
| ~ ssPv4(X2054)
| ~ ssPv1(skf1(X2054))
| ssPv3(X2054) ),
inference(resolution,[status(thm)],[c916,clause1]) ).
cnf(c645,plain,
( ~ ssRr(X1676,X1673)
| ~ ssPv3(X1673)
| ~ ssRr(X1674,X1676)
| ~ ssRr(X1676,X1675)
| ssPv2(X1675)
| ssPv4(X1676)
| ssPv4(X1674) ),
inference(factor,[status(thm)],[c255]) ).
cnf(c754,plain,
( ~ ssRr(X1690,X1691)
| ~ ssPv3(X1691)
| ~ ssRr(X1689,X1690)
| ssPv2(skf1(X1690))
| ssPv4(X1690)
| ssPv4(X1689) ),
inference(resolution,[status(thm)],[c645,clause1]) ).
cnf(c759,plain,
( ~ ssRr(skf1(X2027),X2026)
| ~ ssPv3(X2026)
| ssPv2(skf1(skf1(X2027)))
| ssPv4(skf1(X2027))
| ssPv4(X2027) ),
inference(resolution,[status(thm)],[c754,clause1]) ).
cnf(c877,plain,
( ~ ssRr(X1968,X1967)
| ~ ssPv3(X1967)
| ~ ssRr(X1969,X1968)
| ~ ssPv2(X1968)
| ssPv1(X1967)
| ssPv4(X1969) ),
inference(factor,[status(thm)],[c749]) ).
cnf(c885,plain,
( ~ ssRr(skf1(X1974),X1973)
| ~ ssPv3(X1973)
| ~ ssPv2(skf1(X1974))
| ssPv1(X1973)
| ssPv4(X1974) ),
inference(resolution,[status(thm)],[c877,clause1]) ).
cnf(c886,plain,
( ~ ssPv3(skf1(skf1(X2015)))
| ~ ssPv2(skf1(X2015))
| ssPv1(skf1(skf1(X2015)))
| ssPv4(X2015) ),
inference(resolution,[status(thm)],[c885,clause1]) ).
cnf(c322,plain,
( ~ ssRr(X2002,X2004)
| ~ ssPv2(X2004)
| ~ ssRr(X2005,X2002)
| ~ ssRr(X2003,X2006)
| ~ ssRr(X2005,X2003)
| ~ ssPv1(skf1(X2005))
| ~ ssPv1(X2005)
| ssPv3(X2006) ),
inference(resolution,[status(thm)],[clause46,clause1]) ).
cnf(c892,plain,
( ~ ssRr(X1997,X1998)
| ~ ssPv2(X1998)
| ~ ssRr(X1996,X1997)
| ~ ssRr(X1996,X1996)
| ~ ssPv1(X1996)
| ssPv3(X1996) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c901,plain,
( ~ ssRr(X2000,X2001)
| ~ ssPv2(X2001)
| ~ ssRr(X2000,X2000)
| ~ ssPv1(X2000)
| ssPv3(X2000) ),
inference(factor,[status(thm)],[c892]) ).
cnf(c890,plain,
( ~ ssRr(X1987,X1987)
| ~ ssPv2(X1987)
| ~ ssRr(X1987,X1988)
| ~ ssPv1(X1988)
| ~ ssPv1(X1987)
| ssPv3(X1988) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c880,plain,
( ~ ssRr(X1977,X1976)
| ~ ssPv2(X1976)
| ~ ssRr(X1977,X1977)
| ~ ssRr(X1976,X1975)
| ~ ssPv1(X1977)
| ssPv3(X1975) ),
inference(factor,[status(thm)],[c319]) ).
cnf(c889,plain,
( ~ ssRr(X1985,X1984)
| ~ ssPv2(X1984)
| ~ ssRr(X1985,X1985)
| ~ ssPv1(X1985)
| ssPv3(skf1(X1984)) ),
inference(resolution,[status(thm)],[c880,clause1]) ).
cnf(c893,plain,
( ~ ssRr(X1986,X1986)
| ~ ssPv2(X1986)
| ~ ssPv1(X1986)
| ssPv3(skf1(X1986)) ),
inference(factor,[status(thm)],[c889]) ).
cnf(c748,plain,
( ~ ssRr(X1945,X1943)
| ~ ssPv3(X1943)
| ~ ssRr(X1945,X1945)
| ~ ssRr(X1943,X1944)
| ~ ssPv2(X1945)
| ssPv1(X1944)
| ssPv4(X1945) ),
inference(factor,[status(thm)],[c282]) ).
cnf(c870,plain,
( ~ ssRr(X1955,X1956)
| ~ ssPv3(X1956)
| ~ ssRr(X1955,X1955)
| ~ ssPv2(X1955)
| ssPv1(skf1(X1956))
| ssPv4(X1955) ),
inference(resolution,[status(thm)],[c748,clause1]) ).
cnf(c313,plain,
( ~ ssRr(X1935,X1937)
| ~ ssPv4(X1937)
| ~ ssRr(X1938,X1935)
| ~ ssRr(X1934,X1936)
| ~ ssRr(X1938,X1934)
| ~ ssPv2(skf1(X1938))
| ~ ssPv4(X1938)
| ssPv3(X1936) ),
inference(resolution,[status(thm)],[clause45,clause1]) ).
cnf(c743,plain,
( ~ ssRr(X1929,X1927)
| ~ ssPv3(X1927)
| ~ ssRr(X1929,X1929)
| ~ ssRr(X1927,X1928)
| ~ ssPv2(X1927)
| ssPv1(X1928)
| ssPv4(X1929) ),
inference(factor,[status(thm)],[c281]) ).
cnf(c866,plain,
( ~ ssRr(X1932,X1933)
| ~ ssPv3(X1933)
| ~ ssRr(X1932,X1932)
| ~ ssPv2(X1933)
| ssPv1(skf1(X1933))
| ssPv4(X1932) ),
inference(resolution,[status(thm)],[c743,clause1]) ).
cnf(c311,plain,
( ~ ssRr(X1908,X1910)
| ~ ssPv4(X1910)
| ~ ssRr(X1909,X1908)
| ~ ssRr(X1909,X1911)
| ~ ssRr(X1909,X1909)
| ~ ssPv2(X1911)
| ~ ssPv4(X1909)
| ssPv3(X1911) ),
inference(factor,[status(thm)],[clause45]) ).
cnf(c854,plain,
( ~ ssRr(X1913,X1913)
| ~ ssPv4(X1913)
| ~ ssRr(X1913,X1912)
| ~ ssPv2(X1912)
| ssPv3(X1912) ),
inference(factor,[status(thm)],[c311]) ).
cnf(c858,plain,
( ~ ssRr(X1915,X1915)
| ~ ssPv4(X1915)
| ~ ssPv2(skf1(X1915))
| ssPv3(skf1(X1915)) ),
inference(resolution,[status(thm)],[c854,clause1]) ).
cnf(c272,plain,
( ~ ssRr(X1610,X1611)
| ~ ssPv4(X1611)
| ~ ssRr(X1612,X1610)
| ~ ssRr(X1612,X1609)
| ~ ssRr(X1612,X1612)
| ssPv3(X1609)
| ssPv1(X1609)
| ssPv2(X1612) ),
inference(factor,[status(thm)],[clause41]) ).
cnf(c723,plain,
( ~ ssRr(X1888,X1886)
| ~ ssPv4(X1886)
| ~ ssRr(X1888,X1888)
| ~ ssRr(X1888,X1887)
| ssPv3(X1887)
| ssPv1(X1887)
| ssPv2(X1888) ),
inference(factor,[status(thm)],[c272]) ).
cnf(c612,plain,
( ~ ssRr(X1599,X1598)
| ~ ssPv1(X1598)
| ~ ssRr(X1600,X1599)
| ~ ssRr(X1599,X1597)
| ssPv1(X1597)
| ssPv3(X1599)
| ssPv3(X1600) ),
inference(factor,[status(thm)],[c245]) ).
cnf(c719,plain,
( ~ ssRr(X1607,X1608)
| ~ ssPv1(X1608)
| ~ ssRr(X1606,X1607)
| ssPv1(skf1(X1607))
| ssPv3(X1607)
| ssPv3(X1606) ),
inference(resolution,[status(thm)],[c612,clause1]) ).
cnf(c721,plain,
( ~ ssRr(skf1(X1884),X1883)
| ~ ssPv1(X1883)
| ssPv1(skf1(skf1(X1884)))
| ssPv3(skf1(X1884))
| ssPv3(X1884) ),
inference(resolution,[status(thm)],[c719,clause1]) ).
cnf(c843,plain,
( ~ ssRr(X1881,X1880)
| ~ ssPv4(X1880)
| ~ ssRr(X1881,X1881)
| ~ ssPv2(X1880)
| ~ ssPv4(X1881)
| ssPv3(X1881) ),
inference(factor,[status(thm)],[c309]) ).
cnf(c845,plain,
( ~ ssRr(X1882,X1882)
| ~ ssPv4(X1882)
| ~ ssPv2(X1882)
| ssPv3(X1882) ),
inference(factor,[status(thm)],[c843]) ).
cnf(c715,plain,
( ~ ssRr(X1871,X1870)
| ~ ssPv4(X1870)
| ~ ssRr(X1872,X1871)
| ~ ssRr(X1872,X1872)
| ssPv3(X1872)
| ssPv1(X1871)
| ssPv2(X1872) ),
inference(factor,[status(thm)],[c271]) ).
cnf(c827,plain,
( ~ ssRr(X1854,X1852)
| ~ ssPv4(X1852)
| ~ ssRr(X1853,X1854)
| ssPv3(X1852)
| ssPv1(X1854)
| ssPv2(X1853) ),
inference(factor,[status(thm)],[c714]) ).
cnf(c835,plain,
( ~ ssRr(skf1(X1859),X1858)
| ~ ssPv4(X1858)
| ssPv3(X1858)
| ssPv1(skf1(X1859))
| ssPv2(X1859) ),
inference(resolution,[status(thm)],[c827,clause1]) ).
cnf(c836,plain,
( ~ ssPv4(skf1(skf1(X1869)))
| ssPv3(skf1(skf1(X1869)))
| ssPv1(skf1(X1869))
| ssPv2(X1869) ),
inference(resolution,[status(thm)],[c835,clause1]) ).
cnf(c302,plain,
( ~ ssRr(X1864,X1865)
| ~ ssPv1(X1865)
| ~ ssRr(X1867,X1864)
| ~ ssRr(X1866,X1863)
| ~ ssRr(X1867,X1866)
| ~ ssPv4(skf1(X1867))
| ssPv2(X1863)
| ssPv3(X1867) ),
inference(resolution,[status(thm)],[clause44,clause1]) ).
cnf(c708,plain,
( ~ ssRr(X1816,X1817)
| ~ ssPv4(X1817)
| ~ ssRr(X1816,X1816)
| ~ ssRr(X1816,X1818)
| ssPv3(X1818)
| ssPv1(X1817)
| ssPv2(X1816) ),
inference(factor,[status(thm)],[c270]) ).
cnf(c815,plain,
( ~ ssRr(X1830,X1829)
| ~ ssPv4(X1829)
| ~ ssRr(X1830,X1830)
| ssPv3(skf1(X1830))
| ssPv1(X1829)
| ssPv2(X1830) ),
inference(resolution,[status(thm)],[c708,clause1]) ).
cnf(c813,plain,
( ~ ssRr(X1824,X1825)
| ~ ssPv4(X1825)
| ~ ssRr(X1824,X1824)
| ssPv3(X1825)
| ssPv1(X1825)
| ssPv2(X1824) ),
inference(factor,[status(thm)],[c708]) ).
cnf(c707,plain,
( ~ ssRr(X1802,X1801)
| ~ ssPv4(X1801)
| ~ ssRr(X1802,X1802)
| ~ ssRr(X1801,X1803)
| ssPv3(X1803)
| ssPv1(X1801)
| ssPv2(X1802) ),
inference(factor,[status(thm)],[c270]) ).
cnf(c806,plain,
( ~ ssRr(X1814,X1813)
| ~ ssPv4(X1813)
| ~ ssRr(X1814,X1814)
| ssPv3(skf1(X1813))
| ssPv1(X1813)
| ssPv2(X1814) ),
inference(resolution,[status(thm)],[c707,clause1]) ).
cnf(c577,plain,
( ~ ssRr(X1493,X1494)
| ~ ssPv2(X1494)
| ~ ssRr(X1492,X1493)
| ~ ssRr(X1493,X1491)
| ssPv1(X1491)
| ssPv1(X1493)
| ssPv4(X1492) ),
inference(factor,[status(thm)],[c237]) ).
cnf(c670,plain,
( ~ ssRr(X1539,X1538)
| ~ ssPv2(X1538)
| ~ ssRr(X1540,X1539)
| ssPv1(skf1(X1539))
| ssPv1(X1539)
| ssPv4(X1540) ),
inference(resolution,[status(thm)],[c577,clause1]) ).
cnf(c693,plain,
( ~ ssRr(skf1(X1787),X1786)
| ~ ssPv2(X1786)
| ssPv1(skf1(skf1(X1787)))
| ssPv1(skf1(X1787))
| ssPv4(X1787) ),
inference(resolution,[status(thm)],[c670,clause1]) ).
cnf(c789,plain,
( ~ ssRr(X1773,X1771)
| ~ ssPv3(X1771)
| ~ ssRr(X1772,X1773)
| ~ ssRr(X1772,X1772)
| ~ ssPv1(X1772)
| ssPv4(X1772) ),
inference(factor,[status(thm)],[c292]) ).
cnf(c793,plain,
( ~ ssRr(X1781,X1780)
| ~ ssPv3(X1780)
| ~ ssRr(X1781,X1781)
| ~ ssPv1(X1781)
| ssPv4(X1781) ),
inference(factor,[status(thm)],[c789]) ).
cnf(c787,plain,
( ~ ssRr(X1767,X1767)
| ~ ssPv3(X1767)
| ~ ssRr(X1767,X1768)
| ~ ssPv1(X1768)
| ssPv4(X1768)
| ssPv4(X1767) ),
inference(factor,[status(thm)],[c292]) ).
cnf(c791,plain,
( ~ ssRr(X1770,X1770)
| ~ ssPv3(X1770)
| ~ ssPv1(skf1(X1770))
| ssPv4(skf1(X1770))
| ssPv4(X1770) ),
inference(resolution,[status(thm)],[c787,clause1]) ).
cnf(c780,plain,
( ~ ssRr(X1754,X1753)
| ~ ssPv3(X1753)
| ~ ssRr(X1754,X1754)
| ~ ssRr(X1753,X1755)
| ~ ssPv1(X1755)
| ssPv4(X1754) ),
inference(factor,[status(thm)],[c291]) ).
cnf(c786,plain,
( ~ ssRr(X1758,X1759)
| ~ ssPv3(X1759)
| ~ ssRr(X1758,X1758)
| ~ ssPv1(skf1(X1759))
| ssPv4(X1758) ),
inference(resolution,[status(thm)],[c780,clause1]) ).
cnf(c767,plain,
( ~ ssRr(X1729,X1728)
| ~ ssRr(X1730,X1729)
| ~ ssPv4(X1730)
| ssPv4(X1728)
| ssPv3(X1728)
| ssPv4(X1729) ),
inference(factor,[status(thm)],[c683]) ).
cnf(c771,plain,
( ~ ssRr(skf1(X1734),X1735)
| ~ ssPv4(X1734)
| ssPv4(X1735)
| ssPv3(X1735)
| ssPv4(skf1(X1734)) ),
inference(resolution,[status(thm)],[c767,clause1]) ).
cnf(c772,plain,
( ~ ssPv4(X1747)
| ssPv4(skf1(skf1(X1747)))
| ssPv3(skf1(skf1(X1747)))
| ssPv4(skf1(X1747)) ),
inference(resolution,[status(thm)],[c771,clause1]) ).
cnf(c285,plain,
( ~ ssRr(X1723,X1722)
| ~ ssPv3(X1722)
| ~ ssRr(X1721,X1723)
| ~ ssRr(X1720,X1719)
| ~ ssRr(X1721,X1720)
| ~ ssPv2(skf1(X1721))
| ssPv1(X1719)
| ssPv4(X1721) ),
inference(resolution,[status(thm)],[clause42,clause1]) ).
cnf(c256,plain,
( ~ ssRr(X1459,X1460)
| ~ ssPv3(X1460)
| ~ ssRr(X1458,X1459)
| ~ ssRr(X1458,X1457)
| ~ ssRr(X1458,X1458)
| ssPv2(X1457)
| ssPv4(X1457)
| ssPv4(X1458) ),
inference(factor,[status(thm)],[clause39]) ).
cnf(c653,plain,
( ~ ssRr(X1698,X1697)
| ~ ssPv3(X1697)
| ~ ssRr(X1698,X1698)
| ~ ssRr(X1698,X1699)
| ssPv2(X1699)
| ssPv4(X1699)
| ssPv4(X1698) ),
inference(factor,[status(thm)],[c256]) ).
cnf(c752,plain,
( ~ ssRr(X1679,X1681)
| ~ ssPv3(X1681)
| ~ ssRr(X1680,X1679)
| ssPv2(X1681)
| ssPv4(X1679)
| ssPv4(X1680) ),
inference(factor,[status(thm)],[c645]) ).
cnf(c756,plain,
( ~ ssRr(skf1(X1684),X1683)
| ~ ssPv3(X1683)
| ssPv2(X1683)
| ssPv4(skf1(X1684))
| ssPv4(X1684) ),
inference(resolution,[status(thm)],[c752,clause1]) ).
cnf(c757,plain,
( ~ ssPv3(skf1(skf1(X1693)))
| ssPv2(skf1(skf1(X1693)))
| ssPv4(skf1(X1693))
| ssPv4(X1693) ),
inference(resolution,[status(thm)],[c756,clause1]) ).
cnf(c639,plain,
( ~ ssRr(X1653,X1651)
| ~ ssPv3(X1651)
| ~ ssRr(X1653,X1653)
| ~ ssRr(X1653,X1652)
| ssPv2(X1652)
| ssPv4(X1651)
| ssPv4(X1653) ),
inference(factor,[status(thm)],[c254]) ).
cnf(c741,plain,
( ~ ssRr(X1666,X1665)
| ~ ssPv3(X1665)
| ~ ssRr(X1666,X1666)
| ssPv2(skf1(X1666))
| ssPv4(X1665)
| ssPv4(X1666) ),
inference(resolution,[status(thm)],[c639,clause1]) ).
cnf(c739,plain,
( ~ ssRr(X1655,X1654)
| ~ ssPv3(X1654)
| ~ ssRr(X1655,X1655)
| ssPv2(X1654)
| ssPv4(X1654)
| ssPv4(X1655) ),
inference(factor,[status(thm)],[c639]) ).
cnf(c543,plain,
( ~ ssRr(X1366,X1363)
| ~ ssPv4(X1363)
| ~ ssRr(X1365,X1366)
| ~ ssRr(X1366,X1364)
| ssPv1(X1364)
| ssPv2(X1366)
| ssPv1(X1365) ),
inference(factor,[status(thm)],[c225]) ).
cnf(c608,plain,
( ~ ssRr(X1413,X1411)
| ~ ssPv4(X1411)
| ~ ssRr(X1412,X1413)
| ssPv1(skf1(X1413))
| ssPv2(X1413)
| ssPv1(X1412) ),
inference(resolution,[status(thm)],[c543,clause1]) ).
cnf(c633,plain,
( ~ ssRr(skf1(X1646),X1645)
| ~ ssPv4(X1645)
| ssPv1(skf1(skf1(X1646)))
| ssPv2(skf1(X1646))
| ssPv1(X1646) ),
inference(resolution,[status(thm)],[c608,clause1]) ).
cnf(c246,plain,
( ~ ssRr(X1387,X1388)
| ~ ssPv1(X1388)
| ~ ssRr(X1389,X1387)
| ~ ssRr(X1389,X1390)
| ~ ssRr(X1389,X1389)
| ssPv1(X1390)
| ssPv3(X1390)
| ssPv3(X1389) ),
inference(factor,[status(thm)],[clause38]) ).
cnf(c621,plain,
( ~ ssRr(X1627,X1626)
| ~ ssPv1(X1626)
| ~ ssRr(X1627,X1627)
| ~ ssRr(X1627,X1628)
| ssPv1(X1628)
| ssPv3(X1628)
| ssPv3(X1627) ),
inference(factor,[status(thm)],[c246]) ).
cnf(c722,plain,
( ~ ssRr(X1615,X1615)
| ~ ssPv4(X1615)
| ~ ssRr(X1615,X1614)
| ssPv3(X1614)
| ssPv1(X1614)
| ssPv2(X1615) ),
inference(factor,[status(thm)],[c272]) ).
cnf(c726,plain,
( ~ ssRr(X1617,X1617)
| ~ ssPv4(X1617)
| ssPv3(skf1(X1617))
| ssPv1(skf1(X1617))
| ssPv2(X1617) ),
inference(resolution,[status(thm)],[c722,clause1]) ).
cnf(c603,plain,
( ~ ssRr(X1575,X1577)
| ~ ssPv1(X1577)
| ~ ssRr(X1575,X1575)
| ~ ssRr(X1575,X1576)
| ssPv1(X1576)
| ssPv3(X1577)
| ssPv3(X1575) ),
inference(factor,[status(thm)],[c244]) ).
cnf(c706,plain,
( ~ ssRr(X1590,X1589)
| ~ ssPv1(X1589)
| ~ ssRr(X1590,X1590)
| ssPv1(skf1(X1590))
| ssPv3(X1589)
| ssPv3(X1590) ),
inference(resolution,[status(thm)],[c603,clause1]) ).
cnf(c709,plain,
( ~ ssRr(X1586,X1587)
| ~ ssPv4(X1587)
| ~ ssRr(X1586,X1586)
| ssPv3(X1586)
| ssPv1(X1587)
| ssPv2(X1586) ),
inference(factor,[status(thm)],[c270]) ).
cnf(c262,plain,
( ~ ssRr(X1506,X1504)
| ~ ssRr(X1506,X1506)
| ~ ssRr(X1503,X1505)
| ~ ssRr(X1506,X1503)
| ~ ssPv4(X1506)
| ssPv4(X1504)
| ssPv3(X1505) ),
inference(factor,[status(thm)],[clause40]) ).
cnf(c677,plain,
( ~ ssRr(X1553,X1552)
| ~ ssRr(X1553,X1553)
| ~ ssRr(skf1(X1553),X1551)
| ~ ssPv4(X1553)
| ssPv4(X1552)
| ssPv3(X1551) ),
inference(resolution,[status(thm)],[c262,clause1]) ).
cnf(c698,plain,
( ~ ssRr(X1554,X1555)
| ~ ssRr(X1554,X1554)
| ~ ssPv4(X1554)
| ssPv4(X1555)
| ssPv3(skf1(skf1(X1554))) ),
inference(resolution,[status(thm)],[c677,clause1]) ).
cnf(c668,plain,
( ~ ssRr(X1498,X1497)
| ~ ssPv2(X1497)
| ~ ssRr(X1499,X1498)
| ssPv1(X1497)
| ssPv1(X1498)
| ssPv4(X1499) ),
inference(factor,[status(thm)],[c577]) ).
cnf(c672,plain,
( ~ ssRr(skf1(X1502),X1501)
| ~ ssPv2(X1501)
| ssPv1(X1501)
| ssPv1(skf1(X1502))
| ssPv4(X1502) ),
inference(resolution,[status(thm)],[c668,clause1]) ).
cnf(c673,plain,
( ~ ssPv2(skf1(skf1(X1550)))
| ssPv1(skf1(skf1(X1550)))
| ssPv1(skf1(X1550))
| ssPv4(X1550) ),
inference(resolution,[status(thm)],[c672,clause1]) ).
cnf(c675,plain,
( ~ ssRr(X1524,X1525)
| ~ ssRr(X1524,X1524)
| ~ ssRr(X1524,X1523)
| ~ ssPv4(X1524)
| ssPv4(X1525)
| ssPv3(X1523) ),
inference(factor,[status(thm)],[c262]) ).
cnf(c689,plain,
( ~ ssRr(X1536,X1535)
| ~ ssRr(X1536,X1536)
| ~ ssPv4(X1536)
| ssPv4(X1535)
| ssPv3(skf1(X1536)) ),
inference(resolution,[status(thm)],[c675,clause1]) ).
cnf(c687,plain,
( ~ ssRr(X1526,X1527)
| ~ ssRr(X1526,X1526)
| ~ ssPv4(X1526)
| ssPv4(X1527)
| ssPv3(X1527) ),
inference(factor,[status(thm)],[c675]) ).
cnf(c674,plain,
( ~ ssRr(X1512,X1511)
| ~ ssRr(X1512,X1512)
| ~ ssRr(X1511,X1510)
| ~ ssPv4(X1512)
| ssPv4(X1511)
| ssPv3(X1510) ),
inference(factor,[status(thm)],[c262]) ).
cnf(c681,plain,
( ~ ssRr(X1520,X1521)
| ~ ssRr(X1520,X1520)
| ~ ssPv4(X1520)
| ssPv4(X1521)
| ssPv3(skf1(X1521)) ),
inference(resolution,[status(thm)],[c674,clause1]) ).
cnf(c676,plain,
( ~ ssRr(X1508,X1507)
| ~ ssRr(X1508,X1508)
| ~ ssPv4(X1508)
| ssPv4(X1507)
| ssPv3(X1508) ),
inference(factor,[status(thm)],[c262]) ).
cnf(c654,plain,
( ~ ssRr(X1467,X1465)
| ~ ssPv3(X1465)
| ~ ssRr(X1466,X1467)
| ~ ssRr(X1466,X1466)
| ssPv2(X1466)
| ssPv4(X1466) ),
inference(factor,[status(thm)],[c256]) ).
cnf(c658,plain,
( ~ ssRr(X1474,X1475)
| ~ ssPv3(X1475)
| ~ ssRr(X1474,X1474)
| ssPv2(X1474)
| ssPv4(X1474) ),
inference(factor,[status(thm)],[c654]) ).
cnf(c652,plain,
( ~ ssRr(X1461,X1461)
| ~ ssPv3(X1461)
| ~ ssRr(X1461,X1462)
| ssPv2(X1462)
| ssPv4(X1462)
| ssPv4(X1461) ),
inference(factor,[status(thm)],[c256]) ).
cnf(c644,plain,
( ~ ssRr(X1449,X1451)
| ~ ssPv3(X1451)
| ~ ssRr(X1449,X1449)
| ~ ssRr(X1451,X1450)
| ssPv2(X1450)
| ssPv4(X1449) ),
inference(factor,[status(thm)],[c255]) ).
cnf(c650,plain,
( ~ ssRr(X1455,X1454)
| ~ ssPv3(X1454)
| ~ ssRr(X1455,X1455)
| ssPv2(skf1(X1454))
| ssPv4(X1455) ),
inference(resolution,[status(thm)],[c644,clause1]) ).
cnf(c651,plain,
( ~ ssRr(X1456,X1456)
| ~ ssPv3(X1456)
| ssPv2(skf1(X1456))
| ssPv4(X1456) ),
inference(factor,[status(thm)],[c650]) ).
cnf(c520,plain,
( ~ ssRr(X1267,X1268)
| ~ ssPv4(X1268)
| ~ ssRr(X1266,X1267)
| ~ ssRr(X1267,X1265)
| ssPv1(X1265)
| ssPv4(X1267)
| ssPv1(X1266) ),
inference(factor,[status(thm)],[c216]) ).
cnf(c559,plain,
( ~ ssRr(X1284,X1283)
| ~ ssPv4(X1283)
| ~ ssRr(X1282,X1284)
| ssPv1(skf1(X1284))
| ssPv4(X1284)
| ssPv1(X1282) ),
inference(resolution,[status(thm)],[c520,clause1]) ).
cnf(c568,plain,
( ~ ssRr(skf1(X1439),X1438)
| ~ ssPv4(X1438)
| ssPv1(skf1(skf1(X1439)))
| ssPv4(skf1(X1439))
| ssPv1(X1439) ),
inference(resolution,[status(thm)],[c559,clause1]) ).
cnf(c640,plain,
( ~ ssRr(X1436,X1435)
| ~ ssPv3(X1435)
| ~ ssRr(X1436,X1436)
| ssPv2(X1436)
| ssPv4(X1435)
| ssPv4(X1436) ),
inference(factor,[status(thm)],[c254]) ).
cnf(c642,plain,
( ~ ssRr(X1437,X1437)
| ~ ssPv3(X1437)
| ssPv2(X1437)
| ssPv4(X1437) ),
inference(factor,[status(thm)],[c640]) ).
cnf(c606,plain,
( ~ ssRr(X1371,X1369)
| ~ ssPv4(X1369)
| ~ ssRr(X1370,X1371)
| ssPv1(X1369)
| ssPv2(X1371)
| ssPv1(X1370) ),
inference(factor,[status(thm)],[c543]) ).
cnf(c610,plain,
( ~ ssRr(skf1(X1379),X1378)
| ~ ssPv4(X1378)
| ssPv1(X1378)
| ssPv2(skf1(X1379))
| ssPv1(X1379) ),
inference(resolution,[status(thm)],[c606,clause1]) ).
cnf(c615,plain,
( ~ ssPv4(skf1(skf1(X1420)))
| ssPv1(skf1(skf1(X1420)))
| ssPv2(skf1(X1420))
| ssPv1(X1420) ),
inference(resolution,[status(thm)],[c610,clause1]) ).
cnf(c622,plain,
( ~ ssRr(X1397,X1398)
| ~ ssPv1(X1398)
| ~ ssRr(X1396,X1397)
| ~ ssRr(X1396,X1396)
| ssPv1(X1396)
| ssPv3(X1396) ),
inference(factor,[status(thm)],[c246]) ).
cnf(c626,plain,
( ~ ssRr(X1406,X1405)
| ~ ssPv1(X1405)
| ~ ssRr(X1406,X1406)
| ssPv1(X1406)
| ssPv3(X1406) ),
inference(factor,[status(thm)],[c622]) ).
cnf(c620,plain,
( ~ ssRr(X1392,X1392)
| ~ ssPv1(X1392)
| ~ ssRr(X1392,X1393)
| ssPv1(X1393)
| ssPv3(X1393)
| ssPv3(X1392) ),
inference(factor,[status(thm)],[c246]) ).
cnf(c611,plain,
( ~ ssRr(X1381,X1382)
| ~ ssPv1(X1382)
| ~ ssRr(X1381,X1381)
| ~ ssRr(X1382,X1380)
| ssPv1(X1380)
| ssPv3(X1381) ),
inference(factor,[status(thm)],[c245]) ).
cnf(c618,plain,
( ~ ssRr(X1385,X1386)
| ~ ssPv1(X1386)
| ~ ssRr(X1385,X1385)
| ssPv1(skf1(X1386))
| ssPv3(X1385) ),
inference(resolution,[status(thm)],[c611,clause1]) ).
cnf(c619,plain,
( ~ ssRr(X1391,X1391)
| ~ ssPv1(X1391)
| ssPv1(skf1(X1391))
| ssPv3(X1391) ),
inference(factor,[status(thm)],[c618]) ).
cnf(c238,plain,
( ~ ssRr(X1317,X1316)
| ~ ssPv2(X1316)
| ~ ssRr(X1315,X1317)
| ~ ssRr(X1315,X1318)
| ~ ssRr(X1315,X1315)
| ssPv1(X1318)
| ssPv4(X1315) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c583,plain,
( ~ ssRr(X1345,X1346)
| ~ ssPv2(X1346)
| ~ ssRr(X1347,X1345)
| ~ ssRr(X1347,X1347)
| ssPv1(X1347)
| ssPv4(X1347) ),
inference(factor,[status(thm)],[c238]) ).
cnf(c582,plain,
( ~ ssRr(X1325,X1323)
| ~ ssPv2(X1323)
| ~ ssRr(X1325,X1325)
| ~ ssRr(X1325,X1324)
| ssPv1(X1324)
| ssPv4(X1325) ),
inference(factor,[status(thm)],[c238]) ).
cnf(c588,plain,
( ~ ssRr(X1337,X1338)
| ~ ssPv2(X1338)
| ~ ssRr(X1337,X1337)
| ssPv1(skf1(X1337))
| ssPv4(X1337) ),
inference(resolution,[status(thm)],[c582,clause1]) ).
cnf(c587,plain,
( ~ ssRr(X1335,X1334)
| ~ ssPv2(X1334)
| ~ ssRr(X1335,X1335)
| ssPv1(X1335)
| ssPv4(X1335) ),
inference(factor,[status(thm)],[c582]) ).
cnf(c586,plain,
( ~ ssRr(X1326,X1327)
| ~ ssPv2(X1327)
| ~ ssRr(X1326,X1326)
| ssPv1(X1327)
| ssPv4(X1326) ),
inference(factor,[status(thm)],[c582]) ).
cnf(c581,plain,
( ~ ssRr(X1320,X1320)
| ~ ssPv2(X1320)
| ~ ssRr(X1320,X1319)
| ssPv1(X1319)
| ssPv4(X1320) ),
inference(factor,[status(thm)],[c238]) ).
cnf(c585,plain,
( ~ ssRr(X1322,X1322)
| ~ ssPv2(X1322)
| ssPv1(skf1(X1322))
| ssPv4(X1322) ),
inference(resolution,[status(thm)],[c581,clause1]) ).
cnf(c495,plain,
( ~ ssRr(X1211,X1208)
| ~ ssPv4(X1208)
| ~ ssRr(X1209,X1211)
| ~ ssRr(X1211,X1210)
| ssPv4(X1210)
| ssPv4(X1211)
| ssPv1(X1209) ),
inference(factor,[status(thm)],[c208]) ).
cnf(c539,plain,
( ~ ssRr(X1219,X1218)
| ~ ssPv4(X1218)
| ~ ssRr(X1217,X1219)
| ssPv4(skf1(X1219))
| ssPv4(X1219)
| ssPv1(X1217) ),
inference(resolution,[status(thm)],[c495,clause1]) ).
cnf(c541,plain,
( ~ ssRr(skf1(X1313),X1312)
| ~ ssPv4(X1312)
| ssPv4(skf1(skf1(X1313)))
| ssPv4(skf1(X1313))
| ssPv1(X1313) ),
inference(resolution,[status(thm)],[c539,clause1]) ).
cnf(c562,plain,
( ~ ssRr(X1296,X1295)
| ~ ssPv4(X1295)
| ~ ssRr(X1294,X1296)
| ~ ssRr(X1294,X1294)
| ssPv1(X1294)
| ssPv2(skf1(X1294)) ),
inference(factor,[status(thm)],[c228]) ).
cnf(c557,plain,
( ~ ssRr(X1276,X1278)
| ~ ssPv4(X1278)
| ~ ssRr(X1277,X1276)
| ssPv1(X1278)
| ssPv4(X1276)
| ssPv1(X1277) ),
inference(factor,[status(thm)],[c520]) ).
cnf(c565,plain,
( ~ ssRr(skf1(X1281),X1280)
| ~ ssPv4(X1280)
| ssPv1(X1280)
| ssPv4(skf1(X1281))
| ssPv1(X1281) ),
inference(resolution,[status(thm)],[c557,clause1]) ).
cnf(c566,plain,
( ~ ssPv4(skf1(skf1(X1293)))
| ssPv1(skf1(skf1(X1293)))
| ssPv4(skf1(X1293))
| ssPv1(X1293) ),
inference(resolution,[status(thm)],[c565,clause1]) ).
cnf(c236,plain,
( ~ ssRr(X1288,X1289)
| ~ ssPv2(X1289)
| ~ ssRr(X1288,X1288)
| ~ ssRr(X1287,X1286)
| ~ ssRr(X1288,X1287)
| ssPv1(X1286)
| ssPv1(X1289)
| ssPv4(X1288) ),
inference(factor,[status(thm)],[clause37]) ).
cnf(c571,plain,
( ~ ssRr(X1290,X1291)
| ~ ssPv2(X1291)
| ~ ssRr(X1290,X1290)
| ssPv1(X1290)
| ssPv1(X1291)
| ssPv4(X1290) ),
inference(factor,[status(thm)],[c236]) ).
cnf(c573,plain,
( ~ ssRr(X1292,X1292)
| ~ ssPv2(X1292)
| ssPv1(X1292)
| ssPv4(X1292) ),
inference(factor,[status(thm)],[c571]) ).
cnf(c226,plain,
( ~ ssRr(X1238,X1237)
| ~ ssPv4(X1237)
| ~ ssRr(X1235,X1238)
| ~ ssRr(X1235,X1236)
| ~ ssRr(X1235,X1235)
| ssPv1(X1236)
| ssPv2(X1236)
| ssPv1(X1235) ),
inference(factor,[status(thm)],[clause36]) ).
cnf(c550,plain,
( ~ ssRr(X1242,X1243)
| ~ ssPv4(X1243)
| ~ ssRr(X1241,X1242)
| ~ ssRr(X1241,X1241)
| ssPv1(X1241)
| ssPv2(X1241) ),
inference(factor,[status(thm)],[c226]) ).
cnf(c544,plain,
( ~ ssRr(X1228,X1226)
| ~ ssPv4(X1226)
| ~ ssRr(X1227,X1228)
| ~ ssRr(X1227,X1227)
| ssPv1(X1227)
| ssPv2(X1228) ),
inference(factor,[status(thm)],[c225]) ).
cnf(clause33,negated_conjecture,
( ~ ssRr(X407,X409)
| ~ ssPv4(X409)
| ~ ssRr(X410,X407)
| ~ ssRr(X406,X408)
| ~ ssPv3(X408)
| ~ ssRr(X410,X406)
| ~ ssPv3(X410)
| ssPv2(X410) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(c203,plain,
( ~ ssRr(X1026,X1029)
| ~ ssPv4(X1029)
| ~ ssRr(X1028,X1026)
| ~ ssRr(skf1(X1028),X1027)
| ~ ssPv3(X1027)
| ~ ssPv3(X1028)
| ssPv2(X1028) ),
inference(resolution,[status(thm)],[clause33,clause1]) ).
cnf(c488,plain,
( ~ ssRr(X1200,X1199)
| ~ ssPv4(X1199)
| ~ ssRr(X1198,X1200)
| ~ ssPv3(skf1(skf1(X1198)))
| ~ ssPv3(X1198)
| ssPv2(X1198) ),
inference(resolution,[status(thm)],[c203,clause1]) ).
cnf(c533,plain,
( ~ ssRr(X1192,X1191)
| ~ ssPv4(X1191)
| ~ ssRr(X1190,X1192)
| ~ ssRr(X1190,X1190)
| ssPv1(X1190)
| ssPv4(skf1(X1190)) ),
inference(factor,[status(thm)],[c219]) ).
cnf(clause32,negated_conjecture,
( ~ ssRr(X393,X395)
| ~ ssPv2(X395)
| ~ ssRr(X396,X393)
| ~ ssRr(X392,X394)
| ~ ssRr(X396,X392)
| ~ ssPv3(X396)
| ~ ssPv4(X396)
| ssPv4(X394) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c195,plain,
( ~ ssRr(X1002,X1000)
| ~ ssPv2(X1000)
| ~ ssRr(X1001,X1002)
| ~ ssRr(skf1(X1001),X999)
| ~ ssPv3(X1001)
| ~ ssPv4(X1001)
| ssPv4(X999) ),
inference(resolution,[status(thm)],[clause32,clause1]) ).
cnf(c477,plain,
( ~ ssRr(X1181,X1180)
| ~ ssPv2(X1180)
| ~ ssRr(X1179,X1181)
| ~ ssPv3(X1179)
| ~ ssPv4(X1179)
| ssPv4(skf1(skf1(X1179))) ),
inference(resolution,[status(thm)],[c195,clause1]) ).
cnf(c529,plain,
( ~ ssRr(X1182,X1182)
| ~ ssPv2(X1182)
| ~ ssPv3(X1182)
| ~ ssPv4(X1182)
| ssPv4(skf1(skf1(X1182))) ),
inference(factor,[status(thm)],[c477]) ).
cnf(clause31,negated_conjecture,
( ~ ssRr(X377,X379)
| ~ ssPv4(X379)
| ~ ssRr(X380,X377)
| ~ ssRr(X380,X376)
| ~ ssPv1(X376)
| ~ ssRr(X380,X378)
| ~ ssPv4(X380)
| ssPv3(X378) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(c184,plain,
( ~ ssRr(X948,X947)
| ~ ssPv4(X947)
| ~ ssRr(X950,X948)
| ~ ssRr(X950,X949)
| ~ ssPv1(X949)
| ~ ssPv4(X950)
| ssPv3(X949) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c458,plain,
( ~ ssRr(X1165,X1163)
| ~ ssPv4(X1163)
| ~ ssRr(X1164,X1165)
| ~ ssPv1(skf1(X1164))
| ~ ssPv4(X1164)
| ssPv3(skf1(X1164)) ),
inference(resolution,[status(thm)],[c184,clause1]) ).
cnf(clause30,negated_conjecture,
( ~ ssRr(X363,X365)
| ~ ssPv3(X365)
| ~ ssRr(X366,X363)
| ~ ssRr(X362,X364)
| ~ ssPv1(X364)
| ~ ssRr(X366,X362)
| ssPv1(X366)
| ssPv2(X366) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(c178,plain,
( ~ ssRr(X922,X924)
| ~ ssPv3(X924)
| ~ ssRr(X921,X922)
| ~ ssRr(skf1(X921),X923)
| ~ ssPv1(X923)
| ssPv1(X921)
| ssPv2(X921) ),
inference(resolution,[status(thm)],[clause30,clause1]) ).
cnf(c444,plain,
( ~ ssRr(X1160,X1162)
| ~ ssPv3(X1162)
| ~ ssRr(X1161,X1160)
| ~ ssPv1(skf1(skf1(X1161)))
| ssPv1(X1161)
| ssPv2(X1161) ),
inference(resolution,[status(thm)],[c178,clause1]) ).
cnf(c521,plain,
( ~ ssRr(X1140,X1141)
| ~ ssPv4(X1141)
| ~ ssRr(X1142,X1140)
| ~ ssRr(X1142,X1142)
| ssPv1(X1142)
| ssPv4(X1140) ),
inference(factor,[status(thm)],[c216]) ).
cnf(clause27,negated_conjecture,
( ~ ssRr(X320,X322)
| ~ ssPv4(X322)
| ~ ssRr(X323,X320)
| ~ ssRr(X319,X321)
| ~ ssRr(X323,X319)
| ~ ssPv4(X323)
| ssPv4(X321)
| ssPv1(X323) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c153,plain,
( ~ ssRr(X850,X852)
| ~ ssPv4(X852)
| ~ ssRr(X851,X850)
| ~ ssRr(skf1(X851),X849)
| ~ ssPv4(X851)
| ssPv4(X849)
| ssPv1(X851) ),
inference(resolution,[status(thm)],[clause27,clause1]) ).
cnf(c418,plain,
( ~ ssRr(X1133,X1131)
| ~ ssPv4(X1131)
| ~ ssRr(X1132,X1133)
| ~ ssPv4(X1132)
| ssPv4(skf1(skf1(X1132)))
| ssPv1(X1132) ),
inference(resolution,[status(thm)],[c153,clause1]) ).
cnf(clause25,negated_conjecture,
( ~ ssRr(X287,X289)
| ~ ssPv1(X289)
| ~ ssRr(X290,X287)
| ~ ssRr(X286,X288)
| ~ ssRr(X290,X286)
| ~ ssPv3(X290)
| ssPv3(X288)
| ssPv4(X290) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(c139,plain,
( ~ ssRr(X823,X824)
| ~ ssPv1(X824)
| ~ ssRr(X822,X823)
| ~ ssRr(skf1(X822),X821)
| ~ ssPv3(X822)
| ssPv3(X821)
| ssPv4(X822) ),
inference(resolution,[status(thm)],[clause25,clause1]) ).
cnf(c407,plain,
( ~ ssRr(X1116,X1118)
| ~ ssPv1(X1118)
| ~ ssRr(X1117,X1116)
| ~ ssPv3(X1117)
| ssPv3(skf1(skf1(X1117)))
| ssPv4(X1117) ),
inference(resolution,[status(thm)],[c139,clause1]) ).
cnf(clause28,negated_conjecture,
( ~ ssRr(X333,X335)
| ~ ssRr(X336,X333)
| ~ ssRr(X336,X332)
| ~ ssPv2(X332)
| ~ ssRr(X336,X334)
| ~ ssPv2(X336)
| ssPv2(X335)
| ssPv4(X334) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c160,plain,
( ~ ssRr(X803,X804)
| ~ ssRr(X802,X803)
| ~ ssRr(X802,X805)
| ~ ssPv2(X805)
| ~ ssPv2(X802)
| ssPv2(X804)
| ssPv4(X805) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c400,plain,
( ~ ssRr(X1108,X1109)
| ~ ssRr(X1110,X1108)
| ~ ssPv2(skf1(X1110))
| ~ ssPv2(X1110)
| ssPv2(X1109)
| ssPv4(skf1(X1110)) ),
inference(resolution,[status(thm)],[c160,clause1]) ).
cnf(clause21,negated_conjecture,
( ~ ssRr(X224,X226)
| ~ ssRr(X227,X224)
| ~ ssRr(X223,X225)
| ~ ssRr(X227,X223)
| ~ ssPv4(X227)
| ssPv4(X226)
| ssPv2(X225)
| ssPv3(X227) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c114,plain,
( ~ ssRr(X762,X763)
| ~ ssRr(X761,X762)
| ~ ssRr(skf1(X761),X760)
| ~ ssPv4(X761)
| ssPv4(X763)
| ssPv2(X760)
| ssPv3(X761) ),
inference(resolution,[status(thm)],[clause21,clause1]) ).
cnf(c387,plain,
( ~ ssRr(X1099,X1098)
| ~ ssRr(X1097,X1099)
| ~ ssPv4(X1097)
| ssPv4(X1098)
| ssPv2(skf1(skf1(X1097)))
| ssPv3(X1097) ),
inference(resolution,[status(thm)],[c114,clause1]) ).
cnf(c209,plain,
( ~ ssRr(X1075,X1073)
| ~ ssPv4(X1073)
| ~ ssRr(X1074,X1075)
| ~ ssRr(X1074,X1072)
| ~ ssRr(X1074,X1074)
| ssPv4(X1072)
| ssPv1(X1074) ),
inference(factor,[status(thm)],[clause34]) ).
cnf(c502,plain,
( ~ ssRr(X1081,X1083)
| ~ ssPv4(X1083)
| ~ ssRr(X1082,X1081)
| ~ ssRr(X1082,X1082)
| ssPv4(X1082)
| ssPv1(X1082) ),
inference(factor,[status(thm)],[c209]) ).
cnf(clause20,negated_conjecture,
( ~ ssRr(X210,X212)
| ~ ssRr(X213,X210)
| ~ ssRr(X209,X211)
| ~ ssRr(X213,X209)
| ~ ssPv3(X213)
| ssPv3(X212)
| ssPv1(X211)
| ssPv4(X213) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c106,plain,
( ~ ssRr(X745,X746)
| ~ ssRr(X747,X745)
| ~ ssRr(skf1(X747),X748)
| ~ ssPv3(X747)
| ssPv3(X746)
| ssPv1(X748)
| ssPv4(X747) ),
inference(resolution,[status(thm)],[clause20,clause1]) ).
cnf(c382,plain,
( ~ ssRr(X1068,X1067)
| ~ ssRr(X1066,X1068)
| ~ ssPv3(X1066)
| ssPv3(X1067)
| ssPv1(skf1(skf1(X1066)))
| ssPv4(X1066) ),
inference(resolution,[status(thm)],[c106,clause1]) ).
cnf(clause26,negated_conjecture,
( ~ ssRr(X302,X304)
| ~ ssPv4(X304)
| ~ ssRr(X305,X302)
| ~ ssRr(X305,X301)
| ~ ssPv4(X301)
| ~ ssRr(X305,X303)
| ssPv1(X303)
| ssPv1(X305) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c146,plain,
( ~ ssRr(X730,X731)
| ~ ssPv4(X731)
| ~ ssRr(X729,X730)
| ~ ssRr(X729,X732)
| ~ ssPv4(X732)
| ssPv1(X732)
| ssPv1(X729) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c377,plain,
( ~ ssRr(X1054,X1055)
| ~ ssPv4(X1055)
| ~ ssRr(X1053,X1054)
| ~ ssPv4(skf1(X1053))
| ssPv1(skf1(X1053))
| ssPv1(X1053) ),
inference(resolution,[status(thm)],[c146,clause1]) ).
cnf(c492,plain,
( ~ ssRr(X1057,skf1(X1056))
| ~ ssPv4(skf1(X1056))
| ~ ssRr(X1056,X1057)
| ssPv1(skf1(X1056))
| ssPv1(X1056) ),
inference(factor,[status(thm)],[c377]) ).
cnf(clause19,negated_conjecture,
( ~ ssRr(X196,X198)
| ~ ssRr(X199,X196)
| ~ ssRr(X195,X197)
| ~ ssRr(X199,X195)
| ~ ssPv1(X199)
| ssPv3(X198)
| ssPv2(X197)
| ssPv3(X199) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c99,plain,
( ~ ssRr(X725,X726)
| ~ ssRr(X727,X725)
| ~ ssRr(skf1(X727),X728)
| ~ ssPv1(X727)
| ssPv3(X726)
| ssPv2(X728)
| ssPv3(X727) ),
inference(resolution,[status(thm)],[clause19,clause1]) ).
cnf(c374,plain,
( ~ ssRr(X1047,X1048)
| ~ ssRr(X1049,X1047)
| ~ ssPv1(X1049)
| ssPv3(X1048)
| ssPv2(skf1(skf1(X1049)))
| ssPv3(X1049) ),
inference(resolution,[status(thm)],[c99,clause1]) ).
cnf(c490,plain,
( ~ ssRr(X1050,X1050)
| ~ ssPv1(X1050)
| ssPv3(X1050)
| ssPv2(skf1(skf1(X1050))) ),
inference(factor,[status(thm)],[c374]) ).
cnf(clause23,negated_conjecture,
( ~ ssRr(X253,X255)
| ~ ssRr(X256,X253)
| ~ ssRr(X256,X252)
| ~ ssPv3(X252)
| ~ ssRr(X256,X254)
| ~ ssPv1(X254)
| ssPv3(X255)
| ssPv4(X256) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(c126,plain,
( ~ ssRr(X590,X591)
| ~ ssRr(X592,X590)
| ~ ssRr(X592,X589)
| ~ ssPv3(X589)
| ~ ssPv1(X589)
| ssPv3(X591)
| ssPv4(X592) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c305,plain,
( ~ ssRr(X1040,X1038)
| ~ ssRr(X1039,X1040)
| ~ ssPv3(skf1(X1039))
| ~ ssPv1(skf1(X1039))
| ssPv3(X1038)
| ssPv4(X1039) ),
inference(resolution,[status(thm)],[c126,clause1]) ).
cnf(clause22,negated_conjecture,
( ~ ssRr(X237,X239)
| ~ ssRr(X240,X237)
| ~ ssRr(X240,X236)
| ~ ssPv4(X236)
| ~ ssRr(X240,X238)
| ~ ssPv1(X238)
| ssPv4(X239)
| ssPv4(X240) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(c120,plain,
( ~ ssRr(X538,X536)
| ~ ssRr(X537,X538)
| ~ ssRr(X537,X539)
| ~ ssPv4(X539)
| ~ ssPv1(X539)
| ssPv4(X536)
| ssPv4(X537) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c277,plain,
( ~ ssRr(X1035,X1036)
| ~ ssRr(X1037,X1035)
| ~ ssPv4(skf1(X1037))
| ~ ssPv1(skf1(X1037))
| ssPv4(X1036)
| ssPv4(X1037) ),
inference(resolution,[status(thm)],[c120,clause1]) ).
cnf(c201,plain,
( ~ ssRr(X1015,X1016)
| ~ ssPv4(X1016)
| ~ ssRr(X1014,X1015)
| ~ ssRr(X1015,X1013)
| ~ ssPv3(X1013)
| ~ ssPv3(X1014)
| ssPv2(X1014) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c483,plain,
( ~ ssRr(X1032,X1031)
| ~ ssPv4(X1031)
| ~ ssRr(X1030,X1032)
| ~ ssPv3(skf1(X1032))
| ~ ssPv3(X1030)
| ssPv2(X1030) ),
inference(resolution,[status(thm)],[c201,clause1]) ).
cnf(c489,plain,
( ~ ssRr(X1034,X1033)
| ~ ssPv4(X1033)
| ~ ssRr(skf1(X1034),X1034)
| ~ ssPv3(skf1(X1034))
| ssPv2(skf1(X1034)) ),
inference(factor,[status(thm)],[c483]) ).
cnf(c481,plain,
( ~ ssRr(X1021,X1019)
| ~ ssPv4(X1019)
| ~ ssRr(X1020,X1021)
| ~ ssPv3(X1019)
| ~ ssPv3(X1020)
| ssPv2(X1020) ),
inference(factor,[status(thm)],[c201]) ).
cnf(c485,plain,
( ~ ssRr(skf1(X1024),X1023)
| ~ ssPv4(X1023)
| ~ ssPv3(X1023)
| ~ ssPv3(X1024)
| ssPv2(X1024) ),
inference(resolution,[status(thm)],[c481,clause1]) ).
cnf(c486,plain,
( ~ ssPv4(skf1(skf1(X1025)))
| ~ ssPv3(skf1(skf1(X1025)))
| ~ ssPv3(X1025)
| ssPv2(X1025) ),
inference(resolution,[status(thm)],[c485,clause1]) ).
cnf(c193,plain,
( ~ ssRr(X986,X985)
| ~ ssPv2(X985)
| ~ ssRr(X984,X986)
| ~ ssRr(X986,X983)
| ~ ssPv3(X984)
| ~ ssPv4(X984)
| ssPv4(X983) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c472,plain,
( ~ ssRr(X1004,X1005)
| ~ ssPv2(X1005)
| ~ ssRr(X1003,X1004)
| ~ ssPv3(X1003)
| ~ ssPv4(X1003)
| ssPv4(skf1(X1004)) ),
inference(resolution,[status(thm)],[c193,clause1]) ).
cnf(c479,plain,
( ~ ssRr(skf1(X1008),X1007)
| ~ ssPv2(X1007)
| ~ ssPv3(X1008)
| ~ ssPv4(X1008)
| ssPv4(skf1(skf1(X1008))) ),
inference(resolution,[status(thm)],[c472,clause1]) ).
cnf(c470,plain,
( ~ ssRr(X990,X992)
| ~ ssPv2(X992)
| ~ ssRr(X991,X990)
| ~ ssPv3(X991)
| ~ ssPv4(X991)
| ssPv4(X992) ),
inference(factor,[status(thm)],[c193]) ).
cnf(c474,plain,
( ~ ssRr(skf1(X995),X994)
| ~ ssPv2(X994)
| ~ ssPv3(X995)
| ~ ssPv4(X995)
| ssPv4(X994) ),
inference(resolution,[status(thm)],[c470,clause1]) ).
cnf(c475,plain,
( ~ ssPv2(skf1(skf1(X998)))
| ~ ssPv3(X998)
| ~ ssPv4(X998)
| ssPv4(skf1(skf1(X998))) ),
inference(resolution,[status(thm)],[c474,clause1]) ).
cnf(c192,plain,
( ~ ssRr(X976,X977)
| ~ ssPv2(X977)
| ~ ssRr(X976,X976)
| ~ ssRr(X977,X975)
| ~ ssPv3(X976)
| ~ ssPv4(X976)
| ssPv4(X975) ),
inference(factor,[status(thm)],[clause32]) ).
cnf(c468,plain,
( ~ ssRr(X980,X981)
| ~ ssPv2(X981)
| ~ ssRr(X980,X980)
| ~ ssPv3(X980)
| ~ ssPv4(X980)
| ssPv4(skf1(X981)) ),
inference(resolution,[status(thm)],[c192,clause1]) ).
cnf(c469,plain,
( ~ ssRr(X982,X982)
| ~ ssPv2(X982)
| ~ ssPv3(X982)
| ~ ssPv4(X982)
| ssPv4(skf1(X982)) ),
inference(factor,[status(thm)],[c468]) ).
cnf(c185,plain,
( ~ ssRr(X964,X963)
| ~ ssPv4(X963)
| ~ ssRr(X965,X964)
| ~ ssRr(X965,X962)
| ~ ssPv1(X962)
| ~ ssPv4(X965)
| ssPv3(skf1(X965)) ),
inference(resolution,[status(thm)],[clause31,clause1]) ).
cnf(c461,plain,
( ~ ssRr(X971,X969)
| ~ ssPv4(X969)
| ~ ssRr(X970,X971)
| ~ ssPv1(X971)
| ~ ssPv4(X970)
| ssPv3(skf1(X970)) ),
inference(factor,[status(thm)],[c185]) ).
cnf(c460,plain,
( ~ ssRr(X966,X967)
| ~ ssPv4(X967)
| ~ ssRr(X966,X966)
| ~ ssPv1(X967)
| ~ ssPv4(X966)
| ssPv3(skf1(X966)) ),
inference(factor,[status(thm)],[c185]) ).
cnf(c463,plain,
( ~ ssRr(X968,X968)
| ~ ssPv4(X968)
| ~ ssPv1(X968)
| ssPv3(skf1(X968)) ),
inference(factor,[status(thm)],[c460]) ).
cnf(c183,plain,
( ~ ssRr(X935,X934)
| ~ ssPv4(X934)
| ~ ssRr(X937,X935)
| ~ ssRr(X937,X936)
| ~ ssPv1(X936)
| ~ ssPv4(X937)
| ssPv3(X935) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c451,plain,
( ~ ssRr(X943,X942)
| ~ ssPv4(X942)
| ~ ssRr(X941,X943)
| ~ ssPv1(X943)
| ~ ssPv4(X941)
| ssPv3(X943) ),
inference(factor,[status(thm)],[c183]) ).
cnf(c455,plain,
( ~ ssRr(skf1(X960),X959)
| ~ ssPv4(X959)
| ~ ssPv1(skf1(X960))
| ~ ssPv4(X960)
| ssPv3(skf1(X960)) ),
inference(resolution,[status(thm)],[c451,clause1]) ).
cnf(c459,plain,
( ~ ssPv4(skf1(skf1(X961)))
| ~ ssPv1(skf1(X961))
| ~ ssPv4(X961)
| ssPv3(skf1(X961)) ),
inference(resolution,[status(thm)],[c455,clause1]) ).
cnf(c452,plain,
( ~ ssRr(X958,X957)
| ~ ssPv4(X957)
| ~ ssRr(X956,X958)
| ~ ssPv1(skf1(X956))
| ~ ssPv4(X956)
| ssPv3(X958) ),
inference(resolution,[status(thm)],[c183,clause1]) ).
cnf(c182,plain,
( ~ ssRr(X927,X925)
| ~ ssPv4(X925)
| ~ ssRr(X927,X927)
| ~ ssRr(X927,X926)
| ~ ssPv1(X926)
| ~ ssPv4(X927)
| ssPv3(X925) ),
inference(factor,[status(thm)],[clause31]) ).
cnf(c447,plain,
( ~ ssRr(X946,X945)
| ~ ssPv4(X945)
| ~ ssRr(X946,X946)
| ~ ssPv1(skf1(X946))
| ~ ssPv4(X946)
| ssPv3(X945) ),
inference(resolution,[status(thm)],[c182,clause1]) ).
cnf(c446,plain,
( ~ ssRr(X931,X932)
| ~ ssPv4(X932)
| ~ ssRr(X931,X931)
| ~ ssPv1(X931)
| ~ ssPv4(X931)
| ssPv3(X932) ),
inference(factor,[status(thm)],[c182]) ).
cnf(c445,plain,
( ~ ssRr(X929,X928)
| ~ ssPv4(X928)
| ~ ssRr(X929,X929)
| ~ ssPv1(X928)
| ~ ssPv4(X929)
| ssPv3(X928) ),
inference(factor,[status(thm)],[c182]) ).
cnf(c448,plain,
( ~ ssRr(X930,X930)
| ~ ssPv4(X930)
| ~ ssPv1(X930)
| ssPv3(X930) ),
inference(factor,[status(thm)],[c445]) ).
cnf(c176,plain,
( ~ ssRr(X903,X904)
| ~ ssPv3(X904)
| ~ ssRr(X902,X903)
| ~ ssRr(X903,X905)
| ~ ssPv1(X905)
| ssPv1(X902)
| ssPv2(X902) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c439,plain,
( ~ ssRr(X920,X919)
| ~ ssPv3(X919)
| ~ ssRr(X918,X920)
| ~ ssPv1(skf1(X920))
| ssPv1(X918)
| ssPv2(X918) ),
inference(resolution,[status(thm)],[c176,clause1]) ).
cnf(c437,plain,
( ~ ssRr(X906,X907)
| ~ ssPv3(X907)
| ~ ssRr(X908,X906)
| ~ ssPv1(X907)
| ssPv1(X908)
| ssPv2(X908) ),
inference(factor,[status(thm)],[c176]) ).
cnf(c441,plain,
( ~ ssRr(skf1(X914),X913)
| ~ ssPv3(X913)
| ~ ssPv1(X913)
| ssPv1(X914)
| ssPv2(X914) ),
inference(resolution,[status(thm)],[c437,clause1]) ).
cnf(c442,plain,
( ~ ssPv3(skf1(skf1(X917)))
| ~ ssPv1(skf1(skf1(X917)))
| ssPv1(X917)
| ssPv2(X917) ),
inference(resolution,[status(thm)],[c441,clause1]) ).
cnf(c175,plain,
( ~ ssRr(X895,X896)
| ~ ssPv3(X896)
| ~ ssRr(X895,X895)
| ~ ssRr(X896,X897)
| ~ ssPv1(X897)
| ssPv1(X895)
| ssPv2(X895) ),
inference(factor,[status(thm)],[clause30]) ).
cnf(c436,plain,
( ~ ssRr(X900,X901)
| ~ ssPv3(X901)
| ~ ssRr(X900,X900)
| ~ ssPv1(skf1(X901))
| ssPv1(X900)
| ssPv2(X900) ),
inference(resolution,[status(thm)],[c175,clause1]) ).
cnf(clause29,negated_conjecture,
( ~ ssRr(X349,X351)
| ~ ssRr(X352,X349)
| ~ ssRr(X352,X348)
| ~ ssPv3(X348)
| ~ ssRr(X352,X350)
| ~ ssPv4(X352)
| ssPv1(X351)
| ssPv3(X350) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(c171,plain,
( ~ ssRr(X882,X884)
| ~ ssRr(X885,X882)
| ~ ssRr(X885,X883)
| ~ ssPv3(X883)
| ~ ssPv4(X885)
| ssPv1(X884)
| ssPv3(skf1(X885)) ),
inference(resolution,[status(thm)],[clause29,clause1]) ).
cnf(c429,plain,
( ~ ssRr(X890,X889)
| ~ ssRr(X891,X890)
| ~ ssPv3(X890)
| ~ ssPv4(X891)
| ssPv1(X889)
| ssPv3(skf1(X891)) ),
inference(factor,[status(thm)],[c171]) ).
cnf(c428,plain,
( ~ ssRr(X887,X886)
| ~ ssRr(X887,X887)
| ~ ssPv3(X886)
| ~ ssPv4(X887)
| ssPv1(X886)
| ssPv3(skf1(X887)) ),
inference(factor,[status(thm)],[c171]) ).
cnf(c161,plain,
( ~ ssRr(X867,X868)
| ~ ssRr(X869,X867)
| ~ ssRr(X869,X866)
| ~ ssPv2(X866)
| ~ ssPv2(X869)
| ssPv2(X868)
| ssPv4(skf1(X869)) ),
inference(resolution,[status(thm)],[clause28,clause1]) ).
cnf(c424,plain,
( ~ ssRr(X873,X872)
| ~ ssRr(X874,X873)
| ~ ssPv2(X873)
| ~ ssPv2(X874)
| ssPv2(X872)
| ssPv4(skf1(X874)) ),
inference(factor,[status(thm)],[c161]) ).
cnf(c169,plain,
( ~ ssRr(X853,X855)
| ~ ssRr(X854,X853)
| ~ ssRr(X854,X856)
| ~ ssPv3(X856)
| ~ ssPv4(X854)
| ssPv1(X855)
| ssPv3(X853) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c421,plain,
( ~ ssRr(X863,X865)
| ~ ssRr(X864,X863)
| ~ ssPv3(skf1(X864))
| ~ ssPv4(X864)
| ssPv1(X865)
| ssPv3(X863) ),
inference(resolution,[status(thm)],[c169,clause1]) ).
cnf(c419,plain,
( ~ ssRr(X858,X857)
| ~ ssRr(X858,X858)
| ~ ssPv3(X857)
| ~ ssPv4(X858)
| ssPv1(X857)
| ssPv3(X858) ),
inference(factor,[status(thm)],[c169]) ).
cnf(c147,plain,
( ~ ssRr(X835,X837)
| ~ ssPv4(X837)
| ~ ssRr(X838,X835)
| ~ ssRr(X838,X836)
| ~ ssPv4(X836)
| ssPv1(skf1(X838))
| ssPv1(X838) ),
inference(resolution,[status(thm)],[clause26,clause1]) ).
cnf(c413,plain,
( ~ ssRr(X844,X843)
| ~ ssPv4(X843)
| ~ ssRr(X845,X844)
| ~ ssPv4(X844)
| ssPv1(skf1(X845))
| ssPv1(X845) ),
inference(factor,[status(thm)],[c147]) ).
cnf(c168,plain,
( ~ ssRr(X828,X827)
| ~ ssRr(X828,X828)
| ~ ssRr(X828,X829)
| ~ ssPv3(X829)
| ~ ssPv4(X828)
| ssPv1(X827)
| ssPv3(X827) ),
inference(factor,[status(thm)],[clause29]) ).
cnf(c410,plain,
( ~ ssRr(X842,X841)
| ~ ssRr(X842,X842)
| ~ ssPv3(skf1(X842))
| ~ ssPv4(X842)
| ssPv1(X841)
| ssPv3(X841) ),
inference(resolution,[status(thm)],[c168,clause1]) ).
cnf(c409,plain,
( ~ ssRr(X832,X833)
| ~ ssRr(X832,X832)
| ~ ssPv3(X832)
| ~ ssPv4(X832)
| ssPv1(X833)
| ssPv3(X833) ),
inference(factor,[status(thm)],[c168]) ).
cnf(clause24,negated_conjecture,
( ~ ssRr(X270,X272)
| ~ ssPv3(X272)
| ~ ssRr(X273,X270)
| ~ ssRr(X273,X269)
| ~ ssPv4(X269)
| ~ ssRr(X273,X271)
| ssPv4(X271)
| ssPv4(X273) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c133,plain,
( ~ ssRr(X806,X807)
| ~ ssPv3(X807)
| ~ ssRr(X809,X806)
| ~ ssRr(X809,X808)
| ~ ssPv4(X808)
| ssPv4(skf1(X809))
| ssPv4(X809) ),
inference(resolution,[status(thm)],[clause24,clause1]) ).
cnf(c402,plain,
( ~ ssRr(X817,X819)
| ~ ssPv3(X819)
| ~ ssRr(X818,X817)
| ~ ssPv4(X817)
| ssPv4(skf1(X818))
| ssPv4(X818) ),
inference(factor,[status(thm)],[c133]) ).
cnf(c159,plain,
( ~ ssRr(X785,X784)
| ~ ssRr(X782,X785)
| ~ ssRr(X782,X783)
| ~ ssPv2(X783)
| ~ ssPv2(X782)
| ssPv2(X784)
| ssPv4(X785) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c393,plain,
( ~ ssRr(X789,X790)
| ~ ssRr(X788,X789)
| ~ ssPv2(X789)
| ~ ssPv2(X788)
| ssPv2(X790)
| ssPv4(X789) ),
inference(factor,[status(thm)],[c159]) ).
cnf(c396,plain,
( ~ ssRr(skf1(X800),X799)
| ~ ssPv2(skf1(X800))
| ~ ssPv2(X800)
| ssPv2(X799)
| ssPv4(skf1(X800)) ),
inference(resolution,[status(thm)],[c393,clause1]) ).
cnf(c397,plain,
( ~ ssPv2(skf1(X801))
| ~ ssPv2(X801)
| ssPv2(skf1(skf1(X801)))
| ssPv4(skf1(X801)) ),
inference(resolution,[status(thm)],[c396,clause1]) ).
cnf(c394,plain,
( ~ ssRr(X798,X796)
| ~ ssRr(X797,X798)
| ~ ssPv2(skf1(X797))
| ~ ssPv2(X797)
| ssPv2(X796)
| ssPv4(X798) ),
inference(resolution,[status(thm)],[c159,clause1]) ).
cnf(c127,plain,
( ~ ssRr(X792,X793)
| ~ ssRr(X794,X792)
| ~ ssRr(X794,X791)
| ~ ssPv3(X791)
| ~ ssPv1(skf1(X794))
| ssPv3(X793)
| ssPv4(X794) ),
inference(resolution,[status(thm)],[clause23,clause1]) ).
cnf(c121,plain,
( ~ ssRr(X775,X774)
| ~ ssRr(X776,X775)
| ~ ssRr(X776,X777)
| ~ ssPv4(X777)
| ~ ssPv1(skf1(X776))
| ssPv4(X774)
| ssPv4(X776) ),
inference(resolution,[status(thm)],[clause22,clause1]) ).
cnf(c158,plain,
( ~ ssRr(X769,X770)
| ~ ssRr(X769,X769)
| ~ ssRr(X769,X768)
| ~ ssPv2(X768)
| ~ ssPv2(X769)
| ssPv2(X770)
| ssPv4(X770) ),
inference(factor,[status(thm)],[clause28]) ).
cnf(c389,plain,
( ~ ssRr(X771,X772)
| ~ ssRr(X771,X771)
| ~ ssPv2(X771)
| ssPv2(X772)
| ssPv4(X772) ),
inference(factor,[status(thm)],[c158]) ).
cnf(c151,plain,
( ~ ssRr(X744,X742)
| ~ ssPv4(X742)
| ~ ssRr(X743,X744)
| ~ ssRr(X744,X741)
| ~ ssPv4(X743)
| ssPv4(X741)
| ssPv1(X743) ),
inference(factor,[status(thm)],[clause27]) ).
cnf(c380,plain,
( ~ ssRr(X755,X756)
| ~ ssPv4(X756)
| ~ ssRr(X754,X755)
| ~ ssPv4(X754)
| ssPv4(skf1(X755))
| ssPv1(X754) ),
inference(resolution,[status(thm)],[c151,clause1]) ).
cnf(c384,plain,
( ~ ssRr(skf1(X759),X758)
| ~ ssPv4(X758)
| ~ ssPv4(X759)
| ssPv4(skf1(skf1(X759)))
| ssPv1(X759) ),
inference(resolution,[status(thm)],[c380,clause1]) ).
cnf(c145,plain,
( ~ ssRr(X701,X700)
| ~ ssPv4(X700)
| ~ ssRr(X698,X701)
| ~ ssRr(X698,X699)
| ~ ssPv4(X699)
| ssPv1(X701)
| ssPv1(X698) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c359,plain,
( ~ ssRr(X706,X707)
| ~ ssPv4(X707)
| ~ ssRr(X705,X706)
| ~ ssPv4(X706)
| ssPv1(X706)
| ssPv1(X705) ),
inference(factor,[status(thm)],[c145]) ).
cnf(c363,plain,
( ~ ssRr(skf1(X722),X723)
| ~ ssPv4(X723)
| ~ ssPv4(skf1(X722))
| ssPv1(skf1(X722))
| ssPv1(X722) ),
inference(resolution,[status(thm)],[c359,clause1]) ).
cnf(c372,plain,
( ~ ssPv4(skf1(skf1(X724)))
| ~ ssPv4(skf1(X724))
| ssPv1(skf1(X724))
| ssPv1(X724) ),
inference(resolution,[status(thm)],[c363,clause1]) ).
cnf(c360,plain,
( ~ ssRr(X716,X718)
| ~ ssPv4(X718)
| ~ ssRr(X717,X716)
| ~ ssPv4(skf1(X717))
| ssPv1(X716)
| ssPv1(X717) ),
inference(resolution,[status(thm)],[c145,clause1]) ).
cnf(c370,plain,
( ~ ssRr(X719,skf1(X720))
| ~ ssPv4(skf1(X720))
| ~ ssRr(X720,X719)
| ssPv1(X719)
| ssPv1(X720) ),
inference(factor,[status(thm)],[c360]) ).
cnf(c371,plain,
( ~ ssPv4(skf1(X721))
| ~ ssRr(X721,X721)
| ssPv1(X721) ),
inference(resolution,[status(thm)],[c370,clause1]) ).
cnf(c358,plain,
( ~ ssRr(X702,X703)
| ~ ssPv4(X703)
| ~ ssRr(X702,X702)
| ssPv1(X702) ),
inference(factor,[status(thm)],[c145]) ).
cnf(c144,plain,
( ~ ssRr(X682,X683)
| ~ ssPv4(X683)
| ~ ssRr(X682,X682)
| ~ ssRr(X682,X681)
| ~ ssPv4(X681)
| ssPv1(X683)
| ssPv1(X682) ),
inference(factor,[status(thm)],[clause26]) ).
cnf(c348,plain,
( ~ ssRr(X685,X684)
| ~ ssPv4(X684)
| ~ ssRr(X685,X685)
| ssPv1(X684)
| ssPv1(X685) ),
inference(factor,[status(thm)],[c144]) ).
cnf(c351,plain,
( ~ ssRr(X686,X686)
| ~ ssPv4(X686)
| ssPv1(X686) ),
inference(factor,[status(thm)],[c348]) ).
cnf(c137,plain,
( ~ ssRr(X642,X641)
| ~ ssPv1(X641)
| ~ ssRr(X639,X642)
| ~ ssRr(X642,X640)
| ~ ssPv3(X639)
| ssPv3(X640)
| ssPv4(X639) ),
inference(factor,[status(thm)],[clause25]) ).
cnf(c325,plain,
( ~ ssRr(X666,X665)
| ~ ssPv1(X665)
| ~ ssRr(X664,X666)
| ~ ssPv3(X664)
| ssPv3(skf1(X666))
| ssPv4(X664) ),
inference(resolution,[status(thm)],[c137,clause1]) ).
cnf(c340,plain,
( ~ ssRr(skf1(X668),X669)
| ~ ssPv1(X669)
| ~ ssPv3(X668)
| ssPv3(skf1(skf1(X668)))
| ssPv4(X668) ),
inference(resolution,[status(thm)],[c325,clause1]) ).
cnf(c323,plain,
( ~ ssRr(X650,X651)
| ~ ssPv1(X651)
| ~ ssRr(X649,X650)
| ~ ssPv3(X649)
| ssPv3(X651)
| ssPv4(X649) ),
inference(factor,[status(thm)],[c137]) ).
cnf(c332,plain,
( ~ ssRr(skf1(X654),X653)
| ~ ssPv1(X653)
| ~ ssPv3(X654)
| ssPv3(X653)
| ssPv4(X654) ),
inference(resolution,[status(thm)],[c323,clause1]) ).
cnf(c333,plain,
( ~ ssPv1(skf1(skf1(X657)))
| ~ ssPv3(X657)
| ssPv3(skf1(skf1(X657)))
| ssPv4(X657) ),
inference(resolution,[status(thm)],[c332,clause1]) ).
cnf(c131,plain,
( ~ ssRr(X616,X613)
| ~ ssPv3(X613)
| ~ ssRr(X614,X616)
| ~ ssRr(X614,X615)
| ~ ssPv4(X615)
| ssPv4(X616)
| ssPv4(X614) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c316,plain,
( ~ ssRr(X629,X630)
| ~ ssPv3(X630)
| ~ ssRr(X631,X629)
| ~ ssPv4(skf1(X631))
| ssPv4(X629)
| ssPv4(X631) ),
inference(resolution,[status(thm)],[c131,clause1]) ).
cnf(c314,plain,
( ~ ssRr(X618,X617)
| ~ ssPv3(X617)
| ~ ssRr(X618,X618)
| ~ ssPv4(X617)
| ssPv4(X618) ),
inference(factor,[status(thm)],[c131]) ).
cnf(c130,plain,
( ~ ssRr(X598,X600)
| ~ ssPv3(X600)
| ~ ssRr(X598,X598)
| ~ ssRr(X598,X599)
| ~ ssPv4(X599)
| ssPv4(X600)
| ssPv4(X598) ),
inference(factor,[status(thm)],[clause24]) ).
cnf(c308,plain,
( ~ ssRr(X612,X611)
| ~ ssPv3(X611)
| ~ ssRr(X612,X612)
| ~ ssPv4(skf1(X612))
| ssPv4(X611)
| ssPv4(X612) ),
inference(resolution,[status(thm)],[c130,clause1]) ).
cnf(c125,plain,
( ~ ssRr(X564,X562)
| ~ ssRr(X563,X564)
| ~ ssRr(X563,X561)
| ~ ssPv3(X561)
| ~ ssPv1(X564)
| ssPv3(X562)
| ssPv4(X563) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c288,plain,
( ~ ssRr(X575,X574)
| ~ ssRr(X573,X575)
| ~ ssPv3(X575)
| ~ ssPv1(X575)
| ssPv3(X574)
| ssPv4(X573) ),
inference(factor,[status(thm)],[c125]) ).
cnf(c296,plain,
( ~ ssRr(skf1(X581),X580)
| ~ ssPv3(skf1(X581))
| ~ ssPv1(skf1(X581))
| ssPv3(X580)
| ssPv4(X581) ),
inference(resolution,[status(thm)],[c288,clause1]) ).
cnf(c297,plain,
( ~ ssPv3(skf1(X582))
| ~ ssPv1(skf1(X582))
| ssPv3(skf1(skf1(X582)))
| ssPv4(X582) ),
inference(resolution,[status(thm)],[c296,clause1]) ).
cnf(c289,plain,
( ~ ssRr(X579,X578)
| ~ ssRr(X577,X579)
| ~ ssPv3(skf1(X577))
| ~ ssPv1(X579)
| ssPv3(X578)
| ssPv4(X577) ),
inference(resolution,[status(thm)],[c125,clause1]) ).
cnf(c124,plain,
( ~ ssRr(X547,X546)
| ~ ssRr(X547,X547)
| ~ ssRr(X547,X545)
| ~ ssPv3(X545)
| ~ ssPv1(X546)
| ssPv3(X546)
| ssPv4(X547) ),
inference(factor,[status(thm)],[clause23]) ).
cnf(c280,plain,
( ~ ssRr(X560,X559)
| ~ ssRr(X560,X560)
| ~ ssPv3(skf1(X560))
| ~ ssPv1(X559)
| ssPv3(X559)
| ssPv4(X560) ),
inference(resolution,[status(thm)],[c124,clause1]) ).
cnf(c119,plain,
( ~ ssRr(X508,X510)
| ~ ssRr(X509,X508)
| ~ ssRr(X509,X511)
| ~ ssPv4(X511)
| ~ ssPv1(X508)
| ssPv4(X510)
| ssPv4(X509) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c260,plain,
( ~ ssRr(X520,X522)
| ~ ssRr(X521,X520)
| ~ ssPv4(X520)
| ~ ssPv1(X520)
| ssPv4(X522)
| ssPv4(X521) ),
inference(factor,[status(thm)],[c119]) ).
cnf(c268,plain,
( ~ ssRr(skf1(X527),X528)
| ~ ssPv4(skf1(X527))
| ~ ssPv1(skf1(X527))
| ssPv4(X528)
| ssPv4(X527) ),
inference(resolution,[status(thm)],[c260,clause1]) ).
cnf(c269,plain,
( ~ ssPv4(skf1(X529))
| ~ ssPv1(skf1(X529))
| ssPv4(skf1(skf1(X529)))
| ssPv4(X529) ),
inference(resolution,[status(thm)],[c268,clause1]) ).
cnf(c261,plain,
( ~ ssRr(X524,X526)
| ~ ssRr(X525,X524)
| ~ ssPv4(skf1(X525))
| ~ ssPv1(X524)
| ssPv4(X526)
| ssPv4(X525) ),
inference(resolution,[status(thm)],[c119,clause1]) ).
cnf(c118,plain,
( ~ ssRr(X494,X493)
| ~ ssRr(X494,X494)
| ~ ssRr(X494,X495)
| ~ ssPv4(X495)
| ~ ssPv1(X493)
| ssPv4(X493)
| ssPv4(X494) ),
inference(factor,[status(thm)],[clause22]) ).
cnf(c253,plain,
( ~ ssRr(X507,X506)
| ~ ssRr(X507,X507)
| ~ ssPv4(skf1(X507))
| ~ ssPv1(X506)
| ssPv4(X506)
| ssPv4(X507) ),
inference(resolution,[status(thm)],[c118,clause1]) ).
cnf(c113,plain,
( ~ ssRr(X488,X489)
| ~ ssRr(X487,X488)
| ~ ssRr(X487,X487)
| ~ ssPv4(X487)
| ssPv4(X489)
| ssPv2(X487)
| ssPv3(X487) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c112,plain,
( ~ ssRr(X457,X455)
| ~ ssRr(X454,X457)
| ~ ssRr(X457,X456)
| ~ ssPv4(X454)
| ssPv4(X455)
| ssPv2(X456)
| ssPv3(X454) ),
inference(factor,[status(thm)],[clause21]) ).
cnf(c231,plain,
( ~ ssRr(X476,X475)
| ~ ssRr(X474,X476)
| ~ ssPv4(X474)
| ssPv4(X475)
| ssPv2(skf1(X476))
| ssPv3(X474) ),
inference(resolution,[status(thm)],[c112,clause1]) ).
cnf(c242,plain,
( ~ ssRr(skf1(X479),X478)
| ~ ssPv4(X479)
| ssPv4(X478)
| ssPv2(skf1(skf1(X479)))
| ssPv3(X479) ),
inference(resolution,[status(thm)],[c231,clause1]) ).
cnf(c229,plain,
( ~ ssRr(X460,X458)
| ~ ssRr(X459,X460)
| ~ ssPv4(X459)
| ssPv4(X458)
| ssPv2(X458)
| ssPv3(X459) ),
inference(factor,[status(thm)],[c112]) ).
cnf(c233,plain,
( ~ ssRr(skf1(X463),X462)
| ~ ssPv4(X463)
| ssPv4(X462)
| ssPv2(X462)
| ssPv3(X463) ),
inference(resolution,[status(thm)],[c229,clause1]) ).
cnf(c234,plain,
( ~ ssPv4(X473)
| ssPv4(skf1(skf1(X473)))
| ssPv2(skf1(skf1(X473)))
| ssPv3(X473) ),
inference(resolution,[status(thm)],[c233,clause1]) ).
cnf(c105,plain,
( ~ ssRr(X428,X430)
| ~ ssRr(X429,X428)
| ~ ssRr(X429,X429)
| ~ ssPv3(X429)
| ssPv3(X430)
| ssPv1(X429)
| ssPv4(X429) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c104,plain,
( ~ ssRr(X384,X386)
| ~ ssRr(X385,X384)
| ~ ssRr(X384,X387)
| ~ ssPv3(X385)
| ssPv3(X386)
| ssPv1(X387)
| ssPv4(X385) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c189,plain,
( ~ ssRr(X405,X404)
| ~ ssRr(X403,X405)
| ~ ssPv3(X403)
| ssPv3(X404)
| ssPv1(skf1(X405))
| ssPv4(X403) ),
inference(resolution,[status(thm)],[c104,clause1]) ).
cnf(c199,plain,
( ~ ssRr(skf1(X426),X425)
| ~ ssPv3(X426)
| ssPv3(X425)
| ssPv1(skf1(skf1(X426)))
| ssPv4(X426) ),
inference(resolution,[status(thm)],[c189,clause1]) ).
cnf(c202,plain,
( ~ ssRr(X412,X414)
| ~ ssPv4(X414)
| ~ ssRr(X413,X412)
| ~ ssRr(X413,X413)
| ~ ssPv3(X413)
| ssPv2(X413) ),
inference(factor,[status(thm)],[clause33]) ).
cnf(c205,plain,
( ~ ssRr(X416,X417)
| ~ ssPv4(X417)
| ~ ssRr(X416,X416)
| ~ ssPv3(X416)
| ssPv2(X416) ),
inference(factor,[status(thm)],[c202]) ).
cnf(c204,plain,
( ~ ssRr(X415,X415)
| ~ ssPv4(X415)
| ~ ssPv3(X415)
| ssPv2(X415) ),
inference(factor,[status(thm)],[c202]) ).
cnf(c187,plain,
( ~ ssRr(X390,X388)
| ~ ssRr(X389,X390)
| ~ ssPv3(X389)
| ssPv3(X388)
| ssPv1(X388)
| ssPv4(X389) ),
inference(factor,[status(thm)],[c104]) ).
cnf(c191,plain,
( ~ ssRr(skf1(X397),X398)
| ~ ssPv3(X397)
| ssPv3(X398)
| ssPv1(X398)
| ssPv4(X397) ),
inference(resolution,[status(thm)],[c187,clause1]) ).
cnf(c196,plain,
( ~ ssPv3(X402)
| ssPv3(skf1(skf1(X402)))
| ssPv1(skf1(skf1(X402)))
| ssPv4(X402) ),
inference(resolution,[status(thm)],[c191,clause1]) ).
cnf(c188,plain,
( ~ ssRr(X399,X400)
| ~ ssRr(X399,X399)
| ~ ssPv3(X399)
| ssPv3(X400)
| ssPv1(X399)
| ssPv4(X399) ),
inference(factor,[status(thm)],[c104]) ).
cnf(c103,plain,
( ~ ssRr(X372,X371)
| ~ ssRr(X372,X372)
| ~ ssRr(X371,X373)
| ~ ssPv3(X372)
| ssPv3(X371)
| ssPv1(X373)
| ssPv4(X372) ),
inference(factor,[status(thm)],[clause20]) ).
cnf(c181,plain,
( ~ ssRr(X381,X382)
| ~ ssRr(X381,X381)
| ~ ssPv3(X381)
| ssPv3(X382)
| ssPv1(skf1(X382))
| ssPv4(X381) ),
inference(resolution,[status(thm)],[c103,clause1]) ).
cnf(c97,plain,
( ~ ssRr(X341,X340)
| ~ ssRr(X339,X341)
| ~ ssRr(X341,X338)
| ~ ssPv1(X339)
| ssPv3(X340)
| ssPv2(X338)
| ssPv3(X339) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c164,plain,
( ~ ssRr(X358,X357)
| ~ ssRr(X356,X358)
| ~ ssPv1(X356)
| ssPv3(X357)
| ssPv2(skf1(X358))
| ssPv3(X356) ),
inference(resolution,[status(thm)],[c97,clause1]) ).
cnf(c173,plain,
( ~ ssRr(skf1(X361),X360)
| ~ ssPv1(X361)
| ssPv3(X360)
| ssPv2(skf1(skf1(X361)))
| ssPv3(X361) ),
inference(resolution,[status(thm)],[c164,clause1]) ).
cnf(c162,plain,
( ~ ssRr(X344,X342)
| ~ ssRr(X343,X344)
| ~ ssPv1(X343)
| ssPv3(X342)
| ssPv2(X342)
| ssPv3(X343) ),
inference(factor,[status(thm)],[c97]) ).
cnf(c166,plain,
( ~ ssRr(skf1(X347),X346)
| ~ ssPv1(X347)
| ssPv3(X346)
| ssPv2(X346)
| ssPv3(X347) ),
inference(resolution,[status(thm)],[c162,clause1]) ).
cnf(c167,plain,
( ~ ssPv1(X355)
| ssPv3(skf1(skf1(X355)))
| ssPv2(skf1(skf1(X355)))
| ssPv3(X355) ),
inference(resolution,[status(thm)],[c166,clause1]) ).
cnf(c96,plain,
( ~ ssRr(X326,X327)
| ~ ssRr(X326,X326)
| ~ ssRr(X327,X325)
| ~ ssPv1(X326)
| ssPv3(X327)
| ssPv2(X325)
| ssPv3(X326) ),
inference(factor,[status(thm)],[clause19]) ).
cnf(c156,plain,
( ~ ssRr(X330,X331)
| ~ ssRr(X330,X330)
| ~ ssPv1(X330)
| ssPv3(X331)
| ssPv2(skf1(X331))
| ssPv3(X330) ),
inference(resolution,[status(thm)],[c96,clause1]) ).
cnf(c157,plain,
( ~ ssRr(X337,X337)
| ~ ssPv1(X337)
| ssPv3(X337)
| ssPv2(skf1(X337)) ),
inference(factor,[status(thm)],[c156]) ).
cnf(c154,plain,
( ~ ssRr(X328,X328)
| ~ ssPv1(X328)
| ssPv3(X328)
| ssPv2(X328) ),
inference(factor,[status(thm)],[c96]) ).
cnf(clause18,negated_conjecture,
( ~ ssRr(X184,X185)
| ~ ssPv3(X185)
| ~ ssRr(X186,X184)
| ~ ssRr(X186,X183)
| ~ ssPv3(X183)
| ~ ssPv1(X186)
| ~ ssPv3(X186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(c92,plain,
( ~ ssRr(X315,X314)
| ~ ssPv3(X314)
| ~ ssRr(X316,X315)
| ~ ssPv3(skf1(X316))
| ~ ssPv1(X316)
| ~ ssPv3(X316) ),
inference(resolution,[status(thm)],[clause18,clause1]) ).
cnf(c148,plain,
( ~ ssRr(X318,skf1(X317))
| ~ ssPv3(skf1(X317))
| ~ ssRr(X317,X318)
| ~ ssPv1(X317)
| ~ ssPv3(X317) ),
inference(factor,[status(thm)],[c92]) ).
cnf(clause17,negated_conjecture,
( ~ ssRr(X171,X172)
| ~ ssRr(X173,X171)
| ~ ssRr(X173,X170)
| ~ ssPv1(X170)
| ~ ssPv1(X173)
| ~ ssPv3(X173)
| ssPv1(X172) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c85,plain,
( ~ ssRr(X313,X311)
| ~ ssRr(X312,X313)
| ~ ssPv1(skf1(X312))
| ~ ssPv1(X312)
| ~ ssPv3(X312)
| ssPv1(X311) ),
inference(resolution,[status(thm)],[clause17,clause1]) ).
cnf(clause16,negated_conjecture,
( ~ ssRr(X160,X161)
| ~ ssPv3(X161)
| ~ ssRr(X162,X160)
| ~ ssRr(X162,X159)
| ~ ssPv1(X159)
| ~ ssPv3(X162)
| ssPv1(X162) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c80,plain,
( ~ ssRr(X309,X308)
| ~ ssPv3(X308)
| ~ ssRr(X310,X309)
| ~ ssPv1(skf1(X310))
| ~ ssPv3(X310)
| ssPv1(X310) ),
inference(resolution,[status(thm)],[clause16,clause1]) ).
cnf(clause15,negated_conjecture,
( ~ ssRr(X147,X148)
| ~ ssPv2(X148)
| ~ ssRr(X149,X147)
| ~ ssRr(X149,X146)
| ~ ssPv1(X149)
| ~ ssPv4(X149)
| ssPv1(X146) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c74,plain,
( ~ ssRr(X297,X298)
| ~ ssPv2(X298)
| ~ ssRr(X299,X297)
| ~ ssPv1(X299)
| ~ ssPv4(X299)
| ssPv1(skf1(X299)) ),
inference(resolution,[status(thm)],[clause15,clause1]) ).
cnf(clause14,negated_conjecture,
( ~ ssRr(X134,X135)
| ~ ssPv3(X135)
| ~ ssRr(X136,X134)
| ~ ssRr(X136,X133)
| ~ ssPv2(X136)
| ssPv3(X133)
| ssPv3(X136) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(c67,plain,
( ~ ssRr(X293,X291)
| ~ ssPv3(X291)
| ~ ssRr(X292,X293)
| ~ ssPv2(X292)
| ssPv3(skf1(X292))
| ssPv3(X292) ),
inference(resolution,[status(thm)],[clause14,clause1]) ).
cnf(clause13,negated_conjecture,
( ~ ssRr(X122,X123)
| ~ ssRr(X124,X122)
| ~ ssRr(X124,X121)
| ~ ssPv3(X121)
| ~ ssPv2(X124)
| ssPv4(X123)
| ssPv3(X124) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(c61,plain,
( ~ ssRr(X284,X283)
| ~ ssRr(X285,X284)
| ~ ssPv3(skf1(X285))
| ~ ssPv2(X285)
| ssPv4(X283)
| ssPv3(X285) ),
inference(resolution,[status(thm)],[clause13,clause1]) ).
cnf(clause12,negated_conjecture,
( ~ ssRr(X109,X110)
| ~ ssPv1(X110)
| ~ ssRr(X111,X109)
| ~ ssRr(X111,X108)
| ~ ssPv1(X108)
| ssPv2(X111)
| ssPv4(X111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c55,plain,
( ~ ssRr(X278,X277)
| ~ ssPv1(X277)
| ~ ssRr(X279,X278)
| ~ ssPv1(skf1(X279))
| ssPv2(X279)
| ssPv4(X279) ),
inference(resolution,[status(thm)],[clause12,clause1]) ).
cnf(c134,plain,
( ~ ssRr(X280,skf1(X281))
| ~ ssPv1(skf1(X281))
| ~ ssRr(X281,X280)
| ssPv2(X281)
| ssPv4(X281) ),
inference(factor,[status(thm)],[c55]) ).
cnf(c135,plain,
( ~ ssPv1(skf1(X282))
| ~ ssRr(X282,X282)
| ssPv2(X282)
| ssPv4(X282) ),
inference(resolution,[status(thm)],[c134,clause1]) ).
cnf(clause11,negated_conjecture,
( ~ ssRr(X96,X97)
| ~ ssPv3(X97)
| ~ ssRr(X98,X96)
| ~ ssRr(X98,X95)
| ~ ssPv1(X95)
| ssPv2(X98)
| ssPv4(X98) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c48,plain,
( ~ ssRr(X274,X275)
| ~ ssPv3(X275)
| ~ ssRr(X276,X274)
| ~ ssPv1(skf1(X276))
| ssPv2(X276)
| ssPv4(X276) ),
inference(resolution,[status(thm)],[clause11,clause1]) ).
cnf(clause10,negated_conjecture,
( ~ ssRr(X84,X85)
| ~ ssRr(X86,X84)
| ~ ssRr(X86,X83)
| ~ ssPv3(X83)
| ~ ssPv1(X86)
| ssPv2(X85)
| ssPv2(X86) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c42,plain,
( ~ ssRr(X266,X267)
| ~ ssRr(X268,X266)
| ~ ssPv3(skf1(X268))
| ~ ssPv1(X268)
| ssPv2(X267)
| ssPv2(X268) ),
inference(resolution,[status(thm)],[clause10,clause1]) ).
cnf(clause9,negated_conjecture,
( ~ ssRr(X71,X72)
| ~ ssPv2(X72)
| ~ ssRr(X73,X71)
| ~ ssRr(X73,X70)
| ~ ssPv1(X73)
| ssPv1(X70)
| ssPv3(X73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(c35,plain,
( ~ ssRr(X262,X260)
| ~ ssPv2(X260)
| ~ ssRr(X261,X262)
| ~ ssPv1(X261)
| ssPv1(skf1(X261))
| ssPv3(X261) ),
inference(resolution,[status(thm)],[clause9,clause1]) ).
cnf(clause8,negated_conjecture,
( ~ ssRr(X60,X61)
| ~ ssRr(X62,X60)
| ~ ssRr(X62,X59)
| ~ ssPv2(X59)
| ~ ssPv1(X62)
| ssPv4(X61)
| ssPv3(X62) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c30,plain,
( ~ ssRr(X259,X257)
| ~ ssRr(X258,X259)
| ~ ssPv2(skf1(X258))
| ~ ssPv1(X258)
| ssPv4(X257)
| ssPv3(X258) ),
inference(resolution,[status(thm)],[clause8,clause1]) ).
cnf(clause7,negated_conjecture,
( ~ ssRr(X46,X47)
| ~ ssRr(X48,X46)
| ~ ssRr(X48,X45)
| ~ ssPv1(X45)
| ssPv3(X47)
| ssPv1(X48)
| ssPv3(X48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(c22,plain,
( ~ ssRr(X249,X250)
| ~ ssRr(X251,X249)
| ~ ssPv1(skf1(X251))
| ssPv3(X250)
| ssPv1(X251)
| ssPv3(X251) ),
inference(resolution,[status(thm)],[clause7,clause1]) ).
cnf(clause6,negated_conjecture,
( ~ ssRr(X35,X36)
| ~ ssPv1(X36)
| ~ ssRr(X37,X35)
| ~ ssRr(X37,X34)
| ssPv4(X34)
| ssPv2(X37)
| ssPv3(X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c17,plain,
( ~ ssRr(X243,X244)
| ~ ssPv1(X244)
| ~ ssRr(X245,X243)
| ssPv4(skf1(X245))
| ssPv2(X245)
| ssPv3(X245) ),
inference(resolution,[status(thm)],[clause6,clause1]) ).
cnf(clause5,negated_conjecture,
( ~ ssRr(X22,X23)
| ~ ssRr(X24,X22)
| ~ ssRr(X24,X21)
| ~ ssPv2(X24)
| ssPv1(X23)
| ssPv2(X21)
| ssPv4(X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c10,plain,
( ~ ssRr(X233,X232)
| ~ ssRr(X234,X233)
| ~ ssPv2(X234)
| ssPv1(X232)
| ssPv2(skf1(X234))
| ssPv4(X234) ),
inference(resolution,[status(thm)],[clause5,clause1]) ).
cnf(c91,plain,
( ~ ssRr(X214,X215)
| ~ ssPv3(X215)
| ~ ssRr(X216,X214)
| ~ ssPv3(X214)
| ~ ssPv1(X216)
| ~ ssPv3(X216) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c108,plain,
( ~ ssRr(skf1(X230),X229)
| ~ ssPv3(X229)
| ~ ssPv3(skf1(X230))
| ~ ssPv1(X230)
| ~ ssPv3(X230) ),
inference(resolution,[status(thm)],[c91,clause1]) ).
cnf(c115,plain,
( ~ ssPv3(skf1(skf1(X231)))
| ~ ssPv3(skf1(X231))
| ~ ssPv1(X231)
| ~ ssPv3(X231) ),
inference(resolution,[status(thm)],[c108,clause1]) ).
cnf(c84,plain,
( ~ ssRr(X203,X202)
| ~ ssRr(X204,X203)
| ~ ssPv1(X203)
| ~ ssPv1(X204)
| ~ ssPv3(X204)
| ssPv1(X202) ),
inference(factor,[status(thm)],[clause17]) ).
cnf(c101,plain,
( ~ ssRr(skf1(X222),X221)
| ~ ssPv1(skf1(X222))
| ~ ssPv1(X222)
| ~ ssPv3(X222)
| ssPv1(X221) ),
inference(resolution,[status(thm)],[c84,clause1]) ).
cnf(c110,plain,
( ~ ssPv1(skf1(X228))
| ~ ssPv1(X228)
| ~ ssPv3(X228)
| ssPv1(skf1(skf1(X228))) ),
inference(resolution,[status(thm)],[c101,clause1]) ).
cnf(c79,plain,
( ~ ssRr(X192,X191)
| ~ ssPv3(X191)
| ~ ssRr(X193,X192)
| ~ ssPv1(X192)
| ~ ssPv3(X193)
| ssPv1(X193) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c95,plain,
( ~ ssRr(skf1(X219),X218)
| ~ ssPv3(X218)
| ~ ssPv1(skf1(X219))
| ~ ssPv3(X219)
| ssPv1(X219) ),
inference(resolution,[status(thm)],[c79,clause1]) ).
cnf(c109,plain,
( ~ ssPv3(skf1(skf1(X220)))
| ~ ssPv1(skf1(X220))
| ~ ssPv3(X220)
| ssPv1(X220) ),
inference(resolution,[status(thm)],[c95,clause1]) ).
cnf(c73,plain,
( ~ ssRr(X174,X176)
| ~ ssPv2(X176)
| ~ ssRr(X175,X174)
| ~ ssPv1(X175)
| ~ ssPv4(X175)
| ssPv1(X174) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c87,plain,
( ~ ssRr(skf1(X206),X207)
| ~ ssPv2(X207)
| ~ ssPv1(X206)
| ~ ssPv4(X206)
| ssPv1(skf1(X206)) ),
inference(resolution,[status(thm)],[c73,clause1]) ).
cnf(c102,plain,
( ~ ssPv2(skf1(skf1(X208)))
| ~ ssPv1(X208)
| ~ ssPv4(X208)
| ssPv1(skf1(X208)) ),
inference(resolution,[status(thm)],[c87,clause1]) ).
cnf(c90,plain,
( ~ ssRr(X189,X188)
| ~ ssPv3(X188)
| ~ ssRr(X189,X189)
| ~ ssPv1(X189)
| ~ ssPv3(X189) ),
inference(factor,[status(thm)],[clause18]) ).
cnf(c93,plain,
( ~ ssRr(X190,X190)
| ~ ssPv3(X190)
| ~ ssPv1(X190) ),
inference(factor,[status(thm)],[c90]) ).
cnf(c78,plain,
( ~ ssRr(X182,X181)
| ~ ssPv3(X181)
| ~ ssRr(X182,X182)
| ~ ssPv1(X181)
| ~ ssPv3(X182)
| ssPv1(X182) ),
inference(factor,[status(thm)],[clause16]) ).
cnf(c66,plain,
( ~ ssRr(X157,X156)
| ~ ssPv3(X156)
| ~ ssRr(X158,X157)
| ~ ssPv2(X158)
| ssPv3(X157)
| ssPv3(X158) ),
inference(factor,[status(thm)],[clause14]) ).
cnf(c77,plain,
( ~ ssRr(skf1(X179),X178)
| ~ ssPv3(X178)
| ~ ssPv2(X179)
| ssPv3(skf1(X179))
| ssPv3(X179) ),
inference(resolution,[status(thm)],[c66,clause1]) ).
cnf(c88,plain,
( ~ ssPv3(skf1(skf1(X180)))
| ~ ssPv2(X180)
| ssPv3(skf1(X180))
| ssPv3(X180) ),
inference(resolution,[status(thm)],[c77,clause1]) ).
cnf(c72,plain,
( ~ ssRr(X167,X168)
| ~ ssPv2(X168)
| ~ ssRr(X167,X167)
| ~ ssPv1(X167)
| ~ ssPv4(X167)
| ssPv1(X168) ),
inference(factor,[status(thm)],[clause15]) ).
cnf(c60,plain,
( ~ ssRr(X144,X143)
| ~ ssRr(X145,X144)
| ~ ssPv3(X144)
| ~ ssPv2(X145)
| ssPv4(X143)
| ssPv3(X145) ),
inference(factor,[status(thm)],[clause13]) ).
cnf(c71,plain,
( ~ ssRr(skf1(X165),X164)
| ~ ssPv3(skf1(X165))
| ~ ssPv2(X165)
| ssPv4(X164)
| ssPv3(X165) ),
inference(resolution,[status(thm)],[c60,clause1]) ).
cnf(c81,plain,
( ~ ssPv3(skf1(X166))
| ~ ssPv2(X166)
| ssPv4(skf1(skf1(X166)))
| ssPv3(X166) ),
inference(resolution,[status(thm)],[c71,clause1]) ).
cnf(c54,plain,
( ~ ssRr(X130,X129)
| ~ ssPv1(X129)
| ~ ssRr(X131,X130)
| ~ ssPv1(X130)
| ssPv2(X131)
| ssPv4(X131) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c64,plain,
( ~ ssRr(skf1(X152),X151)
| ~ ssPv1(X151)
| ~ ssPv1(skf1(X152))
| ssPv2(X152)
| ssPv4(X152) ),
inference(resolution,[status(thm)],[c54,clause1]) ).
cnf(c75,plain,
( ~ ssPv1(skf1(skf1(X153)))
| ~ ssPv1(skf1(X153))
| ssPv2(X153)
| ssPv4(X153) ),
inference(resolution,[status(thm)],[c64,clause1]) ).
cnf(c47,plain,
( ~ ssRr(X118,X120)
| ~ ssPv3(X120)
| ~ ssRr(X119,X118)
| ~ ssPv1(X118)
| ssPv2(X119)
| ssPv4(X119) ),
inference(factor,[status(thm)],[clause11]) ).
cnf(c58,plain,
( ~ ssRr(skf1(X138),X137)
| ~ ssPv3(X137)
| ~ ssPv1(skf1(X138))
| ssPv2(X138)
| ssPv4(X138) ),
inference(resolution,[status(thm)],[c47,clause1]) ).
cnf(c68,plain,
( ~ ssPv3(skf1(skf1(X139)))
| ~ ssPv1(skf1(X139))
| ssPv2(X139)
| ssPv4(X139) ),
inference(resolution,[status(thm)],[c58,clause1]) ).
cnf(c41,plain,
( ~ ssRr(X104,X102)
| ~ ssRr(X103,X104)
| ~ ssPv3(X104)
| ~ ssPv1(X103)
| ssPv2(X102)
| ssPv2(X103) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c51,plain,
( ~ ssRr(skf1(X127),X126)
| ~ ssPv3(skf1(X127))
| ~ ssPv1(X127)
| ssPv2(X126)
| ssPv2(X127) ),
inference(resolution,[status(thm)],[c41,clause1]) ).
cnf(c62,plain,
( ~ ssPv3(skf1(X128))
| ~ ssPv1(X128)
| ssPv2(skf1(skf1(X128)))
| ssPv2(X128) ),
inference(resolution,[status(thm)],[c51,clause1]) ).
cnf(c34,plain,
( ~ ssRr(X90,X88)
| ~ ssPv2(X88)
| ~ ssRr(X89,X90)
| ~ ssPv1(X89)
| ssPv1(X90)
| ssPv3(X89) ),
inference(factor,[status(thm)],[clause9]) ).
cnf(c44,plain,
( ~ ssRr(skf1(X107),X106)
| ~ ssPv2(X106)
| ~ ssPv1(X107)
| ssPv1(skf1(X107))
| ssPv3(X107) ),
inference(resolution,[status(thm)],[c34,clause1]) ).
cnf(c52,plain,
( ~ ssPv2(skf1(skf1(X115)))
| ~ ssPv1(X115)
| ssPv1(skf1(X115))
| ssPv3(X115) ),
inference(resolution,[status(thm)],[c44,clause1]) ).
cnf(c53,plain,
( ~ ssRr(X113,X112)
| ~ ssPv1(X112)
| ~ ssRr(X113,X113)
| ssPv2(X113)
| ssPv4(X113) ),
inference(factor,[status(thm)],[clause12]) ).
cnf(c56,plain,
( ~ ssRr(X114,X114)
| ~ ssPv1(X114)
| ssPv2(X114)
| ssPv4(X114) ),
inference(factor,[status(thm)],[c53]) ).
cnf(c40,plain,
( ~ ssRr(X99,X100)
| ~ ssRr(X99,X99)
| ~ ssPv3(X100)
| ~ ssPv1(X99)
| ssPv2(X100)
| ssPv2(X99) ),
inference(factor,[status(thm)],[clause10]) ).
cnf(c29,plain,
( ~ ssRr(X79,X77)
| ~ ssRr(X78,X79)
| ~ ssPv2(X79)
| ~ ssPv1(X78)
| ssPv4(X77)
| ssPv3(X78) ),
inference(factor,[status(thm)],[clause8]) ).
cnf(c38,plain,
( ~ ssRr(skf1(X93),X92)
| ~ ssPv2(skf1(X93))
| ~ ssPv1(X93)
| ssPv4(X92)
| ssPv3(X93) ),
inference(resolution,[status(thm)],[c29,clause1]) ).
cnf(c45,plain,
( ~ ssPv2(skf1(X94))
| ~ ssPv1(X94)
| ssPv4(skf1(skf1(X94)))
| ssPv3(X94) ),
inference(resolution,[status(thm)],[c38,clause1]) ).
cnf(c21,plain,
( ~ ssRr(X58,X56)
| ~ ssRr(X57,X58)
| ~ ssPv1(X58)
| ssPv3(X56)
| ssPv1(X57)
| ssPv3(X57) ),
inference(factor,[status(thm)],[clause7]) ).
cnf(c27,plain,
( ~ ssRr(skf1(X68),X67)
| ~ ssPv1(skf1(X68))
| ssPv3(X67)
| ssPv1(X68)
| ssPv3(X68) ),
inference(resolution,[status(thm)],[c21,clause1]) ).
cnf(c32,plain,
( ~ ssPv1(skf1(X69))
| ssPv3(skf1(skf1(X69)))
| ssPv1(X69)
| ssPv3(X69) ),
inference(resolution,[status(thm)],[c27,clause1]) ).
cnf(c16,plain,
( ~ ssRr(X50,X51)
| ~ ssPv1(X51)
| ~ ssRr(X49,X50)
| ssPv4(X50)
| ssPv2(X49)
| ssPv3(X49) ),
inference(factor,[status(thm)],[clause6]) ).
cnf(c24,plain,
( ~ ssRr(skf1(X65),X64)
| ~ ssPv1(X64)
| ssPv4(skf1(X65))
| ssPv2(X65)
| ssPv3(X65) ),
inference(resolution,[status(thm)],[c16,clause1]) ).
cnf(c31,plain,
( ~ ssPv1(skf1(skf1(X66)))
| ssPv4(skf1(X66))
| ssPv2(X66)
| ssPv3(X66) ),
inference(resolution,[status(thm)],[c24,clause1]) ).
cnf(c9,plain,
( ~ ssRr(X31,X33)
| ~ ssRr(X32,X31)
| ~ ssPv2(X32)
| ssPv1(X33)
| ssPv2(X31)
| ssPv4(X32) ),
inference(factor,[status(thm)],[clause5]) ).
cnf(c14,plain,
( ~ ssRr(skf1(X39),X40)
| ~ ssPv2(X39)
| ssPv1(X40)
| ssPv2(skf1(X39))
| ssPv4(X39) ),
inference(resolution,[status(thm)],[c9,clause1]) ).
cnf(c18,plain,
( ~ ssPv2(X41)
| ssPv1(skf1(skf1(X41)))
| ssPv2(skf1(X41))
| ssPv4(X41) ),
inference(resolution,[status(thm)],[c14,clause1]) ).
cnf(clause4,negated_conjecture,
( ~ ssRr(X17,X18)
| ~ ssPv1(X18)
| ~ ssRr(X19,X17)
| ~ ssPv1(X19)
| ~ ssPv2(X19)
| ssPv3(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(c7,plain,
( ~ ssRr(skf1(X26),X25)
| ~ ssPv1(X25)
| ~ ssPv1(X26)
| ~ ssPv2(X26)
| ssPv3(X26) ),
inference(resolution,[status(thm)],[clause4,clause1]) ).
cnf(c11,plain,
( ~ ssPv1(skf1(skf1(X27)))
| ~ ssPv1(X27)
| ~ ssPv2(X27)
| ssPv3(X27) ),
inference(resolution,[status(thm)],[c7,clause1]) ).
cnf(c6,plain,
( ~ ssRr(X20,X20)
| ~ ssPv1(X20)
| ~ ssPv2(X20)
| ssPv3(X20) ),
inference(factor,[status(thm)],[clause4]) ).
cnf(clause3,negated_conjecture,
( ~ ssRr(X10,X11)
| ~ ssPv4(X11)
| ~ ssRr(X12,X10)
| ~ ssPv1(X12)
| ssPv2(X12)
| ssPv3(X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c4,plain,
( ~ ssRr(skf1(X14),X15)
| ~ ssPv4(X15)
| ~ ssPv1(X14)
| ssPv2(X14)
| ssPv3(X14) ),
inference(resolution,[status(thm)],[clause3,clause1]) ).
cnf(c5,plain,
( ~ ssPv4(skf1(skf1(X16)))
| ~ ssPv1(X16)
| ssPv2(X16)
| ssPv3(X16) ),
inference(resolution,[status(thm)],[c4,clause1]) ).
cnf(clause2,negated_conjecture,
( ~ ssRr(X3,X4)
| ~ ssRr(X5,X3)
| ~ ssPv2(X5)
| ~ ssPv4(X5)
| ssPv1(X4)
| ssPv3(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(c1,plain,
( ~ ssRr(skf1(X8),X7)
| ~ ssPv2(X8)
| ~ ssPv4(X8)
| ssPv1(X7)
| ssPv3(X8) ),
inference(resolution,[status(thm)],[clause2,clause1]) ).
cnf(c2,plain,
( ~ ssPv2(X9)
| ~ ssPv4(X9)
| ssPv1(skf1(skf1(X9)))
| ssPv3(X9) ),
inference(resolution,[status(thm)],[c1,clause1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SYN760-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:13:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.52/3.75 % Version: 1.5
% 3.52/3.75 % SZS status Satisfiable
% 3.52/3.75 % SZS output start Saturation
% See solution above
% 3.61/3.78
% 3.61/3.78 % Initial clauses : 51
% 3.61/3.78 % Processed clauses : 842
% 3.61/3.78 % Factors computed : 1046
% 3.61/3.78 % Resolvents computed: 530
% 3.61/3.78 % Tautologies deleted: 128
% 3.61/3.78 % Forward subsumed : 657
% 3.61/3.78 % Backward subsumed : 50
% 3.61/3.78 % -------- CPU Time ---------
% 3.61/3.78 % User time : 3.416 s
% 3.61/3.78 % System time : 0.013 s
% 3.61/3.78 % Total time : 3.429 s
%------------------------------------------------------------------------------