*** Some Example Proofs Produced with Seqs # (\x . P(x)) -> ]y . P(y) *** example 1 (\x . P(x)) -> ]y . P(y) *** example 1 (forall x . P(x)) -> (exists y . P(y)) ((forall [x:Atom] . [(P([x:Atom])):Pred]) -> (exists [y:Atom] . [(P([y:Atom])):Pred])) [1:0][1:5][2:7] proof tree [ ; P(_B) ; forall x . P(x) => ; P(_A) ; ] [P(_B) ; ; forall x . P(x) => ; P(_A) ; ] [ ; ; forall x . P(x) => ; P(_A) ; ] [ ; ; forall x . P(x) => P(_A) ; ; ] [ ; ; forall x . P(x) => exists y . P(y) ; ; ] [forall x . P(x) ; ; => exists y . P(y) ; ; ] [ ; ; => (forall x . P(x)) -> (exists y . P(y)) ; ; ] with: P(_B) eq P(_A) where: [_B->_A] [proof COMPLETE!!!] considered 7 sequents # (]x . \y . P(x, y)) -> \u . ]v . P(v, u) *** example 2 (]x . \y . P(x, y)) -> \u . ]v . P(v, u) *** example 2 (exists x . (forall y . P(x, y))) -> (forall u . (exists v . P(v, u))) ((exists [x:Atom] . (forall [y:Atom] . [(P([x:Atom], [y:Atom])):Pred])) -> (forall [u:Atom] . (exists [v:Atom] . [(P([v:Atom], [u:Atom])):Pred]))) [1:0][1:7][2:9] proof tree [ ; P(_a, _D) ; forall y . P(_a, y) => ; P(_C, _b) ; ] [P(_a, _D) ; ; forall y . P(_a, y) => ; P(_C, _b) ; ] [ ; ; forall y . P(_a, y) => ; P(_C, _b) ; ] [ ; ; forall y . P(_a, y) => P(_C, _b) ; ; ] [ ; ; forall y . P(_a, y) => exists v . P(v, _b) ; ; ] [ ; ; forall y . P(_a, y) => forall u . (exists v . P(v, u)) ; ; ] [forall y . P(_a, y) ; ; => forall u . (exists v . P(v, u)) ; ; ] [exists x . (forall y . P(x, y)) ; ; => forall u . (exists v . P(v, u)) ; ; ] [ ; ; => (exists x . (forall y . P(x, y))) -> (forall u . (exists v . P(v, u))) ; ; ] with: P(_a, _D) eq P(_C, _b) where: [_C->_a, _D->_b] [proof COMPLETE!!!] considered 9 sequents # (\x . P(x) -> P(f(x))) & (]y . P(g(y))) -> ]z . P(f(f(g(z)))) *** example 3 (\x . P(x) -> P(f(x))) & (]y . P(g(y))) -> ]z . P(f(f(g(z)))) *** example 3 ((forall x . (P(x) -> P(f(x)))) & (exists y . P(g(y)))) -> (exists z . P(f(f(g(z))))) (((forall [x:Atom] . ([(P([x:Atom])):Pred] -> [(P([(f([x:Atom])):Func])):Pred])) & (exists [y:Atom] . [(P([(g([y:Atom])):Func])):Pred])) -> (exists [z:Atom] . [(P([(f([(f([(g([z:Atom])):Func])):Func])):Func])):Pred])) [1:0][2:8][1:8][3:10][2:10][5:12][8:16][7:16][11:18][15:22][19:26][22:27][25:28][28:31][31:36][30:36][35:38][40:42][45:46][50:50][54:51][58:52][62:55][66:60][70:65][74:66][78:67][82:70][86:75][90:80][89:80][88:80][92:82][97:86][96:86][95:86][99:88][104:92][108:93][112:94][116:97][120:102][123:104][126:106][129:110][132:116][131:116][137:118][143:122][149:126][155:130][161:134][166:135][171:136][176:139][181:144][186:149][191:154][196:155][201:156][206:159][211:164][216:169][221:174][226:175][231:176][236:179][241:184][246:189][251:194][250:194][249:194][254:196][260:200][266:204][265:204][264:204][269:206][275:210][281:214][286:215][291:216][296:219][301:224][306:229][310:231][314:233][318:237][322:243][326:249][331:251][336:253][341:257][346:263][351:269][350:269][349:269][354:271][360:275][366:279][365:279][364:279][369:281][375:285][381:289][386:290][391:291][396:294][401:299][406:304][411:306][416:308][421:312][426:318][431:324][435:326][439:328][443:332][447:338][451:344][450:344][449:344][454:346][460:350][466:354][469:355][472:356][475:357][478:358][481:361][484:366][483:366][482:366][487:368][493:372][499:376][502:377][505:378][508:379][511:380][514:383][517:388][516:388][515:388][520:390][524:394][529:398][528:398][527:398][532:400][536:404][541:408][545:409][549:410][553:413][557:418][561:423][566:425][571:427][576:431][581:437][586:443][591:444][596:445][601:448][606:453][611:454][616:455][621:458][626:463][631:465][636:467][641:471][646:477][651:480][656:483][661:488][666:495][665:495][672:497][679:501][686:505][693:509][700:513][707:517][713:518][719:519][725:522][731:527][737:532][743:537][749:542][755:543][761:544][767:547][773:552][779:557][785:562][791:567][797:568][803:569][809:572][815:577][821:582][827:587][833:592][839:593][845:594][851:597][857:602][863:607][869:612][875:617][874:617][873:617][879:619][886:623][893:627][900:631][899:631][898:631][904:633][911:637][918:641][925:645][931:646][937:647][943:650][949:655][955:660][961:665][966:667][971:669][976:673][981:679][986:685][991:691][997:693][1003:695][1009:699][1015:705][1021:711][1027:717][1033:719][1039:721][1045:725][1051:731][1057:737][1063:743][1062:743][1061:743][1067:745][1074:749][1081:753][1088:757][1087:757][1086:757][1092:759][1099:763][1106:767][1113:771][1119:772][1125:773][1131:776][1137:781][1143:786][1149:791][1155:793][1161:795][1167:799][1173:805][1179:811][1185:817][1190:819][1195:821][1200:825][1205:831][1210:837][1215:843][1221:845][1227:847][1233:851][1239:857][1245:863][1251:869][1250:869][1249:869][1255:871][1262:875][1269:879][1276:883][1275:883][1274:883][1280:885][1287:889][1294:893][1301:897][1307:898][1313:899][1319:902][1325:907][1331:912][1337:917][1343:919][1349:921][1355:925][1361:931][1367:937][1373:943][1379:945][1385:947][1391:951][1397:957][1403:963][1409:969][1414:971][1419:973][1424:977][1429:983][1434:989][1439:995][1438:995][1437:995][1443:997][1450:1001][1457:1005][1464:1009][1468:1010][1472:1011][1476:1012][1480:1013][1484:1016][1488:1021][1492:1026][1497:1027][1502:1028][1507:1029][1512:1030][1517:1033][1522:1038][1527:1043][1526:1043][1525:1043][1531:1045][1538:1049][1545:1053][1552:1057][1556:1058][1560:1059][1564:1060][1568:1061][1572:1064][1576:1069][1580:1074][1585:1075][1590:1076][1595:1077][1600:1078][1605:1081][1610:1086][1615:1091][1614:1091][1613:1091][1619:1093][1624:1097][1630:1101][1636:1105][1635:1105][1634:1105][1640:1107][1645:1111][1651:1115][1657:1119][1662:1120][1667:1121][1672:1124][1677:1129][1682:1134][1687:1139][1693:1141][1699:1143][1705:1147][1711:1153][1717:1159][1723:1165][1729:1167][1735:1169][1741:1173][1747:1179][1753:1185][1759:1191][1765:1192][1771:1193][1777:1196][1783:1201][1789:1206][1795:1207][1801:1208][1807:1211][1813:1216][1819:1221][1825:1223][1831:1225][1837:1229][1843:1235][1849:1241][1855:1244][1861:1247][1867:1252][1873:1259][1879:1266][1885:1269][1891:1272][1897:1277][1903:1284][1909:1291][1915:1292][1921:1293][1927:1294][1933:1297][1939:1302][1945:1307][1951:1308][1957:1309][1963:1310][1969:1313][1975:1318][1981:1323][1987:1325][1993:1327][1999:1329][2005:1333][2011:1339][2017:1345][2023:1348][2029:1351][2035:1354][2041:1359][2047:1366][2053:1373][2059:1376][2065:1379][2071:1382][2077:1387][2083:1394][2089:1401][2088:1401][2087:1401][2093:1403][2100:1407][2107:1411][2114:1415][2119:1416][2124:1417][2129:1418][2134:1419][2139:1422][2144:1427][2149:1432][2153:1433][2157:1434][2161:1435][2165:1436][2169:1439][2173:1444][2177:1449][2176:1449][2175:1449][2181:1451][2188:1455][2195:1459][2202:1463][2207:1464][2212:1465][2217:1466][2222:1467][2227:1470][2232:1475][2237:1480][2241:1481][2245:1482][2249:1483][2253:1484][2257:1487][2261:1492][2265:1497][2264:1497][2263:1497][2269:1499][2275:1503][2280:1507][2286:1511][2285:1511][2284:1511][2290:1513][2296:1517][2301:1521][2307:1525][2312:1526][2317:1527][2322:1530][2327:1535][2332:1540][2337:1545][2343:1547][2349:1549][2355:1553][2361:1559][2367:1565][2373:1571][2379:1573][2385:1575][2391:1579][2397:1585][2403:1591][2409:1597][2415:1598][2421:1599][2427:1600][2433:1603][2439:1608][2445:1613][2451:1614][2457:1615][2463:1616][2469:1619][2475:1624][2481:1629][2487:1631][2493:1633][2499:1635][2505:1639][2511:1645][2517:1651][2523:1654][2529:1657][2535:1660][2541:1665][2547:1672][2553:1679][2559:1682][2565:1685][2571:1688][2577:1693][2583:1700][2589:1707][2595:1708][2601:1709][2607:1712][2613:1717][2619:1722][2625:1723][2631:1724][2637:1727][2643:1732][2649:1737][2655:1739][2661:1741][2667:1745][2673:1751][2679:1757][2685:1760][2691:1763][2697:1768][2703:1775][2709:1782][2715:1785][2721:1788][2727:1793][2733:1800][2739:1807][2738:1807][2737:1807][2743:1809][2750:1813][2757:1817][2764:1821][2768:1822][2772:1823][2776:1824][2780:1825][2784:1828][2788:1833][2792:1838][2797:1839][2802:1840][2807:1841][2812:1842][2817:1845][2822:1850][2827:1855][2826:1855][2825:1855][2829:1857][2834:1861][2833:1861][2832:1861][2836:1863][2841:1867][2840:1867][2839:1867][2843:1869][2848:1873][2847:1873][2846:1873][2850:1875][2855:1879][2861:1880][2867:1881][2873:1884][2879:1889][2884:1891][2889:1893][2894:1897][2899:1903][2898:1903][2897:1903][2903:1905][2910:1909][2917:1913][2924:1917][2928:1918][2932:1919][2936:1920][2940:1921][2944:1924][2948:1929][2952:1934][2957:1935][2962:1936][2967:1937][2972:1938][2977:1941][2982:1946][2987:1951][2986:1951][2985:1951][2989:1953][2994:1957][2993:1957][2992:1957][2996:1959][3001:1963][3000:1963][2999:1963][3003:1965][3008:1969][3007:1969][3006:1969][3010:1971][3015:1975][3021:1976][3027:1977][3033:1980][3039:1985][3044:1987][3049:1989][3054:1993][3059:1999][3058:1999][3057:1999][3063:2001][3068:2005][3074:2009][3080:2013][3086:2014][3092:2015][3098:2018][3104:2023][3110:2028][3116:2029][3122:2030][3128:2031][3134:2034][3140:2039][3146:2044][3145:2044][3144:2044][3150:2046][3155:2050][3161:2054][3167:2058][3173:2059][3179:2060][3185:2063][3191:2068][3197:2073][3203:2074][3209:2075][3215:2076][3221:2079][3227:2084][3233:2089][3232:2089][3231:2089][3236:2091][3242:2095][3248:2099][3247:2099][3246:2099][3251:2101][3257:2105][3263:2109][3268:2110][3273:2111][3278:2114][3283:2119][3288:2124][3292:2126][3296:2128][3300:2132][3304:2138][3308:2144][3313:2146][3318:2148][3323:2152][3328:2158][3333:2164][3336:2165][3339:2166][3342:2167][3345:2168][3348:2171][3351:2176][3354:2177][3357:2178][3360:2179][3363:2180][3366:2183][3369:2188][3372:2190][3375:2192][3378:2194][3381:2196][3384:2200][3387:2206][3390:2209][3393:2212][3396:2215][3399:2218][3402:2223][3405:2230][3408:2233][3411:2236][3414:2239][3417:2242][3420:2247][3423:2254][3422:2254][3421:2254][3420:2254][3419:2254][3425:2256][3430:2260][3429:2260][3428:2260][3427:2260][3426:2260][3432:2262][3437:2266][3441:2267][3445:2268][3449:2269][3453:2270][3457:2273][3461:2278][3464:2280][3467:2282][3470:2284][3473:2286][3476:2290][3479:2296][3478:2296][3477:2296][3476:2296][3475:2296][3481:2298][3486:2302][3485:2302][3484:2302][3483:2302][3482:2302][3488:2304][3493:2308][3497:2309][3501:2310][3505:2311][3509:2312][3513:2315][3517:2320][3520:2322][3523:2324][3526:2326][3529:2328][3532:2332][3535:2338][3539:2339][3543:2340][3547:2341][3551:2342][3555:2345][3559:2350][3563:2351][3567:2352][3571:2353][3575:2354][3579:2357][3583:2362][3587:2364][3591:2366][3595:2368][3599:2370][3603:2374][3607:2380][3611:2383][3615:2386][3619:2389][3623:2392][3627:2397][3631:2404][3636:2406][3641:2408][3646:2410][3651:2412][3656:2416][3661:2422][3666:2424][3671:2426][3676:2428][3681:2430][3686:2434][3691:2440][3696:2443][3701:2446][3706:2449][3711:2452][3716:2457][3721:2464][3726:2468][3731:2472][3736:2476][3741:2480][3746:2486][3751:2494][3750:2494][3758:2496][3766:2500][3774:2504][3782:2508][3790:2512][3798:2516][3806:2520][3813:2521][3820:2522][3827:2525][3834:2530][3841:2535][3848:2540][3855:2545][3862:2550][3869:2551][3876:2552][3883:2555][3890:2560][3897:2565][3904:2570][3911:2575][3918:2580][3925:2581][3932:2582][3939:2585][3946:2590][3953:2595][3960:2600][3967:2605][3974:2610][3981:2611][3988:2612][3995:2615][4002:2620][4009:2625][4016:2630][4023:2635][4030:2640][4037:2641][4044:2642][4051:2645][4058:2650][4065:2655][4072:2660][4079:2665][4086:2670][4085:2670][4084:2670][4091:2672][4099:2676][4107:2680][4115:2684][4123:2688][4122:2688][4121:2688][4128:2690][4136:2694][4144:2698][4152:2702][4160:2706][4167:2707][4174:2708][4181:2711][4188:2716][4195:2721][4202:2726][4209:2731][4215:2733][4221:2735][4227:2739][4233:2745][4239:2751][4245:2757][4251:2763][4258:2765][4265:2767][4272:2771][4279:2777][4286:2783][4293:2789][4300:2795][4307:2797][4314:2799][4321:2803][4328:2809][4335:2815][4342:2821][4349:2827][4356:2829][4363:2831][4370:2835][4377:2841][4384:2847][4391:2853][4398:2859][4397:2859][4396:2859][4403:2861][4411:2865][4419:2869][4427:2873][4435:2877][4434:2877][4433:2877][4440:2879][4448:2883][4456:2887][4464:2891][4472:2895][4479:2896][4486:2897][4493:2900][4500:2905][4507:2910][4514:2915][4521:2920][4528:2922][4535:2924][4542:2928][4549:2934][4556:2940][4563:2946][4570:2952][4576:2954][4582:2956][4588:2960][4594:2966][4600:2972][4606:2978][4612:2984][4619:2986][4626:2988][4633:2992][4640:2998][4647:3004][4654:3010][4661:3016][4668:3018][4675:3020][4682:3024][4689:3030][4696:3036][4703:3042][4710:3048][4709:3048][4708:3048][4715:3050][4723:3054][4731:3058][4739:3062][4747:3066][4746:3066][4745:3066][4752:3068][4760:3072][4768:3076][4776:3080][4784:3084][4791:3085][4798:3086][4805:3089][4812:3094][4819:3099][4826:3104][4833:3109][4840:3111][4847:3113][4854:3117][4861:3123][4868:3129][4875:3135][4882:3141][4889:3143][4896:3145][4903:3149][4910:3155][4917:3161][4924:3167][4931:3173][4937:3175][4943:3177][4949:3181][4955:3187][4961:3193][4967:3199][4973:3205][4980:3207][4987:3209][4994:3213][5001:3219][5008:3225][5015:3231][5022:3237][5021:3237][5020:3237][5027:3239][5035:3243][5043:3247][5051:3251][5059:3255][5058:3255][5057:3255][5064:3257][5072:3261][5080:3265][5088:3269][5096:3273][5103:3274][5110:3275][5117:3278][5124:3283][5131:3288][5138:3293][5145:3298][5152:3300][5159:3302][5166:3306][5173:3312][5180:3318][5187:3324][5194:3330][5201:3332][5208:3334][5215:3338][5222:3344][5229:3350][5236:3356][5243:3362][5250:3364][5257:3366][5264:3370][5271:3376][5278:3382][5285:3388][5292:3394][5298:3396][5304:3398][5310:3402][5316:3408][5322:3414][5328:3420][5334:3426][5333:3426][5332:3426][5339:3428][5347:3432][5355:3436][5363:3440][5371:3444][5376:3445][5381:3446][5386:3447][5391:3448][5396:3451][5401:3456][5406:3461][5411:3466][5417:3467][5423:3468][5429:3469][5435:3470][5441:3473][5447:3478][5453:3483][5459:3488][5465:3489][5471:3490][5477:3491][5483:3492][5489:3495][5495:3500][5501:3505][5507:3510][5506:3510][5505:3510][5512:3512][5520:3516][5528:3520][5536:3524][5544:3528][5549:3529][5554:3530][5559:3531][5564:3532][5569:3535][5574:3540][5579:3545][5584:3550][5590:3551][5596:3552][5602:3553][5608:3554][5614:3557][5620:3562][5626:3567][5632:3572][5638:3573][5644:3574][5650:3575][5656:3576][5662:3579][5668:3584][5674:3589][5680:3594][5679:3594][5678:3594][5685:3596][5691:3600][5698:3604][5705:3608][5712:3612][5711:3612][5710:3612][5717:3614][5723:3618][5730:3622][5737:3626][5744:3630][5750:3631][5756:3632][5762:3635][5768:3640][5774:3645][5780:3650][5786:3655][5793:3657][5800:3659][5807:3663][5814:3669][5821:3675][5828:3681][5835:3687][5842:3689][5849:3691][5856:3695][5863:3701][5870:3707][5877:3713][5884:3719][5891:3721][5898:3723][5905:3727][5912:3733][5919:3739][5926:3745][5933:3751][5940:3752][5947:3753][5954:3756][5961:3761][5968:3766][5975:3771][5982:3772][5989:3773][5996:3776][6003:3781][6010:3786][6017:3791][6024:3793][6031:3795][6038:3799][6045:3805][6052:3811][6059:3817][6066:3820][6073:3823][6080:3828][6087:3835][6094:3842][6101:3849][6108:3852][6115:3855][6122:3860][6129:3867][6136:3874][6143:3881][6150:3884][6157:3887][6164:3892][6171:3899][6178:3906][6185:3913][6192:3914][6199:3915][6206:3916][6213:3919][6220:3924][6227:3929][6234:3934][6241:3935][6248:3936][6255:3937][6262:3940][6269:3945][6276:3950][6283:3955][6290:3957][6297:3959][6304:3961][6311:3965][6318:3971][6325:3977][6332:3983][6339:3986][6346:3989][6353:3992][6360:3997][6367:4004][6374:4011][6381:4018][6388:4021][6395:4024][6402:4027][6409:4032][6416:4039][6423:4046][6430:4053][6437:4056][6444:4059][6451:4062][6458:4067][6465:4074][6472:4081][6479:4088][6486:4089][6493:4090][6500:4091][6507:4094][6514:4099][6521:4104][6528:4109][6535:4110][6542:4111][6549:4112][6556:4115][6563:4120][6570:4125][6577:4130][6584:4132][6591:4134][6598:4136][6605:4140][6612:4146][6619:4152][6626:4158][6633:4161][6640:4164][6647:4167][6654:4172][6661:4179][6668:4186][6675:4193][6682:4196][6689:4199][6696:4202][6703:4207][6710:4214][6717:4221][6724:4228][6731:4231][6738:4234][6745:4237][6752:4242][6759:4249][6766:4256][6773:4263][6772:4263][6771:4263][6778:4265][6786:4269][6794:4273][6802:4277][6810:4281][6816:4282][6822:4283][6828:4284][6834:4285][6840:4288][6846:4293][6852:4298][6858:4303][6863:4304][6868:4305][6873:4306][6878:4307][6883:4310][6888:4315][6893:4320][6898:4325][6904:4326][6910:4327][6916:4328][6922:4329][6928:4332][6934:4337][6940:4342][6946:4347][6945:4347][6944:4347][6951:4349][6959:4353][6967:4357][6975:4361][6983:4365][6989:4366][6995:4367][7001:4368][7007:4369][7013:4372][7019:4377][7025:4382][7031:4387][7036:4388][7041:4389][7046:4390][7051:4391][7056:4394][7061:4399][7066:4404][7071:4409][7077:4410][7083:4411][7089:4412][7095:4413][7101:4416][7107:4421][7113:4426][7119:4431][7118:4431][7117:4431][7124:4433][7131:4437][7137:4441][7144:4445][7151:4449][7150:4449][7149:4449][7156:4451][7163:4455][7169:4459][7176:4463][7183:4467][7189:4468][7195:4469][7201:4472][7207:4477][7213:4482][7219:4487][7225:4492][7232:4494][7239:4496][7246:4500][7253:4506][7260:4512][7267:4518][7274:4524][7281:4526][7288:4528][7295:4532][7302:4538][7309:4544][7316:4550][7323:4556][7330:4558][7337:4560][7344:4564][7351:4570][7358:4576][7365:4582][7372:4588][7379:4589][7386:4590][7393:4591][7400:4594][7407:4599][7414:4604][7421:4609][7428:4610][7435:4611][7442:4612][7449:4615][7456:4620][7463:4625][7470:4630][7477:4632][7484:4634][7491:4636][7498:4640][7505:4646][7512:4652][7519:4658][7526:4661][7533:4664][7540:4667][7547:4672][7554:4679][7561:4686][7568:4693][7575:4696][7582:4699][7589:4702][7596:4707][7603:4714][7610:4721][7617:4728][7624:4731][7631:4734][7638:4737][7645:4742][7652:4749][7659:4756][7666:4763][7673:4764][7680:4765][7687:4768][7694:4773][7701:4778][7708:4783][7715:4784][7722:4785][7729:4788][7736:4793][7743:4798][7750:4803][7757:4805][7764:4807][7771:4811][7778:4817][7785:4823][7792:4829][7799:4832][7806:4835][7813:4840][7820:4847][7827:4854][7834:4861][7841:4864][7848:4867][7855:4872][7862:4879][7869:4886][7876:4893][7883:4896][7890:4899][7897:4904][7904:4911][7911:4918][7918:4925][7925:4926][7932:4927][7939:4928][7946:4931][7953:4936][7960:4941][7967:4946][7974:4947][7981:4948][7988:4949][7995:4952][8002:4957][8009:4962][8016:4967][8023:4969][8030:4971][8037:4973][8044:4977][8051:4983][8058:4989][8065:4995][8072:4998][8079:5001][8086:5004][8093:5009][8100:5016][8107:5023][8114:5030][8121:5033][8128:5036][8135:5039][8142:5044][8149:5051][8156:5058][8163:5065][8170:5068][8177:5071][8184:5074][8191:5079][8198:5086][8205:5093][8212:5100][8211:5100][8210:5100][8217:5102][8225:5106][8233:5110][8241:5114][8249:5118][8255:5119][8261:5120][8267:5121][8273:5122][8279:5125][8285:5130][8291:5135][8297:5140][8303:5141][8309:5142][8315:5143][8321:5144][8327:5147][8333:5152][8339:5157][8345:5162][8350:5163][8355:5164][8360:5165][8365:5166][8370:5169][8375:5174][8380:5179][8385:5184][8384:5184][8383:5184][8390:5186][8398:5190][8406:5194][8414:5198][8422:5202][8428:5203][8434:5204][8440:5205][8446:5206][8452:5209][8458:5214][8464:5219][8470:5224][8476:5225][8482:5226][8488:5227][8494:5228][8500:5231][8506:5236][8512:5241][8518:5246][8523:5247][8528:5248][8533:5249][8538:5250][8543:5253][8548:5258][8553:5263][8558:5268][8557:5268][8556:5268][8563:5270][8570:5274][8577:5278][8583:5282][8590:5286][8589:5286][8588:5286][8595:5288][8602:5292][8609:5296][8615:5300][8622:5304][8628:5305][8634:5306][8640:5309][8646:5314][8652:5319][8658:5324][8664:5329][8671:5331][8678:5333][8685:5337][8692:5343][8699:5349][8706:5355][8713:5361][8720:5363][8727:5365][8734:5369][8741:5375][8748:5381][8755:5387][8762:5393][8769:5395][8776:5397][8783:5401][8790:5407][8797:5413][8804:5419][8811:5425][8818:5426][8825:5427][8832:5428][8839:5431][8846:5436][8853:5441][8860:5446][8867:5447][8874:5448][8881:5449][8888:5452][8895:5457][8902:5462][8909:5467][8916:5469][8923:5471][8930:5473][8937:5477][8944:5483][8951:5489][8958:5495][8965:5498][8972:5501][8979:5504][8986:5509][8993:5516][9000:5523][9007:5530][9014:5533][9021:5536][9028:5539][9035:5544][9042:5551][9049:5558][9056:5565][9063:5568][9070:5571][9077:5574][9084:5579][9091:5586][9098:5593][9105:5600][9112:5601][9119:5602][9126:5603][9133:5606][9140:5611][9147:5616][9154:5621][9161:5622][9168:5623][9175:5624][9182:5627][9189:5632][9196:5637][9203:5642][9210:5644][9217:5646][9224:5648][9231:5652][9238:5658][9245:5664][9252:5670][9259:5673][9266:5676][9273:5679][9280:5684][9287:5691][9294:5698][9301:5705][9308:5708][9315:5711][9322:5714][9329:5719][9336:5726][9343:5733][9350:5740][9357:5743][9364:5746][9371:5749][9378:5754][9385:5761][9392:5768][9399:5775][9406:5776][9413:5777][9420:5780][9427:5785][9434:5790][9441:5795][9448:5796][9455:5797][9462:5800][9469:5805][9476:5810][9483:5815][9490:5817][9497:5819][9504:5823][9511:5829][9518:5835][9525:5841][9532:5844][9539:5847][9546:5852][9553:5859][9560:5866][9567:5873][9574:5876][9581:5879][9588:5884][9595:5891][9602:5898][9609:5905][9616:5908][9623:5911][9630:5916][9637:5923][9644:5930][9651:5937][9650:5937][9649:5937][9656:5939][9664:5943][9672:5947][9680:5951][9688:5955][9693:5956][9698:5957][9703:5958][9708:5959][9713:5962][9718:5967][9723:5972][9728:5977][9734:5978][9740:5979][9746:5980][9752:5981][9758:5984][9764:5989][9770:5994][9776:5999][9782:6000][9788:6001][9794:6002][9800:6003][9806:6006][9812:6011][9818:6016][9824:6021][9823:6021][9822:6021][9827:6023][9833:6027][9839:6031][9838:6031][9837:6031][9842:6033][9848:6037][9854:6041][9853:6041][9852:6041][9857:6043][9863:6047][9869:6051][9868:6051][9867:6051][9872:6053][9878:6057][9884:6061][9891:6062][9898:6063][9905:6066][9912:6071][9919:6076][9925:6078][9931:6080][9937:6084][9943:6090][9949:6096][9957:6098][9965:6100][9973:6104][9981:6110][9989:6116] proof tree [ ; P(f(_D)), P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(_D), P(f(f(g(_B)))) ; ; P(f(_D)), P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(f(_D)), P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(_D), P(f(f(g(_B)))) ; ; P(f(_D)), P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [P(f(_D)) ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(_D), P(f(f(g(_B)))) ; ] [ ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => P(_D) ; P(f(f(g(_B)))) ; P(f(_D)) ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(_C), P(f(f(g(_B)))) ; ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(_C), P(f(f(g(_B)))) ; ; P(f(_C)), P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [P(f(_C)) ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(_C), P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => P(_C) ; P(f(f(g(_B)))) ; P(f(_C)) ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)), P(_D) -> P(f(_D)) => ; P(f(f(g(_B)))) ; ] [P(_D) -> P(f(_D)) ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)) => ; P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))), P(_C) -> P(f(_C)) => ; P(f(f(g(_B)))) ; ] [P(_C) -> P(f(_C)) ; P(g(_a)) ; forall x . (P(x) -> P(f(x))) => ; P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))) => ; P(f(f(g(_B)))) ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))) => P(f(f(g(_B)))) ; ; ] [ ; P(g(_a)) ; forall x . (P(x) -> P(f(x))) => exists z . P(f(f(g(z)))) ; ; ] [P(g(_a)) ; ; forall x . (P(x) -> P(f(x))) => exists z . P(f(f(g(z)))) ; ; ] [exists y . P(g(y)) ; ; forall x . (P(x) -> P(f(x))) => exists z . P(f(f(g(z)))) ; ; ] [forall x . (P(x) -> P(f(x))), exists y . P(g(y)) ; ; => exists z . P(f(f(g(z)))) ; ; ] [(forall x . (P(x) -> P(f(x)))) & (exists y . P(g(y))) ; ; => exists z . P(f(f(g(z)))) ; ; ] [ ; ; => ((forall x . (P(x) -> P(f(x)))) & (exists y . P(g(y)))) -> (exists z . P(f(f(g(z))))) ; ; ] with: P(f(_C)) eq P(_D) P(f(_D)) eq P(f(f(g(_B)))) P(g(_a)) eq P(_C) where: [_D->f(g(_a)), _C->g(_a), _B->_a] [proof COMPLETE!!!] considered 6116 sequents # (\x . ]y . P(x, y)) & (\x . \y . P(x, y) -> P(y, x)) -> \x . ]y . P(y, x) *** example 4 (\x . ]y . P(x, y)) & (\x . \y . P(x, y) -> P(y, x)) -> \x . ]y . P(y, x) *** example 4 ((forall x . (exists y . P(x, y))) & (forall x . (forall y . (P(x, y) -> P(y, x))))) -> (forall x . (exists y . P(y, x))) (((forall [x:Atom] . (exists [y:Atom] . [(P([x:Atom], [y:Atom])):Pred])) & (forall [x:Atom] . (forall [y:Atom] . ([(P([x:Atom], [y:Atom])):Pred] -> [(P([y:Atom], [x:Atom])):Pred])))) -> (forall [x:Atom] . (exists [y:Atom] . [(P([y:Atom], [x:Atom])):Pred]))) [1:0][1:8][2:12][1:12][4:17][3:17][2:17][8:23][13:27][12:27][11:27][10:27][20:34][29:38][38:42][47:46][51:47][55:48][59:49][63:50][67:57][71:62][70:62][69:62][68:62][67:62][82:70][96:74][110:78][124:82][138:86][152:90][166:94][173:95][180:96][187:97][194:98][201:99][208:100][215:108][222:113][229:118][236:123][243:124][250:125][257:126][264:127][271:128][278:129][285:137][292:142][299:147][306:152][313:153][320:154][327:155][334:156][341:157][348:158][355:166][362:171][369:176][376:181][375:181][374:181][373:181][380:187][387:191][386:191][385:191][384:191][391:197][398:201][397:201][396:201][395:201][402:207][409:211][408:211][407:211][406:211][413:217][420:221][429:222][438:223][447:224][456:231][465:236][470:238][475:240][480:242][485:250][490:256][489:256][488:256][487:256][486:256][485:256][506:265][526:269][546:273][566:277][586:281][606:285][626:289][646:293][666:297][686:301][706:305][717:306][728:307][739:308][750:309][761:310][772:311][783:312][794:313][805:322][816:327][827:332][838:337][849:342][860:347][871:352][882:353][893:354][904:355][915:356][926:357][937:358][948:359][959:360][970:369][981:374][992:379][1003:384][1014:389][1025:394][1036:399][1047:400][1058:401][1069:402][1080:403][1091:404][1102:405][1113:406][1124:407][1135:416][1146:421][1157:426][1168:431][1179:436][1190:441][1201:446][1212:447][1223:448][1234:449][1245:450][1256:451][1267:452][1278:453][1289:454][1300:463][1311:468][1322:473][1333:478][1344:483][1355:488][1366:493][1377:494][1388:495][1399:496][1410:497][1421:498][1432:499][1443:500][1454:501][1465:510][1476:515][1487:520][1498:525][1509:530][1520:535][1531:540][1542:541][1553:542][1564:543][1575:544][1586:545][1597:546][1608:547][1619:548][1630:557][1641:562][1652:567][1663:572][1674:577][1685:582][1696:587][1695:587][1694:587][1693:587][1692:587][1703:594][1714:598][1725:602][1736:606][1735:606][1734:606][1733:606][1732:606][1743:613][1754:617][1765:621][1776:625][1775:625][1774:625][1773:625][1772:625][1783:632][1794:636][1805:640][1816:644][1815:644][1814:644][1813:644][1812:644][1823:651][1834:655][1845:659][1856:663][1855:663][1854:663][1853:663][1852:663][1863:670][1874:674][1885:678][1896:682][1895:682][1894:682][1893:682][1892:682][1903:689][1914:693][1925:697][1936:701][1950:702][1964:703][1978:704][1992:705][2006:713][2020:718][2034:723][2048:728][2057:730][2066:732][2075:734][2084:736][2093:745][2102:751][2111:757][2120:763][2132:765][2144:767][2156:769][2168:771][2180:780][2192:786][2204:792][2216:798][2228:800][2240:802][2252:804][2264:806][2276:815][2288:821][2300:827][2312:833][2311:833][2310:833][2309:833][2308:833][2319:840][2330:844][2341:848][2352:852][2351:852][2350:852][2349:852][2348:852][2359:859][2370:863][2381:867][2392:871][2391:871][2390:871][2389:871][2388:871][2399:878][2410:882][2421:886][2432:890][2431:890][2430:890][2429:890][2428:890][2439:897][2450:901][2461:905][2472:909][2471:909][2470:909][2469:909][2468:909][2479:916][2490:920][2501:924][2512:928][2511:928][2510:928][2509:928][2508:928][2519:935][2530:939][2541:943][2552:947][2566:948][2580:949][2594:950][2608:951][2622:959][2636:964][2650:969][2664:974][2676:976][2688:978][2700:980][2712:982][2724:991][2736:997][2748:1003][2760:1009][2769:1011][2778:1013][2787:1015][2796:1017][2805:1026][2814:1032][2823:1038][2832:1044][2844:1046][2856:1048][2868:1050][2880:1052][2892:1061][2904:1067][2916:1073][2928:1079][2927:1079][2926:1079][2925:1079][2924:1079][2935:1086][2946:1090][2957:1094][2968:1098][2967:1098][2966:1098][2965:1098][2964:1098][2975:1105][2986:1109][2997:1113][3008:1117][3007:1117][3006:1117][3005:1117][3004:1117][3015:1124][3026:1128][3037:1132][3048:1136][3047:1136][3046:1136][3045:1136][3044:1136][3055:1143][3066:1147][3077:1151][3088:1155][3087:1155][3086:1155][3085:1155][3084:1155][3095:1162][3106:1166][3117:1170][3128:1174][3127:1174][3126:1174][3125:1174][3124:1174][3135:1181][3146:1185][3157:1189][3168:1193][3182:1194][3196:1195][3210:1196][3224:1197][3238:1205][3252:1210][3266:1215][3280:1220][3292:1222][3304:1224][3316:1226][3328:1228][3340:1237][3352:1243][3364:1249][3376:1255][3388:1257][3400:1259][3412:1261][3424:1263][3436:1272][3448:1278][3460:1284][3472:1290][3481:1292][3490:1294][3499:1296][3508:1298][3517:1307][3526:1313][3535:1319][3544:1325][3543:1325][3542:1325][3541:1325][3540:1325][3551:1332][3562:1336][3573:1340][3584:1344][3588:1345][3592:1346][3596:1347][3600:1348][3604:1349][3608:1350][3612:1357][3616:1362][3615:1362][3614:1362][3613:1362][3612:1362][3623:1369][3634:1373][3645:1377][3656:1381][3660:1382][3664:1383][3668:1384][3672:1385][3676:1386][3680:1387][3684:1394][3688:1399][3687:1399][3686:1399][3685:1399][3684:1399][3695:1406][3706:1410][3717:1414][3728:1418][3732:1419][3736:1420][3740:1421][3744:1422][3748:1423][3752:1424][3756:1431][3760:1436][3759:1436][3758:1436][3757:1436][3756:1436][3767:1443][3778:1447][3789:1451][3800:1455][3804:1456][3808:1457][3812:1458][3816:1459][3820:1460][3824:1461][3828:1468][3832:1473] proof tree [ ; P(_Q, _r), P(_H, _i), P(_D, _e) ; forall y . (P(_P, y) -> P(y, _P)), forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C), P(_G, _N) -> P(_N, _G), P(_C, _O) -> P(_O, _C) => ; P(_C, _F), P(_B, _a) ; ] [ ; P(_F, _C), P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ; P(_Q, _r), P(_H, _i), P(_D, _e) ; forall y . (P(_P, y) -> P(y, _P)), forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C), P(_G, _N) -> P(_N, _G), P(_C, _O) -> P(_O, _C) => ; P(_C, _F), P(_B, _a) ; ] [P(_G, _N) -> P(_N, _G), P(_C, _O) -> P(_O, _C), forall y . (P(_P, y) -> P(y, _P)), exists y . P(_Q, y) ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_C, _F), P(_B, _a) ; ] [ ; P(_F, _C), P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; P(_G, _N) -> P(_N, _G), P(_C, _O) -> P(_O, _C), forall y . (P(_P, y) -> P(y, _P)), exists y . P(_Q, y) ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_C, _F), P(_B, _a) ; ] [ ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_C, _F), P(_B, _a) ; ; P(_F, _C), P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [ ; P(_F, _C), P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [ ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_C, _F), P(_B, _a) ; ; P(_F, _C), P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [P(_F, _C) ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_C, _F), P(_B, _a) ; ] [ ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => P(_C, _F) ; P(_B, _a) ; P(_F, _C) ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [ ; P(_H, _i), P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [P(_H, _i) ; P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [exists y . P(_H, y) ; P(_D, _e) ; forall y . (P(_G, y) -> P(y, _G)), forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [forall y . (P(_G, y) -> P(y, _G)), exists y . P(_H, y) ; P(_D, _e) ; forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)), P(_C, _F) -> P(_F, _C) => ; P(_B, _a) ; ] [P(_C, _F) -> P(_F, _C), forall y . (P(_G, y) -> P(y, _G)), exists y . P(_H, y) ; P(_D, _e) ; forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => ; P(_B, _a) ; ] [ ; P(_D, _e) ; forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => ; P(_B, _a) ; ] [P(_D, _e) ; ; forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => ; P(_B, _a) ; ] [exists y . P(_D, y) ; ; forall y . (P(_C, y) -> P(y, _C)), forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => ; P(_B, _a) ; ] [forall y . (P(_C, y) -> P(y, _C)), exists y . P(_D, y) ; ; forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => ; P(_B, _a) ; ] [ ; ; forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => ; P(_B, _a) ; ] [ ; ; forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => P(_B, _a) ; ; ] [ ; ; forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => exists y . P(y, _a) ; ; ] [ ; ; forall x . (forall y . (P(x, y) -> P(y, x))), forall x . (exists y . P(x, y)) => forall x . (exists y . P(y, x)) ; ; ] [forall x . (forall y . (P(x, y) -> P(y, x))) ; ; forall x . (exists y . P(x, y)) => forall x . (exists y . P(y, x)) ; ; ] [forall x . (exists y . P(x, y)), forall x . (forall y . (P(x, y) -> P(y, x))) ; ; => forall x . (exists y . P(y, x)) ; ; ] [(forall x . (exists y . P(x, y))) & (forall x . (forall y . (P(x, y) -> P(y, x)))) ; ; => forall x . (exists y . P(y, x)) ; ; ] [ ; ; => ((forall x . (exists y . P(x, y))) & (forall x . (forall y . (P(x, y) -> P(y, x))))) -> (forall x . (exists y . P(y, x))) ; ; ] with: P(_F, _C) eq P(_B, _a) P(_Q, _r) eq P(_C, _F) _e notin _B _e notin _C _e notin _D _i notin _B _i notin _C _i notin _D _i notin _F _i notin _G _i notin _H where: [_F->_r, _C->_a, _Q->_a, _B->_r] [proof COMPLETE!!!] considered 1473 sequents # Even(zero)&(\x.Even(x)->Odd(succ(x)))&(\x.Odd(x)->Even(succ(x)))->Even(succ(succ(zero))) *** 2 is even Even(zero)&(\x.Even(x)->Odd(succ(x)))&(\x.Odd(x)->Even(succ(x)))->Even(succ(succ(zero))) *** 2 is even ((Even(zero) & (forall x . (Even(x) -> Odd(succ(x))))) & (forall x . (Odd(x) -> Even(succ(x))))) -> Even(succ(succ(zero))) ((([(Even([zero:Atom])):Pred] & (forall [x:Atom] . ([(Even([x:Atom])):Pred] -> [(Odd([(succ([x:Atom])):Func])):Pred]))) & (forall [x:Atom] . ([(Odd([x:Atom])):Pred] -> [(Even([(succ([x:Atom])):Func])):Pred]))) -> [(Even([(succ([(succ([zero:Atom])):Func])):Func])):Pred]) proof tree [ ; Odd(succ(_B)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(_B), Odd(_A), Even(succ(succ(zero))) ; ; Odd(succ(_B)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Odd(succ(_B)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(_B), Odd(_A), Even(succ(succ(zero))) ; ; Odd(succ(_B)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(succ(_A)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(_B), Odd(_A), Even(succ(succ(zero))) ; ; Odd(succ(_B)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => Even(_B) ; Odd(_A), Even(succ(succ(zero))) ; Odd(succ(_B)) ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(succ(_A)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => Even(_B) ; Odd(_A), Even(succ(succ(zero))) ; Odd(succ(_B)) ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ; Even(succ(_A)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ] [ ; Even(succ(_A)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ; Even(succ(_A)), Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ] [Even(succ(_A)) ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Odd(_A), Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => Odd(_A) ; Even(succ(succ(zero))) ; Even(succ(_A)) ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) => ; Even(succ(succ(zero))) ; ] [Even(_B) -> Odd(succ(_B)) ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))), Odd(_A) -> Even(succ(_A)) => ; Even(succ(succ(zero))) ; ] [Odd(_A) -> Even(succ(_A)), Even(_B) -> Odd(succ(_B)) ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))) => ; Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))) => ; Even(succ(succ(zero))) ; ] [ ; Even(zero) ; forall x . (Odd(x) -> Even(succ(x))), forall x . (Even(x) -> Odd(succ(x))) => Even(succ(succ(zero))) ; ; ] [forall x . (Odd(x) -> Even(succ(x))) ; Even(zero) ; forall x . (Even(x) -> Odd(succ(x))) => Even(succ(succ(zero))) ; ; ] [forall x . (Even(x) -> Odd(succ(x))), forall x . (Odd(x) -> Even(succ(x))) ; Even(zero) ; => Even(succ(succ(zero))) ; ; ] [Even(zero), forall x . (Even(x) -> Odd(succ(x))), forall x . (Odd(x) -> Even(succ(x))) ; ; => Even(succ(succ(zero))) ; ; ] [Even(zero) & (forall x . (Even(x) -> Odd(succ(x)))), forall x . (Odd(x) -> Even(succ(x))) ; ; => Even(succ(succ(zero))) ; ; ] [(Even(zero) & (forall x . (Even(x) -> Odd(succ(x))))) & (forall x . (Odd(x) -> Even(succ(x)))) ; ; => Even(succ(succ(zero))) ; ; ] [ ; ; => ((Even(zero) & (forall x . (Even(x) -> Odd(succ(x))))) & (forall x . (Odd(x) -> Even(succ(x))))) -> Even(succ(succ(zero))) ; ; ] with: Even(succ(_A)) eq Even(succ(succ(zero))) Even(zero) eq Even(_B) Odd(succ(_B)) eq Odd(_A) where: [_A->succ(zero), _B->zero] [proof COMPLETE!!!] considered 13357 sequents