%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN785-1 : TPTP v9.0.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 10:04:54 PM UTC 2025 % Result : Satisfiable 19.85s 10.18s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.10 % Problem : SYN785-1 : TPTP v9.0.0. Released v2.5.0. % 0.06/0.11 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.11/0.29 % Computer : n032.cluster.edu % 0.11/0.29 % Model : x86_64 x86_64 % 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.29 % Memory : 8042.1875MB % 0.11/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.29 % CPULimit : 300 % 0.11/0.29 % WCLimit : 300 % 0.11/0.29 % DateTime : Wed Apr 9 08:19:45 EDT 2025 % 0.11/0.29 % CPUTime : % 19.85/10.18 % 19.85/10.18 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.85/10.18 % 19.85/10.18 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.85/10.19 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf3 > skf2 % 19.85/10.19 % 19.85/10.19 %Foreground sorts: % 19.85/10.19 % 19.85/10.19 % 19.85/10.19 %Background operators: % 19.85/10.19 % 19.85/10.19 % 19.85/10.19 %Foreground operators: % 19.85/10.19 tff(skf3, type, skf3: $i > $i). % 19.85/10.19 tff(ssPv1, type, ssPv1: $i > $o). % 19.85/10.19 tff(ssPv3, type, ssPv3: $i > $o). % 19.85/10.19 tff(skf2, type, skf2: $i > $i). % 19.85/10.19 tff(ssRr, type, ssRr: ($i * $i) > $o). % 19.85/10.19 tff(ssPv4, type, ssPv4: $i > $o). % 19.85/10.19 tff(ssPv2, type, ssPv2: $i > $o). % 19.85/10.19 % 19.85/10.19 %Saturated clause set: % 19.85/10.19 tff(c_49492, plain, (![U_1613, V_1615]: (~ssPv2(skf2(U_1613)) | ~ssPv3(skf2(skf2(U_1613))) | ~ssPv4(V_1615) | ~ssRr(skf2(U_1613), V_1615) | ~ssPv4(skf2(U_1613)) | ~ssPv2(U_1613)))). % 19.85/10.19 tff(c_48257, plain, (![U_1523, W_411, V_412]: (~ssPv2(skf2(U_1523)) | ~ssPv3(W_411) | ~ssRr(skf2(U_1523), W_411) | ~ssPv4(V_412) | ~ssRr(skf2(U_1523), V_412) | ~ssPv4(skf2(U_1523)) | ~ssPv2(U_1523)))). % 19.85/10.19 tff(c_48381, plain, (![U_1528, W_303, U_304]: (ssPv2(U_1528) | ~ssPv1(W_303) | ~ssRr(W_303, U_1528) | ~ssPv4(U_304) | ~ssRr(U_304, U_1528) | ssPv2(skf2(U_1528)) | ~ssPv3(skf2(U_1528)) | ~ssPv1(U_1528)))). % 19.85/10.19 tff(c_49471, plain, (![U_1608]: (~ssPv3(skf3(skf3(U_1608))) | ssPv1(skf3(skf3(U_1608))) | ssPv1(U_1608) | ssPv2(skf3(U_1608)) | ~ssPv1(skf3(U_1608))))). % 19.85/10.19 tff(c_49446, plain, (![U_1606]: (ssPv1(skf3(skf3(U_1606))) | ssPv4(skf3(skf3(U_1606))) | ssPv1(U_1606) | ssPv2(skf3(U_1606)) | ~ssPv1(skf3(U_1606))))). % 19.85/10.19 tff(c_49441, plain, (![U_1605, U_1604]: (ssPv1(skf3(skf3(U_1605))) | ssPv4(U_1604) | ~ssRr(U_1604, skf3(U_1605)) | ssPv1(U_1605) | ssPv2(skf3(U_1605)) | ~ssPv1(skf3(U_1605))))). % 19.85/10.19 tff(c_49360, plain, (![W_376, U_377, U_1590]: (ssPv1(W_376) | ssPv4(U_377) | ~ssRr(W_376, skf3(U_1590)) | ~ssRr(U_377, skf3(U_1590)) | ssPv1(U_1590) | ssPv2(skf3(U_1590)) | ~ssPv1(skf3(U_1590))))). % 19.85/10.19 tff(c_49431, plain, (![U_1598, U_1600]: (ssPv2(skf3(U_1598)) | ~ssPv4(U_1600) | ~ssRr(U_1600, skf3(U_1598)) | ssPv3(skf3(U_1598)) | ~ssPv2(U_1598) | ~ssPv1(skf3(skf3(U_1598)))))). % 19.85/10.19 tff(c_49415, plain, (![U_1596]: (ssPv2(skf2(U_1596)) | ssPv4(skf2(U_1596)) | ssPv2(skf2(skf2(U_1596))) | ~ssPv1(U_1596) | ~ssPv2(skf3(skf2(U_1596)))))). % 19.85/10.19 tff(c_49375, plain, (![U_1594]: (ssPv2(skf2(U_1594)) | ~ssPv4(skf3(skf2(U_1594))) | ssPv4(skf2(U_1594)) | ssPv2(skf2(skf2(U_1594))) | ~ssPv1(U_1594)))). % 19.85/10.19 tff(c_49368, plain, (![U_2, U_1593]: (ssPv2(skf2(U_2)) | ~ssPv4(U_1593) | ~ssRr(U_1593, skf2(U_2)) | ssPv4(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ~ssPv1(U_2)))). % 19.85/10.19 tff(c_49320, plain, (![U_1589]: (ssPv1(U_1589) | ssPv2(skf3(U_1589)) | ssPv2(skf2(skf3(U_1589))) | ~ssPv1(skf3(U_1589))))). % 19.85/10.19 tff(c_49284, plain, (![U_1585]: (~ssPv3(skf3(skf2(U_1585))) | ssPv1(skf3(skf2(U_1585))) | ~ssPv2(U_1585) | ~ssPv1(skf2(U_1585))))). % 19.85/10.19 tff(c_49260, plain, (![U_1583]: (ssPv1(skf3(skf2(U_1583))) | ssPv4(skf3(skf2(U_1583))) | ~ssPv2(U_1583) | ~ssPv1(skf2(U_1583))))). % 19.85/10.19 tff(c_49217, plain, (![U_1579, U_1578]: (ssPv1(skf3(skf2(U_1579))) | ssPv4(U_1578) | ~ssRr(U_1578, skf2(U_1579)) | ~ssPv2(U_1579) | ~ssPv1(skf2(U_1579))))). % 19.85/10.19 tff(c_49227, plain, (![U_1580]: (ssPv1(U_1580) | ssPv4(skf3(skf2(U_1580))) | ~ssPv2(U_1580) | ~ssPv1(skf2(U_1580))))). % 19.85/10.19 tff(c_49218, plain, (![U_2, U_1578]: (ssPv1(U_2) | ssPv4(U_1578) | ~ssRr(U_1578, skf2(U_2)) | ~ssPv2(U_2) | ~ssPv1(skf2(U_2))))). % 19.85/10.19 tff(c_47040, plain, (![W_376, U_377, U_1482]: (ssPv1(W_376) | ssPv4(U_377) | ~ssRr(W_376, skf2(U_1482)) | ~ssRr(U_377, skf2(U_1482)) | ~ssPv2(U_1482) | ~ssPv1(skf2(U_1482))))). % 19.85/10.19 tff(c_41879, plain, (![U_580]: (ssPv1(skf2(skf3(U_580))) | ~ssPv3(skf2(skf3(U_580))) | ssPv3(skf3(U_580)) | ~ssPv2(U_580) | ~ssPv1(skf3(skf3(U_580)))))). % 19.85/10.19 tff(c_41878, plain, (![U_591]: (ssPv1(skf3(skf3(U_591))) | ~ssPv3(skf3(skf3(U_591))) | ssPv1(U_591) | ssPv2(skf3(skf3(U_591))) | ~ssPv1(skf3(U_591))))). % 19.85/10.19 tff(c_48705, plain, (![U_580]: (ssPv3(skf2(skf3(U_580))) | ~ssPv2(skf3(U_580)) | ssPv3(skf3(U_580)) | ~ssPv2(U_580) | ~ssPv1(skf3(skf3(U_580)))))). % 19.85/10.20 tff(c_41897, plain, (![U_1]: (ssPv1(skf2(skf3(U_1))) | ~ssPv3(skf2(skf3(U_1))) | ssPv2(skf3(U_1)) | ~ssPv1(skf3(U_1)) | ~ssPv4(U_1)))). % 19.85/10.20 tff(c_41887, plain, (![U_431]: (ssPv1(skf3(skf3(U_431))) | ~ssPv3(skf3(skf3(U_431))) | ssPv3(skf3(U_431)) | ssPv3(U_431) | ~ssPv4(skf3(U_431))))). % 19.85/10.20 tff(c_43517, plain, (![U_580]: (~ssPv3(skf2(skf3(U_580))) | ~ssPv2(skf3(U_580)) | ssPv3(skf3(U_580)) | ~ssPv2(U_580) | ~ssPv1(skf3(skf3(U_580)))))). % 19.85/10.20 tff(c_48961, plain, (![U_1561]: (ssPv1(U_1561) | ssPv4(skf3(skf2(U_1561))) | ssPv1(skf2(skf2(U_1561))) | ~ssPv1(skf2(U_1561))))). % 19.85/10.20 tff(c_48950, plain, (![U_1560]: (~ssPv3(skf3(U_1560)) | ssPv1(skf3(U_1560)) | ssPv1(skf2(U_1560)) | ~ssPv1(U_1560)))). % 19.85/10.20 tff(c_48914, plain, (![U_2, U_1556]: (ssPv1(U_2) | ssPv4(U_1556) | ~ssRr(U_1556, skf2(U_2)) | ssPv1(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 19.85/10.20 tff(c_48920, plain, (![U_1]: (ssPv1(skf3(U_1)) | ssPv4(skf3(U_1)) | ssPv1(skf2(U_1)) | ~ssPv1(U_1)))). % 19.85/10.20 tff(c_48913, plain, (![U_1, U_1556]: (ssPv1(skf3(U_1)) | ssPv4(U_1556) | ~ssRr(U_1556, U_1) | ssPv1(skf2(U_1)) | ~ssPv1(U_1)))). % 19.85/10.20 tff(c_48477, plain, (![W_376, U_377, U_1530]: (ssPv1(W_376) | ssPv4(U_377) | ~ssRr(W_376, U_1530) | ~ssRr(U_377, U_1530) | ssPv1(skf2(U_1530)) | ~ssPv1(U_1530)))). % 19.85/10.20 tff(c_48896, plain, (![U_1553]: (ssPv2(skf2(U_1553)) | ~ssPv1(U_1553) | ~ssPv2(skf2(skf2(U_1553))) | ~ssPv2(skf3(skf2(U_1553)))))). % 19.85/10.20 tff(c_48872, plain, (![U_1551]: (ssPv2(skf2(U_1551)) | ~ssPv1(U_1551) | ~ssPv4(skf3(skf2(U_1551))) | ~ssPv2(skf2(skf2(U_1551)))))). % 19.85/10.20 tff(c_48837, plain, (![U_2, U_1547]: (ssPv2(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(U_1547) | ~ssRr(U_1547, skf2(U_2)) | ~ssPv2(skf2(skf2(U_2)))))). % 19.85/10.20 tff(c_48844, plain, (![U_2]: (ssPv2(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ~ssPv4(U_2) | ~ssPv2(skf2(skf2(U_2)))))). % 19.85/10.20 tff(c_48836, plain, (![U_1, U_1547]: (ssPv2(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv4(U_1547) | ~ssRr(U_1547, U_1) | ~ssPv2(skf2(U_1))))). % 19.85/10.20 tff(c_48148, plain, (![U_2, W_303, U_304]: (ssPv2(U_2) | ~ssPv1(W_303) | ~ssRr(W_303, U_2) | ~ssPv4(U_304) | ~ssRr(U_304, U_2) | ~ssPv2(skf2(U_2))))). % 19.85/10.20 tff(c_48792, plain, (![U_1543]: (ssPv1(skf2(skf2(U_1543))) | ssPv4(skf2(U_1543)) | ssPv2(skf2(skf2(U_1543))) | ~ssPv1(U_1543)))). % 19.85/10.20 tff(c_48768, plain, (![U_2]: (ssPv3(skf2(skf2(U_2))) | ssPv4(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ~ssPv1(U_2)))). % 19.85/10.20 tff(c_48739, plain, (![U_1541]: (ssPv2(skf2(U_1541)) | ssPv3(skf2(U_1541)) | ssPv4(U_1541) | ~ssPv4(skf2(U_1541))))). % 19.85/10.20 tff(c_48585, plain, (![U_580]: (~ssPv1(skf2(skf3(U_580))) | ssPv3(skf3(U_580)) | ~ssPv2(U_580) | ~ssPv1(skf3(skf3(U_580)))))). % 19.85/10.20 tff(c_48683, plain, (![U_1522]: (ssPv3(skf2(U_1522)) | ~ssPv4(skf2(U_1522)) | ~ssPv2(U_1522)))). % 19.85/10.20 tff(c_48590, plain, (![U_431]: (~ssPv1(skf3(skf3(U_431))) | ssPv3(skf3(U_431)) | ssPv3(U_431) | ~ssPv4(skf3(U_431))))). % 19.85/10.20 tff(c_48659, plain, (![U_1535]: (~ssPv1(skf2(U_1535)) | ~ssPv1(skf3(U_1535)) | ssPv3(U_1535) | ~ssPv4(U_1535)))). % 19.85/10.20 tff(c_48594, plain, (![U_1]: (~ssPv1(skf3(U_1)) | ssPv3(U_1) | ssPv3(skf2(U_1)) | ~ssPv4(U_1)))). % 19.85/10.20 tff(c_48619, plain, (![U_1533]: (ssPv4(U_1533) | ~ssPv1(skf3(U_1533))))). % 19.85/10.20 tff(c_48515, plain, (![U_1531]: (~ssPv4(U_1531) | ~ssPv1(U_1531)))). % 19.85/10.20 tff(c_48425, plain, (![U_1478]: (ssPv1(skf2(U_1478)) | ssPv2(skf2(U_1478)) | ~ssPv1(U_1478)))). % 19.85/10.20 tff(c_48335, plain, (![U_1527]: (ssPv2(skf2(U_1527)) | ~ssPv3(skf2(U_1527)) | ssPv4(skf2(U_1527)) | ~ssPv1(U_1527)))). % 19.85/10.20 tff(c_45833, plain, (![U_2]: (ssPv2(skf2(U_2)) | ~ssPv1(skf3(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(U_2) | ~ssPv2(U_2)))). % 19.85/10.20 tff(c_48256, plain, (![U_1523]: (~ssPv3(skf2(U_1523)) | ~ssPv4(skf2(U_1523)) | ~ssPv2(U_1523)))). % 19.85/10.20 tff(c_48217, plain, (![U_1522]: (ssPv1(skf2(skf2(U_1522))) | ~ssPv4(skf2(U_1522)) | ~ssPv2(U_1522)))). % 19.85/10.20 tff(c_48163, plain, (![U_1]: (ssPv1(skf3(U_1)) | ~ssPv2(U_1) | ssPv3(U_1) | ssPv3(skf2(U_1)) | ~ssPv4(U_1)))). % 19.85/10.20 tff(c_41899, plain, (![U_1]: (ssPv1(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ssPv3(U_1) | ssPv3(skf2(U_1)) | ~ssPv4(U_1)))). % 19.85/10.20 tff(c_48085, plain, (![U_1518]: (ssPv4(U_1518) | ~ssPv2(U_1518)))). % 19.85/10.20 tff(c_41877, plain, (![U_641]: (~ssPv3(skf3(skf3(U_641))) | ssPv1(skf3(skf3(U_641))) | ~ssPv1(skf3(U_641)) | ~ssPv2(U_641)))). % 19.85/10.20 tff(c_47691, plain, (![U_1505]: (~ssPv1(skf2(U_1505)) | ~ssPv1(skf2(skf2(U_1505))) | ssPv3(skf2(U_1505)) | ~ssPv2(U_1505)))). % 19.85/10.20 tff(c_47693, plain, (![U_1505]: (ssPv2(skf2(U_1505)) | ~ssPv1(skf2(skf2(U_1505))) | ssPv3(skf2(U_1505)) | ~ssPv2(U_1505)))). % 19.85/10.20 tff(c_40807, plain, (![U_2]: (~ssPv1(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(skf3(skf2(U_2))) | ~ssPv2(U_2)))). % 19.85/10.20 tff(c_40805, plain, (![U_543]: (~ssPv1(skf3(skf3(U_543))) | ssPv2(skf3(U_543)) | ssPv1(skf2(skf3(U_543))) | ~ssPv3(U_543)))). % 19.85/10.20 tff(c_45669, plain, (![U_543]: (~ssPv4(skf3(U_543)) | ssPv2(skf3(U_543)) | ssPv1(skf2(skf3(U_543))) | ~ssPv3(U_543)))). % 19.85/10.20 tff(c_47563, plain, (![U_1498]: (ssPv2(skf3(U_1498)) | ~ssPv3(skf3(U_1498)) | ~ssPv4(U_1498)))). % 19.85/10.20 tff(c_44770, plain, (![U_1]: (ssPv3(skf3(U_1)) | ~ssPv2(U_1) | ssPv3(U_1) | ssPv3(skf2(U_1)) | ~ssPv4(U_1)))). % 19.85/10.20 tff(c_43861, plain, (![U_2]: (~ssPv2(skf2(U_2)) | ssPv3(skf2(U_2)) | ssPv1(skf3(skf2(U_2))) | ~ssPv2(U_2)))). % 19.85/10.20 tff(c_47435, plain, (![U_1494]: (~ssPv2(skf2(U_1494)) | ssPv1(U_1494) | ~ssPv2(U_1494)))). % 19.85/10.20 tff(c_47374, plain, (![U_1492]: (~ssPv2(U_1492) | ~ssPv2(skf2(U_1492))))). % 19.85/10.20 tff(c_47002, plain, (![U_2]: (~ssPv2(U_2) | ssPv2(skf2(skf2(U_2))) | ~ssPv1(skf2(U_2))))). % 19.85/10.20 tff(c_46993, plain, (![U_485, U_1479]: (~ssPv2(U_485) | ~ssRr(U_485, U_1479) | ssPv2(skf2(U_1479)) | ~ssPv1(U_1479)))). % 19.85/10.20 tff(c_46950, plain, (![U_1478]: (ssPv3(skf2(U_1478)) | ssPv2(skf2(U_1478)) | ~ssPv1(U_1478)))). % 19.85/10.20 tff(c_43343, plain, (![U_543]: (ssPv3(skf3(U_543)) | ssPv2(skf3(U_543)) | ssPv1(skf2(skf3(U_543))) | ~ssPv3(U_543)))). % 19.85/10.20 tff(c_40770, plain, (![U_2]: (~ssPv1(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv4(U_2) | ~ssPv4(skf2(U_2))))). % 19.85/10.20 tff(c_40771, plain, (![U_1]: (~ssPv1(skf2(skf3(U_1))) | ssPv1(skf3(U_1)) | ~ssPv2(skf3(U_1)) | ~ssPv2(U_1)))). % 19.85/10.20 tff(c_46676, plain, (![U_1]: (ssPv2(skf3(U_1)) | ~ssPv3(skf3(U_1)) | ~ssPv3(U_1)))). % 19.85/10.20 tff(c_46546, plain, (![U_1464]: (~ssPv1(skf2(U_1464)) | ~ssPv1(U_1464)))). % 19.85/10.21 tff(c_40780, plain, (![U_907]: (ssPv1(U_907) | ssPv3(skf3(U_907)) | ssPv2(skf3(U_907)) | ~ssPv1(skf3(skf3(U_907)))))). % 19.85/10.21 tff(c_46386, plain, (![U_1460]: (ssPv1(skf2(U_1460)) | ~ssPv3(skf2(U_1460)) | ~ssPv3(U_1460)))). % 19.85/10.21 tff(c_46324, plain, (![U_1458]: (~ssPv1(skf3(U_1458)) | ~ssPv3(U_1458)))). % 19.85/10.21 tff(c_46208, plain, (![U_1454]: (~ssPv1(skf3(U_1454)) | ~ssPv1(U_1454)))). % 19.85/10.21 tff(c_46082, plain, (![U_1]: (ssPv4(skf3(U_1)) | ssPv3(skf3(U_1)) | ~ssPv1(U_1)))). % 19.85/10.21 tff(c_45992, plain, (![U_1450]: (ssPv4(U_1450) | ~ssPv1(skf2(U_1450))))). % 19.85/10.21 tff(c_45526, plain, (![U_1]: (~ssPv2(skf2(U_1)) | ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(skf3(U_1))))). % 19.85/10.21 tff(c_45517, plain, (![U_554]: (ssPv1(U_554) | ~ssPv4(skf3(U_554)) | ~ssPv2(skf3(skf3(U_554)))))). % 19.85/10.21 tff(c_45510, plain, (![U_2]: (ssPv2(U_2) | ~ssPv3(U_2) | ~ssPv2(skf2(U_2))))). % 19.85/10.21 tff(c_45519, plain, (![U_1]: (ssPv1(skf2(U_1)) | ~ssPv4(U_1) | ~ssPv2(skf3(U_1))))). % 19.85/10.21 tff(c_45506, plain, (![U_2]: (~ssPv2(skf2(U_2)) | ~ssPv4(U_2)))). % 19.85/10.21 tff(c_45504, plain, (![U_1424]: (~ssPv2(U_1424) | ~ssPv2(skf3(U_1424))))). % 19.85/10.21 tff(c_45402, plain, (![U_1437]: (~ssPv2(U_1437) | ~ssPv3(U_1437)))). % 19.85/10.21 tff(c_41303, plain, (![U_545]: (ssPv4(skf3(U_545)) | ssPv3(skf3(U_545)) | ssPv2(skf3(U_545)) | ~ssPv3(U_545)))). % 19.85/10.21 tff(c_40806, plain, (![U_2]: (~ssPv1(skf2(skf2(U_2))) | ssPv3(skf2(U_2)) | ssPv1(U_2) | ~ssPv2(U_2)))). % 19.85/10.21 tff(c_44706, plain, (![U_417]: (ssPv3(skf3(U_417)) | ~ssPv4(skf3(U_417)) | ~ssPv2(U_417)))). % 19.85/10.21 tff(c_44655, plain, (![U_1422]: (ssPv3(U_1422) | ~ssPv2(skf3(U_1422))))). % 19.85/10.21 tff(c_44486, plain, (![U_1419]: (~ssPv1(U_1419) | ~ssPv2(skf3(U_1419))))). % 19.85/10.21 tff(c_44156, plain, (![U_1413]: (ssPv2(skf3(U_1413)) | ssPv1(U_1413) | ~ssPv3(U_1413)))). % 19.85/10.21 tff(c_43801, plain, (![U_2]: (ssPv3(U_2) | ~ssPv2(skf2(U_2)) | ~ssPv2(U_2)))). % 19.85/10.21 tff(c_40811, plain, (![U_240]: (~ssPv1(skf2(U_240)) | ssPv3(U_240) | ssPv2(U_240) | ~ssPv1(skf3(U_240))))). % 19.85/10.21 tff(c_40795, plain, (![U_1]: (ssPv1(skf2(U_1)) | ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(skf3(U_1))))). % 19.85/10.21 tff(c_39936, plain, (![U_1]: (~ssPv1(skf2(U_1)) | ~ssPv2(U_1) | ssPv3(U_1) | ~ssPv4(U_1)))). % 19.85/10.21 tff(c_40951, plain, (![U_915]: (~ssPv4(U_915) | ssPv1(U_915) | ~ssPv3(U_915)))). % 19.85/10.21 tff(c_41555, plain, (![U_1374]: (~ssPv3(U_1374) | ~ssPv1(U_1374)))). % 19.85/10.21 tff(c_40803, plain, (![U_2]: (~ssPv1(skf2(U_2)) | ~ssPv3(U_2)))). % 19.85/10.21 tff(c_40508, plain, (![U_681]: (~ssPv1(U_681) | ~ssPv2(U_681)))). % 19.85/10.21 tff(c_32491, plain, (![U_2]: (ssPv1(skf3(skf2(U_2))) | ~ssPv3(skf3(skf2(U_2))) | ssPv1(skf2(U_2)) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2)))). % 19.85/10.21 tff(c_6467, plain, (![U_664, U_665]: (ssPv2(U_664) | ~ssPv1(skf3(U_664)) | ~ssPv2(U_665) | ~ssRr(U_665, skf3(U_664)) | ssPv3(skf3(U_664)) | ssPv2(skf3(U_664)) | ~ssPv1(skf3(skf3(U_664)))))). % 19.85/10.21 tff(c_3598, plain, (![U_2, W_526, U_527]: (ssPv2(U_2) | ~ssPv1(W_526) | ~ssRr(W_526, U_2) | ~ssPv4(U_527) | ~ssRr(U_527, U_2) | ssPv4(U_2) | ~ssPv1(U_2) | ~ssPv3(skf2(U_2))))). % 19.85/10.21 tff(c_21024, plain, (![U_991]: (ssPv1(skf2(U_991)) | ~ssPv2(skf2(U_991)) | ~ssPv2(U_991)))). % 19.85/10.21 tff(c_16466, plain, (![U_920]: (ssPv4(U_920) | ssPv1(skf2(U_920)) | ~ssPv3(skf2(U_920))))). % 19.85/10.21 tff(c_14199, plain, (![U_867]: (ssPv2(skf3(U_867)) | ~ssPv2(U_867) | ssPv3(U_867) | ssPv3(skf2(U_867)) | ~ssPv4(U_867)))). % 19.85/10.21 tff(c_1736, plain, (![U_413]: (ssPv1(skf3(U_413)) | ssPv1(U_413) | ~ssPv2(skf3(U_413)) | ssPv3(skf3(U_413)) | ssPv3(skf2(skf3(U_413))) | ~ssPv4(skf3(U_413))))). % 19.85/10.21 tff(c_1399, plain, (![U_375]: (ssPv2(U_375) | ~ssPv2(skf3(U_375)) | ssPv3(skf3(U_375)) | ssPv3(skf2(skf3(U_375))) | ~ssPv4(skf3(U_375))))). % 19.85/10.21 tff(c_7153, plain, (![U_693, U_695]: (ssPv2(skf3(U_693)) | ~ssPv4(U_693) | ~ssPv1(skf3(skf3(U_693))) | ~ssPv4(U_695) | ~ssRr(U_695, skf3(U_693))))). % 19.85/10.21 tff(c_6915, plain, (![U_683, U_684]: (ssPv2(skf3(U_683)) | ssPv1(U_683) | ssPv2(U_684) | ~ssPv3(skf2(skf3(U_683))) | ~ssRr(U_684, skf3(U_683))))). % 19.85/10.21 tff(c_881, plain, (![U_1, W_303, U_304]: (ssPv2(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv1(W_303) | ~ssRr(W_303, skf3(U_1)) | ~ssPv4(U_304) | ~ssRr(U_304, skf3(U_1))))). % 19.85/10.21 tff(c_1524, plain, (![U_1, U_388, W_389]: (ssPv2(skf3(U_1)) | ssPv1(U_1) | ssPv2(U_388) | ~ssPv3(W_389) | ~ssRr(skf3(U_1), W_389) | ~ssRr(U_388, skf3(U_1))))). % 19.85/10.21 tff(c_6512, plain, (![U_669, U_671]: (ssPv3(skf3(U_669)) | ssPv2(U_669) | ssPv1(skf3(skf3(U_669))) | ~ssPv2(U_671) | ~ssRr(U_671, skf3(U_669))))). % 19.85/10.21 tff(c_5230, plain, (![U_613, U_614]: (ssPv2(skf3(skf3(U_613))) | ~ssPv2(skf3(U_613)) | ~ssPv2(U_613) | ~ssPv2(U_614) | ~ssRr(U_614, skf3(U_613))))). % 19.85/10.21 tff(c_1243, plain, (![U_1, W_360, U_361]: (ssPv3(skf3(U_1)) | ssPv2(U_1) | ssPv1(W_360) | ~ssRr(W_360, skf3(U_1)) | ~ssPv2(U_361) | ~ssRr(U_361, skf3(U_1))))). % 19.85/10.21 tff(c_6278, plain, (![U_653, U_655]: (ssPv4(skf3(U_653)) | ssPv2(U_653) | ssPv4(skf2(skf3(U_653))) | ~ssPv1(U_655) | ~ssRr(U_655, skf3(U_653))))). % 19.85/10.21 tff(c_5719, plain, (![U_625, U_627]: (ssPv2(U_625) | ~ssPv1(skf3(U_625)) | ~ssPv3(skf2(skf3(U_625))) | ~ssPv2(U_627) | ~ssRr(U_627, skf3(U_625))))). % 19.85/10.21 tff(c_6277, plain, (![U_1, U_655]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ssPv4(U_1) | ~ssPv1(U_655) | ~ssRr(U_655, skf3(U_1))))). % 19.85/10.21 tff(c_1642, plain, (![U_1, W_403, U_404]: (ssPv4(skf3(U_1)) | ssPv2(U_1) | ssPv4(W_403) | ~ssRr(skf3(U_1), W_403) | ~ssPv1(U_404) | ~ssRr(U_404, skf3(U_1))))). % 19.85/10.21 tff(c_6001, plain, (![U_638, U_640]: (ssPv4(skf3(U_638)) | ssPv3(skf3(skf3(U_638))) | ~ssPv1(U_638) | ~ssPv1(U_640) | ~ssRr(U_640, skf3(U_638))))). % 19.85/10.21 tff(c_6006, plain, (![U_641]: (ssPv1(skf3(skf3(U_641))) | ssPv4(skf3(skf3(U_641))) | ~ssPv1(skf3(U_641)) | ~ssPv2(U_641)))). % 19.85/10.21 tff(c_4609, plain, (![U_587, U_586]: (ssPv1(skf3(skf3(U_587))) | ssPv4(U_586) | ~ssPv1(skf3(U_587)) | ~ssPv2(U_587) | ~ssRr(U_586, skf3(U_587))))). % 19.85/10.21 tff(c_1123, plain, (![U_1, W_341, U_343]: (ssPv4(skf3(U_1)) | ssPv3(W_341) | ~ssPv1(U_1) | ~ssRr(W_341, skf3(U_1)) | ~ssPv1(U_343) | ~ssRr(U_343, skf3(U_1))))). % 19.85/10.21 tff(c_1344, plain, (![U_1, W_370, U_371]: (ssPv2(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv3(W_370) | ~ssRr(skf3(U_1), W_370) | ~ssPv2(U_371) | ~ssRr(U_371, skf3(U_1))))). % 19.85/10.21 tff(c_4919, plain, (![U_598, U_600]: (ssPv3(skf3(U_598)) | ssPv4(U_598) | ~ssPv2(skf2(skf3(U_598))) | ~ssPv1(U_600) | ~ssRr(U_600, skf3(U_598))))). % 19.85/10.21 tff(c_943, plain, (![W_313, U_1, U_316]: (ssPv2(W_313) | ~ssPv2(skf3(U_1)) | ~ssPv2(U_1) | ~ssRr(W_313, skf3(U_1)) | ~ssPv2(U_316) | ~ssRr(U_316, skf3(U_1))))). % 19.85/10.21 tff(c_1208, plain, (![U_1, W_352, U_353]: (ssPv3(skf3(U_1)) | ssPv4(U_1) | ~ssPv2(W_352) | ~ssRr(skf3(U_1), W_352) | ~ssPv1(U_353) | ~ssRr(U_353, skf3(U_1))))). % 19.85/10.21 tff(c_4666, plain, (![U_591]: (ssPv1(U_591) | ssPv2(skf3(skf3(U_591))) | ssPv4(skf3(skf3(U_591))) | ~ssPv1(skf3(U_591))))). % 19.85/10.21 tff(c_4268, plain, (![U_566, U_568]: (ssPv1(U_566) | ssPv2(skf3(skf3(U_566))) | ssPv4(U_568) | ~ssPv1(skf3(U_566)) | ~ssRr(U_568, skf3(U_566))))). % 19.85/10.22 tff(c_1407, plain, (![W_376, U_377, U_1]: (ssPv1(W_376) | ssPv4(U_377) | ~ssPv1(skf3(U_1)) | ~ssPv2(U_1) | ~ssRr(W_376, skf3(U_1)) | ~ssRr(U_377, skf3(U_1))))). % 19.85/10.22 tff(c_4536, plain, (![U_580]: (ssPv3(skf3(U_580)) | ssPv4(skf2(skf3(U_580))) | ~ssPv2(U_580) | ~ssPv1(skf3(skf3(U_580)))))). % 19.85/10.22 tff(c_2663, plain, (![U_1, U_476]: (ssPv3(skf3(U_1)) | ssPv4(skf2(skf3(U_1))) | ~ssPv2(U_1) | ~ssPv1(U_476) | ~ssRr(U_476, skf3(U_1))))). % 19.85/10.22 tff(c_1606, plain, (![U_1, W_395, V_396]: (ssPv1(U_1) | ~ssPv1(skf3(U_1)) | ~ssPv1(W_395) | ~ssRr(skf3(U_1), W_395) | ~ssPv4(V_396) | ~ssRr(skf3(U_1), V_396)))). % 19.85/10.22 tff(c_1002, plain, (![U_1, W_322, U_323]: (ssPv1(U_1) | ssPv2(W_322) | ssPv4(U_323) | ~ssPv1(skf3(U_1)) | ~ssRr(W_322, skf3(U_1)) | ~ssRr(U_323, skf3(U_1))))). % 19.85/10.22 tff(c_3760, plain, (![U_540, U_542]: (ssPv1(U_540) | ssPv3(skf3(skf3(U_540))) | ~ssPv4(skf3(U_540)) | ~ssPv2(U_542) | ~ssRr(U_542, skf3(U_540))))). % 19.85/10.22 tff(c_2423, plain, (![U_2, U_461]: (ssPv1(skf2(skf2(U_2))) | ssPv3(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv2(U_461) | ~ssRr(U_461, skf2(U_2))))). % 19.85/10.22 tff(c_2173, plain, (![U_1, U_445]: (ssPv4(skf3(U_1)) | ssPv2(skf2(skf3(U_1))) | ssPv4(U_1) | ~ssPv1(U_445) | ~ssRr(U_445, skf3(U_1))))). % 19.85/10.22 tff(c_3765, plain, (![U_543]: (ssPv2(skf3(U_543)) | ssPv1(skf2(skf3(U_543))) | ssPv2(skf3(skf3(U_543))) | ~ssPv3(U_543)))). % 19.85/10.22 tff(c_3272, plain, (![U_1, U_506]: (ssPv2(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ssPv2(U_506) | ~ssPv3(U_1) | ~ssRr(U_506, skf3(U_1))))). % 19.85/10.22 tff(c_1072, plain, (![U_1, W_333, U_335]: (ssPv1(U_1) | ssPv3(W_333) | ~ssPv4(skf3(U_1)) | ~ssRr(W_333, skf3(U_1)) | ~ssPv2(U_335) | ~ssRr(U_335, skf3(U_1))))). % 19.85/10.22 tff(c_3716, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ssPv1(U_2) | ~ssPv2(U_2)))). % 19.85/10.22 tff(c_3559, plain, (![U_2, U_524]: (ssPv3(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ssPv1(U_2) | ~ssPv2(U_524) | ~ssRr(U_524, skf2(U_2))))). % 19.85/10.22 tff(c_3660, plain, (![U_532]: (ssPv1(skf2(skf2(U_532))) | ssPv2(U_532) | ssPv4(skf3(skf2(U_532))) | ~ssPv1(skf2(U_532))))). % 19.85/10.22 tff(c_2985, plain, (![U_2, U_495]: (ssPv1(skf2(skf2(U_2))) | ssPv2(U_2) | ssPv4(U_495) | ~ssPv1(skf2(U_2)) | ~ssRr(U_495, skf2(U_2))))). % 19.85/10.22 tff(c_3610, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ssPv1(skf3(skf2(U_2))) | ~ssPv2(U_2)))). % 19.85/10.22 tff(c_3558, plain, (![U_1, U_524]: (ssPv3(U_1) | ssPv2(skf2(U_1)) | ssPv1(skf3(U_1)) | ~ssPv2(U_524) | ~ssRr(U_524, U_1)))). % 19.85/10.22 tff(c_882, plain, (![U_2, W_303, U_304]: (ssPv2(U_2) | ~ssPv4(skf2(U_2)) | ~ssPv1(W_303) | ~ssRr(W_303, U_2) | ~ssPv4(U_304) | ~ssRr(U_304, U_2)))). % 19.85/10.22 tff(c_1244, plain, (![U_2, W_360, U_361]: (ssPv3(U_2) | ssPv2(skf2(U_2)) | ssPv1(W_360) | ~ssRr(W_360, U_2) | ~ssPv2(U_361) | ~ssRr(U_361, U_2)))). % 19.85/10.22 tff(c_1408, plain, (![W_376, U_377, U_2]: (ssPv1(W_376) | ssPv4(U_377) | ~ssPv1(U_2) | ~ssPv2(skf2(U_2)) | ~ssRr(W_376, U_2) | ~ssRr(U_377, U_2)))). % 19.85/10.22 tff(c_1693, plain, (![U_2, W_411, V_412]: (~ssPv2(U_2) | ~ssPv1(skf2(U_2)) | ~ssPv3(W_411) | ~ssRr(U_2, W_411) | ~ssPv4(V_412) | ~ssRr(U_2, V_412)))). % 19.85/10.22 tff(c_3273, plain, (![U_2, U_506]: (ssPv2(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_506) | ~ssPv3(skf2(U_2)) | ~ssRr(U_506, U_2)))). % 19.85/10.22 tff(c_1525, plain, (![U_2, U_388, W_389]: (ssPv2(U_2) | ssPv1(skf2(U_2)) | ssPv2(U_388) | ~ssPv3(W_389) | ~ssRr(U_2, W_389) | ~ssRr(U_388, U_2)))). % 19.85/10.22 tff(c_2991, plain, (![U_1]: (ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 19.85/10.22 tff(c_2984, plain, (![U_1, U_495]: (ssPv1(skf2(U_1)) | ssPv2(skf3(U_1)) | ssPv4(U_495) | ~ssPv1(U_1) | ~ssRr(U_495, U_1)))). % 19.85/10.22 tff(c_1003, plain, (![U_2, W_322, U_323]: (ssPv1(skf2(U_2)) | ssPv2(W_322) | ssPv4(U_323) | ~ssPv1(U_2) | ~ssRr(W_322, U_2) | ~ssRr(U_323, U_2)))). % 19.85/10.22 tff(c_1209, plain, (![U_2, W_352, U_353]: (ssPv3(U_2) | ssPv4(skf2(U_2)) | ~ssPv2(W_352) | ~ssRr(U_2, W_352) | ~ssPv1(U_353) | ~ssRr(U_353, U_2)))). % 19.85/10.22 tff(c_2422, plain, (![U_1, U_461]: (ssPv1(skf2(U_1)) | ssPv3(skf3(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_461) | ~ssRr(U_461, U_1)))). % 19.85/10.22 tff(c_1073, plain, (![U_2, W_333, U_335]: (ssPv1(skf2(U_2)) | ssPv3(W_333) | ~ssPv4(U_2) | ~ssRr(W_333, U_2) | ~ssPv2(U_335) | ~ssRr(U_335, U_2)))). % 19.85/10.22 tff(c_313, plain, (![U_192]: (ssPv1(U_192) | ssPv1(skf2(U_192)) | ~ssPv2(U_192) | ssPv3(U_192) | ssPv3(skf2(U_192)) | ~ssPv4(U_192)))). % 19.85/10.22 tff(c_1607, plain, (![U_2, W_395, V_396]: (ssPv1(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv1(W_395) | ~ssRr(U_2, W_395) | ~ssPv4(V_396) | ~ssRr(U_2, V_396)))). % 19.85/10.22 tff(c_2181, plain, (![U_2]: (ssPv4(skf2(U_2)) | ssPv2(skf2(skf2(U_2))) | ssPv4(skf2(skf2(U_2))) | ~ssPv1(U_2)))). % 19.85/10.22 tff(c_2174, plain, (![U_2, U_445]: (ssPv4(U_2) | ssPv2(skf2(U_2)) | ssPv4(skf2(U_2)) | ~ssPv1(U_445) | ~ssRr(U_445, U_2)))). % 19.85/10.22 tff(c_1643, plain, (![U_2, W_403, U_404]: (ssPv4(U_2) | ssPv2(skf2(U_2)) | ssPv4(W_403) | ~ssRr(U_2, W_403) | ~ssPv1(U_404) | ~ssRr(U_404, U_2)))). % 19.85/10.22 tff(c_1949, plain, (![U_431]: (ssPv3(skf3(U_431)) | ssPv3(U_431) | ssPv4(skf3(skf3(U_431))) | ~ssPv4(skf3(U_431))))). % 19.85/10.22 tff(c_297, plain, (![U_1, U_189]: (ssPv3(skf3(U_1)) | ssPv3(U_1) | ssPv4(U_189) | ~ssPv4(skf3(U_1)) | ~ssRr(U_189, skf3(U_1))))). % 19.85/10.22 tff(c_1840, plain, (![U_422]: (ssPv3(skf3(U_422)) | ssPv1(U_422) | ~ssPv4(skf3(U_422)) | ~ssPv1(skf2(skf3(U_422)))))). % 19.85/10.22 tff(c_674, plain, (![U_1, V_264]: (ssPv3(skf3(U_1)) | ssPv1(U_1) | ~ssPv4(skf3(U_1)) | ~ssPv1(V_264) | ~ssRr(skf3(U_1), V_264)))). % 19.85/10.22 tff(c_1829, plain, (![U_419]: (ssPv3(skf3(U_419)) | ssPv2(skf3(U_419)) | ssPv3(U_419) | ~ssPv1(skf3(skf3(U_419)))))). % 19.85/10.22 tff(c_511, plain, (![U_1, U_234]: (ssPv3(skf3(U_1)) | ssPv2(skf3(U_1)) | ssPv3(U_1) | ~ssPv1(U_234) | ~ssRr(U_234, skf3(U_1))))). % 19.85/10.22 tff(c_1686, plain, (![U_407]: (ssPv1(skf3(U_407)) | ssPv1(U_407) | ~ssPv2(skf3(U_407)) | ~ssPv4(skf3(skf3(U_407)))))). % 19.85/10.22 tff(c_84, plain, (![U_124, X_127, W_126, V_125]: (~ssPv2(U_124) | ~ssPv1(X_127) | ~ssRr(U_124, X_127) | ~ssPv3(W_126) | ~ssRr(U_124, W_126) | ~ssPv4(V_125) | ~ssRr(U_124, V_125)))). % 19.85/10.22 tff(c_227, plain, (![U_1, U_171]: (ssPv1(skf3(U_1)) | ssPv1(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_171) | ~ssRr(U_171, skf3(U_1))))). % 19.85/10.22 tff(c_62, plain, (![V_81, X_83, W_82, U_80]: (ssPv4(V_81) | ssPv2(X_83) | ssPv4(W_82) | ~ssRr(V_81, X_83) | ~ssRr(V_81, W_82) | ~ssPv1(U_80) | ~ssRr(U_80, V_81)))). % 19.85/10.22 tff(c_76, plain, (![X_111, U_108, W_110, V_109]: (ssPv1(X_111) | ~ssPv1(U_108) | ~ssRr(U_108, X_111) | ~ssPv1(W_110) | ~ssRr(U_108, W_110) | ~ssPv4(V_109) | ~ssRr(U_108, V_109)))). % 19.85/10.22 tff(c_66, plain, (![V_89, X_91, U_88, W_90]: (ssPv2(V_89) | ssPv1(X_91) | ssPv2(U_88) | ~ssRr(V_89, X_91) | ~ssPv3(W_90) | ~ssRr(V_89, W_90) | ~ssRr(U_88, V_89)))). % 19.85/10.22 tff(c_68, plain, (![W_94, U_92, V_93, X_95]: (ssPv1(W_94) | ssPv4(U_92) | ~ssPv1(V_93) | ~ssPv2(X_95) | ~ssRr(V_93, X_95) | ~ssRr(W_94, V_93) | ~ssRr(U_92, V_93)))). % 19.85/10.22 tff(c_1360, plain, (![U_373]: (ssPv3(skf3(U_373)) | ssPv2(U_373) | ~ssPv2(skf3(U_373)) | ~ssPv4(skf3(skf3(U_373)))))). % 19.85/10.22 tff(c_525, plain, (![U_1, U_239]: (ssPv3(skf3(U_1)) | ssPv2(U_1) | ~ssPv2(skf3(U_1)) | ~ssPv4(U_239) | ~ssRr(U_239, skf3(U_1))))). % 19.85/10.22 tff(c_78, plain, (![X_115, V_113, W_114, U_112]: (ssPv2(X_115) | ~ssPv1(V_113) | ~ssRr(V_113, X_115) | ~ssPv3(W_114) | ~ssRr(V_113, W_114) | ~ssPv2(U_112) | ~ssRr(U_112, V_113)))). % 19.85/10.22 tff(c_64, plain, (![V_85, X_87, W_86, U_84]: (ssPv3(V_85) | ssPv2(X_87) | ssPv1(W_86) | ~ssRr(V_85, X_87) | ~ssRr(W_86, V_85) | ~ssPv2(U_84) | ~ssRr(U_84, V_85)))). % 19.85/10.22 tff(c_70, plain, (![V_97, X_99, W_98, U_96]: (ssPv3(V_97) | ssPv4(X_99) | ~ssRr(V_97, X_99) | ~ssPv2(W_98) | ~ssRr(V_97, W_98) | ~ssPv1(U_96) | ~ssRr(U_96, V_97)))). % 19.85/10.22 tff(c_74, plain, (![V_105, W_106, X_107, U_104]: (ssPv4(V_105) | ssPv3(W_106) | ~ssPv1(X_107) | ~ssRr(V_105, X_107) | ~ssRr(W_106, V_105) | ~ssPv1(U_104) | ~ssRr(U_104, V_105)))). % 19.85/10.22 tff(c_586, plain, (![U_1, V_248]: (ssPv4(skf3(U_1)) | ssPv3(skf3(U_1)) | ssPv1(U_1) | ~ssPv1(V_248) | ~ssRr(skf3(U_1), V_248)))). % 19.85/10.22 tff(c_72, plain, (![X_103, W_102, V_101, U_100]: (ssPv1(X_103) | ssPv3(W_102) | ~ssPv4(V_101) | ~ssRr(V_101, X_103) | ~ssRr(W_102, V_101) | ~ssPv2(U_100) | ~ssRr(U_100, V_101)))). % 19.85/10.22 tff(c_1013, plain, (![U_325]: (ssPv2(skf3(U_325)) | ssPv3(U_325) | ~ssPv3(skf3(U_325)) | ~ssPv4(skf2(skf3(U_325)))))). % 20.01/10.22 tff(c_181, plain, (![U_1, V_157]: (ssPv2(skf3(U_1)) | ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv4(V_157) | ~ssRr(skf3(U_1), V_157)))). % 20.01/10.22 tff(c_60, plain, (![X_79, W_78, U_76, V_77]: (ssPv1(X_79) | ssPv2(W_78) | ssPv4(U_76) | ~ssPv1(V_77) | ~ssRr(V_77, X_79) | ~ssRr(W_78, V_77) | ~ssRr(U_76, V_77)))). % 20.01/10.22 tff(c_82, plain, (![W_122, V_121, X_123, U_120]: (ssPv2(W_122) | ~ssPv2(V_121) | ~ssPv2(X_123) | ~ssRr(V_121, X_123) | ~ssRr(W_122, V_121) | ~ssPv2(U_120) | ~ssRr(U_120, V_121)))). % 20.01/10.22 tff(c_918, plain, (![U_308]: (ssPv1(skf3(U_308)) | ssPv3(U_308) | ~ssPv3(skf3(U_308)) | ~ssPv3(skf3(skf3(U_308)))))). % 20.01/10.22 tff(c_421, plain, (![U_1, U_214]: (ssPv1(skf3(U_1)) | ssPv3(U_1) | ~ssPv3(skf3(U_1)) | ~ssPv3(U_214) | ~ssRr(U_214, skf3(U_1))))). % 20.01/10.22 tff(c_80, plain, (![V_117, X_119, W_118, U_116]: (ssPv2(V_117) | ~ssPv4(X_119) | ~ssRr(V_117, X_119) | ~ssPv1(W_118) | ~ssRr(W_118, V_117) | ~ssPv4(U_116) | ~ssRr(U_116, V_117)))). % 20.01/10.22 tff(c_769, plain, (![U_1]: (ssPv1(skf3(U_1)) | ssPv3(skf2(skf3(U_1))) | ~ssPv2(skf3(U_1)) | ~ssPv2(U_1)))). % 20.01/10.22 tff(c_763, plain, (![U_2, V_280]: (ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv2(V_280) | ~ssRr(U_2, V_280)))). % 20.01/10.22 tff(c_52, plain, (![U_64, W_66, V_65]: (ssPv1(U_64) | ssPv3(W_66) | ~ssPv2(U_64) | ~ssRr(U_64, W_66) | ~ssPv2(V_65) | ~ssRr(U_64, V_65)))). % 20.01/10.22 tff(c_717, plain, (![U_2]: (ssPv1(skf2(U_2)) | ssPv4(skf3(skf2(U_2))) | ~ssPv3(skf2(U_2)) | ~ssPv2(U_2)))). % 20.01/10.22 tff(c_705, plain, (![U_1, U_271]: (ssPv1(U_1) | ssPv4(skf3(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_271) | ~ssRr(U_271, U_1)))). % 20.01/10.22 tff(c_48, plain, (![V_59, W_60, U_58]: (ssPv1(V_59) | ssPv4(W_60) | ~ssPv3(V_59) | ~ssRr(W_60, V_59) | ~ssPv2(U_58) | ~ssRr(U_58, V_59)))). % 20.01/10.22 tff(c_681, plain, (![U_1]: (ssPv3(skf3(U_1)) | ssPv1(skf2(skf3(U_1))) | ~ssPv4(skf3(U_1)) | ~ssPv1(U_1)))). % 20.01/10.22 tff(c_675, plain, (![U_2, V_264]: (ssPv3(U_2) | ssPv1(skf2(U_2)) | ~ssPv4(U_2) | ~ssPv1(V_264) | ~ssRr(U_2, V_264)))). % 20.01/10.22 tff(c_38, plain, (![U_43, W_45, V_44]: (ssPv3(U_43) | ssPv1(W_45) | ~ssPv4(U_43) | ~ssRr(U_43, W_45) | ~ssPv1(V_44) | ~ssRr(U_43, V_44)))). % 20.01/10.22 tff(c_561, plain, (![U_1]: (ssPv2(skf2(U_1)) | ~ssPv2(U_1) | ssPv3(U_1) | ssPv3(skf2(U_1)) | ~ssPv4(U_1)))). % 20.01/10.22 tff(c_587, plain, (![U_2, V_248]: (ssPv4(U_2) | ssPv3(U_2) | ssPv1(skf2(U_2)) | ~ssPv1(V_248) | ~ssRr(U_2, V_248)))). % 20.01/10.22 tff(c_26, plain, (![U_25, W_27, V_26]: (ssPv4(U_25) | ssPv3(U_25) | ssPv1(W_27) | ~ssRr(U_25, W_27) | ~ssPv1(V_26) | ~ssRr(U_25, V_26)))). % 20.01/10.22 tff(c_545, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf2(U_1)) | ~ssPv2(U_1) | ~ssPv4(skf3(U_1))))). % 20.01/10.22 tff(c_526, plain, (![U_2, U_239]: (ssPv3(U_2) | ssPv2(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv4(U_239) | ~ssRr(U_239, U_2)))). % 20.01/10.22 tff(c_518, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv3(skf2(U_1)) | ~ssPv1(skf3(U_1))))). % 20.01/10.22 tff(c_40, plain, (![V_47, W_48, U_46]: (ssPv3(V_47) | ssPv2(W_48) | ~ssPv2(V_47) | ~ssRr(V_47, W_48) | ~ssPv4(U_46) | ~ssRr(U_46, V_47)))). % 20.01/10.22 tff(c_512, plain, (![U_2, U_234]: (ssPv3(U_2) | ssPv2(U_2) | ssPv3(skf2(U_2)) | ~ssPv1(U_234) | ~ssRr(U_234, U_2)))). % 20.01/10.22 tff(c_28, plain, (![V_29, W_30, U_28]: (ssPv3(V_29) | ssPv2(V_29) | ssPv3(W_30) | ~ssRr(V_29, W_30) | ~ssPv1(U_28) | ~ssRr(U_28, V_29)))). % 20.01/10.22 tff(c_44, plain, (![V_53, U_52, W_54]: (ssPv2(V_53) | ssPv4(U_52) | ~ssPv1(V_53) | ~ssPv1(W_54) | ~ssRr(V_53, W_54) | ~ssRr(U_52, V_53)))). % 20.01/10.23 tff(c_452, plain, (![U_2]: (ssPv4(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv3(skf2(U_2))))). % 20.01/10.23 tff(c_445, plain, (![U_2, V_220]: (ssPv4(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv3(V_220) | ~ssRr(U_2, V_220)))). % 20.01/10.23 tff(c_34, plain, (![U_37, W_39, V_38]: (ssPv4(U_37) | ssPv4(W_39) | ~ssPv1(U_37) | ~ssRr(U_37, W_39) | ~ssPv3(V_38) | ~ssRr(U_37, V_38)))). % 20.01/10.23 tff(c_428, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf2(U_1)) | ~ssPv3(U_1) | ~ssPv3(skf3(U_1))))). % 20.01/10.23 tff(c_422, plain, (![U_2, U_214]: (ssPv1(U_2) | ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv3(U_214) | ~ssRr(U_214, U_2)))). % 20.01/10.23 tff(c_50, plain, (![V_62, W_63, U_61]: (ssPv1(V_62) | ssPv3(W_63) | ~ssPv3(V_62) | ~ssRr(V_62, W_63) | ~ssPv3(U_61) | ~ssRr(U_61, V_62)))). % 20.01/10.23 tff(c_254, plain, (![U_1]: (ssPv2(skf3(U_1)) | ssPv4(skf2(skf3(U_1))) | ~ssPv1(skf3(U_1)) | ~ssPv4(U_1)))). % 20.01/10.23 tff(c_305, plain, (![U_2]: (ssPv3(skf2(U_2)) | ssPv3(skf2(skf2(U_2))) | ssPv4(U_2) | ~ssPv4(skf2(U_2))))). % 20.01/10.23 tff(c_36, plain, (![V_41, U_40, W_42]: (ssPv3(V_41) | ssPv3(U_40) | ~ssPv4(V_41) | ~ssPv2(W_42) | ~ssRr(V_41, W_42) | ~ssRr(U_40, V_41)))). % 20.01/10.23 tff(c_304, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf2(U_1)) | ssPv4(skf3(U_1)) | ~ssPv4(U_1)))). % 20.01/10.23 tff(c_298, plain, (![U_2, U_189]: (ssPv3(U_2) | ssPv3(skf2(U_2)) | ssPv4(U_189) | ~ssPv4(U_2) | ~ssRr(U_189, U_2)))). % 20.01/10.23 tff(c_24, plain, (![V_23, W_24, U_22]: (ssPv3(V_23) | ssPv3(W_24) | ssPv4(U_22) | ~ssPv4(V_23) | ~ssRr(V_23, W_24) | ~ssRr(U_22, V_23)))). % 20.01/10.23 tff(c_261, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf2(U_1)) | ~ssPv2(U_1) | ~ssPv4(skf3(U_1))))). % 20.01/10.23 tff(c_228, plain, (![U_2, U_171]: (ssPv1(U_2) | ssPv1(skf2(U_2)) | ~ssPv2(U_2) | ~ssPv4(U_171) | ~ssRr(U_171, U_2)))). % 20.01/10.23 tff(c_206, plain, (![U_2, V_165]: (ssPv2(U_2) | ssPv4(skf2(U_2)) | ~ssPv1(U_2) | ~ssPv4(V_165) | ~ssRr(U_2, V_165)))). % 20.01/10.23 tff(c_235, plain, (![U_2]: (ssPv2(U_2) | ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv4(skf2(U_2))))). % 20.01/10.23 tff(c_182, plain, (![U_2, V_157]: (ssPv2(U_2) | ssPv3(skf2(U_2)) | ~ssPv3(U_2) | ~ssPv4(V_157) | ~ssRr(U_2, V_157)))). % 20.01/10.23 tff(c_54, plain, (![V_68, W_69, U_67]: (ssPv1(V_68) | ssPv1(W_69) | ~ssPv2(V_68) | ~ssRr(V_68, W_69) | ~ssPv4(U_67) | ~ssRr(U_67, V_68)))). % 20.01/10.23 tff(c_46, plain, (![U_55, W_57, V_56]: (ssPv2(U_55) | ssPv4(W_57) | ~ssPv1(U_55) | ~ssRr(U_55, W_57) | ~ssPv4(V_56) | ~ssRr(U_55, V_56)))). % 20.01/10.23 tff(c_42, plain, (![U_49, W_51, V_50]: (ssPv2(U_49) | ssPv3(W_51) | ~ssPv3(U_49) | ~ssRr(U_49, W_51) | ~ssPv4(V_50) | ~ssRr(U_49, V_50)))). % 20.01/10.23 tff(c_145, plain, (![U_2]: (ssPv4(U_2) | ssPv2(U_2) | ~ssPv3(U_2) | ~ssPv3(skf2(U_2))))). % 20.01/10.23 tff(c_12, plain, (![U_9, V_10]: (ssPv4(U_9) | ssPv2(U_9) | ~ssPv3(U_9) | ~ssPv3(V_10) | ~ssRr(U_9, V_10)))). % 20.01/10.23 tff(c_104, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv3(skf3(U_1))))). % 20.01/10.23 tff(c_14, plain, (![V_12, U_11]: (ssPv3(V_12) | ssPv2(V_12) | ~ssPv1(V_12) | ~ssPv3(U_11) | ~ssRr(U_11, V_12)))). % 20.01/10.23 tff(c_2, plain, (![U_1]: (ssRr(skf3(U_1), U_1)))). % 20.01/10.23 tff(c_4, plain, (![U_2]: (ssRr(U_2, skf2(U_2))))). % 20.01/10.23 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.01/10.23 %------------------------------------------------------------------------------